PolyBoRi
CDDInterface.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
220 //*****************************************************************************
221 
222 #ifndef CDDInterface_h_
223 #define CDDInterface_h_
224 
225 #include "extrafwd.h"
226 // load basic definitions
227 #include "pbori_defs.h"
228 
229 
230 
231 // Getting iterator type for navigating through Cudd's ZDDs structure
232 #include "CCuddNavigator.h"
233 
234 // Getting iterator type for retrieving first term from Cudd's ZDDs
235 #include "CCuddFirstIter.h"
236 
237 // Getting iterator type for retrieving last term from Cudd's ZDDs
238 #include "CCuddLastIter.h"
239 
240 // Getting functional for generating new Cudd's ZDD nodes
241 #include "CCuddGetNode.h"
242 
243 // Getting output iterator functionality
244 #include "PBoRiOutIter.h"
245 
246 // Getting error coe functionality
247 #include "PBoRiGenericError.h"
248 
249 // Cudd's internal definitions
250 #include "cuddInt.h"
251 
252 #include "pbori_algo.h"
253 
254 #include "pbori_tags.h"
255 #include "pbori_routines_hash.h"
256 
257 // Using stl's vector
258 #include <vector>
259 #include <numeric>
260 
261 #include "CCuddInterface.h"
262 #include "pbori_traits.h"
263 
265 
266 
267 inline Cudd*
268 extract_manager(const Cudd& mgr) {
269  return &const_cast<Cudd&>(mgr);
270 }
271 
272 inline CCuddInterface::mgrcore_ptr
274  return mgr.managerCore();
275 }
276 
277 template <class MgrType>
278 inline const MgrType&
279 extract_manager(const MgrType& mgr) {
280  return mgr;
281 }
282 
283 inline Cudd&
284 get_manager(Cudd* mgr) {
285  return *mgr;
286 }
287 
288 template <class MgrType>
289 inline const MgrType&
290 get_manager(const MgrType& mgr) {
291  return mgr;
292 }
300 template<class DDType>
302 
303  public:
304 
306  typedef DDType interfaced_type;
307 
310 
313  m_interfaced() {}
314 
316  CDDInterfaceBase(const interfaced_type& interfaced) :
317  m_interfaced(interfaced) {}
318 
320  CDDInterfaceBase(const self& rhs) :
321  m_interfaced(rhs.m_interfaced) {}
322 
325 
327  operator const interfaced_type&() const { return m_interfaced; }
328 
329  protected:
331 };
332 
335 template<class CuddLikeZDD>
337  public CDDInterfaceBase<CuddLikeZDD> {
338  public:
339 
341  typedef CuddLikeZDD interfaced_type;
342 
344  typedef typename zdd_traits<interfaced_type>::manager_base manager_base;
345 
348 
351 
354 
357  typedef base_type base;
358  using base::m_interfaced;
359 
362 
365 
368 
371 
374 
377 
380 
383 
386 
388  typedef FILE* pretty_out_type;
389 
391  typedef const char* filename_type;
392 
395 
398 
400  CDDInterface(const self& rhs): base_type(rhs) {}
401 
404 
406  CDDInterface(const manager_base& mgr, const navigator& navi):
407  base_type(self::newDiagram(mgr, navi)) {}
408 
411  idx_type idx, navigator thenNavi, navigator elseNavi):
412  base_type( self::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) {
413  }
414 
418  idx_type idx, navigator navi):
419  base_type( self::newNodeDiagram(mgr, idx, navi, navi) ) {
420  }
421 
423  CDDInterface(idx_type idx, const self& thenDD, const self& elseDD):
424  base_type( self::newNodeDiagram(thenDD.manager(), idx,
425  thenDD.navigation(),
426  elseDD.navigation()) ) {
427  }
428 
431 
433  hash_type hash() const {
434  return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t>(m_interfaced
435  .getNode()));
436  }
437 
440  return stable_hash_range(navigation());
441  }
442 
444  self unite(const self& rhs) const {
445  return self(base_type(m_interfaced.Union(rhs.m_interfaced)));
446  };
447 
449  self& uniteAssign(const self& rhs) {
450  m_interfaced = m_interfaced.Union(rhs.m_interfaced);
451  return *this;
452  };
454  self ite(const self& then_dd, const self& else_dd) const {
455  return self(m_interfaced.Ite(then_dd, else_dd));
456  };
457 
459  self& iteAssign(const self& then_dd, const self& else_dd) {
460  m_interfaced = m_interfaced.Ite(then_dd, else_dd);
461  return *this;
462  };
463 
465  self diff(const self& rhs) const {
466  return m_interfaced.Diff(rhs.m_interfaced);
467  };
468 
470  self& diffAssign(const self& rhs) {
471  m_interfaced = m_interfaced.Diff(rhs.m_interfaced);
472  return *this;
473  };
474 
476  self diffConst(const self& rhs) const {
477  return m_interfaced.DiffConst(rhs.m_interfaced);
478  };
479 
481  self& diffConstAssign(const self& rhs) {
482  m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced);
483  return *this;
484  };
485 
487  self intersect(const self& rhs) const {
488  return m_interfaced.Intersect(rhs.m_interfaced);
489  };
490 
492  self& intersectAssign(const self& rhs) {
493  m_interfaced = m_interfaced.Intersect(rhs.m_interfaced);
494  return *this;
495  };
496 
498  self product(const self& rhs) const {
499  return m_interfaced.Product(rhs.m_interfaced);
500  };
501 
503  self& productAssign(const self& rhs) {
504  m_interfaced = m_interfaced.Product(rhs.m_interfaced);
505  return *this;
506  };
507 
509  self unateProduct(const self& rhs) const {
510  return m_interfaced.UnateProduct(rhs.m_interfaced);
511  };
512 
513 
514 
516  self dotProduct(const self& rhs) const {
517  return interfaced_type(m_interfaced.manager(),
519  manager().getManager(),
520  m_interfaced.getNode(),
521  rhs.m_interfaced.getNode()));
522  }
523 
524  self& dotProductAssign(const self& rhs){
525  m_interfaced=interfaced_type(m_interfaced.manager(),
527  manager().getManager(),
528  m_interfaced.getNode(),
529  rhs.m_interfaced.getNode()));
530  return *this;
531  }
532 
533  self Xor(const self& rhs) const {
534  if (rhs.emptiness())
535  return *this;
536 #ifdef PBORI_LOWLEVEL_XOR
537  return interfaced_type(m_interfaced.manager(),
539  manager().getManager(),
540  m_interfaced.getNode(),
541  rhs.m_interfaced.getNode()));
542 #else
543  return interfaced_type(m_interfaced.manager(),
545  manager().getManager(),
546  m_interfaced.getNode(),
547  rhs.m_interfaced.getNode()));
548 #endif
549  }
550 
551 
553  self& unateProductAssign(const self& rhs) {
554  m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced);
555  return *this;
556  };
557 
559  self subset0(idx_type idx) const {
560  return m_interfaced.Subset0(idx);
561  };
562 
564  self& subset0Assign(idx_type idx) {
565  m_interfaced = m_interfaced.Subset0(idx);
566  return *this;
567  };
568 
570  self subset1(idx_type idx) const {
571  return m_interfaced.Subset1(idx);
572  };
573 
575  self& subset1Assign(idx_type idx) {
576  m_interfaced = m_interfaced.Subset1(idx);
577  return *this;
578  };
579 
581  self change(idx_type idx) const {
582 
583  return m_interfaced.Change(idx);
584  };
585 
587  self& changeAssign(idx_type idx) {
588  m_interfaced = m_interfaced.Change(idx);
589  return *this;
590  };
591 
593  self ddDivide(const self& rhs) const {
594  return m_interfaced.Divide(rhs);
595  };
596 
598  self& ddDivideAssign(const self& rhs) {
599  m_interfaced = m_interfaced.Divide(rhs);
600  return *this;
601  };
603  self weakDivide(const self& rhs) const {
604  return m_interfaced.WeakDiv(rhs);
605  };
606 
608  self& weakDivideAssign(const self& rhs) {
609  m_interfaced = m_interfaced.WeakDiv(rhs);
610  return *this;
611  };
612 
614  self& divideFirstAssign(const self& rhs) {
615 
617  std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
618 
619  return *this;
620  }
621 
623  self divideFirst(const self& rhs) const {
624 
625  self result(*this);
626  result.divideFirstAssign(rhs);
627 
628  return result;
629  }
630 
631 
633  size_type nNodes() const {
634  return Cudd_zddDagSize(m_interfaced.getNode());
635  }
636 
639 
640  FILE* oldstdout = manager().ReadStdout();
641 
643  if (os == std::cout)
644  manager().SetStdout(stdout);
645  else if (os == std::cerr)
646  manager().SetStdout(stderr);
647 
648  m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) );
649  m_interfaced.PrintMinterm();
650 
651  manager().SetStdout(oldstdout);
652  return os;
653  }
654 
656  void prettyPrint(pretty_out_type filehandle = stdout) const {
657  DdNode* tmp = m_interfaced.getNode();
658  Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp,
659  NULL, NULL, filehandle);
660  };
661 
664 
665  FILE* theFile = fopen( filename, "w");
666  if (theFile == NULL)
667  return true;
668 
669  prettyPrint(theFile);
670  fclose(theFile);
671 
672  return false;
673  };
674 
676  bool_type operator==(const self& rhs) const {
677  return (m_interfaced == rhs.m_interfaced);
678  }
679 
681  bool_type operator!=(const self& rhs) const {
682  return (m_interfaced != rhs.m_interfaced);
683  }
684 
686  mgr_ref manager() const {
687  return get_manager(m_interfaced.manager());
688  }
690  return m_interfaced.manager();
691  }
693  size_type nSupport() const {
694  return Cudd_SupportSize(manager().getManager(), m_interfaced.getNode());
695  }
696 
697 #if 1
698 
699  self support() const {
700 
701 // BDD supp( &manager(),
702  DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode());
703  Cudd_Ref(tmp);
704 
705  self result = interfaced_type(m_interfaced.manager(),
706  Cudd_zddPortFromBdd(manager().getManager(), tmp));
707  Cudd_RecursiveDeref(manager().getManager(), tmp);
708 // return supp.PortToZdd();
709 
710 // assert(false);
711  return result;
712  }
713 #endif
714 
716  template<class VectorLikeType>
717  void usedIndices(VectorLikeType& indices) const {
718 
719  int* pIdx = Cudd_SupportIndex( manager().getManager(),
720  m_interfaced.getNode() );
721 
722 
723 
724  size_type nlen(nVariables());
725 
726  indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type()));
727 
728  for(size_type idx = 0; idx < nlen; ++idx)
729  if (pIdx[idx] == 1){
730  indices.push_back(idx);
731  }
732  FREE(pIdx);
733  }
734 
736  int* usedIndices() const {
737 
738  return Cudd_SupportIndex( manager().getManager(),
739  m_interfaced.getNode() );
740 
741 
742  }
743 
744 
747  return first_iterator(navigation());
748  }
749 
752  return first_iterator();
753  }
754 
757  return last_iterator(m_interfaced.getNode());
758  }
759 
762  return last_iterator();
763  }
764 
766  self firstMultiples(const std::vector<idx_type>& multipliers) const {
767 
768  std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
769 
770  std::copy( firstBegin(), firstEnd(), indices.begin() );
771 
772  return cudd_generate_multiples( manager(),
773  indices.rbegin(), indices.rend(),
774  multipliers.rbegin(),
775  multipliers.rend() );
776  }
777 
778 
779 
780  self subSet(const self& rhs) const {
781 
782  return interfaced_type(m_interfaced.manager(),
783  Extra_zddSubSet(manager().getManager(),
784  m_interfaced.getNode(),
785  rhs.m_interfaced.getNode()) );
786  }
787 
788  self supSet(const self& rhs) const {
789 
790  return interfaced_type(m_interfaced.manager(),
791  Extra_zddSupSet(manager().getManager(),
792  m_interfaced.getNode(),
793  rhs.m_interfaced.getNode()) );
794  }
796  self firstDivisors() const {
797 
798  std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
799 
800  std::copy( firstBegin(), firstEnd(), indices.begin() );
801 
802  return cudd_generate_divisors(manager(), indices.rbegin(), indices.rend());
803  }
804 
807  return navigator(m_interfaced.getNode());
808  }
809 
812  return ( m_interfaced.getNode() == manager().zddZero().getNode() );
813  }
814 
817 
818  return ( m_interfaced.getNode() ==
819  manager().zddOne( nVariables() ).getNode() );
820 
821  }
822 
824  return (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode());
825  }
826 
828  size_type size() const {
829  return m_interfaced.Count();
830  }
831 
833  size_type length() const {
834  return size();
835  }
836 
839  return Cudd_ReadZddSize(manager().getManager() );
840  }
841 
843  self minimalElements() const {
844  return interfaced_type(m_interfaced.manager(),
845  Extra_zddMinimal(manager().getManager(),m_interfaced.getNode()));
846  }
847 
848  self cofactor0(const self& rhs) const {
849 
850  return interfaced_type(m_interfaced.manager(),
851  Extra_zddCofactor0(manager().getManager(),
852  m_interfaced.getNode(),
853  rhs.m_interfaced.getNode()) );
854  }
855 
856  self cofactor1(const self& rhs, idx_type includeVars) const {
857 
858  return interfaced_type(m_interfaced.manager(),
859  Extra_zddCofactor1(manager().getManager(),
860  m_interfaced.getNode(),
861  rhs.m_interfaced.getNode(),
862  includeVars) );
863  }
864 
866  bool_type ownsOne() const {
867  navigator navi(navigation());
868 
869  while (!navi.isConstant() )
870  navi.incrementElse();
871 
872  return navi.terminalValue();
873  }
874  double sizeDouble() const {
875  return m_interfaced.CountDouble();
876  }
877 
879  self emptyElement() const {
880  return manager().zddZero();
881  }
882 
884  self blankElement() const {
885  return manager().zddOne();
886  }
887 
888 private:
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()));
895  }
896 
897  interfaced_type newDiagram(const manager_base& mgr, navigator navi) const {
898  return interfaced_type(extract_manager(mgr), navi.getNode());
899  }
900 
901  self fromTemporaryNode(const navigator& navi) const {
902  navi.decRef();
903  return self(manager(), navi.getNode());
904  }
905 
906 
907  interfaced_type newNodeDiagram(const manager_base& mgr, idx_type idx,
908  navigator thenNavi,
909  navigator elseNavi) const {
910  if ((idx >= *thenNavi) || (idx >= *elseNavi))
911  throw PBoRiGenericError<CTypes::invalid_ite>();
912 
913  return newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) );
914  }
915 
916  interfaced_type newNodeDiagram(const manager_base& mgr,
917  idx_type idx, navigator navi) const {
918  if (idx >= *navi)
919  throw PBoRiGenericError<CTypes::invalid_ite>();
920 
921  navi.incRef();
922  interfaced_type result =
923  newDiagram(mgr, newNode(mgr, idx, navi, navi) );
924  navi.decRef();
925  return result;
926  }
927 
928 
929 
930 };
931 
932 
933 
934 
935 
937 template <class DDType>
938 typename CDDInterface<DDType>::ostream_type&
939 operator<<( typename CDDInterface<DDType>::ostream_type& os,
940  const CDDInterface<DDType>& dd ) {
941  return dd.print(os);
942 }
943 
945 
946 #endif // of #ifndef CDDInterface_h_