signature FD structure FD : FD
The FD structure provides access to finite domain variables and propagators.
Finite domain variables are variables whose values are non-negative integers.
If a propagator is invoked, it tries to narrow the domains of the variables it is posted on. The amount of narrowing of domains depends on the operational semantics of the propagator. There are two main schemes for the operational semantics of a propagator. Domain propagation means that the propagator narrows the domains such that all values are discarded, which are not contained in a solution of the modeled constraint. But due to efficiency reasons, most propagators provide only interval propagation, i. e. only the bounds of domains are narrowed. For some propagators, there is an operational semantics in between both schemes.
A propagator ceases to exist if all the variables it is posted on are determined. In the following sections, only exceptions from this rule are mentioned, i. e. if the propagator ceases to exist earlier. For example, FD.lessEq(x, y) ceases to exist if the current upper bound of x is smaller than or equal to the current lower bound of y.
Note that every propagator creation can raise a Tell exception if it is performed on toplevel and the constraint is inconsistent with other constraints.
import signature FD from "x-alice:/lib/constraints/FD-sig" import structure FD from "x-alice:/lib/constraints/FD"
signature FD = sig type fd type bin = fd exception Tell of {cause : exn} datatype domain_element = SINGLE of int | RANGE of int * int type domain = domain_element vector datatype relation = LESS | LESSEQ | EQUAL | NOTEQUAL | GREATER | GREATEREQ datatype dist_mode = NAIVE | FIRSTFAIL | SPLIT_MIN | SPLIT_MAX | NBSUSPS datatype assign = MIN | MID | MAX (* Implementation dependent fd limits *) val inf : int val sup : int (* Allocation Functions *) val fd : domain option -> fd (* Domain, Overflow *) val fdVec : int * domain -> fd vector (* Domain, Overflow *) val range : int * int -> fd (* Domain, Overflow *) val rangeVec : int * (int * int) -> fd vector (* Domain, Overflow *) val bin : unit -> bin val binVec : int -> bin (* Assignment *) val assign : assign * fd vector -> unit (* Conversion *) val toInt : fd -> int val future : fd -> int val fromInt : int -> fd val isBin : fd -> bool (* Standards Sums *) val sum : fd vector * relation * fd -> unit val sumC : (int * fd) vector * relation * fd -> unit val sumAC : (int * fd) vector * relation * fd -> unit val sumCN : (int * fd vector) vector * relation * fd -> unit val sumACN : (int * fd vector) vector * relation * fd -> unit val sumD : fd vector * relation * fd -> unit val sumCD : (int * fd) vector * relation * fd -> unit (* Standard Propagators; Interval propagation *) val plus : fd * fd * fd -> unit (* X + Y =: Z *) val minus : fd * fd * fd -> unit (* X - Y =: Z *) val times : fd * fd * fd -> unit (* X * Y =: Z *) val power : fd * int * fd -> unit (* pow(X, I) =: Z *) val divI : fd * int * fd -> unit (* X divI I =: Z *) val modI : fd * int * fd -> unit (* X modI I =: Z *) (* Standard Propagators; Domain propagation *) val plusD : fd * fd * fd -> unit (* X + Y =: Z *) val minusD : fd * fd * fd -> unit (* X - Y =: Z *) val timesD : fd * fd * fd -> unit (* X * Y =: Z *) val divD : fd * int * fd -> unit (* X divD I =: Z *) val modD : fd * int * fd -> unit (* X modD I =: Z *) val min : fd * fd * fd -> unit (* min(X, Y) =: Z *) val max : fd * fd * fd -> unit (* max(X, Y) =: Z *) val equal : fd * fd -> unit (* X =: Y *) val notequal : fd * fd -> unit (* X \=: Y *) val distance : fd * fd * relation * fd -> unit val less : fd * fd -> unit (* X <: Y *) val lessEq : fd * fd -> unit (* X <=: Y *) val greater : fd * fd -> unit (* X >: Y *) val greaterEq : fd * fd -> unit (* X >=: Y *) val disjoint : fd * int * fd * int -> unit val disjointC : fd * int * fd * int * bin -> unit val tasksOverlap : fd * int * fd * int * bin -> unit (* Non-Linear Propagators *) val distinct : fd vector -> unit val distinctOffset : (fd * int) vector -> unit val distinct2 : ((fd * int) * (fd * int)) vector -> unit val atMost : fd * fd vector * int -> unit val atLeast : fd * fd vector * int -> unit val exactly : fd * fd vector * int -> unit val element : fd * int vector * fd -> unit (* 0/1 Propagators *) val conj : bin * bin * bin -> unit val disj : bin * bin * bin -> unit val exor : bin * bin * bin -> unit val nega : bin * bin -> unit val impl : bin * bin * bin -> unit val equi : bin * bin * bin -> unit (* Reified Constraints *) structure Reified : sig (* Reified Variable is returned *) val fd : domain * bin -> fd (* Domain, Overflow *) (* Reified Vector of Variables is returned *) val fdVec : int * domain * bin -> fd vector (* Domain, Overflow *) (* Same as in Oz *) val card : int * bin vector * int * bin -> unit val distance : fd * fd * relation * fd * bin -> unit val sum : fd vector * relation * fd * bin -> unit val sumC : (int * fd) vector * relation * fd * bin -> unit val sumAC : (int * fd) vector * relation * fd * bin -> unit val sumCN : (int * fd vector) vector * relation * fd * bin -> unit val sumACN : (int * fd vector) vector * relation * fd * bin -> unit end (* Reflection *) structure Reflect : sig val min : fd -> int val max : fd -> int val mid : fd -> int val nextLarger : fd * int -> int val nextSmaller : fd * int -> int val size : fd -> int val dom : fd -> domain val domList : fd -> int list val nbSusps : fd -> int val eq : fd * fd -> bool (* token eq *) end (* Watching *) structure Watch : sig val min : fd * int -> bool val max : fd * int -> bool val size : fd * int -> bool end (* Distribution *) val distribute : dist_mode * fd vector -> unit val choose : dist_mode * fd vector -> fd * domain (* Scheduling Stuff *) structure Schedule : sig type tasks = (string * string list) vector type starts = (string * fd) vector type specs = (string * int) vector val cumulative : tasks * starts * specs * specs * specs -> unit val cumulativeEF : tasks * starts * specs * specs * specs -> unit val cumulativeTI : tasks * starts * specs * specs * specs -> unit val cumulativeUp : tasks * starts * specs * specs * specs -> unit val disjoint : fd * int * fd * int -> unit val firstsDist : tasks * starts * specs -> unit val lastsDist : tasks * starts * specs -> unit val firstsLastsDist : tasks * starts * specs -> unit val taskIntervalsDistP : tasks * starts * specs -> unit val taskIntervalsDistO : tasks * starts * specs -> unit val serializedDisj : tasks * starts * specs -> unit val serialized : tasks * starts * specs -> unit val taskIntervals : tasks * starts * specs -> unit end end
The type of finite domain variables. The type bin is used to indicate boolean 0/1 variables.
is raised when a propagator is created on toplevel and is inconsistent with other constraints.
The type of finite domains. Use SINGLE i to specify a single integer i and RANGE(il, ih) to specify a value domain [il, il + 1, ..., ih], presuming that ih is greater than or equal to il.
For example, the value #[SINGLE(5), RANGE(7, 10)] specifies the domain [5,7,8,9,10].
This is the datatype to denote a arithmetic relation which is given to generic propagators as an argument.
This datatype is used to denote the distribution stragety which is given to the FD.distribute function.
This datatype is used to assign implementation dependent values to finite domain variables. MIN denotes the minimal integer value, MAX denotes the maximal integer value and MID the medium value.
denotes the implementation dependent lower bound of a fd variable.
denotes the implementation dependent upper bound of a fd variable.
returns a freshly created finite domain variable initialized with the given domain dom. In case dom equals to NONE, the maximal domain [MIN, MIN + 1, ..., MAX] is used.
returns a vector of freshly created finite domain variables. The vector has size n and all variables are initialized with the domain denoted by dom.
convenience abbreviation for fd (SOME (#[RANGE(il, ih)])).
convenience abbreviation for fdVec (n,#[RANGE(il, ih)]).
convenience abbreviation for fd (SOME (#[RANGE(0, 1)])).
convenience abbreviation for fdVec (n,#[RANGE(0, 1)]).
Every finite domain variable contained in vector v is assigned the value denoted by as, that is, either the minimal, medium or maximal value possible.
returns the integer value i denoted by the finite domain variable is returned, presuming that f has a singleton domain.
returns the integer value i denoted by the finite domain variable is returned, presuming that f has a singleton domain.
returns a freshly created finite domain variable initialized with the singleton domain #[SINGLE i].
returns true iff f is 0/1 variable, false otherwise.
creates a propagator for
v1 + ... + vn - r rel 0
For the precise operational semantics, see here.
In case, rel denotes NOTEQUAL, the propagator waits until at most one non-determined variable is left. Then the appropriate value is discarded from the variable's domain. For the other relations, the propagator does interval propagation.
creates a propagator for
i1 * v1 + ... + in * vn - r rel 0
For the precise operational semantics, see here.
creates a propagator for the absolute value of the scalar product
|iv * v| = |i1 * v1 + ... + in * vn| rel r
For the precise operational semantics, see here.
creates a propagator for
i1 * v1 * ... * v1m1 + ... + in * vn1 * ... *vnmn - r rel 0
For the precise operational semantics, see here.
creates a propagator for
|i1 * v1 * ... * v1m1 + ... + in * vn1 * ... *vnmn| rel r
For the precise operational semantics, see here.
creates a propagator analogous to sum but performs domain propagation. Note that only equality (EQUAL) and non-equality are supported (NOTEQUAL), as for inequalities domain and bounds propagation are equivalent
creates a propagator analogous to sumC but performs domain propagation. Note that only equality (EQUAL) and non-equality are supported (NOTEQUAL), as for inequalities domain and bounds propagation are equivalent
z is the sum of x and y. The propagator constraints its arguments as X + Y = Z.
z is the difference of x and y. The propagator constraints its arguments as X - Y = Z.
z is the product of x and y. Coreferences are exploited. If the store entails X = Z, the propagator ceases to exist and the constraint Y = 1 is imposed. If the store entails Y = Z, the propagator ceases to exist and the constraint X = 1 is imposed. If the store entails X = Y, the propagator ceases to exist and a propagator is imposed instead, which constrains the variables X and Y as described here.
z is the result of x raised to the power of i. The propagator constrains the variables X and Y as described here.
z is the result of the integer division of x by i.
A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if x = z, the propagator is replaced by I = 1.
z is the result of x modulus i.
A domain bound is discarded from the domain of one variable, if there is no value between the lower and upper bound of the domain of the other variable, such that the constraint holds. Additionally, if x = z, the propagator is replaced by x < i. If the current upper bound of x is less than i, the propagator is replaced by x=z.
z is the sum of x and y. The propagator constraints its arguments as X + Y = Z.
Does domain propagation, which can be very expensive.
z is the difference of x and y. The propagator constraints its arguments as X - Y = Z.
Does domain propagation, which can be very expensive.
z is the product of x and y.
Does domain propagation, which can be very expensive.
z is the result of the integer division of x by i.
Does domain propagation, which can be very expensive.
z is the result of x modulus i.
Does domain propagation, which can be very expensive.
z is the minimum of x modulus y.
For precise operational semantics, see here.
z is the maximum of x and y.
For precise operational semantics, see here.
Post the constraint that x equals y.
Post the constraint that x does not equal y.
creates a propagator for
|x - y| rel z
May cut holes into domains.
This propagator is equivalent to sumAC(#[(1, x), (~1, y)], rel, z) but is more efficient.
Post the constraint that x is less than y.
Post the constraint that x is less than or equal to y.
Post the constraint that x is greater than y.
Post the constraint that x is greater than or equal to y.
creates a propagator for
x + i1 <= y or y + i2 <= x
May cut holes into the domains.
For precise operational semantics, see here.
creates a propagator for
((x + i1 <= y) and (c = 0)) or ((y + i2 <= x) and (c = 1))
May cut holes into the domains.
For precise operational semantics, see here.
For operational semantics, see here.
All elements in v are pairwise distinct. If one element becomes determined, the remaining elements are constrained to be different from it. If two variables become equal, the propagator fails, e. g. FD.distinct #[a,a, b] will fail even if a is not determined.
All sums di + ii are pairwise distinct. If one becomes determined, the remaining elements dj are constrained to be different from di + ii - ij.
For operational semantics, see here.
Post the constraint that at most x elements of v are equal to i.
For precise operational semantics, see here.
Post the constraint that at least x elements of v are equal to i.
For precise operational semantics, see here.
Post the constraint that exactly x elements of v are equal to i.
For precise operational semantics, see here.
Post the constraint that the xth element of v is z.
It propagates as follows. For each integer i in the domain of x, the i-th element of v is in the domain of z; and no other values. For each value j in the domain of z, all positions where j occurs in v are in the domain of x; and no other values.
z is the conjunction of x and y.
For operational semantics, see here.
z is the disjunction of x and y.
z is the exclusive disjunction of x and y.
y is the negation of x.
z is the implication of x by y (x -> y).
z is the equivalence of x by y (x <-> y).
returns a freshly created finite domain variable which is initialized with dom and reified into c.
returns a vector of size n of finite domain variables. Each variable is initialized with dom and reified into c.
For detailed documentation, see here.
Reifies sum(v, rel, r) into c.
Reifies sumC(v, rel, r) into c.
Reifies sumAC(v, rel, r) into c.
Reifies sumCN(v, rel, r) into c.
returns the current lower bound of x.
returns the current upper bound of x.
returns the integer which is closest to the middle of the current domain (the arithmetical means of the lower and upper bound of x). In case of ties, the smaller element is selected.
returns the smallest integer in the domain of x which is larger than i.
returns the largest integer in the domain of x which is smaller than i.
returns the size of the current domain of x.
returns the the current domain of x.
returns the the current domain of x as an ordered list of integers.
returns the the current number of suspensions on x.
returns true iff x and y denote the same variable, false otherwise.
v is distributed according to the distribution spec spec:
selects a element e from v according to the distribution spec spec and returns a tuple consisting of e and its specification according to spec.