16 #ifndef polybori_routines_pbori_algo_int_h_
17 #define polybori_routines_pbori_algo_int_h_
36 template<
class NaviType>
47 template<
class NaviType>
58 template<
class NaviType>
61 return navi.getNode();
64 template <
class MgrType>
70 template <
class MgrType,
class NaviType>
73 navi.recursiveDecRef(mgr);
126 template<
class NaviType,
class ReverseIterator,
class DDOperations>
129 ReverseIterator idxStart, ReverseIterator idxFinish,
130 const DDOperations& apply){
132 typedef typename NaviType::value_type
idx_type;
133 typedef typename std::vector<idx_type> vector_type;
134 typedef typename vector_type::iterator iterator;
135 typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
137 vector_type indices(apply.nSupport(navi));
138 iterator iter(indices.begin());
140 NaviType multiples = navi;
142 while(!multiples.isConstant()) {
144 multiples.incrementThen();
148 const_reverse_iterator start(indices.rbegin()),
149 finish(indices.rend());
154 while(start != finish){
156 while( (idxStart != idxFinish) && (*idxStart > *start) ) {
157 apply.multiplesAssign(multiples, *idxStart);
160 apply.productAssign(multiples, *start);
161 if(idxStart != idxFinish)
171 template <
class NaviType>
175 while(!second.isConstant()){
176 while( (!first.isConstant()) && (*first < *second))
177 first.incrementThen();
178 if(*first != *second)
180 second.incrementThen();
185 template<
class NaviType,
class ReverseIterator,
class DDOperations>
188 ReverseIterator idxStart, ReverseIterator idxFinish,
189 const DDOperations& apply){
191 typedef typename NaviType::value_type
idx_type;
192 typedef typename std::vector<idx_type> vector_type;
193 typedef typename vector_type::iterator iterator;
194 typedef typename vector_type::size_type size_type;
195 typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
200 size_type nmax = apply.nSupport(navi);
201 vector_type thenIdx(nmax), elseIdx(nmax);
206 NaviType thenNavi = navi;
207 NaviType elseNavi = navi;
210 NaviType tmp(elseNavi);
211 elseNavi.incrementElse();
213 while(!elseNavi.isConstant()){
215 elseNavi.incrementElse();
217 if(elseNavi.isEmpty())
222 bool isReducible =
true;
223 while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
225 while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
230 thenIdx.push_back(*thenNavi);
231 thenNavi.incrementThen();
234 if(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
235 thenIdx.push_back(*thenNavi);
236 thenNavi.incrementThen();
242 elseIdx.push_back(*elseNavi);
245 elseNavi.incrementThen();
246 if( !elseNavi.isConstant() ) {
249 elseNavi.incrementElse();
252 if( elseNavi.isEmpty() )
259 NaviType elseTail, elseMult;
260 apply.assign(elseTail, elseNavi);
265 if (!elseNavi.isConstant()) {
275 apply.assign(elseMult, elseTail);
279 idxStart, idxFinish, apply);
286 NaviType thenTail, thenMult;
292 apply.assign(thenTail, thenNavi);
295 if (!thenNavi.isConstant()){
306 apply.assign(thenMult, thenTail);
311 ReverseIterator idxIter = idxStart;
312 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
317 if(!elseMult.isConstant())
318 while((idxIter != idxFinish) && (*idxIter >= *elseMult) )
321 while(start != finish){
323 while((idxIter != idxFinish) && (*idxIter > *start) ) {
325 apply.multiplesAssign(elseMult, *idxIter);
328 apply.productAssign(elseMult, *start);
331 apply.productAssign(elseTail, *start);
333 if(idxIter != idxFinish)
339 multiples = elseMult;
353 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
354 ReverseIterator idxIter = idxStart;
362 if(!thenMult.isConstant())
363 while((idxIter != idxFinish) && (*idxIter >= *thenMult) )
370 while(start2 != finish2){
372 while((idxIter != idxFinish) && (*idxIter > *start2) ) {
374 apply.multiplesAssign(thenMult, *idxIter);
377 apply.productAssign(thenMult, *start2);
379 if(idxIter != idxFinish)
385 apply.replacingUnite(multiples, elseMult, thenMult);
401 apply.kill(elseTail);
402 apply.kill(thenTail);
405 return apply.newNode(navi);
438 template <
class NaviType,
class SizeType,
class ReverseIterator,
442 ReverseIterator start, ReverseIterator finish,
443 const DDOperations& apply) {
445 if (navi.isConstant()){
446 if (!navi.terminalValue())
450 while ( (start != finish) && (*start >= *navi) )
453 while( (start != finish) && (*start > minIdx) ){
454 apply.multiplesAssign(navi, *start);
460 template<
class FunctionType,
class ManagerType,
class NodeType>
462 NodeType& first,
const NodeType& second) {
472 template<
class FunctionType,
class ManagerType,
class ResultType,
476 const NodeType& first,
477 const NodeType& second) {
485 template<
class FunctionType,
class ManagerType,
class NodeType>
487 const NodeType& first,
const NodeType& second) {
495 template <
class DDType>
508 const navigator& first,
const navigator& second)
const {
513 void uniteAssign(navigator& first,
const navigator& second)
const {
516 void diffAssign(navigator& first,
const navigator& second)
const {
519 navigator
diff(
const navigator& first,
const navigator& second)
const {
523 navigator& first, navigator& second)
const {
533 navigator& thenNode,
const navigator& elseNode)
const {
544 newNodeAssign(idx, node, node);
549 newNodeAssign(idx, node, emptyset);
552 void assign(navigator& first,
const navigator& second)
const {
557 void replace(navigator& first,
const navigator& second)
const {
574 void kill(navigator& node)
const {
584 template <
class NaviType,
class DDType2,
class ReverseIterator,
589 ReverseIterator idxStart, ReverseIterator idxEnd,
590 const DDOperations& apply) {
594 if (!navi.isConstant()) {
596 int nlen = apply.length(navi);
598 if(
false&&(nlen == 2)) {
610 std::vector<int> indices (apply.nSupport(navi));
611 std::vector<int>::iterator iter(indices.begin()), iend(indices.end());
612 bool is_reducible =
true;
613 bool reducible_tested =
false;
618 while( is_reducible&&(!multiples.isConstant())) {
622 thenBr = multiples.thenBranch();
623 elseBr = multiples.elseBranch();
625 if((elseBr.isConstant() && elseBr.terminalValue())) {
630 else if (elseBr.isConstant() && !elseBr.terminalValue())
633 if (!reducible_tested){
634 reducible_tested ==
true;
652 indices.resize(used);
656 std::vector<int>::const_reverse_iterator start(indices.rbegin()),
657 finish(indices.rend());
664 NaviType tmp,tmpnavi;
666 apply.assign(tmpnavi, multiples);
668 ReverseIterator idxIter = idxStart;
669 while(start != finish){
671 while((idxIter != idxEnd) && (*idxIter > *start) ) {
673 apply.multiplesAssign(multiples, *idxIter);
676 apply.productAssign(multiples, *start);
677 apply.productAssign(tmpnavi, *start);
678 if(idxIter != idxEnd)
700 return apply.newNode(navi);
707 elseMult, idxStart, idxEnd, apply);
709 idxStart, idxEnd, apply);
712 if( (navi.elseBranch() == navi.thenBranch()) ||
713 (elsedd.isConstant() && elsedd.terminalValue()) ){
714 multiples = elseMult;
719 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
724 idxStart, idxEnd, apply));
726 idxStart, idxEnd, apply);
729 apply.uniteAssign(thenMult, elseMult);
730 apply.replacingNode(multiples, *navi, thenMult, elseMult);
734 apply.replacingNode(result, *navi, thenNavi, elsedd);
740 apply.assign(multiples, navi);
742 return apply.newNode(navi);
#define PBORI_PREFIX(name)
Definition: prefix.h:27
void replacingUnite(navigator &newNode, const navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:507
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
DdManager * manager_type
Definition: pbori_algo_int.h:502
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
NaviType minimal_of_two_terms(NaviType navi, NaviType &multiples, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply)
Definition: pbori_algo_int.h:187
void replace(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:557
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
void replacingNode(navigator &newNode, idx_type idx, navigator &first, navigator &second) const
Definition: pbori_algo_int.h:522
void incRef() const
Force incrementation of reference count.
Definition: CCuddNavigator.h:142
NaviType prepend_multiples_wrt_indices(NaviType navi, SizeType minIdx, ReverseIterator start, ReverseIterator finish, const DDOperations &apply)
Definition: pbori_algo_int.h:441
navigator diff(const navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:519
void apply_replacing_cudd_function(FunctionType func, ManagerType &mgr, ResultType &newNode, const NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:474
#define cuddZddGetNode
Definition: prefix_internal.h:231
#define Cudd_zddDiff
Definition: prefix_internal.h:172
DdNode * do_get_node(const NaviType &navi)
Definition: pbori_algo_int.h:60
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
void assign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:552
void recursive_dec_ref(const MgrType &mgr, const NaviType &navi)
Definition: pbori_algo_int.h:72
void productAssign(navigator &node, idx_type idx) const
Definition: pbori_algo_int.h:547
#define Cudd_zddUnion
Definition: prefix_internal.h:174
navigator & newNode(navigator &node) const
Definition: pbori_algo_int.h:569
Definition: pbori_algo_int.h:496
size_type length(const navigator &node) const
Definition: pbori_algo_int.h:565
dd_operations(manager_type man)
Definition: pbori_algo_int.h:506
size_type nSupport(const navigator &node) const
Definition: pbori_algo_int.h:562
pbori_DdManager DdManager
Definition: traits.h:33
void inc_ref(const NaviType &navi)
Definition: pbori_algo_int.h:38
int idx_type
Type for indices.
Definition: pbori_defs.h:228
void diffAssign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:516
const_access_type getNode() const
Constant pointer access operator.
Definition: CCuddNavigator.h:107
#define Cudd_ReadZero
Definition: prefix_internal.h:46
manager_type mgr
Definition: pbori_algo_int.h:578
void kill(navigator &node) const
Definition: pbori_algo_int.h:574
NaviType indexed_term_multiples(NaviType navi, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply)
Definition: pbori_algo_int.h:128
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_Deref
Definition: prefix_internal.h:160
void multiplesAssign(navigator &node, idx_type idx) const
Definition: pbori_algo_int.h:543
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
bool is_reducible_by(NaviType first, NaviType second)
Definition: pbori_algo_int.h:173
NaviType dd_minimal_elements(NaviType navi, DDType2 &multiples, ReverseIterator idxStart, ReverseIterator idxEnd, const DDOperations &apply)
Definition: pbori_algo_int.h:588
void dec_ref(const NaviType &navi)
Definition: pbori_algo_int.h:49
void apply_assign_cudd_function(FunctionType func, ManagerType &mgr, NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:461
NodeType apply_cudd_function(FunctionType func, ManagerType &mgr, const NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:486
void newNodeAssign(idx_type idx, navigator &thenNode, const navigator &elseNode) const
Definition: pbori_algo_int.h:532
CCuddNavigator navigator
Definition: pbori_algo_int.h:503
void uniteAssign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:513
#define Cudd_Ref
Definition: prefix_internal.h:157