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_SET_H 00019 #define CUEX_SET_H 00020 00021 #include <cuex/fwd.h> 00022 #include <cuoo/type.h> 00023 #include <cu/algo.h> 00024 00025 CU_BEGIN_DECLARATIONS 00026 extern cuoo_type_t cuexP_set_type; 00027 extern cuex_t cuexP_set_empty; 00028 00029 /** \defgroup cuex_set_h cuex/set.h: Set-Like Terms 00030 ** @{ \ingroup cuex_mod 00031 ** 00032 ** \see cuex_semilattice_h 00033 ** \see cuex_labelling_h 00034 ** \see cuex_atree_h 00035 **/ 00036 00037 /** The type of set terms. */ 00038 CU_SINLINE cuoo_type_t 00039 cuex_set_type() 00040 { return cuexP_set_type; } 00041 00042 /** True iff \a e is a set. */ 00043 CU_SINLINE cu_bool_t 00044 cuex_is_set(cuex_t e) 00045 { return cuex_meta(e) == cuoo_type_to_meta(cuex_set_type()); } 00046 00047 /** The empty set term. */ 00048 CU_SINLINE cuex_t 00049 cuex_empty_set(void) 00050 { return cuexP_set_empty; } 00051 00052 /** True iff \a S is the empty set term. */ 00053 CU_SINLINE cu_bool_t 00054 cuex_is_empty_set(cuex_t S) 00055 { return S == cuexP_set_empty; } 00056 00057 /** Returns the singleton set {\a e}. */ 00058 cuex_t cuex_singleton_set(cuex_t e); 00059 00060 /** Returns \a S ∪ \a e. */ 00061 cuex_t cuex_set_insert(cuex_t S, cuex_t e); 00062 00063 /** Returns \a S ∖ \a e. */ 00064 cuex_t cuex_set_erase(cuex_t S, cuex_t e); 00065 00066 /** Returns \a S0 ∪ \a S1. */ 00067 cuex_t cuex_set_union(cuex_t S0, cuex_t S1); 00068 00069 /** Returns \a S0 ∩ \a S1. */ 00070 cuex_t cuex_set_isecn(cuex_t S0, cuex_t S1); 00071 00072 /** True iff \a e ∈ \a S. */ 00073 cu_bool_t cuex_set_contains(cuex_t S, cuex_t e); 00074 00075 /** True iff \a S0 ⊆ \a S1. */ 00076 cu_bool_t cuex_set_subeq(cuex_t S0, cuex_t S1); 00077 00078 /** Return the most strict ordering predicate \e R such that 00079 ** \a S0 \e R \a S1. */ 00080 cu_order_t cuex_set_order(cuex_t S0, cuex_t S1); 00081 00082 /** A commutative source over all elements of \a S. */ 00083 cu_ptr_source_t cuex_set_iter_source(cuex_t S); 00084 00085 /** @} */ 00086 CU_END_DECLARATIONS 00087 00088 #endif