From be7856c57ddde2b0aafd2d541a56c60f9d0c08ad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jan 2024 14:56:15 -0800 Subject: [PATCH] fix #7027 TODO: review old nlsat bugs for effect of this fix. --- src/math/polynomial/polynomial.cpp | 2 - src/nlsat/nlsat_evaluator.cpp | 2 +- src/nlsat/nlsat_explain.cpp | 51 +++++++++---- src/nlsat/nlsat_solver.cpp | 115 ++++++++++++++++++++--------- 4 files changed, 117 insertions(+), 53 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index a3af87f52d7..96a4a05cae5 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -1583,9 +1583,7 @@ namespace polynomial { m_i->display_smt2(out, proc); } else { - out << "(* "; m_i->display_smt2(out, proc); - out << ")"; } } else { diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 97e0e3d725e..247b41485aa 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -491,7 +491,7 @@ namespace nlsat { interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { sign_table & table = m_sign_table_tmp; 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(); var x = a->max_var(); for (unsigned i = 0; i < num_ps; i++) { diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 68a646f9228..0b76a14efb1 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -38,7 +38,7 @@ namespace nlsat { polynomial_ref_vector m_ps; polynomial_ref_vector m_ps2; 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; bool m_simplify_cores; bool m_full_dimensional; @@ -142,6 +142,7 @@ namespace nlsat { m_ps2(m_pm), m_psc_tmp(m_pm), m_factors(m_pm), + m_factors_save(m_pm), m_roots_tmp(m_am), m_todo(u), m_core1(s), @@ -259,22 +260,42 @@ namespace nlsat { */ ptr_vector m_zero_fs; 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) { // 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. // I don't want to create a nested conjunction in the clause. // Then, I assert p_i1 * ... * p_im != 0 - factor(p, m_factors); - unsigned num_factors = m_factors.size(); - m_zero_fs.reset(); - m_is_even.reset(); - polynomial_ref f(m_pm); - for (unsigned i = 0; i < num_factors; i++) { - f = m_factors.get(i); - if (is_zero(sign(f))) { - m_zero_fs.push_back(m_factors.get(i)); - m_is_even.push_back(false); - } + { + restore_factors _restore(m_factors, m_factors_save); + factor(p, m_factors); + unsigned num_factors = m_factors.size(); + m_zero_fs.reset(); + m_is_even.reset(); + polynomial_ref f(m_pm); + for (unsigned i = 0; i < num_factors; i++) { + f = m_factors.get(i); + 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. 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)) return; 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); + TRACE("nlsat_explain", display(tout << "adding factors of\n", p); tout << "\n" << m_factors << "\n";); polynomial_ref f(m_pm); for (unsigned i = 0; i < m_factors.size(); 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) { + TRACE("nlsat_explain", display_var(tout, y); m_pm.display(tout << ": ", p, m_solver.display_proc()); tout << "\n"); polynomial_ref p_prime(m_pm); p_prime = p; bool lsign = false; @@ -1379,7 +1402,7 @@ namespace nlsat { var max_x = max_var(m_ps); TRACE("nlsat_explain", tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";); 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); TRACE("nlsat_explain", tout << "after projection\n"; display(tout, m_ps); tout << "\n";); } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 2e482218cc7..050398d0519 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -114,10 +114,10 @@ namespace nlsat { unsigned_vector m_levels; // bool_var -> level svector m_justifications; 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; - 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 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. 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) { TRACE("nlsat", display(tout << "check lemma: ", n, cls) << "\n"; 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"); scoped_suspend_rlimit _limit(m_rlimit); 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) { - if (!is_valid) - display_smt2(out); - out << "(assert (not "; - display_smt2(out, n, cls) << "))\n"; + if (is_valid) { + display_smt2_bool_decls(out); + display_smt2_arith_decls(out); + } + else + display_smt2(out); + display_smt2(out << "(assert (not ", n, cls) << "))\n"; display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n"; out << "(check-sat)\n(reset)\n"; } @@ -1144,7 +1147,7 @@ namespace nlsat { \brief Assign literal using the given justification */ void assign(literal l, justification j) { - TRACE("nlsat", + TRACE("nlsat_assign", display(tout << "assigning literal: ", l); display(tout << " <- ", j);); @@ -1264,7 +1267,9 @@ namespace nlsat { m_ism.get_justifications(s, core, clauses); if (include_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); } @@ -1815,7 +1820,7 @@ namespace nlsat { } 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()); m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); } @@ -3012,8 +3017,14 @@ namespace nlsat { } return out; } + + bool m_display_eval = false; + std::ostream& display_eval(std::ostream& out, justification j) { + flet _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(); for (unsigned i = 0; i < sz; i++) { if (use_star && i > 0) @@ -3021,7 +3032,7 @@ namespace nlsat { bool is_even = a.is_even(i); if (is_even || sz > 1) 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) out << ")"; if (is_even) @@ -3061,7 +3072,7 @@ namespace nlsat { 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()) { case atom::LT: out << "(< "; break; case atom::GT: out << "(> "; break; @@ -3090,15 +3101,29 @@ namespace nlsat { 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 { - polynomial_ref A(m_pm), B(m_pm); - polynomial::scoped_numeral one(m_qm); - m_pm.m().set(one, 1); + polynomial_ref A(m_pm), B(m_pm), Z(m_pm), Ax(m_pm); + polynomial::scoped_numeral zero(m_qm); + m_pm.m().set(zero, 0); 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(); + + Ax = m_pm.mul(m_pm.mk_polynomial(a.x()), A); - // x < root[1](ax + b) == (a > 0 => ax < b) & (a < 0 => ax > b) + // 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 = ">"; switch (a.get_kind()) { @@ -3111,21 +3136,22 @@ namespace nlsat { } out << "(and "; - out << "(=> (> "; m_pm.display_smt2(out, A, proc); out << " 0) "; - out << "(" << rel1 << " (* "; proc(out, a.x()); out << " "; m_pm.display_smt2(out, A, proc); out << " "; m_pm.display_smt2(out, 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 << "(=> "; display_binary_smt2(out, A, ">", Z, proc); display_binary_smt2(out, Ax, rel1, B, proc); out << ") "; + out << "(=> "; display_binary_smt2(out, A, "<", Z, proc); display_binary_smt2(out, Ax, rel2, B, proc); out << ") "; out << ")"; return out; } - std::ostream& display_smt2(std::ostream & out, root_atom const & a, display_var_proc const & proc) const { -#if 0 + std::ostream& display_root_smt2(std::ostream& out, root_atom const& a, display_var_proc const& proc) const { if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1) 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()); switch (a.get_kind()) { case atom::ROOT_LT: out << " < "; break; @@ -3136,7 +3162,7 @@ namespace nlsat { default: UNREACHABLE(); break; } out << "root[" << a.i() << "]("; - m_pm.display(out, a.p(), proc); + display_polynomial(out, a.p(), proc); out << ")"; return out; } @@ -3164,21 +3190,16 @@ namespace nlsat { default: UNREACHABLE(); break; } 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() << "]"; 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 { if (a.is_ineq_atom()) - return display(out, static_cast(a), proc); + return display_ineq(out, static_cast(a), proc); else - return display(out, static_cast(a), proc); + return display_root(out, static_cast(a), proc); } 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 { if (a.is_ineq_atom()) - return display_smt2(out, static_cast(a), proc); + return display_ineq_smt2(out, static_cast(a), proc); else - return display_smt2(out, static_cast(a), proc); + return display_root_smt2(out, static_cast(a), proc); } 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 { return display_smt2(out, n, ls, display_var_proc()); }