#include <CDDInterface.h>
Public Types | |
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::deg_type | deg_type |
Define degree 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 Member Functions | |
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. | |
self & | uniteAssign (const self &rhs) |
Set union with assignment. | |
self | ite (const self &then_dd, const self &else_dd) const |
If-Then-Else operation. | |
self & | iteAssign (const self &then_dd, const self &else_dd) |
If-Then-Else operation with assignment. | |
self | diff (const self &rhs) const |
Set difference. | |
self & | diffAssign (const self &rhs) |
Set difference with assignment. | |
self | diffConst (const self &rhs) const |
Set difference. | |
self & | diffConstAssign (const self &rhs) |
Set difference with assignment. | |
self | intersect (const self &rhs) const |
Set intersection. | |
self & | intersectAssign (const self &rhs) |
Set intersection with assignment. | |
self | product (const self &rhs) const |
Product. | |
self & | productAssign (const self &rhs) |
Product with assignment. | |
self | unateProduct (const self &rhs) const |
Unate product. | |
self | dotProduct (const self &rhs) const |
Returns dot Product. | |
self & | dotProductAssign (const self &rhs) |
self | Xor (const self &rhs) const |
self & | unateProductAssign (const self &rhs) |
Unate product with assignment. | |
self | subset0 (idx_type idx) const |
Generate subset, where decision diagram manager variable idx is false. | |
self & | subset0Assign (idx_type idx) |
subset0 with assignment | |
self | subset1 (idx_type idx) const |
Generate subset, where decision diagram manager variable idx is asserted. | |
self & | subset1Assign (idx_type idx) |
subset1 with assignment | |
self | change (idx_type idx) const |
Substitute variable with index idx by its complement. | |
self & | changeAssign (idx_type idx) |
Change with assignment. | |
self | ddDivide (const self &rhs) const |
Division. | |
self & | ddDivideAssign (const self &rhs) |
Division with assignment. | |
self | weakDivide (const self &rhs) const |
Weak division. | |
self & | weakDivideAssign (const self &rhs) |
Weak division with assignment. | |
self & | divideFirstAssign (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. | |
ostream_type & | print (ostream_type &os) 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 | emptyElement () const |
Get corresponding zero element. | |
self | blankElement () const |
Get corresponding one element. |
For Cudd-like ZDDs, like ZDD or CCuddZDD
typedef base_type CDDInterface< CuddLikeZDD >::base |
Reimplemented in BooleSet.
typedef CDDInterfaceBase<interfaced_type> CDDInterface< CuddLikeZDD >::base_type |
Generic access to base type.
typedef CTypes::bool_type CDDInterface< CuddLikeZDD >::bool_type |
Type for comparisons.
typedef manager_traits<manager_base>::core_type CDDInterface< CuddLikeZDD >::core_type |
Decision diagram manager core type.
typedef CTypes::deg_type CDDInterface< CuddLikeZDD >::deg_type |
Define degree type.
typedef valid_tag CDDInterface< CuddLikeZDD >::easy_equality_property |
This type has an easy equality check.
typedef const char* CDDInterface< CuddLikeZDD >::filename_type |
Type for file name of pretty print output.
typedef CCuddFirstIter CDDInterface< CuddLikeZDD >::first_iterator |
Iterator type for retrieving first term from Cudd's ZDDs.
typedef CTypes::hash_type CDDInterface< CuddLikeZDD >::hash_type |
Type for hashed.
typedef CTypes::idx_type CDDInterface< CuddLikeZDD >::idx_type |
Define index type.
Reimplemented in BooleSet.
typedef CuddLikeZDD CDDInterface< CuddLikeZDD >::interfaced_type |
Interfacing Cudd's zero-suppressed decision diagram type.
Reimplemented from CDDInterfaceBase< CuddLikeZDD >.
typedef CCuddLastIter CDDInterface< CuddLikeZDD >::last_iterator |
Iterator type for retrieving last term from Cudd's ZDDs.
typedef zdd_traits<interfaced_type>::manager_base CDDInterface< CuddLikeZDD >::manager_base |
Cudd's decision diagram manager type.
typedef CDDManager<CCuddInterface> CDDInterface< CuddLikeZDD >::manager_type |
Interface to Cudd's decision diagram manager type.
typedef manager_traits<manager_base>::tmp_ref CDDInterface< CuddLikeZDD >::mgr_ref |
Reference to decision diagram manager type.
typedef CCuddNavigator CDDInterface< CuddLikeZDD >::navigator |
Iterator type for navigation throught Cudd's ZDDs structure.
Reimplemented in BooleSet.
typedef CTypes::ostream_type CDDInterface< CuddLikeZDD >::ostream_type |
Type for output streams.
typedef FILE* CDDInterface< CuddLikeZDD >::pretty_out_type |
Type for output of pretty print.
typedef CDDInterface<interfaced_type> CDDInterface< CuddLikeZDD >::self |
Generic access to type of *this.
Reimplemented from CDDInterfaceBase< CuddLikeZDD >.
Reimplemented in BooleSet.
typedef CTypes::size_type CDDInterface< CuddLikeZDD >::size_type |
Define size type.
Reimplemented in BooleSet.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | ) | [inline] |
Default constructor.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | const self & | rhs | ) | [inline] |
Copy constructor.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | const interfaced_type & | rhs | ) | [inline] |
Construct from interfaced type.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | const manager_base & | mgr, | |
const navigator & | navi | |||
) | [inline] |
Construct from Manager and navigator.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | const manager_base & | mgr, | |
idx_type | idx, | |||
navigator | thenNavi, | |||
navigator | elseNavi | |||
) | [inline] |
Construct new node from manager, index, and navigators.
CDDInterface< CuddLikeZDD >::CDDInterface | ( | const manager_base & | mgr, | |
idx_type | idx, | |||
navigator | navi | |||
) | [inline] |
Construct new node from manager, index, and common navigator for then and else-branches
CDDInterface< CuddLikeZDD >::CDDInterface | ( | idx_type | idx, | |
const self & | thenDD, | |||
const self & | elseDD | |||
) | [inline] |
Construct new node.
CDDInterface< CuddLikeZDD >::~CDDInterface | ( | ) | [inline] |
Destructor.
self CDDInterface< CuddLikeZDD >::blankElement | ( | ) | const [inline] |
Get corresponding one element.
References CDDInterface< CuddLikeZDD >::manager().
bool_type CDDInterface< CuddLikeZDD >::blankness | ( | ) | const [inline] |
Checks whether the decision diagram has every variable negated.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, CDDInterface< CuddLikeZDD >::manager(), and CDDInterface< CuddLikeZDD >::nVariables().
Referenced by BoolePolynomial::isOne().
self CDDInterface< CuddLikeZDD >::change | ( | idx_type | idx | ) | const [inline] |
Substitute variable with index idx by its complement.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by LiteralFactorization::LiteralFactorization(), lower_term_accumulate(), term_accumulate(), and CDDManagerBase< CCuddInterface, CCuddInterface >::variable().
self& CDDInterface< CuddLikeZDD >::changeAssign | ( | idx_type | idx | ) | [inline] |
Change with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BoolePolynomial::BoolePolynomial(), and BooleMonomial::changeAssign().
self CDDInterface< CuddLikeZDD >::cofactor0 | ( | const self & | rhs | ) | const [inline] |
self CDDInterface< CuddLikeZDD >::cofactor1 | ( | const self & | rhs, | |
idx_type | includeVars | |||
) | const [inline] |
self CDDInterface< CuddLikeZDD >::ddDivide | ( | const self & | rhs | ) | const [inline] |
Division.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self& CDDInterface< CuddLikeZDD >::ddDivideAssign | ( | const self & | rhs | ) | [inline] |
Division with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self CDDInterface< CuddLikeZDD >::diff | ( | const self & | rhs | ) | const [inline] |
Set difference.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self& CDDInterface< CuddLikeZDD >::diffAssign | ( | const self & | rhs | ) | [inline] |
Set difference with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BoolePolynomial::operator%=().
self CDDInterface< CuddLikeZDD >::diffConst | ( | const self & | rhs | ) | const [inline] |
Set difference.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::contains().
self& CDDInterface< CuddLikeZDD >::diffConstAssign | ( | const self & | rhs | ) | [inline] |
Set difference with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self CDDInterface< CuddLikeZDD >::divideFirst | ( | const self & | rhs | ) | const [inline] |
Division with first term of right-hand side.
Referenced by BooleSet::divide().
self& CDDInterface< CuddLikeZDD >::divideFirstAssign | ( | const self & | rhs | ) | [inline] |
Division with first term of right-hand side and assignment.
Referenced by BooleSet::divideAssign().
self CDDInterface< CuddLikeZDD >::dotProduct | ( | const self & | rhs | ) | const [inline] |
Returns dot Product.
References Extra_zddDotProduct(), CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
self& CDDInterface< CuddLikeZDD >::dotProductAssign | ( | const self & | rhs | ) | [inline] |
bool_type CDDInterface< CuddLikeZDD >::emptiness | ( | ) | const [inline] |
Checks whether the decision diagram is empty.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
Referenced by BooleSet::contains(), BoolePolynomial::firstDivisors(), BooleSet::hasTermOfVariables(), LexHelper::irreducible_lead(), BoolePolynomial::isZero(), LiteralFactorization::LiteralFactorization(), BooleSet::owns(), and BooleSet::print().
self CDDInterface< CuddLikeZDD >::emptyElement | ( | ) | const [inline] |
Get corresponding zero element.
Reimplemented in BooleSet.
References CDDInterface< CuddLikeZDD >::manager().
Referenced by BooleSet::emptyElement().
first_iterator CDDInterface< CuddLikeZDD >::firstBegin | ( | ) | const [inline] |
Start of first term.
References CDDInterface< CuddLikeZDD >::navigation().
Referenced by BoolePolynomial::firstBegin(), CDDInterface< CuddLikeZDD >::firstDivisors(), CDDInterface< CuddLikeZDD >::firstMultiples(), and BooleExponent::multiplyFirst().
self CDDInterface< CuddLikeZDD >::firstDivisors | ( | ) | const [inline] |
Get decison diagram representing the divisors of the first term.
References cudd_generate_divisors(), CDDInterface< CuddLikeZDD >::firstBegin(), CDDInterface< CuddLikeZDD >::firstEnd(), and CDDInterface< CuddLikeZDD >::manager().
Referenced by BoolePolynomial::firstDivisors().
first_iterator CDDInterface< CuddLikeZDD >::firstEnd | ( | ) | const [inline] |
Finish of first term.
Referenced by CDDInterface< CuddLikeZDD >::firstDivisors(), BoolePolynomial::firstEnd(), CDDInterface< CuddLikeZDD >::firstMultiples(), and BooleExponent::multiplyFirst().
self CDDInterface< CuddLikeZDD >::firstMultiples | ( | const std::vector< idx_type > & | multipliers | ) | const [inline] |
Get decison diagram representing the multiples of the first term.
References cudd_generate_multiples(), CDDInterface< CuddLikeZDD >::firstBegin(), CDDInterface< CuddLikeZDD >::firstEnd(), and CDDInterface< CuddLikeZDD >::manager().
hash_type CDDInterface< CuddLikeZDD >::hash | ( | ) | const [inline] |
Get unique hash value (valid only per runtime).
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BoolePolynomial::hash().
self CDDInterface< CuddLikeZDD >::intersect | ( | const self & | rhs | ) | const [inline] |
Set intersection.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::owns().
self& CDDInterface< CuddLikeZDD >::intersectAssign | ( | const self & | rhs | ) | [inline] |
Set intersection with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
bool_type CDDInterface< CuddLikeZDD >::isConstant | ( | ) | const [inline] |
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BoolePolynomial::isConstant().
self CDDInterface< CuddLikeZDD >::ite | ( | const self & | then_dd, | |
const self & | else_dd | |||
) | const [inline] |
If-Then-Else operation.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::ite().
self& CDDInterface< CuddLikeZDD >::iteAssign | ( | const self & | then_dd, | |
const self & | else_dd | |||
) | [inline] |
If-Then-Else operation with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::iteAssign().
last_iterator CDDInterface< CuddLikeZDD >::lastBegin | ( | ) | const [inline] |
Start of first term.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
last_iterator CDDInterface< CuddLikeZDD >::lastEnd | ( | ) | const [inline] |
Finish of first term.
size_type CDDInterface< CuddLikeZDD >::length | ( | ) | const [inline] |
Returns number of terms (deprecated).
References CDDInterface< CuddLikeZDD >::size().
Referenced by BoolePolynomial::length(), and LiteralFactorization::LiteralFactorization().
mgr_ref CDDInterface< CuddLikeZDD >::manager | ( | ) | const [inline] |
Get reference to actual decision diagram manager.
References get_manager(), and CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by CDDInterface< CuddLikeZDD >::blankElement(), CDDInterface< CuddLikeZDD >::blankness(), CDDInterface< CuddLikeZDD >::cofactor0(), CDDInterface< CuddLikeZDD >::cofactor1(), BoolePolynomial::deg(), BooleExponent::divisors(), CDDInterface< CuddLikeZDD >::dotProduct(), CDDInterface< CuddLikeZDD >::dotProductAssign(), CDDInterface< CuddLikeZDD >::emptiness(), CDDInterface< CuddLikeZDD >::emptyElement(), BooleSet::existAbstract(), CDDInterface< CuddLikeZDD >::firstDivisors(), BooleSet::firstDivisorsOf(), CDDInterface< CuddLikeZDD >::firstMultiples(), BoolePolynomial::gradedPart(), BooleSet::minimalElements(), BooleExponent::multiples(), BooleSet::multiplesOf(), CDDInterface< CuddLikeZDD >::nSupport(), CDDInterface< CuddLikeZDD >::nVariables(), BooleMonomial::popFirst(), CDDInterface< CuddLikeZDD >::print(), BooleSet::ring(), BoolePolynomial::ring(), CDDInterface< CuddLikeZDD >::subSet(), CDDInterface< CuddLikeZDD >::support(), CDDInterface< CuddLikeZDD >::supSet(), CDDInterface< CuddLikeZDD >::usedIndices(), and CDDInterface< CuddLikeZDD >::Xor().
core_type CDDInterface< CuddLikeZDD >::managerCore | ( | ) | const [inline] |
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::begin(), BoolePolynomial::begin(), BoolePolynomial::degBegin(), BooleSet::expBegin(), BoolePolynomial::genericBegin(), BoolePolynomial::genericExpBegin(), BooleSet::print(), BoolePolynomial::print(), and BooleSet::rbegin().
navigator CDDInterface< CuddLikeZDD >::navigation | ( | ) | const [inline] |
Navigate through ZDD by incrementThen(), incrementElse(), and terminated().
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::begin(), BooleSet::containsDivisorsOfDecDeg(), BooleSet::existAbstract(), BooleSet::expBegin(), CDDInterface< CuddLikeZDD >::firstBegin(), BooleSet::firstDivisorsOf(), BooleSet::hasTermOfVariables(), BooleSet::isPair(), BooleSet::isSingleton(), BooleSet::isSingletonOrPair(), ll_red_nf_generic(), BooleSet::minimalElements(), BooleSet::multiplesOf(), BoolePolynomial::navigation(), BoolePolynomial::operator*=(), BoolePolynomial::operator/=(), BooleSet::owns(), CDDInterface< CuddLikeZDD >::ownsOne(), BooleSet::rbegin(), and CDDInterface< CuddLikeZDD >::stableHash().
size_type CDDInterface< CuddLikeZDD >::nNodes | ( | ) | const [inline] |
Get number of nodes in decision diagram.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BoolePolynomial::nNodes().
size_type CDDInterface< CuddLikeZDD >::nSupport | ( | ) | const [inline] |
Get numbers of used variables.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
Referenced by BoolePolynomial::nUsedVariables().
size_type CDDInterface< CuddLikeZDD >::nVariables | ( | ) | const [inline] |
Returns number of variables in manager.
References CDDInterface< CuddLikeZDD >::manager().
Referenced by CDDInterface< CuddLikeZDD >::blankness(), and CDDInterface< CuddLikeZDD >::usedIndices().
bool_type CDDInterface< CuddLikeZDD >::operator!= | ( | const self & | rhs | ) | const [inline] |
Nonequality check.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
bool_type CDDInterface< CuddLikeZDD >::operator== | ( | const self & | rhs | ) | const [inline] |
Equality check.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
bool_type CDDInterface< CuddLikeZDD >::ownsOne | ( | ) | const [inline] |
Test whether the empty set is included.
References CDDInterface< CuddLikeZDD >::navigation(), and owns_one().
Referenced by BoolePolynomial::hasConstantPart().
bool_type CDDInterface< CuddLikeZDD >::prettyPrint | ( | filename_type | filename | ) | const [inline] |
Print Dot-output to file given by file name.
References CDDInterface< CuddLikeZDD >::prettyPrint().
void CDDInterface< CuddLikeZDD >::prettyPrint | ( | pretty_out_type | filehandle = stdout |
) | const [inline] |
Print Dot-output to file given by file handle.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by CDDInterface< CuddLikeZDD >::prettyPrint(), and BoolePolynomial::prettyPrint().
ostream_type& CDDInterface< CuddLikeZDD >::print | ( | ostream_type & | os | ) | const [inline] |
Get number of nodes in decision diagram.
Enable ostream cout and cerr (at least)
Reimplemented in BooleSet.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
self CDDInterface< CuddLikeZDD >::product | ( | const self & | rhs | ) | const [inline] |
Product.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self& CDDInterface< CuddLikeZDD >::productAssign | ( | const self & | rhs | ) | [inline] |
Product with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
size_type CDDInterface< CuddLikeZDD >::size | ( | ) | const [inline] |
Returns number of terms.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::countIndex(), BooleSet::countIndexDouble(), and CDDInterface< CuddLikeZDD >::length().
double CDDInterface< CuddLikeZDD >::sizeDouble | ( | ) | const [inline] |
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
hash_type CDDInterface< CuddLikeZDD >::stableHash | ( | ) | const [inline] |
Get stable hash value, which is reproducible.
References CDDInterface< CuddLikeZDD >::navigation(), and stable_hash_range().
Referenced by BoolePolynomial::stableHash().
self CDDInterface< CuddLikeZDD >::subSet | ( | const self & | rhs | ) | const [inline] |
self CDDInterface< CuddLikeZDD >::subset0 | ( | idx_type | idx | ) | const [inline] |
Generate subset, where decision diagram manager variable idx is false.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by LiteralFactorization::LiteralFactorization().
self& CDDInterface< CuddLikeZDD >::subset0Assign | ( | idx_type | idx | ) | [inline] |
subset0 with assignment
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self CDDInterface< CuddLikeZDD >::subset1 | ( | idx_type | idx | ) | const [inline] |
Generate subset, where decision diagram manager variable idx is asserted.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by LiteralFactorization::LiteralFactorization(), polybori::groebner::reduce_by_monom(), and polybori::groebner::reduce_complete().
self& CDDInterface< CuddLikeZDD >::subset1Assign | ( | idx_type | idx | ) | [inline] |
subset1 with assignment
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleMonomial::operator/=().
self CDDInterface< CuddLikeZDD >::support | ( | ) | const [inline] |
Get multiples of used variables.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
Referenced by BoolePolynomial::operator%=().
self CDDInterface< CuddLikeZDD >::supSet | ( | const self & | rhs | ) | const [inline] |
self CDDInterface< CuddLikeZDD >::unateProduct | ( | const self & | rhs | ) | const [inline] |
Unate product.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::cartesianProduct(), and polybori::groebner::reduce_complete().
self& CDDInterface< CuddLikeZDD >::unateProductAssign | ( | const self & | rhs | ) | [inline] |
Unate product with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleMonomial::operator*=(), and polybori::groebner::reduce_by_monom().
self CDDInterface< CuddLikeZDD >::unite | ( | const self & | rhs | ) | const [inline] |
Set union.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self& CDDInterface< CuddLikeZDD >::uniteAssign | ( | const self & | rhs | ) | [inline] |
Set union with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
Referenced by BooleSet::addAssign().
int* CDDInterface< CuddLikeZDD >::usedIndices | ( | ) | const [inline] |
Get used variables (assuming indices of length nSupport()).
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().
Referenced by BooleSet::usedVariablesExp().
void CDDInterface< CuddLikeZDD >::usedIndices | ( | VectorLikeType & | indices | ) | const [inline] |
Get used variables (assuming indices of zero length).
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, CDDInterface< CuddLikeZDD >::manager(), and CDDInterface< CuddLikeZDD >::nVariables().
Referenced by BoolePolynomial::usedVariablesExp().
self CDDInterface< CuddLikeZDD >::weakDivide | ( | const self & | rhs | ) | const [inline] |
Weak division.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self& CDDInterface< CuddLikeZDD >::weakDivideAssign | ( | const self & | rhs | ) | [inline] |
Weak division with assignment.
References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.
self CDDInterface< CuddLikeZDD >::Xor | ( | const self & | rhs | ) | const [inline] |