00001
00002
00070
00071
00072
00073
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 };
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