00001
00002
00099
00100
00101 #ifndef CDDManager_h_
00102 #define CDDManager_h_
00103 #include "cacheopts.h"
00104
00105 #include "pbori_defs.h"
00106 #include "pbori_traits.h"
00107
00108
00109 #include "CDDInterface.h"
00110
00111 #include "CCuddInterface.h"
00112
00113
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
00128
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
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
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
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
00413 ~CDDManager() { }
00414
00415 };
00416 END_NAMESPACE_PBORI
00417
00418 #endif // of #ifndef CDDManager_h_