7.4 Finite Set Interval Variables

var.is

{FS.var.is +M ?B}

Tests whether M is a finite set variable.

7.4.1 Declaring a Single Variable

var.decl

{FS.var.decl ?M}

\emptyset \subseteq {\tt M} \subseteq \uniset

var.upperBound

{FS.var.upperBound +Spec ?M}

\emptyset \subseteq \codeinline{oz}{M} \subseteq \conv(\codeinline{oz}{Spec})

var.lowerBound

{FS.var.lowerBound +Spec ?M}

\conv({\tt Spec}) \subseteq \codeinline{oz}{M} \subseteq \uniset

var.bounds

{FS.var.bounds +Spec1 +Spec2 ?M}

\conv({\tt Spec1}) \subseteq {\tt M} \subseteq \conv({\tt Spec2})

7.4.2 Declaring a List of Variables

The following functions return a list Ms of length I and all its elements are constrained to finite set interval variables according to the following specifications.

var.list.decl

{FS.var.list.decl +I ?Ms}

For all elements M of Ms: \emptyset \subseteq \codeinline{oz}{M} \subseteq \uniset

var.list.upperBound

{FS.var.list.upperBound ++Spec ?Ms}

For all elements M of Ms: \emptyset \subseteq \codeinline{oz}{M} \subseteq
\conv({\tt Spec})

var.list.lowerBound

{FS.var.list.lowerBound ++Spec ?Ms}

For all elements M of Ms: \conv(\codeinline{oz}{Spec}) \subseteq \codeinline{oz}{M}\subseteq \uniset

var.list.bounds

{FS.var.list.bounds ++Spec1 +Spec2 ?Ms}

For all elements M of Ms: \conv({\tt Spec1})\subseteq
{\tt M}\subseteq \conv({\tt Spec2})

7.4.3 Declaring a Tuple of Variables

The following functions return a tuple Mt with label L and width I and all its elements are constrained to finite set interval variables according to the following specifications.

var.tuple.decl

{FS.var.tuple.decl ++I ?Mt}

For all elements M of Mt: \emptyset \subseteq {\tt M} \subseteq
\uniset

var.tuple.upperBound

{FS.var.tuple.upperBound +++Spec ?Mt}

For all elements M of Mt: \emptyset \subseteq \codeinline{oz}{M} \subseteq
\conv({\tt Spec})

var.tuple.lowerBound

{FS.var.tuple.lowerBound +++Spec ?Mt}

For all elements M of Mt: \conv(\codeinline{oz}{Spec}) \subseteq
\codeinline{oz}{M}\subseteq \uniset

var.tuple.bounds

{FS.var.tuple.bounds +++Spec1 +Spec2 ?Mt}

For all elements M of Mt: \conv({\tt Spec1})\subseteq
{\tt M}\subseteq \conv({\tt Spec2})

7.4.4 Declaring a Record of Variables

The following functions return a record Mr with label L and the fields Ls and all its fields are constrained to finite set interval variables according to the following specifications.

var.record.decl

{FS.var.record.decl ++Ls ?Mr}

For all elements M of Mr: \emptyset \subseteq {\tt M} \subseteq
\uniset

var.record.upperBound

{FS.var.record.upperBound ++Ls +Spec ?Mr}

For all elements M of Mr: \emptyset \subseteq \codeinline{oz}{M} \subseteq
\conv({\tt Spec})

var.record.lowerBound

{FS.var.record.lowerBound ++Ls +Spec ?Mr}

For all elements M of Mr: \conv(\codeinline{oz}{Spec}) \subseteq
\codeinline{oz}{M}\subseteq \uniset

var.record.bounds

{FS.var.record.bounds ++Ls +Spec1 +Spec2 ?Mr}

For all elements M of Mr: {\tt M} \in
\sic{\conv({\tt Spec1})}{\conv({\tt Spec2})}


Denys Duchier, Leif Kornstaedt, Martin Homik, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.4.0 (20080702)