mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-10 11:41:25 +00:00
Code Activity

clean up

Browse source
This commit is contained in:
Valentin Promies 2025-09-03 13:44:03 +02:00
parent 187f013224
commit 14fb08d54c
3 changed files with 22 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/math/lp/nra_solver.cpp
View file

@ -255,8 +255,7 @@ struct solver::imp {
setup_solver(); setup_solver();
lbool r = l_undef; lbool r = l_undef;
statistics& st = m_nla_core.lp_settings().stats().m_st; statistics& st = m_nla_core.lp_settings().stats().m_st;
nlsat::atom_vector clause; nlsat::literal_vector clause;
nlsat::literal_vector cell;
polynomial::manager& pm = m_nlsat->pm(); polynomial::manager& pm = m_nlsat->pm();
try { try {
nlsat::assignment rvalues(m_nlsat->am()); nlsat::assignment rvalues(m_nlsat->am());
@ -265,7 +264,7 @@ struct solver::imp {
am().set(a, m_nla_core.val(j).to_mpq()); am().set(a, m_nla_core.val(j).to_mpq());
rvalues.set(x, a); rvalues.set(x, a);
} }
r = m_nlsat->check(rvalues, clause, cell); r = m_nlsat->check(rvalues, clause);
} }
catch (z3_exception&) { catch (z3_exception&) {
if (m_limit.is_canceled()) { if (m_limit.is_canceled()) {
@ -289,16 +288,13 @@ struct solver::imp {
validate_constraints(); validate_constraints();
break; break;
case l_false: { case l_false: {
lp::explanation ex;
constraint_core2ex(ex);
u_map<lp::lpvar> nl2lp; u_map<lp::lpvar> nl2lp;
for (auto [j, x] : m_lp2nl) for (auto [j, x] : m_lp2nl)
nl2lp.insert(x, j); nl2lp.insert(x, j);
nla::lemma_builder lemma(m_nla_core, __FUNCTION__); nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
lemma &= ex; for (nlsat::literal l : clause) {
nlsat::atom* a = m_nlsat->bool_var2atom(l.var());
auto translate_atom = [&](nlsat::atom* a, bool negated){
SASSERT(!a->is_root_atom()); SASSERT(!a->is_root_atom());
SASSERT(a->is_ineq_atom()); SASSERT(a->is_ineq_atom());
auto& ia = *to_ineq_atom(a); auto& ia = *to_ineq_atom(a);
@ -351,23 +347,18 @@ struct solver::imp {
} }
switch (a->get_kind()) { switch (a->get_kind()) {
case nlsat::atom::EQ: 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: 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: 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: default:
UNREACHABLE(); 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"); IF_VERBOSE(1, verbose_stream() << "linear lemma: " << lemma << "\n");

17
src/nlsat/nlsat_solver.cpp
View file

@ -2034,7 +2034,7 @@ namespace nlsat {
m_assignment.reset(); 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 // temporarily set m_assignment to the given one
assignment tmp = m_assignment; assignment tmp = m_assignment;
m_assignment.reset(); m_assignment.reset();
@ -2076,21 +2076,16 @@ namespace nlsat {
// assignment does not satisfy the constraints -> create lemma // assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal); SASSERT(best_literal != null_literal);
cell.reset(); clause.reset();
m_lazy_clause.reset(); m_lazy_clause.reset();
m_explain.set_linear_project(true); m_explain.set_linear_project(true);
m_explain.main_operator(1, &best_literal, m_lazy_clause); m_explain.main_operator(1, &best_literal, m_lazy_clause);
m_explain.set_linear_project(false); m_explain.set_linear_project(false);
for (auto l : m_lazy_clause) { for (auto l : m_lazy_clause) {
cell.push_back(l); clause.push_back(l);
} }
clause.push_back(~best_literal);
m_lemma_assumptions = nullptr;
core.clear();
SASSERT(!best_literal.sign());
core.push_back(m_atoms[best_literal.var()]);
m_assignment.reset(); m_assignment.reset();
m_assignment.copy(tmp); m_assignment.copy(tmp);
@ -4167,8 +4162,8 @@ namespace nlsat {
return m_imp->check(assumptions); return m_imp->check(assumptions);
} }
lbool solver::check(assignment const& rvalues, atom_vector& clause, literal_vector& cell) { lbool solver::check(assignment const& rvalues, literal_vector& clause) {
return m_imp->check(rvalues, clause, cell); return m_imp->check(rvalues, clause);
} }
void solver::get_core(vector<assumption, false>& assumptions) { void solver::get_core(vector<assumption, false>& assumptions) {

11
src/nlsat/nlsat_solver.h
View file

@ -222,15 +222,14 @@ namespace nlsat {
// check satisfiability of asserted formulas relative to state of the nlsat solver. // check satisfiability of asserted formulas relative to state of the nlsat solver.
// produce either, // produce either,
// l_true - a model is available (rvalues can be ignored) or, // 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, // l_false - a clause (not core v not cell) excluding a cell around rvalues if core (consisting of atoms
// such that the conjunction of the assumptions and the polynomials in core is unsatisfiable. // passed to nlsat) is asserted.
// l_undef - if the search was interrupted by a resource limit. // 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. // clause is a list of literals. Their disjunction is valid.
// Different implementations of check are possible. One where core comprises of linear polynomials could // Different implementations of check are possible. One where cell comprises of linear polynomials could
// produce lemmas that are friendly to linear arithmetic solvers. // 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);
// ----------------------- // -----------------------
// //