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