From 14fb08d54c31373ed530b183f19a1c26270c46a9 Mon Sep 17 00:00:00 2001 From: Valentin Promies Date: Wed, 3 Sep 2025 13:44:03 +0200 Subject: [PATCH] clean up --- src/math/lp/nra_solver.cpp | 31 +++++++++++-------------------- src/nlsat/nlsat_solver.cpp | 17 ++++++----------- src/nlsat/nlsat_solver.h | 11 +++++------ 3 files changed, 22 insertions(+), 37 deletions(-) diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index b4f0cbe70..3328547d6 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -255,8 +255,7 @@ struct solver::imp { setup_solver(); lbool r = l_undef; statistics& st = m_nla_core.lp_settings().stats().m_st; - nlsat::atom_vector clause; - nlsat::literal_vector cell; + nlsat::literal_vector clause; polynomial::manager& pm = m_nlsat->pm(); try { nlsat::assignment rvalues(m_nlsat->am()); @@ -265,7 +264,7 @@ struct solver::imp { am().set(a, m_nla_core.val(j).to_mpq()); rvalues.set(x, a); } - r = m_nlsat->check(rvalues, clause, cell); + r = m_nlsat->check(rvalues, clause); } catch (z3_exception&) { if (m_limit.is_canceled()) { @@ -289,16 +288,13 @@ struct solver::imp { validate_constraints(); break; case l_false: { - lp::explanation ex; - constraint_core2ex(ex); u_map nl2lp; for (auto [j, x] : m_lp2nl) nl2lp.insert(x, j); nla::lemma_builder lemma(m_nla_core, __FUNCTION__); - lemma &= ex; - - auto translate_atom = [&](nlsat::atom* a, bool negated){ + for (nlsat::literal l : clause) { + nlsat::atom* a = m_nlsat->bool_var2atom(l.var()); SASSERT(!a->is_root_atom()); SASSERT(a->is_ineq_atom()); auto& ia = *to_ineq_atom(a); @@ -351,23 +347,18 @@ struct solver::imp { } switch (a->get_kind()) { case nlsat::atom::EQ: - return nla::ineq(negated ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound); + break; case nlsat::atom::LT: - return nla::ineq(negated ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound); + break; case nlsat::atom::GT: - return nla::ineq(negated ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + lemma |= nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound); + break; default: UNREACHABLE(); + return l_undef; } - }; - - - 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"); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 70a203f70..aaa3c0857 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, literal_vector& cell) { + lbool check(assignment const& rvalues, literal_vector& clause) { // temporarily set m_assignment to the given one assignment tmp = m_assignment; m_assignment.reset(); @@ -2076,21 +2076,16 @@ namespace nlsat { // assignment does not satisfy the constraints -> create lemma SASSERT(best_literal != null_literal); - cell.reset(); + clause.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); for (auto l : m_lazy_clause) { - cell.push_back(l); + clause.push_back(l); } - - m_lemma_assumptions = nullptr; - - core.clear(); - SASSERT(!best_literal.sign()); - core.push_back(m_atoms[best_literal.var()]); + clause.push_back(~best_literal); m_assignment.reset(); m_assignment.copy(tmp); @@ -4167,8 +4162,8 @@ namespace nlsat { return m_imp->check(assumptions); } - lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) { - return m_imp->check(rvalues, clause, cell); + lbool solver::check(assignment const& rvalues, literal_vector& clause) { + return m_imp->check(rvalues, clause); } void solver::get_core(vector& assumptions) { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 00138ae9b..3d984c8cd 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -222,15 +222,14 @@ namespace nlsat { // check satisfiability of asserted formulas relative to state of the nlsat solver. // produce either, // l_true - a model is available (rvalues can be ignored) or, - // l_false - the conjunction of literals from get_core, and negations of atoms in clause, - // such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. + // l_false - a clause (not core v not cell) excluding a cell around rvalues if core (consisting of atoms + // passed to nlsat) is asserted. // l_undef - if the search was interrupted by a resource limit. - // 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 + // clause is a list of literals. Their disjunction is valid. + // Different implementations of check are possible. One where cell comprises of linear polynomials could // produce lemmas that are friendly to linear arithmetic solvers. - // TODO: update // - lbool check(assignment const& rvalues, atom_vector& clause, literal_vector& cell); + lbool check(assignment const& rvalues, literal_vector& clause); // ----------------------- //