167 #include <functional>
169 #ifndef CCacheManagement_h_
170 #define CCacheManagement_h_
243 template <
class TagType>
251 template <
class BaseTag>
253 enum{ value = count_tags<BaseTag>::value + 1 };
260 class count_tags<
CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
267 template <
unsigned Counted,
unsigned Offset = 18>
271 ( ((Counted + Offset) & 0x3 ) << 2) |
272 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
280 template <
class MgrType>
305 m_mgr(mgr.managerCore()) {}
320 return dd_base(m_mgr, DD_ONE(m_mgr->manager));
324 return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));
331 return m_mgr->manager;
338 typename manager_type::mgrcore_ptr m_mgr;
350 template <
class ManagerType,
class CacheType,
unsigned ArgumentLength>
354 template <
class CacheType,
unsigned ArgumentLength>
361 template <
class CacheType,
unsigned ArgumentLength>
368 template <
class ManagerType,
class CacheType>
370 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
377 typedef typename pbori_base<self>::type
base;
399 template <
class ManagerType,
class CacheType>
401 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
408 typedef typename pbori_base<self>::type
base;
422 return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node);
433 cuddCacheInsert1(internalManager(), cache_dummy, node, result);
439 insert(node.getNode(), result.getNode());
444 using base::internalManager;
448 static node_type cache_dummy(
typename base::internal_manager_type,node_type){
454 template <
class ManagerType,
class CacheType>
456 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
463 typedef typename pbori_base<self>::type
base;
477 return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second);
487 cuddCacheInsert2(internalManager(), cache_dummy, first, second, result);
493 insert(first.getNode(), second.getNode(), result.getNode());
498 using base::internalManager;
502 static node_type cache_dummy(
typename base::internal_manager_type,
503 node_type, node_type){
509 template <
class ManagerType,
class CacheType>
511 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
518 typedef typename pbori_base<self>::type
base;
532 return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG,
533 first, second, third);
546 cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG,
547 first, second, third, result);
553 insert(first.getNode(), second.getNode(), third.getNode(),
559 using base::internalManager;
562 enum { GENERIC_DD_TAG =
578 template <
class CacheType,
579 unsigned ArgumentLength = CacheType::nargs>
582 CacheType, ArgumentLength> {
590 enum { nargs = ArgumentLength };
610 template <
class CacheType>
633 if ( std::less<node_type>()(first, second) )
634 return base::find(first, second);
636 return base::find(second, first);
647 if ( std::less<node_type>()(first, second) )
648 base::insert(first, second, result);
650 base::insert(second, first, result);
655 insert(first.getNode(), second.getNode(), result.getNode());