alice
library
manual.

Alice Project

The FS structure


________ Synopsis ____________________________________________________

    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 ______________________________________________________

    import signature FS from "x-alice:/lib/constraints/FS-sig"
    import structure FS from "x-alice:/lib/constraints/FS"

________ Interface ___________________________________________________

    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

________ Description _________________________________________________

type fd
type bin = fd

The type of finite domain variables. Usually equal to FD.fd.

type fs

The type of finite set variables.

exception Tell of {cause : exn}

is raised when a propagator is created on toplevel and is inconsistent with other constraints. Usually equal to FD.Tell.

inf

denotes the implementation dependent smallest possible element of a finite set.

sup

denotes the implementation dependent largest possible element of a finite set.

fs spec

returns a freshly created finite set variables initialized according to spec.

fsVec (n,spec)

returns a vector of size n containing freshly created finite set variables initialized according to spec.

compl (x,y)

y = [FS.inf, ..., FS.sup] - x

compl (x,y)

y = [FS.inf, ..., FS.sup] - x

complIn (x,y,z)

z = y - x

incl (x,y)

Post the constraint that x is an element of y and that inf <= x <= sup holds.

excl (x,y)

Post the constraint that x is not an element of y.

card (x,y)

y is constrained to denote the cardinality of x.

cardRange (l,u,x)

Post the constraint that the cardinality of x is greater than or equal to l and less than or equal to h.

isIn (i,x)

returns true iff i is an element of x, false otherwise.

difference (x,y,z)

Post the constraint that z = x - y.

intersect (x,y,z)

Post the constraint that z is the intersection of y and y.

intersectN (v,x)

x constraint to the the intersection of all v1, ..., vn.

union (x,y,z)

Post the constraint that z is the union of y and y.

unionN (v,x)

x constraint to the the union of all v1, ..., vn.

subset (x,y)

Post the constraint that x must be a subset of or equal to y.

disjoint (x,y)

x and y must be disjoint.

disjointN v

All elements x must be pairwise disjoint.

distinct (x,x)

x and y must be distinct.

distinctN v

All elements of v must be pairwise distinct.

partition (v,x)

v is a partition of x, that is, v containts pairwise disjoint set such that the union yields x.

value x

returns a freshly created finite set value according to spec.

emptyValue ()

returns a freshly created finite set value denoting the empty set.

singletonValue i

returns a freshly created finite set value denoting the the singleton value i.

universalValue ()

returns a freshly created finite set value denoting the universal value.

isValue x

returns true iff x denotes a finite set value, false otherwise.

Int.min (x,y)

y is constrained to denote the minimal element of x.

Int.max (x,y)

y is constrained to denote the maximal element of x.

Int.convex x

Whenever l and h are elements of x, then every value between l and h is also in x.

Int.match (x,v)

v is a vector of n integer variables that denote the elements of x in ascending order.

Int.minN (x,v)

v is a vector of n integer variables that denote the n minimal elements of x in ascending order.

Int.maxN (x,v)

v is a vector of n integer variables that denote the n maximal elements of x in ascending order.

Reified.isIn (i,x,c)

Reifies FS.isIn(i, x) into c.

Reified.areIn (is,x,cs)

Equivalent to ListPair.app (fn (i, c) => Reified.isIn(i, x, c)) (is, cs).

Reified.incl (x,y,c)

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.

Reified.equal (x,y,c)

c reifies the equality of x and y.

Reified.partition (vs,is,x,cs)

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.

Reflect.card x

returns a description of the current information on the cardinality of x.

Reflect.lowerBound x

returns a specification of the greatest lower bound that is currently known about the set x.

Reflect.unknown x

returns a specification of the set of elements that are neither known to included in x nor excluded from x.

Reflect.upperBound x

returns a specification of the least upper bound that is currently known about the set x.

Reflect.cardOfLowerBound x

returns the cardinality of the current greatest lower bound for x.

Reflect.cardOfUnknown x

returns the number of elements that are currently not known to be included or excluded from x.

Reflect.cardOfUpperBound x

returns the cardinality of the current least upper bound for x.



last modified 1970/01/01 01:00