PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 // include basic definitions 00017 #include "pbori_defs.h" 00018 00019 // get DD navigation 00020 #include "CCuddNavigator.h" 00021 00022 #include "CCuddCore.h" 00023 #include <boost/intrusive_ptr.hpp> 00024 // get standard functionality 00025 #include <functional> 00026 00027 #ifndef CCacheManagement_h_ 00028 #define CCacheManagement_h_ 00029 00030 BEGIN_NAMESPACE_PBORI 00031 00032 00033 00034 class CCacheTypes { 00035 00036 public: 00037 struct no_cache_tag { enum { nargs = 0 }; }; 00038 struct unary_cache_tag { enum { nargs = 1 }; }; 00039 struct binary_cache_tag { enum { nargs = 2 }; }; 00040 struct ternary_cache_tag { enum { nargs = 3 }; }; 00041 00042 template <class TagType> 00043 struct lead_tag: public binary_cache_tag {}; 00044 00045 // user functions 00046 struct no_cache: public no_cache_tag { }; 00047 struct union_xor: public binary_cache_tag { }; 00048 00049 struct multiply_recursive: public binary_cache_tag { }; 00050 struct divide: public binary_cache_tag { }; 00051 00052 struct minimal_mod: public binary_cache_tag { }; 00053 struct minimal_elements: public unary_cache_tag { }; 00054 00055 struct multiplesof: public binary_cache_tag { }; 00056 struct divisorsof: public binary_cache_tag { }; 00057 struct ll_red_nf: public binary_cache_tag { }; 00058 struct plug_1: public binary_cache_tag { }; 00059 struct exist_abstract: public binary_cache_tag { }; 00060 00061 struct degree: public unary_cache_tag { }; 00062 00063 struct has_factor_x: public binary_cache_tag { }; 00064 struct has_factor_x_plus_one: public binary_cache_tag { }; 00065 00066 00067 struct mod_varset: public binary_cache_tag { }; 00068 struct interpolate: public binary_cache_tag { }; 00069 struct zeros: public binary_cache_tag { }; 00070 struct interpolate_smallest_lex: public binary_cache_tag { }; 00071 00072 struct include_divisors: public unary_cache_tag { }; 00073 00074 //struct mod_deg2_set: public binary_cache_tag { }; 00075 typedef mod_varset mod_deg2_set; 00076 typedef mod_varset mod_mon_set; 00077 00078 struct contained_deg2: public unary_cache_tag { }; 00079 struct contained_variables: public unary_cache_tag { }; 00080 00081 struct map_every_x_to_x_plus_one: public unary_cache_tag { }; 00082 00083 struct lex_lead: public unary_cache_tag {}; 00084 typedef lead_tag<dlex_tag> dlex_lead; 00085 typedef lead_tag<dp_asc_tag> dp_asc_lead; 00086 00087 typedef lead_tag<block_dlex_tag> block_dlex_lead; 00088 typedef lead_tag<block_dp_asc_tag> block_dp_asc_lead; 00089 00090 struct divisorsof_fixedpath: public ternary_cache_tag { }; 00091 struct testwise_ternary: public ternary_cache_tag { }; 00092 00093 struct used_variables: public unary_cache_tag { }; 00094 00095 struct block_degree: public binary_cache_tag { }; 00096 00097 00098 struct has_factor_x_plus_y: public ternary_cache_tag { }; 00099 struct left_equals_right_x_branch_and_r_has_fac_x: 00100 public ternary_cache_tag { }; 00101 00102 struct graded_part: public binary_cache_tag { }; 00103 struct mapping: public binary_cache_tag { }; 00104 00105 struct is_rewriteable: public binary_cache_tag{}; 00106 }; 00107 00108 // Reserve integer Numbers for Ternary operations (for cudd) 00109 template <class TagType> 00110 struct count_tags; 00111 00112 template<> 00113 struct count_tags<CCacheTypes::divisorsof_fixedpath>{ 00114 enum { value = 0 }; 00115 }; 00116 00117 template <class BaseTag> 00118 struct increment_count_tags { 00119 enum{ value = count_tags<BaseTag>::value + 1 }; 00120 }; 00121 00122 template<> 00123 class count_tags<CCacheTypes::testwise_ternary>: 00124 public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ }; 00125 template<> 00126 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>: 00127 public increment_count_tags<CCacheTypes::testwise_ternary>{ }; 00128 template<> 00129 class count_tags<CCacheTypes::has_factor_x_plus_y>: 00130 public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ }; 00131 // generate tag number (special pattern with 4 usable bits) 00132 // 18 bits are already used 00133 template <unsigned Counted, unsigned Offset = 18> 00134 class cudd_tag_number { 00135 public: 00136 enum { value = 00137 ( ((Counted + Offset) & 0x3 ) << 2) | 00138 ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 }; 00139 }; 00140 00146 template <class MgrType> 00147 class CCuddLikeMgrStorage { 00148 public: 00150 typedef MgrType manager_type; 00151 00153 typedef DdManager* internal_manager_type; 00154 00156 typedef DdNode* node_type; 00157 00159 typedef CCuddNavigator navigator; 00160 00161 00162 // typedef CTypes::dd_base dd_base; 00163 // typedef typename manager_type::mgrcore_ptr mgrcore_ptr; 00164 00166 typedef BoolePolyRing ring_type; 00167 00169 typedef typename ring_type::dd_type dd_type; 00170 00172 CCuddLikeMgrStorage(const manager_type& mgr): 00173 m_mgr(mgr) {} 00174 00175 // CCuddLikeMgrStorage(const mgrcore_ptr& mgr): 00176 // m_mgr(mgr) {} 00177 00179 manager_type manager() const { return m_mgr; } 00180 00182 dd_type generate(navigator navi) const { 00183 return dd_type(m_mgr, navi); 00184 } 00185 00187 dd_type one() const { 00188 return ring_type(m_mgr).one();//dd_type(m_mgr, DD_ONE(m_mgr->manager()));//manager().zddOne(); 00189 } 00191 dd_type zero() const { 00192 return ring_type(m_mgr).zero();//dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager()));//manager().zddZero(); 00193 } 00194 00195 ring_type ring() const { return ring_type(manager()); } 00196 protected: 00198 internal_manager_type internalManager() const { 00199 return m_mgr.getManager(); 00200 // return manager().getManager(); 00201 } 00202 00203 private: 00205 manager_type m_mgr; 00206 // typename manager_type::mgrcore_ptr m_mgr; 00207 }; 00208 00220 template <class ManagerType, class CacheType, unsigned ArgumentLength> 00221 class CCacheManBase; 00222 00223 // Fixing base type for Cudd-Like type CCuddInterface 00224 template <class CacheType, unsigned ArgumentLength> 00225 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > { 00226 00227 typedef CCuddLikeMgrStorage<CCuddInterface> type; 00228 }; 00229 00230 00231 // Fixing base type for Cudd-Like type CCuddInterface 00232 template <class CacheType, unsigned ArgumentLength> 00233 struct pbori_base<CCacheManBase<BoolePolyRing, CacheType, ArgumentLength> > { 00234 00235 typedef CCuddLikeMgrStorage<BoolePolyRing> type; 00236 }; 00237 00238 // Fixing base type for Cudd-Like type CCuddInterface 00239 template <class CacheType, unsigned ArgumentLength> 00240 struct pbori_base<CCacheManBase<boost::intrusive_ptr<CCuddCore>, CacheType, ArgumentLength> > { 00241 00242 typedef CCuddLikeMgrStorage<boost::intrusive_ptr<CCuddCore> > type; 00243 }; 00244 // Dummy variant for generating empty cache managers, e.g. for using generate() 00245 template <class ManagerType, class CacheType> 00246 class CCacheManBase<ManagerType, CacheType, 0> : 00247 public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type { 00248 00249 public: 00251 typedef CCacheManBase<ManagerType, CacheType, 0> self; 00252 00254 typedef typename pbori_base<self>::type base; 00255 00257 00258 typedef typename base::node_type node_type; 00259 typedef typename base::navigator navigator; 00260 typedef typename base::manager_type manager_type; 00262 00264 CCacheManBase(const manager_type& mgr): base(mgr) {} 00265 00267 00268 navigator find(navigator, ...) const { return navigator(); } 00269 node_type find(node_type, ...) const { return NULL; } 00270 void insert(...) const {} 00272 }; 00273 00274 00275 // Variant for unary functions 00276 template <class ManagerType, class CacheType> 00277 class CCacheManBase<ManagerType, CacheType, 1> : 00278 public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type { 00279 00280 public: 00282 typedef CCacheManBase<ManagerType, CacheType, 1> self; 00283 00285 typedef typename pbori_base<self>::type base; 00286 00288 00289 typedef typename base::node_type node_type; 00290 typedef typename base::navigator navigator; 00291 typedef typename base::manager_type manager_type; 00293 00295 CCacheManBase(const manager_type& mgr): base(mgr) {} 00296 00298 node_type find(node_type node) const { 00299 return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node); 00300 } 00301 00303 navigator find(navigator node) const { 00304 return explicit_navigator_cast(find(node.getNode())); 00305 } 00306 00308 void insert(node_type node, node_type result) const { 00309 Cudd_Ref(result); 00310 cuddCacheInsert1(internalManager(), cache_dummy, node, result); 00311 Cudd_Deref(result); 00312 } 00313 00315 void insert(navigator node, navigator result) const { 00316 insert(node.getNode(), result.getNode()); 00317 } 00318 00319 protected: 00321 using base::internalManager; 00322 00323 private: 00325 static node_type cache_dummy(typename base::internal_manager_type,node_type){ // LCOV_EXCL_LINE 00326 return NULL; // LCOV_EXCL_LINE 00327 } 00328 }; 00329 00330 // Variant for binary functions 00331 template <class ManagerType, class CacheType> 00332 class CCacheManBase<ManagerType, CacheType, 2> : 00333 public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type { 00334 00335 public: 00337 typedef CCacheManBase<ManagerType, CacheType, 2> self; 00338 00340 typedef typename pbori_base<self>::type base; 00341 00343 00344 typedef typename base::node_type node_type; 00345 typedef typename base::navigator navigator; 00346 typedef typename base::manager_type manager_type; 00348 00350 CCacheManBase(const manager_type& mgr): base(mgr) {} 00351 00353 node_type find(node_type first, node_type second) const { 00354 return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second); 00355 } 00357 navigator find(navigator first, navigator second) const { 00358 return explicit_navigator_cast(find(first.getNode(), second.getNode())); 00359 } 00360 00362 void insert(node_type first, node_type second, node_type result) const { 00363 Cudd_Ref(result); 00364 cuddCacheInsert2(internalManager(), cache_dummy, first, second, result); 00365 Cudd_Deref(result); 00366 } 00367 00369 void insert(navigator first, navigator second, navigator result) const { 00370 insert(first.getNode(), second.getNode(), result.getNode()); 00371 } 00372 00373 protected: 00375 using base::internalManager; 00376 00377 private: 00379 static node_type cache_dummy(typename base::internal_manager_type, // LCOV_EXCL_LINE 00380 node_type, node_type){ // LCOV_EXCL_LINE 00381 return NULL; // LCOV_EXCL_LINE 00382 } 00383 }; 00384 00385 // Variant for ternary functions 00386 template <class ManagerType, class CacheType> 00387 class CCacheManBase<ManagerType, CacheType, 3> : 00388 public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type { 00389 00390 public: 00392 typedef CCacheManBase<ManagerType, CacheType, 3> self; 00393 00395 typedef typename pbori_base<self>::type base; 00396 00398 00399 typedef typename base::node_type node_type; 00400 typedef typename base::navigator navigator; 00401 typedef typename base::manager_type manager_type; 00403 00405 CCacheManBase(const manager_type& mgr): base(mgr) {} 00406 00408 node_type find(node_type first, node_type second, node_type third) const { 00409 return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG, 00410 first, second, third); 00411 } 00412 00414 navigator find(navigator first, navigator second, navigator third) const { 00415 return explicit_navigator_cast(find(first.getNode(), second.getNode(), 00416 third.getNode())); 00417 } 00418 00420 void insert(node_type first, node_type second, node_type third, 00421 node_type result) const { 00422 Cudd_Ref(result); 00423 cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG, 00424 first, second, third, result); 00425 Cudd_Deref(result); 00426 } 00428 void insert(navigator first, navigator second, navigator third, 00429 navigator result) const { 00430 insert(first.getNode(), second.getNode(), third.getNode(), 00431 result.getNode()); 00432 } 00433 00434 protected: 00436 using base::internalManager; 00437 00438 private: 00439 enum { GENERIC_DD_TAG = 00440 cudd_tag_number<count_tags<CacheType>::value>::value }; 00441 }; 00442 00455 template <class ManagerType, class CacheType, 00456 unsigned ArgumentLength = CacheType::nargs> 00457 class CCacheManagement: 00458 public CCacheManBase<ManagerType, 00459 CacheType, ArgumentLength>, 00460 public CAuxTypes { 00461 public: 00462 00464 00465 typedef ManagerType manager_type; 00466 typedef CTypes::idx_type idx_type; 00467 typedef CacheType cache_type; 00468 enum { nargs = ArgumentLength }; 00470 00472 typedef CCacheManBase<manager_type, cache_type, nargs> base; 00473 00475 typedef typename base::node_type node_type; 00476 00478 CCacheManagement(const manager_type& mgr): 00479 base(mgr) {} 00480 00481 using base::find; 00482 using base::insert; 00483 }; 00484 00488 template <class ManagerType, class CacheType> 00489 class CCommutativeCacheManagement: 00490 public CCacheManagement<ManagerType, CacheType, 2> { 00491 00492 public: 00494 00495 typedef ManagerType manager_type; 00496 typedef CacheType cache_type; 00498 00500 typedef CCacheManagement<manager_type, cache_type, 2> base; 00501 00503 typedef typename base::node_type node_type; 00504 typedef typename base::navigator navigator; 00505 00507 CCommutativeCacheManagement(const typename base::manager_type& mgr): 00508 base(mgr) {} 00509 00511 node_type find(node_type first, node_type second) const { 00512 if ( std::less<node_type>()(first, second) ) 00513 return base::find(first, second); 00514 else 00515 return base::find(second, first); 00516 } 00517 00519 navigator find(navigator first, navigator second) const { 00520 return explicit_navigator_cast(find(first.getNode(), second.getNode())); 00521 } 00522 00523 00525 void insert(node_type first, node_type second, node_type result) const { 00526 if ( std::less<node_type>()(first, second) ) 00527 base::insert(first, second, result); 00528 else 00529 base::insert(second, first, result); 00530 } 00531 00533 void insert(navigator first, navigator second, navigator result) const { 00534 insert(first.getNode(), second.getNode(), result.getNode()); 00535 } 00536 00537 }; 00538 00539 END_NAMESPACE_PBORI 00540 00541 #endif