The module FD supports finite domain programming. A variable or a list of variables is constrained to a finite domain by
x::d | x:::d | x\::d | x\:::d where d ::= i |i#i | [(i|i#i)]
Finite domain infix operators all have a colon as the last character. The expressions containing the infix operators ::, :::, \::, and \::: are translated into calls of the procedures FD.dom, FD.doms, FD.coDom, and FD.coDoms, respectively, where the arguments are switched to allow for nesting. Oz provides so called propagators for finite domain programming by the infix expressions
s=:t | s<:t | s>:t | s=<:t | s>=:t | s\=:t where s,t ::= s+t | s-t | s*t | (s) | x | i
A propagator reads and amplifies the constraint store. The operational semantics of a propagator is sound but usually incomplete with respect to the declarative semantics of the corresponding logic constraint. As an example consider
X::1#3 Y::1#6 2*X=:YFirst X is constrained to an integer between 1 and 3 and Y to an integer between 1 and 6. Then the value 1 is discarded from Y but 3 and 5 remain, though they cannot contribute to a solution of the corresponding logic constraint 2*X=Y. The set of integers between the lower and upper bound of a variable's domain is called the completed domain (a domain of a variable is the greatest set of possible integers for the variable. Almost all of the propagators enforce interval-consistency (for the sake of efficiency), i.e., the propagator imposes constraints such that for the lower and upper bound of a variable's domain there exist integers in the completed domains of the other constrained variables such that the logic reading is true. If this is not possible, the propagator is discarded and the computation space is failed. A propagator ceases to exist, if for all possible valuations resulting from the completed domains of constrained variables, the logic reading is true (the logic reading is interval-entailed). In this case we say that Oz provides for interval-consistency and -entailment for this propagator. For all procedures in the sections on arithmetical and boolean constraints, Oz provides also for interval-consistency and -entailment. A propagator resulting from an infix comparison suspends until all occurring variables are constrained to finite domains and the terms are linear. For a more detailed description of the semantics and how to use constraints see Constraint Programming in Oz [9] .
{FiniteDomain D}
FD.fd=FiniteDomain
D is constrained to a finite domain, i.e. D may be bound to an integer between 0 and FD.bound.
{dom +X D}
D is constrained to a finite domain specified by X, which must be an integer, a pair of integers (denoting a range) or a list of integers and pairs. If X is a list, D is constrained to the union of the contained integers and ranges.
{doms +X Ds}
All elements of Ds are constrained to finite domains specified by X (for a description of X see FD.dom).
{coDom +X D}
D is constrained to a finite domain specified by 0... FD.bound without the domain represented by X (for a description of X see FD.dom).
{coDoms +X Ds}
All elements of Ds are constrained to finite domains specified by 0... FD.bound without the domain represented by X (for a description of X see FD.dom).
{is +D}
D is a finite domain.
{'+' D1 D2 D3}
D3 is the sum of D1 and D2.
{'-' D1 D2 D3}
D3 is the difference between D1 and D2.
{'*' D1 D2 D3}
D3 is the product of D1 and D2. {FD.'*' X Y Z} is an abbreviation for X*Y=<:Z and X*Y>=:Z where Oz provides for interval-consistency and -entailment.
{'<' +D1 +D2}
D1 is less than D2.
{'=<' +D1 +D2}
D1 is less than or equal to D2.
{'>' +D1 +D2}
D1 is greater than D2.
{'>=' +D1 +D2}
D1 is greater than or equal to D2.
{'div' D1 D2 D3}
D3 is the result of the integer division of D1 by D2.
{'mod' D1 D2 D3}
D3 is the result of D1 modulus D2.
{max D1 D2 D3}
D3 is the maximum of D1 and D2.
{min D1 D2 D3}
D3 is the minimum of D1 and D2.
{FiniteDomainNE +D +I}
FD.ne=FiniteDomainNE
D is constrained to be different from I.
{allDifferent +Ds}
All elements of Ds are pairwise different. Oz provides for interval-consistency but not -entailment.
{union D1 D2 D3}
The domain of D3 is the union of the domains of D1 and D2. For propagation the whole domain is considered, not only the bounds. Oz provides for domain-consistency and -entailment (see Constraint Programming in Oz [9] ).
{abs +Is +Ds +I D}
Is and Ds must be lists of integers [ I_1... I_n ] and finite domains [ D_1... D_n ] with the same length, respectively. The declarative semantics is the equation | I_1* D_1 + ... + I_n* D_n + I|=\ MVD, where | E| denotes the absolute value of E. The application is an abbreviation for two ineqations similar to FD.'*' where Oz provides for interval-consistency and -entailment.
{genEq +Is +Ds +I}
{genLeq +Is +Ds +I}
{genNeq +Is +Ds +I}
Is and Ds must be lists of integers [ I_1... I_n ] and finite domains [ D_1... D_n ] with the same length, respectively. The application is equivalent to the finite domain expression I_1 * D_1 +... + I_n * D_n + I =:0, I_1 * D_1 +... + I_n * D_n + I =<:0, I_1 * D_1 +... + I_n * D_n + I =¯:0, respectively (see The Oz Notation [2] and Constraint Programming in Oz [9] ).
{genEqNL +Is +Dss +I}
{genLeqNL +Is +Dss +I}
{genNeqNL +Is +Dss +I}
Is and Dss must be lists of integers [ I_1... I_n ] and lists of lists of finite domains [[ D_11... D_1n_1 ]... [ D_n1... D_nn_n ]]. The application is equivalent to the finite domain expression I_1 * D_11 * D_1n_1 +... + I_n * D_n1 * D_nn_n + I =:0 (and the corresponding disequations and inequations, respectively, see The Oz Notation [2] and Constraint Programming in Oz [9] ).
{genEqNLProp +Is +Dss +I}
{genLeqNLProp +Is +Dss +I}
Is and Dss must be lists of integers [ I_1... I_n ] and lists of lists of finite domains [[ D_11... D_1n_1 ]... [ D_n1... D_nn_n ]]. This propagator is a more propagating version than FD.genEqNL and FD.genLeqNL. See Constraint Programming in Oz [9] for more details.
{bool D}
D is constrained to be 0 or 1.
{bools +Ds}
FD.bool is applied to all elements of Ds.
{con D1 D2 D3}
D3 is the conjunction of D1 and D2.
{dis D1 D2 D3}
D3 is the disjunction of D1 and D2.
{xor D1 D2 D3}
D3 is the exclusive disjunction of D1 and D2.
{neg D1 D2}
D2 is the negation of D1.
{imp D1 D2 D3}
D3 is the implication of D2 by D1 (" D1-> D2").
{equ D1 D2 D3}
D3 is the equivalence of D1 by D2 (" D1<-> D2").
Most of the following operators allow to check whether a constraint is entailed (but can also be used for imposing the constraint). These operators are used for implementation of the cardinality operator as defined in [13].
{domB +X D1 D2}
{domsB +X Ds D}
{coDomB +X D1 D2}
{coDomsB +X Ds D}
For FD.domB, D2 is constrained to the finite domain {0,1} and X by applying {FD.fd X}. D2 is constrained to 1 if and only if D1 is constrained to a finite domain specified by X (see also FD.dom). The other propagators are defined analogously.
{genEqB +Is +Ds +I D}
{genLeqB +Is +Ds +I D}
{genNeqB +Is +Ds +I D}
Is and Ds must be lists of integers [ I_1... I_n ] and finite domains [ D_1... D_n ] with the same length, respectively. D is constrained to the finite domain {0,1}. For FD.genEqB, D is constrained to 1 if and only if the equation I_1* D_1+...+ I_n* D_n+ I=0 holds. The other propagators are defined analogously.
{genEqNLB +Is +Dss +I D}
{genLeqNLB +Is +Dss +I D}
{genNeqNLB +Is +Dss +I D}
Is and Dss must be lists of integers [ I_1... I_n ] and lists of lists of finite domains [[ D_11... D_1n_1 ]... [ D_n1... D_nn_n ]]. D is constrained to the finite domain {0,1}. For FD.genEqNLB, D is constrained to 1 if and only if the equation I_1* D_11* D_1n_1+...+ I_n* D_n1* D_nn_n+ I=0 holds. The other propagators are defined analogously.
{genCard +D1 +Ps +D2}
Ps is a list of nullary procedures. The number of succeeding procedures in Ps is at least D1 and at most D2.
{card +D1 +Ds +D2 +D3}
D3 and the elements of Ds are constrained to variables with domain {0,1}. D3 is constrained to 1 if and only if the sum of the elements of Ds is at least D1 and at most D2.
{atMost +I1 +Ds +I2}
{atLeast +I1 +Ds +I2}
{atCount +I1 +Ds +I2}
At most, at least, exactly I1 elements of Ds may be equal to I2, respectively.
{element +D1 +Is +D2}
If both D1 and D2 are constrained to integers, the D1-th element of Is is the integer D2. In the general case, for each integer i in the domain of D1, the i-th element of Is is in the domain of D2. For each value j in the domain of D2, all positions where j occurs in Is are in the domain of D1.
The following procedures are useful in combination with search to assign values to finite domains. They spawn a binary disjunction such that in the body of one alternative (or in both alternatives) a recursive call of the procedure occurs.
{enum +D}
Spawns a disjunction such that in one alternative the current minimum of D is assigned to D, while in the other alternative this value is excluded from D and FD.enum is called recursively in the body. If D is an integer, no disjunction is spawned.
{enums +Ds}
From Ds the leftmost D with the smallest domain (different from an integer) is chosen. A disjunction is spawned such that in one alternative the current minimum of D is assigned to D. In the other alternative this value is excluded from D and FD.enums is called recursively in the body (the order in Ds is preserved).
{enumSplit +D}
The domain is split in the middle into a lower and an upper half. A disjunction is spawned such that in the two alternatives D is constrained to these halves, respectively, and FD.enumSplit is called recursively in both bodies.
{enumSplits +Ds}
A D is chosen like in procedure FD.enums from Ds. A disjunction is elaborated like in FD.enumSplit and in both alternatives the procedure FD.enumSplits is called recursively in both bodies (with integers removed from Ds).
{getMin +D ?I}
I is the current minimum of the domain of D.
{getMax +D ?I}
I is the current maximum of the domain of D.
{getNextTo +D1 +D2 ?IT}
IT is the value in the domain of D1, which is nearest to D2. If there are two integers equally near to D2, IT is bound to the pair of both integers.
{getSize +D ?I}
I is the current size of the domain of D.
{GetFiniteDomain +D ?Is}
FD.get=GetFiniteDomain
Is is a list of integers representing the domain of D.
{getDomCompact +D ?X}
X is the representation of the domain of D where the specification described for FD.dom is used.
FD.bound=FiniteDomainBound
The largest possible upper bound of a finite domain as defined by the implementation.