|#define||cuex_joinlattice_order(opr, x, y) cuex_meetlattice_order(opr, y, x)|
|cuex_t||cuex_meetlattice_top (cuex_meta_t meet)|
|cuex_t||cuex_meetlattice_meet (cuex_meta_t meet, cuex_t x, cuex_t y)|
|cuex_t||cuex_meetlattice_semijoin (cuex_meta_t meet, cuex_t x, cuex_t y)|
|cu_bool_t||cuex_meetlattice_leq (cuex_meta_t meet, cuex_t x, cuex_t y)|
|cu_order_t||cuex_meetlattice_order (cuex_meta_t meet, cuex_t x, cuex_t y)|
This provides expressions in a canonical form according to the three axioms of semilattices. Assuming a meet-semilattice, these are
We also assume an identity element ⊤ (top) which fulfils x ∧ ⊤ = x for any x. For join-semilattices, replace ∧ with ∨ (join) and ⊤ with ⊥ (bottom).
Since the operator is stored in the lattice structures, the same functions can be used for both meet- or join-semilattices, as well as other semi-lattice like terms. To avoid confusion while reading client code, separate naming schemes for meet and join semi-lattices are implemented by using
#define aliases for the latter.
Elements are considered equal if they are pointer-equal. Since expressions are hash-consed, this gives structural equality. Terms are atomic with respect to a ∧-semilattice if their top-level node is not a ∧ operation.
There is no special treatment of variables.
For a ∧-semilattice where meet = ∧, returns x ∧ y in a canonical form with respect top-level ∧-terms of x and y.
Returns the most precise ordering predicate for x and y.
This computes x ∨ y where ∨ is the dual of ∧ = meet, under the assumption that a ∧ b = ⊤ for any two distinct atomic terms a and b.