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