CCuddInterface.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_ring_CCuddInterface_h_
#define polybori_ring_CCuddInterface_h_
// include basic definitions
#include <polybori/pbori_defs.h>
#include <polybori/cudd/cudd.h>
#include <polybori/cudd/cuddInt.h>
#include <polybori/routines/pbori_func.h> // handle_error
#include "CCallbackWrapper.h"
#include <vector>
#include <boost/intrusive_ptr.hpp>
#include <boost/scoped_array.hpp>
#include <boost/preprocessor/cat.hpp>
#include <boost/preprocessor/seq/for_each.hpp>
#include <boost/preprocessor/facilities/expand.hpp>
#include <boost/preprocessor/stringize.hpp>
#include <polybori/except/PBoRiError.h>
#include <stdexcept>
#include <algorithm>
#include <polybori/common/CWeakPtrFacade.h>
// get PBORI_PREFIX(cudd error) texts
inline const char* error_text(PBORI_PREFIX(DdManager)* mgr) {
switch (PBORI_PREFIX(Cudd_ReadErrorCode)(mgr)) {
case CUDD_MEMORY_OUT:
return("Out of memory.");
case CUDD_TOO_MANY_NODES:
return("To many nodes.");
case CUDD_MAX_MEM_EXCEEDED:
return("Maximum memory exceeded.");
case CUDD_INVALID_ARG:
return("Invalid argument.");
case CUDD_INTERNAL_ERROR:
return("Internal error.");
case CUDD_TIMEOUT_EXPIRED:
return("Timed out.");
case CUDD_NO_ERROR:
return("No error. (Should not reach here!)");
}
return("Unexpected error.");
}
inline void
intrusive_ptr_add_ref(PBORI_PREFIX(DdManager)* ptr){
++(ptr->hooks);
}
inline void
intrusive_ptr_release(PBORI_PREFIX(DdManager)* ptr) {
if (!(--(ptr->hooks))) {
PBORI_ASSERT(PBORI_PREFIX(Cudd_CheckZeroRef)(ptr) == 0);
PBORI_PREFIX(Cudd_Quit)(ptr);
}
}
BEGIN_NAMESPACE_PBORI
typedef PBORI_PREFIX(DdManager) DdManager;
#define PB_CUDDMGR_READ(count, data, funcname) data funcname() const { \
return BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
#define PB_CUDDMGR_SWITCH(count, data, funcname) void funcname() { \
BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this); }
#define PB_CUDDMGR_SET(count, data, funcname) void funcname(data arg) { \
BOOST_PP_CAT(PBORI_PREFIX(Cudd_), funcname)(*this, arg); }
class CCuddInterface:
public CTypes::auxtypes_type {
typedef CCuddInterface self;
public:
typedef DdNode* node_ptr;
typedef DdManager mgr_type;
typedef int cudd_idx_type;
typedef node_ptr (*unary_int_function)(mgr_type*, cudd_idx_type);
typedef node_ptr (*void_function)(mgr_type*);
typedef boost::intrusive_ptr<mgr_type> mgr_ptr;
CCuddInterface(size_type numVars, size_type numVarsZ,
size_type numSlots = PBORI_UNIQUE_SLOTS,
size_type cacheSize = PBORI_CACHE_SLOTS,
unsigned long maxMemory = PBORI_MAX_MEMORY):
p_mgr(init(numVars, numVarsZ, numSlots, cacheSize, maxMemory)),
m_vars(numVarsZ) {
for (idx_type idx = 0; size_type(idx) < numVarsZ; ++idx) initVar(m_vars[idx], idx);
}
CCuddInterface(const self& rhs): p_mgr(rhs.p_mgr), m_vars(rhs.m_vars) {
std::for_each(m_vars.begin(), m_vars.end(), PBORI_PREFIX(Cudd_Ref));
}
~CCuddInterface() {
std::for_each(m_vars.begin(), m_vars.end(),
callBack(&self::recursiveDeref));
}
mgr_type* getManager() const { return p_mgr.operator->(); }
mgr_ptr pManager() const { return p_mgr; }
self& operator=(const self & right) {
p_mgr = right.p_mgr;
return *this;
}
node_ptr zddVar(idx_type idx) const { return apply(PBORI_PREFIX(Cudd_zddIthVar), idx); }
node_ptr zddOne(idx_type iMax) const { return apply(PBORI_PREFIX(Cudd_ReadZddOne), iMax); }
node_ptr zddZero() const { return apply(PBORI_PREFIX(Cudd_ReadZero)); }
node_ptr zddOne() const {
return checkedResult(DD_ONE(getManager()));
}
#ifdef CUDD_ORIGINAL_INCLUSION
int ReorderingStatusZdd(PBORI_PREFIX(Cudd_ReorderingType) * method) const {
return PBORI_PREFIX(Cudd_ReorderingStatusZdd)(*this, method);
}
idx_type ReadPermZdd(idx_type idx) const {
return PBORI_PREFIX(Cudd_ReadPermZdd)(*this, idx);
}
idx_type ReadInvPermZdd(idx_type idx) const {
return PBORI_PREFIX(Cudd_ReadInvPermZdd)(*this, idx);
}
void AddHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
checkedResult(PBORI_PREFIX(Cudd_AddHook)(*this, f, where));
}
void RemoveHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) {
checkedResult(PBORI_PREFIX(Cudd_RemoveHook)(*this, f, where));
}
int IsInHook(DD_HFP f, PBORI_PREFIX(Cudd_HookType) where) const {
return PBORI_PREFIX(Cudd_IsInHook)(*this, f, where);
}
void EnableReorderingReporting() {
checkedResult(PBORI_PREFIX(Cudd_EnableReorderingReporting)(*this));
}
void DisableReorderingReporting() {
checkedResult(PBORI_PREFIX(Cudd_DisableReorderingReporting)(*this));
}
void DebugCheck(){ checkedResult(PBORI_PREFIX(Cudd_DebugCheck)(*this)); }
void CheckKeys(){ checkedResult(PBORI_PREFIX(Cudd_CheckKeys)(*this)); }
void PrintLinear() { checkedResult(PBORI_PREFIX(Cudd_PrintLinear)(*this)); }
int ReadLinear(int x, int y) { return PBORI_PREFIX(Cudd_ReadLinear)(*this, x, y); }
size_type Prime(size_type pr) const { return PBORI_PREFIX(Cudd_Prime)(pr); }
void PrintVersion(FILE * fp) const { std::cout.flush(); PBORI_PREFIX(Cudd_PrintVersion)(fp); }
void zddPrintSubtable() const{
std::cout.flush();
PBORI_PREFIX(Cudd_zddPrintSubtable)(*this);
}
void zddReduceHeap(PBORI_PREFIX(Cudd_ReorderingType) heuristic, int minsize) {
checkedResult(PBORI_PREFIX(Cudd_zddReduceHeap)(*this, heuristic, minsize));
}
void zddShuffleHeap(int * permutation) {
checkedResult(PBORI_PREFIX(Cudd_zddShuffleHeap)(*this, permutation));
}
void zddSymmProfile(int lower, int upper) const {
PBORI_PREFIX(Cudd_zddSymmProfile)(*this, lower, upper);
}
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, size_type,
(SetMinHit)(SetLooseUpTo)(SetMaxCacheHard)(SetMaxLive) )
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, int,
(SetSiftMaxVar)(SetSiftMaxSwap)(SetRecomb)(SetSymmviolation)
(SetArcviolation)(SetPopulationSize)(SetNumberXovers)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SET, FILE*, (SetStdout)(SetStderr))
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_SWITCH, BOOST_PP_NIL,
(zddRealignEnable)(zddRealignDisable)
(AutodynDisableZdd)
(EnableGarbageCollection)(DisableGarbageCollection)
(TurnOnCountDead)(TurnOffCountDead)(ClearErrorCode)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, double,
(ReadCacheUsedSlots)(ReadCacheLookUps)(ReadCacheHits)
(ReadSwapSteps)(ReadMaxGrowth)(AverageDistance)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, size_type,
(ReadCacheSlots)(ReadMinHit)(ReadLooseUpTo)(ReadMaxCache)
(ReadMaxCacheHard)(ReadSlots)(ReadKeys)(ReadDead)(ReadMinDead)
(ReadNextReordering)(ReadMaxLive)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,
(zddRealignmentEnabled)(ReadZddSize)(ReadReorderings)(ReadSiftMaxVar)
(ReadSiftMaxSwap)(ReadGarbageCollections)(GarbageCollectionEnabled)
(DeadAreCounted)(ReadRecomb)
(ReadPopulationSize)(ReadSymmviolation)(ReadArcviolation)
(ReadNumberXovers)(ReorderingReporting)(ReadErrorCode)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, long,
(ReadReorderingTime)(ReadGarbageCollectionTime)
(ReadPeakNodeCount)(zddReadNodeCount)
)
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, large_size_type,
(ReadMemoryInUse)(ReadMaxMemory) )
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, FILE*, (ReadStdout)(ReadStderr))
PB_CUDDMGR_SET(BOOST_PP_NIL, PBORI_PREFIX(Cudd_ReorderingType), AutodynEnableZdd)
PB_CUDDMGR_SET(BOOST_PP_NIL, unsigned long, SetMaxMemory)
PB_CUDDMGR_SET(BOOST_PP_NIL, double, SetMaxGrowth)
#else
BOOST_PP_SEQ_FOR_EACH(PB_CUDDMGR_READ, int,(ReadZddSize))
#endif
node_ptr getVar(idx_type idx) const {
if PBORI_UNLIKELY(size_type(idx) >= m_vars.size())
throw PBoRiError(CTypes::out_of_bounds);
return m_vars[idx];
}
size_type nVariables() const { return (size_type)ReadZddSize(); }
void cacheFlush() { PBORI_PREFIX(cuddCacheFlush)(*this); }
protected:
mgr_ptr init(size_type numVars,size_type numVarsZ, size_type numSlots,
size_type cacheSize, large_size_type maxMemory) {
DdManager* ptr = PBORI_PREFIX(Cudd_Init)(numVars, numVarsZ, numSlots, cacheSize, maxMemory);
if PBORI_UNLIKELY(ptr==NULL)
throw PBoRiError(CTypes::failed);
ptr->hooks = NULL; // abusing hooks pointer for reference counting
return ptr;
}
node_ptr checkedResult(node_ptr result) const {
checkedResult(int(result != NULL));
return result;
}
void checkedResult(int result) const {
if PBORI_UNLIKELY(result == 0) {
throw std::runtime_error(error_text(*this));
}
}
node_ptr apply(unary_int_function func, idx_type idx) const {
return checkedResult(func(*this, idx) );
}
node_ptr apply(void_function func) const {
return checkedResult(func(*this) );
}
protected:
void recursiveDeref(node_ptr node) const {
PBORI_PREFIX(Cudd_RecursiveDerefZdd)(*this, node);
}
void initVar(node_ptr& node, idx_type idx) const {
PBORI_PREFIX(Cudd_Ref)(node = PBORI_PREFIX(cuddUniqueInterZdd)(*this,
idx, zddOne(), zddZero()));
}
template <class MemberFuncPtr>
CCallbackWrapper<MemberFuncPtr>
callBack(MemberFuncPtr ptr) {
return CCallbackWrapper<MemberFuncPtr>(*this, ptr);
}
private:
operator mgr_type*() const { return getManager(); }
mgr_ptr p_mgr;
std::vector<node_ptr> m_vars;
}; // CCuddInterface
#undef PB_CUDDMGR_READ
#undef PB_CUDDMGR_SWITCH
#undef PB_CUDDMGR_SET
END_NAMESPACE_PBORI
#endif
PBORI_PREFIX
#define PBORI_PREFIX(name)
Definition: prefix.h:27
polybori::CCuddInterface::pManager
mgr_ptr pManager() const
Get (shared) pointer to initialized manager.
Definition: CCuddInterface.h:157
END_NAMESPACE_PBORI
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
polybori::CCuddInterface::cacheFlush
void cacheFlush()
clear all temporarily stored data
Definition: CCuddInterface.h:306
Cudd_IsInHook
#define Cudd_IsInHook
Definition: prefix_internal.h:123
polybori::CCuddInterface::apply
node_ptr apply(void_function func) const
Call function.
Definition: CCuddInterface.h:341
Cudd_Prime
#define Cudd_Prime
Definition: prefix_internal.h:162
polybori::CCuddInterface::checkedResult
void checkedResult(int result) const
Generate check numerical result of previous operation.
Definition: CCuddInterface.h:329
Cudd_ReorderingStatusZdd
#define Cudd_ReorderingStatusZdd
Definition: prefix_internal.h:37
BEGIN_NAMESPACE_PBORI
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
Cudd_ReadPermZdd
#define Cudd_ReadPermZdd
Definition: prefix_internal.h:93
polybori::CCuddInterface::CCuddInterface
CCuddInterface(const self &rhs)
Copy constructor.
Definition: CCuddInterface.h:143
Cudd_Quit
#define Cudd_Quit
Definition: prefix_internal.h:154
polybori::CCuddInterface::zddOne
node_ptr zddOne() const
Get 1-terminal for ZDDs.
Definition: CCuddInterface.h:175
Cudd_RecursiveDerefZdd
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
Cudd_zddIthVar
#define Cudd_zddIthVar
Definition: prefix_internal.h:148
cuddInt.h
polybori::CCuddInterface::zddOne
node_ptr zddOne(idx_type iMax) const
Get 1-terminal for ZDDs.
Definition: CCuddInterface.h:169
cuddUniqueInterZdd
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
DdManager
#define DdManager
Definition: prefix_internal.h:262
polybori::CCuddInterface::mgr_ptr
boost::intrusive_ptr< mgr_type > mgr_ptr
Smart pointer to Cudd manager.
Definition: CCuddInterface.h:130
PB_CUDDMGR_READ
#define PB_CUDDMGR_READ(count, data, funcname)
Definition: CCuddInterface.h:88
polybori::CCuddInterface::init
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
cuddCacheFlush
#define cuddCacheFlush
Definition: prefix_internal.h:185
pbori_func.h
polybori::CCallbackWrapper
This template class defines a functional, which wraps operator .*, which is the callback of a dynamic...
Definition: CCallbackWrapper.h:72
polybori::CAuxTypes
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
polybori::CCuddInterface::getVar
node_ptr getVar(idx_type idx) const
Definition: CCuddInterface.h:296
polybori::CCuddInterface
This class defines a C++ interface to CUDD's decicion diagram manager.
Definition: CCuddInterface.h:111
intrusive_ptr_release
void intrusive_ptr_release(pbori_DdManager *ptr)
Release current pointer by decrementing reference counting.
Definition: CCuddInterface.h:73
cudd.h
Cudd_AddHook
#define Cudd_AddHook
Definition: prefix_internal.h:152
pbori_defs.h
polybori::CCuddInterface::operator=
self & operator=(const self &right)
Assignment operation.
Definition: CCuddInterface.h:160
polybori::CCuddInterface::checkedResult
node_ptr checkedResult(node_ptr result) const
Generate check result of previous node operation and convert.
Definition: CCuddInterface.h:323
polybori::PBoRiError
This class is used for polybori's exception handling.
Definition: PBoRiError.h:31
polybori::CCuddInterface::~CCuddInterface
~CCuddInterface()
Destructor.
Definition: CCuddInterface.h:148
Cudd_Init
#define Cudd_Init
Definition: prefix_internal.h:155
polybori::CCuddInterface::node_ptr
DdNode * node_ptr
Type of Cudd's decision diagrams.
Definition: CCuddInterface.h:119
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
PB_CUDDMGR_SWITCH
#define PB_CUDDMGR_SWITCH(count, data, funcname)
Definition: CCuddInterface.h:91
polybori::CCuddInterface::callBack
CCallbackWrapper< MemberFuncPtr > callBack(MemberFuncPtr ptr)
Wrapping memeber function as functional.
Definition: CCuddInterface.h:360
Cudd_ReadInvPermZdd
#define Cudd_ReadInvPermZdd
Definition: prefix_internal.h:95
polybori::CCuddInterface::nVariables
size_type nVariables() const
Get number of managed variables.
Definition: CCuddInterface.h:303
polybori::CCuddInterface::initVar
void initVar(node_ptr &node, idx_type idx) const
Generate raw variable.
Definition: CCuddInterface.h:352
polybori::CCuddInterface::apply
node_ptr apply(unary_int_function func, idx_type idx) const
Apply function to given index.
Definition: CCuddInterface.h:336
polybori::CAuxTypes::idx_type
int idx_type
Type for indices.
Definition: pbori_defs.h:228
polybori::CCuddInterface::recursiveDeref
void recursiveDeref(node_ptr node) const
Dereferencing of diagram node.
Definition: CCuddInterface.h:347
PB_CUDDMGR_SET
#define PB_CUDDMGR_SET(count, data, funcname)
Definition: CCuddInterface.h:94
polybori::CCuddInterface::mgr_type
DdManager mgr_type
Type of Cudd decision diagram manager.
Definition: CCuddInterface.h:122
PBoRiError.h
Cudd_ReadZero
#define Cudd_ReadZero
Definition: prefix_internal.h:46
CWeakPtrFacade.h
polybori::CCuddInterface::cudd_idx_type
int cudd_idx_type
Definition: CCuddInterface.h:123
Cudd_ReadZddOne
#define Cudd_ReadZddOne
Definition: prefix_internal.h:45
CCallbackWrapper.h
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
Cudd_CheckZeroRef
#define Cudd_CheckZeroRef
Definition: prefix_internal.h:161
polybori::CCuddInterface::CCuddInterface
CCuddInterface(size_type numVars, size_type numVarsZ, size_type numSlots=256, size_type cacheSize=262144, unsigned long maxMemory=0)
Initialize CUDD-like decision diagram manager.
Definition: CCuddInterface.h:133
polybori::CAuxTypes::size_type
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
PBORI_MAX_MEMORY
#define PBORI_MAX_MEMORY
Definition: pbori_defs.h:40
polybori::CCuddInterface::zddVar
node_ptr zddVar(idx_type idx) const
Get ZDD variable.
Definition: CCuddInterface.h:166
Cudd_DisableReorderingReporting
#define Cudd_DisableReorderingReporting
Definition: prefix_internal.h:141
Cudd_ReadErrorCode
#define Cudd_ReadErrorCode
Definition: prefix_internal.h:126
Cudd_RemoveHook
#define Cudd_RemoveHook
Definition: prefix_internal.h:140
PBORI_UNLIKELY
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
PBORI_CACHE_SLOTS
#define PBORI_CACHE_SLOTS
Definition: pbori_defs.h:36
error_text
const char * error_text(pbori_DdManager *mgr)
Definition: CCuddInterface.h:45
PBORI_UNIQUE_SLOTS
#define PBORI_UNIQUE_SLOTS
Definition: pbori_defs.h:32
Cudd_EnableReorderingReporting
#define Cudd_EnableReorderingReporting
Definition: prefix_internal.h:153
intrusive_ptr_add_ref
void intrusive_ptr_add_ref(pbori_DdManager *ptr)
Increment reference count.
Definition: CCuddInterface.h:67
polybori::for_each
void for_each(InIter start, InIter finish, Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:857
polybori::CCuddInterface::zddZero
node_ptr zddZero() const
Get 0-terminal for ZDDs.
Definition: CCuddInterface.h:172
Cudd_Ref
#define Cudd_Ref
Definition: prefix_internal.h:157
polybori::CCuddInterface::getManager
mgr_type * getManager() const
Get pure CUDD structure.
Definition: CCuddInterface.h:154