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