PolyBoRi
CCacheManagement.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_cache_CCacheManagement_h_
17 #define polybori_cache_CCacheManagement_h_
18 
19 // include basic definitions
20 #include <polybori/pbori_defs.h>
21 
22 // get DD navigation
24 
26 #include <boost/intrusive_ptr.hpp>
27 // get standard functionality
28 #include <functional>
29 
31 
32 class CCacheTypes {
33 
34 public:
35  struct no_cache_tag { enum { nargs = 0 }; };
36  struct unary_cache_tag { enum { nargs = 1 }; };
37  struct binary_cache_tag { enum { nargs = 2 }; };
38  struct ternary_cache_tag { enum { nargs = 3 }; };
39 
40  template <class TagType>
41  struct lead_tag: public binary_cache_tag {};
42 
43  // user functions
44  struct no_cache: public no_cache_tag { };
45  struct union_xor: public binary_cache_tag { };
46 
48  struct divide: public binary_cache_tag { };
49 
50  struct minimal_mod: public binary_cache_tag { };
51  struct minimal_elements: public unary_cache_tag { };
52 
53  struct multiplesof: public binary_cache_tag { };
54  struct divisorsof: public binary_cache_tag { };
55  struct ll_red_nf: public binary_cache_tag { };
56  struct plug_1: public binary_cache_tag { };
57  struct exist_abstract: public binary_cache_tag { };
58 
59  struct degree: public unary_cache_tag { };
60 
61  struct has_factor_x: public binary_cache_tag { };
63 
64 
65  struct mod_varset: public binary_cache_tag { };
66  struct interpolate: public binary_cache_tag { };
67  struct zeros: public binary_cache_tag { };
69 
70  struct include_divisors: public unary_cache_tag { };
71 
72  //struct mod_deg2_set: public binary_cache_tag { };
75 
76  struct contained_deg2: public unary_cache_tag { };
78 
80 
81  struct lex_lead: public unary_cache_tag {};
84 
87 
89  struct testwise_ternary: public ternary_cache_tag { };
90 
91  struct used_variables: public unary_cache_tag { };
92 
93  struct block_degree: public binary_cache_tag { };
94 
95 
98  public ternary_cache_tag { };
99 
100  struct graded_part: public binary_cache_tag { };
101  struct mapping: public binary_cache_tag { };
102 
104 };
105 
106 // Reserve integer Numbers for Ternary operations (for cudd)
107 template <class TagType>
108 struct count_tags;
109 
110 template<>
111 struct count_tags<CCacheTypes::divisorsof_fixedpath>{
112  enum { value = 0 };
113 };
114 
115 template <class BaseTag>
117  enum{ value = count_tags<BaseTag>::value + 1 };
118 };
119 
120 template<>
121 class count_tags<CCacheTypes::testwise_ternary>:
122  public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ };
123 template<>
124 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
125  public increment_count_tags<CCacheTypes::testwise_ternary>{ };
126 template<>
127 class count_tags<CCacheTypes::has_factor_x_plus_y>:
128  public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ };
129 // generate tag number (special pattern with 4 usable bits)
130 // 18 bits are already used
131 template <unsigned Counted, unsigned Offset = 18>
133 public:
134  enum { value =
135  ( ((Counted + Offset) & 0x3 ) << 2) |
136  ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
137 };
138 
144 template <class MgrType>
146 public:
148  typedef MgrType manager_type;
149 
152 
154  typedef DdNode* node_type;
155 
158 
159 
160  // typedef CTypes::dd_base dd_base;
161  // typedef typename manager_type::mgrcore_ptr mgrcore_ptr;
162 
165 
167  typedef typename ring_type::dd_type dd_type;
168 
171  m_mgr(mgr) {}
172 
173 // CCuddLikeMgrStorage(const mgrcore_ptr& mgr):
174 // m_mgr(mgr) {}
175 
177  manager_type manager() const { return m_mgr; }
178 
180  dd_type generate(navigator navi) const {
181  return dd_type(m_mgr, navi);
182  }
183 
185  dd_type one() const {
186  return ring_type(m_mgr).one();//dd_type(m_mgr, DD_ONE(m_mgr->manager()));//manager().zddOne();
187  }
189  dd_type zero() const {
190  return ring_type(m_mgr).zero();//dd_base(m_mgr, PBORI_PREFIX(Cudd_ReadZero)(m_mgr->manager()));//manager().zddZero();
191  }
192 
193  ring_type ring() const { return ring_type(manager()); }
194 protected:
197  return m_mgr.getManager();
198  // return manager().getManager();
199  }
200 
201 private:
203  manager_type m_mgr;
204  // typename manager_type::mgrcore_ptr m_mgr;
205 };
206 
218 template <class ManagerType, class CacheType, unsigned ArgumentLength>
220 
221 // Fixing base type for Cudd-Like type CCuddInterface
222 template <class CacheType, unsigned ArgumentLength>
223 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > {
224 
226 };
227 
228 
229 // Fixing base type for Cudd-Like type CCuddInterface
230 template <class CacheType, unsigned ArgumentLength>
231 struct pbori_base<CCacheManBase<BoolePolyRing, CacheType, ArgumentLength> > {
232 
234 };
235 
236 // Fixing base type for Cudd-Like type CCuddInterface
237 template <class CacheType, unsigned ArgumentLength>
238 struct pbori_base<CCacheManBase<boost::intrusive_ptr<CCuddCore>, CacheType, ArgumentLength> > {
239 
241 };
242 // Dummy variant for generating empty cache managers, e.g. for using generate()
243 template <class ManagerType, class CacheType>
244 class CCacheManBase<ManagerType, CacheType, 0> :
245  public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
246 
247 public:
250 
252  typedef typename pbori_base<self>::type base;
253 
255 
256  typedef typename base::node_type node_type;
257  typedef typename base::navigator navigator;
258  typedef typename base::manager_type manager_type;
260 
262  CCacheManBase(const manager_type& mgr): base(mgr) {}
263 
265 
266  navigator find(navigator, ...) const { return navigator(); }
267  node_type find(node_type, ...) const { return NULL; }
268  void insert(...) const {}
270 };
271 
272 
273 // Variant for unary functions
274 template <class ManagerType, class CacheType>
275 class CCacheManBase<ManagerType, CacheType, 1> :
276  public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
277 
278 public:
281 
283  typedef typename pbori_base<self>::type base;
284 
286 
287  typedef typename base::node_type node_type;
288  typedef typename base::navigator navigator;
289  typedef typename base::manager_type manager_type;
291 
293  CCacheManBase(const manager_type& mgr): base(mgr) {}
294 
296  node_type find(node_type node) const {
297  return PBORI_PREFIX(cuddCacheLookup1Zdd)(internalManager(), cache_dummy, node);
298  }
299 
301  navigator find(navigator node) const {
302  return explicit_navigator_cast(find(node.getNode()));
303  }
304 
306  void insert(node_type node, node_type result) const {
307  PBORI_PREFIX(Cudd_Ref)(result);
308  PBORI_PREFIX(cuddCacheInsert1)(internalManager(), cache_dummy, node, result);
309  PBORI_PREFIX(Cudd_Deref)(result);
310  }
311 
313  void insert(navigator node, navigator result) const {
314  insert(node.getNode(), result.getNode());
315  }
316 
317 protected:
319  using base::internalManager;
320 
321 private:
323  static node_type cache_dummy(typename base::internal_manager_type,node_type){ // LCOV_EXCL_LINE
324  return NULL; // LCOV_EXCL_LINE
325  }
326 };
327 
328 // Variant for binary functions
329 template <class ManagerType, class CacheType>
330 class CCacheManBase<ManagerType, CacheType, 2> :
331  public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
332 
333 public:
336 
338  typedef typename pbori_base<self>::type base;
339 
341 
342  typedef typename base::node_type node_type;
343  typedef typename base::navigator navigator;
344  typedef typename base::manager_type manager_type;
346 
348  CCacheManBase(const manager_type& mgr): base(mgr) {}
349 
351  node_type find(node_type first, node_type second) const {
352  return PBORI_PREFIX(cuddCacheLookup2Zdd)(internalManager(), cache_dummy, first, second);
353  }
355  navigator find(navigator first, navigator second) const {
356  return explicit_navigator_cast(find(first.getNode(), second.getNode()));
357  }
358 
360  void insert(node_type first, node_type second, node_type result) const {
361  PBORI_PREFIX(Cudd_Ref)(result);
362  PBORI_PREFIX(cuddCacheInsert2)(internalManager(), cache_dummy, first, second, result);
363  PBORI_PREFIX(Cudd_Deref)(result);
364  }
365 
367  void insert(navigator first, navigator second, navigator result) const {
368  insert(first.getNode(), second.getNode(), result.getNode());
369  }
370 
371 protected:
373  using base::internalManager;
374 
375 private:
377  static node_type cache_dummy(typename base::internal_manager_type, // LCOV_EXCL_LINE
378  node_type, node_type){ // LCOV_EXCL_LINE
379  return NULL; // LCOV_EXCL_LINE
380  }
381 };
382 
383 // Variant for ternary functions
384 template <class ManagerType, class CacheType>
385 class CCacheManBase<ManagerType, CacheType, 3> :
386  public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
387 
388 public:
391 
393  typedef typename pbori_base<self>::type base;
394 
396 
397  typedef typename base::node_type node_type;
398  typedef typename base::navigator navigator;
399  typedef typename base::manager_type manager_type;
401 
403  CCacheManBase(const manager_type& mgr): base(mgr) {}
404 
406  node_type find(node_type first, node_type second, node_type third) const {
407  return PBORI_PREFIX(cuddCacheLookupZdd)(internalManager(), (ptruint)GENERIC_DD_TAG,
408  first, second, third);
409  }
410 
412  navigator find(navigator first, navigator second, navigator third) const {
413  return explicit_navigator_cast(find(first.getNode(), second.getNode(),
414  third.getNode()));
415  }
416 
418  void insert(node_type first, node_type second, node_type third,
419  node_type result) const {
420  PBORI_PREFIX(Cudd_Ref)(result);
421  PBORI_PREFIX(cuddCacheInsert)(internalManager(), (ptruint)GENERIC_DD_TAG,
422  first, second, third, result);
423  PBORI_PREFIX(Cudd_Deref)(result);
424  }
426  void insert(navigator first, navigator second, navigator third,
427  navigator result) const {
428  insert(first.getNode(), second.getNode(), third.getNode(),
429  result.getNode());
430  }
431 
432 protected:
434  using base::internalManager;
435 
436 private:
437  enum { GENERIC_DD_TAG =
439 };
440 
453 template <class ManagerType, class CacheType,
454  unsigned ArgumentLength = CacheType::nargs>
456  public CCacheManBase<ManagerType,
457  CacheType, ArgumentLength> {
458 public:
459 
461 
462  typedef ManagerType manager_type;
466  typedef CacheType cache_type;
467  enum { nargs = ArgumentLength };
469 
472 
474  typedef typename base::node_type node_type;
475 
478  base(mgr) {}
479 
480  using base::find;
481  using base::insert;
482 };
483 
487 template <class ManagerType, class CacheType>
489  public CCacheManagement<ManagerType, CacheType, 2> {
490 
491 public:
493 
494  typedef ManagerType manager_type;
495  typedef CacheType cache_type;
497 
500 
502  typedef typename base::node_type node_type;
503  typedef typename base::navigator navigator;
504 
506  CCommutativeCacheManagement(const typename base::manager_type& mgr):
507  base(mgr) {}
508 
510  node_type find(node_type first, node_type second) const {
511  if ( std::less<node_type>()(first, second) )
512  return base::find(first, second);
513  else
514  return base::find(second, first);
515  }
516 
518  navigator find(navigator first, navigator second) const {
519  return explicit_navigator_cast(find(first.getNode(), second.getNode()));
520  }
521 
522 
524  void insert(node_type first, node_type second, node_type result) const {
525  if ( std::less<node_type>()(first, second) )
526  base::insert(first, second, result);
527  else
528  base::insert(second, first, result);
529  }
530 
532  void insert(navigator first, navigator second, navigator result) const {
533  insert(first.getNode(), second.getNode(), result.getNode());
534  }
535 
536 };
537 
539 
540 #endif