PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00160 //***************************************************************************** 00161 00162 // include basic definitions 00163 #include "pbori_defs.h" 00164 00165 // get DD navigation 00166 #include "CCuddNavigator.h" 00167 #include "CDDInterface.h" 00168 #include "BooleRing.h" 00169 // get standard functionality 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 // user functions 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 //struct mod_deg2_set: public binary_cache_tag { }; 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 // Reserve integer Numbers for Ternary operations (for cudd) 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 // generate tag number (special pattern with 4 usable bits) 00269 // 18 bits are already used 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));//manager().zddOne(); 00324 } 00326 dd_type zero() const { 00327 return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));//manager().zddZero(); 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 // return manager().getManager(); 00336 } 00337 00338 private: 00340 // const manager_type& m_mgr; 00341 typename manager_type::mgrcore_ptr m_mgr; 00342 }; 00343 00355 template <class ManagerType, class CacheType, unsigned ArgumentLength> 00356 class CCacheManBase; 00357 00358 // Fixing base type for Cudd-Like type Cudd 00359 template <class CacheType, unsigned ArgumentLength> 00360 struct pbori_base<CCacheManBase<Cudd, CacheType, ArgumentLength> > { 00361 00362 typedef CCuddLikeMgrStorage<Cudd> type; 00363 }; 00364 00365 // Fixing base type for Cudd-Like type CCuddInterface 00366 template <class CacheType, unsigned ArgumentLength> 00367 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > { 00368 00369 typedef CCuddLikeMgrStorage<CCuddInterface> type; 00370 }; 00371 00372 // Dummy variant for generating empty cache managers, e.g. for using generate() 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 // Variant for unary functions 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 // Variant for binary functions 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 // Variant for ternary functions 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