signature FS structure FS : FS where type fd = FD.fd
The FS structure provides access to finite set variables and propagators.
Finite set variables are variables whose values are sets of non-negative integers.
Note that every propagator creation can raise a Tell exception if it is performed on toplevel and the constraint is inconsistent with other constraints.
See also: FD
import signature FS from "x-alice:/lib/constraints/FS-sig" import structure FS from "x-alice:/lib/constraints/FS"
signature FS = sig type fd type bin = fd type fs exception Tell of {cause : exn} (* Implementation dependent fs limits *) val inf : int val sup : int (* Allocation Function *) val fs : (FD.domain * FD.domain) option -> fs (* Domain, Overflow *) val fsVec : int * FD.domain * FD.domain -> fs vector (* Domain, Overflow *) (* Standard Propagators *) val compl : fs * fs -> unit val complIn : fs * fs * fs -> unit val incl : fd * fs -> unit val excl : fd * fs -> unit val card : fs * fd -> unit val cardRange : int * int * fs -> unit val isIn : int * fs -> bool val isEmpty : fs -> bool val difference : fs * fs * fs -> unit val intersect : fs * fs * fs -> unit val intersectN : fs vector * fs -> unit val union : fs * fs * fs -> unit val unionN : fs vector * fs -> unit val subset : fs * fs -> unit val disjoint : fs * fs -> unit val disjointN : fs vector -> unit val distinct : fs * fs -> unit val distinctN : fs vector -> unit val partition : fs vector * fs -> unit (* Values *) val value : FD.domain -> fs (* Domain, Overflow *) val emptyValue : unit -> fs val singletonValue : int -> fs (* val upperBound : FD.domain -> fs *) val universalValue : unit -> fs val isValue : fs -> bool (* Integer FS *) structure Int : sig val min : fs * fd -> unit val max : fs * fd -> unit val convex : fs -> unit val match : fs * fd vector -> unit val minN : fs * fd vector -> unit val maxN : fs * fd vector -> unit end (* Reified Propagators *) structure Reified : sig val isIn : int * fs * bin -> unit val areIn : int list * fs * bin list -> unit val incl : fd * fs * bin -> unit val equal : fs * fs * bin -> unit val partition : fs list * int list * fs * bin list -> unit end (* Reflection *) structure Reflect : sig val card : fs -> FD.domain val lowerBound : fs -> FD.domain val unknown : fs -> FD.domain val upperBound : fs -> FD.domain val cardOfLowerBound : fs -> int val cardOfUnknown : fs -> int val cardOfUpperBound : fs -> int end end
The type of finite domain variables. Usually equal to FD.fd.
The type of finite set variables.
is raised when a propagator is created on toplevel and is inconsistent with other constraints. Usually equal to FD.Tell.
denotes the implementation dependent smallest possible element of a finite set.
denotes the implementation dependent largest possible element of a finite set.
returns a freshly created finite set variables initialized according to spec.
returns a vector of size n containing freshly created finite set variables initialized according to spec.
y = [FS.inf, ..., FS.sup] - x
y = [FS.inf, ..., FS.sup] - x
z = y - x
Post the constraint that x is an element of y and that inf <= x <= sup holds.
Post the constraint that x is not an element of y.
y is constrained to denote the cardinality of x.
Post the constraint that the cardinality of x is greater than or equal to l and less than or equal to h.
returns true iff i is an element of x, false otherwise.
Post the constraint that z = x - y.
Post the constraint that z is the intersection of y and y.
x constraint to the the intersection of all v1, ..., vn.
Post the constraint that z is the union of y and y.
x constraint to the the union of all v1, ..., vn.
Post the constraint that x must be a subset of or equal to y.
x and y must be disjoint.
All elements x must be pairwise disjoint.
x and y must be distinct.
All elements of v must be pairwise distinct.
v is a partition of x, that is, v containts pairwise disjoint set such that the union yields x.
returns a freshly created finite set value according to spec.
returns a freshly created finite set value denoting the empty set.
returns a freshly created finite set value denoting the the singleton value i.
returns a freshly created finite set value denoting the universal value.
returns true iff x denotes a finite set value, false otherwise.
y is constrained to denote the minimal element of x.
y is constrained to denote the maximal element of x.
Whenever l and h are elements of x, then every value between l and h is also in x.
v is a vector of n integer variables that denote the elements of x in ascending order.
v is a vector of n integer variables that denote the n minimal elements of x in ascending order.
v is a vector of n integer variables that denote the n maximal elements of x in ascending order.
Reifies FS.isIn(i, x) into c.
Equivalent to ListPair.app (fn (i, c) => Reified.isIn(i, x, c)) (is, cs).
c reifies the presence of x in y. This propagator detects in contrast to Reified.isIn earlier if x is or is not constrained in y.
c reifies the equality of x and y.
The propagator partitions the set value x by selecting elements from the list of set values vs. The positive integers in is denote the cost resp. benefit of the corresponding set value in vs if it is selected for the partition. Each element of cs is either 0 or the corresponding integer value in is depending on whether the corresponding set value in vs is part of the partition or not. Excluding a set value from the partition is done by constraining the corresponding element of cs to 0. An element in cs not equal to 0 includes the corresponding set value in vs in the partition. The propagator ensures a valid partition according to the values of cs.
returns a description of the current information on the cardinality of x.
returns a specification of the greatest lower bound that is currently known about the set x.
returns a specification of the set of elements that are neither known to included in x nor excluded from x.
returns a specification of the least upper bound that is currently known about the set x.
returns the cardinality of the current greatest lower bound for x.
returns the number of elements that are currently not known to be included or excluded from x.
returns the cardinality of the current least upper bound for x.