222 #ifndef CDDInterface_h_
223 #define CDDInterface_h_
269 return &
const_cast<Cudd&
>(mgr);
272 inline CCuddInterface::mgrcore_ptr
277 template <
class MgrType>
278 inline const MgrType&
288 template <
class MgrType>
289 inline const MgrType&
300 template<
class DDType>
317 m_interfaced(interfaced) {}
321 m_interfaced(rhs.m_interfaced) {}
335 template<
class CuddLikeZDD>
344 typedef typename zdd_traits<interfaced_type>::manager_base
manager_base;
358 using base::m_interfaced;
412 base_type(
self::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) {
426 elseDD.navigation()) ) {
434 return static_cast<hash_type>(
reinterpret_cast<std::ptrdiff_t
>(m_interfaced
445 return self(
base_type(m_interfaced.Union(rhs.m_interfaced)));
450 m_interfaced = m_interfaced.Union(rhs.m_interfaced);
454 self ite(
const self& then_dd,
const self& else_dd)
const {
455 return self(m_interfaced.Ite(then_dd, else_dd));
459 self&
iteAssign(
const self& then_dd,
const self& else_dd) {
460 m_interfaced = m_interfaced.Ite(then_dd, else_dd);
465 self diff(
const self& rhs)
const {
466 return m_interfaced.Diff(rhs.m_interfaced);
471 m_interfaced = m_interfaced.Diff(rhs.m_interfaced);
477 return m_interfaced.DiffConst(rhs.m_interfaced);
482 m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced);
488 return m_interfaced.Intersect(rhs.m_interfaced);
493 m_interfaced = m_interfaced.Intersect(rhs.m_interfaced);
499 return m_interfaced.Product(rhs.m_interfaced);
504 m_interfaced = m_interfaced.Product(rhs.m_interfaced);
510 return m_interfaced.UnateProduct(rhs.m_interfaced);
519 manager().getManager(),
520 m_interfaced.getNode(),
521 rhs.m_interfaced.getNode()));
527 manager().getManager(),
528 m_interfaced.getNode(),
529 rhs.m_interfaced.getNode()));
533 self Xor(
const self& rhs)
const {
536 #ifdef PBORI_LOWLEVEL_XOR
539 manager().getManager(),
540 m_interfaced.getNode(),
541 rhs.m_interfaced.getNode()));
545 manager().getManager(),
546 m_interfaced.getNode(),
547 rhs.m_interfaced.getNode()));
554 m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced);
560 return m_interfaced.Subset0(idx);
565 m_interfaced = m_interfaced.Subset0(idx);
571 return m_interfaced.Subset1(idx);
576 m_interfaced = m_interfaced.Subset1(idx);
583 return m_interfaced.Change(idx);
588 m_interfaced = m_interfaced.Change(idx);
594 return m_interfaced.Divide(rhs);
599 m_interfaced = m_interfaced.Divide(rhs);
604 return m_interfaced.WeakDiv(rhs);
609 m_interfaced = m_interfaced.WeakDiv(rhs);
617 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
626 result.divideFirstAssign(rhs);
634 return Cudd_zddDagSize(m_interfaced.getNode());
640 FILE* oldstdout = manager().ReadStdout();
644 manager().SetStdout(stdout);
645 else if (os == std::cerr)
646 manager().SetStdout(stderr);
648 m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) );
649 m_interfaced.PrintMinterm();
651 manager().SetStdout(oldstdout);
657 DdNode* tmp = m_interfaced.getNode();
658 Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp,
659 NULL, NULL, filehandle);
665 FILE* theFile = fopen( filename,
"w");
669 prettyPrint(theFile);
677 return (m_interfaced == rhs.m_interfaced);
682 return (m_interfaced != rhs.m_interfaced);
690 return m_interfaced.manager();
694 return Cudd_SupportSize(manager().getManager(), m_interfaced.getNode());
702 DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode());
706 Cudd_zddPortFromBdd(manager().getManager(), tmp));
707 Cudd_RecursiveDeref(manager().getManager(), tmp);
716 template<
class VectorLikeType>
719 int* pIdx = Cudd_SupportIndex( manager().getManager(),
720 m_interfaced.getNode() );
726 indices.reserve(std::accumulate(pIdx, pIdx + nlen,
size_type()));
728 for(
size_type idx = 0; idx < nlen; ++idx)
730 indices.push_back(idx);
738 return Cudd_SupportIndex( manager().getManager(),
739 m_interfaced.getNode() );
768 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
770 std::copy( firstBegin(), firstEnd(), indices.begin() );
773 indices.rbegin(), indices.rend(),
774 multipliers.rbegin(),
775 multipliers.rend() );
784 m_interfaced.getNode(),
785 rhs.m_interfaced.getNode()) );
792 m_interfaced.getNode(),
793 rhs.m_interfaced.getNode()) );
798 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
800 std::copy( firstBegin(), firstEnd(), indices.begin() );
807 return navigator(m_interfaced.getNode());
812 return ( m_interfaced.getNode() == manager().zddZero().getNode() );
818 return ( m_interfaced.getNode() ==
819 manager().zddOne( nVariables() ).getNode() );
824 return (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode());
829 return m_interfaced.Count();
839 return Cudd_ReadZddSize(manager().getManager() );
852 m_interfaced.getNode(),
853 rhs.m_interfaced.getNode()) );
860 m_interfaced.getNode(),
861 rhs.m_interfaced.getNode(),
875 return m_interfaced.CountDouble();
880 return manager().zddZero();
885 return manager().zddOne();
889 navigator newNode(
const manager_base& mgr,
idx_type idx,
890 navigator thenNavi, navigator elseNavi)
const {
891 assert(idx < *thenNavi);
892 assert(idx < *elseNavi);
893 return navigator(cuddZddGetNode(mgr.getManager(), idx,
894 thenNavi.getNode(), elseNavi.getNode()));
897 interfaced_type newDiagram(
const manager_base& mgr, navigator navi)
const {
901 self fromTemporaryNode(
const navigator& navi)
const {
903 return self(manager(), navi.getNode());
907 interfaced_type newNodeDiagram(
const manager_base& mgr,
idx_type idx,
909 navigator elseNavi)
const {
910 if ((idx >= *thenNavi) || (idx >= *elseNavi))
911 throw PBoRiGenericError<CTypes::invalid_ite>();
913 return newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) );
916 interfaced_type newNodeDiagram(
const manager_base& mgr,
917 idx_type idx, navigator navi)
const {
919 throw PBoRiGenericError<CTypes::invalid_ite>();
922 interfaced_type result =
923 newDiagram(mgr, newNode(mgr, idx, navi, navi) );
937 template <
class DDType>
938 typename CDDInterface<DDType>::ostream_type&
939 operator<<( typename CDDInterface<DDType>::ostream_type& os,
946 #endif // of #ifndef CDDInterface_h_