PolyBoRi
Public Types | Public Member Functions | List of all members
polybori::BooleSet Class Reference

#include <BooleSet.h>

Inheritance diagram for polybori::BooleSet:
polybori::CDDInterface< CuddLikeZDD > polybori::CDDInterfaceBase< CuddLikeZDD >

Public Types

typedef BooleSet self
 Generic access to type of *this.
typedef CTypes::dd_type base
 Generic access to base type.
typedef base dd_type
 Generic access to underlying diagram type.
typedef base::navigator navigator
typedef base::size_type size_type
typedef base::idx_type idx_type
typedef BooleMonomial term_type
 Type of terms.
typedef BooleExponent exp_type
 Fix type for treatment of exponent vectors.
typedef BooleRing ring_type
 Type for Boolean polynomial rings (without ordering)
typedef CGenericIter< LexOrder,
navigator, term_type
const_iterator
 Iterator type for iterating all monomials.
typedef CGenericIter< LexOrder,
navigator, exp_type
exp_iterator
 Iterator type for iterating all exponent vectors.
- Public Types inherited from polybori::CDDInterface< CuddLikeZDD >
typedef CuddLikeZDD interfaced_type
 Interfacing Cudd's zero-suppressed decision diagram type.
typedef zdd_traits
< interfaced_type >
::manager_base 
manager_base
 Cudd's decision diagram manager type.
typedef manager_traits
< manager_base >::tmp_ref 
mgr_ref
 Reference to decision diagram manager type.
typedef manager_traits
< manager_base >::core_type 
core_type
 Decision diagram manager core type.
typedef CDDManager
< CCuddInterface
manager_type
 Interface to Cudd's decision diagram manager type.
typedef CDDInterfaceBase
< interfaced_type
base_type
 Generic access to base type.
typedef base_type base
typedef CDDInterface
< interfaced_type
self
 Generic access to type of *this.
typedef CTypes::size_type size_type
 Define size type.
typedef CTypes::idx_type idx_type
 Define index type.
typedef CTypes::ostream_type ostream_type
 Type for output streams.
typedef CTypes::bool_type bool_type
 Type for comparisons.
typedef CTypes::hash_type hash_type
 Type for hashed.
typedef CCuddFirstIter first_iterator
 Iterator type for retrieving first term from Cudd's ZDDs.
typedef CCuddLastIter last_iterator
 Iterator type for retrieving last term from Cudd's ZDDs.
typedef CCuddNavigator navigator
 Iterator type for navigation throught Cudd's ZDDs structure.
typedef FILE * pretty_out_type
 Type for output of pretty print.
typedef const char * filename_type
 Type for file name of pretty print output.
typedef valid_tag easy_equality_property
 This type has an easy equality check.
- Public Types inherited from polybori::CDDInterfaceBase< CuddLikeZDD >
typedef CuddLikeZDD interfaced_type
 The interfaced type.
typedef CDDInterfaceBase
< interfaced_type
self
 Generic access to type of *this.

Public Member Functions

 BooleSet ()
 Default constructor.
 BooleSet (const self &rhs)
 Copy constructor.
 BooleSet (const base &rhs)
 Copy constructor.
 BooleSet (idx_type idx, const self &first, const self &second)
 Construct new node.
 BooleSet (idx_type idx, navigator first, navigator second, const ring_type &ring)
 Construct new node (using navigator nodes)
 BooleSet (idx_type idx, const self &rhs)
 Construct new node (using navigator for then and else-branches)
 BooleSet (navigator navi, const ring_type &ring)
 Construct one or zero set from constant.
 ~BooleSet ()
 Destructor.
const_iterator begin () const
 Start of iteration over terms.
const_iterator end () const
 Finish of iteration over terms.
exp_iterator expBegin () const
 Start of iteration over exponent vectors.
exp_iterator expEnd () const
 Finish of iteration over exponent vectors.
selfoperator= (const self &)
 Assignment operator.
term_type usedVariables () const
 Set of variables of the whole set.
exp_type usedVariablesExp () const
 Exponent vector of variables of the whole set.
selfaddAssign (const term_type &)
 Add given monomial to sets and assign.
self add (const term_type &) const
 Add given monomial to sets.
bool_type owns (const term_type &) const
 Check whether rhs is included in *this.
bool_type owns (const exp_type &) const
 Check whether rhs is included in *this.
term_type lastLexicographicalTerm () const
 Get last term (wrt. lexicographical order)
self divisorsOf (const term_type &rhs) const
 Compute intersection with divisors of rhs.
self divisorsOf (const exp_type &rhs) const
 Compute intersection with divisors of rhs.
self firstDivisorsOf (const self &rhs) const
 Intersection with divisors of first (lexicographical) term of rhs.
self multiplesOf (const term_type &rhs) const
 Compute intersection with multiples of rhs.
self divide (const term_type &rhs) const
 Division by given term.
selfdivideAssign (const term_type &rhs)
 Division with assignment by given term.
bool_type hasTermOfVariables (const term_type &rhs) const
 Check for empty intersection with divisors of rhs.
self minimalElements () const
 Get minimal elements wrt. inclusion.
bool_type isSingleton () const
 Test, whether we have one term only.
bool_type isSingletonOrPair () const
 Test, whether we have one or two terms only.
bool_type isPair () const
 Test, whether we have two terms only.
self existAbstract (const term_type &rhs) const
 Compute existential abstraction.
const dd_typediagram () const
 Access internal decision diagram.
self ite (const self &then_dd, const self &else_dd)
 If-Then-Else operation.
selfiteAssign (const self &then_dd, const self &else_dd)
 If-Then-Else operation with assignment.
self cartesianProduct (const self &rhs) const
 Cartesean product.
ostream_typeprint (ostream_type &) const
 Print current set to output stream.
self emptyElement () const
 Get corresponding zero element (may be removed in the future)
size_type countIndex (idx_type idx) const
 Count terms containing BooleVariable(idx)
double countIndexDouble (idx_type idx) const
 Count many terms containing BooleVariable(idx)
ring_type ring () const
 Access ring, where this belongs to.
Members from base
self subset0 (idx_type idx) const
 Generate subset, where decision diagram manager variable idx is false.
self subset1 (idx_type idx) const
 Generate subset, where decision diagram manager variable idx is asserted.
self change (idx_type idx) const
 Substitute variable with index idx by its complement.
self unite (const self &rhs) const
self diff (const self &rhs) const
self diffConst (const self &rhs) const
self intersect (const self &rhs) const
self product (const self &rhs) const
self dotProduct (const self &rhs) const
self Xor (const self &rhs) const
self ddDivide (const self &rhs) const
self weakDivide (const self &rhs) const
self divideFirst (const self &rhs) const
selfsubset0Assign (idx_type idx)
selfsubset1Assign (idx_type idx)
 subset1 with assignment
selfchangeAssign (idx_type idx)
 Change with assignment.
selfuniteAssign (const self &rhs)
selfdiffAssign (const self &rhs)
selfdiffConstAssign (const self &rhs)
selfintersectAssign (const self &rhs)
selfproductAssign (const self &rhs)
selfdotProductAssign (const self &rhs)
selfddDivideAssign (const self &rhs)
selfweakDivideAssign (const self &rhs)
selfdivideFirstAssign (const self &rhs)
- Public Member Functions inherited from polybori::CDDInterface< CuddLikeZDD >
 CDDInterface ()
 Default constructor.
 CDDInterface (const self &rhs)
 Copy constructor.
 CDDInterface (const interfaced_type &rhs)
 Construct from interfaced type.
 CDDInterface (const manager_base &mgr, const navigator &navi)
 Construct from Manager and navigator.
 CDDInterface (const manager_base &mgr, idx_type idx, navigator thenNavi, navigator elseNavi)
 Construct new node from manager, index, and navigators.
 CDDInterface (const manager_base &mgr, idx_type idx, navigator navi)
 CDDInterface (idx_type idx, const self &thenDD, const self &elseDD)
 Construct new node.
 ~CDDInterface ()
 Destructor.
hash_type hash () const
 Get unique hash value (valid only per runtime)
hash_type stableHash () const
 Get stable hash value, which is reproducible.
self unite (const self &rhs) const
 Set union.
selfuniteAssign (const self &rhs)
 Set union with assignment.
self ite (const self &then_dd, const self &else_dd) const
 If-Then-Else operation.
selfiteAssign (const self &then_dd, const self &else_dd)
 If-Then-Else operation with assignment.
self diff (const self &rhs) const
 Set difference.
selfdiffAssign (const self &rhs)
 Set difference with assignment.
self diffConst (const self &rhs) const
 Set difference.
selfdiffConstAssign (const self &rhs)
 Set difference with assignment.
self intersect (const self &rhs) const
 Set intersection.
selfintersectAssign (const self &rhs)
 Set intersection with assignment.
self product (const self &rhs) const
 Product.
selfproductAssign (const self &rhs)
 Product with assignment.
self unateProduct (const self &rhs) const
 Unate product.
self dotProduct (const self &rhs) const
 Returns dot Product.
selfdotProductAssign (const self &rhs)
self Xor (const self &rhs) const
selfunateProductAssign (const self &rhs)
 Unate product with assignment.
self ddDivide (const self &rhs) const
 Division.
selfddDivideAssign (const self &rhs)
 Division with assignment.
self weakDivide (const self &rhs) const
 Weak division.
selfweakDivideAssign (const self &rhs)
 Weak division with assignment.
selfdivideFirstAssign (const self &rhs)
 Division with first term of right-hand side and assignment.
self divideFirst (const self &rhs) const
 Division with first term of right-hand side.
size_type nNodes () const
 Get number of nodes in decision diagram.
void prettyPrint (pretty_out_type filehandle=stdout) const
 Print Dot-output to file given by file handle.
bool_type prettyPrint (filename_type filename) const
 Print Dot-output to file given by file name.
bool_type operator== (const self &rhs) const
 Equality check.
bool_type operator!= (const self &rhs) const
 Nonequality check.
mgr_ref manager () const
 Get reference to actual decision diagram manager.
core_type managerCore () const
size_type nSupport () const
 Get numbers of used variables.
self support () const
 Get multiples of used variables.
template<class VectorLikeType >
void usedIndices (VectorLikeType &indices) const
 Get used variables (assuming indices of zero length)
int * usedIndices () const
 Get used variables (assuming indices of length nSupport())
first_iterator firstBegin () const
 Start of first term.
first_iterator firstEnd () const
 Finish of first term.
last_iterator lastBegin () const
 Start of first term.
last_iterator lastEnd () const
 Finish of first term.
self firstMultiples (const std::vector< idx_type > &multipliers) const
 Get decison diagram representing the multiples of the first term.
self subSet (const self &rhs) const
self supSet (const self &rhs) const
self firstDivisors () const
 Get decison diagram representing the divisors of the first term.
navigator navigation () const
 Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
bool_type emptiness () const
 Checks whether the decision diagram is empty.
bool_type blankness () const
 Checks whether the decision diagram has every variable negated.
bool_type isConstant () const
size_type size () const
 Returns number of terms.
size_type length () const
 Returns number of terms (deprecated)
size_type nVariables () const
 Returns number of variables in manager.
self cofactor0 (const self &rhs) const
self cofactor1 (const self &rhs, idx_type includeVars) const
bool_type ownsOne () const
 Test whether the empty set is included.
double sizeDouble () const
self blankElement () const
 Get corresponding one element.
- Public Member Functions inherited from polybori::CDDInterfaceBase< CuddLikeZDD >
 CDDInterfaceBase ()
 Default constructor.
 CDDInterfaceBase (const interfaced_type &interfaced)
 Construct instance from interfaced type.
 CDDInterfaceBase (const self &rhs)
 Copy constructor.
 ~CDDInterfaceBase ()
 Destructor.
 operator const interfaced_type & () const
 Constant casting operator to interfaced type.

Additional Inherited Members

- Protected Attributes inherited from polybori::CDDInterfaceBase< CuddLikeZDD >
interfaced_type m_interfaced

Member Typedef Documentation

Generic access to base type.

Iterator type for iterating all monomials.

Generic access to underlying diagram type.

Iterator type for iterating all exponent vectors.

Fix type for treatment of exponent vectors.

Type for Boolean polynomial rings (without ordering)

Generic access to type of *this.

Type of terms.

Constructor & Destructor Documentation

polybori::BooleSet::BooleSet ( )

Default constructor.

References PBORI_TRACE_FUNC.

polybori::BooleSet::BooleSet ( const self rhs)
inline

Copy constructor.

polybori::BooleSet::BooleSet ( const base rhs)
inline

Copy constructor.

polybori::BooleSet::BooleSet ( idx_type  idx,
const self first,
const self second 
)
inline

Construct new node.

polybori::BooleSet::BooleSet ( idx_type  idx,
navigator  first,
navigator  second,
const ring_type ring 
)
inline

Construct new node (using navigator nodes)

polybori::BooleSet::BooleSet ( idx_type  idx,
const self rhs 
)
inline

Construct new node (using navigator for then and else-branches)

polybori::BooleSet::BooleSet ( navigator  navi,
const ring_type ring 
)
inline

Construct one or zero set from constant.

Todo:
temporarily deactivated, as it slow downs procedures like term_accumulate, needs check, what happens to inlinings etc. in this case

Construct from navigator node

polybori::BooleSet::~BooleSet ( )
inline

Destructor.

Member Function Documentation

BooleSet polybori::BooleSet::add ( const term_type rhs) const

Add given monomial to sets.

References PBORI_TRACE_FUNC.

BooleSet & polybori::BooleSet::addAssign ( const term_type rhs)

Add given monomial to sets and assign.

References polybori::BooleMonomial::diagram(), PBORI_TRACE_FUNC, and uniteAssign().

BooleSet::const_iterator polybori::BooleSet::begin ( ) const
self polybori::BooleSet::cartesianProduct ( const self rhs) const
inline

Cartesean product.

self polybori::BooleSet::change ( idx_type  idx) const
inline
self& polybori::BooleSet::changeAssign ( idx_type  idx)
inline

Change with assignment.

Reimplemented from polybori::CDDInterface< CuddLikeZDD >.

BooleSet::size_type polybori::BooleSet::countIndex ( idx_type  idx) const

Count terms containing BooleVariable(idx)

References polybori::count_index(), and polybori::CDDInterface< CuddLikeZDD >::size().

double polybori::BooleSet::countIndexDouble ( idx_type  idx) const

Count many terms containing BooleVariable(idx)

References polybori::count_index(), and polybori::CDDInterface< CuddLikeZDD >::size().

self polybori::BooleSet::ddDivide ( const self rhs) const
inline
self& polybori::BooleSet::ddDivideAssign ( const self rhs)
inline
const dd_type& polybori::BooleSet::diagram ( ) const
inline

Access internal decision diagram.

Referenced by divisorsOf().

self polybori::BooleSet::diff ( const self rhs) const
inline
self& polybori::BooleSet::diffAssign ( const self rhs)
inline
self polybori::BooleSet::diffConst ( const self rhs) const
inline
self& polybori::BooleSet::diffConstAssign ( const self rhs)
inline
BooleSet polybori::BooleSet::divide ( const term_type rhs) const
BooleSet & polybori::BooleSet::divideAssign ( const term_type rhs)
self polybori::BooleSet::divideFirst ( const self rhs) const
inline
self& polybori::BooleSet::divideFirstAssign ( const self rhs)
inline
BooleSet polybori::BooleSet::divisorsOf ( const term_type rhs) const
BooleSet polybori::BooleSet::divisorsOf ( const exp_type rhs) const

Compute intersection with divisors of rhs.

References diagram(), firstDivisorsOf(), PBORI_TRACE_FUNC, and ring().

self polybori::BooleSet::dotProduct ( const self rhs) const
inline
self& polybori::BooleSet::dotProductAssign ( const self rhs)
inline
self polybori::BooleSet::emptyElement ( ) const
inline

Get corresponding zero element (may be removed in the future)

Reimplemented from polybori::CDDInterface< CuddLikeZDD >.

BooleSet::const_iterator polybori::BooleSet::end ( ) const
BooleSet polybori::BooleSet::existAbstract ( const term_type rhs) const
BooleSet::exp_iterator polybori::BooleSet::expBegin ( ) const
BooleSet::exp_iterator polybori::BooleSet::expEnd ( ) const
BooleSet polybori::BooleSet::firstDivisorsOf ( const self rhs) const

Intersection with divisors of first (lexicographical) term of rhs.

References polybori::dd_first_divisors_of(), polybori::CDDInterface< CuddLikeZDD >::manager(), polybori::CDDInterface< CuddLikeZDD >::navigation(), and PBORI_TRACE_FUNC.

Referenced by divisorsOf().

BooleSet::bool_type polybori::BooleSet::hasTermOfVariables ( const term_type rhs) const
self polybori::BooleSet::intersect ( const self rhs) const
inline
self& polybori::BooleSet::intersectAssign ( const self rhs)
inline
bool_type polybori::BooleSet::isPair ( ) const
inline

Test, whether we have two terms only.

References polybori::dd_is_pair().

bool_type polybori::BooleSet::isSingleton ( ) const
inline

Test, whether we have one term only.

References polybori::dd_is_singleton().

bool_type polybori::BooleSet::isSingletonOrPair ( ) const
inline

Test, whether we have one or two terms only.

References polybori::dd_is_singleton_or_pair().

self polybori::BooleSet::ite ( const self then_dd,
const self else_dd 
)
inline

If-Then-Else operation.

self& polybori::BooleSet::iteAssign ( const self then_dd,
const self else_dd 
)
inline

If-Then-Else operation with assignment.

BooleSet::term_type polybori::BooleSet::lastLexicographicalTerm ( ) const

Get last term (wrt. lexicographical order)

References polybori::dd_last_lexicographical_term(), and PBORI_TRACE_FUNC.

BooleSet polybori::BooleSet::minimalElements ( ) const
BooleSet polybori::BooleSet::multiplesOf ( const term_type rhs) const
BooleSet & polybori::BooleSet::operator= ( const self rhs)

Assignment operator.

References PBORI_TRACE_FUNC.

BooleSet::bool_type polybori::BooleSet::owns ( const term_type rhs) const
BooleSet::bool_type polybori::BooleSet::owns ( const exp_type rhs) const
BooleSet::ostream_type & polybori::BooleSet::print ( ostream_type os) const
self polybori::BooleSet::product ( const self rhs) const
inline
self& polybori::BooleSet::productAssign ( const self rhs)
inline
ring_type polybori::BooleSet::ring ( ) const
inline
self polybori::BooleSet::subset0 ( idx_type  idx) const
inline
self& polybori::BooleSet::subset0Assign ( idx_type  idx)
inline
Todo:
Do we really nee the assign variante here at high level?

Reimplemented from polybori::CDDInterface< CuddLikeZDD >.

self polybori::BooleSet::subset1 ( idx_type  idx) const
inline
self& polybori::BooleSet::subset1Assign ( idx_type  idx)
inline

subset1 with assignment

Reimplemented from polybori::CDDInterface< CuddLikeZDD >.

self polybori::BooleSet::unite ( const self rhs) const
inline
self& polybori::BooleSet::uniteAssign ( const self rhs)
inline
BooleSet::term_type polybori::BooleSet::usedVariables ( ) const

Set of variables of the whole set.

References PBORI_TRACE_FUNC.

BooleSet::exp_type polybori::BooleSet::usedVariablesExp ( ) const

Exponent vector of variables of the whole set.

References PBORI_TRACE_FUNC, and polybori::CDDInterface< CuddLikeZDD >::usedIndices().

self polybori::BooleSet::weakDivide ( const self rhs) const
inline
self& polybori::BooleSet::weakDivideAssign ( const self rhs)
inline
self polybori::BooleSet::Xor ( const self rhs) const
inline

The documentation for this class was generated from the following files: