PolyBoRi
|
#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::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. | |
![]() | |
typedef CuddLikeZDD | interfaced_type |
The interfaced type. | |
typedef CDDInterfaceBase < interfaced_type > | self |
Generic access to type of *this. |
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 | minimalElements () const |
Returns minimal factors of all minimal terms. | |
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. | |
![]() | |
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 | |
![]() | |
interfaced_type | m_interfaced |
For Cudd-like ZDDs, like ZDD or CCuddZDD
typedef base_type polybori::CDDInterface< CuddLikeZDD >::base |
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 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.
typedef CuddLikeZDD polybori::CDDInterface< CuddLikeZDD >::interfaced_type |
Interfacing Cudd's zero-suppressed decision diagram type.
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.
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.
typedef CTypes::size_type polybori::CDDInterface< CuddLikeZDD >::size_type |
Define size type.
|
inline |
Default constructor.
|
inline |
Copy constructor.
|
inline |
Construct from interfaced type.
|
inline |
Construct from Manager and navigator.
|
inline |
Construct new node from manager, index, and navigators.
|
inline |
Construct new node from manager, index, and common navigator for then and else-branches
|
inline |
Construct new node.
|
inline |
Destructor.
|
inline |
Get corresponding one element.
|
inline |
Checks whether the decision diagram has every variable negated.
|
inline |
Substitute variable with index idx by its complement.
Reimplemented in polybori::BooleSet.
|
inline |
Change with assignment.
Reimplemented in polybori::BooleSet.
Referenced by polybori::BoolePolynomial::BoolePolynomial(), and polybori::BooleMonomial::changeAssign().
|
inline |
References Extra_zddCofactor0().
|
inline |
References Extra_zddCofactor1().
|
inline |
Division.
|
inline |
Division with assignment.
|
inline |
Set difference.
Referenced by polybori::groebner::plug_1_top(), polybori::groebner::red_tail_general(), and polybori::groebner::red_tail_generic().
|
inline |
Set difference with assignment.
Referenced by polybori::BoolePolynomial::operator%=().
|
inline |
Set difference.
|
inline |
Set difference with assignment.
|
inline |
Division with first term of right-hand side.
Referenced by polybori::BooleSet::divide().
|
inline |
Division with first term of right-hand side and assignment.
Referenced by polybori::BooleSet::divideAssign().
|
inline |
Returns dot Product.
References Extra_zddDotProduct().
|
inline |
References Extra_zddDotProduct().
|
inline |
Checks whether the decision diagram is empty.
Referenced by polybori::groebner::GroebnerStrategy::add4ImplDelayed(), polybori::groebner::GroebnerStrategy::addAsYouWish(), polybori::groebner::GroebnerStrategy::addGenerator(), polybori::groebner::addPolynomialToReductor(), polybori::BoolePolynomial::firstDivisors(), polybori::BooleSet::hasTermOfVariables(), polybori::groebner::interpolate(), polybori::groebner::interpolate_smallest_lex(), polybori::groebner::LexHelper::irreducible_lead(), polybori::groebner::LiteralFactorization::LiteralFactorization(), polybori::groebner::minimal_elements_cudd_style_unary(), polybori::groebner::minimal_elements_internal(), polybori::groebner::minimal_elements_internal2(), polybori::groebner::minimal_elements_internal3(), polybori::groebner::mod_var_set(), polybori::BooleSet::owns(), polybori::BooleSet::print(), polybori::groebner::select1(), polybori::groebner::select_no_deg_growth(), and polybori::groebner::zeros().
|
inline |
Get corresponding zero element.
Reimplemented in polybori::BooleSet.
|
inline |
Start of first term.
Referenced by polybori::BoolePolynomial::firstBegin(), and polybori::BooleExponent::multiplyFirst().
|
inline |
Get decison diagram representing the divisors of the first term.
References polybori::cudd_generate_divisors().
Referenced by polybori::BoolePolynomial::firstDivisors(), and polybori::BoolePolynomial::lmDivisors().
|
inline |
Finish of first term.
Referenced by polybori::BoolePolynomial::firstEnd(), and polybori::BooleExponent::multiplyFirst().
|
inline |
Get decison diagram representing the multiples of the first term.
References polybori::cudd_generate_multiples().
|
inline |
Get unique hash value (valid only per runtime)
|
inline |
Set intersection.
|
inline |
Set intersection with assignment.
|
inline |
|
inline |
If-Then-Else operation.
|
inline |
If-Then-Else operation with assignment.
|
inline |
Start of first term.
|
inline |
Finish of first term.
|
inline |
Returns number of terms (deprecated)
Referenced by polybori::groebner::GroebnerStrategy::addGenerator(), polybori::BoolePolynomial::length(), polybori::groebner::LiteralFactorization::LiteralFactorization(), polybori::groebner::minimal_elements_internal(), polybori::groebner::minimal_elements_internal2(), polybori::groebner::GroebnerStrategy::minimalizeAndTailReduce(), polybori::groebner::reduce_complete(), and polybori::groebner::sum_size().
|
inline |
Get reference to actual decision diagram manager.
References polybori::get_manager().
Referenced by polybori::groebner::contained_deg2_cudd_style(), polybori::groebner::contained_variables_cudd_style(), polybori::BoolePolynomial::deg(), polybori::BooleExponent::divisors(), polybori::groebner::do_is_rewriteable(), polybori::groebner::do_plug_1(), polybori::BooleSet::existAbstract(), polybori::BooleSet::firstDivisorsOf(), polybori::BoolePolynomial::gradedPart(), polybori::groebner::include_divisors(), polybori::groebner::interpolate(), polybori::groebner::interpolate_smallest_lex(), polybori::groebner::ll_red_nf_generic(), polybori::groebner::map_every_x_to_x_plus_one(), polybori::groebner::minimal_elements_cudd_style_unary(), polybori::BooleSet::minimalElements(), polybori::groebner::mod_deg2_set(), polybori::groebner::mod_mon_set(), polybori::groebner::mod_var_set(), polybori::BooleExponent::multiples(), polybori::BooleSet::multiplesOf(), polybori::groebner::recursively_insert(), polybori::groebner::variety_lex_leading_terms(), and polybori::groebner::zeros().
|
inline |
Referenced by polybori::BooleSet::begin(), polybori::BoolePolynomial::begin(), polybori::BoolePolynomial::degBegin(), polybori::BooleSet::expBegin(), polybori::BoolePolynomial::genericBegin(), polybori::BoolePolynomial::genericExpBegin(), polybori::BooleSet::print(), and polybori::BoolePolynomial::print().
|
inline |
Returns minimal factors of all minimal terms.
Reimplemented in polybori::BooleSet.
References Extra_zddMinimal().
|
inline |
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Referenced by polybori::groebner::GroebnerStrategy::addGenerator(), polybori::BooleSet::begin(), polybori::groebner::contained_deg2_cudd_style(), polybori::groebner::contained_variables_cudd_style(), polybori::groebner::do_is_rewriteable(), polybori::groebner::do_plug_1(), polybori::BooleSet::existAbstract(), polybori::BooleSet::expBegin(), polybori::BooleSet::firstDivisorsOf(), polybori::BooleSet::hasTermOfVariables(), polybori::groebner::include_divisors(), polybori::groebner::interpolate(), polybori::groebner::interpolate_smallest_lex(), polybori::groebner::ll_red_nf_generic(), polybori::groebner::map_every_x_to_x_plus_one(), polybori::groebner::minimal_elements_cudd_style_unary(), polybori::groebner::minimal_elements_internal(), polybori::groebner::minimal_elements_internal2(), polybori::BooleSet::minimalElements(), polybori::groebner::mod_deg2_set(), polybori::groebner::mod_mon_set(), polybori::groebner::mod_var_set(), polybori::BooleSet::multiplesOf(), polybori::BoolePolynomial::operator*=(), polybori::BoolePolynomial::operator/=(), polybori::BooleSet::owns(), polybori::groebner::recursively_insert(), and polybori::groebner::zeros().
|
inline |
Get number of nodes in decision diagram.
Referenced by polybori::BoolePolynomial::nNodes().
|
inline |
Get numbers of used variables.
Referenced by polybori::BoolePolynomial::nUsedVariables().
|
inline |
Returns number of variables in manager.
Referenced by polybori::BooleEnv::nVariables().
|
inline |
Nonequality check.
|
inline |
Equality check.
|
inline |
Test whether the empty set is included.
References polybori::CCuddNavigator::incrementElse(), polybori::CCuddNavigator::isConstant(), and polybori::CCuddNavigator::terminalValue().
Referenced by polybori::groebner::do_is_rewriteable(), polybori::groebner::minimal_elements_cudd_style_unary(), and polybori::groebner::mod_mon_set().
|
inline |
Print Dot-output to file given by file handle.
Referenced by polybori::BoolePolynomial::prettyPrint().
|
inline |
Print Dot-output to file given by file name.
|
inline |
Get number of nodes in decision diagram.
Enable ostream cout and cerr (at least)
Reimplemented in polybori::BooleSet.
Referenced by polybori::operator<<().
|
inline |
Product.
|
inline |
Product with assignment.
|
inline |
Returns number of terms.
Referenced by polybori::BooleSet::countIndex(), polybori::BooleSet::countIndexDouble(), and polybori::groebner::variety_lex_leading_terms().
|
inline |
|
inline |
Get stable hash value, which is reproducible.
References polybori::stable_hash_range().
|
inline |
References Extra_zddSubSet().
|
inline |
Generate subset, where decision diagram manager variable idx is false.
Reimplemented in polybori::BooleSet.
Referenced by polybori::groebner::nf2(), polybori::groebner::nf2_short(), polybori::groebner::nf_delaying(), polybori::groebner::nf_delaying_exchanging(), and polybori::groebner::translate_indices().
|
inline |
subset0 with assignment
Reimplemented in polybori::BooleSet.
|
inline |
Generate subset, where decision diagram manager variable idx is asserted.
Reimplemented in polybori::BooleSet.
Referenced by polybori::groebner::nf2(), polybori::groebner::nf2_short(), polybori::groebner::nf_delaying(), polybori::groebner::nf_delaying_exchanging(), and polybori::groebner::translate_indices().
|
inline |
subset1 with assignment
Reimplemented in polybori::BooleSet.
Referenced by polybori::BooleMonomial::operator/=().
|
inline |
Get multiples of used variables.
Referenced by polybori::BoolePolynomial::operator%=().
|
inline |
References Extra_zddSupSet().
|
inline |
Unate product.
Referenced by polybori::groebner::minimal_elements_internal(), polybori::groebner::minimal_elements_internal2(), and polybori::groebner::reduce_complete().
|
inline |
Unate product with assignment.
Referenced by polybori::BooleMonomial::operator*=(), and polybori::groebner::reduce_by_monom().
|
inline |
Set union.
|
inline |
Set union with assignment.
|
inline |
Get used variables (assuming indices of zero length)
Referenced by polybori::BoolePolynomial::usedVariablesExp().
|
inline |
Get used variables (assuming indices of length nSupport())
Referenced by polybori::BooleSet::minimalElements(), and polybori::BooleSet::usedVariablesExp().
|
inline |
Weak division.
|
inline |
Weak division with assignment.
|
inline |
References Extra_zddUnionExor(), and polybori::pboriCudd_zddUnionXor().