PolyBoRi
CCacheManagement.h
Go to the documentation of this file.
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