PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 #ifndef polybori_ring_CCuddInterface_h_ 00017 #define polybori_ring_CCuddInterface_h_ 00018 00019 // include basic definitions 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> // handle_error 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 // get PBORI_PREFIX(cudd error) texts 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 00180 00181 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; // abusing hooks pointer for reference counting 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 }; // CCuddInterface 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