mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #7027

Browse source 
TODO: review old nlsat bugs for effect of this fix.
This commit is contained in:
Nikolaj Bjorner 2024-01-23 14:56:15 -08:00
parent 125a82bea5
commit be7856c57d
4 changed files with 117 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polynomial/polynomial.cpp
View file

@ -1583,9 +1583,7 @@ namespace polynomial {
m_i->display_smt2(out, proc); m_i->display_smt2(out, proc);
} }
else { else {
out << "(* ";
m_i->display_smt2(out, proc); m_i->display_smt2(out, proc);
out << ")";
} }
} }
else { else {

2
src/nlsat/nlsat_evaluator.cpp
View file

@ -491,7 +491,7 @@ namespace nlsat {
interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) {
sign_table & table = m_sign_table_tmp; sign_table & table = m_sign_table_tmp;
table.reset(); table.reset();
TRACE("nsat_evaluator", m_solver.display(tout, *a) << "\n";); TRACE("nlsat_evaluator", m_solver.display(tout, *a) << "\n";);
unsigned num_ps = a->size(); unsigned num_ps = a->size();
var x = a->max_var(); var x = a->max_var();
for (unsigned i = 0; i < num_ps; i++) { for (unsigned i = 0; i < num_ps; i++) {

51
src/nlsat/nlsat_explain.cpp
View file

@ -38,7 +38,7 @@ namespace nlsat {
polynomial_ref_vector m_ps; polynomial_ref_vector m_ps;
polynomial_ref_vector m_ps2; polynomial_ref_vector m_ps2;
polynomial_ref_vector m_psc_tmp; polynomial_ref_vector m_psc_tmp;
polynomial_ref_vector m_factors; polynomial_ref_vector m_factors, m_factors_save;
scoped_anum_vector m_roots_tmp; scoped_anum_vector m_roots_tmp;
bool m_simplify_cores; bool m_simplify_cores;
bool m_full_dimensional; bool m_full_dimensional;
@ -142,6 +142,7 @@ namespace nlsat {
m_ps2(m_pm), m_ps2(m_pm),
m_psc_tmp(m_pm), m_psc_tmp(m_pm),
m_factors(m_pm), m_factors(m_pm),
m_factors_save(m_pm),
m_roots_tmp(m_am), m_roots_tmp(m_am),
m_todo(u), m_todo(u),
m_core1(s), m_core1(s),
@ -259,22 +260,42 @@ namespace nlsat {
*/ */
ptr_vector<poly> m_zero_fs; ptr_vector<poly> m_zero_fs;
bool_vector m_is_even; bool_vector m_is_even;
struct restore_factors {
polynomial_ref_vector& m_factors, &m_factors_save;
unsigned num_saved = 0;
restore_factors(polynomial_ref_vector&f, polynomial_ref_vector& fs):
m_factors(f), m_factors_save(fs)
{
num_saved = m_factors_save.size();
m_factors_save.append(m_factors);
}
~restore_factors() {
m_factors.reset();
m_factors.append(m_factors_save.size() - num_saved, m_factors_save.data() + num_saved);
m_factors_save.shrink(num_saved);
}
};
void add_zero_assumption(polynomial_ref & p) { void add_zero_assumption(polynomial_ref & p) {
// If p is of the form p1^n1 * ... * pk^nk, // If p is of the form p1^n1 * ... * pk^nk,
// then only the factors that are zero in the current interpretation needed to be considered. // then only the factors that are zero in the current interpretation needed to be considered.
// I don't want to create a nested conjunction in the clause. // I don't want to create a nested conjunction in the clause.
// Then, I assert p_i1 * ... * p_im != 0 // Then, I assert p_i1 * ... * p_im != 0
factor(p, m_factors); {
unsigned num_factors = m_factors.size(); restore_factors _restore(m_factors, m_factors_save);
m_zero_fs.reset(); factor(p, m_factors);
m_is_even.reset(); unsigned num_factors = m_factors.size();
polynomial_ref f(m_pm); m_zero_fs.reset();
for (unsigned i = 0; i < num_factors; i++) { m_is_even.reset();
f = m_factors.get(i); polynomial_ref f(m_pm);
if (is_zero(sign(f))) { for (unsigned i = 0; i < num_factors; i++) {
m_zero_fs.push_back(m_factors.get(i)); f = m_factors.get(i);
m_is_even.push_back(false); if (is_zero(sign(f))) {
} m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false);
}
}
} }
SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it. SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data()); literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
@ -582,8 +603,9 @@ namespace nlsat {
if (is_const(p)) if (is_const(p))
return; return;
if (m_factor) { if (m_factor) {
TRACE("nlsat_explain", display(tout << "adding factors of\n", p); tout << "\n";); restore_factors _restore(m_factors, m_factors_save);
factor(p, m_factors); factor(p, m_factors);
TRACE("nlsat_explain", display(tout << "adding factors of\n", p); tout << "\n" << m_factors << "\n";);
polynomial_ref f(m_pm); polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); i++) { for (unsigned i = 0; i < m_factors.size(); i++) {
f = m_factors.get(i); f = m_factors.get(i);
@ -859,6 +881,7 @@ namespace nlsat {
*/ */
void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) { void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) {
TRACE("nlsat_explain", display_var(tout, y); m_pm.display(tout << ": ", p, m_solver.display_proc()); tout << "\n");
polynomial_ref p_prime(m_pm); polynomial_ref p_prime(m_pm);
p_prime = p; p_prime = p;
bool lsign = false; bool lsign = false;
@ -1379,7 +1402,7 @@ namespace nlsat {
var max_x = max_var(m_ps); var max_x = max_var(m_ps);
TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";); TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
elim_vanishing(m_ps); elim_vanishing(m_ps);
TRACE("nlsat_explain", tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";); TRACE("nlsat_explain", tout << "elim vanishing x" << max_x << "\n"; display(tout, m_ps); tout << "\n";);
project(m_ps, max_x); project(m_ps, max_x);
TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";); TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
} }

115
src/nlsat/nlsat_solver.cpp
View file

@ -114,10 +114,10 @@ namespace nlsat {
unsigned_vector m_levels; // bool_var -> level unsigned_vector m_levels; // bool_var -> level
svector<justification> m_justifications; svector<justification> m_justifications;
vector<clause_vector> m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal vector<clause_vector> m_bwatches; // bool_var (that are not attached to atoms) -> clauses where it is maximal
bool_vector m_dead; // mark dead boolean variables bool_vector m_dead; // mark dead boolean variables
id_gen m_bid_gen; id_gen m_bid_gen;
bool_vector m_is_int; // m_is_int[x] is true if variable is integer bool_vector m_is_int; // m_is_int[x] is true if variable is integer
vector<clause_vector> m_watches; // var -> clauses where variable is maximal vector<clause_vector> m_watches; // var -> clauses where variable is maximal
interval_set_vector m_infeasible; // var -> to a set of interval where the variable cannot be assigned to. interval_set_vector m_infeasible; // var -> to a set of interval where the variable cannot be assigned to.
atom_vector m_var2eq; // var -> to asserted equality atom_vector m_var2eq; // var -> to asserted equality
@ -810,7 +810,7 @@ namespace nlsat {
void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) { void check_lemma(unsigned n, literal const* cls, bool is_valid, assumption_set a) {
TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n"; TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n";
display(tout);); display(tout););
IF_VERBOSE(0, display(verbose_stream() << "check lemma " << (is_valid?"valid: ":"consequence: "), n, cls) << "\n"); IF_VERBOSE(2, display(verbose_stream() << "check lemma " << (is_valid?"valid: ":"consequence: "), n, cls) << "\n");
for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n"); for (clause* c : m_learned) IF_VERBOSE(1, display(verbose_stream() << "lemma: ", *c) << "\n");
scoped_suspend_rlimit _limit(m_rlimit); scoped_suspend_rlimit _limit(m_rlimit);
ctx c(m_rlimit, m_ctx.m_params, m_ctx.m_incremental); ctx c(m_rlimit, m_ctx.m_params, m_ctx.m_incremental);
@ -916,10 +916,13 @@ namespace nlsat {
} }
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) { void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
if (!is_valid) if (is_valid) {
display_smt2(out); display_smt2_bool_decls(out);
out << "(assert (not "; display_smt2_arith_decls(out);
display_smt2(out, n, cls) << "))\n"; }
else
display_smt2(out);
display_smt2(out << "(assert (not ", n, cls) << "))\n";
display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n"; display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
out << "(check-sat)\n(reset)\n"; out << "(check-sat)\n(reset)\n";
} }
@ -1144,7 +1147,7 @@ namespace nlsat {
\brief Assign literal using the given justification \brief Assign literal using the given justification
*/ */
void assign(literal l, justification j) { void assign(literal l, justification j) {
TRACE("nlsat", TRACE("nlsat_assign",
display(tout << "assigning literal: ", l); display(tout << "assigning literal: ", l);
display(tout << " <- ", j);); display(tout << " <- ", j););
@ -1264,7 +1267,9 @@ namespace nlsat {
m_ism.get_justifications(s, core, clauses); m_ism.get_justifications(s, core, clauses);
if (include_l) if (include_l)
core.push_back(~l); core.push_back(~l);
assign(l, mk_lazy_jst(m_allocator, core.size(), core.data(), clauses.size(), clauses.data())); auto j = mk_lazy_jst(m_allocator, core.size(), core.data(), clauses.size(), clauses.data());
TRACE("nlsat_resolve", display(tout, j); display_eval(tout, j));
assign(l, j);
SASSERT(value(l) == l_true); SASSERT(value(l) == l_true);
} }
@ -1815,7 +1820,7 @@ namespace nlsat {
} }
void resolve_clause(bool_var b, clause const & c) { void resolve_clause(bool_var b, clause const & c) {
TRACE("nlsat_resolve", tout << "resolving clause for b: " << b << "\n"; display(tout, c) << "\n";); TRACE("nlsat_resolve", tout << "resolving clause "; if (b != null_bool_var) tout << "for b: " << b << "\n"; display(tout, c) << "\n";);
resolve_clause(b, c.size(), c.data()); resolve_clause(b, c.size(), c.data());
m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions);
} }
@ -3012,8 +3017,14 @@ namespace nlsat {
} }
return out; return out;
} }
bool m_display_eval = false;
std::ostream& display_eval(std::ostream& out, justification j) {
flet<bool> _display(m_display_eval, true);
return display(out, j);
}
std::ostream& display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const { std::ostream& display_ineq(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const {
unsigned sz = a.size(); unsigned sz = a.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (use_star && i > 0) if (use_star && i > 0)
@ -3021,7 +3032,7 @@ namespace nlsat {
bool is_even = a.is_even(i); bool is_even = a.is_even(i);
if (is_even || sz > 1) if (is_even || sz > 1)
out << "("; out << "(";
m_pm.display(out, a.p(i), proc, use_star); display_polynomial(out, a.p(i), proc, use_star);
if (is_even || sz > 1) if (is_even || sz > 1)
out << ")"; out << ")";
if (is_even) if (is_even)
@ -3061,7 +3072,7 @@ namespace nlsat {
return out; return out;
} }
std::ostream& display_smt2(std::ostream & out, ineq_atom const & a, display_var_proc const & proc) const { std::ostream& display_ineq_smt2(std::ostream & out, ineq_atom const & a, display_var_proc const & proc) const {
switch (a.get_kind()) { switch (a.get_kind()) {
case atom::LT: out << "(< "; break; case atom::LT: out << "(< "; break;
case atom::GT: out << "(> "; break; case atom::GT: out << "(> "; break;
@ -3090,15 +3101,29 @@ namespace nlsat {
return out; return out;
} }
std::ostream& display_binary_smt2(std::ostream& out, poly const* p1, char const* rel, poly const* p2, display_var_proc const& proc) const {
out << "(" << rel << " ";
m_pm.display_smt2(out, p1, proc);
out << " ";
m_pm.display_smt2(out, p2, proc);
out << ")";
return out;
}
std::ostream& display_linear_root_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { std::ostream& display_linear_root_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const {
polynomial_ref A(m_pm), B(m_pm); polynomial_ref A(m_pm), B(m_pm), Z(m_pm), Ax(m_pm);
polynomial::scoped_numeral one(m_qm); polynomial::scoped_numeral zero(m_qm);
m_pm.m().set(one, 1); m_pm.m().set(zero, 0);
A = m_pm.derivative(a.p(), a.x()); A = m_pm.derivative(a.p(), a.x());
B = m_pm.substitute(a.p(), a.x(), one); B = m_pm.neg(m_pm.substitute(a.p(), a.x(), zero));
Z = m_pm.mk_zero();
// x < root[1](ax + b) == (a > 0 => ax < b) & (a < 0 => ax > b) Ax = m_pm.mul(m_pm.mk_polynomial(a.x()), A);
// x < root[1](ax + b) == (a > 0 => ax + b < 0) & (a < 0 => ax + b > 0)
// x < root[1](ax + b) == (a > 0 => ax < -b) & (a < 0 => ax > -b)
char const* rel1 = "<", *rel2 = ">"; char const* rel1 = "<", *rel2 = ">";
switch (a.get_kind()) { switch (a.get_kind()) {
@ -3111,21 +3136,22 @@ namespace nlsat {
} }
out << "(and "; out << "(and ";
out << "(=> (> "; m_pm.display_smt2(out, A, proc); out << " 0) "; out << "(=> "; display_binary_smt2(out, A, ">", Z, proc); display_binary_smt2(out, Ax, rel1, B, proc); out << ") ";
out << "(" << rel1 << " (* "; proc(out, a.x()); out << " "; m_pm.display_smt2(out, A, proc); out << " "; m_pm.display_smt2(out, B, proc); out << ")) "; out << "(=> "; display_binary_smt2(out, A, "<", Z, proc); display_binary_smt2(out, Ax, rel2, B, proc); out << ") ";
out << "(=> (< "; m_pm.display_smt2(out, A, proc); out << " 0) ";
out << "(" << rel2 << " (* "; proc(out, a.x()); out << " "; m_pm.display_smt2(out, A, proc); out << " "; m_pm.display_smt2(out, B, proc); out << ")) ";
out << ")"; out << ")";
return out; return out;
} }
std::ostream& display_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { std::ostream& display_root_smt2(std::ostream& out, root_atom const& a, display_var_proc const& proc) const {
#if 0
if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1) if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1)
return display_linear_root_smt2(out, a, proc); return display_linear_root_smt2(out, a, proc);
#endif else
return display_root(out, a, proc);
}
std::ostream& display_root(std::ostream & out, root_atom const & a, display_var_proc const & proc) const {
proc(out, a.x()); proc(out, a.x());
switch (a.get_kind()) { switch (a.get_kind()) {
case atom::ROOT_LT: out << " < "; break; case atom::ROOT_LT: out << " < "; break;
@ -3136,7 +3162,7 @@ namespace nlsat {
default: UNREACHABLE(); break; default: UNREACHABLE(); break;
} }
out << "root[" << a.i() << "]("; out << "root[" << a.i() << "](";
m_pm.display(out, a.p(), proc); display_polynomial(out, a.p(), proc);
out << ")"; out << ")";
return out; return out;
} }
@ -3164,21 +3190,16 @@ namespace nlsat {
default: UNREACHABLE(); break; default: UNREACHABLE(); break;
} }
out << "Root["; out << "Root[";
m_pm.display(out, a.p(), mathematica_var_proc(a.x()), true); display_polynomial(out, a.p(), mathematica_var_proc(a.x()), true);
out << " &, " << a.i() << "]"; out << " &, " << a.i() << "]";
return out; return out;
} }
std::ostream& display_smt2(std::ostream & out, root_atom const & a) const {
NOT_IMPLEMENTED_YET();
return out;
}
std::ostream& display(std::ostream & out, atom const & a, display_var_proc const & proc) const { std::ostream& display(std::ostream & out, atom const & a, display_var_proc const & proc) const {
if (a.is_ineq_atom()) if (a.is_ineq_atom())
return display(out, static_cast<ineq_atom const &>(a), proc); return display_ineq(out, static_cast<ineq_atom const &>(a), proc);
else else
return display(out, static_cast<root_atom const &>(a), proc); return display_root(out, static_cast<root_atom const &>(a), proc);
} }
std::ostream& display(std::ostream & out, atom const & a) const { std::ostream& display(std::ostream & out, atom const & a) const {
@ -3194,9 +3215,9 @@ namespace nlsat {
std::ostream& display_smt2(std::ostream & out, atom const & a, display_var_proc const & proc) const { std::ostream& display_smt2(std::ostream & out, atom const & a, display_var_proc const & proc) const {
if (a.is_ineq_atom()) if (a.is_ineq_atom())
return display_smt2(out, static_cast<ineq_atom const &>(a), proc); return display_ineq_smt2(out, static_cast<ineq_atom const &>(a), proc);
else else
return display_smt2(out, static_cast<root_atom const &>(a), proc); return display_root_smt2(out, static_cast<root_atom const &>(a), proc);
} }
std::ostream& display_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const { std::ostream& display_atom(std::ostream & out, bool_var b, display_var_proc const & proc) const {
@ -3340,6 +3361,28 @@ namespace nlsat {
} }
std::ostream& display_polynomial(std::ostream& out, poly* p, display_var_proc const & proc, bool use_star = false) const {
if (m_display_eval) {
polynomial_ref q(m_pm);
q = p;
for (var x = 0; x < num_vars(); x++)
if (m_assignment.is_assigned(x)) {
auto& a = m_assignment.value(x);
if (!m_am.is_rational(a))
continue;
mpq r;
m_am.to_rational(a, r);
q = m_pm.substitute(q, 1, &x, &r);
}
m_pm.display(out, q, proc, use_star);
}
else
m_pm.display(out, p, proc, use_star);
return out;
}
// --
std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const { std::ostream& display_smt2(std::ostream & out, unsigned n, literal const* ls) const {
return display_smt2(out, n, ls, display_var_proc()); return display_smt2(out, n, ls, display_var_proc());
} }