16 #ifndef polybori_groebner_minimal_elements_h_
17 #define polybori_groebner_minimal_elements_h_
58 s1=s1.diff(s0.unateProduct(
Polynomial(s1).usedVariablesExp().divisors(s.
ring())));
61 return s0.unite(s1.
change(i));
77 if ((cv.size()>0) && (s.
length()==cv.size())){
83 for(z=cv.size()-1;z>=0;z--){
85 cv_set=cv_set.unite(mv.
diagram());
87 for(z=0;z<cv.size();z++){
93 if (s.
isZero())
return result;
126 s1=s1.diff(s0.unateProduct(
Polynomial(s1).usedVariables().divisors()));
129 return s0.unite(s1.
change(i)).unite(result);
133 inline std::vector<Exponent>
135 std::vector<Exponent> result;
136 if (s.
isZero())
return result;
152 std::vector<Exponent> exponents;
156 std::vector<std::vector<int> > occ_vecs(nvars);
161 occ_vecs[*it].push_back(i);
170 std::vector<bool> still_minimal(exponents.size());
172 still_minimal[i]=
true;
177 if (still_minimal[i]){
182 std::vector<int> occ_set=occ_vecs[first_index];
186 std::vector<int> occ_set_next;
190 occ_vecs[*it].begin(),
192 std::back_insert_iterator<std::vector<int> >(occ_set_next));
193 occ_set=occ_set_next;
197 std::vector<int>::const_iterator oc_it= occ_set.begin();
198 std::vector<int>::const_iterator oc_end= occ_set.end();
199 while(oc_it!=oc_end){
200 still_minimal[*oc_it]=
false;
204 it=((
const Exponent&) exponents[i]).begin();
206 std::vector<int> occ_set_difference;
208 occ_vecs[*it].begin(),
212 std::back_insert_iterator<std::vector<int> >(occ_set_difference));
213 occ_vecs[*it]=occ_set_difference;
216 result.push_back(exponents[i]);
237 std::cout <<
"ERROR minimalElements"<<std::endl;
238 std::cout <<
"orig "<<s<< std::endl;
239 std::cout <<
"correct "<<minElts<< std::endl;
263 typedef PBORI::CacheManager<CCacheTypes::minimal_elements>
268 cache_mgr_type cache_mgr(m.
ring());
269 PBORI::BoolePolynomial::navigator cached =
270 cache_mgr.find(m_nav);
274 if (cached.isValid() ){
275 return cache_mgr.generate(cached);
281 if ((minimal_else.
navigation()==ms0) &&(minimal_then.navigation()==ms1)) result=m;
283 result=
MonomialSet(*m_nav,minimal_then,minimal_else);
285 cache_mgr.insert(m_nav, result.navigation());
308 if (m.
isZero())
return cv;
309 bool cv_empty=cv.
isZero();
320 while((!(nav_mod.
isConstant())) && (index>*nav_mod)){
332 typedef PBORI::CacheManager<CCacheTypes::minimal_mod>
337 cache_mgr_type cache_mgr(m.
ring());
338 PBORI::BoolePolynomial::navigator cached =
339 cache_mgr.find(m_nav, mod_nav);
343 if (cached.isValid() ){
344 return cv.unite((
MonomialSet)cache_mgr.generate(cached));
360 cache_mgr.generate(ms1),result0.unite(mod));
361 if (result1.isZero()) {result=result0;}
373 result0.unite(cache_mgr.generate(ms0).unite(cache_mgr.generate(mod1))));
378 if (cv_empty)
return result;
380 return cv.unite(result);
399 return m.unateProduct(lm.
set());
404 inline std::vector<Monomial>
408 return std::vector<Monomial>(result.
begin(), result.
end());
414 #ifdef MIN_ELEMENTS_BINARY
418 if (m.divisorsOf(lm).isZero()){
419 m=divide_monomial_divisors_out(m,lm);
423 return m.ring().one();
447 std::vector<Exponent>& result){
449 result.resize(elements.
length());
450 std::copy(elements.
expBegin(), elements.
expEnd(), result.begin());
self minimalElements() const
Get minimal elements wrt. inclusion.
Definition: BooleSet.cc:207
MonomialSet contained_deg2_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:63
dd_type one() const
Get decision diagram with all variables negated.
Definition: BoolePolyRing.cc:46
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
MonomialSet do_minimal_elements_cudd_style(MonomialSet m, MonomialSet mod)
Definition: minimal_elements.h:290
std::vector< idx_type > contained_variables(const MonomialSet &m)
Definition: contained_variables.h:91
bool_type reducibleBy(const self &rhs) const
Test for reducibility.
Definition: BooleMonomial.h:190
bool_type isOne() const
Check whether polynomial is constant one.
Definition: BoolePolynomial.h:297
MonomialSet contained_variables_cudd_style(const MonomialSet &m)
Definition: contained_variables.h:25
polybori::BooleExponent Exponent
Definition: groebner_defs.h:33
set_type set() const
Get corresponding subset of of the powerset over all variables.
Definition: BooleMonomial.h:216
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
self existAbstract(const term_type &rhs) const
Definition: BooleSet.cc:252
MonomialSet minimal_elements_internal(const MonomialSet &s)
Definition: minimal_elements.h:33
bool_type hasConstantPart() const
Check whether polynomial has term one.
Definition: BoolePolynomial.h:303
self divisorsOf(const term_type &rhs) const
Compute intersection with divisors of rhs.
Definition: BooleSet.cc:156
MonomialSet mod_deg2_set(const MonomialSet &as, const MonomialSet &vs)
Definition: groebner_alg.cc:135
exp_iterator expEnd() const
Finish of iteration over exponent vectors.
Definition: BooleSet.cc:109
MonomialSet mod_var_set(const MonomialSet &as, const MonomialSet &vs)
Definition: groebner_alg.cc:85
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 & insert(idx_type)
Insert variable with index idx in exponent vector.
Definition: BooleExponent.cc:171
self elseBranch() const
Increment in else direction.
Definition: CCuddNavigator.h:98
exp_iterator expBegin() const
Start of iteration over exponent vectors.
Definition: BooleSet.cc:101
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
BooleVariable Variable
Definition: embed.h:52
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
std::vector< Monomial > minimal_elements_multiplied(MonomialSet m, Monomial lm)
Definition: minimal_elements.h:405
MonomialSet minimal_elements_internal2(MonomialSet s)
Definition: minimal_elements.h:66
MonomialSet mod_mon_set(const MonomialSet &as, const MonomialSet &vs)
Definition: nf.cc:855
MonomialSet minimal_elements_cudd_style_unary(MonomialSet m)
Definition: minimal_elements.h:252
self thenBranch() const
Increment in then direction.
Definition: CCuddNavigator.h:92
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
MonomialSet minimal_elements(const MonomialSet &s)
Definition: minimal_elements.h:225
size_type nVariables() const
Get number of ring variables.
Definition: BoolePolyRing.h:126
bool_type ownsOne() const
Test whether the empty set is included.
Definition: BooleSet.h:211
MonomialSet minimal_elements_cudd_style(MonomialSet m)
Definition: minimal_elements.h:384
const dd_type & diagram() const
Read-only access to internal decision diagramm structure.
Definition: BooleMonomial.h:213
const_iterator end() const
Finish of iteration over terms.
Definition: BooleSet.cc:78
Definition: BoolePolynomial.h:70
self change(idx_type idx) const
Definition: BooleSet.h:169
void minimal_elements_divided(MonomialSet m, Monomial lm, MonomialSet mod, std::vector< Exponent > &result)
Definition: minimal_elements.h:446
std::vector< Exponent > minimal_elements_internal3(MonomialSet s)
Definition: minimal_elements.h:134
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
MonomialSet minimal_elements_multiplied_monoms(MonomialSet m, Monomial lm)
Definition: minimal_elements.h:393
data_type::const_iterator const_iterator
Definition: BooleExponent.h:52
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
const_iterator begin() const
Start of iteration over terms.
Definition: BooleSet.cc:70
size_type length() const
Returns number of terms (deprecated)
Definition: BooleSet.h:245
Definition: BooleSet.h:57
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
self & push_back(idx_type idx)
Insert variable with index idx in exponent vector (trying end first)
Definition: BooleExponent.cc:188