CCuddDDFacade.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_diagram_CCuddDDFacade_h
#define polybori_diagram_CCuddDDFacade_h
// include basic definitions
#include <polybori/pbori_defs.h>
#include <polybori/cudd/cudd.h>
#include <polybori/cudd/prefix.h>
#include "CApplyNodeFacade.h"
#include "CNodeCounter.h"
#include <polybori/routines/pbori_routines_cuddext.h>
#include <polybori/common/CExtrusivePtr.h>
// Getting iterator type for navigating through Cudd's ZDDs structure
#include <polybori/iterators/CCuddNavigator.h>
// Getting iterator type for retrieving first term from Cudd's ZDDs
#include <polybori/iterators/CCuddFirstIter.h>
// Getting iterator type for retrieving last term from Cudd's ZDDs
#include <polybori/iterators/CCuddLastIter.h>
// Getting output iterator functionality
#include <polybori/iterators/PBoRiOutIter.h>
// Getting error coe functionality
#include <polybori/except/PBoRiGenericError.h>
// test input idx_type
#include <polybori/common/CCheckedIdx.h>
#include <polybori/routines/pbori_algo.h>
#include <polybori/common/tags.h>
#include <polybori/routines/pbori_routines_hash.h>
#include <boost/preprocessor/cat.hpp>
#include <boost/preprocessor/seq/for_each.hpp>
#include <boost/preprocessor/facilities/expand.hpp>
#include <boost/preprocessor/stringize.hpp>
#include <stdexcept>
#include <algorithm>
#include <numeric>
BEGIN_NAMESPACE_PBORI
template <class DataType>
inline void
extrusive_ptr_release(const DataType& data, DdNode* ptr) {
if (ptr != NULL) {
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(data.getManager(), ptr);
}
}
template <class DataType>
inline void
extrusive_ptr_add_ref(const DataType&, DdNode* ptr) {
if (ptr) PBORI_PREFIX(Cudd_Ref)(ptr);
}
#define PBORI_NAME_Product product
#define PBORI_NAME_UnateProduct unateProduct
#define PBORI_NAME_WeakDiv weakDivide
#define PBORI_NAME_Divide divide
#define PBORI_NAME_WeakDivF weakDivF
#define PBORI_NAME_DivideF divideF
#define PBORI_NAME_Union unite
#define PBORI_NAME_Intersect intersect
#define PBORI_NAME_Diff diff
#define PBORI_NAME_Subset1 subset1
#define PBORI_NAME_Subset0 subset0
#define PBORI_NAME_Change change
#define PB_ZDD_APPLY(count, data, funcname) \
diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const { \
return apply(BOOST_PP_CAT(PBORI_PREFIX(Cudd_zdd), funcname), \
rhs); }
template <class RingType, class DiagramType>
class CCuddDDFacade:
public CApplyNodeFacade<DiagramType, DdNode*>,
public CAuxTypes {
typedef CCuddDDFacade self;
public:
typedef CTypes::ostream_type ostream_type;
typedef RingType ring_type;
typedef DiagramType diagram_type;
typedef DdNode node_type;
typedef node_type* node_ptr;
typedef CApplyNodeFacade<diagram_type, node_ptr> base;
typedef CCuddFirstIter first_iterator;
typedef CCuddLastIter last_iterator;
typedef CCuddNavigator navigator;
typedef valid_tag easy_equality_property;
typedef typename ring_type::mgr_type mgr_type;
typedef int cudd_idx_type;
typedef CCheckedIdx checked_idx_type;
CCuddDDFacade(const ring_type& ring, node_ptr node):
p_node(ring, node) {
checkAssumption(node != NULL);
}
CCuddDDFacade(const ring_type& ring, const navigator& navi):
p_node(ring, navi.getNode()) {
checkAssumption(navi.isValid());
}
CCuddDDFacade(const ring_type& ring,
idx_type idx, navigator thenNavi, navigator elseNavi):
p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { }
CCuddDDFacade(const ring_type& ring,
idx_type idx, navigator navi):
p_node(ring, getNewNode(ring, idx, navi, navi)) { }
CCuddDDFacade(idx_type idx, const self& thenDD, const self& elseDD):
p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { }
private: CCuddDDFacade(): p_node() {}
public:
CCuddDDFacade(const self &from): p_node(from.p_node) {}
~CCuddDDFacade() {}
diagram_type& operator=(const diagram_type& rhs) {
p_node = rhs.p_node;
return static_cast<diagram_type&>(*this);
}
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))
bool implies(const self& rhs) const {
return PBORI_PREFIX(Cudd_zddDiffConst)(getManager(), getNode(), rhs.getNode()) ==
PBORI_PREFIX(Cudd_ReadZero)(getManager());
}
std::ostream& printIntern(std::ostream& os) const {
os << getNode() <<": ";
if (isZero())
os << "empty";
else
os << nNodes() << " nodes " << count() << "terms";
return os;
}
void PrintMinterm() const {
checkAssumption(apply(PBORI_PREFIX(Cudd_zddPrintMinterm)) == 1);
}
size_type count() const { return dd_long_count<size_type>(navigation()); }
double countDouble() const { return dd_long_count<double>(navigation()); }
size_type rootIndex() const { return PBORI_PREFIX(Cudd_NodeReadIndex)(getNode()); }
size_type nNodes() const { return CNodeCounter<navigator>()(navigation()); }
size_type refCount() const {
PBORI_ASSERT(getNode() != NULL);
return PBORI_PREFIX(Cudd_Regular)(getNode())->ref;
}
bool isZero() const { return getNode() == PBORI_PREFIX(Cudd_ReadZero)(getManager()); }
bool isOne() const { return getNode() == DD_ONE(getManager()); }
const ring_type& ring() const { return p_node.data(); }
node_ptr getNode() const { return p_node.get(); }
mgr_type* getManager() const { return p_node.data().getManager(); }
protected:
using base::apply;
template <class ResultType>
ResultType memApply(ResultType (*func)(mgr_type *, node_ptr)) const {
ResultType result = apply(func);
checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM);
return result;
}
void checkAssumption(bool isValid) const {
if PBORI_UNLIKELY(!isValid)
throw std::runtime_error(error_text(getManager()));
}
template<class ManagerType, class ReverseIterator, class MultReverseIterator>
diagram_type
cudd_generate_multiples(const ManagerType& mgr,
ReverseIterator start, ReverseIterator finish,
MultReverseIterator multStart,
MultReverseIterator multFinish) const {
// signed case
while ((multStart != multFinish) && (*multStart > CTypes::max_idx))
++multStart;
// unsigned case
while ((multStart != multFinish) && (*multStart < 0))
--multFinish;
DdNode* prev( (getManager())->one );
DdNode* zeroNode( (getManager())->zero );
PBORI_PREFIX(Cudd_Ref)(prev);
while(start != finish) {
while((multStart != multFinish) && (*start < *multStart)) {
DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
prev, prev );
PBORI_PREFIX(Cudd_Ref)(result);
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
prev = result;
++multStart;
};
DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *start,
prev, zeroNode );
PBORI_PREFIX(Cudd_Ref)(result);
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
prev = result;
if((multStart != multFinish) && (*start == *multStart))
++multStart;
++start;
}
while(multStart != multFinish) {
DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
prev, prev );
PBORI_PREFIX(Cudd_Ref)(result);
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
prev = result;
++multStart;
};
PBORI_PREFIX(Cudd_Deref)(prev);
return diagram_type(mgr, prev);
}
template<class ManagerType, class ReverseIterator>
diagram_type
cudd_generate_divisors(const ManagerType& mgr,
ReverseIterator start, ReverseIterator finish) const {
DdNode* prev= (getManager())->one;
PBORI_PREFIX(Cudd_Ref)(prev);
while(start != finish) {
DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(),
*start, prev, prev);
PBORI_PREFIX(Cudd_Ref)(result);
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
prev = result;
++start;
}
PBORI_PREFIX(Cudd_Deref)(prev);
return diagram_type(mgr, prev);
}
public:
diagram_type Xor(const diagram_type& rhs) const {
if (rhs.isZero())
return *this;
// return apply(pboriPBORI_PREFIX(Cudd_zddUnionXor), rhs);
base::checkSameManager(rhs);
return diagram_type(ring(), pboriCudd_zddUnionXor(getManager(), getNode(), rhs.getNode()) );
}
diagram_type divideFirst(const diagram_type& rhs) const {
diagram_type result(*this);
PBoRiOutIter<diagram_type, idx_type, subset1_assign<diagram_type> > outiter(result);
std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
return result;
}
ostream_type& print(ostream_type& os) const {
printIntern(os) << std::endl;;
PrintMinterm();
return os;
}
// size_type nSupport() const { return apply(PBORI_PREFIX(PBORI_PREFIX(Cudd_SupportSize));) }
first_iterator firstBegin() const {
return first_iterator(navigation());
}
first_iterator firstEnd() const {
return first_iterator();
}
last_iterator lastBegin() const {
return last_iterator(getNode());
}
last_iterator lastEnd() const {
return last_iterator();
}
diagram_type firstMultiples(const std::vector<idx_type>& input_multipliers) const {
std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end());
std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
std::copy( firstBegin(), firstEnd(), indices.begin() );
return cudd_generate_multiples( ring(),
indices.rbegin(), indices.rend(),
multipliers.rbegin(),
multipliers.rend() );
}
diagram_type firstDivisors() const {
std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
std::copy( firstBegin(), firstEnd(), indices.begin() );
return cudd_generate_divisors(ring(), indices.rbegin(), indices.rend());
}
navigator navigation() const {
return navigator(getNode());
}
bool_type isConstant() const {
return (getNode()) && PBORI_PREFIX(Cudd_IsConstant)(getNode());
}
private:
static node_ptr
getNewNode(const ring_type& ring, checked_idx_type idx,
navigator thenNavi, navigator elseNavi) {
if ((idx >= *thenNavi) || (idx >= *elseNavi))
throw PBoRiGenericError<CTypes::invalid_ite>();
return PBORI_PREFIX(cuddZddGetNode)(ring.getManager(), idx,
thenNavi.getNode(), elseNavi.getNode());
}
static node_ptr
getNewNode(idx_type idx, const self& thenDD, const self& elseDD) {
thenDD.checkSameManager(elseDD);
return getNewNode(thenDD.ring(),
idx, thenDD.navigation(), elseDD.navigation());
}
private:
CExtrusivePtr<ring_type, node_type> p_node;
};
#undef PB_ZDD_APPLY
END_NAMESPACE_PBORI
#endif
PBORI_PREFIX
#define PBORI_PREFIX(name)
Definition: prefix.h:27
PBoRiOutIter.h
polybori::CCuddDDFacade::isConstant
bool_type isConstant() const
Checks whether the the diagram corresponds to {} or {{}} (polynomial 0 or 1)
Definition: CCuddDDFacade.h:460
polybori::CCuddDDFacade::~CCuddDDFacade
~CCuddDDFacade()
Destructor.
Definition: CCuddDDFacade.h:183
polybori::CCuddDDFacade::node_ptr
node_type * node_ptr
Pointer type for nodes.
Definition: CCuddDDFacade.h:124
END_NAMESPACE_PBORI
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
polybori::CCuddDDFacade::node_type
DdNode node_type
Type for C-style struct.
Definition: CCuddDDFacade.h:121
polybori::CCuddDDFacade::firstEnd
first_iterator firstEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:416
polybori::CCuddDDFacade::cudd_generate_divisors
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)
Definition: CCuddDDFacade.h:350
BEGIN_NAMESPACE_PBORI
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
polybori::CCuddDDFacade::isOne
bool isOne() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:247
Cudd_RecursiveDerefZdd
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
CCuddFirstIter.h
polybori::CCuddDDFacade::PrintMinterm
void PrintMinterm() const
Definition: CCuddDDFacade.h:220
PBoRiGenericError.h
polybori::CCuddDDFacade::firstMultiples
diagram_type firstMultiples(const std::vector< idx_type > &input_multipliers) const
Get decison diagram representing the multiples of the first term.
Definition: CCuddDDFacade.h:431
Cudd_NodeReadIndex
#define Cudd_NodeReadIndex
Definition: prefix_internal.h:91
polybori::CCuddDDFacade::lastBegin
last_iterator lastBegin() const
Start of first term.
Definition: CCuddDDFacade.h:421
polybori::pboriCudd_zddUnionXor
NodeType pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q)
Definition: pbori_algo.h:755
Cudd_zddDiffConst
#define Cudd_zddDiffConst
Definition: prefix_internal.h:175
CCuddLastIter.h
polybori::CCuddDDFacade::ostream_type
CTypes::ostream_type ostream_type
Type for output streams.
Definition: CCuddDDFacade.h:112
cuddUniqueInterZdd
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
polybori::CCuddDDFacade::countDouble
double countDouble() const
Appriximate the number of terms.
Definition: CCuddDDFacade.h:229
cuddZddGetNode
#define cuddZddGetNode
Definition: prefix_internal.h:231
polybori::CCuddDDFacade::navigation
navigator navigation() const
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Definition: CCuddDDFacade.h:455
polybori::CCuddDDFacade::checked_idx_type
CCheckedIdx checked_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:148
polybori::cudd_generate_divisors
DDBase cudd_generate_divisors(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:582
polybori::CApplyNodeFacade
This template class defines a facade as a C++ interface for applying C-style functions to C-style str...
Definition: CApplyNodeFacade.h:41
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator navi)
Definition: CCuddDDFacade.h:168
polybori::CAuxTypes
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
polybori::PBoRiGenericError
This template class is used for polybori's exception handling.
Definition: PBoRiGenericError.h:35
polybori::CAuxTypes::ostream_type
std::ostream ostream_type
Type for out-stream.
Definition: pbori_defs.h:246
polybori::CCuddDDFacade::firstBegin
first_iterator firstBegin() const
Get numbers of used variables.
Definition: CCuddDDFacade.h:411
CApplyNodeFacade.h
prefix.h
polybori::CCuddDDFacade::ring
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
CExtrusivePtr.h
CNodeCounter.h
cudd.h
polybori::extrusive_ptr_add_ref
void extrusive_ptr_add_ref(const DataType &, DdNode *ptr)
Incrememting reference counts to raw pointers to decision diagrams.
Definition: CCuddDDFacade.h:75
polybori::CCuddDDFacade::isZero
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
pbori_defs.h
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(const ring_type &ring, node_ptr node)
Construct diagram from ring and node.
Definition: CCuddDDFacade.h:151
polybori::CCuddDDFacade::diagram_type
DiagramType diagram_type
Type for diagrams.
Definition: CCuddDDFacade.h:118
polybori::CCuddLastIter
This class defines an iterator over the last minimal term of a given ZDD node.
Definition: CCuddLastIter.h:32
polybori::CCuddDDFacade
This template class defines a facade for decision diagrams.
Definition: CCuddDDFacade.h:103
polybori::CCuddDDFacade::easy_equality_property
valid_tag easy_equality_property
This type has an easy equality check.
Definition: CCuddDDFacade.h:139
polybori::CCuddDDFacade::memApply
ResultType memApply(ResultType(*func)(mgr_type *, node_ptr)) const
Definition: CCuddDDFacade.h:265
CCuddNavigator.h
polybori::CCuddDDFacade::getManager
mgr_type * getManager() const
Get raw decision diagram manager.
Definition: CCuddDDFacade.h:256
polybori::CCuddDDFacade::firstDivisors
diagram_type firstDivisors() const
Get decison diagram representing the divisors of the first term.
Definition: CCuddDDFacade.h:445
polybori::CCuddDDFacade::refCount
size_type refCount() const
Number of references pointing here.
Definition: CCuddDDFacade.h:238
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::CCuddDDFacade::lastEnd
last_iterator lastEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:426
polybori::CAuxTypes::idx_type
int idx_type
Type for indices.
Definition: pbori_defs.h:228
polybori::CCuddDDFacade::first_iterator
CCuddFirstIter first_iterator
Iterator type for retrieving first term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:130
polybori::CCuddDDFacade::last_iterator
CCuddLastIter last_iterator
Iterator type for retrieving last term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:133
polybori::CCuddDDFacade::nNodes
size_type nNodes() const
Number of nodes in the current decision diagram.
Definition: CCuddDDFacade.h:235
polybori::CCuddFirstIter
This class defines an iterator over the first minimal term of a given ZDD node.
Definition: CCuddFirstIter.h:35
polybori::CCuddDDFacade::cudd_generate_multiples
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)
Definition: CCuddDDFacade.h:280
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator thenNavi, navigator elseNavi)
Construct new node from manager, index, and navigators.
Definition: CCuddDDFacade.h:162
polybori::CCuddDDFacade::checkAssumption
void checkAssumption(bool isValid) const
Check whether previous decision diagram operation for validity.
Definition: CCuddDDFacade.h:272
polybori::CCuddDDFacade::divideFirst
diagram_type divideFirst(const diagram_type &rhs) const
Division with first term of right-hand side.
Definition: CCuddDDFacade.h:387
Cudd_ReadZero
#define Cudd_ReadZero
Definition: prefix_internal.h:46
polybori::CCuddDDFacade::cudd_idx_type
int cudd_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:145
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(const self &from)
Copy constructor.
Definition: CCuddDDFacade.h:180
CCheckedIdx.h
pbori_routines_cuddext.h
polybori::CCuddDDFacade::mgr_type
ring_type::mgr_type mgr_type
Raw context.
Definition: CCuddDDFacade.h:142
polybori::CCuddDDFacade::operator=
diagram_type & operator=(const diagram_type &rhs)
Assignment operator.
Definition: CCuddDDFacade.h:186
polybori::CCuddDDFacade::count
size_type count() const
Determine the number of terms.
Definition: CCuddDDFacade.h:226
polybori::cudd_generate_multiples
DDBase cudd_generate_multiples(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, MultReverseIterator multStart, MultReverseIterator multFinish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:517
polybori::CCuddDDFacade::base
CApplyNodeFacade< diagram_type, node_ptr > base
Type this is inherited from the following.
Definition: CCuddDDFacade.h:127
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
Cudd_Deref
#define Cudd_Deref
Definition: prefix_internal.h:160
polybori::CCuddDDFacade::printIntern
std::ostream & printIntern(std::ostream &os) const
Definition: CCuddDDFacade.h:209
tags.h
polybori::CAuxTypes::size_type
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(idx_type idx, const self &thenDD, const self &elseDD)
Construct new node.
Definition: CCuddDDFacade.h:173
polybori::CCuddNavigator::isValid
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
pbori_routines_hash.h
polybori::CCuddNavigator
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
polybori::CCuddDDFacade::ring_type
RingType ring_type
Type for diagrams.
Definition: CCuddDDFacade.h:115
polybori::CCuddDDFacade::Xor
diagram_type Xor(const diagram_type &rhs) const
Union Xor.
Definition: CCuddDDFacade.h:377
polybori::CCuddDDFacade::navigator
CCuddNavigator navigator
Iterator type for navigation throught Cudd's ZDDs structure.
Definition: CCuddDDFacade.h:136
polybori::PBoRiOutIter
This template class defines an output iterator which interprets assignments of indices as a change of...
Definition: PBoRiOutIter.h:31
pbori_algo.h
polybori::extrusive_ptr_release
void extrusive_ptr_release(const DataType &data, DdNode *ptr)
Releasing raw pointers to decision diagrams here.
Definition: CCuddDDFacade.h:66
polybori::CAuxTypes::bool_type
bool bool_type
Type for standard true/false statements.
Definition: pbori_defs.h:216
polybori::CCuddDDFacade::CCuddDDFacade
CCuddDDFacade(const ring_type &ring, const navigator &navi)
Construct from Manager and navigator.
Definition: CCuddDDFacade.h:157
PBORI_UNLIKELY
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
polybori::BoolePolyRing::mgr_type
DdManager mgr_type
Definition: BoolePolyRing.h:90
polybori::CCuddDDFacade::rootIndex
size_type rootIndex() const
Get index of curent node.
Definition: CCuddDDFacade.h:232
polybori::CCuddDDFacade::print
ostream_type & print(ostream_type &os) const
Get number of nodes in decision diagram.
Definition: CCuddDDFacade.h:398
polybori::CNodeCounter
This class defines CNodeCounter.
Definition: CNodeCounter.h:30
PB_ZDD_APPLY
#define PB_ZDD_APPLY(count, data, funcname)
Definition: CCuddDDFacade.h:97
error_text
const char * error_text(pbori_DdManager *mgr)
Definition: CCuddInterface.h:45
polybori::valid_tag
This class shows, whether a property of an order is valid.
Definition: tags.h:32
polybori::CCuddDDFacade::getNode
node_ptr getNode() const
Get raw node structure.
Definition: CCuddDDFacade.h:253
polybori::CCheckedIdx
This class defines CCheckedIdx.
Definition: CCheckedIdx.h:29
Cudd_Ref
#define Cudd_Ref
Definition: prefix_internal.h:157