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