PolyBoRi
|
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_