CDDInterface.h

Go to the documentation of this file.

// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************

#ifndef CDDInterface_h_
#define CDDInterface_h_

#include "extrafwd.h"
// load basic definitions
#include "pbori_defs.h"



// Getting iterator type for navigating through Cudd's ZDDs structure
#include "CCuddNavigator.h"

// Getting iterator type for retrieving first term from Cudd's ZDDs
#include "CCuddFirstIter.h"

// Getting iterator type for retrieving last term from Cudd's ZDDs
#include "CCuddLastIter.h"

// Getting functional for generating new Cudd's ZDD nodes
#include "CCuddGetNode.h"

// Getting output iterator functionality
#include "PBoRiOutIter.h"

// Getting error coe functionality
#include "PBoRiGenericError.h"

// Cudd's internal definitions
#include "cuddInt.h"

#include "pbori_algo.h"

#include "pbori_tags.h"
#include "pbori_routines_hash.h"

// Using stl's vector
#include <vector>
#include <numeric>

#include "CCuddInterface.h"
#include "pbori_traits.h"

BEGIN_NAMESPACE_PBORI


inline Cudd*
extract_manager(const Cudd& mgr) {
  return &const_cast<Cudd&>(mgr);
}

inline CCuddInterface::mgrcore_ptr
extract_manager(const CCuddInterface& mgr) {
  return mgr.managerCore();
}

template <class MgrType>
inline const MgrType&
extract_manager(const MgrType& mgr) {
  return mgr;
}

inline Cudd&
get_manager(Cudd* mgr) {
  return *mgr;
}

template <class MgrType>
inline const MgrType&
get_manager(const MgrType& mgr) {
  return mgr;
}
template<class DDType>
class CDDInterfaceBase {

 public:

  typedef DDType interfaced_type;

  typedef CDDInterfaceBase<interfaced_type> self;

  CDDInterfaceBase() :
    m_interfaced() {}

  CDDInterfaceBase(const interfaced_type& interfaced) :
    m_interfaced(interfaced) {}

  CDDInterfaceBase(const self& rhs) :
    m_interfaced(rhs.m_interfaced) {}

  ~CDDInterfaceBase() {}

  operator const interfaced_type&() const { return m_interfaced; }

 protected:
  interfaced_type m_interfaced;
};

template<class CuddLikeZDD>
class CDDInterface:
 public CDDInterfaceBase<CuddLikeZDD> {
 public:
  
  typedef CuddLikeZDD interfaced_type;
  
  typedef typename zdd_traits<interfaced_type>::manager_base manager_base;

  typedef typename manager_traits<manager_base>::tmp_ref mgr_ref;

  typedef typename manager_traits<manager_base>::core_type core_type;

  typedef CDDManager<CCuddInterface> manager_type;

  typedef CDDInterfaceBase<interfaced_type> base_type;
  typedef base_type base;
  using base::m_interfaced;

  typedef CDDInterface<interfaced_type> self;

  typedef CTypes::size_type size_type;

  typedef CTypes::idx_type idx_type;

  typedef CTypes::ostream_type ostream_type;

  typedef CTypes::bool_type bool_type;

  typedef CTypes::hash_type hash_type;

  typedef CCuddFirstIter first_iterator;

  typedef CCuddLastIter last_iterator;

  typedef CCuddNavigator navigator;

  typedef FILE* pretty_out_type;

  typedef const char* filename_type;

  typedef valid_tag easy_equality_property;

  CDDInterface(): base_type() {}

  CDDInterface(const self& rhs): base_type(rhs) {}

  CDDInterface(const interfaced_type& rhs): base_type(rhs) {}

  CDDInterface(const manager_base& mgr, const navigator& navi): 
    base_type(self::newDiagram(mgr, navi)) {}

  CDDInterface(const manager_base& mgr, 
               idx_type idx, navigator thenNavi, navigator elseNavi): 
    base_type( self::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) {
  }

  CDDInterface(const manager_base& mgr, 
               idx_type idx, navigator navi): 
    base_type( self::newNodeDiagram(mgr, idx, navi, navi) ) {
  }

  CDDInterface(idx_type idx, const self& thenDD, const self& elseDD): 
    base_type( self::newNodeDiagram(thenDD.manager(), idx, 
                                    thenDD.navigation(), 
                                    elseDD.navigation()) ) {
  }

  ~CDDInterface() {}

  hash_type hash() const { 
    return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t>(m_interfaced
                                                                   .getNode()));
  }

  hash_type stableHash() const { 
    return stable_hash_range(navigation());
  }

  self unite(const self& rhs) const {
    return self(base_type(m_interfaced.Union(rhs.m_interfaced)));
  };

  self& uniteAssign(const self& rhs) {
    m_interfaced = m_interfaced.Union(rhs.m_interfaced);
    return *this;
  };
  self ite(const self& then_dd, const self& else_dd) const {
    return self(m_interfaced.Ite(then_dd, else_dd));
  };

  self& iteAssign(const self& then_dd, const self& else_dd) {
    m_interfaced = m_interfaced.Ite(then_dd, else_dd);
    return *this;
  };

  self diff(const self& rhs) const {
    return m_interfaced.Diff(rhs.m_interfaced);
  };

  self& diffAssign(const self& rhs) {
    m_interfaced = m_interfaced.Diff(rhs.m_interfaced);
    return *this;
  };

  self diffConst(const self& rhs) const {
    return m_interfaced.DiffConst(rhs.m_interfaced);
  };

  self& diffConstAssign(const self& rhs) {
    m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced);
    return *this;
  };

  self intersect(const self& rhs) const {
    return m_interfaced.Intersect(rhs.m_interfaced);
  };

  self& intersectAssign(const self& rhs) {
    m_interfaced = m_interfaced.Intersect(rhs.m_interfaced);
    return *this;
  };

  self product(const self& rhs) const {
    return m_interfaced.Product(rhs.m_interfaced);
  };

  self& productAssign(const self& rhs) {
    m_interfaced = m_interfaced.Product(rhs.m_interfaced);
    return *this;
  };

  self unateProduct(const self& rhs) const {
    return m_interfaced.UnateProduct(rhs.m_interfaced);
  };



  self dotProduct(const self& rhs) const {
        return interfaced_type(m_interfaced.manager(),
            Extra_zddDotProduct(
                manager().getManager(),
                m_interfaced.getNode(),
                rhs.m_interfaced.getNode()));
  }
  
  self& dotProductAssign(const self& rhs){
        m_interfaced=interfaced_type(m_interfaced.manager(),
            Extra_zddDotProduct(
                manager().getManager(),
                m_interfaced.getNode(),
                rhs.m_interfaced.getNode()));
        return *this;
  }

  self Xor(const self& rhs) const {
    if (rhs.emptiness())
      return *this;
#ifdef PBORI_LOWLEVEL_XOR
    return interfaced_type(m_interfaced.manager(),
            pboriCudd_zddUnionXor(
                manager().getManager(),
                m_interfaced.getNode(),
                rhs.m_interfaced.getNode()));
#else
        return interfaced_type(m_interfaced.manager(),
            Extra_zddUnionExor(
                manager().getManager(),
                m_interfaced.getNode(),
                rhs.m_interfaced.getNode()));
#endif
  }

  
  self& unateProductAssign(const self& rhs) {
    m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced);
    return *this;
  };

  self subset0(idx_type idx) const {
    return m_interfaced.Subset0(idx);
  };

  self& subset0Assign(idx_type idx) {
    m_interfaced = m_interfaced.Subset0(idx);
    return *this;
  };

  self subset1(idx_type idx) const {
    return m_interfaced.Subset1(idx);
  };

  self& subset1Assign(idx_type idx) {
    m_interfaced = m_interfaced.Subset1(idx);
    return *this;
  };

  self change(idx_type idx) const {    

    return m_interfaced.Change(idx);
  };

  self& changeAssign(idx_type idx) {
    m_interfaced = m_interfaced.Change(idx);
    return *this;
  };

  self ddDivide(const self& rhs) const {
    return m_interfaced.Divide(rhs);
  };

  self& ddDivideAssign(const self& rhs) {
    m_interfaced = m_interfaced.Divide(rhs);
    return *this;
  };
  self weakDivide(const self& rhs) const {
    return m_interfaced.WeakDiv(rhs);
  };

  self& weakDivideAssign(const self& rhs) {
    m_interfaced = m_interfaced.WeakDiv(rhs);
    return *this;
  };

  self& divideFirstAssign(const self& rhs) {

    PBoRiOutIter<self, idx_type, subset1_assign<self> >  outiter(*this);
    std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);

    return *this;
  }

  self divideFirst(const self& rhs) const {

    self result(*this);
    result.divideFirstAssign(rhs);

    return result;
  }


  size_type nNodes() const {
    return Cudd_zddDagSize(m_interfaced.getNode());
  }

  ostream_type& print(ostream_type& os) const {

    FILE* oldstdout = manager().ReadStdout();

    if (os == std::cout)
      manager().SetStdout(stdout);
    else if (os == std::cerr)
      manager().SetStdout(stderr);

    m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) );
    m_interfaced.PrintMinterm();

    manager().SetStdout(oldstdout);
    return os;
  }

  void prettyPrint(pretty_out_type filehandle = stdout) const {
    DdNode* tmp = m_interfaced.getNode();
    Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp, 
                    NULL, NULL, filehandle);
  };

  bool_type prettyPrint(filename_type filename) const {

    FILE* theFile = fopen( filename, "w");
    if (theFile == NULL)
      return true;

    prettyPrint(theFile);
    fclose(theFile);

    return false;
 };

  bool_type operator==(const self& rhs) const {
    return (m_interfaced == rhs.m_interfaced);
  }

  bool_type operator!=(const self& rhs) const {
    return (m_interfaced != rhs.m_interfaced);
  }

  mgr_ref manager() const {
    return get_manager(m_interfaced.manager());
  }
  core_type managerCore() const{
    return m_interfaced.manager();
  }
  size_type nSupport() const {
    return Cudd_SupportSize(manager().getManager(), m_interfaced.getNode());
  }

#if 1
  self support() const {

//    BDD supp( &manager(), 
    DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode());
    Cudd_Ref(tmp);
 
    self result = interfaced_type(m_interfaced.manager(),  
      Cudd_zddPortFromBdd(manager().getManager(), tmp));
    Cudd_RecursiveDeref(manager().getManager(), tmp);        
//    return supp.PortToZdd();

//    assert(false);
    return result;
  }
#endif

  template<class VectorLikeType>
  void usedIndices(VectorLikeType& indices) const {

    int* pIdx = Cudd_SupportIndex( manager().getManager(), 
                                   m_interfaced.getNode() );



    size_type nlen(nVariables());

    indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type()));

    for(size_type idx = 0; idx < nlen; ++idx)
      if (pIdx[idx] == 1){
        indices.push_back(idx);
      }
    FREE(pIdx);
  }

  int* usedIndices() const {

    return Cudd_SupportIndex( manager().getManager(), 
                                   m_interfaced.getNode() );


  }


  first_iterator firstBegin() const {
    return first_iterator(m_interfaced.getNode());
  }

  first_iterator firstEnd() const { 
    return first_iterator();
  }

  last_iterator lastBegin() const {
    return last_iterator(m_interfaced.getNode());
  }

  last_iterator lastEnd() const { 
    return last_iterator();
  }

  self firstMultiples(const std::vector<idx_type>& multipliers) const {

    std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );

    std::copy( firstBegin(), firstEnd(), indices.begin() );

    return cudd_generate_multiples( manager(),
                                    indices.rbegin(), indices.rend(),
                                    multipliers.rbegin(),
                                    multipliers.rend() );
  }



  self subSet(const self& rhs) const {

    return interfaced_type(m_interfaced.manager(),
            Extra_zddSubSet(manager().getManager(), 
                                   m_interfaced.getNode(), 
                                   rhs.m_interfaced.getNode()) );
  }
  
  self supSet(const self& rhs) const {

    return interfaced_type(m_interfaced.manager(),
            Extra_zddSupSet(manager().getManager(), 
                                   m_interfaced.getNode(), 
                                   rhs.m_interfaced.getNode()) );
  }
  self firstDivisors() const {

    std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );

    std::copy( firstBegin(), firstEnd(), indices.begin() );

    return cudd_generate_divisors(manager(), indices.rbegin(), indices.rend());
  }

  navigator navigation() const {
    return navigator(m_interfaced.getNode());
  }

  bool_type emptiness() const {
    return ( m_interfaced.getNode() == manager().zddZero().getNode() );
  }

  bool_type blankness() const {

    return ( m_interfaced.getNode() == 
             manager().zddOne( nVariables() ).getNode() );

  }

  bool_type isConstant() const {
    return (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode());
  }

  size_type size() const {
    return m_interfaced.Count();
  }

  size_type length() const {
    return size();
  }

  size_type nVariables() const {
   return Cudd_ReadZddSize(manager().getManager() );
  }

  self minimalElements() const {
        return interfaced_type(m_interfaced.manager(),
            Extra_zddMinimal(manager().getManager(),m_interfaced.getNode()));
  }

  self cofactor0(const self& rhs) const {

    return interfaced_type(m_interfaced.manager(),
            Extra_zddCofactor0(manager().getManager(), 
                               m_interfaced.getNode(), 
                               rhs.m_interfaced.getNode()) );
  }

  self cofactor1(const self& rhs, idx_type includeVars) const {

    return interfaced_type(m_interfaced.manager(),
            Extra_zddCofactor1(manager().getManager(), 
                               m_interfaced.getNode(), 
                               rhs.m_interfaced.getNode(),
                               includeVars) );
  }

  bool_type ownsOne() const {
    navigator navi(navigation());

    while (!navi.isConstant() )
      navi.incrementElse();
    
    return navi.terminalValue();
  }
  double sizeDouble() const {
    return m_interfaced.CountDouble();
  }

  self emptyElement() const {
    return manager().zddZero();
  }

  self blankElement() const {
    return manager().zddOne();
  }

private:
  navigator newNode(const manager_base& mgr, idx_type idx, 
                    navigator thenNavi, navigator elseNavi) const {
    assert(idx < *thenNavi);
    assert(idx < *elseNavi); 
    return navigator(cuddZddGetNode(mgr.getManager(), idx, 
                                    thenNavi.getNode(), elseNavi.getNode()));
  }

  interfaced_type newDiagram(const manager_base& mgr, navigator navi) const { 
    return interfaced_type(extract_manager(mgr), navi.getNode());
  }

  self fromTemporaryNode(const navigator& navi) const { 
    navi.decRef();
    return self(manager(), navi.getNode());
  }


  interfaced_type newNodeDiagram(const manager_base& mgr, idx_type idx, 
                                 navigator thenNavi, 
                                 navigator elseNavi) const {
    if ((idx >= *thenNavi) || (idx >= *elseNavi))
      throw PBoRiGenericError<CTypes::invalid_ite>();

    return newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) );
  }

  interfaced_type newNodeDiagram(const manager_base& mgr, 
                                 idx_type idx, navigator navi) const {
    if (idx >= *navi)
      throw PBoRiGenericError<CTypes::invalid_ite>();

    navi.incRef();
    interfaced_type result =
      newDiagram(mgr, newNode(mgr, idx, navi, navi) );
    navi.decRef();
    return result;
  }



};





template <class DDType>
typename CDDInterface<DDType>::ostream_type& 
operator<<( typename CDDInterface<DDType>::ostream_type& os, 
            const CDDInterface<DDType>& dd ) {
  return dd.print(os);
}

END_NAMESPACE_PBORI

#endif // of #ifndef CDDInterface_h_

---