mirror of
https://github.com/Z3Prover/z3
synced 2026-03-16 02:00:00 +00:00
Nl2lin - integrate a linear under approximation of a CAD cell by Valentin Promies. (#8982)
* outline of signature for assignment based conflict generation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * outline of interface contract Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove confusing construction Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add material in nra-solver to interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add marshaling from nlsat lemmas into core solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add call to check-assignment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Nl2lin (#7795) * add linearized projection in nlsat * implement nlsat check for given assignment * add some comments * fixup loop Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debug nl2lin Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Nl2lin (#7827) * fix linear projection * fix linear projection * use an explicit cell description in check_assignment * clean up (#7844) * Simplify no effect checks in nla_core.cpp Move up linear nlsat call to replace bounded nlsat. * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * detangle mess Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove the too early return Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * do not set use_nra_model to true Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add a hook to add new multiplication definitions in nla_core * add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add internalization routine that uses macro-expanded polynomial representation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixup backtranslation to not use roots Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * call setup_assignment_solver instead of setup_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debug the setup, still not working Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * updated clang format Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simplify Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * create polynomials with integer coefficients, use the hook to create new monomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * integrating changes from master related to work with polynomials Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add forgotten files Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Update nlsat_explain.cpp Remove a duplicate call * fix * move linear cell construction to levelwise * fix * fix * Port throttle and soundness fixes from master - 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> * Add arith.nl.nra_check_assignment_max_fail parameter Replace hardcoded failure threshold with configurable parameter (default 10). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * Add cha_abort_on_fail parameter to control failure counter decrement Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> * abort nla check_assignment after a set number of allowed failures Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Add missing AST query methods to Java API (#8977) * add Expr.isGround() to Java API Expose Z3_is_ground as a public method on Expr. Returns true when the expression contains no free variables. * add Expr.isLambda() to Java API Expose Z3_is_lambda as a public method on Expr. Returns true when the expression is a lambda quantifier. * add AST.getDepth() to Java API Expose Z3_get_depth as a public method on AST. Returns the maximum number of nodes on any path from root to leaf. * add ArraySort.getArity() to Java API Expose Z3_get_array_arity as a public method on ArraySort. Returns the number of dimensions of a multi-dimensional array sort. * add DatatypeSort.isRecursive() to Java API Expose Z3_is_recursive_datatype_sort as a public method on DatatypeSort. Returns true when the datatype refers to itself. * add FPExpr.isNumeral() to Java API Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true when the expression is a concrete floating-point value. * add isGroundExample test to JavaExample Test Expr.isGround() on constants, variables, and compound expressions. * add astDepthExample test to JavaExample Test AST.getDepth() on leaf nodes and nested expressions to verify the depth computation. * add arrayArityExample test to JavaExample Test ArraySort.getArity() on single-domain and multi-domain array sorts. * add recursiveDatatypeExample test to JavaExample Test DatatypeSort.isRecursive() on a recursive list datatype and a non-recursive pair datatype. * add fpNumeralExample test to JavaExample Test FPExpr.isNumeral() on a floating point constant and a symbolic variable. * add isLambdaExample test to JavaExample Test Expr.isLambda() on a lambda expression and a plain variable. * change the default number of failures in check_assignment to 7 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Fix high and medium priority API coherence issues (Go, Java, C++, TypeScript) (#8983) * Initial plan * Add missing API functions to Go, Java, C++, and TypeScript bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * qf-s-benchmark: debug build + seq tracing + seq-fast/nseq-slow trace analysis (#8988) * Initial plan * Update qf-s-benchmark: debug build, seq tracing, trace analysis Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * disable linear approximation by default to check the merge Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * set check_assignment to true Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix restore_x by recalulating new column values Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a memory leak Signed-off-by: Lev Nachmanson <levnach@hotmail.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: ValentinPromies <44966217+ValentinPromies@users.noreply.github.com> Co-authored-by: Valentin Promies <valentin.promies@rwth-aachen.de> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: Angelica Moreira <48168649+angelica-moreira@users.noreply.github.com> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson
GitHub
parent
cb13fa2325
commit
6fb68ac010
17 changed files with 497 additions and 22 deletions
|
|
@ -446,8 +446,11 @@ public:
|
|||
cs.restore_x();
|
||||
if (backup_sz < current_sz) {
|
||||
// New columns were added after backup.
|
||||
// move_non_basic_columns_to_bounds snaps non-basic
|
||||
// columns to their bounds and finds a feasible solution.
|
||||
// Recalculate basic variable values from non-basic ones
|
||||
// to restore the Ax=0 tableau invariant, then snap
|
||||
// non-basic columns to their bounds and find a feasible solution.
|
||||
for (unsigned i = 0; i < A_r().row_count(); i++)
|
||||
set_column_value(r_basis()[i], get_basic_var_value_from_row(i));
|
||||
move_non_basic_columns_to_bounds();
|
||||
}
|
||||
else {
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2025 Microsoft Corporation
|
||||
|
||||
|
|
@ -85,4 +84,4 @@ namespace nla {
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,3 @@
|
|||
|
||||
/*++
|
||||
Copyright (c) 2025 Microsoft Corporation
|
||||
|
||||
|
|
@ -14,6 +13,9 @@
|
|||
|
||||
#pragma once
|
||||
|
||||
#include "util/uint_set.h"
|
||||
#include "util/vector.h"
|
||||
|
||||
namespace nla {
|
||||
|
||||
class core;
|
||||
|
|
@ -40,4 +42,4 @@ namespace nla {
|
|||
indexed_uint_set const &vars() { return m_var_set; }
|
||||
|
||||
};
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1331,7 +1331,14 @@ lbool core::check(unsigned level) {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
|
||||
if (no_effect() && params().arith_nl_nra_check_assignment() && m_check_assignment_fail_cnt < params().arith_nl_nra_check_assignment_max_fail()) {
|
||||
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;
|
||||
}
|
||||
|
||||
if (no_effect() && should_run_bounded_nlsat())
|
||||
ret = bounded_nlsat();
|
||||
|
||||
|
|
@ -1582,4 +1589,4 @@ void core::refine_pseudo_linear(monic const& m) {
|
|||
}
|
||||
SASSERT(nlvar != null_lpvar);
|
||||
lemma |= ineq(lp::lar_term(m.var(), rational(-prod), nlvar), llc::EQ, rational(0));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
@ -94,6 +95,8 @@ class core {
|
|||
emonics m_emons;
|
||||
svector<lpvar> m_add_buffer;
|
||||
mutable indexed_uint_set m_active_var_set;
|
||||
// hook installed by theory_lra for creating a multiplication definition
|
||||
std::function<lpvar(unsigned, lpvar const*)> m_add_mul_def_hook;
|
||||
|
||||
reslimit m_nra_lim;
|
||||
|
||||
|
|
@ -215,6 +218,8 @@ public:
|
|||
void add_idivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_idivision(q, x, y); }
|
||||
void add_rdivision(lpvar q, lpvar x, lpvar y) { m_divisions.add_rdivision(q, x, y); }
|
||||
void add_bounded_division(lpvar q, lpvar x, lpvar y) { m_divisions.add_bounded_division(q, x, y); }
|
||||
void set_add_mul_def_hook(std::function<lpvar(unsigned, lpvar const*)> const& f) { m_add_mul_def_hook = f; }
|
||||
lpvar add_mul_def(unsigned sz, lpvar const* vs) { SASSERT(m_add_mul_def_hook); lpvar v = m_add_mul_def_hook(sz, vs); add_monic(v, sz, vs); return v; }
|
||||
|
||||
void set_relevant(std::function<bool(lpvar)>& is_relevant) { m_relevant = is_relevant; }
|
||||
bool is_relevant(lpvar v) const { return !m_relevant || m_relevant(v); }
|
||||
|
|
@ -478,4 +483,3 @@ inline std::ostream& operator<<(std::ostream& out, pp_factorization const& f) {
|
|||
inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
|
||||
|
||||
} // end of namespace nla
|
||||
|
||||
|
|
|
|||
|
|
@ -12,6 +12,7 @@
|
|||
#include "math/lp/nla_intervals.h"
|
||||
#include "math/lp/nex.h"
|
||||
#include "math/lp/cross_nested.h"
|
||||
#include "util/params.h"
|
||||
#include "util/uint_set.h"
|
||||
#include "math/grobner/pdd_solver.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -432,4 +432,4 @@ std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::l
|
|||
out << (evaluation ? "true" : "false");
|
||||
out << "\n";
|
||||
return out;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@
|
|||
#include "math/lp/nra_solver.h"
|
||||
#include "math/lp/nla_coi.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
#include "nlsat/nlsat_assignment.h"
|
||||
#include "math/polynomial/polynomial.h"
|
||||
#include "math/polynomial/algebraic_numbers.h"
|
||||
#include "util/map.h"
|
||||
|
|
@ -35,6 +36,13 @@ struct solver::imp {
|
|||
scoped_ptr<scoped_anum_vector> m_values; // values provided by LRA solver
|
||||
scoped_ptr<scoped_anum> m_tmp1, m_tmp2;
|
||||
nla::coi m_coi;
|
||||
svector<lp::constraint_index> m_literal2constraint;
|
||||
struct eq {
|
||||
bool operator()(unsigned_vector const &a, unsigned_vector const &b) const {
|
||||
return a == b;
|
||||
}
|
||||
};
|
||||
map<unsigned_vector, unsigned, svector_hash<unsigned_hash>, eq> m_vars2mon;
|
||||
nla::core& m_nla_core;
|
||||
|
||||
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
|
||||
|
|
@ -92,6 +100,44 @@ struct solver::imp {
|
|||
denominators.push_back(den);
|
||||
}
|
||||
|
||||
// Create polynomial definition for variable v used in setup_assignment_solver.
|
||||
// Side-effects: updates m_vars2mon when v is a monic variable.
|
||||
void mk_definition_assignment(unsigned v, polynomial_ref_vector &definitions) {
|
||||
auto &pm = m_nlsat->pm();
|
||||
polynomial::polynomial_ref p(pm);
|
||||
if (m_nla_core.emons().is_monic_var(v)) {
|
||||
auto const &m = m_nla_core.emons()[v];
|
||||
auto vars = m.vars();
|
||||
std::sort(vars.begin(), vars.end());
|
||||
m_vars2mon.insert(vars, v);
|
||||
for (auto v2 : vars) {
|
||||
auto pv = definitions.get(v2);
|
||||
if (!p)
|
||||
p = pv;
|
||||
else
|
||||
p = pm.mul(p, pv);
|
||||
}
|
||||
}
|
||||
else if (lra.column_has_term(v)) {
|
||||
rational den(1);
|
||||
for (auto const& [w, coeff] : lra.get_term(v))
|
||||
den = lcm(den, denominator(coeff));
|
||||
for (auto const& [w, coeff] : lra.get_term(v)) {
|
||||
auto pw = definitions.get(w);
|
||||
polynomial::polynomial_ref term(pm);
|
||||
term = pm.mul(den * coeff, pw);
|
||||
if (!p)
|
||||
p = term;
|
||||
else
|
||||
p = pm.add(p, term);
|
||||
}
|
||||
}
|
||||
else {
|
||||
p = pm.mk_polynomial(lp2nl(v));
|
||||
}
|
||||
definitions.push_back(p);
|
||||
}
|
||||
|
||||
void setup_solver_poly() {
|
||||
m_coi.init();
|
||||
auto &pm = m_nlsat->pm();
|
||||
|
|
@ -273,7 +319,195 @@ struct solver::imp {
|
|||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
}
|
||||
|
||||
void setup_assignment_solver() {
|
||||
SASSERT(need_check());
|
||||
reset();
|
||||
m_literal2constraint.reset();
|
||||
m_vars2mon.reset();
|
||||
m_coi.init();
|
||||
auto &pm = m_nlsat->pm();
|
||||
polynomial_ref_vector definitions(pm);
|
||||
for (unsigned v = 0; v < lra.number_of_vars(); ++v) {
|
||||
auto j = m_nlsat->mk_var(lra.var_is_int(v));
|
||||
VERIFY(j == v);
|
||||
m_lp2nl.insert(v, j);
|
||||
scoped_anum a(am());
|
||||
am().set(a, m_nla_core.val(v).to_mpq());
|
||||
m_values->push_back(a);
|
||||
mk_definition_assignment(v, definitions);
|
||||
}
|
||||
|
||||
for (auto ci : m_coi.constraints()) {
|
||||
auto &c = lra.constraints()[ci];
|
||||
auto &pm = m_nlsat->pm();
|
||||
auto k = c.kind();
|
||||
auto rhs = c.rhs();
|
||||
auto lhs = c.coeffs();
|
||||
rational den = denominator(rhs);
|
||||
for (auto [coeff, v] : lhs)
|
||||
den = lcm(den, denominator(coeff));
|
||||
polynomial::polynomial_ref p(pm);
|
||||
p = pm.mk_const(-den * rhs);
|
||||
|
||||
for (auto [coeff, v] : lhs) {
|
||||
polynomial_ref poly(pm);
|
||||
poly = pm.mul(den * coeff, definitions.get(v));
|
||||
p = p + poly;
|
||||
}
|
||||
auto lit = add_constraint(p, ci, k);
|
||||
m_literal2constraint.setx(lit.index(), ci, lp::null_ci);
|
||||
}
|
||||
}
|
||||
|
||||
void process_polynomial_check_assignment(polynomial::polynomial const* p, rational& bound, const u_map<lp::lpvar>& nl2lp, lp::lar_term& t) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
for (unsigned i = 0; i < pm.size(p); ++i) {
|
||||
polynomial::monomial* m = pm.get_monomial(p, i);
|
||||
auto& coeff = pm.coeff(p, i);
|
||||
|
||||
unsigned num_vars = pm.size(m);
|
||||
// add mon * coeff to t;
|
||||
switch (num_vars) {
|
||||
case 0:
|
||||
bound -= coeff;
|
||||
break;
|
||||
case 1: {
|
||||
auto v = nl2lp[pm.get_var(m, 0)];
|
||||
t.add_monomial(coeff, v);
|
||||
break;
|
||||
}
|
||||
default: {
|
||||
svector<lp::lpvar> vars;
|
||||
for (unsigned j = 0; j < num_vars; ++j)
|
||||
vars.push_back(nl2lp[pm.get_var(m, j)]);
|
||||
std::sort(vars.begin(), vars.end());
|
||||
lp::lpvar v;
|
||||
if (m_vars2mon.contains(vars))
|
||||
v = m_vars2mon[vars];
|
||||
else
|
||||
v = m_nla_core.add_mul_def(vars.size(), vars.data());
|
||||
t.add_monomial(coeff, v);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
u_map<lp::lpvar> reverse_lp2nl() {
|
||||
u_map<lp::lpvar> nl2lp;
|
||||
for (auto [j, x] : m_lp2nl)
|
||||
nl2lp.insert(x, j);
|
||||
return nl2lp;
|
||||
}
|
||||
|
||||
lbool check_assignment() {
|
||||
setup_assignment_solver();
|
||||
lbool r = l_undef;
|
||||
statistics &st = m_nla_core.lp_settings().stats().m_st;
|
||||
nlsat::literal_vector clause;
|
||||
try {
|
||||
nlsat::assignment rvalues(m_nlsat->am());
|
||||
for (auto [j, x] : m_lp2nl) {
|
||||
scoped_anum a(am());
|
||||
am().set(a, m_nla_core.val(j).to_mpq());
|
||||
rvalues.set(x, a);
|
||||
}
|
||||
r = m_nlsat->check(rvalues, clause);
|
||||
}
|
||||
catch (z3_exception &) {
|
||||
if (m_limit.is_canceled()) {
|
||||
r = l_undef;
|
||||
}
|
||||
else {
|
||||
m_nlsat->collect_statistics(st);
|
||||
throw;
|
||||
}
|
||||
}
|
||||
m_nlsat->collect_statistics(st);
|
||||
switch (r) {
|
||||
case l_true:
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
lra.init_model();
|
||||
for (lp::constraint_index ci : lra.constraints().indices())
|
||||
if (!check_constraint(ci))
|
||||
return l_undef;
|
||||
for (auto const& m : m_nla_core.emons())
|
||||
if (!check_monic(m))
|
||||
return l_undef;
|
||||
m_nla_core.set_use_nra_model(true);
|
||||
break;
|
||||
case l_false:
|
||||
r = add_lemma(clause);
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool add_lemma(nlsat::literal_vector const &clause) {
|
||||
u_map<lp::lpvar> nl2lp = reverse_lp2nl();
|
||||
polynomial::manager &pm = m_nlsat->pm();
|
||||
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();
|
||||
result = l_undef;
|
||||
break;
|
||||
}
|
||||
if (result == l_undef)
|
||||
break;
|
||||
if (m_nla_core.ineq_holds(inq)) {
|
||||
result = l_undef;
|
||||
break;
|
||||
}
|
||||
lemma |= inq;
|
||||
}
|
||||
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;
|
||||
}
|
||||
|
||||
|
||||
void add_monic_eq_bound(mon_eq const& m) {
|
||||
|
|
@ -643,10 +877,9 @@ struct solver::imp {
|
|||
unsigned w;
|
||||
scoped_anum a(am());
|
||||
for (unsigned v = m_values->size(); v < sz; ++v) {
|
||||
if (m_nla_core.emons().is_monic_var(v)) {
|
||||
if (m_nla_core.emons().is_monic_var(v)) {
|
||||
am().set(a, 1);
|
||||
auto &m = m_nla_core.emon(v);
|
||||
|
||||
for (auto x : m.vars())
|
||||
am().mul(a, (*m_values)[x], a);
|
||||
m_values->push_back(a);
|
||||
|
|
@ -654,7 +887,7 @@ struct solver::imp {
|
|||
else if (lra.column_has_term(v)) {
|
||||
scoped_anum b(am());
|
||||
am().set(a, 0);
|
||||
for (auto const &[w, coeff] : lra.get_term(v)) {
|
||||
for (auto const &[w, coeff] : lra.get_term(v)) {
|
||||
am().set(b, coeff.to_mpq());
|
||||
am().mul(b, (*m_values)[w], b);
|
||||
am().add(a, b, a);
|
||||
|
|
@ -737,6 +970,10 @@ lbool solver::check(dd::solver::equation_vector const& eqs) {
|
|||
return m_imp->check(eqs);
|
||||
}
|
||||
|
||||
lbool solver::check_assignment() {
|
||||
return m_imp->check_assignment();
|
||||
}
|
||||
|
||||
bool solver::need_check() {
|
||||
return m_imp->need_check();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -47,6 +47,11 @@ namespace nra {
|
|||
*/
|
||||
lbool check(dd::solver::equation_vector const& eqs);
|
||||
|
||||
/**
|
||||
\brief Check feasibility modulo current value assignment.
|
||||
*/
|
||||
lbool check_assignment();
|
||||
|
||||
/*
|
||||
\brief determine whether nra check is needed.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -60,6 +60,8 @@ 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.nra_check_assignment_max_fail', UINT, 7, 'maximum consecutive check_assignment failures before disabling it'),
|
||||
('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'),
|
||||
|
|
|
|||
|
|
@ -155,6 +155,7 @@ class theory_lra::imp {
|
|||
ptr_vector<expr> m_not_handled;
|
||||
ptr_vector<app> m_underspecified;
|
||||
ptr_vector<app> m_bv_terms;
|
||||
ptr_vector<expr> m_mul_defs; // fresh multiplication definition vars
|
||||
vector<ptr_vector<api_bound> > m_use_list; // bounds where variables are used.
|
||||
|
||||
// attributes for incremental version:
|
||||
|
|
@ -267,9 +268,25 @@ class theory_lra::imp {
|
|||
};
|
||||
m_nla->set_relevant(is_relevant);
|
||||
m_nla->updt_params(ctx().get_params());
|
||||
m_nla->get_core().set_add_mul_def_hook([&](unsigned sz, lpvar const* vs) { return add_mul_def(sz, vs); });
|
||||
}
|
||||
}
|
||||
|
||||
lpvar add_mul_def(unsigned sz, lpvar const* vs) {
|
||||
bool is_int = true;
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
theory_var tv = lp().local_to_external(vs[i]);
|
||||
is_int &= this->is_int(tv);
|
||||
}
|
||||
sort* srt = is_int ? a.mk_int() : a.mk_real();
|
||||
app_ref c(m.mk_fresh_const("mul!", srt), m);
|
||||
mk_enode(c);
|
||||
theory_var v = mk_var(c);
|
||||
ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_mul_defs));
|
||||
m_mul_defs.push_back(c);
|
||||
return register_theory_var_in_lar_solver(v);
|
||||
}
|
||||
|
||||
void found_unsupported(expr* n) {
|
||||
ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_not_handled));
|
||||
TRACE(arith, tout << "unsupported " << mk_pp(n, m) << "\n");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue