1 // -*- c++ -*- 2 //***************************************************************************** 3 /** @file BooleSet.h 4 * 5 * @author Alexander Dreyer 6 * @date 2006-04-20 7 * 8 * This file defines the class BooleSet, which is currently just a typedef. 9 * 10 * @par Copyright: 11 * (c) 2006-2010 by The PolyBoRi Team 12 * 13 **/ 14 //***************************************************************************** 15 16 #ifndef polybori_BooleSet_h_ 17 #define polybori_BooleSet_h_ 18 19 // include basic definitions 20 #include <polybori/pbori_defs.h> 21 22 // include polybori functionals 23 #include <polybori/routines/pbori_func.h> 24 25 #include <polybori/diagram/CCuddDDFacade.h> 26 27 #include "BoolePolyRing.h" 28 29 BEGIN_NAMESPACE_PBORI 30 31 /// Forward declaration of monomial type 32 class BooleMonomial; 33 class BooleExponent; 34 35 template<class OrderType, class NavigatorType, class MonomType> 36 class CGenericIter; 37 // temporarily 38 class LexOrder; 39 40 template<class OrderType, class NavigatorType, class MonomType> 41 class CReverseIter; 42 43 44 #define PBORI_CONST_DDFUNCS(func) \ 45 self func(const self& rhs) const { return self(base::func(rhs.diagram())); } 46 47 #define PBORI_DDFUNCS(func) \ 48 self& func(const self& rhs) { base::func(rhs.diagram()); return *this; } 49 50 #define PBORI_CONST_DDFUNCS_IDX(func) \ 51 self func(idx_type idx) const { return self(base::func(idx)); } 52 53 #define PBORI_DDFUNCS_IDX(func) \ 54 self& func(idx_type idx) { base::func(idx); return *this; } 55 56 57 class BooleSet: 58 public CCuddDDFacade<BoolePolyRing, BooleSet> { 59 /// Generic access to type of *this 60 typedef BooleSet self; 61 62 public: 63 /// Generic access to type of *this 64 typedef self dd_type; 65 66 /// Generic access to base type 67 typedef CCuddDDFacade<BoolePolyRing, BooleSet> base; 68 69 /// Type of terms 70 typedef BooleMonomial term_type; 71 72 /// Fix type for treatment of exponent vectors 73 typedef BooleExponent exp_type; 74 75 /// Type for Boolean polynomial rings (without ordering) 76 typedef BoolePolyRing ring_type; 77 78 /// Iterator type for iterating all monomials 79 typedef CGenericIter<LexOrder, navigator, term_type> const_iterator; 80 81 /// Iterator type for iterating all exponent vectors 82 typedef CGenericIter<LexOrder, navigator, exp_type> exp_iterator; 83 84 /// Iterator type for iterating all exponent vectors 85 typedef CReverseIter<LexOrder, navigator, exp_type> reverse_exp_iterator; 86 87 /// Iterator type for iterating all monomials 88 typedef CReverseIter<LexOrder, navigator, term_type> const_reverse_iterator; 89 90 public: 91 /// Copy constructor BooleSet(const self & rhs)92 BooleSet(const self& rhs): base(rhs) {} 93 94 /// Copy constructor BooleSet(const base & rhs)95 BooleSet(const base& rhs): base(rhs) {} 96 97 /// Construct new node BooleSet(idx_type idx,const self & first,const self & second)98 BooleSet(idx_type idx, const self& first, const self& second): 99 base(idx, first, second) { } 100 101 /// Construct new node (using navigator nodes) BooleSet(idx_type idx,navigator first,navigator second,const ring_type & ring)102 BooleSet(idx_type idx, navigator first, navigator second, 103 const ring_type& ring): 104 base(ring, idx, first, second) { } 105 106 /// Construct new node (using nodes) BooleSet(const ring_type & ring,node_ptr node)107 BooleSet(const ring_type& ring, node_ptr node): 108 base(ring, node) { } 109 110 /// Construct new node (using navigator nodes) BooleSet(const ring_type & ring,navigator navi)111 BooleSet(const ring_type& ring, navigator navi): 112 base(ring, navi.getNode()) { } 113 114 /// Construct empty set in ring BooleSet(const ring_type & ring)115 BooleSet(const ring_type& ring): 116 base(ring.zero()) { }; 117 118 /// Construct new node (using navigator for then and else-branches) BooleSet(idx_type idx,const self & rhs)119 BooleSet(idx_type idx, const self& rhs): 120 base(idx, rhs, rhs) { } 121 122 /// Construct from navigator node BooleSet(navigator navi,const ring_type & ring)123 BooleSet(navigator navi, const ring_type& ring): 124 base(ring, navi) { } 125 126 /// Destructor ~BooleSet()127 ~BooleSet() {} 128 129 /// Start of iteration over terms 130 const_iterator begin() const; 131 132 /// Finish of iteration over terms 133 const_iterator end() const; 134 135 /// Start of backward iteration over terms 136 const_reverse_iterator rbegin() const; 137 138 /// Finish of backward iteration over terms 139 const_reverse_iterator rend() const; 140 141 /// Start of backward exponent iteration over terms 142 reverse_exp_iterator rExpBegin() const; 143 144 /// Finish of backward iteration over terms 145 reverse_exp_iterator rExpEnd() const; 146 147 /// Start of iteration over exponent vectors 148 exp_iterator expBegin() const; 149 150 /// Finish of iteration over exponent vectors 151 exp_iterator expEnd() const; 152 153 /// Get unique hash value (valid only per runtime) hash()154 hash_type hash() const { 155 return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t>(getNode())); 156 } 157 158 /// Get stable hash value, which is reproducible stableHash()159 hash_type stableHash() const { 160 return stable_hash_range(navigation()); 161 } 162 163 /// Set of variables of the whole set 164 term_type usedVariables() const; 165 166 /// Exponent vector of variables of the whole set 167 exp_type usedVariablesExp() const; 168 change(idx_type idx)169 self change(idx_type idx) const { 170 if PBORI_UNLIKELY(size_type(idx) >= ring().nVariables()) 171 throw PBoRiError(CTypes::out_of_bounds); 172 return base::change(idx); 173 } 174 175 176 /// Add given monomial to sets 177 self add(const term_type& rhs) const; 178 179 // Check whether rhs is included in *this 180 bool_type owns(const term_type& rhs) const; 181 182 /// Check whether rhs is included in *this 183 bool_type owns(const exp_type&) const; 184 185 /// Get last term (wrt. lexicographical order) 186 term_type lastLexicographicalTerm() const; 187 188 /// Compute intersection with divisors of rhs 189 self divisorsOf(const term_type& rhs) const; 190 191 /// Compute intersection with divisors of rhs 192 self divisorsOf(const exp_type& rhs) const; 193 194 /// Intersection with divisors of first (lexicographical) term of rhs 195 self firstDivisorsOf(const self& rhs) const; 196 197 /// Compute intersection with multiples of rhs 198 self multiplesOf(const term_type& rhs) const; 199 200 /// Division by given term 201 self divide(const term_type& rhs) const; 202 203 /// Check for empty intersection with divisors of rhs, i.e. test whether there 204 /// are terms made of the given variables. 205 bool_type hasTermOfVariables(const term_type& rhs) const; 206 207 /// Get minimal elements wrt. inclusion 208 self minimalElements() const; 209 210 /// Test whether the empty set is included ownsOne()211 bool_type ownsOne() const { return owns_one(navigation()); } 212 213 /// Test, whether we have one term only isSingleton()214 bool_type isSingleton() const { return dd_is_singleton(navigation()); } 215 216 /// Test, whether we have one or two terms only isSingletonOrPair()217 bool_type isSingletonOrPair() const { 218 return dd_is_singleton_or_pair(navigation()); 219 } 220 221 /// Test, whether we have two terms only isPair()222 bool_type isPair() const { return dd_is_pair(navigation()); } 223 224 /// Compute existential abstraction: 225 /// Given a diagram @c F, and a set of variables @c S, remove all occurrences 226 /// of each @c s in @c S from any subset in @c F. This can be implemented by 227 /// cofactoring @c F w.r.t. @c s = 1 and @c s = 0, then forming their union 228 self existAbstract(const term_type& rhs) const; 229 230 /// Access internal decision diagram diagram()231 const self& diagram() const { return *this; } // to be removed 232 233 /// Cartesean product cartesianProduct(const self & rhs)234 self cartesianProduct(const self& rhs) const { 235 return unateProduct(rhs); 236 }; 237 238 /// Test containment contains(const self & rhs)239 bool_type contains(const self& rhs) const { return rhs.implies(*this); } 240 241 /// Returns number of terms size()242 size_type size() const { return count(); } 243 244 /// Returns number of terms (deprecated) length()245 size_type length() const { return size(); } 246 247 /// Returns number of variables in manager nVariables()248 size_type nVariables() const { return ring().nVariables(); } 249 250 /// Approximation of number of terms sizeDouble()251 double sizeDouble() const { return countDouble(); } 252 253 /// Print current set to output stream 254 ostream_type& print(ostream_type&) const; 255 256 /// Get corresponding zero element (may be removed in the future) emptyElement()257 self emptyElement() const { return ring().zero(); } 258 259 /// Count terms containing BooleVariable(idx) 260 size_type countIndex(idx_type idx) const; 261 262 /// Count many terms containing BooleVariable(idx) 263 double countIndexDouble(idx_type idx) const ; 264 265 /// Test whether, all divisors of degree -1 of term rhs are contained in this 266 bool_type containsDivisorsOfDecDeg(const term_type& rhs) const; 267 268 /// Test for term corresponding to exponent rhs 269 bool_type containsDivisorsOfDecDeg(const exp_type& rhs) const; 270 }; 271 272 /// Stream output operator 273 inline BooleSet::ostream_type& 274 operator<<( BooleSet::ostream_type& os, const BooleSet& bset ) { 275 return bset.print(os); 276 } 277 278 279 END_NAMESPACE_PBORI 280 281 #endif 282