PolyBoRi
Public Types | Public Member Functions | Protected Member Functions | List of all members
polybori::CCuddDDFacade< RingType, DiagramType > Class Template Reference

This template class defines a facade for decision diagrams. More...

#include <CCuddDDFacade.h>

Inheritance diagram for polybori::CCuddDDFacade< RingType, DiagramType >:
polybori::CApplyNodeFacade< DiagramType, DdNode * > polybori::CAuxTypes

Public Types

typedef CTypes::ostream_type ostream_type
 Type for output streams. More...
 
typedef RingType ring_type
 Type for diagrams. More...
 
typedef DiagramType diagram_type
 Type for diagrams. More...
 
typedef DdNode node_type
 Type for C-style struct. More...
 
typedef node_typenode_ptr
 Pointer type for nodes. More...
 
typedef CApplyNodeFacade
< diagram_type, node_ptr
base
 Type this is inherited from the following. More...
 
typedef CCuddFirstIter first_iterator
 Iterator type for retrieving first term from Cudd's ZDDs. More...
 
typedef CCuddLastIter last_iterator
 Iterator type for retrieving last term from Cudd's ZDDs. More...
 
typedef CCuddNavigator navigator
 Iterator type for navigation throught Cudd's ZDDs structure. More...
 
typedef valid_tag easy_equality_property
 This type has an easy equality check. More...
 
typedef ring_type::mgr_type mgr_type
 Raw context. More...
 
typedef int cudd_idx_type
 Cudd's index type. More...
 
typedef CCheckedIdx checked_idx_type
 Cudd's index type. More...
 
- Public Types inherited from polybori::CApplyNodeFacade< DiagramType, DdNode * >
typedef DiagramType diagram_type
 
typedef DdNode * node_ptr
 
- Public Types inherited from polybori::CAuxTypes
typedef bool bool_type
 Type for standard true/false statements. More...
 
typedef std::size_t size_type
 Type for lengths, dimensions, etc. More...
 
typedef int deg_type
 Type for polynomial degrees (ranges from -1 to maxint) More...
 
typedef int integer_type
 Type for integer numbers. More...
 
typedef int idx_type
 Type for indices. More...
 
typedef std::size_t hash_type
 Type for hashing. More...
 
typedef unsigned int errornum_type
 Type used to store error codes. More...
 
typedef short int comp_type
 Type for comparisons. More...
 
typedef int ordercode_type
 Type for ordering codes. More...
 
typedef const char * errortext_type
 Type used to verbose error information. More...
 
typedef std::ostream ostream_type
 Type for out-stream. More...
 
typedef const char * vartext_type
 Type for setting/getting names of variables. More...
 
typedef unsigned long large_size_type
 large size_type (necessary?) More...
 
typedef std::size_t refcount_type
 Type for counting references. More...
 

Public Member Functions

 CCuddDDFacade (const ring_type &ring, node_ptr node)
 Construct diagram from ring and node. More...
 
 CCuddDDFacade (const ring_type &ring, const navigator &navi)
 Construct from Manager and navigator. More...
 
 CCuddDDFacade (const ring_type &ring, idx_type idx, navigator thenNavi, navigator elseNavi)
 Construct new node from manager, index, and navigators. More...
 
 CCuddDDFacade (const ring_type &ring, idx_type idx, navigator navi)
 
 CCuddDDFacade (idx_type idx, const self &thenDD, const self &elseDD)
 Construct new node. More...
 
 CCuddDDFacade (const self &from)
 Copy constructor. More...
 
 ~CCuddDDFacade ()
 Destructor. More...
 
diagram_typeoperator= (const diagram_type &rhs)
 Assignment operator. More...
 
*bool implies (const self &rhs) const
 Performs the inclusion test for ZDDs. More...
 
size_type count () const
 Determine the number of terms. More...
 
double countDouble () const
 Appriximate the number of terms. More...
 
size_type rootIndex () const
 Get index of curent node. More...
 
size_type nNodes () const
 Number of nodes in the current decision diagram. More...
 
size_type refCount () const
 Number of references pointing here. More...
 
bool isZero () const
 Test whether diagram represents the empty set. More...
 
bool isOne () const
 Test whether diagram represents the empty set. More...
 
const ring_typering () const
 Get reference to ring. More...
 
node_ptr getNode () const
 Get raw node structure. More...
 
mgr_typegetManager () const
 Get raw decision diagram manager. More...
 
diagram_type Xor (const diagram_type &rhs) const
 Union Xor. More...
 
diagram_type divideFirst (const diagram_type &rhs) const
 Division with first term of right-hand side. More...
 
ostream_typeprint (ostream_type &os) const
 Get number of nodes in decision diagram. More...
 
first_iterator firstBegin () const
 Get numbers of used variables. More...
 
first_iterator firstEnd () const
 Finish of first term. More...
 
last_iterator lastBegin () const
 Start of first term. More...
 
last_iterator lastEnd () const
 Finish of first term. More...
 
diagram_type firstMultiples (const std::vector< idx_type > &input_multipliers) const
 Get decison diagram representing the multiples of the first term. More...
 
diagram_type firstDivisors () const
 Get decison diagram representing the divisors of the first term. More...
 
navigator navigation () const
 Navigate through ZDD by incrementThen(), incrementElse(), and terminated() More...
 
bool_type isConstant () const
 Checks whether the the diagram corresponds to {} or {{}} (polynomial 0 or 1) More...
 
Functions for print useful information
std::ostream & printIntern (std::ostream &os) const
 
void PrintMinterm () const
 
- Public Member Functions inherited from polybori::CApplyNodeFacade< DiagramType, DdNode * >
bool operator== (const diagram_type &rhs) const
 Equality. More...
 
bool operator!= (const diagram_type &rhs) const
 Nonequality. More...
 

Protected Member Functions

template<class ResultType >
ResultType memApply (ResultType(*func)(mgr_type *, node_ptr)) const
 
void checkAssumption (bool isValid) const
 Check whether previous decision diagram operation for validity. More...
 
template<class ManagerType , class ReverseIterator , class MultReverseIterator >
diagram_type cudd_generate_multiples (const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, MultReverseIterator multStart, MultReverseIterator multFinish) const
 temporarily (needs to be more generic) (similar fct in pbori_algo.h) More...
 
template<class ManagerType , class ReverseIterator >
diagram_type cudd_generate_divisors (const ManagerType &mgr, ReverseIterator start, ReverseIterator finish) const
 temporarily (needs to be more generic) (similar fct in pbori_algo.h) More...
 
- Protected Member Functions inherited from polybori::CApplyNodeFacade< DiagramType, DdNode * >
void checkSameManager (const diagram_type &other) const
 Test, whether both operands. More...
 
diagram_type diagram (node_ptr node) const
 Get diagram of the same context. More...
 
diagram_type apply (node_ptr(*func)(MgrType, node_ptr)) const
 Unary function. More...
 
diagram_type apply (node_ptr(*func)(MgrType, node_ptr, node_ptr), const diagram_type &rhs) const
 Binary function (two diagrams) More...
 
diagram_type apply (node_ptr(*func)(MgrType, node_ptr, node_ptr, node_ptr), const diagram_type &first, const diagram_type &second) const
 Ternary function (three diagrams) More...
 
diagram_type apply (node_ptr(*func)(MgrType, node_ptr, Type), Type value) const
 Binary functions with non-diagram right-hand side. More...
 
ResultType apply (ResultType(*func)(MgrType, node_ptr)) const
 Unary functions with non-diagram result value. More...
 

Detailed Description

template<class RingType, class DiagramType>
class polybori::CCuddDDFacade< RingType, DiagramType >

This template class defines a facade for decision diagrams.

Member Typedef Documentation

template<class RingType, class DiagramType>
typedef CApplyNodeFacade<diagram_type, node_ptr> polybori::CCuddDDFacade< RingType, DiagramType >::base

Type this is inherited from the following.

template<class RingType, class DiagramType>
typedef CCheckedIdx polybori::CCuddDDFacade< RingType, DiagramType >::checked_idx_type

Cudd's index type.

template<class RingType, class DiagramType>
typedef int polybori::CCuddDDFacade< RingType, DiagramType >::cudd_idx_type

Cudd's index type.

template<class RingType, class DiagramType>
typedef DiagramType polybori::CCuddDDFacade< RingType, DiagramType >::diagram_type

Type for diagrams.

template<class RingType, class DiagramType>
typedef valid_tag polybori::CCuddDDFacade< RingType, DiagramType >::easy_equality_property

This type has an easy equality check.

template<class RingType, class DiagramType>
typedef CCuddFirstIter polybori::CCuddDDFacade< RingType, DiagramType >::first_iterator

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

template<class RingType, class DiagramType>
typedef CCuddLastIter polybori::CCuddDDFacade< RingType, DiagramType >::last_iterator

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

template<class RingType, class DiagramType>
typedef ring_type::mgr_type polybori::CCuddDDFacade< RingType, DiagramType >::mgr_type

Raw context.

template<class RingType, class DiagramType>
typedef CCuddNavigator polybori::CCuddDDFacade< RingType, DiagramType >::navigator

Iterator type for navigation throught Cudd's ZDDs structure.

template<class RingType, class DiagramType>
typedef node_type* polybori::CCuddDDFacade< RingType, DiagramType >::node_ptr

Pointer type for nodes.

template<class RingType, class DiagramType>
typedef DdNode polybori::CCuddDDFacade< RingType, DiagramType >::node_type

Type for C-style struct.

template<class RingType, class DiagramType>
typedef CTypes::ostream_type polybori::CCuddDDFacade< RingType, DiagramType >::ostream_type

Type for output streams.

template<class RingType, class DiagramType>
typedef RingType polybori::CCuddDDFacade< RingType, DiagramType >::ring_type

Type for diagrams.

Constructor & Destructor Documentation

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( const ring_type ring,
node_ptr  node 
)
inline

Construct diagram from ring and node.

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( const ring_type ring,
const navigator navi 
)
inline

Construct from Manager and navigator.

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( const ring_type ring,
idx_type  idx,
navigator  thenNavi,
navigator  elseNavi 
)
inline

Construct new node from manager, index, and navigators.

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( const ring_type ring,
idx_type  idx,
navigator  navi 
)
inline

Construct new node from manager, index, and common navigator for then and else-branches

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( idx_type  idx,
const self thenDD,
const self elseDD 
)
inline

Construct new node.

template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::CCuddDDFacade ( const self from)
inline

Copy constructor.

Todo:
NULL?
template<class RingType, class DiagramType>
polybori::CCuddDDFacade< RingType, DiagramType >::~CCuddDDFacade ( )
inline

Destructor.

Member Function Documentation

template<class RingType, class DiagramType>
void polybori::CCuddDDFacade< RingType, DiagramType >::checkAssumption ( bool  isValid) const
inlineprotected

Check whether previous decision diagram operation for validity.

template<class RingType, class DiagramType>
size_type polybori::CCuddDDFacade< RingType, DiagramType >::count ( ) const
inline

Determine the number of terms.

template<class RingType, class DiagramType>
double polybori::CCuddDDFacade< RingType, DiagramType >::countDouble ( ) const
inline

Appriximate the number of terms.

template<class RingType, class DiagramType>
template<class ManagerType , class ReverseIterator >
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::cudd_generate_divisors ( const ManagerType &  mgr,
ReverseIterator  start,
ReverseIterator  finish 
) const
inlineprotected

temporarily (needs to be more generic) (similar fct in pbori_algo.h)

Todo:
Next line needs generalization
template<class RingType, class DiagramType>
template<class ManagerType , class ReverseIterator , class MultReverseIterator >
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::cudd_generate_multiples ( const ManagerType &  mgr,
ReverseIterator  start,
ReverseIterator  finish,
MultReverseIterator  multStart,
MultReverseIterator  multFinish 
) const
inlineprotected

temporarily (needs to be more generic) (similar fct in pbori_algo.h)

template<class RingType, class DiagramType>
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::divideFirst ( const diagram_type rhs) const
inline

Division with first term of right-hand side.

template<class RingType, class DiagramType>
first_iterator polybori::CCuddDDFacade< RingType, DiagramType >::firstBegin ( ) const
inline
template<class RingType, class DiagramType>
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::firstDivisors ( ) const
inline

Get decison diagram representing the divisors of the first term.

Referenced by polybori::BoolePolynomial::firstDivisors(), and polybori::BoolePolynomial::leadDivisors().

template<class RingType, class DiagramType>
first_iterator polybori::CCuddDDFacade< RingType, DiagramType >::firstEnd ( ) const
inline
template<class RingType, class DiagramType>
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::firstMultiples ( const std::vector< idx_type > &  input_multipliers) const
inline

Get decison diagram representing the multiples of the first term.

template<class RingType, class DiagramType>
mgr_type* polybori::CCuddDDFacade< RingType, DiagramType >::getManager ( ) const
inline

Get raw decision diagram manager.

Referenced by polybori::CApplyNodeFacade< BooleSet, DdNode * >::checkSameManager().

template<class RingType, class DiagramType>
node_ptr polybori::CCuddDDFacade< RingType, DiagramType >::getNode ( ) const
inline
template<class RingType, class DiagramType>
* bool polybori::CCuddDDFacade< RingType, DiagramType >::implies ( const self rhs) const
inline

Performs the inclusion test for ZDDs.

Note
Preprocessor generated members
BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const diagram_type&,
(Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
(Union)(Intersect)(Diff))
BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
template<class RingType, class DiagramType>
bool_type polybori::CCuddDDFacade< RingType, DiagramType >::isConstant ( ) const
inline

Checks whether the the diagram corresponds to {} or {{}} (polynomial 0 or 1)

template<class RingType, class DiagramType>
bool polybori::CCuddDDFacade< RingType, DiagramType >::isOne ( ) const
inline

Test whether diagram represents the empty set.

template<class RingType, class DiagramType>
bool polybori::CCuddDDFacade< RingType, DiagramType >::isZero ( ) const
inline
template<class RingType, class DiagramType>
last_iterator polybori::CCuddDDFacade< RingType, DiagramType >::lastBegin ( ) const
inline

Start of first term.

template<class RingType, class DiagramType>
last_iterator polybori::CCuddDDFacade< RingType, DiagramType >::lastEnd ( ) const
inline

Finish of first term.

template<class RingType, class DiagramType>
template<class ResultType >
ResultType polybori::CCuddDDFacade< RingType, DiagramType >::memApply ( ResultType(*)(mgr_type *, node_ptr func) const
inlineprotected
template<class RingType, class DiagramType>
navigator polybori::CCuddDDFacade< RingType, DiagramType >::navigation ( ) const
inline
template<class RingType, class DiagramType>
size_type polybori::CCuddDDFacade< RingType, DiagramType >::nNodes ( ) const
inline

Number of nodes in the current decision diagram.

Referenced by polybori::BoolePolynomial::nNodes(), and polybori::groebner::CountCriterion::operator()().

template<class RingType, class DiagramType>
diagram_type& polybori::CCuddDDFacade< RingType, DiagramType >::operator= ( const diagram_type rhs)
inline

Assignment operator.

template<class RingType, class DiagramType>
ostream_type& polybori::CCuddDDFacade< RingType, DiagramType >::print ( ostream_type os) const
inline

Get number of nodes in decision diagram.

template<class RingType, class DiagramType>
std::ostream& polybori::CCuddDDFacade< RingType, DiagramType >::printIntern ( std::ostream &  os) const
inline
template<class RingType, class DiagramType>
void polybori::CCuddDDFacade< RingType, DiagramType >::PrintMinterm ( ) const
inline
template<class RingType, class DiagramType>
size_type polybori::CCuddDDFacade< RingType, DiagramType >::refCount ( ) const
inline

Number of references pointing here.

template<class RingType, class DiagramType>
const ring_type& polybori::CCuddDDFacade< RingType, DiagramType >::ring ( ) const
inline
template<class RingType, class DiagramType>
size_type polybori::CCuddDDFacade< RingType, DiagramType >::rootIndex ( ) const
inline

Get index of curent node.

template<class RingType, class DiagramType>
diagram_type polybori::CCuddDDFacade< RingType, DiagramType >::Xor ( const diagram_type rhs) const
inline

Union Xor.

Referenced by polybori::groebner::zeros().


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