mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
d2b2aedef3
commit
e306287d7b
6 changed files with 120 additions and 107 deletions
|
|
@ -35,6 +35,7 @@ Revision History:
|
|||
#include "smt/smt_model_generator.h"
|
||||
#include "smt/arith_eq_adapter.h"
|
||||
#include "util/nat_set.h"
|
||||
#include "util/lp/nra_solver.h"
|
||||
#include "tactic/filter_model_converter.h"
|
||||
|
||||
namespace lp {
|
||||
|
|
@ -144,10 +145,10 @@ namespace smt {
|
|||
ast_manager& m;
|
||||
theory_arith_params& m_arith_params;
|
||||
arith_util a;
|
||||
|
||||
arith_eq_adapter m_arith_eq_adapter;
|
||||
vector<rational> m_columns;
|
||||
|
||||
|
||||
vector<rational> m_columns;
|
||||
// temporary values kept during internalization
|
||||
struct internalize_state {
|
||||
expr_ref_vector m_terms;
|
||||
|
|
@ -248,6 +249,8 @@ namespace smt {
|
|||
|
||||
unsigned m_num_conflicts;
|
||||
|
||||
scoped_ptr<nra::solver> m_nra;
|
||||
bool m_use_nra_model;
|
||||
|
||||
struct var_value_eq {
|
||||
imp & m_th;
|
||||
|
|
@ -291,6 +294,16 @@ namespace smt {
|
|||
//m_solver->settings().set_ostream(0);
|
||||
}
|
||||
|
||||
void ensure_nra() {
|
||||
if (!m_nra) {
|
||||
m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
|
||||
for (unsigned i = 0; i < m_scopes.size(); ++i) {
|
||||
m_nra->push();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void found_not_handled(expr* n) {
|
||||
m_not_handled = n;
|
||||
if (is_app(n) && is_underspecified(to_app(n))) {
|
||||
|
|
@ -456,7 +469,8 @@ namespace smt {
|
|||
}
|
||||
TRACE("arith", tout << mk_pp(t, m) << "\n";);
|
||||
if (!_has_var) {
|
||||
m_solver->add_monomial(get_var_index(v), vars);
|
||||
ensure_nra();
|
||||
m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr());
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -711,7 +725,8 @@ namespace smt {
|
|||
m_num_conflicts(0),
|
||||
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
|
||||
m_solver(0),
|
||||
m_resource_limit(*this) {
|
||||
m_resource_limit(*this),
|
||||
m_use_nra_model(false) {
|
||||
}
|
||||
|
||||
~imp() {
|
||||
|
|
@ -868,6 +883,7 @@ namespace smt {
|
|||
s.m_underspecified_lim = m_underspecified.size();
|
||||
s.m_var_trail_lim = m_var_trail.size();
|
||||
if (!m_delay_constraints) m_solver->push();
|
||||
if (m_nra) m_nra->push();
|
||||
}
|
||||
|
||||
void pop_scope_eh(unsigned num_scopes) {
|
||||
|
|
@ -900,6 +916,7 @@ namespace smt {
|
|||
// VERIFY(l_false != make_feasible());
|
||||
m_new_bounds.reset();
|
||||
m_to_check.reset();
|
||||
if (m_nra) m_nra->pop(num_scopes);
|
||||
TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -1272,21 +1289,23 @@ namespace smt {
|
|||
}
|
||||
|
||||
lbool check_nra() {
|
||||
m_use_nra_model = false;
|
||||
if (m.canceled()) return l_undef;
|
||||
// return l_true;
|
||||
// TBD:
|
||||
switch (m_solver->check_nra(m_variable_values, m_explanation)) {
|
||||
case lean::final_check_status::DONE:
|
||||
return l_true;
|
||||
case lean::final_check_status::CONTINUE:
|
||||
return l_true; // ?? why have a continue at this level ??
|
||||
case lean::final_check_status::UNSAT:
|
||||
if (!m_nra) return l_true;
|
||||
if (!m_nra->need_check()) return l_true;
|
||||
lbool r = m_nra->check(m_explanation);
|
||||
switch (r) {
|
||||
case l_false:
|
||||
set_conflict1();
|
||||
return l_false;
|
||||
case lean::final_check_status::GIVEUP:
|
||||
return l_undef;
|
||||
break;
|
||||
case l_true:
|
||||
m_use_nra_model = true;
|
||||
// TBD: check equalities
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return l_true;
|
||||
return r;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -2355,9 +2374,16 @@ namespace smt {
|
|||
model_value_proc * mk_value(enode * n, model_generator & mg) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
expr* o = n->get_owner();
|
||||
rational r = get_value(v);
|
||||
if (a.is_int(o) && !r.is_int()) r = floor(r);
|
||||
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
|
||||
if (m_use_nra_model) {
|
||||
SASSERT(m_nra);
|
||||
app* e = a.mk_numeral(m_nra->value(m_theory_var2var_index[v]), a.is_int(o));
|
||||
return alloc(expr_wrapper_proc, e);
|
||||
}
|
||||
else {
|
||||
rational r = get_value(v);
|
||||
if (a.is_int(o) && !r.is_int()) r = floor(r);
|
||||
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
|
||||
}
|
||||
}
|
||||
|
||||
bool get_value(enode* n, expr_ref& r) {
|
||||
|
|
|
|||
|
|
@ -32,7 +32,6 @@ lar_solver::lar_solver() : m_status(OPTIMAL),
|
|||
m_terms_start_index(1000000),
|
||||
m_mpq_lar_core_solver(m_settings, *this)
|
||||
{
|
||||
m_nra = alloc(nra::solver, *this);
|
||||
}
|
||||
|
||||
void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) {
|
||||
|
|
@ -332,7 +331,6 @@ void lar_solver::push() {
|
|||
m_term_count.push();
|
||||
m_constraint_count = m_constraints.size();
|
||||
m_constraint_count.push();
|
||||
m_nra->push();
|
||||
}
|
||||
|
||||
void lar_solver::clean_large_elements_after_pop(unsigned n, int_set& set) {
|
||||
|
|
@ -388,7 +386,6 @@ void lar_solver::pop(unsigned k) {
|
|||
m_settings.simplex_strategy() = m_simplex_strategy;
|
||||
lean_assert(sizes_are_correct());
|
||||
lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
|
||||
m_nra->pop(k);
|
||||
}
|
||||
|
||||
vector<constraint_index> lar_solver::get_all_constraint_indices() const {
|
||||
|
|
@ -1088,13 +1085,6 @@ void lar_solver::get_infeasibility_explanation(vector<std::pair<mpq, constraint_
|
|||
lean_assert(explanation_is_correct(explanation));
|
||||
}
|
||||
|
||||
final_check_status lar_solver::check_nra(nra_model_t& model, explanation_t& explanation) {
|
||||
return m_nra->check(model, explanation);
|
||||
}
|
||||
|
||||
void lar_solver::add_monomial(var_index v, svector<var_index> const& vars) {
|
||||
m_nra->add_monomial(v, vars.size(), vars.c_ptr());
|
||||
}
|
||||
|
||||
|
||||
void lar_solver::get_infeasibility_explanation_for_inf_sign(
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@
|
|||
#include "util/lp/quick_xplain.h"
|
||||
#include "util/lp/conversion_helper.h"
|
||||
#include "util/lp/int_solver.h"
|
||||
#include "util/lp/nra_solver.h"
|
||||
|
||||
namespace lean {
|
||||
|
||||
|
|
@ -64,7 +63,6 @@ class lar_solver : public column_namer {
|
|||
vector<lar_term*> m_terms;
|
||||
const var_index m_terms_start_index;
|
||||
indexed_vector<mpq> m_column_buffer;
|
||||
scoped_ptr<nra::solver> m_nra;
|
||||
public:
|
||||
lar_core_solver m_mpq_lar_core_solver;
|
||||
unsigned constraint_count() const;
|
||||
|
|
@ -204,8 +202,6 @@ public:
|
|||
|
||||
lp_status find_feasible_solution();
|
||||
|
||||
final_check_status check_nra(nra_model_t& model, explanation_t& explanation);
|
||||
|
||||
void add_monomial(var_index v, svector<var_index> const& vars);
|
||||
|
||||
lp_status solve();
|
||||
|
|
|
|||
|
|
@ -26,8 +26,6 @@ enum class final_check_status {
|
|||
|
||||
typedef vector<std::pair<mpq, constraint_index>> explanation_t;
|
||||
|
||||
typedef std::unordered_map<lean::var_index, rational> nra_model_t;
|
||||
|
||||
|
||||
enum class column_type {
|
||||
free_column = 0,
|
||||
|
|
|
|||
|
|
@ -16,9 +16,10 @@ namespace nra {
|
|||
|
||||
struct solver::imp {
|
||||
lean::lar_solver& s;
|
||||
reslimit m_limit; // TBD: extract from lar_solver
|
||||
params_ref m_params; // TBD: pass from outside
|
||||
reslimit& m_limit; // TBD: extract from lar_solver
|
||||
params_ref m_params; // TBD: pass from outside
|
||||
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
|
||||
nlsat::solver m_nlsat;
|
||||
|
||||
struct mon_eq {
|
||||
mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs):
|
||||
|
|
@ -31,23 +32,15 @@ namespace nra {
|
|||
unsigned_vector m_lim;
|
||||
mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
|
||||
|
||||
imp(lean::lar_solver& s):
|
||||
s(s) {
|
||||
imp(lean::lar_solver& s, reslimit& lim, params_ref const& p):
|
||||
s(s),
|
||||
m_limit(lim),
|
||||
m_params(p),
|
||||
m_nlsat(m_limit, m_params) {
|
||||
}
|
||||
|
||||
lean::final_check_status check_feasible(lean::nra_model_t& m, lean::explanation_t& ex) {
|
||||
if (m_monomials.empty()) {
|
||||
return lean::final_check_status::DONE;
|
||||
}
|
||||
if (check_assignments()) {
|
||||
return lean::final_check_status::DONE;
|
||||
}
|
||||
switch (check_nlsat(m, ex)) {
|
||||
case l_undef: return lean::final_check_status::GIVEUP;
|
||||
case l_true: return lean::final_check_status::DONE;
|
||||
case l_false: return lean::final_check_status::UNSAT;
|
||||
}
|
||||
return lean::final_check_status::DONE;
|
||||
bool need_check() {
|
||||
return !m_monomials.empty() && !check_assignments();
|
||||
}
|
||||
|
||||
void add(lean::var_index v, unsigned sz, lean::var_index const* vs) {
|
||||
|
|
@ -97,71 +90,51 @@ namespace nra {
|
|||
|
||||
TBD: use partial model from lra_solver to prime the state of nlsat_solver.
|
||||
*/
|
||||
lbool check_nlsat(lean::nra_model_t& model, lean::explanation_t& ex) {
|
||||
nlsat::solver solver(m_limit, m_params);
|
||||
lbool check(lean::explanation_t& ex) {
|
||||
SASSERT(need_check());
|
||||
m_nlsat.reset();
|
||||
m_lp2nl.reset();
|
||||
vector<nlsat::assumption, false> core;
|
||||
|
||||
// add linear inequalities from lra_solver
|
||||
for (unsigned i = 0; i < s.constraint_count(); ++i) {
|
||||
add_constraint(solver, i);
|
||||
add_constraint(i);
|
||||
}
|
||||
|
||||
// add polynomial definitions.
|
||||
for (auto const& m : m_monomials) {
|
||||
add_monomial_eq(solver, m);
|
||||
add_monomial_eq(m);
|
||||
}
|
||||
// TBD: add variable bounds?
|
||||
|
||||
|
||||
lbool r = solver.check();
|
||||
TRACE("arith", solver.display(tout << r << "\n"););
|
||||
lbool r = m_nlsat.check();
|
||||
TRACE("arith", m_nlsat.display(tout << r << "\n"););
|
||||
switch (r) {
|
||||
case l_true: {
|
||||
nlsat::anum_manager& am = solver.am();
|
||||
model.clear();
|
||||
for (auto kv : m_lp2nl) {
|
||||
kv.m_key;
|
||||
nlsat::anum const& v = solver.value(kv.m_value);
|
||||
if (is_int(kv.m_key) && !am.is_int(v)) {
|
||||
// the nlsat solver should already have returned unknown.
|
||||
TRACE("lp", tout << "Value is not integer " << kv.m_key << "\n";);
|
||||
return l_undef;
|
||||
}
|
||||
if (!am.is_rational(v)) {
|
||||
// TBD extract and convert model.
|
||||
TRACE("lp", tout << "Cannot handle algebraic numbers\n";);
|
||||
return l_undef;
|
||||
}
|
||||
rational r;
|
||||
am.to_rational(v, r);
|
||||
model[kv.m_key] = r;
|
||||
}
|
||||
case l_true:
|
||||
break;
|
||||
}
|
||||
case l_false: {
|
||||
case l_false:
|
||||
ex.reset();
|
||||
vector<nlsat::assumption, false> core;
|
||||
solver.get_core(core);
|
||||
m_nlsat.get_core(core);
|
||||
for (auto c : core) {
|
||||
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
|
||||
ex.push_back(std::pair<rational, unsigned>(rational(1), idx));
|
||||
TRACE("arith", tout << "ex: " << idx << "\n";);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void add_monomial_eq(nlsat::solver& solver, mon_eq const& m) {
|
||||
polynomial::manager& pm = solver.pm();
|
||||
void add_monomial_eq(mon_eq const& m) {
|
||||
polynomial::manager& pm = m_nlsat.pm();
|
||||
svector<polynomial::var> vars;
|
||||
for (auto v : m.m_vs) {
|
||||
vars.push_back(lp2nl(solver, v));
|
||||
vars.push_back(lp2nl(v));
|
||||
}
|
||||
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
|
||||
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(solver, m.m_v), 1), pm);
|
||||
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.m_v), 1), pm);
|
||||
polynomial::monomial* mls[2] = { m1, m2 };
|
||||
polynomial::scoped_numeral_vector coeffs(pm.m());
|
||||
coeffs.push_back(mpz(1));
|
||||
|
|
@ -169,13 +142,13 @@ namespace nra {
|
|||
polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.c_ptr(), mls), pm);
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
bool even[1] = { false };
|
||||
nlsat::literal lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
|
||||
solver.mk_clause(1, &lit, 0);
|
||||
nlsat::literal lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
|
||||
m_nlsat.mk_clause(1, &lit, 0);
|
||||
}
|
||||
|
||||
void add_constraint(nlsat::solver& solver, unsigned idx) {
|
||||
void add_constraint(unsigned idx) {
|
||||
auto& c = s.get_constraint(idx);
|
||||
auto& pm = solver.pm();
|
||||
auto& pm = m_nlsat.pm();
|
||||
auto k = c.m_kind;
|
||||
auto rhs = c.m_right_side;
|
||||
auto lhs = c.get_left_side_coefficients();
|
||||
|
|
@ -183,7 +156,7 @@ namespace nra {
|
|||
svector<polynomial::var> vars;
|
||||
rational den = denominator(rhs);
|
||||
for (auto kv : lhs) {
|
||||
vars.push_back(lp2nl(solver, kv.second));
|
||||
vars.push_back(lp2nl(kv.second));
|
||||
den = lcm(den, denominator(kv.first));
|
||||
}
|
||||
vector<rational> coeffs;
|
||||
|
|
@ -197,24 +170,24 @@ namespace nra {
|
|||
nlsat::literal lit;
|
||||
switch (k) {
|
||||
case lean::lconstraint_kind::LE:
|
||||
lit = ~solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lean::lconstraint_kind::GE:
|
||||
lit = ~solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
lit = ~m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lean::lconstraint_kind::LT:
|
||||
lit = solver.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lean::lconstraint_kind::GT:
|
||||
lit = solver.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lean::lconstraint_kind::EQ:
|
||||
lit = solver.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
lit = m_nlsat.mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
break;
|
||||
}
|
||||
|
||||
nlsat::assumption a = this + idx;
|
||||
solver.mk_clause(1, &lit, a);
|
||||
m_nlsat.mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
bool is_int(lean::var_index v) {
|
||||
|
|
@ -222,15 +195,20 @@ namespace nra {
|
|||
return false;
|
||||
}
|
||||
|
||||
polynomial::var lp2nl(nlsat::solver& solver, lean::var_index v) {
|
||||
|
||||
polynomial::var lp2nl(lean::var_index v) {
|
||||
polynomial::var r;
|
||||
if (!m_lp2nl.find(v, r)) {
|
||||
r = solver.mk_var(is_int(v));
|
||||
r = m_nlsat.mk_var(is_int(v));
|
||||
m_lp2nl.insert(v, r);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
nlsat::anum const& value(lean::var_index v) const {
|
||||
return m_nlsat.value(m_lp2nl.find(v));
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
for (auto m : m_monomials) {
|
||||
out << "v" << m.m_v << " = ";
|
||||
|
|
@ -244,8 +222,8 @@ namespace nra {
|
|||
|
||||
};
|
||||
|
||||
solver::solver(lean::lar_solver& s) {
|
||||
m_imp = alloc(imp, s);
|
||||
solver::solver(lean::lar_solver& s, reslimit& lim, params_ref const& p) {
|
||||
m_imp = alloc(imp, s, lim, p);
|
||||
}
|
||||
|
||||
solver::~solver() {
|
||||
|
|
@ -256,8 +234,12 @@ namespace nra {
|
|||
m_imp->add(v, sz, vs);
|
||||
}
|
||||
|
||||
lean::final_check_status solver::check(lean::nra_model_t& m, lean::explanation_t& ex) {
|
||||
return m_imp->check_feasible(m, ex);
|
||||
lbool solver::check(lean::explanation_t& ex) {
|
||||
return m_imp->check(ex);
|
||||
}
|
||||
|
||||
bool solver::need_check() {
|
||||
return m_imp->need_check();
|
||||
}
|
||||
|
||||
void solver::push() {
|
||||
|
|
@ -272,4 +254,8 @@ namespace nra {
|
|||
return m_imp->display(out);
|
||||
}
|
||||
|
||||
nlsat::anum const& solver::value(lean::var_index v) const {
|
||||
return m_imp->value(v);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -6,20 +6,26 @@
|
|||
#pragma once
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/lp_settings.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "util/params.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
|
||||
namespace lean {
|
||||
class lar_solver;
|
||||
}
|
||||
|
||||
|
||||
namespace nra {
|
||||
|
||||
typedef std::unordered_map<lean::var_index, rational> nra_model_t;
|
||||
|
||||
class solver {
|
||||
struct imp;
|
||||
imp* m_imp;
|
||||
|
||||
public:
|
||||
|
||||
solver(lean::lar_solver& s);
|
||||
solver(lean::lar_solver& s, reslimit& lim, params_ref const& p = params_ref());
|
||||
|
||||
~solver();
|
||||
|
||||
|
|
@ -33,7 +39,17 @@ namespace nra {
|
|||
\brief Check feasiblity of linear constraints augmented by polynomial definitions
|
||||
that are added.
|
||||
*/
|
||||
lean::final_check_status check(lean::nra_model_t& m, lean::explanation_t& ex);
|
||||
lbool check(lean::explanation_t& ex);
|
||||
|
||||
/*
|
||||
\brief determine whether nra check is needed.
|
||||
*/
|
||||
bool need_check();
|
||||
|
||||
/*
|
||||
\brief Access model.
|
||||
*/
|
||||
nlsat::anum const& value(lean::var_index v) const;
|
||||
|
||||
/*
|
||||
\brief push and pop scope.
|
||||
|
|
@ -47,5 +63,6 @@ namespace nra {
|
|||
\brief display state
|
||||
*/
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue