mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
nra to nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
bd0180925b
commit
7a79397769
|
|
@ -24,6 +24,8 @@
|
|||
#include "math/lp/horner.h"
|
||||
#include "math/lp/nla_intervals.h"
|
||||
#include "math/grobner/pdd_solver.h"
|
||||
#include "math/lp/nla_lemma.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
|
||||
|
||||
namespace nla {
|
||||
|
|
@ -66,18 +68,6 @@ public:
|
|||
const rational& rs() const { return m_rs; };
|
||||
};
|
||||
|
||||
class lemma {
|
||||
vector<ineq> m_ineqs;
|
||||
lp::explanation m_expl;
|
||||
public:
|
||||
void push_back(const ineq& i) { m_ineqs.push_back(i);}
|
||||
size_t size() const { return m_ineqs.size() + m_expl.size(); }
|
||||
const vector<ineq>& ineqs() const { return m_ineqs; }
|
||||
vector<ineq>& ineqs() { return m_ineqs; }
|
||||
lp::explanation& expl() { return m_expl; }
|
||||
const lp::explanation& expl() const { return m_expl; }
|
||||
bool is_conflict() const { return m_ineqs.empty() && !m_expl.empty(); }
|
||||
};
|
||||
|
||||
class core;
|
||||
//
|
||||
|
|
|
|||
|
|
@ -12,8 +12,12 @@
|
|||
#include "math/lp/var_eqs.h"
|
||||
#include "math/lp/factorization.h"
|
||||
#include "math/lp/nla_solver.h"
|
||||
#include "math/lp/nla_core.h"
|
||||
|
||||
namespace nla {
|
||||
|
||||
nla_settings& solver::settings() { return m_core->m_nla_settings; }
|
||||
|
||||
void solver::add_monic(lpvar v, unsigned sz, lpvar const* vs) {
|
||||
m_core->add_monic(v, sz, vs);
|
||||
}
|
||||
|
|
@ -36,7 +40,8 @@ void solver::pop(unsigned n) {
|
|||
m_core->pop(n);
|
||||
}
|
||||
|
||||
solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)) {
|
||||
solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit)),
|
||||
m_nra(s, m_res_limit, *m_core) {
|
||||
}
|
||||
|
||||
bool solver::influences_nl_var(lpvar j) const {
|
||||
|
|
|
|||
|
|
@ -11,23 +11,27 @@ Author:
|
|||
#include "math/lp/lp_settings.h"
|
||||
#include "util/rlimit.h"
|
||||
#include "util/params.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
#include "math/lp/lar_solver.h"
|
||||
#include "math/lp/monic.h"
|
||||
#include "math/lp/nla_core.h"
|
||||
#include "math/lp/nla_settings.h"
|
||||
#include "math/lp/nla_lemma.h"
|
||||
|
||||
namespace nra {
|
||||
class solver;
|
||||
}
|
||||
namespace nla {
|
||||
|
||||
class core;
|
||||
// nonlinear integer incremental linear solver
|
||||
class solver {
|
||||
reslimit m_res_limit;
|
||||
core* m_core;
|
||||
nra::solver m_nra;
|
||||
public:
|
||||
void add_monic(lpvar v, unsigned sz, lpvar const* vs);
|
||||
|
||||
solver(lp::lar_solver& s);
|
||||
~solver();
|
||||
nla_settings& settings() { return m_core->m_nla_settings; }
|
||||
nla_settings& settings();
|
||||
void push();
|
||||
void pop(unsigned scopes);
|
||||
bool need_check();
|
||||
|
|
|
|||
|
|
@ -9,272 +9,273 @@
|
|||
#include "math/polynomial/polynomial.h"
|
||||
#include "math/polynomial/algebraic_numbers.h"
|
||||
#include "util/map.h"
|
||||
#include "math/lp/monic.h"
|
||||
#include "math/lp/nla_core.h"
|
||||
|
||||
|
||||
namespace nra {
|
||||
|
||||
typedef nla::mon_eq mon_eq;
|
||||
|
||||
typedef nla::variable_map_type variable_map_type;
|
||||
struct solver::imp {
|
||||
lp::lar_solver& s;
|
||||
reslimit& m_limit;
|
||||
params_ref m_params;
|
||||
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
|
||||
scoped_ptr<nlsat::solver> m_nlsat;
|
||||
scoped_ptr<scoped_anum> m_zero;
|
||||
vector<mon_eq> m_monics;
|
||||
unsigned_vector m_monics_lim;
|
||||
mutable variable_map_type m_variable_values; // current model
|
||||
struct solver::imp {
|
||||
lp::lar_solver& s;
|
||||
reslimit& m_limit;
|
||||
params_ref m_params;
|
||||
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
|
||||
scoped_ptr<nlsat::solver> m_nlsat;
|
||||
scoped_ptr<scoped_anum> m_zero;
|
||||
vector<mon_eq> m_monics;
|
||||
unsigned_vector m_monics_lim;
|
||||
mutable variable_map_type m_variable_values; // current model
|
||||
nla::core& m_nla_core;
|
||||
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
|
||||
s(s),
|
||||
m_limit(lim),
|
||||
m_params(p),
|
||||
m_nla_core(nla_core) {}
|
||||
|
||||
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p):
|
||||
s(s),
|
||||
m_limit(lim),
|
||||
m_params(p) {
|
||||
}
|
||||
bool need_check() {
|
||||
return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
|
||||
}
|
||||
|
||||
bool need_check() {
|
||||
return !m_monics.empty() && !check_assignments(m_monics, s, m_variable_values);
|
||||
}
|
||||
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
|
||||
m_monics.push_back(mon_eq(v, sz, vs));
|
||||
}
|
||||
|
||||
void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
|
||||
m_monics.push_back(mon_eq(v, sz, vs));
|
||||
}
|
||||
void push() {
|
||||
m_monics_lim.push_back(m_monics.size());
|
||||
}
|
||||
|
||||
void push() {
|
||||
m_monics_lim.push_back(m_monics.size());
|
||||
}
|
||||
void pop(unsigned n) {
|
||||
if (n == 0) return;
|
||||
m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
|
||||
m_monics_lim.shrink(m_monics_lim.size() - n);
|
||||
}
|
||||
|
||||
void pop(unsigned n) {
|
||||
if (n == 0) return;
|
||||
m_monics.shrink(m_monics_lim[m_monics_lim.size() - n]);
|
||||
m_monics_lim.shrink(m_monics_lim.size() - n);
|
||||
}
|
||||
/*
|
||||
\brief Check if polynomials are well defined.
|
||||
multiply values for vs and check if they are equal to value for v.
|
||||
epsilon has been computed.
|
||||
*/
|
||||
/* bool check_assignment(mon_eq const& m) const {
|
||||
rational r1 = m_variable_values[m.m_v];
|
||||
rational r2(1);
|
||||
for (auto w : m.vars()) {
|
||||
r2 *= m_variable_values[w];
|
||||
}
|
||||
return r1 == r2;
|
||||
}
|
||||
|
||||
/*
|
||||
\brief Check if polynomials are well defined.
|
||||
multiply values for vs and check if they are equal to value for v.
|
||||
epsilon has been computed.
|
||||
*/
|
||||
/* bool check_assignment(mon_eq const& m) const {
|
||||
rational r1 = m_variable_values[m.m_v];
|
||||
rational r2(1);
|
||||
for (auto w : m.vars()) {
|
||||
r2 *= m_variable_values[w];
|
||||
}
|
||||
return r1 == r2;
|
||||
}
|
||||
|
||||
bool check_assignments() const {
|
||||
s.get_model(m_variable_values);
|
||||
for (auto const& m : m_monics) {
|
||||
if (!check_assignment(m)) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
*/
|
||||
/**
|
||||
\brief one-shot nlsat check.
|
||||
A one shot checker is the least functionality that can
|
||||
enable non-linear reasoning.
|
||||
In addition to checking satisfiability we would also need
|
||||
to identify equalities in the model that should be assumed
|
||||
with the remaining solver.
|
||||
bool check_assignments() const {
|
||||
s.get_model(m_variable_values);
|
||||
for (auto const& m : m_monics) {
|
||||
if (!check_assignment(m)) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
*/
|
||||
/**
|
||||
\brief one-shot nlsat check.
|
||||
A one shot checker is the least functionality that can
|
||||
enable non-linear reasoning.
|
||||
In addition to checking satisfiability we would also need
|
||||
to identify equalities in the model that should be assumed
|
||||
with the remaining solver.
|
||||
|
||||
TBD: use partial model from lra_solver to prime the state of nlsat_solver.
|
||||
TBD: explore more incremental ways of applying nlsat (using assumptions)
|
||||
*/
|
||||
lbool check(lp::explanation& ex) {
|
||||
SASSERT(need_check());
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_lp2nl.reset();
|
||||
vector<nlsat::assumption, false> core;
|
||||
TBD: use partial model from lra_solver to prime the state of nlsat_solver.
|
||||
TBD: explore more incremental ways of applying nlsat (using assumptions)
|
||||
*/
|
||||
lbool check(lp::explanation& ex) {
|
||||
SASSERT(need_check());
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_lp2nl.reset();
|
||||
vector<nlsat::assumption, false> core;
|
||||
|
||||
// add linear inequalities from lra_solver
|
||||
for (lp::constraint_index ci : s.constraints().indices()) {
|
||||
add_constraint(ci);
|
||||
// add linear inequalities from lra_solver
|
||||
for (lp::constraint_index ci : s.constraints().indices()) {
|
||||
add_constraint(ci);
|
||||
}
|
||||
|
||||
// add polynomial definitions.
|
||||
for (auto const& m : m_monics) {
|
||||
add_monic_eq(m);
|
||||
}
|
||||
// TBD: add variable bounds?
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.get_cancel_flag()) {
|
||||
r = l_undef;
|
||||
}
|
||||
|
||||
// add polynomial definitions.
|
||||
for (auto const& m : m_monics) {
|
||||
add_monic_eq(m);
|
||||
else {
|
||||
throw;
|
||||
}
|
||||
// TBD: add variable bounds?
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
}
|
||||
TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
|
||||
switch (r) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
ex.clear();
|
||||
m_nlsat->get_core(core);
|
||||
for (auto c : core) {
|
||||
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
|
||||
ex.push_justification(idx, rational(1));
|
||||
TRACE("arith", tout << "ex: " << idx << "\n";);
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.get_cancel_flag()) {
|
||||
r = l_undef;
|
||||
}
|
||||
else {
|
||||
throw;
|
||||
}
|
||||
}
|
||||
TRACE("arith", display(tout); m_nlsat->display(tout << r << "\n"););
|
||||
switch (r) {
|
||||
case l_true:
|
||||
break;
|
||||
case l_false:
|
||||
ex.clear();
|
||||
m_nlsat->get_core(core);
|
||||
for (auto c : core) {
|
||||
unsigned idx = static_cast<unsigned>(static_cast<imp*>(c) - this);
|
||||
ex.push_justification(idx, rational(1));
|
||||
TRACE("arith", tout << "ex: " << idx << "\n";);
|
||||
}
|
||||
break;
|
||||
break;
|
||||
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void add_monic_eq(mon_eq const& m) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
svector<polynomial::var> vars;
|
||||
void add_monic_eq(mon_eq const& m) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
svector<polynomial::var> vars;
|
||||
for (auto v : m.vars()) {
|
||||
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(m.var()), 1), pm);
|
||||
polynomial::monomial * mls[2] = { m1, m2 };
|
||||
polynomial::scoped_numeral_vector coeffs(pm.m());
|
||||
coeffs.push_back(mpz(1));
|
||||
coeffs.push_back(mpz(-1));
|
||||
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 = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
|
||||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
}
|
||||
|
||||
void add_constraint(unsigned idx) {
|
||||
auto& c = s.constraints()[idx];
|
||||
auto& pm = m_nlsat->pm();
|
||||
auto k = c.kind();
|
||||
auto rhs = c.rhs();
|
||||
auto lhs = c.coeffs();
|
||||
auto sz = lhs.size();
|
||||
svector<polynomial::var> vars;
|
||||
rational den = denominator(rhs);
|
||||
for (auto kv : lhs) {
|
||||
vars.push_back(lp2nl(kv.second));
|
||||
den = lcm(den, denominator(kv.first));
|
||||
}
|
||||
vector<rational> coeffs;
|
||||
for (auto kv : lhs) {
|
||||
coeffs.push_back(den * kv.first);
|
||||
}
|
||||
rhs *= den;
|
||||
polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
bool is_even[1] = { false };
|
||||
nlsat::literal lit;
|
||||
nlsat::assumption a = this + idx;
|
||||
switch (k) {
|
||||
case lp::lconstraint_kind::LE:
|
||||
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::GE:
|
||||
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::LT:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::GT:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::EQ:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
break;
|
||||
default:
|
||||
lp_assert(false); // unreachable
|
||||
}
|
||||
m_nlsat->mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
bool is_int(lp::var_index v) {
|
||||
return s.var_is_int(v);
|
||||
}
|
||||
|
||||
|
||||
polynomial::var lp2nl(lp::var_index v) {
|
||||
polynomial::var r;
|
||||
if (!m_lp2nl.find(v, r)) {
|
||||
r = m_nlsat->mk_var(is_int(v));
|
||||
m_lp2nl.insert(v, r);
|
||||
TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
nlsat::anum const& value(lp::var_index v) const {
|
||||
polynomial::var pv;
|
||||
if (m_lp2nl.find(v, pv))
|
||||
return m_nlsat->value(pv);
|
||||
else
|
||||
return *m_zero;
|
||||
}
|
||||
|
||||
nlsat::anum_manager& am() {
|
||||
return m_nlsat->am();
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
for (auto m : m_monics) {
|
||||
out << "j" << m.var() << " = ";
|
||||
for (auto v : m.vars()) {
|
||||
vars.push_back(lp2nl(v));
|
||||
out << "j" << v << " ";
|
||||
}
|
||||
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
|
||||
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.var()), 1), pm);
|
||||
polynomial::monomial * mls[2] = { m1, m2 };
|
||||
polynomial::scoped_numeral_vector coeffs(pm.m());
|
||||
coeffs.push_back(mpz(1));
|
||||
coeffs.push_back(mpz(-1));
|
||||
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 = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even);
|
||||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
out << "\n";
|
||||
}
|
||||
|
||||
void add_constraint(unsigned idx) {
|
||||
auto& c = s.constraints()[idx];
|
||||
auto& pm = m_nlsat->pm();
|
||||
auto k = c.kind();
|
||||
auto rhs = c.rhs();
|
||||
auto lhs = c.coeffs();
|
||||
auto sz = lhs.size();
|
||||
svector<polynomial::var> vars;
|
||||
rational den = denominator(rhs);
|
||||
for (auto kv : lhs) {
|
||||
vars.push_back(lp2nl(kv.second));
|
||||
den = lcm(den, denominator(kv.first));
|
||||
}
|
||||
vector<rational> coeffs;
|
||||
for (auto kv : lhs) {
|
||||
coeffs.push_back(den * kv.first);
|
||||
}
|
||||
rhs *= den;
|
||||
polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm);
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
bool is_even[1] = { false };
|
||||
nlsat::literal lit;
|
||||
nlsat::assumption a = this + idx;
|
||||
switch (k) {
|
||||
case lp::lconstraint_kind::LE:
|
||||
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::GE:
|
||||
lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::LT:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::GT:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even);
|
||||
break;
|
||||
case lp::lconstraint_kind::EQ:
|
||||
lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
break;
|
||||
default:
|
||||
lp_assert(false); // unreachable
|
||||
}
|
||||
m_nlsat->mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
bool is_int(lp::var_index v) {
|
||||
return s.var_is_int(v);
|
||||
}
|
||||
|
||||
|
||||
polynomial::var lp2nl(lp::var_index v) {
|
||||
polynomial::var r;
|
||||
if (!m_lp2nl.find(v, r)) {
|
||||
r = m_nlsat->mk_var(is_int(v));
|
||||
m_lp2nl.insert(v, r);
|
||||
TRACE("arith", tout << "j" << v << " := x" << r << "\n";);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
nlsat::anum const& value(lp::var_index v) const {
|
||||
polynomial::var pv;
|
||||
if (m_lp2nl.find(v, pv))
|
||||
return m_nlsat->value(pv);
|
||||
else
|
||||
return *m_zero;
|
||||
}
|
||||
|
||||
nlsat::anum_manager& am() {
|
||||
return m_nlsat->am();
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
for (auto m : m_monics) {
|
||||
out << "j" << m.var() << " = ";
|
||||
for (auto v : m.vars()) {
|
||||
out << "j" << v << " ";
|
||||
}
|
||||
out << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
solver::solver(lp::lar_solver& s, reslimit& lim, params_ref const& p) {
|
||||
m_imp = alloc(imp, s, lim, p);
|
||||
return out;
|
||||
}
|
||||
};
|
||||
|
||||
solver::~solver() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
solver::solver(lp::lar_solver& s, reslimit& lim, nla::core & nla_core, params_ref const& p) {
|
||||
m_imp = alloc(imp, s, lim, p, nla_core);
|
||||
}
|
||||
|
||||
void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
|
||||
m_imp->add(v, sz, vs);
|
||||
}
|
||||
solver::~solver() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
lbool solver::check(lp::explanation& ex) {
|
||||
return m_imp->check(ex);
|
||||
}
|
||||
void solver::add_monic(lp::var_index v, unsigned sz, lp::var_index const* vs) {
|
||||
m_imp->add(v, sz, vs);
|
||||
}
|
||||
|
||||
bool solver::need_check() {
|
||||
return m_imp->need_check();
|
||||
}
|
||||
lbool solver::check(lp::explanation& ex) {
|
||||
return m_imp->check(ex);
|
||||
}
|
||||
|
||||
void solver::push() {
|
||||
m_imp->push();
|
||||
}
|
||||
bool solver::need_check() {
|
||||
return m_imp->need_check();
|
||||
}
|
||||
|
||||
void solver::pop(unsigned n) {
|
||||
m_imp->pop(n);
|
||||
}
|
||||
void solver::push() {
|
||||
m_imp->push();
|
||||
}
|
||||
|
||||
std::ostream& solver::display(std::ostream& out) const {
|
||||
return m_imp->display(out);
|
||||
}
|
||||
void solver::pop(unsigned n) {
|
||||
m_imp->pop(n);
|
||||
}
|
||||
|
||||
nlsat::anum const& solver::value(lp::var_index v) const {
|
||||
return m_imp->value(v);
|
||||
}
|
||||
std::ostream& solver::display(std::ostream& out) const {
|
||||
return m_imp->display(out);
|
||||
}
|
||||
|
||||
nlsat::anum_manager& solver::am() {
|
||||
return m_imp->am();
|
||||
}
|
||||
nlsat::anum const& solver::value(lp::var_index v) const {
|
||||
return m_imp->value(v);
|
||||
}
|
||||
|
||||
nlsat::anum_manager& solver::am() {
|
||||
return m_imp->am();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ namespace nra {
|
|||
|
||||
public:
|
||||
|
||||
solver(lp::lar_solver& s, reslimit& lim, params_ref const& p = params_ref());
|
||||
solver(lp::lar_solver& s, reslimit& lim, nla::core & nla_core, params_ref const& p = params_ref());
|
||||
|
||||
~solver();
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@
|
|||
#include "math/lp/lp_dual_simplex.h"
|
||||
#include "math/lp/indexed_value.h"
|
||||
#include "math/lp/lar_solver.h"
|
||||
#include "math/lp/nra_solver.h"
|
||||
#include "math/lp/nla_solver.h"
|
||||
#include "math/lp/lp_types.h"
|
||||
#include "math/polynomial/algebraic_numbers.h"
|
||||
|
|
@ -268,57 +267,21 @@ class theory_lra::imp {
|
|||
unsigned m_num_conflicts;
|
||||
|
||||
// non-linear arithmetic
|
||||
scoped_ptr<nra::solver> m_nra;
|
||||
scoped_ptr<nla::solver> m_nla;
|
||||
bool m_use_nra_model;
|
||||
scoped_ptr<scoped_anum> m_a1, m_a2;
|
||||
|
||||
struct switcher {
|
||||
theory_lra::imp& m_th_imp;
|
||||
scoped_ptr<nra::solver>* m_nra;
|
||||
scoped_ptr<nla::solver>* m_nla;
|
||||
bool m_use_nla;
|
||||
switcher(theory_lra::imp& i): m_th_imp(i), m_nra(nullptr), m_nla(nullptr) {
|
||||
switcher(theory_lra::imp& i): m_th_imp(i), m_nla(nullptr) {
|
||||
}
|
||||
|
||||
|
||||
bool need_check() {
|
||||
if (m_use_nla) {
|
||||
if (m_nla != nullptr)
|
||||
return (*m_nla)->need_check();
|
||||
}
|
||||
else {
|
||||
if (m_nra != nullptr)
|
||||
return (*m_nra)->need_check();
|
||||
}
|
||||
if (m_nla != nullptr)
|
||||
return (*m_nla)->need_check();
|
||||
return false;
|
||||
}
|
||||
|
||||
void push() {
|
||||
if (m_nla != nullptr)
|
||||
(*m_nla)->push();
|
||||
if (m_nra != nullptr)
|
||||
(*m_nra)->push();
|
||||
}
|
||||
|
||||
void pop(unsigned scopes) {
|
||||
if (m_nla != nullptr)
|
||||
(*m_nla)->pop(scopes);
|
||||
if (m_nra != nullptr)
|
||||
(*m_nra)->pop(scopes);
|
||||
}
|
||||
|
||||
|
||||
void add_monic(lpvar v, unsigned sz, lpvar const* vs) {
|
||||
if (m_use_nla) {
|
||||
m_th_imp.ensure_nla();
|
||||
(*m_nla)->add_monic(v, sz, vs);
|
||||
}
|
||||
else {
|
||||
m_th_imp.ensure_nra();
|
||||
(*m_nra)->add_monic(v, sz, vs);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
// integer arithmetic
|
||||
|
|
@ -339,12 +302,7 @@ class theory_lra::imp {
|
|||
imp & m_th;
|
||||
var_value_hash(imp & th):m_th(th) {}
|
||||
unsigned operator()(theory_var v) const {
|
||||
if (m_th.m_use_nra_model) {
|
||||
return m_th.is_int(v);
|
||||
}
|
||||
else {
|
||||
return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));
|
||||
}
|
||||
return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));
|
||||
}
|
||||
};
|
||||
int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
|
||||
|
|
@ -373,15 +331,39 @@ class theory_lra::imp {
|
|||
lp::lar_solver& lp(){ return *m_solver.get(); }
|
||||
const lp::lar_solver& lp() const { return *m_solver.get(); }
|
||||
|
||||
void ensure_nra() {
|
||||
if (!m_nra) {
|
||||
m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params());
|
||||
m_switcher.m_nra = &m_nra;
|
||||
for (auto const& _s : m_scopes) {
|
||||
(void)_s;
|
||||
m_nra->push();
|
||||
}
|
||||
}
|
||||
void init_solver() {
|
||||
if (m_solver) return;
|
||||
|
||||
reset_variable_values();
|
||||
m_solver = alloc(lp::lar_solver);
|
||||
|
||||
// initialize 0, 1 variables:
|
||||
get_one(true);
|
||||
get_one(false);
|
||||
get_zero(true);
|
||||
get_zero(false);
|
||||
|
||||
smt_params_helper lpar(ctx().get_params());
|
||||
lp().settings().set_resource_limit(m_resource_limit);
|
||||
lp().settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lpar.arith_simplex_strategy());
|
||||
lp().settings().bound_propagation() = BP_NONE != propagation_mode();
|
||||
lp().settings().m_enable_hnf = lpar.arith_enable_hnf();
|
||||
lp().settings().m_print_external_var_name = lpar.arith_print_ext_var_names();
|
||||
lp().set_track_pivoted_rows(lpar.arith_bprop_on_pivoted_rows());
|
||||
lp().settings().report_frequency = lpar.arith_rep_freq();
|
||||
lp().settings().print_statistics = lpar.arith_print_stats();
|
||||
|
||||
// todo : do not use m_arith_branch_cut_ratio for deciding on cheap cuts
|
||||
unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio;
|
||||
lp().set_cut_strategy(branch_cut_ratio);
|
||||
|
||||
lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
|
||||
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
|
||||
m_lia = alloc(lp::int_solver, *m_solver.get());
|
||||
get_one(true);
|
||||
get_zero(true);
|
||||
get_one(false);
|
||||
get_zero(false);
|
||||
}
|
||||
|
||||
lpvar add_const(int c, lpvar& var, bool is_int) {
|
||||
|
|
@ -410,7 +392,6 @@ class theory_lra::imp {
|
|||
void ensure_nla() {
|
||||
if (!m_nla) {
|
||||
m_nla = alloc(nla::solver, *m_solver.get());
|
||||
m_switcher.m_nla = &m_nla;
|
||||
for (auto const& _s : m_scopes) {
|
||||
(void)_s;
|
||||
m_nla->push();
|
||||
|
|
@ -667,7 +648,7 @@ class theory_lra::imp {
|
|||
}
|
||||
TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n" << vars << "\n";);
|
||||
m_solver->register_existing_terms();
|
||||
m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
|
||||
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
|
@ -973,7 +954,6 @@ public:
|
|||
m_asserted_qhead(0),
|
||||
m_assume_eq_head(0),
|
||||
m_num_conflicts(0),
|
||||
m_use_nra_model(false),
|
||||
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
|
||||
m_solver(nullptr),
|
||||
m_resource_limit(*this),
|
||||
|
|
@ -1187,7 +1167,9 @@ public:
|
|||
sc.m_not_handled = m_not_handled;
|
||||
sc.m_underspecified_lim = m_underspecified.size();
|
||||
lp().push();
|
||||
m_switcher.push();
|
||||
if (m_nla)
|
||||
m_nla->push();
|
||||
|
||||
}
|
||||
|
||||
void pop_scope_eh(unsigned num_scopes) {
|
||||
|
|
@ -1207,7 +1189,8 @@ public:
|
|||
// VERIFY(l_false != make_feasible());
|
||||
m_new_bounds.reset();
|
||||
m_to_check.reset();
|
||||
m_switcher.pop(num_scopes);
|
||||
if (m_nla)
|
||||
m_nla->pop(num_scopes);
|
||||
TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
|
||||
}
|
||||
|
||||
|
|
@ -1588,7 +1571,7 @@ public:
|
|||
}
|
||||
|
||||
void random_update() {
|
||||
if (m_use_nra_model || m_nla)
|
||||
if (m_nla)
|
||||
return;
|
||||
m_tmp_var_set.clear();
|
||||
m_tmp_var_set.resize(th.get_num_vars());
|
||||
|
|
@ -1696,13 +1679,7 @@ public:
|
|||
}
|
||||
|
||||
bool is_eq(theory_var v1, theory_var v2) {
|
||||
if (m_use_nra_model) {
|
||||
SASSERT(!m_switcher.m_use_nla);
|
||||
return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2));
|
||||
}
|
||||
else {
|
||||
return get_ivalue(v1) == get_ivalue(v2);
|
||||
}
|
||||
return get_ivalue(v1) == get_ivalue(v2);
|
||||
}
|
||||
|
||||
bool has_delayed_constraints() const {
|
||||
|
|
@ -1712,7 +1689,6 @@ public:
|
|||
final_check_status final_check_eh() {
|
||||
reset_variable_values();
|
||||
IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
|
||||
m_use_nra_model = false;
|
||||
lbool is_sat = l_true;
|
||||
SASSERT(lp().ax_is_correct());
|
||||
if (lp().get_status() != lp::lp_status::OPTIMAL) {
|
||||
|
|
@ -2140,27 +2116,6 @@ public:
|
|||
return lia_check;
|
||||
}
|
||||
|
||||
lbool check_aftermath_nra(lbool r) {
|
||||
m_a1 = alloc(scoped_anum, m_nra->am());
|
||||
m_a2 = alloc(scoped_anum, m_nra->am());
|
||||
switch (r) {
|
||||
case l_false:
|
||||
set_conflict();
|
||||
break;
|
||||
case l_true:
|
||||
m_use_nra_model = true;
|
||||
if (assume_eqs()) {
|
||||
return l_false;
|
||||
}
|
||||
break;
|
||||
case l_undef:
|
||||
TRACE("arith", tout << "nra-undef\n";);
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
nla::lemma m_lemma;
|
||||
|
||||
void false_case_of_check_nla(const nla::lemma & l) {
|
||||
|
|
@ -2196,7 +2151,10 @@ public:
|
|||
set_conflict_or_lemma(core, false);
|
||||
}
|
||||
|
||||
lbool check_aftermath_nla(lbool r, const vector<nla::lemma>& lv) {
|
||||
lbool check_nra_continue() {
|
||||
m_a1 = nullptr; m_a2 = nullptr;
|
||||
auto & lv = m_nla_lemma_vector;
|
||||
lbool r = m_nla->check(lv);
|
||||
switch (r) {
|
||||
case l_false: {
|
||||
m_stats.m_nla_lemmas += lv.size();
|
||||
|
|
@ -2217,20 +2175,13 @@ public:
|
|||
}
|
||||
|
||||
lbool check_nra() {
|
||||
m_use_nra_model = false;
|
||||
if (!m.inc()) {
|
||||
TRACE("arith", tout << "canceled\n";);
|
||||
return l_undef;
|
||||
}
|
||||
if (!m_nra && !m_nla) return l_true;
|
||||
if (!m_nla) return l_true;
|
||||
if (!m_switcher.need_check()) return l_true;
|
||||
m_a1 = nullptr; m_a2 = nullptr;
|
||||
if (m_nra) {
|
||||
m_explanation.clear();
|
||||
return check_aftermath_nra(m_nra->check(m_explanation));
|
||||
}
|
||||
vector<nla::lemma> lv;
|
||||
return check_aftermath_nla(m_nla->check(lv), lv);
|
||||
return check_nra_continue();
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -3259,7 +3210,7 @@ public:
|
|||
}
|
||||
|
||||
lp::explanation m_explanation;
|
||||
|
||||
vector<nla::lemma> m_nla_lemma_vector;
|
||||
literal_vector m_core;
|
||||
svector<enode_pair> m_eqs;
|
||||
vector<parameter> m_params;
|
||||
|
|
@ -3363,7 +3314,6 @@ public:
|
|||
}
|
||||
|
||||
void reset_eh() {
|
||||
m_use_nra_model = false;
|
||||
m_arith_eq_adapter.reset_eh();
|
||||
m_solver = nullptr;
|
||||
m_internalize_head = 0;
|
||||
|
|
@ -3385,65 +3335,14 @@ public:
|
|||
TRACE("arith", display(tout););
|
||||
}
|
||||
|
||||
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) {
|
||||
SASSERT(m_nra);
|
||||
SASSERT(m_use_nra_model);
|
||||
auto t = get_tv(v);
|
||||
if (t.is_term()) {
|
||||
|
||||
m_todo_terms.push_back(std::make_pair(t, rational::one()));
|
||||
|
||||
TRACE("arith", tout << "v" << v << " := w" << t.to_string() << "\n";
|
||||
lp().print_term(lp().get_term(t), tout) << "\n";);
|
||||
|
||||
m_nra->am().set(r, 0);
|
||||
while (!m_todo_terms.empty()) {
|
||||
rational wcoeff = m_todo_terms.back().second;
|
||||
t = m_todo_terms.back().first;
|
||||
m_todo_terms.pop_back();
|
||||
lp::lar_term const& term = lp().get_term(t);
|
||||
TRACE("arith", lp().print_term(term, tout) << "\n";);
|
||||
scoped_anum r1(m_nra->am());
|
||||
rational c1(0);
|
||||
m_nra->am().set(r1, c1.to_mpq());
|
||||
m_nra->am().add(r, r1, r);
|
||||
for (auto const & arg : term) {
|
||||
auto wi = lp().column2tv(arg.column());
|
||||
c1 = arg.coeff() * wcoeff;
|
||||
if (wi.is_term()) {
|
||||
m_todo_terms.push_back(std::make_pair(wi, c1));
|
||||
}
|
||||
else {
|
||||
m_nra->am().set(r1, c1.to_mpq());
|
||||
m_nra->am().mul(m_nra->value(wi.id()), r1, r1);
|
||||
m_nra->am().add(r1, r, r);
|
||||
}
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
return m_nra->value(t.id());
|
||||
}
|
||||
}
|
||||
|
||||
model_value_proc * mk_value(enode * n, model_generator & mg) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
expr* o = n->get_owner();
|
||||
if (m_use_nra_model) {
|
||||
anum const& an = nl_value(v, *m_a1);
|
||||
if (a.is_int(o) && !m_nra->am().is_int(an)) {
|
||||
return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o)));
|
||||
}
|
||||
return alloc(expr_wrapper_proc, a.mk_numeral(nl_value(v, *m_a1), a.is_int(o)));
|
||||
}
|
||||
else {
|
||||
rational r = get_value(v);
|
||||
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
|
||||
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
|
||||
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)));
|
||||
}
|
||||
rational r = get_value(v);
|
||||
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
|
||||
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().get_cancel_flag()));
|
||||
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, rational& val) {
|
||||
|
|
@ -3818,9 +3717,6 @@ public:
|
|||
if (m_nla) {
|
||||
m_nla->display(out);
|
||||
}
|
||||
if (m_nra) {
|
||||
m_nra->display(out);
|
||||
}
|
||||
unsigned nv = th.get_num_vars();
|
||||
for (unsigned v = 0; v < nv; ++v) {
|
||||
auto t = get_tv(v);
|
||||
|
|
|
|||
Loading…
Reference in a new issue