# 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.

datatype rel =
`<   of term * term
| `<=  of term * term
| `=   of term * term
| `<>  of term * term
| `>=  of term * term
| `>   of term * term

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.

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

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.