diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 9e221e6ea..b4f0cbe70 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -256,6 +256,7 @@ struct solver::imp { lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; nlsat::atom_vector clause; + nlsat::literal_vector cell; polynomial::manager& pm = m_nlsat->pm(); try { nlsat::assignment rvalues(m_nlsat->am()); @@ -264,8 +265,7 @@ struct solver::imp { am().set(a, m_nla_core.val(j).to_mpq()); rvalues.set(x, a); } - r = m_nlsat->check(rvalues, clause); - + r = m_nlsat->check(rvalues, clause, cell); } catch (z3_exception&) { if (m_limit.is_canceled()) { @@ -294,8 +294,11 @@ struct solver::imp { u_map nl2lp; for (auto [j, x] : m_lp2nl) nl2lp.insert(x, j); - for (auto a : clause) { - // a cannot be a root object. + + nla::lemma_builder lemma(m_nla_core, __FUNCTION__); + lemma &= ex; + + auto translate_atom = [&](nlsat::atom* a, bool negated){ SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto& ia = *to_ineq_atom(a); @@ -305,9 +308,6 @@ struct solver::imp { unsigned num_mon = pm.size(p); rational bound(0); lp::lar_term t; - - nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - lemma &= ex; for (unsigned i = 0; i < num_mon; ++i) { polynomial::monomial* m = pm.get_monomial(p, i); auto& coeff = pm.coeff(p, i); @@ -336,7 +336,6 @@ struct solver::imp { v = mon->var(); else { NOT_IMPLEMENTED_YET(); - return l_undef; // this one is for Lev Nachmanson: lar_solver relies on internal variables // to have terms from outside. The solver doesn't get to create // its own monomials. @@ -349,24 +348,29 @@ struct solver::imp { break; } } - } - TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;); + } switch (a->get_kind()) { - case nlsat::atom::EQ: - lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound); - break; - case nlsat::atom::LT: - lemma |= nla::ineq(lp::lconstraint_kind::LT, t, bound); - break; - case nlsat::atom::GT: - lemma |= nla::ineq(lp::lconstraint_kind::GT, t, bound); - break; + case nlsat::atom::EQ: + return nla::ineq(negated ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + case nlsat::atom::LT: + return nla::ineq(negated ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + case nlsat::atom::GT: + return nla::ineq(negated ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); default: UNREACHABLE(); } + }; - IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); + + for (auto a : clause) { + lemma |= translate_atom(a, true); } + + for (nlsat::literal l : cell) { + lemma |= translate_atom( m_nlsat->bool_var2atom(l.var()), l.sign()); + } + + IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n"); m_nla_core.set_use_nra_model(true); break; } diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index c7fa51825..13ad4f41c 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1287,7 +1287,6 @@ namespace nlsat { bool lower_inf = true, upper_inf = true; scoped_anum lower(m_am), upper(m_am); polynomial_ref p_lower(m_pm), p_upper(m_pm); - unsigned i_lower = UINT_MAX, i_upper = UINT_MAX; scoped_anum_vector & roots = m_roots_tmp; polynomial_ref p(m_pm); @@ -1317,7 +1316,6 @@ namespace nlsat { // roots[i] == x_val ps_equal.push_back(p); p_lower = p; - i_lower = i+1; break; // TODO: choose the best among multiple section polynomials? } else if (s < 0) { @@ -1327,7 +1325,6 @@ namespace nlsat { upper_inf = false; m_am.set(upper, roots[i]); p_upper = p; - i_upper = i + 1; } } // in any case, roots[i-1] might provide a lower bound if it exists @@ -1338,7 +1335,6 @@ namespace nlsat { lower_inf = false; m_am.set(lower, roots[i-1]); p_lower = p; - i_lower = i; } } } @@ -1354,7 +1350,7 @@ namespace nlsat { rational bound; m_am.to_rational(x_val, bound); p_lower = m_pm.mk_polynomial(x); - p_lower = p_lower - bound; + p_lower = denominator(bound)*p_lower - numerator(bound); } add_root_literal(atom::ROOT_EQ, x, 1, p_lower); // make sure bounding poly is at the back of the vector @@ -1369,9 +1365,9 @@ namespace nlsat { rational new_bound; m_am.to_rational(between, new_bound); p_lower = m_pm.mk_polynomial(x); - p_lower = p_lower - new_bound; + p_lower = denominator(new_bound)*p_lower - numerator(new_bound); } - add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); + add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_GE : atom::ROOT_GT, x, 1, p_lower); // make sure bounding poly is at the back of the vector ps_below.push_back(p_lower); } @@ -1383,11 +1379,11 @@ namespace nlsat { rational new_bound; m_am.to_rational(between, new_bound); p_upper = m_pm.mk_polynomial(x); - p_upper = p_upper - new_bound; + p_upper = denominator(new_bound)*p_upper - numerator(new_bound); } - add_root_literal((approximate || m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); + add_root_literal((/*approximate ||*/ m_full_dimensional) ? atom::ROOT_LE : atom::ROOT_LT, x, 1, p_upper); // make sure bounding poly is at the back of the vector - ps_below.push_back(p_upper); + ps_above.push_back(p_upper); } } @@ -1424,7 +1420,7 @@ namespace nlsat { polynomial_ref_vector ps_above_sample(m_pm); polynomial_ref_vector ps_equal_sample(m_pm); var x = m_todo.extract_max_polys(ps); - if (x == max_x) { + if (!m_assignment.is_assigned(x)) { // top level projection like original // we could also do a covering-style projection, sparing some resultants add_lcs(ps, x); @@ -1433,7 +1429,7 @@ namespace nlsat { x = m_todo.extract_max_polys(ps); } - while (!m_todo.empty()) { + while (true) { add_cell_lits_linear(ps, x, ps_below_sample, ps_above_sample, ps_equal_sample); if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); @@ -1463,6 +1459,8 @@ namespace nlsat { } } } + if (m_todo.empty()) + break; x = m_todo.extract_max_polys(ps); } } diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0961f4ee0..70a203f70 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2034,7 +2034,7 @@ namespace nlsat { m_assignment.reset(); } - lbool check(assignment const& rvalues, atom_vector& core) { + lbool check(assignment const& rvalues, atom_vector& core, literal_vector& cell) { // temporarily set m_assignment to the given one assignment tmp = m_assignment; m_assignment.reset(); @@ -2042,7 +2042,6 @@ namespace nlsat { // check whether the asserted atoms are satisfied by rvalues literal best_literal = null_literal; - unsigned sz = m_clauses.size(); lbool satisfied = l_true; for (auto cp : m_clauses) { auto& c = *cp; @@ -2077,17 +2076,22 @@ namespace nlsat { // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); + cell.reset(); m_lazy_clause.reset(); m_explain.set_linear_project(true); m_explain.main_operator(1, &best_literal, m_lazy_clause); m_explain.set_linear_project(false); - m_lazy_clause.push_back(~best_literal); - core.clear(); - for (literal l : m_lazy_clause) { - core.push_back(m_atoms[l.var()]); + for (auto l : m_lazy_clause) { + cell.push_back(l); } + m_lemma_assumptions = nullptr; + + core.clear(); + SASSERT(!best_literal.sign()); + core.push_back(m_atoms[best_literal.var()]); + m_assignment.reset(); m_assignment.copy(tmp); return l_false; @@ -4163,8 +4167,8 @@ namespace nlsat { return m_imp->check(assumptions); } - lbool solver::check(assignment const& rvalues, atom_vector& clause) { - return m_imp->check(rvalues, clause); + lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) { + return m_imp->check(rvalues, clause, cell); } void solver::get_core(vector& assumptions) { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index f9f46d494..00138ae9b 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -228,8 +228,9 @@ namespace nlsat { // clause is a list of atoms. Their negations conjoined with core literals are unsatisfiable. // Different implementations of check are possible. One where core comprises of linear polynomials could // produce lemmas that are friendly to linear arithmetic solvers. + // TODO: update // - lbool check(assignment const& rvalues, atom_vector& clause); + lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell); // ----------------------- //