CCuddCore.h

Go to the documentation of this file.

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

#ifndef CCuddCore_h
#define CCuddCore_h

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

// intrisive (shared) pointer functionality
#include <boost/intrusive_ptr.hpp>

// get PolyBoRi routines and functionals
#include "pbori_func.h"
#include "pbori_traits.h"

#include "CVariableNames.h"

#include <vector>
#include "cuddInt.h"

BEGIN_NAMESPACE_PBORI

class CCuddCore {

public:
  PB_DECLARE_CUDD_TYPES(mgrcore_traits<Cudd>)

  
  typedef CCuddCore self;

  typedef boost::intrusive_ptr<self> mgrcore_ptr;

  typedef CVariableNames variable_names_type;

  typedef variable_names_type::const_reference const_varname_reference;

  mgrcore_type manager;

  static errorfunc_type errorHandler;

  static bool verbose;

  refcount_type ref;

  variable_names_type m_names;

  std::vector<node_type> m_vars;

  CCuddCore(size_type numVars = 0,
            size_type numVarsZ = 0,
            size_type numSlots = CUDD_UNIQUE_SLOTS,
            size_type cacheSize = CUDD_CACHE_SLOTS,
            large_size_type maxMemory = 0):  
    ref(0), m_names(numVarsZ), m_vars(numVarsZ) {
    manager = Cudd_Init(numVars,numVarsZ,numSlots,cacheSize,maxMemory);


    for (unsigned idx = 0 ; idx < numVarsZ; ++idx) {
      m_vars[idx] = cuddUniqueInterZdd(manager, idx, DD_ONE(manager),
                                       DD_ZERO(manager)); 
      Cudd_Ref(m_vars[idx]);
    }

  }

  ~CCuddCore(){ release(); }

  void addRef(){ ++ref; }

  void release() {
    if (--(ref) == 0){
      for (std::vector<node_type>::iterator iter = m_vars.begin();  iter !=
             m_vars.end(); ++iter) {
        
        Cudd_RecursiveDerefZdd(manager, *iter);
    }


      int retval = Cudd_CheckZeroRef(manager);
      if UNLIKELY(retval != 0) {
        std::cerr << retval << " unexpected non-zero reference counts\n";
      } else if (verbose) {
        std::cerr << "All went well\n";
      }
      Cudd_Quit(manager);
    }
  }
};



inline void 
intrusive_ptr_add_ref(CCuddCore* pCore){
  pCore->addRef();
}

inline void 
intrusive_ptr_release(CCuddCore* pCore) {
  pCore->release();
}

END_NAMESPACE_PBORI

#endif

---