00001
00002
00157
00158
00159
00160 #include "pbori_defs.h"
00161
00162
00163 #include "CCuddNavigator.h"
00164 #include "CDDInterface.h"
00165 #include "BooleRing.h"
00166
00167 #include <functional>
00168
00169 #ifndef CCacheManagement_h_
00170 #define CCacheManagement_h_
00171
00172 BEGIN_NAMESPACE_PBORI
00173
00174
00175 class CCacheTypes {
00176
00177 public:
00178 struct no_cache_tag { enum { nargs = 0 }; };
00179 struct unary_cache_tag { enum { nargs = 1 }; };
00180 struct binary_cache_tag { enum { nargs = 2 }; };
00181 struct ternary_cache_tag { enum { nargs = 3 }; };
00182
00183
00184 struct no_cache: public no_cache_tag { };
00185 struct union_xor: public binary_cache_tag { };
00186
00187 struct multiply_recursive: public binary_cache_tag { };
00188 struct divide: public binary_cache_tag { };
00189
00190 struct minimal_mod: public binary_cache_tag { };
00191 struct minimal_elements: public unary_cache_tag { };
00192
00193 struct multiplesof: public binary_cache_tag { };
00194 struct divisorsof: public binary_cache_tag { };
00195 struct ll_red_nf: public binary_cache_tag { };
00196 struct plug_1: public binary_cache_tag { };
00197 struct exist_abstract: public binary_cache_tag { };
00198
00199 struct degree: public unary_cache_tag { };
00200
00201 struct has_factor_x: public binary_cache_tag { };
00202 struct has_factor_x_plus_one: public binary_cache_tag { };
00203
00204
00205 struct mod_varset: public binary_cache_tag { };
00206 struct interpolate: public binary_cache_tag { };
00207 struct zeros: public binary_cache_tag { };
00208 struct interpolate_smallest_lex: public binary_cache_tag { };
00209
00210 struct include_divisors: public unary_cache_tag { };
00211
00212
00213 typedef mod_varset mod_deg2_set;
00214 typedef mod_varset mod_mon_set;
00215
00216 struct contained_deg2: public unary_cache_tag { };
00217 struct contained_variables: public unary_cache_tag { };
00218
00219 struct map_every_x_to_x_plus_one: public unary_cache_tag { };
00220
00221 struct dlex_lead: public unary_cache_tag { };
00222 struct dp_asc_lead: public unary_cache_tag { };
00223
00224 struct divisorsof_fixedpath: public ternary_cache_tag { };
00225 struct testwise_ternary: public ternary_cache_tag { };
00226
00227 struct used_variables: public unary_cache_tag { };
00228
00229 struct block_degree: public binary_cache_tag { };
00230 struct block_dlex_lead: public unary_cache_tag { };
00231
00232 struct has_factor_x_plus_y: public ternary_cache_tag { };
00233 struct left_equals_right_x_branch_and_r_has_fac_x:
00234 public ternary_cache_tag { };
00235
00236 struct graded_part: public binary_cache_tag { };
00237 struct mapping: public binary_cache_tag { };
00238
00239 struct is_rewriteable: public binary_cache_tag{};
00240 };
00241
00242
00243 template <class TagType>
00244 struct count_tags;
00245
00246 template<>
00247 struct count_tags<CCacheTypes::divisorsof_fixedpath>{
00248 enum { value = 0 };
00249 };
00250
00251 template <class BaseTag>
00252 struct increment_count_tags {
00253 enum{ value = count_tags<BaseTag>::value + 1 };
00254 };
00255
00256 template<>
00257 class count_tags<CCacheTypes::testwise_ternary>:
00258 public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ };
00259 template<>
00260 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
00261 public increment_count_tags<CCacheTypes::testwise_ternary>{ };
00262 template<>
00263 class count_tags<CCacheTypes::has_factor_x_plus_y>:
00264 public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ };
00265
00266
00267 template <unsigned Counted, unsigned Offset = 18>
00268 class cudd_tag_number {
00269 public:
00270 enum { value =
00271 ( ((Counted + Offset) & 0x3 ) << 2) |
00272 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
00273 };
00274
00280 template <class MgrType>
00281 class CCuddLikeMgrStorage {
00282 public:
00284 typedef MgrType manager_type;
00285
00287 typedef DdManager* internal_manager_type;
00288
00290 typedef DdNode* node_type;
00291
00293 typedef CCuddNavigator navigator;
00294
00296 typedef CTypes::dd_type dd_type;
00297 typedef CTypes::dd_base dd_base;
00298 typedef typename manager_type::mgrcore_ptr mgrcore_ptr;
00299
00301 typedef BooleRing ring_type;
00302
00304 CCuddLikeMgrStorage(const manager_type& mgr):
00305 m_mgr(mgr.managerCore()) {}
00306
00307 CCuddLikeMgrStorage(const mgrcore_ptr& mgr):
00308 m_mgr(mgr) {}
00309
00311 manager_type manager() const { return m_mgr; }
00312
00314 dd_type generate(navigator navi) const {
00315 return dd_base(m_mgr, navi.getNode());
00316 }
00317
00319 dd_type one() const {
00320 return dd_base(m_mgr, DD_ONE(m_mgr->manager));
00321 }
00323 dd_type zero() const {
00324 return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));
00325 }
00326
00327 ring_type ring() const { return ring_type(manager()); }
00328 protected:
00330 internal_manager_type internalManager() const {
00331 return m_mgr->manager;
00332
00333 }
00334
00335 private:
00337
00338 typename manager_type::mgrcore_ptr m_mgr;
00339 };
00340
00350 template <class ManagerType, class CacheType, unsigned ArgumentLength>
00351 class CCacheManBase;
00352
00353
00354 template <class CacheType, unsigned ArgumentLength>
00355 struct pbori_base<CCacheManBase<Cudd, CacheType, ArgumentLength> > {
00356
00357 typedef CCuddLikeMgrStorage<Cudd> type;
00358 };
00359
00360
00361 template <class CacheType, unsigned ArgumentLength>
00362 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > {
00363
00364 typedef CCuddLikeMgrStorage<CCuddInterface> type;
00365 };
00366
00367
00368 template <class ManagerType, class CacheType>
00369 class CCacheManBase<ManagerType, CacheType, 0> :
00370 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
00371
00372 public:
00374 typedef CCacheManBase<ManagerType, CacheType, 0> self;
00375
00377 typedef typename pbori_base<self>::type base;
00378
00380
00381 typedef typename base::node_type node_type;
00382 typedef typename base::navigator navigator;
00383 typedef typename base::manager_type manager_type;
00385
00387 CCacheManBase(const manager_type& mgr): base(mgr) {}
00388
00390
00391 navigator find(navigator, ...) const { return navigator(); }
00392 node_type find(node_type, ...) const { return NULL; }
00393 void insert(...) const {}
00395 };
00396
00397
00398
00399 template <class ManagerType, class CacheType>
00400 class CCacheManBase<ManagerType, CacheType, 1> :
00401 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
00402
00403 public:
00405 typedef CCacheManBase<ManagerType, CacheType, 1> self;
00406
00408 typedef typename pbori_base<self>::type base;
00409
00411
00412 typedef typename base::node_type node_type;
00413 typedef typename base::navigator navigator;
00414 typedef typename base::manager_type manager_type;
00416
00418 CCacheManBase(const manager_type& mgr): base(mgr) {}
00419
00421 node_type find(node_type node) const {
00422 return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node);
00423 }
00424
00426 navigator find(navigator node) const {
00427 return explicit_navigator_cast(find(node.getNode()));
00428 }
00429
00431 void insert(node_type node, node_type result) const {
00432 Cudd_Ref(result);
00433 cuddCacheInsert1(internalManager(), cache_dummy, node, result);
00434 Cudd_Deref(result);
00435 }
00436
00438 void insert(navigator node, navigator result) const {
00439 insert(node.getNode(), result.getNode());
00440 }
00441
00442 protected:
00444 using base::internalManager;
00445
00446 private:
00448 static node_type cache_dummy(typename base::internal_manager_type,node_type){
00449 return NULL;
00450 }
00451 };
00452
00453
00454 template <class ManagerType, class CacheType>
00455 class CCacheManBase<ManagerType, CacheType, 2> :
00456 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
00457
00458 public:
00460 typedef CCacheManBase<ManagerType, CacheType, 2> self;
00461
00463 typedef typename pbori_base<self>::type base;
00464
00466
00467 typedef typename base::node_type node_type;
00468 typedef typename base::navigator navigator;
00469 typedef typename base::manager_type manager_type;
00471
00473 CCacheManBase(const manager_type& mgr): base(mgr) {}
00474
00476 node_type find(node_type first, node_type second) const {
00477 return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second);
00478 }
00480 navigator find(navigator first, navigator second) const {
00481 return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00482 }
00483
00485 void insert(node_type first, node_type second, node_type result) const {
00486 Cudd_Ref(result);
00487 cuddCacheInsert2(internalManager(), cache_dummy, first, second, result);
00488 Cudd_Deref(result);
00489 }
00490
00492 void insert(navigator first, navigator second, navigator result) const {
00493 insert(first.getNode(), second.getNode(), result.getNode());
00494 }
00495
00496 protected:
00498 using base::internalManager;
00499
00500 private:
00502 static node_type cache_dummy(typename base::internal_manager_type,
00503 node_type, node_type){
00504 return NULL;
00505 }
00506 };
00507
00508
00509 template <class ManagerType, class CacheType>
00510 class CCacheManBase<ManagerType, CacheType, 3> :
00511 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
00512
00513 public:
00515 typedef CCacheManBase<ManagerType, CacheType, 3> self;
00516
00518 typedef typename pbori_base<self>::type base;
00519
00521
00522 typedef typename base::node_type node_type;
00523 typedef typename base::navigator navigator;
00524 typedef typename base::manager_type manager_type;
00526
00528 CCacheManBase(const manager_type& mgr): base(mgr) {}
00529
00531 node_type find(node_type first, node_type second, node_type third) const {
00532 return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG,
00533 first, second, third);
00534 }
00535
00537 navigator find(navigator first, navigator second, navigator third) const {
00538 return explicit_navigator_cast(find(first.getNode(), second.getNode(),
00539 third.getNode()));
00540 }
00541
00543 void insert(node_type first, node_type second, node_type third,
00544 node_type result) const {
00545 Cudd_Ref(result);
00546 cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG,
00547 first, second, third, result);
00548 Cudd_Deref(result);
00549 }
00551 void insert(navigator first, navigator second, navigator third,
00552 navigator result) const {
00553 insert(first.getNode(), second.getNode(), third.getNode(),
00554 result.getNode());
00555 }
00556
00557 protected:
00559 using base::internalManager;
00560
00561 private:
00562 enum { GENERIC_DD_TAG =
00563 cudd_tag_number<count_tags<CacheType>::value>::value };
00564 };
00565
00578 template <class CacheType,
00579 unsigned ArgumentLength = CacheType::nargs>
00580 class CCacheManagement:
00581 public CCacheManBase<typename CTypes::manager_base,
00582 CacheType, ArgumentLength> {
00583 public:
00584
00586
00587 typedef CTypes::manager_base manager_type;
00588 typedef CTypes::idx_type idx_type;
00589 typedef CacheType cache_type;
00590 enum { nargs = ArgumentLength };
00592
00594 typedef CCacheManBase<manager_type, cache_type, nargs> base;
00595
00597 typedef typename base::node_type node_type;
00598
00600 CCacheManagement(const manager_type& mgr):
00601 base(mgr) {}
00602
00603 using base::find;
00604 using base::insert;
00605 };
00606
00610 template <class CacheType>
00611 class CCommutativeCacheManagement:
00612 public CCacheManagement<CacheType, 2> {
00613
00614 public:
00616
00617 typedef CacheType cache_type;
00619
00621 typedef CCacheManagement<cache_type, 2> base;
00622
00624 typedef typename base::node_type node_type;
00625 typedef typename base::navigator navigator;
00626
00628 CCommutativeCacheManagement(const typename base::manager_type& mgr):
00629 base(mgr) {}
00630
00632 node_type find(node_type first, node_type second) const {
00633 if ( std::less<node_type>()(first, second) )
00634 return base::find(first, second);
00635 else
00636 return base::find(second, first);
00637 }
00638
00640 navigator find(navigator first, navigator second) const {
00641 return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00642 }
00643
00644
00646 void insert(node_type first, node_type second, node_type result) const {
00647 if ( std::less<node_type>()(first, second) )
00648 base::insert(first, second, result);
00649 else
00650 base::insert(second, first, result);
00651 }
00652
00654 void insert(navigator first, navigator second, navigator result) const {
00655 insert(first.getNode(), second.getNode(), result.getNode());
00656 }
00657
00658 };
00659
00660 END_NAMESPACE_PBORI
00661
00662 #endif