PolyBoRi
CDDManager.h
Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00096 //*****************************************************************************
00097 
00098 #ifndef CDDManager_h_
00099 #define CDDManager_h_
00100 #include "cacheopts.h"
00101 // load basic definitions
00102 #include "pbori_defs.h"
00103 #include "pbori_traits.h"
00104 
00105 // get decision diagram definitions.
00106 #include "CDDInterface.h"
00107 
00108 #include "CCuddInterface.h"
00109 
00110 // get standard map functionality
00111 #include <map>
00112 
00113 
00114 #ifndef PBORI_UNIQUE_SLOTS
00115 #  define PBORI_UNIQUE_SLOTS CUDD_UNIQUE_SLOTS // initial size of subtables
00116 #endif
00117 
00118 #ifndef PBORI_CACHE_SLOTS
00119 #  define PBORI_CACHE_SLOTS CUDD_CACHE_SLOTS   // default size of the cache
00120 #endif
00121 
00122 #ifndef PBORI_MAX_MEMORY
00123 #  define PBORI_MAX_MEMORY 0    // target maximum memory occupation
00124                                 // if PBORI_MAX_MEMORY == 0 then
00125                                 // guess based on the available memory  
00126 #endif
00127 
00128 
00129 BEGIN_NAMESPACE_PBORI
00130 
00131 
00132 inline ZDD
00133 fetch_diagram(const Cudd& mgr, const ZDD& rhs) {
00134   return ZDD(&const_cast<Cudd&>(mgr), rhs.getNode());
00135 }
00136 
00137 template <class MgrType, class DDType>
00138 inline const DDType&
00139 fetch_diagram(const MgrType& mgr, const DDType& rhs) {
00140   return rhs;
00141 }
00142 
00143 inline Cudd&
00144 fetch_manager(const Cudd& mgr) {
00145   return const_cast<Cudd&>(mgr);
00146 }
00147 
00148 template <class MgrType>
00149 inline const MgrType&
00150 fetch_manager(const MgrType& mgr) {
00151   return mgr;
00152 }
00153 
00154 
00164 template <class CuddLikeManType, class StorageType>
00165 class CDDManagerBase {
00166  public:
00167   
00169   typedef CuddLikeManType interfaced_type;
00170 
00172   typedef StorageType interfaced_store;
00173  
00175   typedef CDDManagerBase<interfaced_type, interfaced_store> self;
00176 
00178   typedef CTypes::size_type size_type;
00179 
00181   typedef CTypes::idx_type idx_type;
00182 
00184   typedef typename manager_traits<interfaced_type>::dd_base dd_base;
00185   
00187   typedef CDDInterface<dd_base> dd_type;
00188 
00190   typedef std::map<idx_type, dd_base> persistent_cache_type;
00191 
00193   typedef CVariableNames variable_names_type;
00194 
00196   typedef variable_names_type::const_reference const_varname_reference;
00197 
00199   CDDManagerBase(size_type nvars = 0,
00200                  size_type numSlots = PBORI_UNIQUE_SLOTS,
00201                  size_type cacheSize = PBORI_CACHE_SLOTS,
00202                  unsigned long maxMemory = PBORI_MAX_MEMORY): 
00203     m_interfaced(0, nvars, numSlots, cacheSize, maxMemory) {  }
00204   
00206   CDDManagerBase(const self& rhs): 
00207     m_interfaced(rhs.m_interfaced) {
00208   }
00209 
00211   CDDManagerBase(const interfaced_type& rhs): 
00212     m_interfaced(fetch_manager(rhs)) {  }
00213 
00215   CDDManagerBase(const dd_type& dd): 
00216     m_interfaced(dd.manager()) { }
00217 
00219   ~CDDManagerBase() { }
00220 
00222   dd_base fetchDiagram(const dd_base& rhs) const {
00223     return fetch_diagram(manager(), rhs);
00224   }
00225 
00227   dd_base ddVariable(idx_type nvar) const {  
00228     return manager().zddVar(nvar); 
00229   }
00230 
00232   dd_base variable(idx_type nvar) const {  
00233     return blank().change(nvar); 
00234   }
00235 
00237   dd_base persistentVariable(idx_type nvar) const {
00238     return manager().getVar(nvar);
00239   }
00240 
00242   size_type nVariables() const { 
00243     return manager().nVariables();
00244   }
00245 
00248   dd_type empty() const { return manager().zddZero(); }
00249 
00252   dd_type blank() const { return manager().zddOne(nVariables()); }
00253 
00255   operator interfaced_type&() { return m_interfaced; }
00256 
00258   operator const interfaced_type&() const { return m_interfaced; }
00259 
00261   interfaced_type& manager() { return m_interfaced; }
00262 
00264   const interfaced_type& manager() const { return m_interfaced; }
00265 
00267   void printInfo() const { manager().info(); }
00268 
00270   void setVariableName(idx_type idx, const_varname_reference varname) {
00271     manager().setName(idx, varname);
00272   }
00273 
00275   const_varname_reference getVariableName(idx_type idx) const { 
00276     return manager().getName(idx);
00277   }
00278 
00279 private:
00281   mutable interfaced_store m_interfaced;
00282 };
00283 
00291 template<>
00292 class CDDManager<Cudd&>:
00293   public CDDManagerBase<Cudd, Cudd&> { 
00294 
00295 public:
00296 
00297   typedef Cudd manager_type;
00298   typedef Cudd& storage_type;
00299   typedef CDDManagerBase<manager_type, storage_type> base;
00300   typedef CDDManager<storage_type> self;
00301 
00303   CDDManager(manager_type& rhs): 
00304     base(rhs) { }
00305 
00307   CDDManager(const dd_type& dd): 
00308     base(dd) { }
00309 
00311   CDDManager(const self& rhs): 
00312     base(rhs) { }
00313 
00314   // Destructor
00315   ~CDDManager() { }
00316 
00317 };
00318 
00327 template<>
00328 class CDDManager<Cudd>:
00329   public CDDManagerBase<Cudd, Cudd> { 
00330 
00331 public:
00332 
00333   typedef Cudd manager_type;
00334   typedef Cudd storage_type;
00335   typedef CDDManagerBase<manager_type, storage_type> base;
00336   typedef CDDManager<storage_type> self;
00337 
00339   CDDManager(size_type nvars = 0): 
00340     base(nvars) { }
00341 
00342   // Destructor
00343   ~CDDManager() { }
00344 
00345 };
00346 
00347 
00355 template<>
00356 class CDDManager<CCuddInterface&>:
00357   public CDDManagerBase<CCuddInterface, const CCuddInterface&> { 
00358 
00359 public:
00360 
00361   typedef CCuddInterface manager_type;
00362   typedef const CCuddInterface& storage_type;
00363   typedef CDDManagerBase<manager_type, storage_type> base;
00364   typedef CDDManager<CCuddInterface&> self;
00365 
00367   CDDManager(const manager_type& rhs): 
00368     base(rhs) { }
00369 
00371   CDDManager(const dd_type& dd): 
00372     base(dd) { }
00373 
00375   CDDManager(const self& rhs): 
00376     base(rhs) { }
00377 
00378   // Destructor
00379   ~CDDManager() { }
00380 
00381 };
00382 
00383 
00391 template<>
00392 class CDDManager<CCuddInterface>:
00393   public CDDManagerBase<CCuddInterface, CCuddInterface> { 
00394 
00395 public:
00396 
00397   typedef CCuddInterface manager_type;
00398   typedef CCuddInterface storage_type;
00399   typedef CDDManagerBase<manager_type, storage_type> base;
00400   typedef CDDManager<storage_type> self;
00401 
00403   CDDManager(size_type nvars = 0): 
00404     base(nvars) { }
00405 
00406   CDDManager(const manager_type& rhs): 
00407     base(rhs) { }
00408 
00409   // Destructor
00410   ~CDDManager() { }
00411 
00412 };
00413 END_NAMESPACE_PBORI
00414 
00415 #endif // of #ifndef CDDManager_h_