19 #ifndef polybori_routines_pbori_algo_h_
20 #define polybori_routines_pbori_algo_h_
37 template<
class NaviType,
class TermType,
38 class TernaryOperator,
39 class TerminalOperator >
42 TerminalOperator terminate ) {
44 TermType result = init;
46 if (navi.isConstant()) {
47 if (navi.terminalValue()){
53 result = newNode(*navi, result,
62 template<
class NaviType,
class TermType,
class OutIterator,
63 class ThenBinaryOperator,
class ElseBinaryOperator,
64 class TerminalOperator >
67 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
68 TerminalOperator terminate ) {
71 if (navi.isConstant()) {
72 if (navi.terminalValue()){
73 *result = terminate(init);
78 result =
dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
79 then_binop, else_binop, terminate);
80 result =
dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
81 then_binop, else_binop, terminate);
88 template<
class NaviType,
class TermType,
class OutIterator,
89 class ThenBinaryOperator,
class ElseBinaryOperator,
90 class TerminalOperator,
class FirstTermOp >
93 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
94 TerminalOperator terminate, FirstTermOp terminate_first ) {
96 if (navi.isConstant()) {
97 if (navi.terminalValue()){
98 *result = terminate_first(init);
103 result =
dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
104 then_binop, else_binop, terminate, terminate_first);
105 result =
dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
106 then_binop, else_binop, terminate);
112 template<
class NaviType,
class TermType,
class OutIterator,
113 class ThenBinaryOperator,
class ElseBinaryOperator >
116 const OutIterator& result,
117 const ThenBinaryOperator& then_binop,
118 const ElseBinaryOperator& else_binop ) {
120 dd_transform(navi, init, result, then_binop, else_binop,
125 template<
class NaviType,
class TermType,
class OutIterator,
126 class ThenBinaryOperator >
129 const OutIterator& result,
130 const ThenBinaryOperator& then_binop ) {
138 template <
class InputIterator,
class OutputIterator,
139 class FirstFunction,
class UnaryFunction>
142 OutputIterator result,
143 UnaryFunction op, FirstFunction firstop) {
144 InputIterator second(first);
145 if (second != last) {
154 template <
class InputIterator,
class Intermediate,
class OutputIterator>
157 Intermediate& inter, OutputIterator output ) {
159 std::copy(start, finish, inter.begin());
161 return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
162 const_cast<const Intermediate&>(inter).rend(),
168 template <
class NaviType>
172 if (navi.isConstant())
173 return navi.terminalValue();
180 template <
class NaviType,
class OrderedIterator>
183 OrderedIterator start, OrderedIterator finish) {
185 if (!navi.isConstant()) {
188 while( (not_at_end = (start != finish)) && (*start < *navi) )
191 NaviType elsenode = navi.elseBranch();
193 if (elsenode.isConstant() && elsenode.terminalValue())
199 if ( (*start == *navi) &&
207 while(!elsenode.isConstant())
208 elsenode.incrementElse();
209 return elsenode.terminalValue();
213 return navi.terminalValue();
219 template <
class NaviType,
class OrderedIterator,
class NodeOperation>
222 OrderedIterator start, OrderedIterator finish,
223 NodeOperation newNode ) {
225 if (!navi.isConstant()) {
227 while( (not_at_end = (start != finish)) && (*start < *navi) )
235 if (*start == *navi) {
241 return newNode(*start, navi, thenNode, elseNode);
248 while(!navi.isConstant())
249 navi = navi.elseBranch();
250 return newNode(navi);
255 return newNode(navi);
261 template <
class NaviType>
265 if (!navi.isConstant()) {
267 std::cout << std::endl<<
"idx " << *navi <<
" addr "<<
268 ((DdNode*)navi)<<
" ref "<<
269 int(
PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref) << std::endl;
276 std::cout <<
"const isvalid? "<<navi.isValid()<<
" addr "
277 <<((DdNode*)navi)<<
" ref "<<
278 int(
PBORI_PREFIX(Cudd_Regular)((DdNode*)navi)->ref)<<std::endl;
284 template <
class IteratorType,
class SizeType>
290 while ((result < limit) && (start != finish)) {
299 template <
class,
class,
class,
class,
class,
class>
class CTermIter;
302 template <
class NaviType,
class SizeType>
304 limited_length(NaviType navi, SizeType limit) {
307 typedef CTermIter<dummy_iterator, NaviType,
308 project_ith<1>, project_ith<1>, project_ith<1, 2>,
317 template <
class NaviType>
319 while (!navi.isConstant() )
320 navi.incrementElse();
322 return navi.terminalValue();
325 template <
class CacheMgr,
class NaviType,
class SetType>
328 NaviType navi, NaviType rhs,
const SetType& init){
331 if (
owns_one(rhs))
return cache_mgr.zero();
333 if (navi.isConstant())
334 return cache_mgr.generate(navi);
340 if (rhs.isConstant())
341 return cache_mgr.generate(navi);
344 return cache_mgr.zero();
347 NaviType cached = cache_mgr.find(navi, rhs);
348 if (cached.isValid())
349 return cache_mgr.generate(cached);
352 SetType result(cache_mgr.zero());
355 NaviType rhselse = rhs.elseBranch();
362 thenres.navigation(), rhselse, init),
364 navi.elseBranch(), rhselse, init)
376 cache_mgr.insert(navi, rhs, result.navigation());
381 template <
class CacheMgr,
class ModMonCacheMgr,
class NaviType,
class SetType>
384 NaviType navi,
const SetType& init){
388 return cache_mgr.generate(navi);
390 if (
owns_one(navi))
return cache_mgr.one();
392 NaviType ms0 = navi.elseBranch();
393 NaviType ms1 = navi.thenBranch();
396 NaviType cached = cache_mgr.find(navi);
397 if (cached.isValid())
398 return cache_mgr.generate(cached);
401 SetType minimal_then =
404 minimal_else.navigation(),
407 SetType result(cache_mgr.zero());
408 if ( (minimal_else.navigation() == ms0)
409 && (minimal_then.navigation() == ms1) )
410 result = cache_mgr.generate(navi);
412 result = SetType(*navi, minimal_then, minimal_else);
414 cache_mgr.insert(navi, result.navigation());
422 template <
class NaviType,
class DDType>
427 if (!navi.isConstant()) {
429 DDType elsedd = dd.subset0(*navi);
432 DDType elseMultiples;
436 if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
437 multiples = elseMultiples;
441 NaviType elseNavi = elseMultiples.navigation();
444 if (elseNavi.isConstant()){
445 if (elseNavi.terminalValue())
446 nmax = dd.nVariables();
454 for(
int i = nmax-1; i > *navi; --i){
455 elseMultiples.uniteAssign(elseMultiples.change(i));
459 DDType thendd = dd.subset1(*navi);
460 thendd = thendd.diff(elseMultiples);
462 DDType thenMultiples;
465 NaviType thenNavi = thenMultiples.navigation();
468 if (thenNavi.isConstant()){
469 if (thenNavi.terminalValue())
470 nmax = dd.nVariables();
478 for(
int i = nmax-1; i > *navi; --i){
479 thenMultiples.uniteAssign(thenMultiples.change(i));
483 thenMultiples = thenMultiples.unite(elseMultiples);
484 thenMultiples = thenMultiples.change(*navi);
487 multiples = thenMultiples.unite(elseMultiples);
488 thendd = thendd.change(*navi);
490 DDType result = thendd.unite(elsedd);
500 template <
class MgrType>
501 inline const MgrType&
514 template<
class ManagerType,
class ReverseIterator,
class MultReverseIterator,
518 ReverseIterator start, ReverseIterator finish,
519 MultReverseIterator multStart,
522 DdNode* prev( (mgr.getManager())->one );
524 DdNode* zeroNode( (mgr.getManager())->zero );
527 while(start != finish) {
529 while((multStart != multFinish) && (*start < *multStart)) {
551 if((multStart != multFinish) && (*start == *multStart))
558 while(multStart != multFinish) {
573 typedef DDBase dd_base;
574 return dd_base(mgr, prev);
580 template<
class ManagerType,
class ReverseIterator,
class DDBase>
586 DdNode* prev= (mgr.getManager())->one;
589 while(start != finish) {
603 return DDBase(mgr, prev);
608 template<
class Iterator,
class SizeType>
615 Iterator result(start);
619 while (start != finish) {
631 template <
class LhsType,
class RhsType,
class BinaryPredicate>
636 return CTypes::equality;
638 return (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
643 template <
class IteratorLike,
class ForwardIteratorTag>
650 template <
class IteratorLike>
654 return iter.thenBranch();
658 template <
class IteratorLike>
662 typedef typename std::iterator_traits<IteratorLike>::iterator_category
668 #ifdef PBORI_LOWLEVEL_XOR
678 template <
class MgrType,
class NodeType>
683 NodeType empty = DD_ZERO(zdd), t, e, res;
710 if (e == NULL)
return (NULL);
718 }
else if (p_top > q_top) {
720 if (e == NULL)
return(NULL);
730 if (t == NULL)
return(NULL);
753 template <
class MgrType,
class NodeType>
761 }
while (dd->reordered == 1);
765 #endif // PBORI_LOWLEVEL_XOR
768 template <
class NaviType>
772 while(!navi.isConstant()) {
773 if (!navi.elseBranch().isEmpty())
775 navi.incrementThen();
780 template <
class NaviType,
class BooleConstant>
784 while(!navi.isConstant()) {
786 if (!navi.elseBranch().isEmpty())
790 navi.incrementThen();
792 return allowSingleton;
796 template <
class NaviType>
803 template <
class NaviType>
812 template <
class SetType>
814 init += bset.sizeDouble();
817 template <
class SetType>
819 typename SetType::size_type& init) {
824 template <
class SizeType,
class IdxType,
class NaviType,
class SetType>
826 count_index(SizeType& size, IdxType idx, NaviType navi,
const SetType& init) {
829 combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
839 template <
class SizeType,
class IdxType,
class SetType>
843 return count_index(size, idx, bset.navigation(), SetType(bset.ring()));
847 template <
class InIter,
class OutIter,
class Object,
class MemberFuncPtr>
849 transform(InIter start, InIter finish, OutIter result, Object& obj,
850 MemberFuncPtr func) {
851 for(; start != finish; ++start, ++result)
852 *result = (obj .* func)(*start);
855 template <
class InIter,
class Object,
class MemberFuncPtr>
857 for_each(InIter start, InIter finish, Object& obj, MemberFuncPtr func) {
858 for(; start != finish; ++start)
859 (obj .* func)(*start);
862 template <
class InIter,
class Object,
class MemberFuncPtr>
864 for_each(InIter start, InIter finish,
const Object& obj, MemberFuncPtr func) {
865 for(; start != finish; ++start)
866 (obj .* func)(*start);
868 template <
class Type,
class Type1>
870 which(
bool condition,
const Type1& value1,
const Type& value) {
876 template <
class Type,
class Type1,
class Type2>
878 which(
bool cond1,
const Type1& value1,
879 bool cond2,
const Type2& value2,
const Type& value) {
880 return which(cond1, value1,
which(cond2, value2, value) );
883 template <
class Type,
class Type1,
class Type2,
class Type3>
885 which(
bool cond1,
const Type1& value1,
886 bool cond2,
const Type2& value2,
887 bool cond3,
const Type3& value3,
const Type& value ) {
888 return which(cond1, value1, cond2, value2,
which(cond3, value3, value) );
894 template <
class IDType,
class Iterator>
895 bool same_rings(
const IDType&
id, Iterator start, Iterator finish) {
897 while ((start != finish) && (start->ring().id() == id)) { ++start; }
898 return (start == finish);
901 template <
class Iterator>
904 return (start == finish) ||
same_rings(start->ring().id(), start, finish);