PolyBoRi
CCuddInterface.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_ring_CCuddInterface_h_
17 #define polybori_ring_CCuddInterface_h_
18 
19 // include basic definitions
20 #include <polybori/pbori_defs.h>
21 
22 #include <polybori/cudd/cudd.h>
23 #include <polybori/cudd/cuddInt.h>
24 
25 #include <polybori/routines/pbori_func.h> // handle_error
26 #include "CCallbackWrapper.h"
27 
28 #include <vector>
29 #include <boost/intrusive_ptr.hpp>
30 #include <boost/scoped_array.hpp>
31 
32 #include <boost/preprocessor/cat.hpp>
33 #include <boost/preprocessor/seq/for_each.hpp>
34 #include <boost/preprocessor/facilities/expand.hpp>
35 #include <boost/preprocessor/stringize.hpp>
36 
38 
39 #include <stdexcept>
40 #include <algorithm>
41 
43 
44 // get PBORI_PREFIX(cudd error) texts
45 inline const char* error_text(PBORI_PREFIX(DdManager)* mgr) {
46  switch (PBORI_PREFIX(Cudd_ReadErrorCode)(mgr)) {
47  case CUDD_MEMORY_OUT:
48  return("Out of memory.");
49  case CUDD_TOO_MANY_NODES:
50  return("To many nodes.");
51  case CUDD_MAX_MEM_EXCEEDED:
52  return("Maximum memory exceeded.");
53  case CUDD_INVALID_ARG:
54  return("Invalid argument.");
55  case CUDD_INTERNAL_ERROR:
56  return("Internal error.");
57  case CUDD_TIMEOUT_EXPIRED:
58  return("Timed out.");
59  case CUDD_NO_ERROR:
60  return("No error. (Should not reach here!)");
61  }
62  return("Unexpected error.");
63  }
64 
66 inline void
68  ++(ptr->hooks);
69 }
70 
72 inline void
74  if (!(--(ptr->hooks))) {
75 
77  PBORI_PREFIX(Cudd_Quit)(ptr);
78  }
79 }
80 
81 
83 
85 
87 
88 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \
89  return BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
90 
91 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \
92  BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
93 
94 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \
95  BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this, arg); }
96 
97 
112  public CTypes::auxtypes_type {
113 
115  typedef CCuddInterface self;
116 
117 public:
119  typedef DdNode* node_ptr;
120 
122  typedef DdManager mgr_type;
123  typedef int cudd_idx_type;
124 
125  typedef node_ptr (*unary_int_function)(mgr_type*, cudd_idx_type);
126  typedef node_ptr (*void_function)(mgr_type*);
127 
128 
130  typedef boost::intrusive_ptr<mgr_type> mgr_ptr;
131 
133  CCuddInterface(size_type numVars, size_type numVarsZ,
134  size_type numSlots = PBORI_UNIQUE_SLOTS,
135  size_type cacheSize = PBORI_CACHE_SLOTS,
136  unsigned long maxMemory = PBORI_MAX_MEMORY):
137  p_mgr(init(numVars, numVarsZ, numSlots, cacheSize, maxMemory)),
138  m_vars(numVarsZ) {
139  for (idx_type idx = 0; size_type(idx) < numVarsZ; ++idx) initVar(m_vars[idx], idx);
140  }
141 
143  CCuddInterface(const self& rhs): p_mgr(rhs.p_mgr), m_vars(rhs.m_vars) {
144  std::for_each(m_vars.begin(), m_vars.end(), PBORI_PREFIX(Cudd_Ref));
145  }
146 
149  std::for_each(m_vars.begin(), m_vars.end(),
150  callBack(&self::recursiveDeref));
151  }
152 
154  mgr_type* getManager() const { return p_mgr.operator->(); }
155 
157  mgr_ptr pManager() const { return p_mgr; }
158 
160  self& operator=(const self & right) {
161  p_mgr = right.p_mgr;
162  return *this;
163  }
164 
166  node_ptr zddVar(idx_type idx) const { return apply(PBORI_PREFIX(Cudd_zddIthVar), idx); }
167 
169  node_ptr zddOne(idx_type iMax) const { return apply(PBORI_PREFIX(Cudd_ReadZddOne), iMax); }
170 
172  node_ptr zddZero() const { return apply(PBORI_PREFIX(Cudd_ReadZero)); }
173 
175  node_ptr zddOne() const {
176  return checkedResult(DD_ONE(getManager()));
177  }
178 
179 #ifdef CUDD_ORIGINAL_INCLUSION
180 
183  int ReorderingStatusZdd(PBORI_PREFIX(Cudd_ReorderingType) * method) const {
184  return PBORI_PREFIX(Cudd_ReorderingStatusZdd)(*this, method);
185  }
186 
188  idx_type ReadPermZdd(idx_type idx) const {
189  return PBORI_PREFIX(Cudd_ReadPermZdd)(*this, idx);
190  }
191 
193  idx_type ReadInvPermZdd(idx_type idx) const {
194  return PBORI_PREFIX(Cudd_ReadInvPermZdd)(*this, idx);
195  }
196 
197  void AddHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
198  checkedResult(PBORI_PREFIX(Cudd_AddHook)(*this, f, where));
199  }
200  void RemoveHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
201  checkedResult(PBORI_PREFIX(Cudd_RemoveHook)(*this, f, where));
202  }
203  int IsInHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) const {
204  return PBORI_PREFIX(Cudd_IsInHook)(*this, f, where);
205  }
206  void EnableReorderingReporting() {
207  checkedResult(PBORI_PREFIX(Cudd_EnableReorderingReporting)(*this));
208  }
209  void DisableReorderingReporting() {
210  checkedResult(PBORI_PREFIX(Cudd_DisableReorderingReporting)(*this));
211  }
212 
213  void DebugCheck(){ checkedResult(PBORI_PREFIX(Cudd_DebugCheck)(*this)); }
214  void CheckKeys(){ checkedResult(PBORI_PREFIX(Cudd_CheckKeys)(*this)); }
215  void PrintLinear() { checkedResult(PBORI_PREFIX(Cudd_PrintLinear)(*this)); }
216 
217  int ReadLinear(int x, int y) { return PBORI_PREFIX(Cudd_ReadLinear)(*this, x, y); }
218 
219  size_type Prime(size_type pr) const { return PBORI_PREFIX(Cudd_Prime)(pr); }
220 
221  void PrintVersion(FILE * fp) const { std::cout.flush(); PBORI_PREFIX(Cudd_PrintVersion)(fp); }
222 
223  void zddPrintSubtable() const{
224  std::cout.flush();
225  PBORI_PREFIX(Cudd_zddPrintSubtable)(*this);
226  }
227 
228  void zddReduceHeap(PBORI_PREFIX(Cudd_ReorderingType) heuristic, int minsize) {
229  checkedResult(PBORI_PREFIX(Cudd_zddReduceHeap)(*this, heuristic, minsize));
230  }
231  void zddShuffleHeap(int * permutation) {
232  checkedResult(PBORI_PREFIX(Cudd_zddShuffleHeap)(*this, permutation));
233  }
234  void zddSymmProfile(int lower, int upper) const {
235  PBORI_PREFIX(Cudd_zddSymmProfile)(*this, lower, upper);
236  }
237 
240  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type,
241  (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) )
242 
243  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int,
244  (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation)
245  (SetArcviolation)(SetPopulationSize)(SetNumberXovers)
246  )
247 
248  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr))
249 
250  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL,
251  (zddRealignEnable)(zddRealignDisable)
252  (AutodynDisableZdd)
253  (EnableGarbageCollection)(DisableGarbageCollection)
254  (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode)
255  )
256 
257  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double,
258  (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits)
259  (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance)
260  )
261 
262  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type,
263  (ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache)
264  (ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead)
265  (ReadNextReordering)(ReadMaxLive)
266  )
267 
268  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,
269  (zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar)
270  (ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled)
271  (DeadAreCounted)(ReadRecomb)
272  (ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation)
273  (ReadNumberXovers)(ReorderingReporting)(ReadErrorCode)
274  )
275 
276  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long,
277  (ReadReorderingTime)(ReadGarbageCollectionTime)
278  (ReadPeakNodeCount)(zddReadNodeCount)
279  )
280 
281  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type,
282  (ReadMemoryInUse)(ReadMaxMemory) )
283 
284  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr))
285 
286  PB_CUDDMGR_SET(BOOST_PP_NIL, PBORI_PREFIX(Cudd_ReorderingType), AutodynEnableZdd)
287  PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory)
288  PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth)
290 
292 #else
293  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,(ReadZddSize))
294 #endif
295 
296  node_ptr getVar(idx_type idx) const {
297  if PBORI_UNLIKELY(size_type(idx) >= m_vars.size())
298  throw PBoRiError(CTypes::out_of_bounds);
299  return m_vars[idx];
300  }
301 
303  size_type nVariables() const { return (size_type)ReadZddSize(); }
304 
307 
308 protected:
309 
311  mgr_ptr init(size_type numVars,size_type numVarsZ, size_type numSlots,
312  size_type cacheSize, large_size_type maxMemory) {
313 
314  DdManager* ptr = PBORI_PREFIX(Cudd_Init)(numVars, numVarsZ, numSlots, cacheSize, maxMemory);
315  if PBORI_UNLIKELY(ptr==NULL)
316  throw PBoRiError(CTypes::failed);
317 
318  ptr->hooks = NULL; // abusing hooks pointer for reference counting
319 
320  return ptr;
321  }
323  node_ptr checkedResult(node_ptr result) const {
324  checkedResult(int(result != NULL));
325  return result;
326  }
327 
329  void checkedResult(int result) const {
330  if PBORI_UNLIKELY(result == 0) {
331  throw std::runtime_error(error_text(*this));
332  }
333  }
334 
336  node_ptr apply(unary_int_function func, idx_type idx) const {
337  return checkedResult(func(*this, idx) );
338  }
339 
341  node_ptr apply(void_function func) const {
342  return checkedResult(func(*this) );
343  }
344 
345 protected:
347  void recursiveDeref(node_ptr node) const {
348  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(*this, node);
349  }
350 
352  void initVar(node_ptr& node, idx_type idx) const {
354  idx, zddOne(), zddZero()));
355  }
356 
358  template <class MemberFuncPtr>
360  callBack(MemberFuncPtr ptr) {
361  return CCallbackWrapper<MemberFuncPtr>(*this, ptr);
362  }
363 
364 private:
366  operator mgr_type*() const { return getManager(); }
367 
369  mgr_ptr p_mgr;
370 
372  std::vector<node_ptr> m_vars;
373 }; // CCuddInterface
374 
375 
376 #undef PB_CUDDMGR_READ
377 #undef PB_CUDDMGR_SWITCH
378 #undef PB_CUDDMGR_SET
379 
381 
382 #endif
383 
384 
#define PBORI_PREFIX(name)
Definition: prefix.h:27
mgr_ptr pManager() const
Get (shared) pointer to initialized manager.
Definition: CCuddInterface.h:157
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
void cacheFlush()
clear all temporarily stored data
Definition: CCuddInterface.h:306
#define Cudd_IsInHook
Definition: prefix_internal.h:123
node_ptr apply(void_function func) const
Call function.
Definition: CCuddInterface.h:341
#define Cudd_Prime
Definition: prefix_internal.h:162
void checkedResult(int result) const
Generate check numerical result of previous operation.
Definition: CCuddInterface.h:329
#define Cudd_ReorderingStatusZdd
Definition: prefix_internal.h:37
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
#define Cudd_ReadPermZdd
Definition: prefix_internal.h:93
CCuddInterface(const self &rhs)
Copy constructor.
Definition: CCuddInterface.h:143
#define Cudd_Quit
Definition: prefix_internal.h:154
node_ptr zddOne() const
Get 1-terminal for ZDDs.
Definition: CCuddInterface.h:175
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
#define Cudd_zddIthVar
Definition: prefix_internal.h:148
node_ptr zddOne(idx_type iMax) const
Get 1-terminal for ZDDs.
Definition: CCuddInterface.h:169
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
#define DdManager
Definition: prefix_internal.h:262
boost::intrusive_ptr< mgr_type > mgr_ptr
Smart pointer to Cudd manager.
Definition: CCuddInterface.h:130
#define PB_CUDDMGR_READ(count, data, funcname)
Definition: CCuddInterface.h:88
mgr_ptr init(size_type numVars, size_type numVarsZ, size_type numSlots, size_type cacheSize, large_size_type maxMemory)
initialized CUDD decision diagrma manager, check it and start reference counting
Definition: CCuddInterface.h:311
#define cuddCacheFlush
Definition: prefix_internal.h:185
This template class defines a functional, which wraps operator .*, which is the callback of a dynamic...
Definition: CCallbackWrapper.h:72
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
node_ptr getVar(idx_type idx) const
Definition: CCuddInterface.h:296
This class defines a C++ interface to CUDD's decicion diagram manager.
Definition: CCuddInterface.h:111
void intrusive_ptr_release(pbori_DdManager *ptr)
Release current pointer by decrementing reference counting.
Definition: CCuddInterface.h:73
#define Cudd_AddHook
Definition: prefix_internal.h:152
self & operator=(const self &right)
Assignment operation.
Definition: CCuddInterface.h:160
node_ptr checkedResult(node_ptr result) const
Generate check result of previous node operation and convert.
Definition: CCuddInterface.h:323
CCuddInterface(size_type numVars, size_type numVarsZ, size_type numSlots=CUDD_UNIQUE_SLOTS, size_type cacheSize=CUDD_CACHE_SLOTS, unsigned long maxMemory=0)
Initialize CUDD-like decision diagram manager.
Definition: CCuddInterface.h:133
This class is used for polybori's exception handling.
Definition: PBoRiError.h:31
~CCuddInterface()
Destructor.
Definition: CCuddInterface.h:148
#define Cudd_Init
Definition: prefix_internal.h:155
DdNode * node_ptr
Type of Cudd's decision diagrams.
Definition: CCuddInterface.h:119
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
#define PB_CUDDMGR_SWITCH(count, data, funcname)
Definition: CCuddInterface.h:91
CCallbackWrapper< MemberFuncPtr > callBack(MemberFuncPtr ptr)
Wrapping memeber function as functional.
Definition: CCuddInterface.h:360
#define Cudd_ReadInvPermZdd
Definition: prefix_internal.h:95
size_type nVariables() const
Get number of managed variables.
Definition: CCuddInterface.h:303
void initVar(node_ptr &node, idx_type idx) const
Generate raw variable.
Definition: CCuddInterface.h:352
node_ptr apply(unary_int_function func, idx_type idx) const
Apply function to given index.
Definition: CCuddInterface.h:336
int idx_type
Type for indices.
Definition: pbori_defs.h:228
void recursiveDeref(node_ptr node) const
Dereferencing of diagram node.
Definition: CCuddInterface.h:347
#define PB_CUDDMGR_SET(count, data, funcname)
Definition: CCuddInterface.h:94
DdManager mgr_type
Type of Cudd decision diagram manager.
Definition: CCuddInterface.h:122
#define Cudd_ReadZero
Definition: prefix_internal.h:46
int cudd_idx_type
Definition: CCuddInterface.h:123
#define Cudd_ReadZddOne
Definition: prefix_internal.h:45
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_CheckZeroRef
Definition: prefix_internal.h:161
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
#define PBORI_MAX_MEMORY
Definition: pbori_defs.h:40
node_ptr zddVar(idx_type idx) const
Get ZDD variable.
Definition: CCuddInterface.h:166
#define Cudd_DisableReorderingReporting
Definition: prefix_internal.h:141
#define Cudd_ReadErrorCode
Definition: prefix_internal.h:126
#define Cudd_RemoveHook
Definition: prefix_internal.h:140
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
#define PBORI_CACHE_SLOTS
Definition: pbori_defs.h:36
const char * error_text(pbori_DdManager *mgr)
Definition: CCuddInterface.h:45
#define PBORI_UNIQUE_SLOTS
Definition: pbori_defs.h:32
#define Cudd_EnableReorderingReporting
Definition: prefix_internal.h:153
void intrusive_ptr_add_ref(pbori_DdManager *ptr)
Increment reference count.
Definition: CCuddInterface.h:67
void for_each(InIter start, InIter finish, Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:857
node_ptr zddZero() const
Get 0-terminal for ZDDs.
Definition: CCuddInterface.h:172
#define Cudd_Ref
Definition: prefix_internal.h:157
mgr_type * getManager() const
Get pure CUDD structure.
Definition: CCuddInterface.h:154