CDDInterface< CuddLikeZDD > Class Template Reference

#include <CDDInterface.h>

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

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::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.
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 CDDInterface< CuddLikeZDD >

For Cudd-like ZDDs, like ZDD or CCuddZDD

Todo:
Generalize it

Member Typedef Documentation

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

Generic access to base type.

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

Type for comparisons.

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

Decision diagram manager core type.

template<class CuddLikeZDD>
typedef CTypes::deg_type CDDInterface< CuddLikeZDD >::deg_type

Define degree type.

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

This type has an easy equality check.

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

Type for file name of pretty print output.

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

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

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

Type for hashed.

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

Define index type.

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

Interfacing Cudd's zero-suppressed decision diagram type.

Reimplemented from CDDInterfaceBase< CuddLikeZDD >.

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

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

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

Cudd's decision diagram manager type.

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

Interface to Cudd's decision diagram manager type.

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

Reference to decision diagram manager type.

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

Iterator type for navigation throught Cudd's ZDDs structure.

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

Type for output streams.

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

Type for output of pretty print.

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

Generic access to type of *this.

Reimplemented from CDDInterfaceBase< CuddLikeZDD >.

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

Define size type.


Constructor & Destructor Documentation

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

Default constructor.

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

Copy constructor.

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

Construct from interfaced type.

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

Construct from Manager and navigator.

template<class CuddLikeZDD>
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>
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>
CDDInterface< CuddLikeZDD >::CDDInterface ( idx_type  idx,
const self thenDD,
const self elseDD 
) [inline]

Construct new node.

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

Destructor.


Member Function Documentation

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

Get corresponding one element.

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

Checks whether the decision diagram has every variable negated.

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

Substitute variable with index idx by its complement.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

Referenced by CDDManagerBase< CCuddInterface, CCuddInterface >::variable().

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

Change with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

References Extra_zddCofactor0().

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

References Extra_zddCofactor1().

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

Division with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set difference.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set difference with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set difference.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set difference with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Division with first term of right-hand side.

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

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

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

Checks whether the decision diagram is empty.

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

Get corresponding zero element.

template<class CuddLikeZDD>
first_iterator CDDInterface< CuddLikeZDD >::firstBegin (  )  const [inline]

Start of first term.

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

Get decison diagram representing the divisors of the first term.

References cudd_generate_divisors().

template<class CuddLikeZDD>
first_iterator CDDInterface< CuddLikeZDD >::firstEnd (  )  const [inline]

Finish of first term.

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

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

Get unique hash value (valid only per runtime).

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set intersection.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set intersection with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

If-Then-Else operation.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

If-Then-Else operation with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Start of first term.

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

Finish of first term.

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

Returns number of terms (deprecated).

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

Returns minimal factors of all minimal terms.

References Extra_zddMinimal().

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

Navigate through ZDD by incrementThen(), incrementElse(), and terminated().

Referenced by CDDInterface< CuddLikeZDD >::stableHash().

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

Get number of nodes in decision diagram.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Returns number of variables in manager.

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

Nonequality check.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Equality check.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Test whether the empty set is included.

References CCuddNavigator::incrementElse(), CCuddNavigator::isConstant(), and CCuddNavigator::terminalValue().

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

Print Dot-output to file given by file name.

References CDDInterface< CuddLikeZDD >::prettyPrint().

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

template<class CuddLikeZDD>
ostream_type& CDDInterface< CuddLikeZDD >::print ( ostream_type os  )  const [inline]

Get number of nodes in decision diagram.

Enable ostream cout and cerr (at least)

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced, and CDDInterface< CuddLikeZDD >::manager().

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

Product with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Returns number of terms.

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

Get stable hash value, which is reproducible.

References CDDInterface< CuddLikeZDD >::navigation(), and polybori::stable_hash_range().

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

References Extra_zddSubSet().

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

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

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

subset0 with assignment

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

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

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

subset1 with assignment

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Get multiples of used variables.

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

References Extra_zddSupSet().

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

Unate product with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

Set union with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

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

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

Get used variables (assuming indices of zero length).

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

Weak division with assignment.

References CDDInterfaceBase< CuddLikeZDD >::m_interfaced.

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

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

Generated on 25 Oct 2009 for PolyBoRi by  doxygen 1.6.1