00001 /* Part of the culibs project, <http://www.eideticdew.org/culibs/>. 00002 * Copyright (C) 2007 Petter Urkedal <urkedal@nbi.dk> 00003 * 00004 * This program is free software: you can redistribute it and/or modify 00005 * it under the terms of the GNU General Public License as published by 00006 * the Free Software Foundation, either version 3 of the License, or 00007 * (at your option) any later version. 00008 * 00009 * This program is distributed in the hope that it will be useful, 00010 * but WITHOUT ANY WARRANTY; without even the implied warranty of 00011 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 00012 * GNU General Public License for more details. 00013 * 00014 * You should have received a copy of the GNU General Public License 00015 * along with this program. If not, see <http://www.gnu.org/licenses/>. 00016 */ 00017 00018 #ifndef CUEX_SEMILATTICE_H 00019 #define CUEX_SEMILATTICE_H 00020 00021 #include <cuex/opn.h> 00022 #include <cu/algo.h> 00023 00024 CU_BEGIN_DECLARATIONS 00025 /** \defgroup cuex_semilattice_h cuex/semilattice.h: Expression Support for Semilattices 00026 ** @{ \ingroup cuex_mod 00027 ** 00028 ** This provides expressions in a canonical form according to the three axioms 00029 ** of semilattices. Assuming a meet-semilattice, these are 00030 ** 00031 ** - associative: \e x ∧ (\e y ∧ \e z) = (\e x ∧ \e y) ∧ \e z 00032 ** - commutative: \e x ∧ \e y = \e y ∧ \e x 00033 ** - idempotent: \e x ∧ \e x = \e x 00034 ** 00035 ** We also assume an identity element ⊤ (top) which fulfils \e x ∧ ⊤ = \e x 00036 ** for any \e x. For join-semilattices, replace ∧ with ∨ (join) and ⊤ with ⊥ 00037 ** (bottom). 00038 ** 00039 ** Since the operator is stored in the lattice structures, the same functions 00040 ** can be used for both meet- or join-semilattices, as well as other 00041 ** semi-lattice like terms. 00042 ** To avoid confusion while reading client code, separate naming schemes for 00043 ** meet and join semi-lattices are implemented by using <code>\#define</code> 00044 ** aliases for the latter. 00045 ** 00046 ** Elements are considered equal if they are pointer-equal. 00047 ** Since expressions are hash-consed, this gives structural equality. 00048 ** Terms are atomic with respect to a ∧-semilattice if their top-level node is 00049 ** not a ∧ operation. 00050 ** 00051 ** There is no special treatment of variables. 00052 **/ 00053 00054 extern cuoo_type_t cuexP_semilattice_type; 00055 00056 CU_SINLINE cuoo_type_t cuex_semilattice_type(void) 00057 { return cuexP_semilattice_type; } 00058 00059 /** Returns the top element of the ∧-semilattice, where ∧ = \a meet. This is 00060 ** also the identity element. */ 00061 cuex_t cuex_meetlattice_top(cuex_meta_t meet); 00062 00063 /** For a ∧-semilattice where \a meet = ∧, returns \a x ∧ \a y in a canonical 00064 ** form with respect top-level ∧-terms of \a x and \a y. */ 00065 cuex_t cuex_meetlattice_meet(cuex_meta_t meet, cuex_t x, cuex_t y); 00066 00067 /** This computes \a x ∨ \a y where ∨ is the dual of ∧ = \a meet, under the 00068 ** assumption that \a a ∧ \a b = ⊤ for any two distinct atomic terms \e a and 00069 ** \e b. */ 00070 cuex_t cuex_meetlattice_semijoin(cuex_meta_t meet, cuex_t x, cuex_t y); 00071 00072 /** True iff \a x = \a x ∧ \e y. */ 00073 cu_bool_t cuex_meetlattice_leq(cuex_meta_t meet, cuex_t x, cuex_t y); 00074 00075 /** Returns the most precise ordering predicate for \a x and \a y. */ 00076 cu_order_t cuex_meetlattice_order(cuex_meta_t meet, cuex_t x, cuex_t y); 00077 00078 #define cuex_joinlattice_bottom cuex_meetlattice_top 00079 #define cuex_joinlattice_join cuex_meetlattice_meet 00080 #define cuex_joinlattice_semimeet cuex_meetlattice_semijoin 00081 #define cuex_joinlattice_geq cuex_meetlattice_leq 00082 #define cuex_joinlattice_leq cuex_meetlattice_geq 00083 #define cuex_joinlattice_order(opr, x, y) cuex_meetlattice_order(opr, y, x) 00084 00085 /** @}*/ 00086 CU_END_DECLARATIONS 00087 00088 #endif