PolyBoRi
CDDManager.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
96 //*****************************************************************************
97 
98 #ifndef CDDManager_h_
99 #define CDDManager_h_
100 #include "cacheopts.h"
101 // load basic definitions
102 #include "pbori_defs.h"
103 #include "pbori_traits.h"
104 
105 // get decision diagram definitions.
106 #include "CDDInterface.h"
107 
108 #include "CCuddInterface.h"
109 
110 // get standard map functionality
111 #include <map>
112 
113 
114 #ifndef PBORI_UNIQUE_SLOTS
115 # define PBORI_UNIQUE_SLOTS CUDD_UNIQUE_SLOTS // initial size of subtables
116 #endif
117 
118 #ifndef PBORI_CACHE_SLOTS
119 # define PBORI_CACHE_SLOTS CUDD_CACHE_SLOTS // default size of the cache
120 #endif
121 
122 #ifndef PBORI_MAX_MEMORY
123 # define PBORI_MAX_MEMORY 0 // target maximum memory occupation
124  // if PBORI_MAX_MEMORY == 0 then
125  // guess based on the available memory
126 #endif
127 
128 
130 
131 
132 inline ZDD
133 fetch_diagram(const Cudd& mgr, const ZDD& rhs) {
134  return ZDD(&const_cast<Cudd&>(mgr), rhs.getNode());
135 }
136 
137 template <class MgrType, class DDType>
138 inline const DDType&
139 fetch_diagram(const MgrType& mgr, const DDType& rhs) {
140  return rhs;
141 }
142 
143 inline Cudd&
144 fetch_manager(const Cudd& mgr) {
145  return const_cast<Cudd&>(mgr);
146 }
147 
148 template <class MgrType>
149 inline const MgrType&
150 fetch_manager(const MgrType& mgr) {
151  return mgr;
152 }
153 
154 
164 template <class CuddLikeManType, class StorageType>
166  public:
167 
169  typedef CuddLikeManType interfaced_type;
170 
172  typedef StorageType interfaced_store;
173 
176 
179 
182 
185 
188 
190  typedef std::map<idx_type, dd_base> persistent_cache_type;
191 
194 
197 
200  size_type numSlots = PBORI_UNIQUE_SLOTS,
201  size_type cacheSize = PBORI_CACHE_SLOTS,
202  unsigned long maxMemory = PBORI_MAX_MEMORY):
203  m_interfaced(0, nvars, numSlots, cacheSize, maxMemory) { }
204 
206  CDDManagerBase(const self& rhs):
207  m_interfaced(rhs.m_interfaced) {
208  }
209 
212  m_interfaced(fetch_manager(rhs)) { }
213 
215  CDDManagerBase(const dd_type& dd):
216  m_interfaced(dd.manager()) { }
217 
220 
222  dd_base fetchDiagram(const dd_base& rhs) const {
223  return fetch_diagram(manager(), rhs);
224  }
225 
227  dd_base ddVariable(idx_type nvar) const {
228  return manager().zddVar(nvar);
229  }
230 
232  dd_base variable(idx_type nvar) const {
233  return blank().change(nvar);
234  }
235 
238  return manager().getVar(nvar);
239  }
240 
243  return manager().nVariables();
244  }
245 
248  dd_type empty() const { return manager().zddZero(); }
249 
252  dd_type blank() const { return manager().zddOne(nVariables()); }
253 
255  operator interfaced_type&() { return m_interfaced; }
256 
258  operator const interfaced_type&() const { return m_interfaced; }
259 
261  interfaced_type& manager() { return m_interfaced; }
262 
264  const interfaced_type& manager() const { return m_interfaced; }
265 
267  void printInfo() const { manager().info(); }
268 
271  manager().setName(idx, varname);
272  }
273 
276  return manager().getName(idx);
277  }
278 
279 private:
281  mutable interfaced_store m_interfaced;
282 };
283 
291 template<>
292 class CDDManager<Cudd&>:
294 
295 public:
296 
297  typedef Cudd manager_type;
298  typedef Cudd& storage_type;
301 
303  CDDManager(manager_type& rhs):
304  base(rhs) { }
305 
307  CDDManager(const dd_type& dd):
308  base(dd) { }
309 
311  CDDManager(const self& rhs):
312  base(rhs) { }
313 
314  // Destructor
316 
317 };
318 
327 template<>
328 class CDDManager<Cudd>:
329  public CDDManagerBase<Cudd, Cudd> {
330 
331 public:
332 
333  typedef Cudd manager_type;
334  typedef Cudd storage_type;
337 
339  CDDManager(size_type nvars = 0):
340  base(nvars) { }
341 
342  // Destructor
344 
345 };
346 
347 
355 template<>
358 
359 public:
360 
362  typedef const CCuddInterface& storage_type;
365 
367  CDDManager(const manager_type& rhs):
368  base(rhs) { }
369 
371  CDDManager(const dd_type& dd):
372  base(dd) { }
373 
375  CDDManager(const self& rhs):
376  base(rhs) { }
377 
378  // Destructor
380 
381 };
382 
383 
391 template<>
393  public CDDManagerBase<CCuddInterface, CCuddInterface> {
394 
395 public:
396 
401 
403  CDDManager(size_type nvars = 0):
404  base(nvars) { }
405 
406  CDDManager(const manager_type& rhs):
407  base(rhs) { }
408 
409  // Destructor
411 
412 };
414 
415 #endif // of #ifndef CDDManager_h_