00001
00002
00014
00015
00016 #ifndef polybori_ring_CCuddInterface_h_
00017 #define polybori_ring_CCuddInterface_h_
00018
00019
00020 #include <polybori/pbori_defs.h>
00021
00022 #include <polybori/cudd/cudd.h>
00023 #include <polybori/cudd/cuddInt.h>
00024
00025 #include <polybori/routines/pbori_func.h>
00026 #include "CCallbackWrapper.h"
00027
00028 #include <vector>
00029 #include <boost/intrusive_ptr.hpp>
00030 #include <boost/scoped_array.hpp>
00031
00032 #include <boost/preprocessor/cat.hpp>
00033 #include <boost/preprocessor/seq/for_each.hpp>
00034 #include <boost/preprocessor/facilities/expand.hpp>
00035 #include <boost/preprocessor/stringize.hpp>
00036
00037 #include <polybori/except/PBoRiError.h>
00038
00039 #include <stdexcept>
00040 #include <algorithm>
00041
00042 #include <polybori/common/CWeakPtrFacade.h>
00043
00044
00045 inline const char* error_text(PBORI_PREFIX(DdManager)* mgr) {
00046 switch (PBORI_PREFIX(Cudd_ReadErrorCode)(mgr)) {
00047 case CUDD_MEMORY_OUT:
00048 return("Out of memory.");
00049 case CUDD_TOO_MANY_NODES:
00050 return("To many nodes.");
00051 case CUDD_MAX_MEM_EXCEEDED:
00052 return("Maximum memory exceeded.");
00053 case CUDD_INVALID_ARG:
00054 return("Invalid argument.");
00055 case CUDD_INTERNAL_ERROR:
00056 return("Internal error.");
00057 case CUDD_TIMEOUT_EXPIRED:
00058 return("Timed out.");
00059 case CUDD_NO_ERROR:
00060 return("No error. (Should not reach here!)");
00061 }
00062 return("Unexpected error.");
00063 }
00064
00066 inline void
00067 intrusive_ptr_add_ref(PBORI_PREFIX(DdManager)* ptr){
00068 ++(ptr->hooks);
00069 }
00070
00072 inline void
00073 intrusive_ptr_release(PBORI_PREFIX(DdManager)* ptr) {
00074 if (!(--(ptr->hooks))) {
00075
00076 PBORI_ASSERT(PBORI_PREFIX(Cudd_CheckZeroRef)(ptr) == 0);
00077 PBORI_PREFIX(Cudd_Quit)(ptr);
00078 }
00079 }
00080
00081
00082 BEGIN_NAMESPACE_PBORI
00083
00084 typedef PBORI_PREFIX(DdManager) DdManager;
00085
00087
00088 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \
00089 return BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
00090
00091 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \
00092 BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
00093
00094 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \
00095 BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this, arg); }
00096
00097
00111 class CCuddInterface:
00112 public CTypes::auxtypes_type {
00113
00115 typedef CCuddInterface self;
00116
00117 public:
00119 typedef DdNode* node_ptr;
00120
00122 typedef DdManager mgr_type;
00123 typedef int cudd_idx_type;
00124
00125 typedef node_ptr (*unary_int_function)(mgr_type*, cudd_idx_type);
00126 typedef node_ptr (*void_function)(mgr_type*);
00127
00128
00130 typedef boost::intrusive_ptr<mgr_type> mgr_ptr;
00131
00133 CCuddInterface(size_type numVars, size_type numVarsZ,
00134 size_type numSlots = PBORI_UNIQUE_SLOTS,
00135 size_type cacheSize = PBORI_CACHE_SLOTS,
00136 unsigned long maxMemory = PBORI_MAX_MEMORY):
00137 p_mgr(init(numVars, numVarsZ, numSlots, cacheSize, maxMemory)),
00138 m_vars(numVarsZ) {
00139 for (idx_type idx = 0; size_type(idx) < numVarsZ; ++idx) initVar(m_vars[idx], idx);
00140 }
00141
00143 CCuddInterface(const self& rhs): p_mgr(rhs.p_mgr), m_vars(rhs.m_vars) {
00144 std::for_each(m_vars.begin(), m_vars.end(), PBORI_PREFIX(Cudd_Ref));
00145 }
00146
00148 ~CCuddInterface() {
00149 std::for_each(m_vars.begin(), m_vars.end(),
00150 callBack(&self::recursiveDeref));
00151 }
00152
00154 mgr_type* getManager() const { return p_mgr.operator->(); }
00155
00157 mgr_ptr pManager() const { return p_mgr; }
00158
00160 self& operator=(const self & right) {
00161 p_mgr = right.p_mgr;
00162 return *this;
00163 }
00164
00166 node_ptr zddVar(idx_type idx) const { return apply(PBORI_PREFIX(Cudd_zddIthVar), idx); }
00167
00169 node_ptr zddOne(idx_type iMax) const { return apply(PBORI_PREFIX(Cudd_ReadZddOne), iMax); }
00170
00172 node_ptr zddZero() const { return apply(PBORI_PREFIX(Cudd_ReadZero)); }
00173
00175 node_ptr zddOne() const {
00176 return checkedResult(DD_ONE(getManager()));
00177 }
00178
00179 #ifdef CUDD_ORIGINAL_INCLUSION
00182
00183 int ReorderingStatusZdd(PBORI_PREFIX(Cudd_ReorderingType) * method) const {
00184 return PBORI_PREFIX(Cudd_ReorderingStatusZdd)(*this, method);
00185 }
00186
00188 idx_type ReadPermZdd(idx_type idx) const {
00189 return PBORI_PREFIX(Cudd_ReadPermZdd)(*this, idx);
00190 }
00191
00193 idx_type ReadInvPermZdd(idx_type idx) const {
00194 return PBORI_PREFIX(Cudd_ReadInvPermZdd)(*this, idx);
00195 }
00196
00197 void AddHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
00198 checkedResult(PBORI_PREFIX(Cudd_AddHook)(*this, f, where));
00199 }
00200 void RemoveHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
00201 checkedResult(PBORI_PREFIX(Cudd_RemoveHook)(*this, f, where));
00202 }
00203 int IsInHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) const {
00204 return PBORI_PREFIX(Cudd_IsInHook)(*this, f, where);
00205 }
00206 void EnableReorderingReporting() {
00207 checkedResult(PBORI_PREFIX(Cudd_EnableReorderingReporting)(*this));
00208 }
00209 void DisableReorderingReporting() {
00210 checkedResult(PBORI_PREFIX(Cudd_DisableReorderingReporting)(*this));
00211 }
00212
00213 void DebugCheck(){ checkedResult(PBORI_PREFIX(Cudd_DebugCheck)(*this)); }
00214 void CheckKeys(){ checkedResult(PBORI_PREFIX(Cudd_CheckKeys)(*this)); }
00215 void PrintLinear() { checkedResult(PBORI_PREFIX(Cudd_PrintLinear)(*this)); }
00216
00217 int ReadLinear(int x, int y) { return PBORI_PREFIX(Cudd_ReadLinear)(*this, x, y); }
00218
00219 size_type Prime(size_type pr) const { return PBORI_PREFIX(Cudd_Prime)(pr); }
00220
00221 void PrintVersion(FILE * fp) const { std::cout.flush(); PBORI_PREFIX(Cudd_PrintVersion)(fp); }
00222
00223 void zddPrintSubtable() const{
00224 std::cout.flush();
00225 PBORI_PREFIX(Cudd_zddPrintSubtable)(*this);
00226 }
00227
00228 void zddReduceHeap(PBORI_PREFIX(Cudd_ReorderingType) heuristic, int minsize) {
00229 checkedResult(PBORI_PREFIX(Cudd_zddReduceHeap)(*this, heuristic, minsize));
00230 }
00231 void zddShuffleHeap(int * permutation) {
00232 checkedResult(PBORI_PREFIX(Cudd_zddShuffleHeap)(*this, permutation));
00233 }
00234 void zddSymmProfile(int lower, int upper) const {
00235 PBORI_PREFIX(Cudd_zddSymmProfile)(*this, lower, upper);
00236 }
00237
00240 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type,
00241 (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) )
00242
00243 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int,
00244 (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation)
00245 (SetArcviolation)(SetPopulationSize)(SetNumberXovers)
00246 )
00247
00248 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr))
00249
00250 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL,
00251 (zddRealignEnable)(zddRealignDisable)
00252 (AutodynDisableZdd)
00253 (EnableGarbageCollection)(DisableGarbageCollection)
00254 (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode)
00255 )
00256
00257 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double,
00258 (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits)
00259 (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance)
00260 )
00261
00262 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type,
00263 (ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache)
00264 (ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead)
00265 (ReadNextReordering)(ReadMaxLive)
00266 )
00267
00268 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,
00269 (zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar)
00270 (ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled)
00271 (DeadAreCounted)(ReadRecomb)
00272 (ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation)
00273 (ReadNumberXovers)(ReorderingReporting)(ReadErrorCode)
00274 )
00275
00276 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long,
00277 (ReadReorderingTime)(ReadGarbageCollectionTime)
00278 (ReadPeakNodeCount)(zddReadNodeCount)
00279 )
00280
00281 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type,
00282 (ReadMemoryInUse)(ReadMaxMemory) )
00283
00284 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr))
00285
00286 PB_CUDDMGR_SET(BOOST_PP_NIL, PBORI_PREFIX(Cudd_ReorderingType), AutodynEnableZdd)
00287 PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory)
00288 PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth)
00290
00291
00292 #else
00293 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,(ReadZddSize))
00294 #endif
00295
00296 node_ptr getVar(idx_type idx) const {
00297 if PBORI_UNLIKELY(size_type(idx) >= m_vars.size())
00298 throw PBoRiError(CTypes::out_of_bounds);
00299 return m_vars[idx];
00300 }
00301
00303 size_type nVariables() const { return (size_type)ReadZddSize(); }
00304
00306 void cacheFlush() { PBORI_PREFIX(cuddCacheFlush)(*this); }
00307
00308 protected:
00309
00311 mgr_ptr init(size_type numVars,size_type numVarsZ, size_type numSlots,
00312 size_type cacheSize, large_size_type maxMemory) {
00313
00314 DdManager* ptr = PBORI_PREFIX(Cudd_Init)(numVars, numVarsZ, numSlots, cacheSize, maxMemory);
00315 if PBORI_UNLIKELY(ptr==NULL)
00316 throw PBoRiError(CTypes::failed);
00317
00318 ptr->hooks = NULL;
00319
00320 return ptr;
00321 }
00323 node_ptr checkedResult(node_ptr result) const {
00324 checkedResult(int(result != NULL));
00325 return result;
00326 }
00327
00329 void checkedResult(int result) const {
00330 if PBORI_UNLIKELY(result == 0) {
00331 throw std::runtime_error(error_text(*this));
00332 }
00333 }
00334
00336 node_ptr apply(unary_int_function func, idx_type idx) const {
00337 return checkedResult(func(*this, idx) );
00338 }
00339
00341 node_ptr apply(void_function func) const {
00342 return checkedResult(func(*this) );
00343 }
00344
00345 protected:
00347 void recursiveDeref(node_ptr node) const {
00348 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(*this, node);
00349 }
00350
00352 void initVar(node_ptr& node, idx_type idx) const {
00353 PBORI_PREFIX(Cudd_Ref)(node = PBORI_PREFIX(cuddUniqueInterZdd)(*this,
00354 idx, zddOne(), zddZero()));
00355 }
00356
00358 template <class MemberFuncPtr>
00359 CCallbackWrapper<MemberFuncPtr>
00360 callBack(MemberFuncPtr ptr) {
00361 return CCallbackWrapper<MemberFuncPtr>(*this, ptr);
00362 }
00363
00364 private:
00366 operator mgr_type*() const { return getManager(); }
00367
00369 mgr_ptr p_mgr;
00370
00372 std::vector<node_ptr> m_vars;
00373 };
00374
00375
00376 #undef PB_CUDDMGR_READ
00377 #undef PB_CUDDMGR_SWITCH
00378 #undef PB_CUDDMGR_SET
00379
00380 END_NAMESPACE_PBORI
00381
00382 #endif
00383
00384
