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

CDDManager.h

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

Generated on Tue Oct 5 2010 for PolyBoRi by  doxygen 1.7.1