Go to the documentation of this file.00001
00002
00096
00097
00098 #ifndef CDDManager_h_
00099 #define CDDManager_h_
00100 #include "cacheopts.h"
00101
00102 #include "pbori_defs.h"
00103 #include "pbori_traits.h"
00104
00105
00106 #include "CDDInterface.h"
00107
00108 #include "CCuddInterface.h"
00109
00110
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
00125
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
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
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
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
00410 ~CDDManager() { }
00411
00412 };
00413 END_NAMESPACE_PBORI
00414
00415 #endif // of #ifndef CDDManager_h_