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