mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-18 19:14:29 +00:00
Code Activity

Port throttle and soundness fixes from master

Browse source 
- Fix soundness: pop incomplete lemma from m_lemmas on add_lemma failure
- Gracefully handle root atoms in add_lemma
- Throttle check_assignment with failure counter (decrement on success)
- Add arith.nl.nra_check_assignment parameter

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-03-12 14:35:52 -10:00
parent 77d81de03f
commit 6c27140bc9
4 changed files with 62 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/nla_core.cpp
View file

@ -1330,10 +1330,14 @@ lbool core::check(unsigned level) {
return l_false;
}
if (no_effect()) {
if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < 10) {
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
ret = m_nra.check_assignment();
if (ret != l_true)
++m_check_assignment_fail_cnt;
else
--m_check_assignment_fail_cnt;
}
if (no_effect() && should_run_bounded_nlsat())

1
src/math/lp/nla_core.h
View file

@ -63,6 +63,7 @@ class core {
unsigned m_nlsat_delay = 0;
unsigned m_nlsat_delay_bound = 0;
unsigned m_check_assignment_fail_cnt = 0;
bool should_run_bounded_nlsat();
lbool bounded_nlsat();

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

@ -448,48 +448,63 @@ struct solver::imp {
lbool add_lemma(nlsat::literal_vector const &clause) {
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
polynomial::manager &pm = m_nlsat->pm();
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
for (nlsat::literal l : clause) {
if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) {
auto ci = m_literal2constraint[(~l).index()];
lp::explanation ex;
ex.push_back(ci);
lemma &= ex;
continue;
}
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);
if (ia.size() != 1) {
return l_undef; // factored polynomials not handled here
}
polynomial::polynomial const *p = ia.p(0);
rational bound(0);
lp::lar_term t;
process_polynomial_check_assignment(p, bound, nl2lp, t);
lbool result = l_false;
{
nla::lemma_builder lemma(m_nla_core, __FUNCTION__);
for (nlsat::literal l : clause) {
if (m_literal2constraint.get((~l).index(), lp::null_ci) != lp::null_ci) {
auto ci = m_literal2constraint[(~l).index()];
lp::explanation ex;
ex.push_back(ci);
lemma &= ex;
continue;
}
nlsat::atom *a = m_nlsat->bool_var2atom(l.var());
if (a->is_root_atom()) {
result = l_undef;
break;
}
SASSERT(a->is_ineq_atom());
auto &ia = *to_ineq_atom(a);
if (ia.size() != 1) {
result = l_undef; // factored polynomials not handled here
break;
}
polynomial::polynomial const *p = ia.p(0);
rational bound(0);
lp::lar_term t;
process_polynomial_check_assignment(p, bound, nl2lp, t);
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
switch (a->get_kind()) {
case nlsat::atom::EQ:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
break;
case nlsat::atom::LT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
break;
case nlsat::atom::GT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
break;
default:
UNREACHABLE();
return l_undef;
nla::ineq inq(lp::lconstraint_kind::EQ, t, bound); // initial value overwritten in cases below
switch (a->get_kind()) {
case nlsat::atom::EQ:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::NE : lp::lconstraint_kind::EQ, t, bound);
break;
case nlsat::atom::LT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LT, t, bound);
break;
case nlsat::atom::GT:
inq = nla::ineq(l.sign() ? lp::lconstraint_kind::LE : lp::lconstraint_kind::GT, t, bound);
break;
default:
UNREACHABLE();
result = l_undef;
break;
}
if (result == l_undef)
break;
if (m_nla_core.ineq_holds(inq)) {
result = l_undef;
break;
}
lemma |= inq;
}
if (m_nla_core.ineq_holds(inq))
return l_undef;
lemma |= inq;
}
this->m_nla_core.m_check_feasible = true;
return l_false;
if (result == l_false)
this->m_nla_core.m_check_feasible = true;
} // lemma_builder destructor runs here
if (result == l_undef)
m_nla_core.m_lemmas.pop_back(); // discard incomplete lemma
return result;
}

1
src/params/smt_params_helper.pyg
View file

@ -60,6 +60,7 @@ def_module_params(module_name='smt',
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'),
('arith.nl.nra_check_assignment', BOOL, True, 'call check_assignment in nra_solver to verify current assignment against nlsat constraints'),
('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'),
('arith.nl.expensive_patching', BOOL, False, 'use the expensive of monomials'),
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic, relevant only if smt.arith.solver=2'),