4.15.1 Overview

The lattice functors are located in Compiler/Lattices. Each lattice functor is a record with at least the following features making up its interface:

     elem(tag: A
          top: SL
          bot: SL
          glb: SLSL2SL
          select: SLsD2SL
          makeVar: U2SL
          encode: ILOpti2SL
          decode: SL2IL
          pretty: SLAbbrB2OL)
          count: U2Co

The tag feature corresponds to an atom (A)¹ denoting the name of the lattice.

The top feature corresponds to the top value of the lattice in the solver language (SL).

The bot feature corresponds to the bottom value of the lattice in the solver language (SL).

The glb feature corresponds to the greatest lower bound function of the lattice. Its type is SL SL -> SL, i.e. it takes two SL values and yields their greatest lower bound (as a SL value). All greatest lower bound functions are commutative, thereby maintaining monotonicity.

The select feature corresponds to the selection function of the lattice which is used by the XDK solver to select one lexical entry from the set of lexical entries for a word. Its type is SLs D -> SL, i.e. it takes a list of SL values and a selector (an Oz finite domain variable), and yields a SL value.

The makeVar feature corresponds to the make variable function of the lattice which is used by the XDK solver to create variables of values. Its type is U -> SL, i.e. it takes no argument (as indicated by the type U for “unit”) and yields an undetermined SL value.

The encode feature corresponds to the encoding function of the lattice. Its type is IL Opti -> SL, i.e. it takes an IL value and an optimization record Opti (introduced for efficiency reasons), and yields a SL value.

The decode feature corresponds to the decoding function of the lattice. Its type is SL -> IL, i.e. it takes a SL value and yields an IL value.

The pretty feature corresponds to the pretty function of the lattice. Its type is SL AbbrB -> OL, i.e. it takes a SL value and a boolean (AbbrB), and yields an OL value. AbbrB specifies whether the yielded OL value shall be abbreviated (AbbrB==true) or not (AbbrB==false).

The count feature corresponds to the counting function of the lattice. Its type is U -> Co, i.e. it takes no argument and yields a fd/fs variable count. This is used for profiling.