PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00051 //***************************************************************************** 00052 00053 #ifndef CCuddCore_h 00054 #define CCuddCore_h 00055 00056 // include basic definitions 00057 #include "pbori_defs.h" 00058 00059 // intrisive (shared) pointer functionality 00060 #include <boost/intrusive_ptr.hpp> 00061 00062 // get PolyBoRi routines and functionals 00063 #include "pbori_func.h" 00064 #include "pbori_traits.h" 00065 00066 #include "CVariableNames.h" 00067 00068 #include <vector> 00069 #include "cuddInt.h" 00070 00071 BEGIN_NAMESPACE_PBORI 00072 00084 class CCuddCore { 00085 00086 public: 00088 PB_DECLARE_CUDD_TYPES(mgrcore_traits<Cudd>) 00089 00090 00091 typedef CCuddCore self; 00092 00094 typedef boost::intrusive_ptr<self> mgrcore_ptr; 00095 00097 typedef CVariableNames variable_names_type; 00098 00100 typedef variable_names_type::const_reference const_varname_reference; 00101 00103 mgrcore_type manager; 00104 00106 static errorfunc_type errorHandler; 00107 00109 static bool verbose; 00110 00112 refcount_type ref; 00113 00115 variable_names_type m_names; 00116 00117 std::vector<node_type> m_vars; 00118 00119 00121 CCuddCore(size_type numVars = 0, 00122 size_type numVarsZ = 0, 00123 size_type numSlots = CUDD_UNIQUE_SLOTS, 00124 size_type cacheSize = CUDD_CACHE_SLOTS, 00125 large_size_type maxMemory = 0): 00126 ref(0), m_names(numVarsZ), m_vars(numVarsZ) { 00127 manager = Cudd_Init(numVars,numVarsZ,numSlots,cacheSize,maxMemory); 00128 00129 00130 for (unsigned idx = 0 ; idx < numVarsZ; ++idx) { 00131 m_vars[idx] = cuddUniqueInterZdd(manager, idx, DD_ONE(manager), 00132 DD_ZERO(manager)); 00133 Cudd_Ref(m_vars[idx]); 00134 } 00135 00136 } 00137 00139 ~CCuddCore(){ 00140 00141 for (std::vector<node_type>::iterator iter = m_vars.begin(); iter != 00142 m_vars.end(); ++iter) { 00143 00144 Cudd_RecursiveDerefZdd(manager, *iter); 00145 } 00146 00147 int retval = Cudd_CheckZeroRef(manager); 00148 // Check for unexpected non-zero reference counts 00149 assert(retval == 0); 00150 00151 Cudd_Quit(manager); 00152 } 00153 00155 void addRef(){ ++ref; } 00156 00158 refcount_type release() { 00159 return (--ref); 00160 } 00161 }; 00162 00164 00165 00166 inline void 00167 intrusive_ptr_add_ref(CCuddCore* pCore){ 00168 pCore->addRef(); 00169 } 00170 00172 inline void 00173 intrusive_ptr_release(CCuddCore* pCore) { 00174 if (!(pCore->release())) { 00175 delete pCore; 00176 } 00177 } 00179 00180 END_NAMESPACE_PBORI 00181 00182 #endif 00183 00184