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