Defines | |
| #define | cuex_joinlattice_bottom cuex_meetlattice_top |
| #define | cuex_joinlattice_join cuex_meetlattice_meet |
| #define | cuex_joinlattice_semimeet cuex_meetlattice_semijoin |
| #define | cuex_joinlattice_geq cuex_meetlattice_leq |
| #define | cuex_joinlattice_leq cuex_meetlattice_geq |
| #define | cuex_joinlattice_order(opr, x, y) cuex_meetlattice_order(opr, y, x) |
Functions | |
| cuoo_type_t | cuex_semilattice_type (void) |
| 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) |
Variables | |
| cuoo_type_t | cuexP_semilattice_type |
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.
| cu_bool_t cuex_meetlattice_leq | ( | cuex_meta_t | meet, | |
| cuex_t | x, | |||
| cuex_t | y | |||
| ) |
True iff x = x ∧ y.
| cuex_t cuex_meetlattice_meet | ( | cuex_meta_t | meet, | |
| cuex_t | x, | |||
| cuex_t | y | |||
| ) |
For a ∧-semilattice where meet = ∧, returns x ∧ y in a canonical form with respect top-level ∧-terms of x and y.
| cu_order_t cuex_meetlattice_order | ( | cuex_meta_t | meet, | |
| cuex_t | x, | |||
| cuex_t | y | |||
| ) |
Returns the most precise ordering predicate for x and y.
| cuex_t cuex_meetlattice_semijoin | ( | cuex_meta_t | meet, | |
| cuex_t | x, | |||
| cuex_t | 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.
| cuex_t cuex_meetlattice_top | ( | cuex_meta_t | meet | ) |
Returns the top element of the ∧-semilattice, where ∧ = meet. This is also the identity element.