PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 #ifndef polybori_cache_CCacheManagement_h_ 00017 #define polybori_cache_CCacheManagement_h_ 00018 00019 // include basic definitions 00020 #include <polybori/pbori_defs.h> 00021 00022 // get DD navigation 00023 #include <polybori/iterators/CCuddNavigator.h> 00024 00025 #include <polybori/ring/CCuddCore.h> 00026 #include <boost/intrusive_ptr.hpp> 00027 // get standard functionality 00028 #include <functional> 00029 00030 BEGIN_NAMESPACE_PBORI 00031 00032 class CCacheTypes { 00033 00034 public: 00035 struct no_cache_tag { enum { nargs = 0 }; }; 00036 struct unary_cache_tag { enum { nargs = 1 }; }; 00037 struct binary_cache_tag { enum { nargs = 2 }; }; 00038 struct ternary_cache_tag { enum { nargs = 3 }; }; 00039 00040 template <class TagType> 00041 struct lead_tag: public binary_cache_tag {}; 00042 00043 // user functions 00044 struct no_cache: public no_cache_tag { }; 00045 struct union_xor: public binary_cache_tag { }; 00046 00047 struct multiply_recursive: public binary_cache_tag { }; 00048 struct divide: public binary_cache_tag { }; 00049 00050 struct minimal_mod: public binary_cache_tag { }; 00051 struct minimal_elements: public unary_cache_tag { }; 00052 00053 struct multiplesof: public binary_cache_tag { }; 00054 struct divisorsof: public binary_cache_tag { }; 00055 struct ll_red_nf: public binary_cache_tag { }; 00056 struct plug_1: public binary_cache_tag { }; 00057 struct exist_abstract: public binary_cache_tag { }; 00058 00059 struct degree: public unary_cache_tag { }; 00060 00061 struct has_factor_x: public binary_cache_tag { }; 00062 struct has_factor_x_plus_one: public binary_cache_tag { }; 00063 00064 00065 struct mod_varset: public binary_cache_tag { }; 00066 struct interpolate: public binary_cache_tag { }; 00067 struct zeros: public binary_cache_tag { }; 00068 struct interpolate_smallest_lex: public binary_cache_tag { }; 00069 00070 struct include_divisors: public unary_cache_tag { }; 00071 00072 //struct mod_deg2_set: public binary_cache_tag { }; 00073 typedef mod_varset mod_deg2_set; 00074 typedef mod_varset mod_mon_set; 00075 00076 struct contained_deg2: public unary_cache_tag { }; 00077 struct contained_variables: public unary_cache_tag { }; 00078 00079 struct map_every_x_to_x_plus_one: public unary_cache_tag { }; 00080 00081 struct lex_lead: public unary_cache_tag {}; 00082 typedef lead_tag<dlex_tag> dlex_lead; 00083 typedef lead_tag<dp_asc_tag> dp_asc_lead; 00084 00085 typedef lead_tag<block_dlex_tag> block_dlex_lead; 00086 typedef lead_tag<block_dp_asc_tag> block_dp_asc_lead; 00087 00088 struct divisorsof_fixedpath: public ternary_cache_tag { }; 00089 struct testwise_ternary: public ternary_cache_tag { }; 00090 00091 struct used_variables: public unary_cache_tag { }; 00092 00093 struct block_degree: public binary_cache_tag { }; 00094 00095 00096 struct has_factor_x_plus_y: public ternary_cache_tag { }; 00097 struct left_equals_right_x_branch_and_r_has_fac_x: 00098 public ternary_cache_tag { }; 00099 00100 struct graded_part: public binary_cache_tag { }; 00101 struct mapping: public binary_cache_tag { }; 00102 00103 struct is_rewriteable: public binary_cache_tag{}; 00104 }; 00105 00106 // Reserve integer Numbers for Ternary operations (for cudd) 00107 template <class TagType> 00108 struct count_tags; 00109 00110 template<> 00111 struct count_tags<CCacheTypes::divisorsof_fixedpath>{ 00112 enum { value = 0 }; 00113 }; 00114 00115 template <class BaseTag> 00116 struct increment_count_tags { 00117 enum{ value = count_tags<BaseTag>::value + 1 }; 00118 }; 00119 00120 template<> 00121 class count_tags<CCacheTypes::testwise_ternary>: 00122 public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ }; 00123 template<> 00124 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>: 00125 public increment_count_tags<CCacheTypes::testwise_ternary>{ }; 00126 template<> 00127 class count_tags<CCacheTypes::has_factor_x_plus_y>: 00128 public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ }; 00129 // generate tag number (special pattern with 4 usable bits) 00130 // 18 bits are already used 00131 template <unsigned Counted, unsigned Offset = 18> 00132 class cudd_tag_number { 00133 public: 00134 enum { value = 00135 ( ((Counted + Offset) & 0x3 ) << 2) | 00136 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 }; 00137 }; 00138 00144 template <class MgrType> 00145 class CCuddLikeMgrStorage { 00146 public: 00148 typedef MgrType manager_type; 00149 00151 typedef DdManager* internal_manager_type; 00152 00154 typedef DdNode* node_type; 00155 00157 typedef CCuddNavigator navigator; 00158 00159 00160 // typedef CTypes::dd_base dd_base; 00161 // typedef typename manager_type::mgrcore_ptr mgrcore_ptr; 00162 00164 typedef BoolePolyRing ring_type; 00165 00167 typedef typename ring_type::dd_type dd_type; 00168 00170 CCuddLikeMgrStorage(const manager_type& mgr): 00171 m_mgr(mgr) {} 00172 00173 // CCuddLikeMgrStorage(const mgrcore_ptr& mgr): 00174 // m_mgr(mgr) {} 00175 00177 manager_type manager() const { return m_mgr; } 00178 00180 dd_type generate(navigator navi) const { 00181 return dd_type(m_mgr, navi); 00182 } 00183 00185 dd_type one() const { 00186 return ring_type(m_mgr).one();//dd_type(m_mgr, DD_ONE(m_mgr->manager()));//manager().zddOne(); 00187 } 00189 dd_type zero() const { 00190 return ring_type(m_mgr).zero();//dd_base(m_mgr, PBORI_PREFIX(Cudd_ReadZero)(m_mgr->manager()));//manager().zddZero(); 00191 } 00192 00193 ring_type ring() const { return ring_type(manager()); } 00194 protected: 00196 internal_manager_type internalManager() const { 00197 return m_mgr.getManager(); 00198 // return manager().getManager(); 00199 } 00200 00201 private: 00203 manager_type m_mgr; 00204 // typename manager_type::mgrcore_ptr m_mgr; 00205 }; 00206 00218 template <class ManagerType, class CacheType, unsigned ArgumentLength> 00219 class CCacheManBase; 00220 00221 // Fixing base type for Cudd-Like type CCuddInterface 00222 template <class CacheType, unsigned ArgumentLength> 00223 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > { 00224 00225 typedef CCuddLikeMgrStorage<CCuddInterface> type; 00226 }; 00227 00228 00229 // Fixing base type for Cudd-Like type CCuddInterface 00230 template <class CacheType, unsigned ArgumentLength> 00231 struct pbori_base<CCacheManBase<BoolePolyRing, CacheType, ArgumentLength> > { 00232 00233 typedef CCuddLikeMgrStorage<BoolePolyRing> type; 00234 }; 00235 00236 // Fixing base type for Cudd-Like type CCuddInterface 00237 template <class CacheType, unsigned ArgumentLength> 00238 struct pbori_base<CCacheManBase<boost::intrusive_ptr<CCuddCore>, CacheType, ArgumentLength> > { 00239 00240 typedef CCuddLikeMgrStorage<boost::intrusive_ptr<CCuddCore> > type; 00241 }; 00242 // Dummy variant for generating empty cache managers, e.g. for using generate() 00243 template <class ManagerType, class CacheType> 00244 class CCacheManBase<ManagerType, CacheType, 0> : 00245 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type { 00246 00247 public: 00249 typedef CCacheManBase<ManagerType, CacheType, 0> self; 00250 00252 typedef typename pbori_base<self>::type base; 00253 00255 00256 typedef typename base::node_type node_type; 00257 typedef typename base::navigator navigator; 00258 typedef typename base::manager_type manager_type; 00260 00262 CCacheManBase(const manager_type& mgr): base(mgr) {} 00263 00265 00266 navigator find(navigator, ...) const { return navigator(); } 00267 node_type find(node_type, ...) const { return NULL; } 00268 void insert(...) const {} 00270 }; 00271 00272 00273 // Variant for unary functions 00274 template <class ManagerType, class CacheType> 00275 class CCacheManBase<ManagerType, CacheType, 1> : 00276 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type { 00277 00278 public: 00280 typedef CCacheManBase<ManagerType, CacheType, 1> self; 00281 00283 typedef typename pbori_base<self>::type base; 00284 00286 00287 typedef typename base::node_type node_type; 00288 typedef typename base::navigator navigator; 00289 typedef typename base::manager_type manager_type; 00291 00293 CCacheManBase(const manager_type& mgr): base(mgr) {} 00294 00296 node_type find(node_type node) const { 00297 return PBORI_PREFIX(cuddCacheLookup1Zdd)(internalManager(), cache_dummy, node); 00298 } 00299 00301 navigator find(navigator node) const { 00302 return explicit_navigator_cast(find(node.getNode())); 00303 } 00304 00306 void insert(node_type node, node_type result) const { 00307 PBORI_PREFIX(Cudd_Ref)(result); 00308 PBORI_PREFIX(cuddCacheInsert1)(internalManager(), cache_dummy, node, result); 00309 PBORI_PREFIX(Cudd_Deref)(result); 00310 } 00311 00313 void insert(navigator node, navigator result) const { 00314 insert(node.getNode(), result.getNode()); 00315 } 00316 00317 protected: 00319 using base::internalManager; 00320 00321 private: 00323 static node_type cache_dummy(typename base::internal_manager_type,node_type){ // LCOV_EXCL_LINE 00324 return NULL; // LCOV_EXCL_LINE 00325 } 00326 }; 00327 00328 // Variant for binary functions 00329 template <class ManagerType, class CacheType> 00330 class CCacheManBase<ManagerType, CacheType, 2> : 00331 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type { 00332 00333 public: 00335 typedef CCacheManBase<ManagerType, CacheType, 2> self; 00336 00338 typedef typename pbori_base<self>::type base; 00339 00341 00342 typedef typename base::node_type node_type; 00343 typedef typename base::navigator navigator; 00344 typedef typename base::manager_type manager_type; 00346 00348 CCacheManBase(const manager_type& mgr): base(mgr) {} 00349 00351 node_type find(node_type first, node_type second) const { 00352 return PBORI_PREFIX(cuddCacheLookup2Zdd)(internalManager(), cache_dummy, first, second); 00353 } 00355 navigator find(navigator first, navigator second) const { 00356 return explicit_navigator_cast(find(first.getNode(), second.getNode())); 00357 } 00358 00360 void insert(node_type first, node_type second, node_type result) const { 00361 PBORI_PREFIX(Cudd_Ref)(result); 00362 PBORI_PREFIX(cuddCacheInsert2)(internalManager(), cache_dummy, first, second, result); 00363 PBORI_PREFIX(Cudd_Deref)(result); 00364 } 00365 00367 void insert(navigator first, navigator second, navigator result) const { 00368 insert(first.getNode(), second.getNode(), result.getNode()); 00369 } 00370 00371 protected: 00373 using base::internalManager; 00374 00375 private: 00377 static node_type cache_dummy(typename base::internal_manager_type, // LCOV_EXCL_LINE 00378 node_type, node_type){ // LCOV_EXCL_LINE 00379 return NULL; // LCOV_EXCL_LINE 00380 } 00381 }; 00382 00383 // Variant for ternary functions 00384 template <class ManagerType, class CacheType> 00385 class CCacheManBase<ManagerType, CacheType, 3> : 00386 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type { 00387 00388 public: 00390 typedef CCacheManBase<ManagerType, CacheType, 3> self; 00391 00393 typedef typename pbori_base<self>::type base; 00394 00396 00397 typedef typename base::node_type node_type; 00398 typedef typename base::navigator navigator; 00399 typedef typename base::manager_type manager_type; 00401 00403 CCacheManBase(const manager_type& mgr): base(mgr) {} 00404 00406 node_type find(node_type first, node_type second, node_type third) const { 00407 return PBORI_PREFIX(cuddCacheLookupZdd)(internalManager(), (ptruint)GENERIC_DD_TAG, 00408 first, second, third); 00409 } 00410 00412 navigator find(navigator first, navigator second, navigator third) const { 00413 return explicit_navigator_cast(find(first.getNode(), second.getNode(), 00414 third.getNode())); 00415 } 00416 00418 void insert(node_type first, node_type second, node_type third, 00419 node_type result) const { 00420 PBORI_PREFIX(Cudd_Ref)(result); 00421 PBORI_PREFIX(cuddCacheInsert)(internalManager(), (ptruint)GENERIC_DD_TAG, 00422 first, second, third, result); 00423 PBORI_PREFIX(Cudd_Deref)(result); 00424 } 00426 void insert(navigator first, navigator second, navigator third, 00427 navigator result) const { 00428 insert(first.getNode(), second.getNode(), third.getNode(), 00429 result.getNode()); 00430 } 00431 00432 protected: 00434 using base::internalManager; 00435 00436 private: 00437 enum { GENERIC_DD_TAG = 00438 cudd_tag_number<count_tags<CacheType>::value>::value }; 00439 }; 00440 00453 template <class ManagerType, class CacheType, 00454 unsigned ArgumentLength = CacheType::nargs> 00455 class CCacheManagement: 00456 public CCacheManBase<ManagerType, 00457 CacheType, ArgumentLength> { 00458 public: 00459 00461 00462 typedef ManagerType manager_type; 00463 typedef typename manager_type::deg_type deg_type; 00464 typedef typename manager_type::size_type size_type; 00465 typedef typename manager_type::idx_type idx_type; 00466 typedef CacheType cache_type; 00467 enum { nargs = ArgumentLength }; 00469 00471 typedef CCacheManBase<manager_type, cache_type, nargs> base; 00472 00474 typedef typename base::node_type node_type; 00475 00477 CCacheManagement(const manager_type& mgr): 00478 base(mgr) {} 00479 00480 using base::find; 00481 using base::insert; 00482 }; 00483 00487 template <class ManagerType, class CacheType> 00488 class CCommutativeCacheManagement: 00489 public CCacheManagement<ManagerType, CacheType, 2> { 00490 00491 public: 00493 00494 typedef ManagerType manager_type; 00495 typedef CacheType cache_type; 00497 00499 typedef CCacheManagement<manager_type, cache_type, 2> base; 00500 00502 typedef typename base::node_type node_type; 00503 typedef typename base::navigator navigator; 00504 00506 CCommutativeCacheManagement(const typename base::manager_type& mgr): 00507 base(mgr) {} 00508 00510 node_type find(node_type first, node_type second) const { 00511 if ( std::less<node_type>()(first, second) ) 00512 return base::find(first, second); 00513 else 00514 return base::find(second, first); 00515 } 00516 00518 navigator find(navigator first, navigator second) const { 00519 return explicit_navigator_cast(find(first.getNode(), second.getNode())); 00520 } 00521 00522 00524 void insert(node_type first, node_type second, node_type result) const { 00525 if ( std::less<node_type>()(first, second) ) 00526 base::insert(first, second, result); 00527 else 00528 base::insert(second, first, result); 00529 } 00530 00532 void insert(navigator first, navigator second, navigator result) const { 00533 insert(first.getNode(), second.getNode(), result.getNode()); 00534 } 00535 00536 }; 00537 00538 END_NAMESPACE_PBORI 00539 00540 #endif