PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00070 //***************************************************************************** 00071 00072 00073 // include basic definitions 00074 00075 #include "CCuddZDD.h" 00076 00077 #ifndef CCuddInterface_h_ 00078 #define CCuddInterface_h_ 00079 00080 BEGIN_NAMESPACE_PBORI 00081 00083 00084 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \ 00085 return BOOST_PP_CAT(Cudd_, funcname)(getManager()); } 00086 00087 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \ 00088 BOOST_PP_CAT(Cudd_, funcname)(getManager()); } 00089 00090 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \ 00091 BOOST_PP_CAT(Cudd_, funcname)(getManager(), arg); } 00092 00093 00107 class CCuddInterface { 00108 00109 public: 00110 00111 PB_DECLARE_CUDD_TYPES(CCuddCore) 00112 00113 00114 00115 typedef CCuddInterface self; 00116 typedef CCuddCore core_type; 00117 typedef core_type::mgrcore_ptr mgrcore_ptr; 00118 typedef CCuddZDD dd_type; 00119 typedef self tmp_ref; 00121 00123 typedef CVariableNames variable_names_type; 00124 00126 typedef variable_names_type::const_reference const_varname_reference; 00127 00129 CCuddInterface(size_type numVars = 0, 00130 size_type numVarsZ = 0, 00131 size_type numSlots = CUDD_UNIQUE_SLOTS, 00132 size_type cacheSize = CUDD_CACHE_SLOTS, 00133 unsigned long maxMemory = 0): 00134 pMgr (new core_type(numVars, numVarsZ, numSlots, cacheSize, maxMemory)) { 00135 } 00136 00138 CCuddInterface(const self& rhs): pMgr(rhs.pMgr) {} 00139 00141 CCuddInterface(mgrcore_ptr rhs): pMgr(rhs) {}; 00142 00144 ~CCuddInterface() {} 00145 00147 errorfunc_type setHandler(errorfunc_type newHandler) { 00148 errorfunc_type oldHandler = pMgr->errorHandler; 00149 pMgr->errorHandler = newHandler; 00150 return oldHandler; 00151 } 00152 00154 errorfunc_type getHandler() const { return pMgr->errorHandler; } 00155 00157 mgrcore_type getManager() const { return pMgr->manager; } 00158 00160 mgrcore_ptr managerCore() const { return pMgr; } 00161 00163 00164 void makeVerbose() { pMgr->verbose = true; } 00165 void makeTerse() { pMgr->verbose = false; } 00166 bool isVerbose() const { return pMgr->verbose; } 00168 00170 void info() const { checkedResult(Cudd_PrintInfo(getManager(),stdout)); } 00171 00172 void checkReturnValue(const node_type result) const { 00173 checkReturnValue(result != NULL); 00174 } 00175 void checkReturnValue(const int result) const { 00176 if UNLIKELY(result == 0) { 00177 handle_error<CUDD_MEMORY_OUT> tmp(pMgr->errorHandler); 00178 tmp(Cudd_ReadErrorCode(getManager())); 00179 } 00180 } 00181 00183 self& operator=(const self & right) { 00184 pMgr = right.pMgr; 00185 return *this; 00186 } 00187 00189 CCuddZDD zddVar(idx_type idx) const { return apply(Cudd_zddIthVar, idx); } 00190 00192 CCuddZDD zddOne(idx_type iMax) const { return apply(Cudd_ReadZddOne, iMax); } 00193 00195 CCuddZDD zddZero() const { return apply(Cudd_ReadZero); } 00196 00198 CCuddZDD zddOne() const { 00199 return checkedResult(DD_ONE(getManager())); 00200 } 00201 00204 00205 int ReorderingStatusZdd(Cudd_ReorderingType * method) const { 00206 return Cudd_ReorderingStatusZdd(getManager(), method); 00207 } 00208 00209 idx_type ReadPermZdd(idx_type i) const { 00210 return Cudd_ReadPermZdd(getManager(), i); 00211 } 00212 00213 idx_type ReadInvPermZdd(idx_type i) const { 00214 return Cudd_ReadInvPermZdd(getManager(), i); 00215 } 00216 00217 void AddHook(DD_HFP f, Cudd_HookType where) { 00218 checkedResult(Cudd_AddHook(getManager(), f, where)); 00219 } 00220 void RemoveHook(DD_HFP f, Cudd_HookType where) { 00221 checkedResult(Cudd_RemoveHook(getManager(), f, where)); 00222 } 00223 int IsInHook(DD_HFP f, Cudd_HookType where) const { 00224 return Cudd_IsInHook(getManager(), f, where); 00225 } 00226 void EnableReorderingReporting() { 00227 checkedResult(Cudd_EnableReorderingReporting(getManager())); 00228 } 00229 void DisableReorderingReporting() { 00230 checkedResult(Cudd_DisableReorderingReporting(getManager())); 00231 } 00232 00233 void DebugCheck(){ checkedResult(Cudd_DebugCheck(getManager())); } 00234 void CheckKeys(){ checkedResult(Cudd_CheckKeys(getManager())); } 00235 void PrintLinear() { checkedResult(Cudd_PrintLinear(getManager())); } 00236 00237 int ReadLinear(int x, int y) { return Cudd_ReadLinear(getManager(), x, y); } 00238 00239 size_type Prime(size_type pr) const { return Cudd_Prime(pr); } 00240 00241 void PrintVersion(FILE * fp) const { cout.flush(); Cudd_PrintVersion(fp); } 00242 00243 MtrNode* MakeZddTreeNode(size_type low, size_type size, size_type type) { 00244 return Cudd_MakeZddTreeNode(getManager(), low, size, type); 00245 } 00246 void zddPrintSubtable() const{ 00247 cout.flush(); 00248 Cudd_zddPrintSubtable(getManager()); 00249 } 00250 00251 void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize) { 00252 checkedResult(Cudd_zddReduceHeap(getManager(), heuristic, minsize)); 00253 } 00254 void zddShuffleHeap(int * permutation) { 00255 checkedResult(Cudd_zddShuffleHeap(getManager(), permutation)); 00256 } 00257 void zddSymmProfile(int lower, int upper) const { 00258 Cudd_zddSymmProfile(getManager(), lower, upper); 00259 } 00260 00261 int SharingSize(dd_type* nodes, int nlen) const { 00262 typedef boost::scoped_array<node_type> node_array; 00263 node_array nodeArray(new node_type[nlen]); 00264 std::transform(nodes, nodes + nlen, nodeArray.get(), get_node<dd_type>()); 00265 00266 return checkedResult(Cudd_SharingSize(nodeArray.get(), nlen)); 00267 } 00268 00271 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type, 00272 (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) ) 00273 00274 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int, 00275 (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation) 00276 (SetArcviolation)(SetPopulationSize)(SetNumberXovers) 00277 ) 00278 00279 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr)) 00280 00281 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL, 00282 (zddRealignEnable)(zddRealignDisable) 00283 (AutodynDisableZdd)(FreeZddTree) 00284 (EnableGarbageCollection)(DisableGarbageCollection) 00285 (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode) 00286 ) 00287 00288 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double, 00289 (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits) 00290 (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance) 00291 ) 00292 00293 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type, 00294 (ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache) 00295 (ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead) 00296 (ReadNextReordering)(ReadMaxLive) 00297 ) 00298 00299 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int, 00300 (zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar) 00301 (ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled) 00302 (DeadAreCounted)(ReadRecomb) 00303 (ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation) 00304 (ReadNumberXovers)(ReorderingReporting)(ReadErrorCode) 00305 ) 00306 00307 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long, 00308 (ReadReorderingTime)(ReadGarbageCollectionTime) 00309 (ReadPeakNodeCount)(zddReadNodeCount) 00310 ) 00311 00312 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type, 00313 (ReadMemoryInUse)(ReadMaxMemory) ) 00314 00315 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr)) 00316 00317 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, MtrNode*, (ReadZddTree)) 00318 00319 PB_CUDDMGR_SET(BOOST_PP_NIL, Cudd_ReorderingType, AutodynEnableZdd) 00320 PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory) 00321 PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth) 00322 PB_CUDDMGR_SET(BOOST_PP_NIL, MtrNode*, SetZddTree) 00324 00325 00326 00328 void setName(idx_type idx, const_varname_reference varname) { 00329 (pMgr->m_names).set(idx, varname); 00330 } 00331 00333 const_varname_reference getName(idx_type idx) const { 00334 return (pMgr->m_names)[idx]; 00335 } 00336 00337 dd_type getVar(idx_type idx) const { 00338 assert(idx < pMgr->m_vars.size()); 00339 return getDiagram(pMgr->m_vars[idx]); 00340 } 00341 00343 size_type nVariables() const { 00344 return Cudd_ReadZddSize(getManager()); 00345 } 00346 00347 protected: 00349 dd_type getDiagram(node_type result) const { 00350 return dd_type(managerCore(), result); 00351 } 00352 00354 dd_type checkedResult(node_type result) const { 00355 checkReturnValue(result); 00356 return getDiagram(result); 00357 } 00358 00360 idx_type checkedResult(idx_type result) const { 00361 checkReturnValue(result); 00362 return result; 00363 } 00364 00366 dd_type apply(unary_int_function func, idx_type idx) const { 00367 return checkedResult(func(getManager(), idx) ); 00368 } 00369 00371 dd_type apply(void_function func) const { 00372 return checkedResult(func(getManager()) ); 00373 } 00374 00375 private: 00376 mgrcore_ptr pMgr; 00377 }; // CCuddInterface 00378 00379 00380 #undef PB_CUDDMGR_READ 00381 #undef PB_CUDDMGR_SWITCH 00382 #undef PB_CUDDMGR_SET 00383 00384 END_NAMESPACE_PBORI 00385 00386 #endif 00387 00388