164 #ifndef pbori_algo_h_
165 #define pbori_algo_h_
171 template<
class NaviType,
class TermType,
172 class TernaryOperator,
173 class TerminalOperator >
176 TerminalOperator terminate ) {
178 TermType result = init;
180 if (navi.isConstant()) {
181 if (navi.terminalValue()){
182 result = terminate();
187 result = newNode(*navi, result,
196 template<
class NaviType,
class TermType,
class OutIterator,
197 class ThenBinaryOperator,
class ElseBinaryOperator,
198 class TerminalOperator >
201 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
202 TerminalOperator terminate ) {
205 if (navi.isConstant()) {
206 if (navi.terminalValue()){
207 *result = terminate(init);
212 result =
dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
213 then_binop, else_binop, terminate);
214 result =
dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
215 then_binop, else_binop, terminate);
222 template<
class NaviType,
class TermType,
class OutIterator,
223 class ThenBinaryOperator,
class ElseBinaryOperator,
224 class TerminalOperator,
class FirstTermOp >
227 ThenBinaryOperator then_binop, ElseBinaryOperator else_binop,
228 TerminalOperator terminate, FirstTermOp terminate_first ) {
230 if (navi.isConstant()) {
231 if (navi.terminalValue()){
232 *result = terminate_first(init);
237 result =
dd_transform(navi.thenBranch(), then_binop(init, *navi), result,
238 then_binop, else_binop, terminate, terminate_first);
239 result =
dd_transform(navi.elseBranch(), else_binop(init, *navi), result,
240 then_binop, else_binop, terminate);
246 template<
class NaviType,
class TermType,
class OutIterator,
247 class ThenBinaryOperator,
class ElseBinaryOperator >
250 const OutIterator& result,
251 const ThenBinaryOperator& then_binop,
252 const ElseBinaryOperator& else_binop ) {
254 dd_transform(navi, init, result, then_binop, else_binop,
259 template<
class NaviType,
class TermType,
class OutIterator,
260 class ThenBinaryOperator >
263 const OutIterator& result,
264 const ThenBinaryOperator& then_binop ) {
272 template <
class InputIterator,
class OutputIterator,
273 class FirstFunction,
class UnaryFunction>
276 OutputIterator result,
277 UnaryFunction op, FirstFunction firstop) {
278 InputIterator second(first);
279 if (second != last) {
281 result = std::transform(first, second, result, firstop);
283 return std::transform(second, last, result, op);
288 template <
class InputIterator,
class Intermediate,
class OutputIterator>
291 Intermediate& inter, OutputIterator output ) {
293 std::copy(start, finish, inter.begin());
295 return std::copy( const_cast<const Intermediate&>(inter).rbegin(),
296 const_cast<const Intermediate&>(inter).rend(),
302 template <
class NaviType>
306 if (navi.isConstant())
307 return navi.terminalValue();
314 template <
class NaviType,
class OrderedIterator>
317 OrderedIterator start, OrderedIterator finish) {
319 if (!navi.isConstant()) {
322 while( (not_at_end = (start != finish)) && (*start < *navi) )
325 NaviType elsenode = navi.elseBranch();
327 if (elsenode.isConstant() && elsenode.terminalValue())
333 if ( (*start == *navi) &&
341 while(!elsenode.isConstant())
342 elsenode.incrementElse();
343 return elsenode.terminalValue();
347 return navi.terminalValue();
353 template <
class NaviType,
class OrderedIterator,
class NodeOperation>
356 OrderedIterator start, OrderedIterator finish,
357 NodeOperation newNode ) {
359 if (!navi.isConstant()) {
361 while( (not_at_end = (start != finish)) && (*start < *navi) )
369 if (*start == *navi) {
375 return newNode(*start, navi, thenNode, elseNode);
382 while(!navi.isConstant())
383 navi = navi.elseBranch();
384 return newNode(navi);
389 return newNode(navi);
395 template <
class NaviType>
399 if (!navi.isConstant()) {
401 std::cout << std::endl<<
"idx " << *navi <<
" addr "<<
402 ((DdNode*)navi)<<
" ref "<<
403 int(Cudd_Regular((DdNode*)navi)->ref) << std::endl;
410 std::cout <<
"const isvalid? "<<navi.isValid()<<
" addr "
411 <<((DdNode*)navi)<<
" ref "<<
412 int(Cudd_Regular((DdNode*)navi)->ref)<<std::endl;
418 template <
class IteratorType,
class SizeType>
424 while ((result < limit) && (start != finish)) {
433 template <
class,
class,
class,
class,
class,
class>
class CTermIter;
436 template <
class NaviType,
class SizeType>
438 limited_length(NaviType navi, SizeType limit) {
441 typedef CTermIter<dummy_iterator, NaviType,
453 template <
class NaviType,
class DDType>
458 if (!navi.isConstant()) {
460 DDType elsedd = dd.subset0(*navi);
463 DDType elseMultiples;
467 if((navi.elseBranch() == navi.thenBranch()) || elsedd.blankness()){
468 multiples = elseMultiples;
472 NaviType elseNavi = elseMultiples.navigation();
475 if (elseNavi.isConstant()){
476 if (elseNavi.terminalValue())
477 nmax = dd.nVariables();
485 for(
int i = nmax-1; i > *navi; --i){
486 elseMultiples.uniteAssign(elseMultiples.change(i));
490 DDType thendd = dd.subset1(*navi);
491 thendd = thendd.diff(elseMultiples);
493 DDType thenMultiples;
496 NaviType thenNavi = thenMultiples.navigation();
499 if (thenNavi.isConstant()){
500 if (thenNavi.terminalValue())
501 nmax = dd.nVariables();
509 for(
int i = nmax-1; i > *navi; --i){
510 thenMultiples.uniteAssign(thenMultiples.change(i));
514 thenMultiples = thenMultiples.unite(elseMultiples);
515 thenMultiples = thenMultiples.change(*navi);
518 multiples = thenMultiples.unite(elseMultiples);
519 thendd = thendd.change(*navi);
521 DDType result = thendd.unite(elsedd);
531 template <
class MgrType>
532 inline const MgrType&
538 return &
const_cast<Cudd&
>(rhs);
542 inline CCuddInterface::mgrcore_ptr
548 template<
class ManagerType,
class ReverseIterator,
class MultReverseIterator>
549 typename manager_traits<ManagerType>::dd_base
551 ReverseIterator start, ReverseIterator finish,
552 MultReverseIterator multStart,
553 MultReverseIterator multFinish) {
555 DdNode* prev( (mgr.getManager())->one );
557 DdNode* zeroNode( (mgr.getManager())->zero );
560 while(start != finish) {
562 while((multStart != multFinish) && (*start < *multStart)) {
564 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
568 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
575 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
579 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
584 if((multStart != multFinish) && (*start == *multStart))
591 while(multStart != multFinish) {
593 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *multStart,
597 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
613 template<
class ManagerType,
class ReverseIterator>
614 typename manager_traits<ManagerType>::dd_base
616 ReverseIterator start, ReverseIterator finish) {
619 DdNode* prev= (mgr.getManager())->one;
622 while(start != finish) {
624 DdNode* result = cuddUniqueInterZdd( mgr.getManager(), *start,
628 Cudd_RecursiveDerefZdd(mgr.getManager(), prev);
641 template<
class Iterator,
class SizeType>
648 Iterator result(start);
652 while (start != finish) {
665 template <
class LhsType,
class RhsType,
class BinaryPredicate>
670 return CTypes::equality;
672 return (comp(lhs, rhs)? CTypes::greater_than: CTypes::less_than);
677 template <
class IteratorLike,
class ForwardIteratorTag>
684 template <
class IteratorLike>
688 return iter.thenBranch();
692 template <
class IteratorLike>
696 typedef typename std::iterator_traits<IteratorLike>::iterator_category
702 #ifdef PBORI_LOWLEVEL_XOR
712 template <
class MgrType,
class NodeType>
717 NodeType empty = DD_ZERO(zdd), t, e, res;
734 if (cuddIsConstant(P))
738 if (cuddIsConstant(Q))
744 if (e == NULL)
return (NULL);
746 res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
748 Cudd_RecursiveDerefZdd(table, e);
752 }
else if (p_top > q_top) {
754 if (e == NULL)
return(NULL);
756 res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
758 Cudd_RecursiveDerefZdd(table, e);
764 if (t == NULL)
return(NULL);
768 Cudd_RecursiveDerefZdd(table, t);
772 res = cuddZddGetNode(zdd, P->index, t, e);
774 Cudd_RecursiveDerefZdd(table, t);
775 Cudd_RecursiveDerefZdd(table, e);
787 template <
class MgrType,
class NodeType>
795 }
while (dd->reordered == 1);
799 #endif // PBORI_LOWLEVEL_XOR
802 template <
class NaviType>
806 while(!navi.isConstant()) {
807 if (!navi.elseBranch().isEmpty())
809 navi.incrementThen();
814 template <
class NaviType,
class BooleConstant>
818 while(!navi.isConstant()) {
820 if (!navi.elseBranch().isEmpty())
824 navi.incrementThen();
826 return allowSingleton;
830 template <
class NaviType>
837 template <
class NaviType>
846 template <
class SetType>
848 init += bset.sizeDouble();
851 template <
class SetType>
853 typename SetType::size_type& init) {
858 template <
class SizeType,
class IdxType,
class NaviType,
class SetType>
860 count_index(SizeType& size, IdxType idx, NaviType navi,
const SetType& init) {
863 combine_sizes(SetType(navi.incrementThen(), init.ring()), size);
873 template <
class SizeType,
class IdxType,
class SetType>
877 return count_index(size, idx, bset.navigation(), SetType());