16 #ifndef polybori_cache_CCacheManagement_h_
17 #define polybori_cache_CCacheManagement_h_
26 #include <boost/intrusive_ptr.hpp>
40 template <
class TagType>
107 template <
class TagType>
115 template <
class BaseTag>
131 template <
unsigned Counted,
unsigned Offset = 18>
135 ( ((Counted + Offset) & 0x3 ) << 2) |
136 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
144 template <
class MgrType>
177 manager_type
manager()
const {
return m_mgr; }
181 return dd_type(m_mgr, navi);
186 return ring_type(m_mgr).one();
190 return ring_type(m_mgr).zero();
193 ring_type
ring()
const {
return ring_type(manager()); }
197 return m_mgr.getManager();
218 template <
class ManagerType,
class CacheType,
unsigned ArgumentLength>
222 template <
class CacheType,
unsigned ArgumentLength>
230 template <
class CacheType,
unsigned ArgumentLength>
237 template <
class CacheType,
unsigned ArgumentLength>
243 template <
class ManagerType,
class CacheType>
245 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
266 navigator
find(navigator, ...)
const {
return navigator(); }
267 node_type
find(node_type, ...)
const {
return NULL; }
274 template <
class ManagerType,
class CacheType>
276 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
296 node_type
find(node_type node)
const {
301 navigator
find(navigator node)
const {
306 void insert(node_type node, node_type result)
const {
313 void insert(navigator node, navigator result)
const {
314 insert(node.getNode(), result.getNode());
319 using base::internalManager;
323 static node_type cache_dummy(
typename base::internal_manager_type,node_type){
329 template <
class ManagerType,
class CacheType>
331 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
351 node_type
find(node_type first, node_type second)
const {
355 navigator
find(navigator first, navigator second)
const {
360 void insert(node_type first, node_type second, node_type result)
const {
367 void insert(navigator first, navigator second, navigator result)
const {
368 insert(first.getNode(), second.getNode(), result.getNode());
373 using base::internalManager;
377 static node_type cache_dummy(
typename base::internal_manager_type,
378 node_type, node_type){
384 template <
class ManagerType,
class CacheType>
386 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
406 node_type
find(node_type first, node_type second, node_type third)
const {
408 first, second, third);
412 navigator
find(navigator first, navigator second, navigator third)
const {
418 void insert(node_type first, node_type second, node_type third,
419 node_type result)
const {
422 first, second, third, result);
426 void insert(navigator first, navigator second, navigator third,
427 navigator result)
const {
428 insert(first.getNode(), second.getNode(), third.getNode(),
434 using base::internalManager;
437 enum { GENERIC_DD_TAG =
453 template <
class ManagerType,
class CacheType,
454 unsigned ArgumentLength = CacheType::nargs>
457 CacheType, ArgumentLength> {
467 enum { nargs = ArgumentLength };
487 template <
class ManagerType,
class CacheType>
510 node_type
find(node_type first, node_type second)
const {
511 if ( std::less<node_type>()(first, second) )
512 return base::find(first, second);
514 return base::find(second, first);
518 navigator
find(navigator first, navigator second)
const {
524 void insert(node_type first, node_type second, node_type result)
const {
525 if ( std::less<node_type>()(first, second) )
526 base::insert(first, second, result);
528 base::insert(second, first, result);
532 void insert(navigator first, navigator second, navigator result)
const {
533 insert(first.getNode(), second.getNode(), result.getNode());
#define PBORI_PREFIX(name)
Definition: prefix.h:27
Definition: CCacheManagement.h:330
Definition: CCacheManagement.h:32
base::node_type node_type
Extracting inherited node type.
Definition: CCacheManagement.h:474
Definition: CCacheManagement.h:100
ring_type::dd_type dd_type
Get high-level decision diagram type.
Definition: CCacheManagement.h:167
dd_type zero() const
Get constant zero.
Definition: CCacheManagement.h:189
lead_tag< dlex_tag > dlex_lead
Definition: CCacheManagement.h:82
base::node_type node_type
Definition: CCacheManagement.h:342
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
node_type find(node_type,...) const
Definition: CCacheManagement.h:267
Definition: CCacheManagement.h:56
This template forms the base for CCacheManagement. It implements routines for finding and inserting r...
Definition: CCacheManagement.h:219
manager_type::deg_type deg_type
Definition: CCacheManagement.h:463
Definition: CCacheManagement.h:68
CCacheManBase(const manager_type &mgr)
Constructor.
Definition: CCacheManagement.h:262
CCuddLikeMgrStorage< boost::intrusive_ptr< CCuddCore > > type
Definition: CCacheManagement.h:240
void insert(navigator first, navigator second, navigator result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:367
node_type find(node_type first, node_type second) const
Find cached value wrt. given node.
Definition: CCacheManagement.h:351
CCacheManagement< manager_type, cache_type, 2 > base
Name base type.
Definition: CCacheManagement.h:499
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
Definition: CCacheManagement.h:38
base::node_type node_type
Definition: CCacheManagement.h:397
MgrType manager_type
Set manager type.
Definition: CCacheManagement.h:148
void insert(...) const
Definition: CCacheManagement.h:268
This template class forms the base for CCommutativeCacheManagement and CacheManager. It is an interface defining find and insert on decision diagram cache.
Definition: CCacheManagement.h:455
CCacheManBase< manager_type, cache_type, nargs > base
Name base type.
Definition: CCacheManagement.h:471
void insert(node_type first, node_type second, node_type result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:524
ManagerType manager_type
Definition: CCacheManagement.h:462
int deg_type
Type for polynomial degrees (ranges from -1 to maxint)
Definition: pbori_defs.h:222
Definition: CCacheManagement.h:50
base::navigator navigator
Definition: CCacheManagement.h:288
Definition: CCacheManagement.h:66
CCommutativeCacheManagement(const typename base::manager_type &mgr)
Constructor and default constructor.
Definition: CCacheManagement.h:506
Definition: CCacheManagement.h:51
lead_tag< block_dp_asc_tag > block_dp_asc_lead
Definition: CCacheManagement.h:86
CCuddNavigator explicit_navigator_cast(CCuddNavigator::pointer_type ptr)
Definition: CCuddNavigator.h:214
Definition: CCacheManagement.h:77
Definition: CCacheManagement.h:96
Definition: CCacheManagement.h:275
Definition: CCacheManagement.h:81
manager_type manager() const
Accessing manager.
Definition: CCacheManagement.h:177
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
dd_type generate(navigator navi) const
Re-generate valid decision diagram from navigator.
Definition: CCacheManagement.h:180
pbori_base< self >::type base
Set base type.
Definition: CCacheManagement.h:393
#define cuddCacheLookup2Zdd
Definition: prefix_internal.h:191
Definition: CCacheManagement.h:35
navigator find(navigator,...) const
Definition: CCacheManagement.h:266
CCacheManagement(const manager_type &mgr)
Constructor and default constructor.
Definition: CCacheManagement.h:477
Definition: CCacheManagement.h:89
base::node_type node_type
Definition: CCacheManagement.h:287
This class defines a C++ interface to CUDD's decicion diagram manager.
Definition: CCuddInterface.h:111
navigator find(navigator first, navigator second) const
Find cached value wrt. given node (for navigator type)
Definition: CCacheManagement.h:355
#define cuddCacheInsert2
Definition: prefix_internal.h:183
Definition: CCacheManagement.h:55
navigator find(navigator node) const
Find cached value wrt. given node (for navigator type)
Definition: CCacheManagement.h:301
DdManager * internal_manager_type
Set type of Cudd's internal manager type.
Definition: CCacheManagement.h:151
#define cuddCacheLookupZdd
Definition: prefix_internal.h:192
Definition: pbori_func.h:881
#define cuddCacheInsert
Definition: prefix_internal.h:182
BoolePolyRing ring_type
Type of Boolean rings.
Definition: CCacheManagement.h:164
void insert(navigator first, navigator second, navigator third, navigator result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:426
Definition: CCacheManagement.h:45
node_type find(node_type first, node_type second, node_type third) const
Find cached value wrt. given node.
Definition: CCacheManagement.h:406
class BooleSet dd_type
set decision diagram type
Definition: BoolePolyRing.h:62
Definition: CCacheManagement.h:57
navigator find(navigator first, navigator second, navigator third) const
Find cached value wrt. given node (for navigator type)
Definition: CCacheManagement.h:412
void insert(node_type first, node_type second, node_type result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:360
CCacheManBase(const manager_type &mgr)
Constructor.
Definition: CCacheManagement.h:403
Definition: CCacheManagement.h:93
base::navigator navigator
Definition: CCacheManagement.h:398
Definition: CCacheManagement.h:91
CCuddLikeMgrStorage(const manager_type &mgr)
Constructor.
Definition: CCacheManagement.h:170
Definition: CCacheManagement.h:61
Definition: CCacheManagement.h:67
Definition: CCacheManagement.h:36
pbori_base< self >::type base
Set base type.
Definition: CCacheManagement.h:283
pbori_DdManager DdManager
Definition: traits.h:33
void insert(node_type first, node_type second, node_type third, node_type result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:418
navigator find(navigator first, navigator second) const
Find cached value wrt. given node (for navigator type)
Definition: CCacheManagement.h:518
lead_tag< block_dlex_tag > block_dlex_lead
Definition: CCacheManagement.h:85
CCuddNavigator navigator
Type of navigators.
Definition: CCacheManagement.h:157
int idx_type
Type for indices.
Definition: pbori_defs.h:228
CCacheManBase(const manager_type &mgr)
Constructor.
Definition: CCacheManagement.h:293
manager_type::idx_type idx_type
Definition: CCacheManagement.h:465
Definition: CCacheManagement.h:132
node_type find(node_type first, node_type second) const
Find cached value wrt. given node.
Definition: CCacheManagement.h:510
mod_varset mod_deg2_set
Definition: CCacheManagement.h:73
base::navigator navigator
Definition: CCacheManagement.h:257
manager_type::size_type size_type
Definition: CCacheManagement.h:464
base::navigator navigator
Definition: CCacheManagement.h:503
CacheType cache_type
Definition: CCacheManagement.h:466
base::manager_type manager_type
Definition: CCacheManagement.h:258
ManagerType manager_type
Definition: CCacheManagement.h:494
void insert(navigator node, navigator result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:313
Definition: CCacheManagement.h:62
Definition: CCacheManagement.h:47
Definition: CCacheManagement.h:385
Definition: CCacheManagement.h:44
Definition: CCacheManagement.h:103
pbori_base< self >::type base
Set base type.
Definition: CCacheManagement.h:338
Definition: CCacheManagement.h:488
CCacheManBase(const manager_type &mgr)
Constructor.
Definition: CCacheManagement.h:348
#define Cudd_Deref
Definition: prefix_internal.h:160
pbori_base< self >::type base
Set base type.
Definition: CCacheManagement.h:252
CacheType cache_type
Definition: CCacheManagement.h:495
Definition: CCacheManagement.h:101
dd_type one() const
Get constant one.
Definition: CCacheManagement.h:185
Definition: CCacheManagement.h:88
CCuddLikeMgrStorage< BoolePolyRing > type
Definition: CCacheManagement.h:233
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
mod_varset mod_mon_set
Definition: CCacheManagement.h:74
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
Definition: CCacheManagement.h:70
internal_manager_type internalManager() const
Accessing Cudd-internal decision diagram manager.
Definition: CCacheManagement.h:196
base::manager_type manager_type
Definition: CCacheManagement.h:399
CCuddLikeMgrStorage< CCuddInterface > type
Definition: CCacheManagement.h:225
Definition: CCacheManagement.h:54
Definition: CCacheManagement.h:65
Definition: CCacheManagement.h:48
DdNode * node_type
Set type of Cudd's nodes.
Definition: CCacheManagement.h:154
Definition: CCacheManagement.h:97
Definition: CCacheManagement.h:76
#define cuddCacheLookup1Zdd
Definition: prefix_internal.h:189
Definition: CCacheManagement.h:79
Definition: CCacheManagement.h:37
void insert(navigator first, navigator second, navigator result) const
Store cached value wrt. given node (for navigator type)
Definition: CCacheManagement.h:532
Definition: CCacheManagement.h:244
base::navigator navigator
Definition: CCacheManagement.h:343
base::manager_type manager_type
Definition: CCacheManagement.h:344
base::node_type node_type
Define node type.
Definition: CCacheManagement.h:502
base::node_type node_type
Definition: CCacheManagement.h:256
node_type find(node_type node) const
Find cached value wrt. given node.
Definition: CCacheManagement.h:296
void insert(node_type node, node_type result) const
Store cached value wrt. given node.
Definition: CCacheManagement.h:306
Definition: CCacheManagement.h:41
Definition: CCacheManagement.h:145
base::manager_type manager_type
Definition: CCacheManagement.h:289
Definition: CCacheManagement.h:53
#define cuddCacheInsert1
Definition: prefix_internal.h:184
ring_type ring() const
Definition: CCacheManagement.h:193
lead_tag< dp_asc_tag > dp_asc_lead
Definition: CCacheManagement.h:83
#define Cudd_Ref
Definition: prefix_internal.h:157
Definition: CCacheManagement.h:59