00001
00002
00223
00224
00225 #ifndef CDDInterface_h_
00226 #define CDDInterface_h_
00227
00228 #include "extrafwd.h"
00229
00230 #include "pbori_defs.h"
00231
00232
00233
00234
00235 #include "CCuddNavigator.h"
00236
00237
00238 #include "CCuddFirstIter.h"
00239
00240
00241 #include "CCuddLastIter.h"
00242
00243
00244 #include "CCuddGetNode.h"
00245
00246
00247 #include "PBoRiOutIter.h"
00248
00249
00250 #include "PBoRiGenericError.h"
00251
00252
00253 #include "cuddInt.h"
00254
00255 #include "pbori_algo.h"
00256
00257 #include "pbori_tags.h"
00258 #include "pbori_routines_hash.h"
00259
00260
00261 #include <vector>
00262 #include <numeric>
00263
00264 #include "CCuddInterface.h"
00265 #include "pbori_traits.h"
00266
00267 BEGIN_NAMESPACE_PBORI
00268
00269
00270 inline Cudd*
00271 extract_manager(const Cudd& mgr) {
00272 return &const_cast<Cudd&>(mgr);
00273 }
00274
00275 inline CCuddInterface::mgrcore_ptr
00276 extract_manager(const CCuddInterface& mgr) {
00277 return mgr.managerCore();
00278 }
00279
00280 template <class MgrType>
00281 inline const MgrType&
00282 extract_manager(const MgrType& mgr) {
00283 return mgr;
00284 }
00285
00286 inline Cudd&
00287 get_manager(Cudd* mgr) {
00288 return *mgr;
00289 }
00290
00291 template <class MgrType>
00292 inline const MgrType&
00293 get_manager(const MgrType& mgr) {
00294 return mgr;
00295 }
00303 template<class DDType>
00304 class CDDInterfaceBase {
00305
00306 public:
00307
00309 typedef DDType interfaced_type;
00310
00312 typedef CDDInterfaceBase<interfaced_type> self;
00313
00315 CDDInterfaceBase() :
00316 m_interfaced() {}
00317
00319 CDDInterfaceBase(const interfaced_type& interfaced) :
00320 m_interfaced(interfaced) {}
00321
00323 CDDInterfaceBase(const self& rhs) :
00324 m_interfaced(rhs.m_interfaced) {}
00325
00327 ~CDDInterfaceBase() {}
00328
00330 operator const interfaced_type&() const { return m_interfaced; }
00331
00332 protected:
00333 interfaced_type m_interfaced;
00334 };
00335
00338 template<class CuddLikeZDD>
00339 class CDDInterface:
00340 public CDDInterfaceBase<CuddLikeZDD> {
00341 public:
00342
00344 typedef CuddLikeZDD interfaced_type;
00345
00347 typedef typename zdd_traits<interfaced_type>::manager_base manager_base;
00348
00350 typedef typename manager_traits<manager_base>::tmp_ref mgr_ref;
00351
00353 typedef typename manager_traits<manager_base>::core_type core_type;
00354
00356 typedef CDDManager<CCuddInterface> manager_type;
00357
00359 typedef CDDInterfaceBase<interfaced_type> base_type;
00360 typedef base_type base;
00361 using base::m_interfaced;
00362
00364 typedef CDDInterface<interfaced_type> self;
00365
00367 typedef CTypes::size_type size_type;
00368
00370 typedef CTypes::deg_type deg_type;
00371
00373 typedef CTypes::idx_type idx_type;
00374
00376 typedef CTypes::ostream_type ostream_type;
00377
00379 typedef CTypes::bool_type bool_type;
00380
00382 typedef CTypes::hash_type hash_type;
00383
00385 typedef CCuddFirstIter first_iterator;
00386
00388 typedef CCuddLastIter last_iterator;
00389
00391 typedef CCuddNavigator navigator;
00392
00394 typedef FILE* pretty_out_type;
00395
00397 typedef const char* filename_type;
00398
00400 typedef valid_tag easy_equality_property;
00401
00403 CDDInterface(): base_type() {}
00404
00406 CDDInterface(const self& rhs): base_type(rhs) {}
00407
00409 CDDInterface(const interfaced_type& rhs): base_type(rhs) {}
00410
00412 CDDInterface(const manager_base& mgr, const navigator& navi):
00413 base_type(self::newDiagram(mgr, navi)) {}
00414
00416 CDDInterface(const manager_base& mgr,
00417 idx_type idx, navigator thenNavi, navigator elseNavi):
00418 base_type( self::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) {
00419 }
00420
00423 CDDInterface(const manager_base& mgr,
00424 idx_type idx, navigator navi):
00425 base_type( self::newNodeDiagram(mgr, idx, navi, navi) ) {
00426 }
00427
00429 CDDInterface(idx_type idx, const self& thenDD, const self& elseDD):
00430 base_type( self::newNodeDiagram(thenDD.manager(), idx,
00431 thenDD.navigation(),
00432 elseDD.navigation()) ) {
00433 }
00434
00436 ~CDDInterface() {}
00437
00439 hash_type hash() const {
00440 return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t>(m_interfaced
00441 .getNode()));
00442 }
00443
00445 hash_type stableHash() const {
00446 return stable_hash_range(navigation());
00447 }
00448
00450 self unite(const self& rhs) const {
00451 return self(base_type(m_interfaced.Union(rhs.m_interfaced)));
00452 };
00453
00455 self& uniteAssign(const self& rhs) {
00456 m_interfaced = m_interfaced.Union(rhs.m_interfaced);
00457 return *this;
00458 };
00460 self ite(const self& then_dd, const self& else_dd) const {
00461 return self(m_interfaced.Ite(then_dd, else_dd));
00462 };
00463
00465 self& iteAssign(const self& then_dd, const self& else_dd) {
00466 m_interfaced = m_interfaced.Ite(then_dd, else_dd);
00467 return *this;
00468 };
00469
00471 self diff(const self& rhs) const {
00472 return m_interfaced.Diff(rhs.m_interfaced);
00473 };
00474
00476 self& diffAssign(const self& rhs) {
00477 m_interfaced = m_interfaced.Diff(rhs.m_interfaced);
00478 return *this;
00479 };
00480
00482 self diffConst(const self& rhs) const {
00483 return m_interfaced.DiffConst(rhs.m_interfaced);
00484 };
00485
00487 self& diffConstAssign(const self& rhs) {
00488 m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced);
00489 return *this;
00490 };
00491
00493 self intersect(const self& rhs) const {
00494 return m_interfaced.Intersect(rhs.m_interfaced);
00495 };
00496
00498 self& intersectAssign(const self& rhs) {
00499 m_interfaced = m_interfaced.Intersect(rhs.m_interfaced);
00500 return *this;
00501 };
00502
00504 self product(const self& rhs) const {
00505 return m_interfaced.Product(rhs.m_interfaced);
00506 };
00507
00509 self& productAssign(const self& rhs) {
00510 m_interfaced = m_interfaced.Product(rhs.m_interfaced);
00511 return *this;
00512 };
00513
00515 self unateProduct(const self& rhs) const {
00516 return m_interfaced.UnateProduct(rhs.m_interfaced);
00517 };
00518
00519
00520
00522 self dotProduct(const self& rhs) const {
00523 return interfaced_type(m_interfaced.manager(),
00524 Extra_zddDotProduct(
00525 manager().getManager(),
00526 m_interfaced.getNode(),
00527 rhs.m_interfaced.getNode()));
00528 }
00529
00530 self& dotProductAssign(const self& rhs){
00531 m_interfaced=interfaced_type(m_interfaced.manager(),
00532 Extra_zddDotProduct(
00533 manager().getManager(),
00534 m_interfaced.getNode(),
00535 rhs.m_interfaced.getNode()));
00536 return *this;
00537 }
00538
00539 self Xor(const self& rhs) const {
00540 if (rhs.emptiness())
00541 return *this;
00542 #ifdef PBORI_LOWLEVEL_XOR
00543 return interfaced_type(m_interfaced.manager(),
00544 pboriCudd_zddUnionXor(
00545 manager().getManager(),
00546 m_interfaced.getNode(),
00547 rhs.m_interfaced.getNode()));
00548 #else
00549 return interfaced_type(m_interfaced.manager(),
00550 Extra_zddUnionExor(
00551 manager().getManager(),
00552 m_interfaced.getNode(),
00553 rhs.m_interfaced.getNode()));
00554 #endif
00555 }
00556
00557
00559 self& unateProductAssign(const self& rhs) {
00560 m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced);
00561 return *this;
00562 };
00563
00565 self subset0(idx_type idx) const {
00566 return m_interfaced.Subset0(idx);
00567 };
00568
00570 self& subset0Assign(idx_type idx) {
00571 m_interfaced = m_interfaced.Subset0(idx);
00572 return *this;
00573 };
00574
00576 self subset1(idx_type idx) const {
00577 return m_interfaced.Subset1(idx);
00578 };
00579
00581 self& subset1Assign(idx_type idx) {
00582 m_interfaced = m_interfaced.Subset1(idx);
00583 return *this;
00584 };
00585
00587 self change(idx_type idx) const {
00588
00589 return m_interfaced.Change(idx);
00590 };
00591
00593 self& changeAssign(idx_type idx) {
00594 m_interfaced = m_interfaced.Change(idx);
00595 return *this;
00596 };
00597
00599 self ddDivide(const self& rhs) const {
00600 return m_interfaced.Divide(rhs);
00601 };
00602
00604 self& ddDivideAssign(const self& rhs) {
00605 m_interfaced = m_interfaced.Divide(rhs);
00606 return *this;
00607 };
00609 self weakDivide(const self& rhs) const {
00610 return m_interfaced.WeakDiv(rhs);
00611 };
00612
00614 self& weakDivideAssign(const self& rhs) {
00615 m_interfaced = m_interfaced.WeakDiv(rhs);
00616 return *this;
00617 };
00618
00620 self& divideFirstAssign(const self& rhs) {
00621
00622 PBoRiOutIter<self, idx_type, subset1_assign<self> > outiter(*this);
00623 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
00624
00625 return *this;
00626 }
00627
00629 self divideFirst(const self& rhs) const {
00630
00631 self result(*this);
00632 result.divideFirstAssign(rhs);
00633
00634 return result;
00635 }
00636
00637
00639 size_type nNodes() const {
00640 return Cudd_zddDagSize(m_interfaced.getNode());
00641 }
00642
00644 ostream_type& print(ostream_type& os) const {
00645
00646 FILE* oldstdout = manager().ReadStdout();
00647
00649 if (os == std::cout)
00650 manager().SetStdout(stdout);
00651 else if (os == std::cerr)
00652 manager().SetStdout(stderr);
00653
00654 m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) );
00655 m_interfaced.PrintMinterm();
00656
00657 manager().SetStdout(oldstdout);
00658 return os;
00659 }
00660
00662 void prettyPrint(pretty_out_type filehandle = stdout) const {
00663 DdNode* tmp = m_interfaced.getNode();
00664 Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp,
00665 NULL, NULL, filehandle);
00666 };
00667
00669 bool_type prettyPrint(filename_type filename) const {
00670
00671 FILE* theFile = fopen( filename, "w");
00672 if (theFile == NULL)
00673 return true;
00674
00675 prettyPrint(theFile);
00676 fclose(theFile);
00677
00678 return false;
00679 };
00680
00682 bool_type operator==(const self& rhs) const {
00683 return (m_interfaced == rhs.m_interfaced);
00684 }
00685
00687 bool_type operator!=(const self& rhs) const {
00688 return (m_interfaced != rhs.m_interfaced);
00689 }
00690
00692 mgr_ref manager() const {
00693 return get_manager(m_interfaced.manager());
00694 }
00695 core_type managerCore() const{
00696 return m_interfaced.manager();
00697 }
00699 size_type nSupport() const {
00700 return Cudd_SupportSize(manager().getManager(), m_interfaced.getNode());
00701 }
00702
00703 #if 1
00705 self support() const {
00706
00707
00708 DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode());
00709 Cudd_Ref(tmp);
00710
00711 self result = interfaced_type(m_interfaced.manager(),
00712 Cudd_zddPortFromBdd(manager().getManager(), tmp));
00713 Cudd_RecursiveDeref(manager().getManager(), tmp);
00714
00715
00716
00717 return result;
00718 }
00719 #endif
00720
00722 template<class VectorLikeType>
00723 void usedIndices(VectorLikeType& indices) const {
00724
00725 int* pIdx = Cudd_SupportIndex( manager().getManager(),
00726 m_interfaced.getNode() );
00727
00728
00729
00730 size_type nlen(nVariables());
00731
00732 indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type()));
00733
00734 for(size_type idx = 0; idx < nlen; ++idx)
00735 if (pIdx[idx] == 1){
00736 indices.push_back(idx);
00737 }
00738 FREE(pIdx);
00739 }
00740
00742 int* usedIndices() const {
00743
00744 return Cudd_SupportIndex( manager().getManager(),
00745 m_interfaced.getNode() );
00746
00747
00748 }
00749
00750
00752 first_iterator firstBegin() const {
00753 return first_iterator(navigation());
00754 }
00755
00757 first_iterator firstEnd() const {
00758 return first_iterator();
00759 }
00760
00762 last_iterator lastBegin() const {
00763 return last_iterator(m_interfaced.getNode());
00764 }
00765
00767 last_iterator lastEnd() const {
00768 return last_iterator();
00769 }
00770
00772 self firstMultiples(const std::vector<idx_type>& multipliers) const {
00773
00774 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00775
00776 std::copy( firstBegin(), firstEnd(), indices.begin() );
00777
00778 return cudd_generate_multiples( manager(),
00779 indices.rbegin(), indices.rend(),
00780 multipliers.rbegin(),
00781 multipliers.rend() );
00782 }
00783
00784
00785
00786 self subSet(const self& rhs) const {
00787
00788 return interfaced_type(m_interfaced.manager(),
00789 Extra_zddSubSet(manager().getManager(),
00790 m_interfaced.getNode(),
00791 rhs.m_interfaced.getNode()) );
00792 }
00793
00794 self supSet(const self& rhs) const {
00795
00796 return interfaced_type(m_interfaced.manager(),
00797 Extra_zddSupSet(manager().getManager(),
00798 m_interfaced.getNode(),
00799 rhs.m_interfaced.getNode()) );
00800 }
00802 self firstDivisors() const {
00803
00804 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00805
00806 std::copy( firstBegin(), firstEnd(), indices.begin() );
00807
00808 return cudd_generate_divisors(manager(), indices.rbegin(), indices.rend());
00809 }
00810
00812 navigator navigation() const {
00813 return navigator(m_interfaced.getNode());
00814 }
00815
00817 bool_type emptiness() const {
00818 return ( m_interfaced.getNode() == manager().zddZero().getNode() );
00819 }
00820
00822 bool_type blankness() const {
00823
00824 return ( m_interfaced.getNode() ==
00825 manager().zddOne( nVariables() ).getNode() );
00826
00827 }
00828
00829 bool_type isConstant() const {
00830 return (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode());
00831 }
00832
00834 size_type size() const {
00835 return m_interfaced.Count();
00836 }
00837
00839 size_type length() const {
00840 return size();
00841 }
00842
00844 size_type nVariables() const {
00845 return Cudd_ReadZddSize(manager().getManager() );
00846 }
00847
00848 self cofactor0(const self& rhs) const {
00849
00850 return interfaced_type(m_interfaced.manager(),
00851 Extra_zddCofactor0(manager().getManager(),
00852 m_interfaced.getNode(),
00853 rhs.m_interfaced.getNode()) );
00854 }
00855
00856 self cofactor1(const self& rhs, idx_type includeVars) const {
00857
00858 return interfaced_type(m_interfaced.manager(),
00859 Extra_zddCofactor1(manager().getManager(),
00860 m_interfaced.getNode(),
00861 rhs.m_interfaced.getNode(),
00862 includeVars) );
00863 }
00864
00866 bool_type ownsOne() const { return owns_one(navigation()); }
00867 double sizeDouble() const {
00868 return m_interfaced.CountDouble();
00869 }
00870
00872 self emptyElement() const {
00873 return manager().zddZero();
00874 }
00875
00877 self blankElement() const {
00878 return manager().zddOne();
00879 }
00880
00881 private:
00882 navigator newNode(const manager_base& mgr, idx_type idx,
00883 navigator thenNavi, navigator elseNavi) const {
00884 assert(idx < *thenNavi);
00885 assert(idx < *elseNavi);
00886 return navigator(cuddZddGetNode(mgr.getManager(), idx,
00887 thenNavi.getNode(), elseNavi.getNode()));
00888 }
00889
00890 interfaced_type newDiagram(const manager_base& mgr, navigator navi) const {
00891 return interfaced_type(extract_manager(mgr), navi.getNode());
00892 }
00893
00894 self fromTemporaryNode(const navigator& navi) const {
00895 navi.decRef();
00896 return self(manager(), navi.getNode());
00897 }
00898
00899
00900 interfaced_type newNodeDiagram(const manager_base& mgr, idx_type idx,
00901 navigator thenNavi,
00902 navigator elseNavi) const {
00903 if ((idx >= *thenNavi) || (idx >= *elseNavi))
00904 throw PBoRiGenericError<CTypes::invalid_ite>();
00905
00906 return newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) );
00907 }
00908
00909 interfaced_type newNodeDiagram(const manager_base& mgr,
00910 idx_type idx, navigator navi) const {
00911 if (idx >= *navi)
00912 throw PBoRiGenericError<CTypes::invalid_ite>();
00913
00914 navi.incRef();
00915 interfaced_type result =
00916 newDiagram(mgr, newNode(mgr, idx, navi, navi) );
00917 navi.decRef();
00918 return result;
00919 }
00920
00921
00922
00923 };
00924
00925
00926
00927
00928
00930 template <class DDType>
00931 typename CDDInterface<DDType>::ostream_type&
00932 operator<<( typename CDDInterface<DDType>::ostream_type& os,
00933 const CDDInterface<DDType>& dd ) {
00934 return dd.print(os);
00935 }
00936
00937 END_NAMESPACE_PBORI
00938
00939 #endif // of #ifndef CDDInterface_h_