PolyBoRi
CCacheManagement.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
157 //*****************************************************************************
158 
159 // include basic definitions
160 #include "pbori_defs.h"
161 
162 // get DD navigation
163 #include "CCuddNavigator.h"
164 #include "CDDInterface.h"
165 #include "BooleRing.h"
166 // get standard functionality
167 #include <functional>
168 
169 #ifndef CCacheManagement_h_
170 #define CCacheManagement_h_
171 
173 
174 
175 class CCacheTypes {
176 
177 public:
178  struct no_cache_tag { enum { nargs = 0 }; };
179  struct unary_cache_tag { enum { nargs = 1 }; };
180  struct binary_cache_tag { enum { nargs = 2 }; };
181  struct ternary_cache_tag { enum { nargs = 3 }; };
182 
183  // user functions
184  struct no_cache: public no_cache_tag { };
185  struct union_xor: public binary_cache_tag { };
186 
188  struct divide: public binary_cache_tag { };
189 
190  struct minimal_mod: public binary_cache_tag { };
191  struct minimal_elements: public unary_cache_tag { };
192 
193  struct multiplesof: public binary_cache_tag { };
194  struct divisorsof: public binary_cache_tag { };
195  struct ll_red_nf: public binary_cache_tag { };
196  struct plug_1: public binary_cache_tag { };
197  struct exist_abstract: public binary_cache_tag { };
198 
199  struct degree: public unary_cache_tag { };
200 
201  struct has_factor_x: public binary_cache_tag { };
203 
204 
205  struct mod_varset: public binary_cache_tag { };
206  struct interpolate: public binary_cache_tag { };
207  struct zeros: public binary_cache_tag { };
209 
210  struct include_divisors: public unary_cache_tag { };
211 
212  //struct mod_deg2_set: public binary_cache_tag { };
215 
216  struct contained_deg2: public unary_cache_tag { };
218 
220 
221  struct dlex_lead: public unary_cache_tag { };
222  struct dp_asc_lead: public unary_cache_tag { };
223 
226 
227  struct used_variables: public unary_cache_tag { };
228 
229  struct block_degree: public binary_cache_tag { };
230  struct block_dlex_lead: public unary_cache_tag { };
231 
234  public ternary_cache_tag { };
235 
236  struct graded_part: public binary_cache_tag { };
237  struct mapping: public binary_cache_tag { };
238 
240 };
241 
242 // Reserve integer Numbers for Ternary operations (for cudd)
243 template <class TagType>
244 struct count_tags;
245 
246 template<>
247 struct count_tags<CCacheTypes::divisorsof_fixedpath>{
248  enum { value = 0 };
249 };
250 
251 template <class BaseTag>
253  enum{ value = count_tags<BaseTag>::value + 1 };
254 };
255 
256 template<>
257 class count_tags<CCacheTypes::testwise_ternary>:
258  public increment_count_tags<CCacheTypes::divisorsof_fixedpath>{ };
259 template<>
260 class count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>:
261  public increment_count_tags<CCacheTypes::testwise_ternary>{ };
262 template<>
263 class count_tags<CCacheTypes::has_factor_x_plus_y>:
264  public increment_count_tags<CCacheTypes::left_equals_right_x_branch_and_r_has_fac_x>{ };
265 // generate tag number (special pattern with 4 usable bits)
266 // 18 bits are already used
267 template <unsigned Counted, unsigned Offset = 18>
269 public:
270  enum { value =
271  ( ((Counted + Offset) & 0x3 ) << 2) |
272  ( ((Counted + Offset) & 0x1C ) << 3) | 0x2 };
273 };
274 
280 template <class MgrType>
282 public:
284  typedef MgrType manager_type;
285 
287  typedef DdManager* internal_manager_type;
288 
290  typedef DdNode* node_type;
291 
294 
298  typedef typename manager_type::mgrcore_ptr mgrcore_ptr;
299 
302 
305  m_mgr(mgr.managerCore()) {}
306 
308  m_mgr(mgr) {}
309 
311  manager_type manager() const { return m_mgr; }
312 
314  dd_type generate(navigator navi) const {
315  return dd_base(m_mgr, navi.getNode());
316  }
317 
319  dd_type one() const {
320  return dd_base(m_mgr, DD_ONE(m_mgr->manager));//manager().zddOne();
321  }
323  dd_type zero() const {
324  return dd_base(m_mgr, Cudd_ReadZero(m_mgr->manager));//manager().zddZero();
325  }
326 
327  ring_type ring() const { return ring_type(manager()); }
328 protected:
331  return m_mgr->manager;
332  // return manager().getManager();
333  }
334 
335 private:
337  // const manager_type& m_mgr;
338  typename manager_type::mgrcore_ptr m_mgr;
339 };
340 
350 template <class ManagerType, class CacheType, unsigned ArgumentLength>
351 class CCacheManBase;
352 
353 // Fixing base type for Cudd-Like type Cudd
354 template <class CacheType, unsigned ArgumentLength>
355 struct pbori_base<CCacheManBase<Cudd, CacheType, ArgumentLength> > {
356 
358 };
359 
360 // Fixing base type for Cudd-Like type CCuddInterface
361 template <class CacheType, unsigned ArgumentLength>
362 struct pbori_base<CCacheManBase<CCuddInterface, CacheType, ArgumentLength> > {
363 
365 };
366 
367 // Dummy variant for generating empty cache managers, e.g. for using generate()
368 template <class ManagerType, class CacheType>
369 class CCacheManBase<ManagerType, CacheType, 0> :
370  public pbori_base<CCacheManBase<ManagerType, CacheType, 0> >::type {
371 
372 public:
375 
377  typedef typename pbori_base<self>::type base;
378 
380 
381  typedef typename base::node_type node_type;
382  typedef typename base::navigator navigator;
383  typedef typename base::manager_type manager_type;
385 
387  CCacheManBase(const manager_type& mgr): base(mgr) {}
388 
390 
391  navigator find(navigator, ...) const { return navigator(); }
392  node_type find(node_type, ...) const { return NULL; }
393  void insert(...) const {}
395 };
396 
397 
398 // Variant for unary functions
399 template <class ManagerType, class CacheType>
400 class CCacheManBase<ManagerType, CacheType, 1> :
401  public pbori_base<CCacheManBase<ManagerType, CacheType, 1> >::type {
402 
403 public:
406 
408  typedef typename pbori_base<self>::type base;
409 
411 
412  typedef typename base::node_type node_type;
413  typedef typename base::navigator navigator;
414  typedef typename base::manager_type manager_type;
416 
418  CCacheManBase(const manager_type& mgr): base(mgr) {}
419 
421  node_type find(node_type node) const {
422  return cuddCacheLookup1Zdd(internalManager(), cache_dummy, node);
423  }
424 
426  navigator find(navigator node) const {
427  return explicit_navigator_cast(find(node.getNode()));
428  }
429 
431  void insert(node_type node, node_type result) const {
432  Cudd_Ref(result);
433  cuddCacheInsert1(internalManager(), cache_dummy, node, result);
434  Cudd_Deref(result);
435  }
436 
438  void insert(navigator node, navigator result) const {
439  insert(node.getNode(), result.getNode());
440  }
441 
442 protected:
444  using base::internalManager;
445 
446 private:
448  static node_type cache_dummy(typename base::internal_manager_type,node_type){
449  return NULL;
450  }
451 };
452 
453 // Variant for binary functions
454 template <class ManagerType, class CacheType>
455 class CCacheManBase<ManagerType, CacheType, 2> :
456  public pbori_base<CCacheManBase<ManagerType, CacheType, 2> >::type {
457 
458 public:
461 
463  typedef typename pbori_base<self>::type base;
464 
466 
467  typedef typename base::node_type node_type;
468  typedef typename base::navigator navigator;
469  typedef typename base::manager_type manager_type;
471 
473  CCacheManBase(const manager_type& mgr): base(mgr) {}
474 
476  node_type find(node_type first, node_type second) const {
477  return cuddCacheLookup2Zdd(internalManager(), cache_dummy, first, second);
478  }
480  navigator find(navigator first, navigator second) const {
481  return explicit_navigator_cast(find(first.getNode(), second.getNode()));
482  }
483 
485  void insert(node_type first, node_type second, node_type result) const {
486  Cudd_Ref(result);
487  cuddCacheInsert2(internalManager(), cache_dummy, first, second, result);
488  Cudd_Deref(result);
489  }
490 
492  void insert(navigator first, navigator second, navigator result) const {
493  insert(first.getNode(), second.getNode(), result.getNode());
494  }
495 
496 protected:
498  using base::internalManager;
499 
500 private:
502  static node_type cache_dummy(typename base::internal_manager_type,
503  node_type, node_type){
504  return NULL;
505  }
506 };
507 
508 // Variant for ternary functions
509 template <class ManagerType, class CacheType>
510 class CCacheManBase<ManagerType, CacheType, 3> :
511  public pbori_base<CCacheManBase<ManagerType, CacheType, 3> >::type {
512 
513 public:
516 
518  typedef typename pbori_base<self>::type base;
519 
521 
522  typedef typename base::node_type node_type;
523  typedef typename base::navigator navigator;
524  typedef typename base::manager_type manager_type;
526 
528  CCacheManBase(const manager_type& mgr): base(mgr) {}
529 
531  node_type find(node_type first, node_type second, node_type third) const {
532  return cuddCacheLookupZdd(internalManager(), (ptruint)GENERIC_DD_TAG,
533  first, second, third);
534  }
535 
537  navigator find(navigator first, navigator second, navigator third) const {
538  return explicit_navigator_cast(find(first.getNode(), second.getNode(),
539  third.getNode()));
540  }
541 
543  void insert(node_type first, node_type second, node_type third,
544  node_type result) const {
545  Cudd_Ref(result);
546  cuddCacheInsert(internalManager(), (ptruint)GENERIC_DD_TAG,
547  first, second, third, result);
548  Cudd_Deref(result);
549  }
551  void insert(navigator first, navigator second, navigator third,
552  navigator result) const {
553  insert(first.getNode(), second.getNode(), third.getNode(),
554  result.getNode());
555  }
556 
557 protected:
559  using base::internalManager;
560 
561 private:
562  enum { GENERIC_DD_TAG =
564 };
565 
578 template <class CacheType,
579  unsigned ArgumentLength = CacheType::nargs>
581  public CCacheManBase<typename CTypes::manager_base,
582  CacheType, ArgumentLength> {
583 public:
584 
586 
589  typedef CacheType cache_type;
590  enum { nargs = ArgumentLength };
592 
595 
597  typedef typename base::node_type node_type;
598 
601  base(mgr) {}
602 
603  using base::find;
604  using base::insert;
605 };
606 
610 template <class CacheType>
612  public CCacheManagement<CacheType, 2> {
613 
614 public:
616 
617  typedef CacheType cache_type;
619 
622 
624  typedef typename base::node_type node_type;
625  typedef typename base::navigator navigator;
626 
629  base(mgr) {}
630 
632  node_type find(node_type first, node_type second) const {
633  if ( std::less<node_type>()(first, second) )
634  return base::find(first, second);
635  else
636  return base::find(second, first);
637  }
638 
640  navigator find(navigator first, navigator second) const {
641  return explicit_navigator_cast(find(first.getNode(), second.getNode()));
642  }
643 
644 
646  void insert(node_type first, node_type second, node_type result) const {
647  if ( std::less<node_type>()(first, second) )
648  base::insert(first, second, result);
649  else
650  base::insert(second, first, result);
651  }
652 
654  void insert(navigator first, navigator second, navigator result) const {
655  insert(first.getNode(), second.getNode(), result.getNode());
656  }
657 
658 };
659 
661 
662 #endif