alice
library
manual.

The `Linear` structure

^Synopsis^{____________________________________________}

    signature LINEAR
    structure Linear : LINEAR

The Linear structure provides functionality to post linear equality constraints using a convenient infix operator syntax.

Notes:

The linear module maps linear constraints onto regular sum constraints of the FD module. This transformation is not always optimal, that is, one might be able to devise a better constraint manually.

Note also that since the linear module extensively performs folding of constant expressions, it eventually might exceed the implementation specific integer constant limit of finite domain constraints. In such a case, folding can be prevented by introducing a finite domain variable that is assigned a singleton value.

^Import^{______________________________________________}

    import signature LINEAR from "x-alice:/lib/constraints/LINEAR-sig"
    import structure Linear from "x-alice:/lib/constraints/Linear"

^Interface^{___________________________________________}

signature LINEAR =
sig
	type space
	type intvar
	type boolvar

        datatype conlevel = 
	         BND | DEF | DOM | VAL

	infix  7  `*
	infix  6  `+ `-
	infix  5  `#
	infix  4  `= `<> `> `>= `< `<=

	infix  3  `->
	infix  3  `<-
	infix  3  `==
	infix  3  `&
	infix  3  `|
	infix  3  XOR


	datatype domain_element =
	    `` of int
	  | `# of int * int

	type domain = domain_element list

	datatype b_var_sel =
	    B_DEGREE_MAX
	  | B_DEGREE_MIN
	  | B_MAX_MAX
	  | B_MAX_MIN
	  | B_MIN_MAX
	  | B_MIN_MIN
	  | B_NONE
	  | B_SIZE_MAX
	  | B_SIZE_MIN
	    
	datatype b_val_sel =
	    B_MAX
	  | B_MED
	  | B_MIN
	  | B_SPLIT_MAX
	  | B_SPLIT_MIN

	datatype term =
	    FD of intvar
	  | `  of int
	  | `+ of term * term
	  | `- of term * term
	  | `* of term * term

	datatype rel =
	    `<   of term * term
	  | `<=  of term * term
	  | `=   of term * term
	  | `<>  of term * term
	  | `>=  of term * term
	  | `>   of term * term
	 
	val fdterm : space * domain -> term
	val fdtermVec : space * int * domain -> term vector
	
	val post : space * rel * conlevel -> unit

	val distinct : space * term vector * conlevel -> unit
	val branch : space * term vector * b_var_sel * b_val_sel -> unit

	datatype b_term = 
	  BV of boolvar
	 | BC of bool
	 | HOLDS of rel
	 | `== of b_term * b_term
	 | `-> of b_term * b_term
	 | `<- of b_term * b_term
	 | `! of b_term
	 | `& of b_term * b_term
	 | XOR of b_term * b_term
	 | `| of b_term * b_term

	val boolterm : space -> b_term
	val booltermVec : space * int -> b_term vector

	val postTrue : space * b_term -> unit

    end

^Description^{_________________________________________}

type space

The type of first class comutational spaces. Usually equal to SPACE.space.

type intvar

The type of finite domain variables.

type boolvar

The type of boolean constraint variables. Fundamentally, they are FD variables constrained to the 0-1 domain.

datatype conlevel

Type to identify the eagerness of propagation. When the required level is not implemented for a propagator, the closest, stricter version is used.
DOM: Domain Proagatin. Strictest.
BND: Bounds Propagation.
VAL: Value Propagation. Most loose.

DEF: The default for the propagator.

datatype domain_element = `` of int | `# of int *int type domain = domain_element list

Used to describe domains of finite domain variables. `` i denotes the single integer value i and >`#(l,h) denotes all integer values between l and h. For example, [``3,`#(5,10)] denotes [3,5,6,7,8,9,10].

datatype term = FD of FD.fd | ` of int | `+ of term * term | `- of term * term | `* of term * term

This datatype is used to post arithmetic constraints.

FD x injects the finite domain variable x into a term.
` i injects a integer value i into a term.
x `+ y denotes the sum of x and y.
x `- y denotes the difference of x and y.
x `* y denotes the product of x and y.

This datatype is used to post linear equations.

x `< y denotes that x is less than y.
x `<= y denotes that x is less than or equal to y.
x `= y denotes that x equals y.
x `<> y denotes that x is not equal to y.
x `>= y denotes that x is greater than or equal to y.
x `> y denotes that x is greater than y.

fdterm (s, d)

returns a freshly created finite domain variable term initialized with d.

fdtermVec (s, n, d)

returns a vector of n freshly created finite domain variable terms initialized with d.

post (s,r,cl)

post the constraint denoted by r in space s using consistency level cl.

distinct (s,v,cl)

post the constraint that all variables in the vector v in space s have to be distinct using consistency level cl. If the vector contains terms other than FD variables, an exception is thrown.

branch (s,v,b_var_sel,b_val_sel)

post a branching on the variables in the vector v in space s, with b_var_sel and b_val_sel as the branching strategies. If the vector contains terms other than FD variables, an exception is thrown.

This datatype is used to post boolean constraints.

BV b injects the true/false domain variable b into a term.
BC c injects the boolean value c into a term.
HOLDS f denotes that the term f is true. This means that the term f is reified to a bolean variable.
b1 `== b2 denotes that the two boolean terms b1 and b2 are equivalent.
b1 `-> b2 denotes that b1 implies b2.
b1 `<- b2 denotes that b2 implies b1.
`! b denotes the negation of b.
b1 `& b2 denotes the conjunction of b1 andb2.
b1 XOR b2 denotes the exclusive disjunction of b1 andb2.
b1 `| b2 denotes the disjunction of b1 andb2.

boolterm s

returns a freshly created true/false domain variable term.

booltermVec (s, n)

returns a vector of n freshly created true/false domain variable terms.

postTrue (s, t)

post the constraint that the boolean term denoted by t holds in space s.

last modified 2005/Aug/03 09:17

alice library manual.

The Linear structure

________ Synopsis ____________________________________________________

________ Import ______________________________________________________