00001
00002
00151
00152
00153
00154 #include "pbori_defs.h"
00155
00156
00157 #include "CCuddNavigator.h"
00158 #include "CDDInterface.h"
00159 #include "BooleRing.h"
00160
00161 #include <functional>
00162
00163 #ifndef CCacheManagement_h_
00164 #define CCacheManagement_h_
00165
00166 BEGIN_NAMESPACE_PBORI
00167
00168
00169 class CCacheTypes {
00170
00171 public:
00172 struct no_cache_tag { enum { nargs = 0 }; };
00173 struct unary_cache_tag { enum { nargs = 1 }; };
00174 struct binary_cache_tag { enum { nargs = 2 }; };
00175 struct ternary_cache_tag { enum { nargs = 3 }; };
00176
00177
00178 struct no_cache: public no_cache_tag { };
00179 struct union_xor: public binary_cache_tag { };
00180
00181 struct multiply_recursive: public binary_cache_tag { };
00182 struct divide: public binary_cache_tag { };
00183
00184 struct minimal_mod: public binary_cache_tag { };
00185 struct minimal_elements: public unary_cache_tag { };
00186
00187 struct multiplesof: public binary_cache_tag { };
00188 struct divisorsof: public binary_cache_tag { };
00189 struct ll_red_nf: public binary_cache_tag { };
00190 struct plug_1: public binary_cache_tag { };
00191 struct exist_abstract: public binary_cache_tag { };
00192
00193 struct degree: public unary_cache_tag { };
00194
00195 struct has_factor_x: public binary_cache_tag { };
00196 struct has_factor_x_plus_one: public binary_cache_tag { };
00197
00198
00199 struct mod_varset: public binary_cache_tag { };
00200 struct interpolate: public binary_cache_tag { };
00201 struct zeroes: public binary_cache_tag { };
00202 struct interpolate_smallest_lex: public binary_cache_tag { };
00203
00204 struct include_divisors: public unary_cache_tag { };
00205
00206
00207 typedef mod_varset mod_deg2_set;
00208 typedef mod_varset mod_mon_set;
00209
00210 struct contained_deg2: public unary_cache_tag { };
00211 struct contained_variables: public unary_cache_tag { };
00212
00213 struct map_every_x_to_x_plus_one: public unary_cache_tag { };
00214
00215 struct dlex_lead: public unary_cache_tag { };
00216 struct dp_asc_lead: public unary_cache_tag { };
00217
00218 struct divisorsof_fixedpath: public ternary_cache_tag { };
00219 struct testwise_ternary: public ternary_cache_tag { };
00220
00221 struct used_variables: public unary_cache_tag { };
00222
00223 struct block_degree: public binary_cache_tag { };
00224 struct block_dlex_lead: public unary_cache_tag { };
00225
00226 struct has_factor_x_plus_y: public ternary_cache_tag { };
00227 struct left_equals_right_x_branch_and_r_has_fac_x:
00228 public ternary_cache_tag { };
00229
00230 struct graded_part: public binary_cache_tag { };
00231 struct mapping: public binary_cache_tag { };
00232 };
00233
00234
00235 template <class TagType>
00236 struct count_tags;
00237
00238 template<>
00239 struct count_tags<CCacheTypes::divisorsof_fixedpath>{
00240 enum { value = 0 };
00241 };
00242
00243 template <class BaseTag>
00244 struct increment_count_tags {
00245 enum{ value = count_tags<BaseTag>::value + 1 };
00246 };
00247
00248 template<>
00249 class count_tags<CCacheTypes::testwise_ternary>:
00250 public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ };
00251 template<>
00252 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
00253 public increment_count_tags<CCacheTypes::testwise_ternary>{ };
00254 template<>
00255 class count_tags<CCacheTypes::has_factor_x_plus_y>:
00256 public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ };
00257
00258
00259 template <unsigned Counted, unsigned Offset = 18>
00260 class cudd_tag_number {
00261 public:
00262 enum { value =
00263 ( ((Counted + Offset) & 0x3 ) << 2) |
00264 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
00265 };
00266
00272 template <class MgrType>
00273 class CCuddLikeMgrStorage {
00274 public:
00276 typedef MgrType manager_type;
00277
00279 typedef DdManager* internal_manager_type;
00280
00282 typedef DdNode* node_type;
00283
00285 typedef CCuddNavigator navigator;
00286
00288 typedef CTypes::dd_type dd_type;
00289 typedef CTypes::dd_base dd_base;
00290 typedef typename manager_type::mgrcore_ptr mgrcore_ptr;
00291
00293 typedef BooleRing ring_type;
00294
00296 CCuddLikeMgrStorage(const manager_type& mgr):
00297 m_mgr(mgr.managerCore()) {}
00298
00299 CCuddLikeMgrStorage(const mgrcore_ptr& mgr):
00300 m_mgr(mgr) {}
00301
00303 manager_type manager() const { return m_mgr; }
00304
00306 dd_type generate(navigator navi) const {
00307 return dd_base(m_mgr, navi.getNode());
00308 }
00309
00311 dd_type one() const {
00312 return dd_base(m_mgr, DD_ONE(m_mgr->manager));
00313 }
00315 dd_type zero() const {
00316 return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));
00317 }
00318
00319 ring_type ring() const { return ring_type(manager()); }
00320 protected:
00322 internal_manager_type internalManager() const {
00323 return m_mgr->manager;
00324
00325 }
00326
00327 private:
00329
00330 typename manager_type::mgrcore_ptr m_mgr;
00331 };
00332
00342 template <class ManagerType, class CacheType, unsigned ArgumentLength>
00343 class CCacheManBase;
00344
00345
00346 template <class CacheType, unsigned ArgumentLength>
00347 struct pbori_base<CCacheManBase<Cudd, CacheType, ArgumentLength> > {
00348
00349 typedef CCuddLikeMgrStorage<Cudd> type;
00350 };
00351
00352
00353 template <class CacheType, unsigned ArgumentLength>
00354 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > {
00355
00356 typedef CCuddLikeMgrStorage<CCuddInterface> type;
00357 };
00358
00359
00360 template <class ManagerType, class CacheType>
00361 class CCacheManBase<ManagerType, CacheType, 0> :
00362 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
00363
00364 public:
00366 typedef CCacheManBase<ManagerType, CacheType, 0> self;
00367
00369 typedef typename pbori_base<self>::type base;
00370
00372
00373 typedef typename base::node_type node_type;
00374 typedef typename base::navigator navigator;
00375 typedef typename base::manager_type manager_type;
00377
00379 CCacheManBase(const manager_type& mgr): base(mgr) {}
00380
00382
00383 navigator find(navigator, ...) const { return navigator(); }
00384 node_type find(node_type, ...) const { return NULL; }
00385 void insert(...) const {}
00387 };
00388
00389
00390
00391 template <class ManagerType, class CacheType>
00392 class CCacheManBase<ManagerType, CacheType, 1> :
00393 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
00394
00395 public:
00397 typedef CCacheManBase<ManagerType, CacheType, 1> self;
00398
00400 typedef typename pbori_base<self>::type base;
00401
00403
00404 typedef typename base::node_type node_type;
00405 typedef typename base::navigator navigator;
00406 typedef typename base::manager_type manager_type;
00408
00410 CCacheManBase(const manager_type& mgr): base(mgr) {}
00411
00413 node_type find(node_type node) const {
00414 return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node);
00415 }
00416
00418 navigator find(navigator node) const {
00419 return explicit_navigator_cast(find(node.getNode()));
00420 }
00421
00423 void insert(node_type node, node_type result) const {
00424 Cudd_Ref(result);
00425 cuddCacheInsert1(internalManager(), cache_dummy, node, result);
00426 Cudd_Deref(result);
00427 }
00428
00430 void insert(navigator node, navigator result) const {
00431 insert(node.getNode(), result.getNode());
00432 }
00433
00434 protected:
00436 using base::internalManager;
00437
00438 private:
00440 static node_type cache_dummy(typename base::internal_manager_type,node_type){
00441 return NULL;
00442 }
00443 };
00444
00445
00446 template <class ManagerType, class CacheType>
00447 class CCacheManBase<ManagerType, CacheType, 2> :
00448 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
00449
00450 public:
00452 typedef CCacheManBase<ManagerType, CacheType, 2> self;
00453
00455 typedef typename pbori_base<self>::type base;
00456
00458
00459 typedef typename base::node_type node_type;
00460 typedef typename base::navigator navigator;
00461 typedef typename base::manager_type manager_type;
00463
00465 CCacheManBase(const manager_type& mgr): base(mgr) {}
00466
00468 node_type find(node_type first, node_type second) const {
00469 return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second);
00470 }
00472 navigator find(navigator first, navigator second) const {
00473 return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00474 }
00475
00477 void insert(node_type first, node_type second, node_type result) const {
00478 Cudd_Ref(result);
00479 cuddCacheInsert2(internalManager(), cache_dummy, first, second, result);
00480 Cudd_Deref(result);
00481 }
00482
00484 void insert(navigator first, navigator second, navigator result) const {
00485 insert(first.getNode(), second.getNode(), result.getNode());
00486 }
00487
00488 protected:
00490 using base::internalManager;
00491
00492 private:
00494 static node_type cache_dummy(typename base::internal_manager_type,
00495 node_type, node_type){
00496 return NULL;
00497 }
00498 };
00499
00500
00501 template <class ManagerType, class CacheType>
00502 class CCacheManBase<ManagerType, CacheType, 3> :
00503 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
00504
00505 public:
00507 typedef CCacheManBase<ManagerType, CacheType, 3> self;
00508
00510 typedef typename pbori_base<self>::type base;
00511
00513
00514 typedef typename base::node_type node_type;
00515 typedef typename base::navigator navigator;
00516 typedef typename base::manager_type manager_type;
00518
00520 CCacheManBase(const manager_type& mgr): base(mgr) {}
00521
00523 node_type find(node_type first, node_type second, node_type third) const {
00524 return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG,
00525 first, second, third);
00526 }
00527
00529 navigator find(navigator first, navigator second, navigator third) const {
00530 return explicit_navigator_cast(find(first.getNode(), second.getNode(),
00531 third.getNode()));
00532 }
00533
00535 void insert(node_type first, node_type second, node_type third,
00536 node_type result) const {
00537 Cudd_Ref(result);
00538 cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG,
00539 first, second, third, result);
00540 Cudd_Deref(result);
00541 }
00543 void insert(navigator first, navigator second, navigator third,
00544 navigator result) const {
00545 insert(first.getNode(), second.getNode(), third.getNode(),
00546 result.getNode());
00547 }
00548
00549 protected:
00551 using base::internalManager;
00552
00553 private:
00554 enum { GENERIC_DD_TAG =
00555 cudd_tag_number<count_tags<CacheType>::value>::value };
00556 };
00557
00570 template <class CacheType,
00571 unsigned ArgumentLength = CacheType::nargs>
00572 class CCacheManagement:
00573 public CCacheManBase<typename CTypes::manager_base,
00574 CacheType, ArgumentLength> {
00575 public:
00576
00578
00579 typedef CTypes::manager_base manager_type;
00580 typedef CTypes::idx_type idx_type;
00581 typedef CacheType cache_type;
00582 enum { nargs = ArgumentLength };
00584
00586 typedef CCacheManBase<manager_type, cache_type, nargs> base;
00587
00589 typedef typename base::node_type node_type;
00590
00592 CCacheManagement(const manager_type& mgr):
00593 base(mgr) {}
00594
00595 using base::find;
00596 using base::insert;
00597 };
00598
00602 template <class CacheType>
00603 class CCommutativeCacheManagement:
00604 public CCacheManagement<CacheType, 2> {
00605
00606 public:
00608
00609 typedef CacheType cache_type;
00611
00613 typedef CCacheManagement<cache_type, 2> base;
00614
00616 typedef typename base::node_type node_type;
00617 typedef typename base::navigator navigator;
00618
00620 CCommutativeCacheManagement(const typename base::manager_type& mgr):
00621 base(mgr) {}
00622
00624 node_type find(node_type first, node_type second) const {
00625 if ( std::less<node_type>()(first, second) )
00626 return base::find(first, second);
00627 else
00628 return base::find(second, first);
00629 }
00630
00632 navigator find(navigator first, navigator second) const {
00633 return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00634 }
00635
00636
00638 void insert(node_type first, node_type second, node_type result) const {
00639 if ( std::less<node_type>()(first, second) )
00640 base::insert(first, second, result);
00641 else
00642 base::insert(second, first, result);
00643 }
00644
00646 void insert(navigator first, navigator second, navigator result) const {
00647 insert(first.getNode(), second.getNode(), result.getNode());
00648 }
00649
00650 };
00651
00652 END_NAMESPACE_PBORI
00653
00654 #endif