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