polybori::CDDInterface< CuddLikeZDD > Class Template Reference

#include <CDDInterface.h>

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

List of all members.

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.

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.
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 subset0 (idx_type idx) const
 Generate subset, where decision diagram manager variable idx is false.
selfsubset0Assign (idx_type idx)
 subset0 with assignment
self subset1 (idx_type idx) const
 Generate subset, where decision diagram manager variable idx is asserted.
selfsubset1Assign (idx_type idx)
 subset1 with assignment
self change (idx_type idx) const
 Substitute variable with index idx by its complement.
selfchangeAssign (idx_type idx)
 Change 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.
ostream_typeprint (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.

Detailed Description

template<class CuddLikeZDD>
class polybori::CDDInterface< CuddLikeZDD >

For Cudd-like ZDDs, like ZDD or CCuddZDD

Todo:
Generalize it

Member Typedef Documentation

template<class CuddLikeZDD >
typedef base_type polybori::CDDInterface< CuddLikeZDD >::base

Reimplemented in polybori::BooleSet.

template<class CuddLikeZDD >
typedef CDDInterfaceBase<interfaced_type> polybori::CDDInterface< CuddLikeZDD >::base_type

Generic access to base type.

template<class CuddLikeZDD >
typedef CTypes::bool_type polybori::CDDInterface< CuddLikeZDD >::bool_type

Type for comparisons.

template<class CuddLikeZDD >
typedef manager_traits<manager_base>::core_type polybori::CDDInterface< CuddLikeZDD >::core_type

Decision diagram manager core type.

template<class CuddLikeZDD >
typedef valid_tag polybori::CDDInterface< CuddLikeZDD >::easy_equality_property

This type has an easy equality check.

template<class CuddLikeZDD >
typedef const char* polybori::CDDInterface< CuddLikeZDD >::filename_type

Type for file name of pretty print output.

template<class CuddLikeZDD >
typedef CCuddFirstIter polybori::CDDInterface< CuddLikeZDD >::first_iterator

Iterator type for retrieving first term from Cudd's ZDDs.

template<class CuddLikeZDD >
typedef CTypes::hash_type polybori::CDDInterface< CuddLikeZDD >::hash_type

Type for hashed.

template<class CuddLikeZDD >
typedef CTypes::idx_type polybori::CDDInterface< CuddLikeZDD >::idx_type

Define index type.

Reimplemented in polybori::BooleSet.

template<class CuddLikeZDD >
typedef CuddLikeZDD polybori::CDDInterface< CuddLikeZDD >::interfaced_type

Interfacing Cudd's zero-suppressed decision diagram type.

Reimplemented from polybori::CDDInterfaceBase< CuddLikeZDD >.

template<class CuddLikeZDD >
typedef CCuddLastIter polybori::CDDInterface< CuddLikeZDD >::last_iterator

Iterator type for retrieving last term from Cudd's ZDDs.

template<class CuddLikeZDD >
typedef zdd_traits<interfaced_type>::manager_base polybori::CDDInterface< CuddLikeZDD >::manager_base

Cudd's decision diagram manager type.

template<class CuddLikeZDD >
typedef CDDManager<CCuddInterface> polybori::CDDInterface< CuddLikeZDD >::manager_type

Interface to Cudd's decision diagram manager type.

template<class CuddLikeZDD >
typedef manager_traits<manager_base>::tmp_ref polybori::CDDInterface< CuddLikeZDD >::mgr_ref

Reference to decision diagram manager type.

template<class CuddLikeZDD >
typedef CCuddNavigator polybori::CDDInterface< CuddLikeZDD >::navigator

Iterator type for navigation throught Cudd's ZDDs structure.

Reimplemented in polybori::BooleSet.

template<class CuddLikeZDD >
typedef CTypes::ostream_type polybori::CDDInterface< CuddLikeZDD >::ostream_type

Type for output streams.

template<class CuddLikeZDD >
typedef FILE* polybori::CDDInterface< CuddLikeZDD >::pretty_out_type

Type for output of pretty print.

template<class CuddLikeZDD >
typedef CDDInterface<interfaced_type> polybori::CDDInterface< CuddLikeZDD >::self

Generic access to type of *this.

Reimplemented from polybori::CDDInterfaceBase< CuddLikeZDD >.

Reimplemented in polybori::BooleSet.

template<class CuddLikeZDD >
typedef CTypes::size_type polybori::CDDInterface< CuddLikeZDD >::size_type

Define size type.

Reimplemented in polybori::BooleSet.


Constructor & Destructor Documentation

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface (  )  [inline]

Default constructor.

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface ( const self rhs  )  [inline]

Copy constructor.

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface ( const interfaced_type rhs  )  [inline]

Construct from interfaced type.

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface ( const manager_base mgr,
const navigator navi 
) [inline]

Construct from Manager and navigator.

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface ( const manager_base mgr,
idx_type  idx,
navigator  thenNavi,
navigator  elseNavi 
) [inline]

Construct new node from manager, index, and navigators.

template<class CuddLikeZDD >
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

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::CDDInterface ( idx_type  idx,
const self thenDD,
const self elseDD 
) [inline]

Construct new node.

template<class CuddLikeZDD >
polybori::CDDInterface< CuddLikeZDD >::~CDDInterface (  )  [inline]

Destructor.


Member Function Documentation

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::blankElement (  )  const [inline]

Get corresponding one element.

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::blankness (  )  const [inline]

Checks whether the decision diagram has every variable negated.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::change ( idx_type  idx  )  const [inline]

Substitute variable with index idx by its complement.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::changeAssign ( idx_type  idx  )  [inline]
template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::cofactor0 ( const self rhs  )  const [inline]

References Extra_zddCofactor0().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::cofactor1 ( const self rhs,
idx_type  includeVars 
) const [inline]

References Extra_zddCofactor1().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::ddDivide ( const self rhs  )  const [inline]

Division.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::ddDivideAssign ( const self rhs  )  [inline]

Division with assignment.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::diff ( const self rhs  )  const [inline]

Set difference.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::diffAssign ( const self rhs  )  [inline]

Set difference with assignment.

Referenced by polybori::BoolePolynomial::operator%=().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::diffConst ( const self rhs  )  const [inline]

Set difference.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::diffConstAssign ( const self rhs  )  [inline]

Set difference with assignment.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::divideFirst ( const self rhs  )  const [inline]

Division with first term of right-hand side.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::divideFirstAssign ( const self rhs  )  [inline]

Division with first term of right-hand side and assignment.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::dotProduct ( const self rhs  )  const [inline]

Returns dot Product.

References Extra_zddDotProduct().

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::dotProductAssign ( const self rhs  )  [inline]

References Extra_zddDotProduct().

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::emptiness (  )  const [inline]
template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::emptyElement (  )  const [inline]

Get corresponding zero element.

Reimplemented in polybori::BooleSet.

template<class CuddLikeZDD >
first_iterator polybori::CDDInterface< CuddLikeZDD >::firstBegin (  )  const [inline]
template<class CuddLikeZDD >
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::lmDivisors().

template<class CuddLikeZDD >
first_iterator polybori::CDDInterface< CuddLikeZDD >::firstEnd (  )  const [inline]
template<class CuddLikeZDD >
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().

template<class CuddLikeZDD >
hash_type polybori::CDDInterface< CuddLikeZDD >::hash (  )  const [inline]

Get unique hash value (valid only per runtime).

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::intersect ( const self rhs  )  const [inline]

Set intersection.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::intersectAssign ( const self rhs  )  [inline]

Set intersection with assignment.

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::isConstant (  )  const [inline]
template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::ite ( const self then_dd,
const self else_dd 
) const [inline]

If-Then-Else operation.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::iteAssign ( const self then_dd,
const self else_dd 
) [inline]

If-Then-Else operation with assignment.

template<class CuddLikeZDD >
last_iterator polybori::CDDInterface< CuddLikeZDD >::lastBegin (  )  const [inline]

Start of first term.

template<class CuddLikeZDD >
last_iterator polybori::CDDInterface< CuddLikeZDD >::lastEnd (  )  const [inline]

Finish of first term.

template<class CuddLikeZDD >
size_type polybori::CDDInterface< CuddLikeZDD >::length (  )  const [inline]
template<class CuddLikeZDD >
mgr_ref polybori::CDDInterface< CuddLikeZDD >::manager (  )  const [inline]
template<class CuddLikeZDD >
core_type polybori::CDDInterface< CuddLikeZDD >::managerCore (  )  const [inline]
template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::minimalElements (  )  const [inline]

Returns minimal factors of all minimal terms.

Reimplemented in polybori::BooleSet.

References Extra_zddMinimal().

template<class CuddLikeZDD >
navigator polybori::CDDInterface< CuddLikeZDD >::navigation (  )  const [inline]
template<class CuddLikeZDD >
size_type polybori::CDDInterface< CuddLikeZDD >::nNodes (  )  const [inline]

Get number of nodes in decision diagram.

Referenced by polybori::BoolePolynomial::nNodes().

template<class CuddLikeZDD >
size_type polybori::CDDInterface< CuddLikeZDD >::nSupport (  )  const [inline]

Get numbers of used variables.

Referenced by polybori::BoolePolynomial::nUsedVariables().

template<class CuddLikeZDD >
size_type polybori::CDDInterface< CuddLikeZDD >::nVariables (  )  const [inline]

Returns number of variables in manager.

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::operator!= ( const self rhs  )  const [inline]

Nonequality check.

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::operator== ( const self rhs  )  const [inline]

Equality check.

template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::ownsOne (  )  const [inline]
template<class CuddLikeZDD >
bool_type polybori::CDDInterface< CuddLikeZDD >::prettyPrint ( filename_type  filename  )  const [inline]

Print Dot-output to file given by file name.

template<class CuddLikeZDD >
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().

template<class CuddLikeZDD >
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.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::product ( const self rhs  )  const [inline]

Product.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::productAssign ( const self rhs  )  [inline]

Product with assignment.

template<class CuddLikeZDD >
size_type polybori::CDDInterface< CuddLikeZDD >::size (  )  const [inline]

Returns number of terms.

template<class CuddLikeZDD >
double polybori::CDDInterface< CuddLikeZDD >::sizeDouble (  )  const [inline]
template<class CuddLikeZDD >
hash_type polybori::CDDInterface< CuddLikeZDD >::stableHash (  )  const [inline]

Get stable hash value, which is reproducible.

References polybori::stable_hash_range().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::subSet ( const self rhs  )  const [inline]

References Extra_zddSubSet().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::subset0 ( idx_type  idx  )  const [inline]

Generate subset, where decision diagram manager variable idx is false.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::subset0Assign ( idx_type  idx  )  [inline]

subset0 with assignment

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::subset1 ( idx_type  idx  )  const [inline]

Generate subset, where decision diagram manager variable idx is asserted.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::subset1Assign ( idx_type  idx  )  [inline]

subset1 with assignment

Referenced by polybori::BooleMonomial::operator/=().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::support (  )  const [inline]

Get multiples of used variables.

Referenced by polybori::BoolePolynomial::operator%=().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::supSet ( const self rhs  )  const [inline]

References Extra_zddSupSet().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::unateProduct ( const self rhs  )  const [inline]

Unate product.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::unateProductAssign ( const self rhs  )  [inline]

Unate product with assignment.

Referenced by polybori::BooleMonomial::operator*=().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::unite ( const self rhs  )  const [inline]

Set union.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::uniteAssign ( const self rhs  )  [inline]

Set union with assignment.

template<class CuddLikeZDD >
int* polybori::CDDInterface< CuddLikeZDD >::usedIndices (  )  const [inline]

Get used variables (assuming indices of length nSupport()).

template<class CuddLikeZDD >
template<class VectorLikeType >
void polybori::CDDInterface< CuddLikeZDD >::usedIndices ( VectorLikeType &  indices  )  const [inline]

Get used variables (assuming indices of zero length).

Referenced by polybori::BoolePolynomial::usedVariablesExp().

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::weakDivide ( const self rhs  )  const [inline]

Weak division.

template<class CuddLikeZDD >
self& polybori::CDDInterface< CuddLikeZDD >::weakDivideAssign ( const self rhs  )  [inline]

Weak division with assignment.

template<class CuddLikeZDD >
self polybori::CDDInterface< CuddLikeZDD >::Xor ( const self rhs  )  const [inline]

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

Generated by  doxygen 1.6.2