mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

work on Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-09 10:33:47 -07:00
parent 7d13bcb18e
commit 2c1d68e163
3 changed files with 47 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

84
src/math/grobner/grobner.cpp
View file

@ -581,6 +581,45 @@ grobner::equation * grobner::copy_equation(equation const * eq) {
return r;
}
bool grobner::simplify_for_loop(equation const * source, equation * target, bool & result, unsigned& j ) {
bool simplified = false;
unsigned i = 0;
j = 0;
unsigned sz = target->m_monomials.size();
monomial const * LT = source->get_monomial(0);
ptr_vector<monomial> & new_monomials = m_tmp_monomials;
new_monomials.reset();
ptr_vector<expr> & rest = m_tmp_vars1;
for (; i < sz; i++) {
monomial * curr = target->m_monomials[i];
rest.reset();
if (is_subset(LT, curr, rest)) {
if (i == 0)
m_changed_leading_term = true;
if (!result) {
// first time that source is being applied.
target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
}
simplified = true;
result = true;
rational coeff = curr->m_coeff;
coeff /= LT->m_coeff;
coeff.neg();
if (!rest.empty())
target->m_lc = false;
mul_append(1, source, coeff, rest, new_monomials);
del_monomial(curr);
target->m_monomials[i] = 0;
}
else {
target->m_monomials[j] = curr;
j++;
}
}
return simplified;
}
/**
\brief Simplify the target equation using the source as a rewrite rule.
Return 0 if target was not simplified.
@ -593,49 +632,18 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
return nullptr;
m_stats.m_simplify++;
bool result = false;
bool simplified;
do {
simplified = false;
unsigned i = 0;
unsigned j = 0;
unsigned sz = target->m_monomials.size();
monomial const * LT = source->get_monomial(0);
ptr_vector<monomial> & new_monomials = m_tmp_monomials;
new_monomials.reset();
ptr_vector<expr> & rest = m_tmp_vars1;
for (; i < sz; i++) {
monomial * curr = target->m_monomials[i];
rest.reset();
if (is_subset(LT, curr, rest)) {
if (i == 0)
m_changed_leading_term = true;
if (!result) {
// first time that source is being applied.
target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
}
simplified = true;
result = true;
rational coeff = curr->m_coeff;
coeff /= LT->m_coeff;
coeff.neg();
if (!rest.empty())
target->m_lc = false;
mul_append(1, source, coeff, rest, new_monomials);
del_monomial(curr);
target->m_monomials[i] = 0;
}
else {
target->m_monomials[j] = curr;
j++;
}
}
if (simplified) {
unsigned j;
if( simplify_for_loop(source, target, result, j)) {
target->m_monomials.shrink(j);
target->m_monomials.append(new_monomials.size(), new_monomials.c_ptr());
target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
simplify(target);
} else {
break;
}
}
while (simplified && !m_manager.canceled());
while (!m_manager.canceled());
TRACE("grobner", tout << "result: "; display_equation(tout, *target););
return result ? target : nullptr;
}

1
src/math/grobner/grobner.h
View file

@ -166,6 +166,7 @@ protected:
equation * copy_equation(equation const * eq);
equation * simplify(equation const * source, equation * target);
bool simplify_for_loop(equation const * source, equation * target, bool&, unsigned &);
equation * simplify_using_processed(equation * eq);

4
src/math/lp/var_eqs.h
View file

@ -344,8 +344,4 @@ public:
}
}
}; // end of var_eqs
// template <typename T>
// std::ostream& operator<<(var_eqs<T> const& ve, std::ostream& out) { return ve.display(out); }
}