mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

port Grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-10 15:59:28 -07:00
parent 1e5ade1dc2
commit 5e40d64a82
3 changed files with 149 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -619,7 +619,9 @@ unsigned grobner::simplify_loop_on_target_monomials(equation const * source, equ
/**
\brief Simplify the target equation using the source as a rewrite rule.
Return 0 if target was not simplified.
Return target if target was simplified but source->m_scope_lvl <= target->m_scope_lvl.
LN. The rest of the comment seems to be incorrect: there is no m_scope_lvl
Return target if target was simplified
Return new_equation if source->m_scope_lvl > target->m_scope_lvl, moreover target is freezed, and new_equation contains the result.
*/
grobner::equation * grobner::simplify_source_target(equation const * source, equation * target) {

150
src/math/lp/nla_grobner.cpp
View file

@ -25,7 +25,9 @@ nla_grobner::nla_grobner(core *c
) :
common(c),
m_nl_gb_exhausted(false),
m_dep_manager(m_val_manager, m_alloc) {}
m_dep_manager(m_val_manager, m_alloc),
m_changed_leading_term(false)
{}
// Scan the grobner basis eqs for equations of the form x - k = 0 or x = 0 is found, and x is not fixed,
// then assert bounds for x, and continue
@ -255,23 +257,149 @@ nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) {
}
nla_grobner::equation* nla_grobner::simplify_processed(equation* eq) {
unsigned nla_grobner::simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result) {
unsigned i = 0;
unsigned n_sz = 0;
unsigned sz = target->m_exp->size();
NOT_IMPLEMENTED_YET();
return nullptr;
/*
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);
}
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);
}
else {
target->m_monomials[n_sz++] = curr;
}
}*/
return n_sz;
}
nla_grobner::equation* nla_grobner::simplify_to_process(equation*) {
NOT_IMPLEMENTED_YET();
return nullptr;
nla_grobner::equation * nla_grobner::simplify_source_target(equation const * source, equation * target) {
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
if (source->get_num_monomials() == 0)
return nullptr;
m_stats.m_simplify++;
bool result = false;
do {
unsigned target_new_size = simplify_loop_on_target_monomials(source, target, result);
if (target_new_size < target->m_exp->size()) {
NOT_IMPLEMENTED_YET();
/*
target->m_monomials.shrink(target_new_size);
target->m_monomials.append(m_tmp_monomials.size(), m_tmp_monomials.c_ptr());
simplify_eq(target);
*/
} else {
NOT_IMPLEMENTED_YET();
break;
}
}
while (!canceled());
TRACE("grobner", tout << "result: "; display_equation(tout, *target););
return result ? target : nullptr;
}
void nla_grobner::process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove) {
if (new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_remove.push_back(target);
if (m_changed_leading_term) {
m_to_process.insert(new_target);
to_remove.push_back(target);
}
else {
to_insert.push_back(new_target);
}
target = new_target;
}
else {
if (m_changed_leading_term) {
m_to_process.insert(target);
to_remove.push_back(target);
}
}
}
bool nla_grobner::simplify_processed_with_eq(equation* eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
equation_set::iterator it = m_processed.begin();
equation_set::iterator end = m_processed.end();
for (; it != end && !canceled(); ++it) {
equation * target = *it;
m_changed_leading_term = false;
// if the leading term is simplified, then the equation has to be moved to m_to_process
equation * new_target = simplify_source_target(eq, target);
if (new_target != nullptr) {
process_simplified_target(to_insert, new_target, target, to_remove);
}
if (is_trivial(target))
to_delete.push_back(target);
}
for (equation* eq : to_insert)
m_processed.insert(eq);
for (equation* eq : to_remove)
m_processed.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
return !canceled();
}
void nla_grobner::simplify_to_process(equation* eq) {
ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete;
for (equation* target : m_to_process) {
equation * new_target = simplify_source_target(eq, target);
if (new_target != nullptr && new_target != target) {
m_equations_to_unfreeze.push_back(target);
to_insert.push_back(new_target);
to_remove.push_back(target);
target = new_target;
}
if (is_trivial(target))
to_delete.push_back(target);
}
for (equation* eq : to_insert)
m_to_process.insert(eq);
for (equation* eq : to_remove)
m_to_process.erase(eq);
for (equation* eq : to_delete)
del_equation(eq);
}
void nla_grobner::superpose(equation * eq1, equation * eq2) {
SASSERT(false);
NOT_IMPLEMENTED_YET();
}
void nla_grobner::superpose(equation * eq){
SASSERT(false);
void nla_grobner::superpose(equation * eq) {
for (equation * target : m_processed) {
superpose(eq, target);
}
}
@ -287,7 +415,7 @@ bool nla_grobner::compute_basis_step() {
eq = new_eq;
}
if (canceled()) return false;
if (!simplify_processed(eq)) return false;
if (!simplify_processed_with_eq(eq)) return false;
superpose(eq);
m_processed.insert(eq);
simplify_to_process(eq);
@ -474,7 +602,7 @@ nla_grobner::equation * nla_grobner::simplify(equation const * source, equation
return nullptr;
}
std::ostream& nla_grobner::display_equation(std::ostream & out, equation & eq) {
std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) {
out << "m_exp = " << *eq.m_exp << "\n";
out << "dep = "; display_dependency(out, eq.m_dep) << "\n";
return out;

10
src/math/lp/nla_grobner.h
View file

@ -89,6 +89,7 @@ class nla_grobner : common {
ci_value_manager m_val_manager;
ci_dependency_manager m_dep_manager;
nex_lt m_lt;
bool m_changed_leading_term;
public:
nla_grobner(core *core);
void grobner_lemmas();
@ -108,9 +109,12 @@ private:
void compute_basis_init();
bool compute_basis_loop();
bool compute_basis_step();
equation * simplify_source_target(equation const * source, equation * target);
equation* simplify_using_processed(equation*);
equation* simplify_processed(equation*);
equation* simplify_to_process(equation*);
unsigned simplify_loop_on_target_monomials(equation const * source, equation * target, bool & result);
void process_simplified_target(ptr_buffer<equation>& to_insert, equation* new_target, equation*& target, ptr_buffer<equation>& to_remove);
bool simplify_processed_with_eq(equation*);
void simplify_to_process(equation*);
equation* pick_next();
void set_gb_exhausted();
bool canceled() { return false; } // todo, implement
@ -121,7 +125,7 @@ private:
void del_equations(unsigned old_size);
void del_equation(equation * eq);
void display_equations(std::ostream & out, equation_set const & v, char const * header) const;
std::ostream& display_equation(std::ostream & out, equation & eq);
std::ostream& display_equation(std::ostream & out, const equation & eq);
void display_monomial(std::ostream & out, monomial const & m) const;