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());
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)) { }
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))
201 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()); }
264 template <
class ResultType>
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) {
348 template<
class ManagerType,
class ReverseIterator>
351 ReverseIterator start, ReverseIterator finish)
const {
354 DdNode* prev= (getManager())->one;
357 while(start != finish) {
382 base::checkSameManager(rhs);
400 printIntern(os) << std::endl;;
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() );
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;