• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

CCuddInterface.h

Go to the documentation of this file.
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 

Generated on Thu Nov 4 2010 08:06:20 for PolyBoRi by  doxygen 1.7.1