00001
00002
00054
00055
00056 #ifndef CCuddCore_h
00057 #define CCuddCore_h
00058
00059
00060 #include "pbori_defs.h"
00061
00062
00063 #include <boost/intrusive_ptr.hpp>
00064
00065
00066 #include "pbori_func.h"
00067 #include "pbori_traits.h"
00068
00069 #include "CVariableNames.h"
00070
00071 #include <vector>
00072 #include "cuddInt.h"
00074 inline void
00075 intrusive_ptr_add_ref(DdManager* ptr){
00076 ++(ptr->hooks);
00077 }
00078
00080 inline void
00081 intrusive_ptr_release(DdManager* ptr) {
00082 if (!(--(ptr->hooks))) {
00083 int retval = Cudd_CheckZeroRef(ptr);
00084
00085 assert(retval == 0);
00086
00087 Cudd_Quit(ptr);
00088 }
00089 }
00090
00091 BEGIN_NAMESPACE_PBORI
00092
00093
00105 class CCuddCore {
00106
00107 public:
00109 PB_DECLARE_CUDD_TYPES(mgrcore_traits<Cudd>)
00110
00111
00112 typedef CCuddCore self;
00113
00115 typedef boost::intrusive_ptr<self> mgrcore_ptr;
00116
00118 typedef CVariableNames variable_names_type;
00119
00121 typedef variable_names_type::const_reference const_varname_reference;
00122
00124 boost::intrusive_ptr<DdManager> pmanager;
00125
00127 static errorfunc_type errorHandler;
00128
00130 static bool verbose;
00131
00133 refcount_type ref;
00134
00136 variable_names_type m_names;
00137
00138 std::vector<node_type> m_vars;
00139
00140
00142 CCuddCore(size_type numVars = 0,
00143 size_type numVarsZ = 0,
00144 size_type numSlots = CUDD_UNIQUE_SLOTS,
00145 size_type cacheSize = CUDD_CACHE_SLOTS,
00146 large_size_type maxMemory = 0):
00147 ref(0), m_names(numVarsZ), m_vars(numVarsZ),
00148 pmanager(getMan(numVars,numVarsZ,numSlots,cacheSize,maxMemory)) {
00149
00150 for (unsigned idx = 0 ; idx < numVarsZ; ++idx) {
00151 m_vars[idx] = cuddUniqueInterZdd(manager(), idx, DD_ONE(manager()),
00152 DD_ZERO(manager()));
00153 Cudd_Ref(m_vars[idx]);
00154 }
00155
00156 }
00157
00159 CCuddCore(const self& rhs):
00160 ref(0), pmanager(rhs.pmanager), m_names(rhs.m_names), m_vars(rhs.m_vars) {
00161
00162 std::vector<node_type>::iterator start(m_vars.begin()),
00163 finish(m_vars.end());
00164 while (start != finish) {
00165 Cudd_Ref(*start);
00166 ++start;
00167 }
00168 }
00169
00170
00171 DdManager* manager() {
00172 return pmanager.get();
00173 }
00174 DdManager*
00175 getMan(size_type numVars = 0,
00176 size_type numVarsZ = 0,
00177 size_type numSlots = CUDD_UNIQUE_SLOTS,
00178 size_type cacheSize = CUDD_CACHE_SLOTS,
00179 large_size_type maxMemory = 0) {
00180
00181 DdManager* ptr
00182 = Cudd_Init(numVars,numVarsZ,numSlots,cacheSize,maxMemory);
00183 ptr->hooks = NULL;
00184 return ptr;
00185 }
00186
00188 ~CCuddCore(){
00189
00190 for (std::vector<node_type>::iterator iter = m_vars.begin(); iter !=
00191 m_vars.end(); ++iter) {
00192
00193 Cudd_RecursiveDerefZdd(manager(), *iter);
00194 }
00195
00197
00198
00199
00200
00201 }
00202
00204 void addRef(){ ++ref; }
00205
00207 refcount_type release() {
00208 return (--ref);
00209 }
00210 };
00211
00213
00214
00215 inline void
00216 intrusive_ptr_add_ref(CCuddCore* pCore){
00217 pCore->addRef();
00218 }
00219
00221 inline void
00222 intrusive_ptr_release(CCuddCore* pCore) {
00223 if (!(pCore->release())) {
00224 delete pCore;
00225 }
00226 }
00227
00228
00229
00231
00232 END_NAMESPACE_PBORI
00233
00234 #endif
00235
00236