PolyBoRi
BooleSet.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
157 //*****************************************************************************
158 
159 // include basic definitions
160 #include "pbori_defs.h"
161 
162 // include definitions of decision diagram interfaces
163 #include "CDDInterface.h"
164 
165 // include polybori functionals
166 #include "pbori_func.h"
167 #include "BooleRing.h"
168 
169 #ifndef BooleSet_h_
170 #define BooleSet_h_
171 
173 
175 class BooleMonomial;
176 class BooleExponent;
177 
178 template<class OrderType, class NavigatorType, class MonomType>
179 class CGenericIter;
180 // temporarily
181 class LexOrder;
182 
183 //template<class OrderType, class NavigatorType, class MonomType>
184 //class CGenericIter;
185 
186 
187 #define PBORI_CONST_DDFUNCS(func) \
188  self func(const self& rhs) const { return self(base::func(rhs.diagram())); }
189 
190 #define PBORI_DDFUNCS(func) \
191  self& func(const self& rhs) { base::func(rhs.diagram()); return *this; }
192 
193 #define PBORI_CONST_DDFUNCS_IDX(func) \
194  self func(idx_type idx) const { return self(base::func(idx)); }
195 
196 #define PBORI_DDFUNCS_IDX(func) \
197  self& func(idx_type idx) { base::func(idx); return *this; }
198 
199 
200 class BooleSet:
201  public CTypes::dd_type {
202 
203 public:
205  typedef BooleSet self;
206 
209 
211  typedef base dd_type;
212 
216 
219 
222 
225 
227  typedef CGenericIter<LexOrder, navigator, term_type> const_iterator;
228 
230  typedef CGenericIter<LexOrder, navigator, exp_type> exp_iterator;
231 
233  BooleSet();
234 
236  BooleSet(const self& rhs): base(rhs) {}
237 
239  BooleSet(const base& rhs): base(rhs) {}
240 
242  BooleSet(idx_type idx, const self& first, const self& second):
243  base(idx, first, second) {
244 
245 
246  }
247 
249  BooleSet(idx_type idx, navigator first, navigator second,
250  const ring_type& ring):
251  base(ring.manager(), idx, first, second) { }
252 
254  BooleSet(idx_type idx, const self& rhs):
255  base(rhs.ring().manager(), idx, rhs.navigation()) { }
256 
258  // BooleSet(bool_type);
261 
263  BooleSet(navigator navi, const ring_type& ring):
264  base(ring.manager().manager(), navi) { }
265 
268 
270  const_iterator begin() const;
271 
273  const_iterator end() const;
274 
276  exp_iterator expBegin() const;
277 
279  exp_iterator expEnd() const;
280 
282  self& operator=(const self&);
283 
285  using base::operator=;
286 
288  term_type usedVariables() const;
289 
291  exp_type usedVariablesExp() const;
292 
294  self& addAssign(const term_type&);
295 
297  self add(const term_type&) const;
298 
300  bool_type owns(const term_type&) const;
301 
303  bool_type owns(const exp_type&) const;
304 
306  term_type lastLexicographicalTerm() const;
307 
309  self divisorsOf(const term_type& rhs) const;
310 
312  self divisorsOf(const exp_type& rhs) const;
313 
315  self firstDivisorsOf(const self& rhs) const;
316 
318  self multiplesOf(const term_type& rhs) const;
319 
321  self divide(const term_type& rhs) const;
322 
324  self& divideAssign(const term_type& rhs);
325 
327  bool_type hasTermOfVariables(const term_type& rhs) const;
328 
330  self minimalElements() const;// { return base::minimalElements(); };
331 
333  using base::ownsOne;
334 
336  bool_type isSingleton() const { return dd_is_singleton(navigation()); }
337 
340  return dd_is_singleton_or_pair(navigation());
341  }
342 
344  bool_type isPair() const { return dd_is_pair(navigation()); }
345 
347  self existAbstract(const term_type& rhs) const;
348 
350  const dd_type& diagram() const { return dynamic_cast<const dd_type&>(*this); }
351 
353  self ite(const self& then_dd, const self& else_dd) {
354  return self(base::ite(then_dd.diagram(), else_dd.diagram()));
355  };
356 
358  self& iteAssign(const self& then_dd, const self& else_dd) {
359  base::iteAssign(then_dd.diagram(), else_dd.diagram());
360  return *this;
361  };
362 
364  self cartesianProduct(const self& rhs) const {
365  return base::unateProduct(rhs.diagram());
366  };
367 
369 
373 
374 
384  PBORI_CONST_DDFUNCS(divideFirst)
385 
387  PBORI_DDFUNCS_IDX(subset0Assign)
388  PBORI_DDFUNCS_IDX(subset1Assign)
390 
391  PBORI_DDFUNCS(uniteAssign)
392  PBORI_DDFUNCS(diffAssign)
393  PBORI_DDFUNCS(diffConstAssign)
394  PBORI_DDFUNCS(intersectAssign)
395  PBORI_DDFUNCS(productAssign)
396  PBORI_DDFUNCS(dotProductAssign)
397  PBORI_DDFUNCS(ddDivideAssign)
398  PBORI_DDFUNCS(weakDivideAssign)
399  PBORI_DDFUNCS(divideFirstAssign)
401 
403  using base::hash;
404 
406  using base::stableHash;
407 
409  ostream_type& print(ostream_type&) const;
410 
412  self emptyElement() const { return base::emptyElement(); }
413 
415  size_type countIndex(idx_type idx) const;
416 
418  double countIndexDouble(idx_type idx) const ;
419 
421  ring_type ring() const { return ring_type(base::manager()); }
422 };
423 
425 inline BooleSet::ostream_type&
427  return bset.print(os);
428 }
430 
431 #endif