18 #ifndef polybori_BoolePolynomial_h_
19 #define polybori_BoolePolynomial_h_
50 class DegRevLexAscOrder;
51 class BlockDegLexOrder;
52 class BlockDegRevLexAscOrder;
59 template <
class IteratorType,
class MonomType>
62 template <
class IteratorType,
class MonomType>
69 template<
class OrderType,
class NavigatorType,
class MonomType>
72 template<
class NavigatorType,
class ExpType>
213 m_dd(ring.zero() ) { }
217 m_dd(isOne? ring.one(): ring.zero() ) { }
226 BoolePolynomial(
const exp_type&,
const ring_type&);
246 return (*
this) =
self(rhs, ring());
251 self& operator+=(
const self&);
255 if (rhs) (*this) = (*
this + ring().one());
258 template <
class RHSType>
259 self&
operator-=(
const RHSType& rhs) {
return operator+=(rhs); }
264 if (!rhs) *
this = ring().zero();
267 self& operator/=(
const var_type&);
268 self& operator/=(
const monom_type&);
269 self& operator/=(
const exp_type&);
270 self& operator/=(
const self& rhs);
271 self& operator/=(constant_type rhs);
272 self& operator%=(
const var_type&);
273 self& operator%=(
const monom_type&);
275 return (*
this) -= (
self(rhs) *= (
self(*
this) /= rhs));
277 self&
operator%=(constant_type rhs) {
return (*
this) /= (!rhs); }
285 return ( rhs? isOne(): isZero() );
289 return (!(*
this==rhs));
306 bool_type firstReducibleBy(
const self&)
const;
309 monom_type lead()
const;
312 monom_type lexLead()
const;
318 monom_type boundedLead(
deg_type bound)
const;
321 exp_type leadExp()
const;
325 exp_type boundedLeadExp(
deg_type bound)
const;
337 hash_type leadStableHash()
const;
355 self gradedPart(
deg_type deg)
const;
358 size_type nNodes()
const;
361 size_type nUsedVariables()
const;
364 monom_type usedVariables()
const;
367 exp_type usedVariablesExp()
const;
370 size_type length()
const;
373 ostream_type& print(ostream_type&)
const;
376 const_iterator begin()
const;
379 const_iterator end()
const;
382 exp_iterator expBegin()
const;
385 exp_iterator expEnd()
const;
388 first_iterator firstBegin()
const;
391 first_iterator firstEnd()
const;
394 monom_type firstTerm()
const;
397 deg_iterator degBegin()
const;
400 deg_iterator degEnd()
const;
403 ordered_iterator orderedBegin()
const;
406 ordered_iterator orderedEnd()
const;
409 ordered_exp_iterator orderedExpBegin()
const;
412 ordered_exp_iterator orderedExpEnd()
const;
416 lex_iterator genericBegin(
lex_tag)
const;
417 lex_iterator genericEnd(
lex_tag)
const;
418 dlex_iterator genericBegin(
dlex_tag)
const;
419 dlex_iterator genericEnd(
dlex_tag)
const;
420 dp_asc_iterator genericBegin(
dp_asc_tag)
const;
428 lex_exp_iterator genericExpBegin(
lex_tag)
const;
429 lex_exp_iterator genericExpEnd(
lex_tag)
const;
430 dlex_exp_iterator genericExpBegin(
dlex_tag)
const;
431 dlex_exp_iterator genericExpEnd(
dlex_tag)
const;
432 dp_asc_exp_iterator genericExpBegin(
dp_asc_tag)
const;
433 dp_asc_exp_iterator genericExpEnd(
dp_asc_tag)
const;
450 operator set_type()
const {
return set(); };
452 size_type eliminationLength()
const;
453 size_type eliminationLengthWithDegBound(
deg_type garantied_deg_bound)
const;
455 void fetchTerms(termlist_type&)
const;
458 termlist_type terms()
const;
461 const dd_type&
diagram()
const {
return m_dd; }
464 set_type
set()
const {
return m_dd; }
478 const ring_type&
ring()
const {
return m_dd.ring(); }
481 comp_type compare(
const self&)
const;
484 bool_type inSingleBlock()
const;
491 self leadFirst()
const;
494 set_type firstDivisors()
const;
503 inline BoolePolynomial
509 inline BoolePolynomial
516 inline BoolePolynomial
524 template <
class RHSType>
525 inline BoolePolynomial
531 inline BoolePolynomial
539 #define PBORI_RHS_MULT(type) inline BoolePolynomial \
540 operator*(const BoolePolynomial& lhs, const type& rhs) { \
541 return BoolePolynomial(lhs) *= rhs; }
549 #undef PBORI_RHS_MULT
552 #define PBORI_LHS_MULT(type) inline BoolePolynomial \
553 operator*(const type& lhs, const BoolePolynomial& rhs) { return rhs * lhs; }
559 #undef PBORI_LHS_MULT
563 template <
class RHSType>
570 template <
class RHSType>
571 inline BoolePolynomial
578 inline BoolePolynomial::bool_type
585 inline BoolePolynomial::bool_type
592 BoolePolynomial::ostream_type&
593 operator<<(BoolePolynomial::ostream_type&,
const BoolePolynomial&);
596 inline BoolePolynomial::bool_type
597 BoolePolynomial::firstReducibleBy(
const self& rhs)
const {
605 return std::includes(firstBegin(), firstEnd(),
606 rhs.firstBegin(), rhs.firstEnd());
613 #endif // of polybori_BoolePolynomial_h_
CGenericIter< LexOrder, navigator, exp_type > lex_exp_iterator
Definition: BoolePolynomial.h:167
CGenericIter< BlockDegRevLexAscOrder, navigator, exp_type > block_dp_asc_exp_iterator
Definition: BoolePolynomial.h:174
bool_type operator!=(constant_type rhs) const
Definition: BoolePolynomial.h:287
bool_type isSingleton() const
Test, whether we have one term only.
Definition: BoolePolynomial.h:467
bool_type operator==(const self &rhs) const
Definition: BoolePolynomial.h:282
bool_type isPair() const
Test, whether we have two terms only.
Definition: BoolePolynomial.h:475
BoolePolynomial(const ring_type &ring)
Default constructor.
Definition: BoolePolynomial.h:212
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
navigator navigation() const
Navigate through structure.
Definition: BoolePolynomial.h:441
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
bool dd_is_pair(NaviType navi)
Definition: pbori_algo.h:805
BoolePolyRing ring_type
Type for Boolean polynomial rings (without ordering)
Definition: BoolePolynomial.h:127
CGenericIter< LexOrder, navigator, monom_type > lex_iterator
Definition: BoolePolynomial.h:156
bool_type isOne() const
Check whether polynomial is constant one.
Definition: BoolePolynomial.h:297
BoolePolynomial(const navigator &rhs, const ring_type &ring)
Construct polynomial from navigator.
Definition: BoolePolynomial.h:229
hash_type stableHash() const
Get hash value, which is reproducible.
Definition: BoolePolynomial.h:334
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
dd_type::easy_equality_property easy_equality_property
The property whether the equality check is easy is inherited from dd_type.
Definition: BoolePolynomial.h:190
self & operator%=(constant_type rhs)
Definition: BoolePolynomial.h:277
bool_type operator==(constant_type rhs) const
Definition: BoolePolynomial.h:284
#define PBORI_RHS_MULT(type)
Multiplication with other left-hand side type.
Definition: BoolePolynomial.h:539
Marker for deg-lex ordering.
Definition: order_tags.h:32
bool_type isConstant() const
Check whether polynomial is zero or one.
Definition: BoolePolynomial.h:300
BooleSet dd_type
Definition: BoolePolynomial.h:102
binary_composition< std::plus< size_type >, project_ith< 1 >, integral_constant< size_type, 1 > > increment_type
Incrementation functional type.
Definition: BoolePolynomial.h:136
int deg_type
Definition: groebner_defs.h:42
const ring_type & ring() const
Access ring, where this belongs to.
Definition: BoolePolynomial.h:478
dd_type::first_iterator first_iterator
Iterator type for iterating over indices of the leading term.
Definition: BoolePolynomial.h:107
bool_type hasConstantPart() const
Check whether polynomial has term one.
Definition: BoolePolynomial.h:303
Accessing ith of n arguments (ITH = 0 returns default value of first type)
Definition: pbori_func.h:144
short int comp_type
Type for comparisons.
Definition: pbori_defs.h:237
Marker for lex ordering.
Definition: order_tags.h:27
self & operator*=(constant_type rhs)
Definition: BoolePolynomial.h:263
set_type set() const
Get corresponding subset of of the powerset over all variables.
Definition: BoolePolynomial.h:464
CGenericIter< DegLexOrder, navigator, exp_type > dlex_exp_iterator
Definition: BoolePolynomial.h:168
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
CTypes::comp_type comp_type
Type for result of polynomial comparisons.
Definition: BoolePolynomial.h:130
CGenericIter< DegLexOrder, navigator, monom_type > dlex_iterator
Definition: BoolePolynomial.h:158
Definition: pbori_func.h:722
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
integral_constant()() returns NUM of int_type, instead of possibly arguments...
Definition: pbori_func.h:263
CGenericIter< BlockDegLexOrder, navigator, monom_type > block_dlex_iterator
Definition: BoolePolynomial.h:163
lex_iterator const_iterator
Iterator type for iterating over all monomials.
Definition: BoolePolynomial.h:178
BoolePolynomial operator%(const BoolePolynomial &lhs, const RHSType &rhs)
Modulus monomial (division remainder)
Definition: BoolePolynomial.h:572
std::ostream ostream_type
Type for out-stream.
Definition: pbori_defs.h:246
BoolePolynomial::ostream_type & operator<<(BoolePolynomial::ostream_type &, const BoolePolynomial &)
Stream output operator.
Definition: BoolePolynomial.cc:744
BoolePolynomial::bool_type operator==(BoolePolynomial::bool_type lhs, const BoolePolynomial &rhs)
Equality check (with constant lhs)
Definition: BoolePolynomial.h:579
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
std::size_t hash_type
Type for hashing.
Definition: pbori_defs.h:231
Definition: BoolePolynomial.h:63
const dd_type & diagram() const
Read-only access to internal decision diagramm structure.
Definition: BoolePolynomial.h:461
std::map< self, std::vector< self >, symmetric_composition< std::less< navigator >, navigates< self > > > poly_vec_map_type
Definition: BoolePolynomial.h:199
bool dd_is_singleton(NaviType navi)
Definition: pbori_algo.h:770
BooleVariable var_type
Fix type for treatment of monomials.
Definition: BoolePolynomial.h:118
CGenericIter< BlockDegLexOrder, navigator, exp_type > block_dlex_exp_iterator
Definition: BoolePolynomial.h:172
bool_type isSingletonOrPair() const
Test, whether we have one or two terms only.
Definition: BoolePolynomial.h:470
CTypes::ostream_type ostream_type
Definition: BoolePolynomial.h:103
diagram_type firstDivisors() const
Get decison diagram representing the divisors of the first term.
Definition: CCuddDDFacade.h:445
#define PBORI_LHS_MULT(type)
Multiplication with other left-hand side type.
Definition: BoolePolynomial.h:552
std::vector< monom_type > termlist_type
Type for lists of terms.
Definition: BoolePolynomial.h:187
binary_composition< std::minus< size_type >, project_ith< 1 >, integral_constant< size_type, 1 > > decrement_type
Decrementation functional type.
Definition: BoolePolynomial.h:142
BooleSet set_type
Type for sets of Boolean variables.
Definition: BoolePolynomial.h:193
BoolePolynomial operator-(const BooleConstant &lhs, const BoolePolynomial &rhs)
Subtraction operation with constant right-hand-side.
Definition: BoolePolynomial.h:532
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
BooleConstant constant_type
Type for wrapping integer and bool values.
Definition: BoolePolynomial.h:124
navigator endOfNavigation() const
End of navigation marker.
Definition: BoolePolynomial.h:444
BoolePolynomial operator+(BooleConstant lhs, const BoolePolynomial &rhs)
Addition operation.
Definition: BoolePolynomial.h:517
Compose a binary function with a default constructable unary function for both arguments.
Definition: pbori_func.h:325
BoolePolynomial operator/(const BoolePolynomial &lhs, const RHSType &rhs)
Division by monomial (skipping remainder)
Definition: BoolePolynomial.h:565
COrderedIter< navigator, exp_type > ordered_exp_iterator
Iterator type for iterating over all exponents in ordering order.
Definition: BoolePolynomial.h:148
std::map< self, idx_type, symmetric_composition< std::less< navigator >, navigates< self > > > idx_map_type
Type for index maps.
Definition: BoolePolynomial.h:197
CGenericIter< BlockDegRevLexAscOrder, navigator, monom_type > block_dp_asc_iterator
Definition: BoolePolynomial.h:165
This class defines an iterator over the first minimal term of a given ZDD node.
Definition: CCuddFirstIter.h:35
Compose a binary function with two default constructable unary functions.
Definition: pbori_func.h:274
self & operator=(constant_type rhs)
Definition: BoolePolynomial.h:245
Definition: BoolePolynomial.h:67
self & operator%=(const self &rhs)
Definition: BoolePolynomial.h:274
Definition: BoolePolynomial.h:70
dd_type & internalDiagram()
Access to internal decision diagramm structure.
Definition: BoolePolynomial.h:488
set_type leadDivisors() const
Get all divisors of the leading term.
Definition: BoolePolynomial.h:328
Marker for ascending deg-rev-lex ordering.
Definition: order_tags.h:37
Marker for block orderings.
Definition: order_tags.h:43
BoolePolynomial & operator*=(BoolePolynomial &lhs, const BooleVariable &rhs)
Multiplication of a polynomial by a variable with assignment.
Definition: BooleMonomial.h:366
hash_type hash() const
Get unique hash value (may change from run to run)
Definition: BoolePolynomial.h:331
self & operator+=(constant_type rhs)
Definition: BoolePolynomial.h:252
CGenericIter< DegRevLexAscOrder, navigator, exp_type > dp_asc_exp_iterator
Definition: BoolePolynomial.h:170
dd_type::navigator navigator
Iterator-like type for navigating through diagram structure.
Definition: BoolePolynomial.h:110
bool_type isZero() const
Check whether polynomial is constant zero.
Definition: BoolePolynomial.h:294
const self & operator-() const
Definition: BoolePolynomial.h:250
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
BooleMonomial monom_type
Fix type for treatment of monomials.
Definition: BoolePolynomial.h:115
~BoolePolynomial()
Destructor.
Definition: BoolePolynomial.h:235
CGenericIter< LexOrder, navigator, deg_type > deg_iterator
Iterator type for iterating all monomials (dereferencing to degree)
Definition: BoolePolynomial.h:184
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
BoolePolynomial::bool_type operator!=(BoolePolynomial::bool_type lhs, const BoolePolynomial &rhs)
Nonquality check (with constant lhs)
Definition: BoolePolynomial.h:586
CGenericIter< DegRevLexAscOrder, navigator, monom_type > dp_asc_iterator
Definition: BoolePolynomial.h:160
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
Definition: BooleSet.h:57
bool dd_is_singleton_or_pair(NaviType navi)
Definition: pbori_algo.h:798
This class wraps a bool value, which was not converted to a boolean polynomial or monomial yet...
Definition: BooleConstant.h:40
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
Definition: BoolePolynomial.h:60
bool bool_type
Type for standard true/false statements.
Definition: pbori_defs.h:216
self & operator-=(const RHSType &rhs)
Definition: BoolePolynomial.h:259
BoolePolynomial(constant_type isOne, const ring_type &ring)
Construct polynomial in given ring from a constant value 0 or 1.
Definition: BoolePolynomial.h:216
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleVariable.h:39
CExpIter< navigator, exp_type > exp_iterator
Iterator type for iterating all exponent vectors.
Definition: BoolePolynomial.h:181
COrderedIter< navigator, monom_type > ordered_iterator
Iterator type for iterating over all monomials in ordering order.
Definition: BoolePolynomial.h:152
BoolePolynomial(const dd_type &rhs)
Construct polynomial from decision diagram.
Definition: BoolePolynomial.h:220
This class shows, whether a property of an order is valid.
Definition: tags.h:32
BooleExponent exp_type
Fix type for treatment of exponent vectors.
Definition: BoolePolynomial.h:121
bool_type operator!=(const self &rhs) const
Definition: BoolePolynomial.h:283
Definition: BoolePolynomial.h:73
dd_type copyDiagram()
gives a copy of the diagram
Definition: BoolePolynomial.h:447