PolyBoRi
contained_variables.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_groebner_contained_variables_h_
17 #define polybori_groebner_contained_variables_h_
18 
19 // include basic definitions
20 #include "groebner_defs.h"
21 
23 
24 inline MonomialSet
26 
28  MonomialSet::navigator orig=nav;
29  typedef PBORI::CacheManager<CCacheTypes::contained_variables>
30  cache_mgr_type;
31 
32  cache_mgr_type cache_mgr(m.ring());
33 
34 
35  while (!(nav.isConstant())){
36  MonomialSet::navigator cached =
37  cache_mgr.find(nav);
38  if (cached.isValid()) return cache_mgr.generate(cached);
39  idx_type v=*nav;
40  MonomialSet::navigator check_nav=nav.thenBranch();
41  while(!(check_nav.isConstant())){
42  check_nav.incrementElse();
43  }
44  if (check_nav.isTerminated()){
45  idx_type result_index=v;
46  MonomialSet result=MonomialSet(result_index,Polynomial(cache_mgr.one()).diagram(),contained_variables_cudd_style(cache_mgr.generate(nav.elseBranch())));
47  MonomialSet::navigator r_nav=result.navigation();
48  while(1){
49  MonomialSet::navigator last=orig;
50  cache_mgr.insert(orig, r_nav);
51  orig.incrementElse();
52  if(last==nav) break;
53  }
54  return result;
55  }
56  nav.incrementElse();
57 
58  }
59  return MonomialSet(cache_mgr.zero());
60 }
61 
62 inline MonomialSet
64 
66 
67  typedef PBORI::CacheManager<CCacheTypes::contained_deg2>
68  cache_mgr_type;
69 
70  cache_mgr_type cache_mgr(m.ring());
71 
72 
73  if (!(nav.isConstant())){
74  MonomialSet::navigator cached =
75  cache_mgr.find(nav);
76  if (cached.isValid()) return cache_mgr.generate(cached);
77  MonomialSet::navigator then_branch=nav.thenBranch();
78  MonomialSet::navigator else_branch=nav.elseBranch();
79  MonomialSet then_res=contained_variables_cudd_style(cache_mgr.generate(then_branch));
80  MonomialSet else_res=contained_deg2_cudd_style(cache_mgr.generate(else_branch));
81  MonomialSet result=MonomialSet(*nav,then_res,else_res);
82  cache_mgr.insert(nav,result.navigation());
83  return result;
84  }
85  else return MonomialSet(cache_mgr.zero());
86 }
87 
88 
89 
90 inline std::vector<idx_type>
92  std::vector<idx_type> result;
94  while (!(nav.isConstant())){
95  idx_type v=*nav;
96  MonomialSet::navigator check_nav=nav.thenBranch();
97  while(!(check_nav.isConstant())){
98  check_nav.incrementElse();
99  }
100  if (check_nav.isTerminated()){
101  result.push_back(v);
102  }
103  nav.incrementElse();
104 
105  }
106  return result;
107 }
108 
109 
111 
112 #endif /* polybori_groebner_contained_variables_h_ */
MonomialSet contained_deg2_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:63
std::vector< idx_type > contained_variables(const MonomialSet &m)
Definition: contained_variables.h:91
MonomialSet contained_variables_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:25
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
BoolePolynomial Polynomial
Definition: embed.h:51
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
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
bool_type isTerminated() const
Check whether end of path was reached.
Definition: CCuddNavigator.h:128
self thenBranch() const
Increment in then direction.
Definition: CCuddNavigator.h:92
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
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