PolyBoRi
fixed_path_divisors.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_groebner_fixed_path_divisors_h_
17 #define polybori_groebner_fixed_path_divisors_h_
18 
19 // include basic definitions
20 #include "groebner_defs.h"
21 
23 
24 #ifndef DANGEROUS_FIXED_PATH
25  typedef PBORI::CacheManager<CCacheTypes::divisorsof_fixedpath>
26 #else
27  typedef PBORI::CacheManager<CCacheTypes::divisorsof>
28 #endif
30 
31 // Variant navigator
32 inline MonomialSet
37 
38  if (n_nav.isTerminated()) return
39  MonomialSet(cache_mgr.generate(a_nav)).firstDivisorsOf(cache_mgr.generate(m_nav));
40  PBORI_ASSERT(!(n_nav.isConstant()&&(!(n_nav.terminalValue()))));
41 
42  if (a_nav.isConstant()) return cache_mgr.generate(a_nav);
43 
44  PBORI_ASSERT(!(n_nav.isConstant()));
45  PBORI_ASSERT(!(m_nav.isConstant()));
46  int m_index=*m_nav;
47  int n_index=*n_nav;
48  int a_index=*a_nav;
49 
50  PBORI_ASSERT(m_index<=n_index);
51 
52 
53  //here we rely on the fact, that in Cudd deref of constant nav. gives a bigger index than allow allowed real indices
54  while((a_index=*a_nav)!=(m_index=*m_nav)){
55  if (a_index<m_index) a_nav.incrementElse();
56  else{
57  n_index=*n_nav;
58  PBORI_ASSERT(n_index>=m_index);
59  if (m_index==n_index){
60  n_nav.incrementThen();
61  m_nav.incrementThen();
62  } else {
63  m_nav.incrementThen();
64  }
65  }
66 
67  }
68  n_index=*n_nav;
69 
70  if (a_nav.isConstant()){
71  return cache_mgr.generate(a_nav);
72  }
73  PBORI_ASSERT((*a_nav)==(*m_nav));
74 
76  #ifndef DANGEROUS_FIXED_PATH
77  cached =
78  cache_mgr.find(a_nav, m_nav,n_nav);
79  if (cached.isValid() ){
80  return cache_mgr.generate(cached);
81  }
82  #else
83  //MonomialSet::navigator cached =
84  //cache_mgr.find(a_nav, m_nav);
85  #endif
86 
87 
88  // here it is theoretically possible to get answers which don't contain the
89  // fixed path n, but that doesn't matter in practice,
90  // as it is optimization anyway
91  typedef PBORI::CacheManager<CCacheTypes::divisorsof>
92  cache_mgr_type2;
93 
94  cache_mgr_type2 cache_mgr2(cache_mgr.manager());
95 
96  cached =
97  cache_mgr2.find(a_nav, m_nav);
98 
99  if (cached.isValid()){
100  return cache_mgr2.generate(cached);
101  }
102 
103  PBORI_ASSERT(a_index==m_index);
104  int index=m_index;
105  MonomialSet result(cache_mgr.zero());
106  if (m_index==n_index){
107  result=do_fixed_path_divisors(cache_mgr, a_nav.thenBranch(),
108  m_nav.thenBranch(), n_nav.thenBranch());
109  if (!(result.isZero()))
110  result = MonomialSet(index, result, cache_mgr.zero());
111  } else {
113  then_path=do_fixed_path_divisors(cache_mgr, a_nav.thenBranch(),
114  m_nav.thenBranch(), n_nav);
116  else_path=do_fixed_path_divisors(cache_mgr, a_nav.elseBranch(),
117  m_nav.thenBranch(), n_nav);
118  if (then_path.isZero()){
119  result=else_path;
120  } else {
121  result=MonomialSet(index,then_path,else_path);
122  }
123  }
124 #ifndef DANGEROUS_FIXED_PATH
125  cache_mgr.insert(a_nav,m_nav,n_nav,result.navigation());
126 #else
127  cache_mgr2.insert(a_nav,m_nav,result.navigation());
128 #endif
129  return result;
130 }
131 // end of variant for navigator
132 
133 // variant for MonomialSet
134 inline MonomialSet
136  MonomialSet m, MonomialSet n){
137 
138  //we assume that m is a multiple of n
141 
143 
144  typedef fixed_divisors_cache_type cache_mgr_type;
145  cache_mgr_type cache_mgr(a.ring());
146 
147  return do_fixed_path_divisors(cache_mgr, a_nav, m_nav, n_nav);
148 }
149 
150 
151 inline MonomialSet
154  return do_fixed_path_divisors(a,m.diagram(),n.diagram());
155 }
156 
157 
159 
160 #endif /* polybori_groebner_fixed_path_divisors_h_ */
bool_type reducibleBy(const self &rhs) const
Test for reducibility.
Definition: BooleMonomial.h:190
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
Definition: CacheManager.h:31
navigator navigation() const
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Definition: CCuddDDFacade.h:455
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
self elseBranch() const
Increment in else direction.
Definition: CCuddNavigator.h:98
MonomialSet fixed_path_divisors(MonomialSet a, Monomial m, Monomial n)
Definition: fixed_path_divisors.h:152
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
bool_type isTerminated() const
Check whether end of path was reached.
Definition: CCuddNavigator.h:128
polybori::CacheManager< CCacheTypes::divisorsof_fixedpath > fixed_divisors_cache_type
Definition: fixed_path_divisors.h:29
self thenBranch() const
Increment in then direction.
Definition: CCuddNavigator.h:92
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
const dd_type & diagram() const
Read-only access to internal decision diagramm structure.
Definition: BooleMonomial.h:213
self & incrementThen()
Increment in then direction.
Definition: CCuddNavigator.h:191
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
bool_type isConstant() const
Check whether constant node was reached.
Definition: CCuddNavigator.h:172
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
self & incrementElse()
Increment in else direction.
Definition: CCuddNavigator.h:203
Definition: BooleSet.h:57
bool_type terminalValue() const
Check whether terminal node marks end of path.
Definition: CCuddNavigator.h:181
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
MonomialSet do_fixed_path_divisors(MonomialSet a, MonomialSet m, MonomialSet n)
Definition: fixed_path_divisors.h:135