• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

CCacheManagement.h

Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00160 //*****************************************************************************
00161 
00162 // include basic definitions
00163 #include "pbori_defs.h"
00164 
00165 // get DD navigation
00166 #include "CCuddNavigator.h"
00167 #include "CDDInterface.h"
00168 #include "BooleRing.h"
00169 // get standard functionality
00170 #include <functional>
00171 
00172 #ifndef CCacheManagement_h_
00173 #define CCacheManagement_h_
00174 
00175 BEGIN_NAMESPACE_PBORI
00176 
00177 
00178 class CCacheTypes {
00179 
00180 public:
00181   struct no_cache_tag { enum { nargs = 0 }; };
00182   struct unary_cache_tag { enum { nargs = 1 }; };
00183   struct binary_cache_tag { enum { nargs = 2 }; };
00184   struct ternary_cache_tag { enum { nargs = 3 }; };
00185 
00186   // user functions
00187   struct no_cache: public no_cache_tag { };
00188   struct union_xor: public binary_cache_tag { };
00189 
00190   struct multiply_recursive: public binary_cache_tag { };
00191   struct divide: public binary_cache_tag { };
00192 
00193   struct minimal_mod: public binary_cache_tag { };
00194   struct minimal_elements: public unary_cache_tag { };
00195 
00196   struct multiplesof: public binary_cache_tag { };
00197   struct divisorsof: public binary_cache_tag { };
00198   struct ll_red_nf: public binary_cache_tag { };
00199   struct plug_1: public binary_cache_tag { };
00200   struct exist_abstract: public binary_cache_tag { };
00201 
00202   struct degree: public unary_cache_tag { };
00203 
00204   struct has_factor_x: public binary_cache_tag { };
00205   struct has_factor_x_plus_one: public binary_cache_tag { };
00206 
00207   
00208   struct mod_varset: public binary_cache_tag { };
00209   struct interpolate: public binary_cache_tag { };
00210   struct zeros: public binary_cache_tag { };
00211   struct interpolate_smallest_lex: public binary_cache_tag { };
00212   
00213   struct include_divisors: public unary_cache_tag { };
00214   
00215   //struct mod_deg2_set: public binary_cache_tag { };
00216   typedef mod_varset mod_deg2_set;
00217   typedef mod_varset mod_mon_set;
00218   
00219   struct contained_deg2: public unary_cache_tag { };
00220   struct contained_variables: public unary_cache_tag { };
00221 
00222   struct map_every_x_to_x_plus_one: public unary_cache_tag { };
00223 
00224   struct dlex_lead: public unary_cache_tag { };
00225   struct dp_asc_lead: public unary_cache_tag { };
00226 
00227   struct divisorsof_fixedpath: public ternary_cache_tag { };
00228   struct testwise_ternary: public ternary_cache_tag { };
00229 
00230   struct used_variables: public unary_cache_tag { };
00231 
00232   struct block_degree: public binary_cache_tag { };
00233   struct block_dlex_lead: public unary_cache_tag { };
00234   
00235   struct has_factor_x_plus_y: public ternary_cache_tag { };
00236   struct left_equals_right_x_branch_and_r_has_fac_x:
00237     public ternary_cache_tag { };
00238 
00239   struct graded_part: public binary_cache_tag { };
00240   struct mapping: public binary_cache_tag { };
00241   
00242   struct is_rewriteable: public binary_cache_tag{};
00243 };
00244 
00245 // Reserve integer Numbers for Ternary operations (for cudd)
00246 template <class TagType>
00247 struct count_tags;
00248 
00249 template<>
00250 struct count_tags<CCacheTypes::divisorsof_fixedpath>{
00251   enum { value = 0 };
00252 };
00253 
00254 template <class BaseTag>
00255 struct increment_count_tags {
00256   enum{ value = count_tags<BaseTag>::value + 1 };
00257 };
00258 
00259 template<>
00260 class count_tags<CCacheTypes::testwise_ternary>:
00261   public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ };
00262 template<>
00263 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
00264   public increment_count_tags<CCacheTypes::testwise_ternary>{ };
00265 template<>
00266 class count_tags<CCacheTypes::has_factor_x_plus_y>:
00267   public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ };
00268 // generate tag number (special pattern with 4 usable bits)
00269 // 18 bits are already used
00270 template <unsigned Counted, unsigned Offset = 18>
00271 class cudd_tag_number {
00272 public:
00273   enum { value = 
00274          ( ((Counted + Offset) & 0x3 ) << 2) | 
00275          ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
00276 };
00277 
00283 template <class MgrType>
00284 class CCuddLikeMgrStorage {
00285 public:
00287   typedef MgrType manager_type;
00288 
00290   typedef DdManager* internal_manager_type;
00291 
00293   typedef DdNode* node_type;
00294 
00296   typedef CCuddNavigator navigator;
00297 
00299   typedef CTypes::dd_type dd_type;
00300   typedef CTypes::dd_base dd_base;
00301   typedef typename manager_type::mgrcore_ptr mgrcore_ptr;
00302 
00304   typedef BooleRing ring_type;
00305 
00307   CCuddLikeMgrStorage(const manager_type& mgr): 
00308     m_mgr(mgr.managerCore()) {}
00309 
00310   CCuddLikeMgrStorage(const mgrcore_ptr& mgr): 
00311     m_mgr(mgr) {}
00312 
00314   manager_type manager() const { return m_mgr; }
00315 
00317   dd_type generate(navigator navi) const {
00318     return dd_base(m_mgr, navi.getNode());
00319   }
00320 
00322   dd_type one() const {
00323     return dd_base(m_mgr, DD_ONE(m_mgr->manager));//manager().zddOne();
00324   }
00326   dd_type zero() const {
00327     return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));//manager().zddZero();
00328   }
00329 
00330   ring_type ring() const { return ring_type(manager()); }
00331 protected:
00333   internal_manager_type internalManager() const { 
00334     return m_mgr->manager; 
00335     //  return manager().getManager(); 
00336   }
00337 
00338 private:
00340   //  const manager_type& m_mgr;
00341   typename manager_type::mgrcore_ptr  m_mgr;
00342 };
00343 
00355 template <class ManagerType, class CacheType, unsigned ArgumentLength>
00356 class CCacheManBase;
00357 
00358 // Fixing base type for Cudd-Like type Cudd
00359 template <class CacheType, unsigned ArgumentLength>
00360 struct pbori_base<CCacheManBase<Cudd, CacheType, ArgumentLength> > {
00361 
00362   typedef CCuddLikeMgrStorage<Cudd>  type;
00363 };
00364 
00365 // Fixing base type for Cudd-Like type CCuddInterface
00366 template <class CacheType, unsigned ArgumentLength>
00367 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > {
00368 
00369   typedef CCuddLikeMgrStorage<CCuddInterface> type;
00370 };
00371 
00372 // Dummy variant for generating empty cache managers, e.g. for using generate()
00373 template <class ManagerType, class CacheType>
00374 class CCacheManBase<ManagerType, CacheType, 0> :
00375   public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
00376 
00377 public:
00379   typedef CCacheManBase<ManagerType, CacheType, 0> self;
00380 
00382   typedef typename pbori_base<self>::type base;
00383 
00385 
00386   typedef typename base::node_type node_type;
00387   typedef typename base::navigator navigator;
00388   typedef typename base::manager_type manager_type;
00390 
00392   CCacheManBase(const manager_type& mgr): base(mgr) {}
00393 
00395 
00396   navigator find(navigator, ...) const { return navigator(); }
00397   node_type find(node_type, ...) const { return NULL; }
00398   void insert(...) const {}
00400 };
00401 
00402 
00403 // Variant for unary functions
00404 template <class ManagerType, class CacheType>
00405 class CCacheManBase<ManagerType, CacheType, 1> :
00406   public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
00407 
00408 public:
00410   typedef CCacheManBase<ManagerType, CacheType, 1> self;
00411 
00413   typedef typename pbori_base<self>::type base;
00414 
00416 
00417   typedef typename base::node_type node_type;
00418   typedef typename base::navigator navigator;
00419   typedef typename base::manager_type manager_type;
00421 
00423   CCacheManBase(const manager_type& mgr): base(mgr) {}
00424 
00426   node_type find(node_type node) const {
00427     return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node);
00428   }
00429 
00431   navigator find(navigator node) const { 
00432     return explicit_navigator_cast(find(node.getNode())); 
00433   }
00434 
00436   void insert(node_type node, node_type result) const {
00437     Cudd_Ref(result);
00438     cuddCacheInsert1(internalManager(), cache_dummy, node, result);
00439     Cudd_Deref(result);
00440   }
00441 
00443   void insert(navigator node, navigator result) const {
00444     insert(node.getNode(), result.getNode());
00445   }
00446 
00447 protected:
00449   using base::internalManager;
00450 
00451 private:
00453   static node_type cache_dummy(typename base::internal_manager_type,node_type){
00454     return NULL;
00455   }
00456 };
00457 
00458 // Variant for binary functions
00459 template <class ManagerType, class CacheType>
00460 class CCacheManBase<ManagerType, CacheType, 2> :
00461   public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
00462 
00463 public:
00465   typedef CCacheManBase<ManagerType, CacheType, 2> self;
00466 
00468   typedef typename pbori_base<self>::type base;
00469 
00471 
00472   typedef typename base::node_type node_type;
00473   typedef typename base::navigator navigator;
00474   typedef typename base::manager_type manager_type;
00476 
00478   CCacheManBase(const manager_type& mgr): base(mgr) {}
00479 
00481   node_type find(node_type first, node_type second) const {
00482     return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second);
00483   }
00485   navigator find(navigator first, navigator second) const { 
00486     return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00487   }
00488 
00490   void insert(node_type first, node_type second, node_type result) const {
00491     Cudd_Ref(result);
00492     cuddCacheInsert2(internalManager(), cache_dummy, first, second, result);
00493     Cudd_Deref(result);
00494   }
00495 
00497   void insert(navigator first, navigator second, navigator result) const {
00498     insert(first.getNode(), second.getNode(), result.getNode());
00499   }
00500 
00501 protected:
00503   using base::internalManager;
00504 
00505 private:
00507   static node_type cache_dummy(typename base::internal_manager_type, 
00508                                node_type, node_type){
00509     return NULL;
00510   }
00511 };
00512 
00513 // Variant for ternary functions
00514 template <class ManagerType, class CacheType>
00515 class CCacheManBase<ManagerType, CacheType, 3> :
00516   public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
00517 
00518 public:
00520   typedef CCacheManBase<ManagerType, CacheType, 3> self;
00521 
00523   typedef typename pbori_base<self>::type base;
00524 
00526 
00527   typedef typename base::node_type node_type;
00528   typedef typename base::navigator navigator;
00529   typedef typename base::manager_type manager_type;
00531 
00533   CCacheManBase(const manager_type& mgr): base(mgr) {}
00534 
00536   node_type find(node_type first, node_type second, node_type third) const {
00537     return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG, 
00538                               first, second, third);
00539   }
00540 
00542   navigator find(navigator first, navigator second, navigator third) const {
00543     return explicit_navigator_cast(find(first.getNode(), second.getNode(),
00544                                         third.getNode())); 
00545   }
00546 
00548   void insert(node_type first, node_type second, node_type third, 
00549               node_type result) const {
00550     Cudd_Ref(result);
00551     cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG, 
00552                     first, second, third, result);
00553     Cudd_Deref(result);
00554   }
00556   void insert(navigator first, navigator second, navigator third, 
00557               navigator result) const {
00558     insert(first.getNode(), second.getNode(), third.getNode(), 
00559            result.getNode());  
00560   }
00561 
00562 protected:
00564   using base::internalManager;
00565 
00566 private:
00567   enum { GENERIC_DD_TAG =
00568          cudd_tag_number<count_tags<CacheType>::value>::value };
00569 };
00570 
00583 template <class CacheType, 
00584           unsigned ArgumentLength = CacheType::nargs>
00585 class CCacheManagement: 
00586   public CCacheManBase<typename CTypes::manager_base, 
00587                        CacheType, ArgumentLength> {
00588 public:
00589 
00591 
00592   typedef CTypes::manager_base manager_type;
00593   typedef CTypes::idx_type idx_type;
00594   typedef CacheType cache_type;
00595   enum { nargs = ArgumentLength };
00597 
00599   typedef CCacheManBase<manager_type, cache_type, nargs> base;
00600 
00602   typedef typename base::node_type node_type;
00603 
00605   CCacheManagement(const manager_type& mgr):
00606     base(mgr) {}
00607 
00608   using base::find;
00609   using base::insert;
00610 };
00611 
00615 template <class CacheType>
00616 class CCommutativeCacheManagement: 
00617   public CCacheManagement<CacheType, 2> {
00618 
00619 public:
00621 
00622   typedef CacheType cache_type;
00624 
00626   typedef CCacheManagement<cache_type, 2> base;
00627 
00629   typedef typename base::node_type node_type;
00630   typedef typename base::navigator navigator;
00631 
00633   CCommutativeCacheManagement(const typename base::manager_type& mgr):
00634     base(mgr) {}
00635 
00637   node_type find(node_type first, node_type second) const {
00638     if ( std::less<node_type>()(first, second) )
00639       return base::find(first, second);
00640     else
00641       return base::find(second, first);
00642   }
00643 
00645   navigator find(navigator first, navigator second) const {
00646     return explicit_navigator_cast(find(first.getNode(), second.getNode()));
00647   }
00648 
00649 
00651   void insert(node_type first, node_type second, node_type result) const {
00652     if ( std::less<node_type>()(first, second) )
00653       base::insert(first, second, result);
00654     else
00655       base::insert(second, first, result);   
00656   }
00657 
00659   void insert(navigator first, navigator second, navigator result) const {
00660     insert(first.getNode(), second.getNode(), result.getNode());
00661   }
00662 
00663 };
00664 
00665 END_NAMESPACE_PBORI
00666 
00667 #endif

Generated on Tue Oct 5 2010 for PolyBoRi by  doxygen 1.7.1