alice
library
manual.

The `Modeling` structure

^Synopsis^{____________________________________________}

    signature MODELING
    structure Modeling : MODELING

The Modeling structure provides functionality to post arithmetic constraints using a convenient infix operator syntax.

Notes:

This module maps 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 this 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 MODELING from "x-alice:/lib/gecode/MODELING-sig"
    import structure Modeling from "x-alice:/lib/gecode/Modeling"

^Interface^{___________________________________________}

signature MODELING =
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_REGRET_MAX_MAX
      | B_REGRET_MAX_MIN
      | B_REGRET_MIN_MAX
      | B_REGRET_MIN_MIN
      | 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
      | SUMV of intvar vector
	
    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 equations, inequations, and disequations.

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 2007/Mar/30 17:10

alice library manual.

The Modeling structure

________ Synopsis ____________________________________________________

________ Import ______________________________________________________