PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 00017 // include basic definitions 00018 #include "pbori_defs.h" 00019 00020 #include <cudd.h> 00021 #include <cuddInt.h> 00022 00023 #include "pbori_func.h" // handle_error 00024 #include "CCallbackWrapper.h" 00025 00026 #include <vector> 00027 #include <boost/intrusive_ptr.hpp> 00028 #include <boost/scoped_array.hpp> 00029 00030 #include <boost/preprocessor/cat.hpp> 00031 #include <boost/preprocessor/seq/for_each.hpp> 00032 #include <boost/preprocessor/facilities/expand.hpp> 00033 #include <boost/preprocessor/stringize.hpp> 00034 00035 #include "PBoRiError.h" 00036 00037 #include <stdexcept> 00038 #include <algorithm> 00039 00040 #ifndef CCuddInterface_h_ 00041 #define CCuddInterface_h_ 00042 00043 // get cudd error texts 00044 inline const char* error_text(DdManager* mgr) { 00045 switch (Cudd_ReadErrorCode(mgr)) { 00046 CUDD_MEMORY_OUT: 00047 return("Out of memory."); 00048 CUDD_TOO_MANY_NODES: 00049 return("To many nodes."); 00050 CUDD_MAX_MEM_EXCEEDED: 00051 return("Maximum memory exceeded."); 00052 CUDD_INVALID_ARG: 00053 return("Invalid argument."); 00054 CUDD_INTERNAL_ERROR: 00055 return("Internal error."); 00056 } 00057 return("Unexpected error."); 00058 } 00059 00061 inline void 00062 intrusive_ptr_add_ref(DdManager* ptr){ 00063 ++(ptr->hooks); 00064 } 00065 00067 inline void 00068 intrusive_ptr_release(DdManager* ptr) { 00069 if (!(--(ptr->hooks))) { 00070 int retval = Cudd_CheckZeroRef(ptr); 00071 // Check for unexpected non-zero reference counts 00072 assert(retval == 0); 00073 00074 Cudd_Quit(ptr); 00075 } 00076 } 00077 00078 00079 BEGIN_NAMESPACE_PBORI 00080 00081 00082 00084 00085 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \ 00086 return BOOST_PP_CAT(Cudd_, funcname)(*this); } 00087 00088 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \ 00089 BOOST_PP_CAT(Cudd_, funcname)(*this); } 00090 00091 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \ 00092 BOOST_PP_CAT(Cudd_, funcname)(*this, arg); } 00093 00094 00108 class CCuddInterface: 00109 public CTypes::auxtypes_type { 00110 00112 typedef CCuddInterface self; 00113 00114 public: 00116 typedef DdNode* node_ptr; 00117 00119 typedef DdManager mgr_type; 00120 typedef int cudd_idx_type; 00121 00122 typedef node_ptr (*unary_int_function)(mgr_type*, cudd_idx_type); 00123 typedef node_ptr (*void_function)(mgr_type*); 00124 00125 00127 typedef boost::intrusive_ptr<mgr_type> mgr_ptr; 00128 00130 CCuddInterface(size_type numVars, size_type numVarsZ, 00131 size_type numSlots = PBORI_UNIQUE_SLOTS, 00132 size_type cacheSize = PBORI_CACHE_SLOTS, 00133 unsigned long maxMemory = PBORI_MAX_MEMORY): 00134 p_mgr(init(numVars, numVarsZ, numSlots, cacheSize, maxMemory)), 00135 m_vars(numVarsZ) { 00136 for (idx_type idx = 0; idx < numVarsZ; ++idx) initVar(m_vars[idx], idx); 00137 } 00138 00140 CCuddInterface(const self& rhs): p_mgr(rhs.p_mgr), m_vars(rhs.m_vars) { 00141 std::for_each(m_vars.begin(), m_vars.end(), Cudd_Ref); 00142 } 00143 00145 ~CCuddInterface() { 00146 std::for_each(m_vars.begin(), m_vars.end(), 00147 callBack(&self::recursiveDeref)); 00148 } 00149 00151 mgr_type* getManager() const { return p_mgr.operator->(); } 00152 00154 mgr_ptr pManager() const { return p_mgr; } 00155 00157 self& operator=(const self & right) { 00158 p_mgr = right.p_mgr; 00159 return *this; 00160 } 00161 00163 node_ptr zddVar(idx_type idx) const { return apply(Cudd_zddIthVar, idx); } 00164 00166 node_ptr zddOne(idx_type iMax) const { return apply(Cudd_ReadZddOne, iMax); } 00167 00169 node_ptr zddZero() const { return apply(Cudd_ReadZero); } 00170 00172 node_ptr zddOne() const { 00173 return checkedResult(DD_ONE(getManager())); 00174 } 00175 00178 00179 int ReorderingStatusZdd(Cudd_ReorderingType * method) const { 00180 return Cudd_ReorderingStatusZdd(*this, method); 00181 } 00182 00184 idx_type ReadPermZdd(idx_type idx) const { 00185 return Cudd_ReadPermZdd(*this, idx); 00186 } 00187 00189 idx_type ReadInvPermZdd(idx_type idx) const { 00190 return Cudd_ReadInvPermZdd(*this, idx); 00191 } 00192 00193 void AddHook(DD_HFP f, Cudd_HookType where) { 00194 checkedResult(Cudd_AddHook(*this, f, where)); 00195 } 00196 void RemoveHook(DD_HFP f, Cudd_HookType where) { 00197 checkedResult(Cudd_RemoveHook(*this, f, where)); 00198 } 00199 int IsInHook(DD_HFP f, Cudd_HookType where) const { 00200 return Cudd_IsInHook(*this, f, where); 00201 } 00202 void EnableReorderingReporting() { 00203 checkedResult(Cudd_EnableReorderingReporting(*this)); 00204 } 00205 void DisableReorderingReporting() { 00206 checkedResult(Cudd_DisableReorderingReporting(*this)); 00207 } 00208 00209 void DebugCheck(){ checkedResult(Cudd_DebugCheck(*this)); } 00210 void CheckKeys(){ checkedResult(Cudd_CheckKeys(*this)); } 00211 void PrintLinear() { checkedResult(Cudd_PrintLinear(*this)); } 00212 00213 int ReadLinear(int x, int y) { return Cudd_ReadLinear(*this, x, y); } 00214 00215 size_type Prime(size_type pr) const { return Cudd_Prime(pr); } 00216 00217 void PrintVersion(FILE * fp) const { std::cout.flush(); Cudd_PrintVersion(fp); } 00218 00219 MtrNode* MakeZddTreeNode(size_type low, size_type size, size_type type) { 00220 return Cudd_MakeZddTreeNode(*this, low, size, type); 00221 } 00222 void zddPrintSubtable() const{ 00223 std::cout.flush(); 00224 Cudd_zddPrintSubtable(*this); 00225 } 00226 00227 void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize) { 00228 checkedResult(Cudd_zddReduceHeap(*this, heuristic, minsize)); 00229 } 00230 void zddShuffleHeap(int * permutation) { 00231 checkedResult(Cudd_zddShuffleHeap(*this, permutation)); 00232 } 00233 void zddSymmProfile(int lower, int upper) const { 00234 Cudd_zddSymmProfile(*this, lower, upper); 00235 } 00236 00239 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type, 00240 (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) ) 00241 00242 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int, 00243 (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation) 00244 (SetArcviolation)(SetPopulationSize)(SetNumberXovers) 00245 ) 00246 00247 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr)) 00248 00249 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL, 00250 (zddRealignEnable)(zddRealignDisable) 00251 (AutodynDisableZdd)(FreeZddTree) 00252 (EnableGarbageCollection)(DisableGarbageCollection) 00253 (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode) 00254 ) 00255 00256 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double, 00257 (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits) 00258 (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance) 00259 ) 00260 00261 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type, 00262 (ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache) 00263 (ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead) 00264 (ReadNextReordering)(ReadMaxLive) 00265 ) 00266 00267 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int, 00268 (zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar) 00269 (ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled) 00270 (DeadAreCounted)(ReadRecomb) 00271 (ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation) 00272 (ReadNumberXovers)(ReorderingReporting)(ReadErrorCode) 00273 ) 00274 00275 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long, 00276 (ReadReorderingTime)(ReadGarbageCollectionTime) 00277 (ReadPeakNodeCount)(zddReadNodeCount) 00278 ) 00279 00280 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type, 00281 (ReadMemoryInUse)(ReadMaxMemory) ) 00282 00283 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr)) 00284 00285 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, MtrNode*, (ReadZddTree)) 00286 00287 PB_CUDDMGR_SET(BOOST_PP_NIL, Cudd_ReorderingType, AutodynEnableZdd) 00288 PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory) 00289 PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth) 00290 PB_CUDDMGR_SET(BOOST_PP_NIL, MtrNode*, SetZddTree) 00292 00293 00294 00295 00296 node_ptr getVar(idx_type idx) const { 00297 if UNLIKELY(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() { 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 = Cudd_Init(numVars, numVarsZ, numSlots, cacheSize, maxMemory); 00315 if 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 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 Cudd_RecursiveDerefZdd(*this, node); 00349 } 00350 00352 void initVar(node_ptr& node, idx_type idx) const { 00353 Cudd_Ref(node = 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