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