mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

add trace statement and a fix change in pick_next() - choosing a smaller monomial

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-07 10:39:24 -10:00
parent 513932bff8
commit 87d7ce69e3
5 changed files with 82 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -163,8 +163,8 @@ void grobner::display_equations(std::ostream & out, equation_set const & v, char
} }
void grobner::display(std::ostream & out) const { void grobner::display(std::ostream & out) const {
display_equations(out, m_to_superpose, "processed:"); display_equations(out, m_to_superpose, "m_to_superpose:");
display_equations(out, m_to_simplify, "to process:"); display_equations(out, m_to_simplify, "m_to_simplify:");
} }
void grobner::set_weight(expr * n, int weight) { void grobner::set_weight(expr * n, int weight) {
@ -751,9 +751,9 @@ bool grobner::simplify_processed_with_eq(equation * eq) {
} }
/** /**
\brief Use the given equation to simplify to-process terms. \brief Use the given equation to simplify m_to_simplify equation.
*/ */
void grobner::simplify_to_process(equation * eq) { void grobner::simplify_m_to_simplify(equation * eq) {
ptr_buffer<equation> to_insert; ptr_buffer<equation> to_insert;
ptr_buffer<equation> to_remove; ptr_buffer<equation> to_remove;
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
@ -832,6 +832,7 @@ void grobner::superpose(equation * eq1, equation * eq2) {
rest1.reset(); rest1.reset();
ptr_vector<expr> & rest2 = m_tmp_vars2; ptr_vector<expr> & rest2 = m_tmp_vars2;
rest2.reset(); rest2.reset();
TRACE("grobner", tout << "trying to superpose:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2););
if (unify(eq1->m_monomials[0], eq2->m_monomials[0], rest1, rest2)) { if (unify(eq1->m_monomials[0], eq2->m_monomials[0], rest1, rest2)) {
TRACE("grobner", tout << "superposing:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2); TRACE("grobner", tout << "superposing:\n"; display_equation(tout, *eq1); display_equation(tout, *eq2);
tout << "rest1: "; display_vars(tout, rest1.size(), rest1.c_ptr()); tout << "\n"; tout << "rest1: "; display_vars(tout, rest1.size(), rest1.c_ptr()); tout << "\n";
@ -853,6 +854,8 @@ void grobner::superpose(equation * eq1, equation * eq2) {
init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep)); init_equation(new_eq, m_dep_manager.mk_join(eq1->m_dep, eq2->m_dep));
new_eq->m_lc = false; new_eq->m_lc = false;
m_to_simplify.insert(new_eq); m_to_simplify.insert(new_eq);
} else {
TRACE("grobner", tout << "unify did not work\n";);
} }
} }
@ -871,6 +874,7 @@ void grobner::compute_basis_init() {
} }
bool grobner::compute_basis_step() { bool grobner::compute_basis_step() {
TRACE("grobner", display(tout););
equation * eq = pick_next(); equation * eq = pick_next();
if (!eq) if (!eq)
return true; return true;
@ -890,10 +894,13 @@ bool grobner::compute_basis_step() {
eq = new_eq; eq = new_eq;
} }
if (m_manager.canceled()) return false; if (m_manager.canceled()) return false;
if (!simplify_processed_with_eq(eq)) return false; if (!simplify_processed_with_eq(eq)) {
TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false;
}
superpose(eq); superpose(eq);
m_to_superpose.insert(eq); m_to_superpose.insert(eq);
simplify_to_process(eq); simplify_m_to_simplify(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout);); TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false; return false;
} }
@ -901,7 +908,10 @@ bool grobner::compute_basis_step() {
bool grobner::compute_basis(unsigned threshold) { bool grobner::compute_basis(unsigned threshold) {
compute_basis_init(); compute_basis_init();
while (m_num_new_equations < threshold && !m_manager.canceled()) { while (m_num_new_equations < threshold && !m_manager.canceled()) {
if (compute_basis_step()) return true; if (compute_basis_step()) {
return true;
}
} }
return false; return false;
} }

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

@ -176,7 +176,7 @@ protected:
bool simplify_processed_with_eq(equation * eq); bool simplify_processed_with_eq(equation * eq);
void simplify_to_process(equation * eq); void simplify_m_to_simplify(equation * eq);
bool unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2); bool unify(monomial const * m1, monomial const * m2, ptr_vector<expr> & rest1, ptr_vector<expr> & rest2);

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

@ -35,7 +35,7 @@ bool nla_grobner::internalize_gb_eq(equation* ) {
} }
void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) { void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
SASSERT(!c().active_var_set_contains(j)); SASSERT(!c().active_var_set_contains(j) && !c().var_is_fixed(j));
TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";); TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";);
const auto& matrix = c().m_lar_solver.A_r(); const auto& matrix = c().m_lar_solver.A_r();
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
@ -45,13 +45,12 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
if (m_rows.contains(row)) continue; if (m_rows.contains(row)) continue;
lpvar basic_in_row = core_slv.m_r_basis[row]; lpvar basic_in_row = core_slv.m_r_basis[row];
if (c().var_is_free(basic_in_row)) { if (c().var_is_free(basic_in_row)) {
TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";); TRACE("grobner", tout << "ignore the row " << row << " with the free basic var\n";);
continue; // mimic the behavior of the legacy solver continue; // mimic the behavior of the legacy solver
} }
m_rows.insert(row); m_rows.insert(row);
for (auto& rc : matrix.m_rows[row]) { for (auto& rc : matrix.m_rows[row]) {
if (c().active_var_set_contains(rc.var())) if (c().active_var_set_contains(rc.var()) || c().var_is_fixed(rc.var()))
continue; continue;
q.push(rc.var()); q.push(rc.var());
} }
@ -64,7 +63,7 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
for (auto fcn : factorization_factory_imp(m, c())) { for (auto fcn : factorization_factory_imp(m, c())) {
for (const factor& fc: fcn) { for (const factor& fc: fcn) {
lpvar j = var(fc); lpvar j = var(fc);
if (! c().active_var_set_contains(j)) if (!c().active_var_set_contains(j) && !c().var_is_fixed(j))
add_var_and_its_factors_to_q_and_collect_new_rows(j, q); add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
} }
} }
@ -75,6 +74,10 @@ void nla_grobner::find_nl_cluster() {
std::queue<lpvar> q; std::queue<lpvar> q;
for (lpvar j : c().m_to_refine) { for (lpvar j : c().m_to_refine) {
TRACE("grobner", c().print_monic(c().emons()[j], tout) << "\n";); TRACE("grobner", c().print_monic(c().emons()[j], tout) << "\n";);
if (c().var_is_fixed(j)) {
TRACE("grobner", tout << "skip fixed var " << j << "\n";);
continue;
}
q.push(j); q.push(j);
} }
@ -110,21 +113,6 @@ std::ostream & nla_grobner::display(std::ostream & out) const {
return out; return out;
} }
void nla_grobner::process_var(nex_mul* m, lpvar j, ci_dependency* & dep, rational & coeff) {
if (c().var_is_fixed(j)) {
if (!m_tmp_var_set.contains(j)) {
m_tmp_var_set.insert(j);
lp::constraint_index lc,uc;
c().m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lc), m_dep_manager.mk_leaf(uc)));
}
coeff *= c().m_lar_solver.column_upper_bound(j).x;
}
else {
m->add_child(m_nex_creator.mk_var(j));
}
}
common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index> & cs) { common::ci_dependency* nla_grobner::dep_from_vector(svector<lp::constraint_index> & cs) {
ci_dependency * d = nullptr; ci_dependency * d = nullptr;
@ -148,7 +136,7 @@ void nla_grobner::add_row(unsigned i) {
assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr); assert_eq_0(e, m_look_for_fixed_vars_in_rows? get_fixed_vars_dep_from_row(row, m_dep_manager) : nullptr);
} }
void nla_grobner::simplify_equations_to_process() { void nla_grobner::simplify_equations_in_m_to_simplify() {
for (equation *eq : m_to_simplify) { for (equation *eq : m_to_simplify) {
eq->exp() = m_nex_creator.simplify(eq->exp()); eq->exp() = m_nex_creator.simplify(eq->exp());
} }
@ -169,7 +157,7 @@ void nla_grobner::init() {
for (unsigned i : m_rows) { for (unsigned i : m_rows) {
add_row(i); add_row(i);
} }
simplify_equations_to_process(); simplify_equations_in_m_to_simplify();
} }
bool nla_grobner::is_trivial(equation* eq) const { bool nla_grobner::is_trivial(equation* eq) const {
@ -184,7 +172,7 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
return true; return true;
if (is_trivial(eq2)) if (is_trivial(eq2))
return false; return false;
return m_nex_creator.lt(eq1->exp(), eq2->exp()); return m_nex_creator.lt(eq2->exp(), eq1->exp());
} }
void nla_grobner::del_equation(equation * eq) { void nla_grobner::del_equation(equation * eq) {
@ -201,8 +189,10 @@ nla_grobner::equation* nla_grobner::pick_next() {
for (equation * curr : m_to_simplify) { for (equation * curr : m_to_simplify) {
if (is_trivial(curr)) if (is_trivial(curr))
to_delete.push_back(curr); to_delete.push_back(curr);
else if (is_better_choice(curr, r)) else if (is_better_choice(curr, r)) {
TRACE("grobner", tout << "preferring "; display_equation(tout, *curr););
r = curr; r = curr;
}
} }
for (equation * e : to_delete) for (equation * e : to_delete)
del_equation(e); del_equation(e);
@ -212,7 +202,7 @@ nla_grobner::equation* nla_grobner::pick_next() {
return r; return r;
} }
nla_grobner::equation* nla_grobner::simplify_using_processed(equation* eq) { nla_grobner::equation* nla_grobner::simplify_using_to_superpose(equation* eq) {
bool result = false; bool result = false;
bool simplified; bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); TRACE("grobner", tout << "simplifying: "; display_equation(tout, *eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
@ -504,7 +494,10 @@ bool nla_grobner::simplify_to_superpose_with_eq(equation* eq) {
return !canceled(); return !canceled();
} }
void nla_grobner::simplify_to_superpose(equation* eq) { /*
Use the given equation to simplify m_to_simplify equations
*/
void nla_grobner::simplify_m_to_simplify(equation* eq) {
TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";); TRACE("grobner_d", tout << "eq->exp " << *(eq->exp()) << "\n";);
ptr_buffer<equation> to_delete; ptr_buffer<equation> to_delete;
for (equation* target : m_to_simplify) { for (equation* target : m_to_simplify) {
@ -557,6 +550,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
TRACE("grobner", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; }; TRACE("grobner", tout << "ab="; if(ab) { tout << *ab; } else { tout << "null"; };
tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";); tout << " , " << " ac="; if(ac) { tout << *ac; } else { tout << "null"; }; tout << "\n";);
if (!find_b_c(ab, ac, b, c)) { if (!find_b_c(ab, ac, b, c)) {
TRACE("grobner", tout << "there is no non-trivial common divider, no superposing\n";);
return; return;
} }
equation* eq = alloc(equation); equation* eq = alloc(equation);
@ -658,27 +652,33 @@ bool nla_grobner::compute_basis_step() {
return true; return true;
} }
m_stats.m_num_processed++; m_stats.m_num_processed++;
equation * new_eq = simplify_using_processed(eq); equation * new_eq = simplify_using_to_superpose(eq);
if (new_eq != nullptr && eq != new_eq) { if (new_eq != nullptr && eq != new_eq) {
// equation was updated using non destructive updates // equation was updated using non destructive updates
eq = new_eq; eq = new_eq;
} }
if (canceled()) return false; if (canceled()) return false;
if (!simplify_to_superpose_with_eq(eq)) return false; if (!simplify_to_superpose_with_eq(eq))
return false;
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
superpose(eq); superpose(eq);
insert_to_superpose(eq); insert_to_superpose(eq);
simplify_to_superpose(eq); simplify_m_to_simplify(eq);
TRACE("grobner", tout << "end of iteration:\n"; display(tout);); TRACE("grobner", tout << "end of iteration:\n"; display(tout););
return false; return false;
} }
void nla_grobner::compute_basis(){ void nla_grobner::compute_basis(){
compute_basis_init(); compute_basis_init();
if (m_rows.size() < 2) {
TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";);
return;
}
if (!compute_basis_loop()) { if (!compute_basis_loop()) {
TRACE("grobner", tout << "false from compute_basis_loop\n";);
set_gb_exhausted(); set_gb_exhausted();
} else { } else {
TRACE("grobner", tout << "m_to_simplify.size() = " << m_to_simplify.size() << " , m_to_superpose.size() == " << m_to_superpose.size() << "\n";); TRACE("grobner", display(tout););
for (equation* e : m_to_simplify) { for (equation* e : m_to_simplify) {
check_eq(e); check_eq(e);
} }
@ -707,7 +707,18 @@ bool nla_grobner::done() const {
m_reported > 100000 m_reported > 100000
|| ||
m_conflict) { m_conflict) {
TRACE("grobner", tout << "done()\n";); TRACE("grobner",
tout << "done() is true because of ";
if (m_num_of_equations >= c().m_nla_settings.grobner_eqs_threshold()) {
tout << "m_num_of_equations = " << m_num_of_equations << "\n";
} else if (canceled()) {
tout << "canceled\n";
} else if (m_reported > 100000) {
tout << "m_reported = " << m_reported;
} else {
tout << "m_conflict = " << m_conflict;
}
tout << "\n";);
return true; return true;
} }
return false; return false;
@ -720,9 +731,7 @@ bool nla_grobner::compute_basis_loop(){
TRACE("grobner", tout << "progress in compute_basis_step\n";); TRACE("grobner", tout << "progress in compute_basis_step\n";);
return true; return true;
} }
TRACE("grobner", tout << "continue compute_basis_loop i= " << i << "\n";); TRACE("grobner", tout << "continue compute_basis_loop i= " << ++i << "\n";);
if (++i > 50)
exit(0);
} }
TRACE("grobner", tout << "return false from compute_basis_loop i= " << i << "\n";); TRACE("grobner", tout << "return false from compute_basis_loop i= " << i << "\n";);
return false; return false;
@ -792,7 +801,7 @@ void nla_grobner::display_equations(std::ostream & out, equation_set const & v,
std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const { std::ostream& nla_grobner::display_equation(std::ostream & out, const equation & eq) const {
out << "expr = " << *eq.exp() << "\n"; out << "expr = " << *eq.exp() << "\n";
out << "deps = "; display_dependency(out, eq.dep()) << "\n"; display_dependency(out, eq.dep());
return out; return out;
} }
std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const nex *e ) { std::unordered_set<lpvar> nla_grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
@ -852,10 +861,10 @@ std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency*
if (!expl.empty()) { if (!expl.empty()) {
out << "constraints\n"; out << "constraints\n";
m_core->print_explanation(e, out); m_core->print_explanation(e, out);
}else { out << "\n";
out << "no constraints\n";
} }
} }
return out; return out;
} }

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

@ -113,11 +113,11 @@ private:
bool compute_basis_loop(); bool compute_basis_loop();
bool compute_basis_step(); bool compute_basis_step();
bool simplify_source_target(equation * source, equation * target); bool simplify_source_target(equation * source, equation * target);
equation* simplify_using_processed(equation*); equation* simplify_using_to_superpose(equation*);
bool simplify_target_monomials(equation * source, equation * target); bool simplify_target_monomials(equation * source, equation * target);
void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove); void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove);
bool simplify_to_superpose_with_eq(equation*); bool simplify_to_superpose_with_eq(equation*);
void simplify_to_superpose(equation*); void simplify_m_to_simplify(equation*);
equation* pick_next(); equation* pick_next();
void set_gb_exhausted(); void set_gb_exhausted();
bool canceled() const; bool canceled() const;
@ -139,8 +139,6 @@ private:
bool internalize_gb_eq(equation*); bool internalize_gb_eq(equation*);
void add_row(unsigned); void add_row(unsigned);
void assert_eq_0(nex*, ci_dependency * dep); void assert_eq_0(nex*, ci_dependency * dep);
void process_var(nex_mul*, lpvar j, ci_dependency *& dep, rational&);
void init_equation(equation* eq, nex*, ci_dependency* d); void init_equation(equation* eq, nex*, ci_dependency* d);
std::ostream& display_dependency(std::ostream& out, ci_dependency*) const; std::ostream& display_dependency(std::ostream& out, ci_dependency*) const;
@ -150,9 +148,10 @@ private:
} }
void insert_to_superpose(equation *eq) { void insert_to_superpose(equation *eq) {
SASSERT(m_nex_creator.is_simplified(eq->exp())); SASSERT(m_nex_creator.is_simplified(eq->exp()));
TRACE("nla_grobner", display_equation(tout, *eq););
m_to_superpose.insert(eq); m_to_superpose.insert(eq);
} }
void simplify_equations_to_process(); void simplify_equations_in_m_to_simplify();
const nex * get_highest_monomial(const nex * e) const; const nex * get_highest_monomial(const nex * e) const;
ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints); ci_dependency* dep_from_vector( svector<lp::constraint_index> & fixed_vars_constraints);
bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*); bool simplify_target_monomials_sum(equation *, equation *, nex_sum*, const nex*);

10
src/smt/theory_arith_nl.h
View file

@ -101,6 +101,9 @@ void theory_arith<Ext>::mark_dependents(theory_var v, svector<theory_var> & vars
for (; it2 != end2; ++it2) { for (; it2 != end2; ++it2) {
if (!it2->is_dead() && !is_fixed(it2->m_var)) if (!it2->is_dead() && !is_fixed(it2->m_var))
mark_var(it2->m_var, vars, already_found); mark_var(it2->m_var, vars, already_found);
if (!it2->is_dead() && is_fixed(it2->m_var)) {
TRACE("non_linear", tout << "skipped fixed\n";);
}
} }
} }
} }
@ -2242,14 +2245,19 @@ void theory_arith<Ext>::set_gb_exhausted() {
// Scan the grobner basis eqs, and look for inconsistencies. // Scan the grobner basis eqs, and look for inconsistencies.
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& eqs, grobner& gb) { bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& eqs, grobner& gb) {
TRACE("grobner", );
eqs.reset(); eqs.reset();
gb.get_equations(eqs); gb.get_equations(eqs);
TRACE("grobner_bug", tout << "after gb\n";); TRACE("grobner_bug", tout << "after gb\n";);
for (grobner::equation* eq : eqs) { for (grobner::equation* eq : eqs) {
TRACE("grobner_bug", gb.display_equation(tout, *eq);); TRACE("grobner_bug", gb.display_equation(tout, *eq););
if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) {
TRACE("grobner", tout << "inconsistent: "; gb.display_equation(tout, *eq););
return true; return true;
}
} }
TRACE("grobner", tout << "not found\n"; );
return false; return false;
} }