PolyBoRi
CCuddInterface.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
70 //*****************************************************************************
71 
72 
73 // include basic definitions
74 
75 #include "CCuddZDD.h"
76 
77 #ifndef CCuddInterface_h_
78 #define CCuddInterface_h_
79 
81 
83 
84 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \
85  return BOOST_PP_CAT(Cudd_, funcname)(getManager()); }
86 
87 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \
88  BOOST_PP_CAT(Cudd_, funcname)(getManager()); }
89 
90 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \
91  BOOST_PP_CAT(Cudd_, funcname)(getManager(), arg); }
92 
93 
108 
109 public:
110 
112 
113 
114 
117  typedef core_type::mgrcore_ptr mgrcore_ptr;
118  typedef CCuddZDD dd_type;
119  typedef self tmp_ref;
121 
124 
126  typedef variable_names_type::const_reference const_varname_reference;
127 
130  size_type numVarsZ = 0,
131  size_type numSlots = CUDD_UNIQUE_SLOTS,
132  size_type cacheSize = CUDD_CACHE_SLOTS,
133  unsigned long maxMemory = 0):
134  pMgr (new core_type(numVars, numVarsZ, numSlots, cacheSize, maxMemory)) {
135  }
136 
138  CCuddInterface(const self& rhs): pMgr(rhs.pMgr) {}
139 
141  CCuddInterface(mgrcore_ptr rhs): pMgr(rhs) {};
142 
145 
148  errorfunc_type oldHandler = pMgr->errorHandler;
149  pMgr->errorHandler = newHandler;
150  return oldHandler;
151  }
152 
154  errorfunc_type getHandler() const { return pMgr->errorHandler; }
155 
157  mgrcore_type getManager() const { return pMgr->manager; }
158 
160  mgrcore_ptr managerCore() const { return pMgr; }
161 
163 
164  void makeVerbose() { pMgr->verbose = true; }
165  void makeTerse() { pMgr->verbose = false; }
166  bool isVerbose() const { return pMgr->verbose; }
168 
170  void info() const { checkedResult(Cudd_PrintInfo(getManager(),stdout)); }
171 
172  void checkReturnValue(const node_type result) const {
173  checkReturnValue(result != NULL);
174  }
175  void checkReturnValue(const int result) const {
176  if UNLIKELY(result == 0) {
177  handle_error<CUDD_MEMORY_OUT> tmp(pMgr->errorHandler);
178  tmp(Cudd_ReadErrorCode(getManager()));
179  }
180  }
181 
183  self& operator=(const self & right) {
184  pMgr = right.pMgr;
185  return *this;
186  }
187 
189  CCuddZDD zddVar(idx_type idx) const { return apply(Cudd_zddIthVar, idx); }
190 
192  CCuddZDD zddOne(idx_type iMax) const { return apply(Cudd_ReadZddOne, iMax); }
193 
195  CCuddZDD zddZero() const { return apply(Cudd_ReadZero); }
196 
198  CCuddZDD zddOne() const {
199  return checkedResult(DD_ONE(getManager()));
200  }
201 
204 
205  int ReorderingStatusZdd(Cudd_ReorderingType * method) const {
206  return Cudd_ReorderingStatusZdd(getManager(), method);
207  }
208 
210  return Cudd_ReadPermZdd(getManager(), i);
211  }
212 
214  return Cudd_ReadInvPermZdd(getManager(), i);
215  }
216 
217  void AddHook(DD_HFP f, Cudd_HookType where) {
218  checkedResult(Cudd_AddHook(getManager(), f, where));
219  }
220  void RemoveHook(DD_HFP f, Cudd_HookType where) {
221  checkedResult(Cudd_RemoveHook(getManager(), f, where));
222  }
223  int IsInHook(DD_HFP f, Cudd_HookType where) const {
224  return Cudd_IsInHook(getManager(), f, where);
225  }
227  checkedResult(Cudd_EnableReorderingReporting(getManager()));
228  }
230  checkedResult(Cudd_DisableReorderingReporting(getManager()));
231  }
232 
233  void DebugCheck(){ checkedResult(Cudd_DebugCheck(getManager())); }
234  void CheckKeys(){ checkedResult(Cudd_CheckKeys(getManager())); }
235  void PrintLinear() { checkedResult(Cudd_PrintLinear(getManager())); }
236 
237  int ReadLinear(int x, int y) { return Cudd_ReadLinear(getManager(), x, y); }
238 
239  size_type Prime(size_type pr) const { return Cudd_Prime(pr); }
240 
241  void PrintVersion(FILE * fp) const { cout.flush(); Cudd_PrintVersion(fp); }
242 
243  MtrNode* MakeZddTreeNode(size_type low, size_type size, size_type type) {
244  return Cudd_MakeZddTreeNode(getManager(), low, size, type);
245  }
246  void zddPrintSubtable() const{
247  cout.flush();
248  Cudd_zddPrintSubtable(getManager());
249  }
250 
251  void zddReduceHeap(Cudd_ReorderingType heuristic, int minsize) {
252  checkedResult(Cudd_zddReduceHeap(getManager(), heuristic, minsize));
253  }
254  void zddShuffleHeap(int * permutation) {
255  checkedResult(Cudd_zddShuffleHeap(getManager(), permutation));
256  }
257  void zddSymmProfile(int lower, int upper) const {
258  Cudd_zddSymmProfile(getManager(), lower, upper);
259  }
260 
261  int SharingSize(dd_type* nodes, int nlen) const {
262  typedef boost::scoped_array<node_type> node_array;
263  node_array nodeArray(new node_type[nlen]);
264  std::transform(nodes, nodes + nlen, nodeArray.get(), get_node<dd_type>());
265 
266  return checkedResult(Cudd_SharingSize(nodeArray.get(), nlen));
267  }
268 
271  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type,
272  (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) )
273 
274  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int,
275  (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation)
276  (SetArcviolation)(SetPopulationSize)(SetNumberXovers)
277  )
278 
279  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr))
280 
281  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL,
282  (zddRealignEnable)(zddRealignDisable)
283  (AutodynDisableZdd)(FreeZddTree)
284  (EnableGarbageCollection)(DisableGarbageCollection)
285  (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode)
286  )
287 
288  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double,
289  (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits)
290  (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance)
291  )
292 
293  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type,
294  (ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache)
295  (ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead)
296  (ReadNextReordering)(ReadMaxLive)
297  )
298 
299  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,
300  (zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar)
301  (ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled)
302  (DeadAreCounted)(ReadRecomb)
303  (ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation)
304  (ReadNumberXovers)(ReorderingReporting)(ReadErrorCode)
305  )
306 
307  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long,
308  (ReadReorderingTime)(ReadGarbageCollectionTime)
309  (ReadPeakNodeCount)(zddReadNodeCount)
310  )
311 
312  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type,
313  (ReadMemoryInUse)(ReadMaxMemory) )
314 
315  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr))
316 
317  BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, MtrNode*, (ReadZddTree))
318 
319  PB_CUDDMGR_SET(BOOST_PP_NIL, Cudd_ReorderingType, AutodynEnableZdd)
320  PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory)
321  PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth)
322  PB_CUDDMGR_SET(BOOST_PP_NIL, MtrNode*, SetZddTree)
324 
325 
326 
328  void setName(idx_type idx, const_varname_reference varname) {
329  (pMgr->m_names).set(idx, varname);
330  }
331 
334  return (pMgr->m_names)[idx];
335  }
336 
337  dd_type getVar(idx_type idx) const {
338  assert(idx < pMgr->m_vars.size());
339  return getDiagram(pMgr->m_vars[idx]);
340  }
341 
344  return Cudd_ReadZddSize(getManager());
345  }
346 
347 protected:
349  dd_type getDiagram(node_type result) const {
350  return dd_type(managerCore(), result);
351  }
352 
354  dd_type checkedResult(node_type result) const {
355  checkReturnValue(result);
356  return getDiagram(result);
357  }
358 
360  idx_type checkedResult(idx_type result) const {
361  checkReturnValue(result);
362  return result;
363  }
364 
367  return checkedResult(func(getManager(), idx) );
368  }
369 
371  dd_type apply(void_function func) const {
372  return checkedResult(func(getManager()) );
373  }
374 
375 private:
376  mgrcore_ptr pMgr;
377 }; // CCuddInterface
378 
379 
380 #undef PB_CUDDMGR_READ
381 #undef PB_CUDDMGR_SWITCH
382 #undef PB_CUDDMGR_SET
383 
385 
386 #endif
387 
388