mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-26 05:43:33 +00:00
Code Activity

Merge branch 'nl2lin'

Browse source
This commit is contained in:
Lev Nachmanson 2026-03-14 09:26:20 -10:00
commit 9026f6c952
16 changed files with 490 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

77
src/nlsat/levelwise.cpp
View file

@ -75,6 +75,8 @@ namespace nlsat {
mutable std_vector<unsigned> m_deg_in_order_graph; // degree of polynomial in resultant graph
mutable std_vector<unsigned> m_unique_neighbor; // UINT_MAX = not set, UINT_MAX-1 = multiple
bool m_linear_cell = false; // indicates whether cell bounds are forced to be linear
assignment const& sample() const { return m_solver.sample(); }
struct root_function {
@ -231,7 +233,8 @@ namespace nlsat {
assignment const&,
pmanager& pm,
anum_manager& am,
polynomial::cache& cache)
polynomial::cache& cache,
bool linear)
: m_solver(solver),
m_P(ps),
m_n(max_x),
@ -240,7 +243,8 @@ namespace nlsat {
m_cache(cache),
m_todo(m_cache, true),
m_level_ps(m_pm),
m_psc_tmp(m_pm) {
m_psc_tmp(m_pm),
m_linear_cell(linear) {
m_I.reserve(m_n);
for (unsigned i = 0; i < m_n; ++i)
m_I.emplace_back(m_pm);
@ -1007,6 +1011,66 @@ namespace nlsat {
}
}
void add_linear_poly_from_root(anum const& a, bool lower, polynomial_ref& p) {
rational r;
m_am.to_rational(a, r);
p = m_pm.mk_polynomial(m_level);
p = denominator(r)*p - numerator(r);
if (lower) {
m_I[m_level].l = p;
m_I[m_level].l_index = 1;
} else {
m_I[m_level].u = p;
m_I[m_level].u_index = 1;
}
m_level_ps.push_back(p);
m_poly_has_roots.push_back(true);
polynomial_ref w = choose_nonzero_coeff(p, m_level);
m_witnesses.push_back(w);
}
// Ensure that the interval bounds will be described by linear polynomials.
// If this is not already the case, the working set of polynomials is extended by
// new linear polynomials whose roots under-approximate the cell boundary.
// Based on: Valentin Promies, Jasper Nalbach, Erika Abraham and Paul Wagner
// "More is Less: Adding Polynomials for Faster Explanations in NLSAT" (CADE30, 2025)
void add_linear_approximations(anum const& v) {
polynomial_ref p_lower(m_pm), p_upper(m_pm);
auto& r = m_rel.m_rfunc;
if (m_I[m_level].is_section()) {
if (!m_am.is_rational(v)) {
NOT_IMPLEMENTED_YET();
}
else if (m_pm.total_degree(m_I[m_level].l) > 1) {
add_linear_poly_from_root(v, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf), m_am, p_lower, 1, v, m_level_ps.size()-1);
}
return;
}
// sector: have to consider lower and upper bound
if (!m_I[m_level].l_inf() && m_pm.total_degree(m_I[m_level].l) > 1) {
scoped_anum between(m_am);
m_am.select(r[m_l_rf].val, v, between);
add_linear_poly_from_root(between, true, p_lower);
// update root function ordering
r.emplace((r.begin() + m_l_rf + 1), m_am, p_lower, 1, between, m_level_ps.size()-1);
++m_l_rf;
if (is_set(m_u_rf))
++m_u_rf;
}
if (!m_I[m_level].u_inf() && m_pm.total_degree(m_I[m_level].u) > 1) {
scoped_anum between(m_am);
m_am.select(v, r[m_u_rf].val, between);
// update root function ordering
add_linear_poly_from_root(between, false, p_upper);
r.emplace((r.begin() + m_u_rf), m_am, p_upper, 1, between, m_level_ps.size()-1);
}
}
// Build Θ (root functions) and pick I_level around sample(level).
// Sets m_l_rf/m_u_rf and m_I[level].
// Returns whether any roots were found (i.e., whether a relation can be built).
@ -1022,6 +1086,10 @@ namespace nlsat {
return false;
set_interval_from_root_partition(v, mid);
if (m_linear_cell)
add_linear_approximations(v);
compute_side_mask();
return true;
}
@ -1376,8 +1444,9 @@ namespace nlsat {
assignment const& s,
pmanager& pm,
anum_manager& am,
polynomial::cache& cache)
: m_impl(new impl(solver, ps, n, s, pm, am, cache)) {}
polynomial::cache& cache,
bool linear)
: m_impl(new impl(solver, ps, n, s, pm, am, cache, linear)) {}
levelwise::~levelwise() { delete m_impl; }

2
src/nlsat/levelwise.h
View file

@ -40,7 +40,7 @@ namespace nlsat {
impl* m_impl;
public:
// Construct with polynomials ps, maximal variable max_x, current sample s, polynomial manager pm, and algebraic-number manager am
levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache);
levelwise(nlsat::solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am, polynomial::cache & cache, bool linear=false);
~levelwise();
levelwise(levelwise const&) = delete;

56
src/nlsat/nlsat_explain.cpp
View file

@ -1040,13 +1040,13 @@ namespace nlsat {
\brief Apply model-based projection operation defined in our paper.
*/
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache, bool linear=false) {
// Store polynomials for debugging unsound lemmas
m_last_lws_input_polys.reset();
for (unsigned i = 0; i < ps.size(); i++)
m_last_lws_input_polys.push_back(ps.get(i));
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache, linear);
auto cell = lws.single_cell();
TRACE(lws, for (unsigned i = 0; i < cell.size(); i++)
display(tout << "I[" << i << "]:", m_solver, cell[i]) << "\n";);
@ -1139,9 +1139,23 @@ namespace nlsat {
x = extract_max_polys(ps);
cac_add_cell_lits(ps, x, samples);
}
}
/**
* \brief compute the resultants of p with each polynomial in ps w.r.t. x
*/
void psc_resultants_with(polynomial_ref_vector const& ps, polynomial_ref p, var const x) {
polynomial_ref q(m_pm);
unsigned sz = ps.size();
for (unsigned i = 0; i < sz; i++) {
q = ps.get(i);
if (q == p) continue;
psc(p, q, x);
}
}
bool check_already_added() const {
for (bool b : m_already_added_literal) {
(void)b;
@ -1698,6 +1712,38 @@ namespace nlsat {
}
void compute_linear_explanation(unsigned num, literal const * ls, scoped_literal_vector & result) {
SASSERT(check_already_added());
SASSERT(num > 0);
SASSERT(max_var(num, ls) != 0 || m_solver.sample().is_assigned(0));
TRACE(nlsat_explain,
tout << "the infeasible clause:\n";
display(tout, m_solver, num, ls) << "\n";
m_solver.display_assignment(tout << "assignment:\n");
);
m_result = &result;
m_lower_stage_polys.reset();
collect_polys(num, ls, m_ps);
for (unsigned i = 0; i < m_lower_stage_polys.size(); i++) {
m_ps.push_back(m_lower_stage_polys.get(i));
}
if (m_ps.empty())
return;
// We call levelwise directly without normalize, simplify, elim_vanishing to preserve the original polynomials
var max_x = max_var(m_ps);
bool levelwise_ok = levelwise_single_cell(m_ps, max_x+1, m_cache, true); // max_x+1 because we have a full sample
SASSERT(levelwise_ok);
m_solver.record_levelwise_result(levelwise_ok);
reset_already_added();
m_result = nullptr;
TRACE(nlsat_explain, display(tout << "[explain] result\n", m_solver, result) << "\n";);
CASSERT("nlsat", check_already_added());
}
void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
unsigned base = result.size();
while (true) {
@ -1876,6 +1922,10 @@ namespace nlsat {
m_imp->compute_conflict_explanation(n, ls, result);
}
void explain::compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->compute_linear_explanation(n, ls, result);
}
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result);
}

6
src/nlsat/nlsat_explain.h
View file

@ -66,6 +66,12 @@ namespace nlsat {
*/
void compute_conflict_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief A variant of compute_conflict_explanation, but all resulting literals s_i are linear.
This is achieved by adding new polynomials during the projection, thereby under-approximating
the computed cell.
*/
void compute_linear_explanation(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief projection for a given variable.

60
src/nlsat/nlsat_solver.cpp
View file

@ -2156,6 +2156,62 @@ namespace nlsat {
m_assignment.reset();
}
lbool check(assignment const& rvalues, literal_vector& clause) {
// temporarily set m_assignment to the given one
assignment tmp = m_assignment;
m_assignment.reset();
m_assignment.copy(rvalues);
// check whether the asserted atoms are satisfied by rvalues
literal best_literal = null_literal;
lbool satisfied = l_true;
for (auto cp : m_clauses) {
auto& c = *cp;
bool is_false = all_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_false; });
bool is_true = any_of(c, [&](literal l) { return const_cast<imp*>(this)->value(l) == l_true; });
if (is_true)
continue;
if (!is_false) {
satisfied = l_undef;
continue;
}
// take best literal from c
for (literal l : c) {
if (best_literal == null_literal) {
best_literal = l;
}
else {
bool_var b_best = best_literal.var();
bool_var b_l = l.var();
if (degree(m_atoms[b_l]) < degree(m_atoms[b_best])) {
best_literal = l;
}
// TODO: there might be better criteria than just the degree in the main variable.
}
}
}
if (best_literal == null_literal)
return satisfied;
// assignment does not satisfy the constraints -> create lemma
SASSERT(best_literal != null_literal);
clause.reset();
m_lazy_clause.reset();
m_explain.compute_linear_explanation(1, &best_literal, m_lazy_clause);
for (auto l : m_lazy_clause) {
clause.push_back(l);
}
clause.push_back(~best_literal);
m_assignment.reset();
m_assignment.copy(tmp);
return l_false;
}
lbool check(literal_vector& assumptions) {
literal_vector result;
unsigned sz = assumptions.size();
@ -4419,6 +4475,10 @@ namespace nlsat {
return m_imp->check(assumptions);
}
lbool solver::check(assignment const& rvalues, literal_vector& clause) {
return m_imp->check(rvalues, clause);
}
void solver::get_core(vector<assumption, false>& assumptions) {
return m_imp->get_core(assumptions);
}

13
src/nlsat/nlsat_solver.h
View file

@ -219,6 +219,19 @@ namespace nlsat {
lbool check(literal_vector& assumptions);
//
// 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 - 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 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.
//
lbool check(assignment const& rvalues, literal_vector& clause);
// -----------------------
//
// Model