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