16 #ifndef polybori_ring_CCuddInterface_h_
17 #define polybori_ring_CCuddInterface_h_
29 #include <boost/intrusive_ptr.hpp>
30 #include <boost/scoped_array.hpp>
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>
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:
60 return(
"No error. (Should not reach here!)");
62 return(
"Unexpected error.");
74 if (!(--(ptr->hooks))) {
88 #define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \
89 return BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
91 #define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \
92 BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
94 #define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \
95 BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this, arg); }
125 typedef node_ptr (*unary_int_function)(mgr_type*, cudd_idx_type);
126 typedef node_ptr (*void_function)(mgr_type*);
130 typedef boost::intrusive_ptr<mgr_type>
mgr_ptr;
137 p_mgr(init(numVars, numVarsZ, numSlots, cacheSize, maxMemory)),
139 for (
idx_type idx = 0;
size_type(idx) < numVarsZ; ++idx) initVar(m_vars[idx], idx);
150 callBack(&self::recursiveDeref));
176 return checkedResult(DD_ONE(getManager()));
179 #ifdef CUDD_ORIGINAL_INCLUSION
183 int ReorderingStatusZdd(
PBORI_PREFIX(Cudd_ReorderingType) * method)
const {
197 void AddHook(DD_HFP f,
PBORI_PREFIX(Cudd_HookType) where) {
200 void RemoveHook(DD_HFP f,
PBORI_PREFIX(Cudd_HookType) where) {
203 int IsInHook(DD_HFP f,
PBORI_PREFIX(Cudd_HookType) where)
const {
206 void EnableReorderingReporting() {
209 void DisableReorderingReporting() {
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)); }
217 int ReadLinear(
int x,
int y) {
return PBORI_PREFIX(Cudd_ReadLinear)(*
this, x, y); }
221 void PrintVersion(FILE * fp)
const { std::cout.flush();
PBORI_PREFIX(Cudd_PrintVersion)(fp); }
223 void zddPrintSubtable()
const{
228 void zddReduceHeap(
PBORI_PREFIX(Cudd_ReorderingType) heuristic,
int minsize) {
229 checkedResult(
PBORI_PREFIX(Cudd_zddReduceHeap)(*
this, heuristic, minsize));
231 void zddShuffleHeap(
int * permutation) {
232 checkedResult(
PBORI_PREFIX(Cudd_zddShuffleHeap)(*
this, permutation));
234 void zddSymmProfile(
int lower,
int upper)
const {
241 (SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) )
244 (SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation)
245 (SetArcviolation)(SetPopulationSize)(SetNumberXovers)
248 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr))
251 (zddRealignEnable)(zddRealignDisable)
253 (EnableGarbageCollection)(DisableGarbageCollection)
254 (TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode)
258 (ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits)
259 (ReadSwapSteps)(ReadMaxGrowth)(AverageDistance)
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)
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)
276 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ,
long,
277 (ReadReorderingTime)(ReadGarbageCollectionTime)
278 (ReadPeakNodeCount)(zddReadNodeCount)
281 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type,
282 (ReadMemoryInUse)(ReadMaxMemory) )
284 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr))
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)
293 BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ,
int,(ReadZddSize))
303 size_type
nVariables()
const {
return (size_type)ReadZddSize(); }
311 mgr_ptr
init(size_type numVars,size_type numVarsZ, size_type numSlots,
312 size_type cacheSize, large_size_type maxMemory) {
324 checkedResult(
int(result != NULL));
337 return checkedResult(func(*
this, idx) );
341 node_ptr
apply(void_function func)
const {
342 return checkedResult(func(*
this) );
354 idx, zddOne(), zddZero()));
358 template <
class MemberFuncPtr>
366 operator mgr_type*()
const {
return getManager(); }
372 std::vector<node_ptr> m_vars;
376 #undef PB_CUDDMGR_READ
377 #undef PB_CUDDMGR_SWITCH
378 #undef PB_CUDDMGR_SET
#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