16 #ifndef polybori_diagram_CCuddDDFacade_h
17 #define polybori_diagram_CCuddDDFacade_h
52 #include <boost/preprocessor/cat.hpp>
53 #include <boost/preprocessor/seq/for_each.hpp>
54 #include <boost/preprocessor/facilities/expand.hpp>
55 #include <boost/preprocessor/stringize.hpp>
64 template <
class DataType>
73 template <
class DataType>
84 #define PBORI_NAME_Product product
85 #define PBORI_NAME_UnateProduct unateProduct
86 #define PBORI_NAME_WeakDiv weakDivide
87 #define PBORI_NAME_Divide divide
88 #define PBORI_NAME_WeakDivF weakDivF
89 #define PBORI_NAME_DivideF divideF
90 #define PBORI_NAME_Union unite
91 #define PBORI_NAME_Intersect intersect
92 #define PBORI_NAME_Diff diff
93 #define PBORI_NAME_Subset1 subset1
94 #define PBORI_NAME_Subset0 subset0
95 #define PBORI_NAME_Change change
97 #define PB_ZDD_APPLY(count, data, funcname) \
98 diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const { \
99 return apply(BOOST_PP_CAT(PBORI_PREFIX(Cudd_zdd), funcname), \
102 template <
class RingType,
class DiagramType>
153 checkAssumption(node != NULL);
158 p_node(ring, navi.getNode()) {
159 checkAssumption(navi.
isValid());
163 idx_type idx, navigator thenNavi, navigator elseNavi):
164 p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { }
170 p_node(ring, getNewNode(ring, idx, navi, navi)) { }
174 p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { }
177 private: CCuddDDFacade(): p_node() {}
188 return static_cast<diagram_type&
>(*this);
193 BOOST_PP_SEQ_FOR_EACH(
PB_ZDD_APPLY,
const diagram_type&,
194 (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
195 (Union)(Intersect)(Diff))
197 BOOST_PP_SEQ_FOR_EACH(
PB_ZDD_APPLY,
int, (Subset1)(Subset0)(Change))
200 bool implies(const self& rhs)
const {
210 os << getNode() <<
": ";
215 os << nNodes() <<
" nodes " << count() <<
"terms";
221 checkAssumption(apply(
PBORI_PREFIX(Cudd_zddPrintMinterm)) == 1);
229 double countDouble()
const {
return dd_long_count<double>(navigation()); }
247 bool isOne()
const {
return getNode() == DD_ONE(getManager()); }
250 const ring_type&
ring()
const {
return p_node.data(); }
253 node_ptr
getNode()
const {
return p_node.get(); }
256 mgr_type*
getManager()
const {
return p_node.data().getManager(); }
264 template <
class ResultType>
265 ResultType
memApply(ResultType (*func)(mgr_type *, node_ptr))
const {
266 ResultType result = apply(func);
267 checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM);
274 throw std::runtime_error(
error_text(getManager()));
278 template<
class ManagerType,
class ReverseIterator,
class MultReverseIterator>
281 ReverseIterator start, ReverseIterator finish,
282 MultReverseIterator multStart,
283 MultReverseIterator multFinish)
const {
286 while ((multStart != multFinish) && (*multStart > CTypes::max_idx))
289 while ((multStart != multFinish) && (*multStart < 0))
292 DdNode* prev( (getManager())->one );
294 DdNode* zeroNode( (getManager())->zero );
297 while(start != finish) {
299 while((multStart != multFinish) && (*start < *multStart)) {
321 if((multStart != multFinish) && (*start == *multStart))
328 while(multStart != multFinish) {
344 return diagram_type(mgr, prev);
348 template<
class ManagerType,
class ReverseIterator>
351 ReverseIterator start, ReverseIterator finish)
const {
354 DdNode* prev= (getManager())->one;
357 while(start != finish) {
371 return diagram_type(mgr, prev);
377 diagram_type
Xor(
const diagram_type& rhs)
const {
382 base::checkSameManager(rhs);
389 diagram_type result(*
this);
398 ostream_type&
print(ostream_type& os)
const {
400 printIntern(os) << std::endl;;
412 return first_iterator(navigation());
417 return first_iterator();
422 return last_iterator(getNode());
427 return last_iterator();
431 diagram_type
firstMultiples(
const std::vector<idx_type>& input_multipliers)
const {
433 std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end());
434 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
436 std::copy( firstBegin(), firstEnd(), indices.begin() );
439 indices.rbegin(), indices.rend(),
440 multipliers.rbegin(),
441 multipliers.rend() );
447 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
449 std::copy( firstBegin(), firstEnd(), indices.begin() );
456 return navigator(getNode());
461 return (getNode()) &&
PBORI_PREFIX(Cudd_IsConstant)(getNode());
470 getNewNode(
const ring_type& ring, checked_idx_type idx,
471 navigator thenNavi, navigator elseNavi) {
473 if ((idx >= *thenNavi) || (idx >= *elseNavi))
477 thenNavi.getNode(), elseNavi.getNode());
482 getNewNode(
idx_type idx,
const self& thenDD,
const self& elseDD) {
483 thenDD.checkSameManager(elseDD);
484 return getNewNode(thenDD.ring(),
485 idx, thenDD.navigation(), elseDD.navigation());
490 CExtrusivePtr<ring_type, node_type> p_node;
#define PBORI_PREFIX(name)
Definition: prefix.h:27
bool_type isConstant() const
Checks whether the the diagram corresponds to {} or {{}} (polynomial 0 or 1)
Definition: CCuddDDFacade.h:460
~CCuddDDFacade()
Destructor.
Definition: CCuddDDFacade.h:183
node_type * node_ptr
Pointer type for nodes.
Definition: CCuddDDFacade.h:124
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
DdNode node_type
Type for C-style struct.
Definition: CCuddDDFacade.h:121
first_iterator firstEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:416
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
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
bool isOne() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:247
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
void PrintMinterm() const
Definition: CCuddDDFacade.h:220
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
#define Cudd_NodeReadIndex
Definition: prefix_internal.h:91
last_iterator lastBegin() const
Start of first term.
Definition: CCuddDDFacade.h:421
NodeType pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q)
Definition: pbori_algo.h:755
#define Cudd_zddDiffConst
Definition: prefix_internal.h:175
CTypes::ostream_type ostream_type
Type for output streams.
Definition: CCuddDDFacade.h:112
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
double countDouble() const
Appriximate the number of terms.
Definition: CCuddDDFacade.h:229
#define cuddZddGetNode
Definition: prefix_internal.h:231
navigator navigation() const
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Definition: CCuddDDFacade.h:455
CCheckedIdx checked_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:148
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
This template class defines a facade as a C++ interface for applying C-style functions to C-style str...
Definition: CApplyNodeFacade.h:41
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator navi)
Definition: CCuddDDFacade.h:168
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
This template class is used for polybori's exception handling.
Definition: PBoRiGenericError.h:35
std::ostream ostream_type
Type for out-stream.
Definition: pbori_defs.h:246
first_iterator firstBegin() const
Get numbers of used variables.
Definition: CCuddDDFacade.h:411
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
void extrusive_ptr_add_ref(const DataType &, DdNode *ptr)
Incrememting reference counts to raw pointers to decision diagrams.
Definition: CCuddDDFacade.h:75
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
CCuddDDFacade(const ring_type &ring, node_ptr node)
Construct diagram from ring and node.
Definition: CCuddDDFacade.h:151
DiagramType diagram_type
Type for diagrams.
Definition: CCuddDDFacade.h:118
This class defines an iterator over the last minimal term of a given ZDD node.
Definition: CCuddLastIter.h:32
This template class defines a facade for decision diagrams.
Definition: CCuddDDFacade.h:103
valid_tag easy_equality_property
This type has an easy equality check.
Definition: CCuddDDFacade.h:139
ResultType memApply(ResultType(*func)(mgr_type *, node_ptr)) const
Definition: CCuddDDFacade.h:265
mgr_type * getManager() const
Get raw decision diagram manager.
Definition: CCuddDDFacade.h:256
diagram_type firstDivisors() const
Get decison diagram representing the divisors of the first term.
Definition: CCuddDDFacade.h:445
size_type refCount() const
Number of references pointing here.
Definition: CCuddDDFacade.h:238
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
last_iterator lastEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:426
int idx_type
Type for indices.
Definition: pbori_defs.h:228
CCuddFirstIter first_iterator
Iterator type for retrieving first term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:130
CCuddLastIter last_iterator
Iterator type for retrieving last term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:133
size_type nNodes() const
Number of nodes in the current decision diagram.
Definition: CCuddDDFacade.h:235
This class defines an iterator over the first minimal term of a given ZDD node.
Definition: CCuddFirstIter.h:35
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
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator thenNavi, navigator elseNavi)
Construct new node from manager, index, and navigators.
Definition: CCuddDDFacade.h:162
void checkAssumption(bool isValid) const
Check whether previous decision diagram operation for validity.
Definition: CCuddDDFacade.h:272
diagram_type divideFirst(const diagram_type &rhs) const
Division with first term of right-hand side.
Definition: CCuddDDFacade.h:387
#define Cudd_ReadZero
Definition: prefix_internal.h:46
int cudd_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:145
CCuddDDFacade(const self &from)
Copy constructor.
Definition: CCuddDDFacade.h:180
ring_type::mgr_type mgr_type
Raw context.
Definition: CCuddDDFacade.h:142
diagram_type & operator=(const diagram_type &rhs)
Assignment operator.
Definition: CCuddDDFacade.h:186
size_type count() const
Determine the number of terms.
Definition: CCuddDDFacade.h:226
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
CApplyNodeFacade< diagram_type, node_ptr > base
Type this is inherited from the following.
Definition: CCuddDDFacade.h:127
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_Deref
Definition: prefix_internal.h:160
std::ostream & printIntern(std::ostream &os) const
Definition: CCuddDDFacade.h:209
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
CCuddDDFacade(idx_type idx, const self &thenDD, const self &elseDD)
Construct new node.
Definition: CCuddDDFacade.h:173
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
RingType ring_type
Type for diagrams.
Definition: CCuddDDFacade.h:115
diagram_type Xor(const diagram_type &rhs) const
Union Xor.
Definition: CCuddDDFacade.h:377
CCuddNavigator navigator
Iterator type for navigation throught Cudd's ZDDs structure.
Definition: CCuddDDFacade.h:136
This template class defines an output iterator which interprets assignments of indices as a change of...
Definition: PBoRiOutIter.h:31
void extrusive_ptr_release(const DataType &data, DdNode *ptr)
Releasing raw pointers to decision diagrams here.
Definition: CCuddDDFacade.h:66
bool bool_type
Type for standard true/false statements.
Definition: pbori_defs.h:216
CCuddDDFacade(const ring_type &ring, const navigator &navi)
Construct from Manager and navigator.
Definition: CCuddDDFacade.h:157
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
DdManager mgr_type
Definition: BoolePolyRing.h:90
size_type rootIndex() const
Get index of curent node.
Definition: CCuddDDFacade.h:232
ostream_type & print(ostream_type &os) const
Get number of nodes in decision diagram.
Definition: CCuddDDFacade.h:398
This class defines CNodeCounter.
Definition: CNodeCounter.h:30
#define PB_ZDD_APPLY(count, data, funcname)
Definition: CCuddDDFacade.h:97
const char * error_text(pbori_DdManager *mgr)
Definition: CCuddInterface.h:45
This class shows, whether a property of an order is valid.
Definition: tags.h:32
node_ptr getNode() const
Get raw node structure.
Definition: CCuddDDFacade.h:253
This class defines CCheckedIdx.
Definition: CCheckedIdx.h:29
#define Cudd_Ref
Definition: prefix_internal.h:157