mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
use cone of influence reduction before calling nlsat.
This commit is contained in:
Nikolaj Bjorner
parent
e2db2b864b
commit
20c54048f7
6 changed files with 323 additions and 138 deletions
|
|
@ -1549,7 +1549,6 @@ lbool core::check() {
|
|||
lbool ret = l_undef;
|
||||
bool run_grobner = need_run_grobner();
|
||||
bool run_horner = need_run_horner();
|
||||
bool run_bounded_nlsat = should_run_bounded_nlsat();
|
||||
bool run_bounds = params().arith_nl_branching();
|
||||
|
||||
auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
|
||||
|
|
@ -1572,7 +1571,7 @@ lbool core::check() {
|
|||
return l_false;
|
||||
}
|
||||
|
||||
if (no_effect() && run_bounded_nlsat)
|
||||
if (no_effect() && should_run_bounded_nlsat())
|
||||
ret = bounded_nlsat();
|
||||
|
||||
if (no_effect())
|
||||
|
|
@ -1582,8 +1581,7 @@ lbool core::check() {
|
|||
m_basics.basic_lemma(false);
|
||||
|
||||
if (no_effect())
|
||||
m_divisions.check();
|
||||
|
||||
m_divisions.check();
|
||||
|
||||
if (no_effect() && ret == l_undef) {
|
||||
std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
|
||||
|
|
@ -1610,7 +1608,6 @@ lbool core::check() {
|
|||
ret = l_false;
|
||||
|
||||
lp_settings().stats().m_nla_lemmas += m_lemmas.size();
|
||||
|
||||
|
||||
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
|
||||
IF_VERBOSE(5, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
|
||||
|
|
@ -1623,7 +1620,7 @@ bool core::should_run_bounded_nlsat() {
|
|||
return false;
|
||||
if (m_nlsat_delay > 0)
|
||||
--m_nlsat_delay;
|
||||
return m_nlsat_delay < 5;
|
||||
return m_nlsat_delay < 2;
|
||||
}
|
||||
|
||||
lbool core::bounded_nlsat() {
|
||||
|
|
|
|||
|
|
@ -50,10 +50,10 @@ namespace nla {
|
|||
return;
|
||||
}
|
||||
|
||||
|
||||
lp_settings().stats().m_grobner_calls++;
|
||||
find_nl_cluster();
|
||||
configure();
|
||||
if (!configure())
|
||||
return;
|
||||
m_solver.saturate();
|
||||
|
||||
if (m_delay_base > 0)
|
||||
|
|
@ -89,15 +89,14 @@ namespace nla {
|
|||
|
||||
IF_VERBOSE(3, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
|
||||
IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
|
||||
}
|
||||
|
||||
|
||||
#if 0
|
||||
// diagnostics: did we miss something
|
||||
vector<dd::pdd> eqs;
|
||||
for (auto eq : m_solver.equations())
|
||||
eqs.push_back(eq->poly());
|
||||
c().m_nra.check(eqs);
|
||||
#endif
|
||||
dd::solver::equation_vector const& grobner::core_equations(bool all_eqs) {
|
||||
flet<bool> _add_all(m_add_all_eqs, all_eqs);
|
||||
find_nl_cluster();
|
||||
if (!configure())
|
||||
throw dd::pdd_manager::mem_out();
|
||||
return m_solver.equations();
|
||||
}
|
||||
|
||||
bool grobner::is_conflicting() {
|
||||
|
|
@ -220,7 +219,7 @@ namespace nla {
|
|||
return true;
|
||||
}
|
||||
|
||||
void grobner::explain(const dd::solver::equation& eq, lp::explanation& exp) {
|
||||
void grobner::explain(dd::solver::equation const& eq, lp::explanation& exp) {
|
||||
u_dependency_manager dm;
|
||||
vector<unsigned, false> lv;
|
||||
dm.linearize(eq.dep(), lv);
|
||||
|
|
@ -235,7 +234,7 @@ namespace nla {
|
|||
lemma &= exp;
|
||||
}
|
||||
|
||||
void grobner::configure() {
|
||||
bool grobner::configure() {
|
||||
m_solver.reset();
|
||||
try {
|
||||
set_level2var();
|
||||
|
|
@ -253,12 +252,12 @@ namespace nla {
|
|||
add_fixed_monic(j);
|
||||
}
|
||||
}
|
||||
catch (...) {
|
||||
catch (dd::pdd_manager::mem_out) {
|
||||
IF_VERBOSE(2, verbose_stream() << "pdd throw\n");
|
||||
return;
|
||||
return false;
|
||||
}
|
||||
TRACE("grobner", m_solver.display(tout));
|
||||
|
||||
|
||||
#if 0
|
||||
IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
|
||||
dd::pdd_eval eval(m_pdd_manager);
|
||||
|
|
@ -282,6 +281,8 @@ namespace nla {
|
|||
m_solver.set(cfg);
|
||||
m_solver.adjust_cfg();
|
||||
m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
|
||||
|
|
@ -389,8 +390,8 @@ namespace nla {
|
|||
for (auto const& m : c().emons())
|
||||
m_mon2var[m.vars()] = m.var();
|
||||
for (auto eq : m_solver.equations())
|
||||
if (propagate_linear_equations(*eq) && ++changed >= m_solver.number_of_conflicts_to_report())
|
||||
return true;
|
||||
if (propagate_linear_equations(*eq))
|
||||
++changed;
|
||||
return changed > 0;
|
||||
}
|
||||
|
||||
|
|
@ -430,7 +431,7 @@ namespace nla {
|
|||
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
|
||||
term_index = c().lra.map_term_index_to_column_index(term_index);
|
||||
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, offset, e.dep());
|
||||
c().m_check_feasible = true;
|
||||
c().m_check_feasible = true;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -455,11 +456,16 @@ namespace nla {
|
|||
continue;
|
||||
m_rows.insert(row);
|
||||
unsigned k = lra.get_base_column_in_row(row);
|
||||
if (lra.column_is_free(k) && k != j)
|
||||
// grobner bassis does not know about integer constraints
|
||||
if (lra.column_is_free(k) && !m_add_all_eqs && k != j)
|
||||
continue;
|
||||
// a free column over the reals can be assigned
|
||||
if (lra.column_is_free(k) && k != j && !lra.var_is_int(k))
|
||||
continue;
|
||||
CTRACE("grobner", matrix.m_rows[row].size() > c().params().arith_nl_grobner_row_length_limit(),
|
||||
tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";);
|
||||
if (matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
|
||||
tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";);
|
||||
// limits overhead of grobner equations, unless this is for extracting a complete COI of the non-satisfied subset.
|
||||
if (!m_add_all_eqs && matrix.m_rows[row].size() > c().params().arith_nl_horner_row_length_limit())
|
||||
continue;
|
||||
for (auto& rc : matrix.m_rows[row])
|
||||
add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
|
||||
|
|
@ -585,7 +591,6 @@ namespace nla {
|
|||
add_eq(sum, dep);
|
||||
}
|
||||
|
||||
|
||||
void grobner::find_nl_cluster() {
|
||||
prepare_rows_and_active_vars();
|
||||
svector<lpvar> q;
|
||||
|
|
|
|||
|
|
@ -26,6 +26,7 @@ namespace nla {
|
|||
unsigned m_quota = 0;
|
||||
unsigned m_delay_base = 0;
|
||||
unsigned m_delay = 0;
|
||||
bool m_add_all_eqs = false;
|
||||
std::unordered_map<unsigned_vector, lpvar, hash_svector> m_mon2var;
|
||||
|
||||
lp::lp_settings& lp_settings();
|
||||
|
|
@ -58,7 +59,7 @@ namespace nla {
|
|||
bool equation_is_true(dd::solver::equation const& eq);
|
||||
|
||||
// setup
|
||||
void configure();
|
||||
bool configure();
|
||||
void set_level2var();
|
||||
void find_nl_cluster();
|
||||
void prepare_rows_and_active_vars();
|
||||
|
|
@ -76,5 +77,6 @@ namespace nla {
|
|||
public:
|
||||
grobner(core *core);
|
||||
void operator()();
|
||||
dd::solver::equation_vector const& core_equations(bool all_eqs);
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,17 +19,17 @@ typedef nla::mon_eq mon_eq;
|
|||
|
||||
typedef nla::variable_map_type variable_map_type;
|
||||
struct solver::imp {
|
||||
lp::lar_solver& s;
|
||||
lp::lar_solver& lra;
|
||||
reslimit& m_limit;
|
||||
params_ref m_params;
|
||||
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
|
||||
indexed_uint_set m_term_set;
|
||||
indexed_uint_set m_term_set;
|
||||
scoped_ptr<nlsat::solver> m_nlsat;
|
||||
scoped_ptr<scoped_anum> m_zero;
|
||||
mutable variable_map_type m_variable_values; // current model
|
||||
nla::core& m_nla_core;
|
||||
scoped_ptr<scoped_anum_vector> m_values; // values provided by LRA solver
|
||||
nla::core& m_nla_core;
|
||||
|
||||
imp(lp::lar_solver& s, reslimit& lim, params_ref const& p, nla::core& nla_core):
|
||||
s(s),
|
||||
lra(s),
|
||||
m_limit(lim),
|
||||
m_params(p),
|
||||
m_nla_core(nla_core) {}
|
||||
|
|
@ -38,6 +38,68 @@ struct solver::imp {
|
|||
return m_nla_core.m_to_refine.size() != 0;
|
||||
}
|
||||
|
||||
indexed_uint_set m_mon_set, m_constraint_set;
|
||||
|
||||
struct occurs {
|
||||
unsigned_vector constraints;
|
||||
unsigned_vector monics;
|
||||
};
|
||||
|
||||
void init_cone_of_influence() {
|
||||
indexed_uint_set visited;
|
||||
unsigned_vector todo;
|
||||
vector<occurs> var2occurs;
|
||||
m_term_set.reset();
|
||||
m_mon_set.reset();
|
||||
m_constraint_set.reset();
|
||||
|
||||
for (auto ci : lra.constraints().indices()) {
|
||||
auto const& c = lra.constraints()[ci];
|
||||
for (auto const& [coeff, v] : c.coeffs()) {
|
||||
var2occurs.reserve(v + 1);
|
||||
var2occurs[v].constraints.push_back(ci);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto const& m : m_nla_core.emons()) {
|
||||
for (auto v : m.vars()) {
|
||||
var2occurs.reserve(v + 1);
|
||||
var2occurs[v].monics.push_back(m.var());
|
||||
}
|
||||
}
|
||||
|
||||
for (auto const& m : m_nla_core.m_to_refine)
|
||||
todo.push_back(m);
|
||||
|
||||
for (unsigned i = 0; i < todo.size(); ++i) {
|
||||
auto v = todo[i];
|
||||
if (visited.contains(v))
|
||||
continue;
|
||||
visited.insert(v);
|
||||
var2occurs.reserve(v + 1);
|
||||
for (auto ci : var2occurs[v].constraints) {
|
||||
m_constraint_set.insert(ci);
|
||||
auto const& c = lra.constraints()[ci];
|
||||
for (auto const& [coeff, w] : c.coeffs())
|
||||
todo.push_back(w);
|
||||
}
|
||||
for (auto w : var2occurs[v].monics)
|
||||
todo.push_back(w);
|
||||
|
||||
if (lra.column_corresponds_to_term(v)) {
|
||||
m_term_set.insert(v);
|
||||
lp::tv ti = lp::tv::raw(lra.column_to_reported_index(v));
|
||||
for (auto kv : lra.get_term(ti))
|
||||
todo.push_back(kv.column().index());
|
||||
}
|
||||
|
||||
if (m_nla_core.is_monic_var(v)) {
|
||||
m_mon_set.insert(v);
|
||||
for (auto w : m_nla_core.emons()[v])
|
||||
todo.push_back(w);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief one-shot nlsat check.
|
||||
|
|
@ -52,24 +114,25 @@ struct solver::imp {
|
|||
*/
|
||||
lbool check() {
|
||||
SASSERT(need_check());
|
||||
m_zero = nullptr;
|
||||
m_values = nullptr;
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_values = alloc(scoped_anum_vector, am());
|
||||
m_term_set.reset();
|
||||
m_lp2nl.reset();
|
||||
vector<nlsat::assumption, false> core;
|
||||
|
||||
init_cone_of_influence();
|
||||
// add linear inequalities from lra_solver
|
||||
for (lp::constraint_index ci : s.constraints().indices()) {
|
||||
for (auto ci : m_constraint_set)
|
||||
add_constraint(ci);
|
||||
}
|
||||
|
||||
|
||||
// add polynomial definitions.
|
||||
for (auto const& m : m_nla_core.emons())
|
||||
add_monic_eq(m);
|
||||
for (auto const& m : m_mon_set)
|
||||
add_monic_eq(m_nla_core.emons()[m]);
|
||||
|
||||
// add term definitions.
|
||||
for (unsigned i : m_term_set)
|
||||
add_term(i);
|
||||
// TBD: add variable bounds?
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
|
|
@ -86,12 +149,27 @@ struct solver::imp {
|
|||
TRACE("nra",
|
||||
m_nlsat->display(tout << r << "\n");
|
||||
display(tout);
|
||||
for (auto kv : m_lp2nl)
|
||||
tout << "j" << kv.m_key << " := x" << kv.m_value << "\n";
|
||||
for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";
|
||||
);
|
||||
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)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
|
||||
lra.constraints().display(verbose_stream()));
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
}
|
||||
for (auto const& m : m_nla_core.emons()) {
|
||||
if (!check_monic(m)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
|
||||
lra.constraints().display(verbose_stream()));
|
||||
UNREACHABLE();
|
||||
return l_undef;
|
||||
}
|
||||
}
|
||||
break;
|
||||
case l_false: {
|
||||
lp::explanation ex;
|
||||
|
|
@ -112,12 +190,31 @@ struct solver::imp {
|
|||
return r;
|
||||
}
|
||||
|
||||
void add_monic_eq_bound(mon_eq const& m) {
|
||||
if (!lra.column_has_lower_bound(m.var()) &&
|
||||
!lra.column_has_upper_bound(m.var()))
|
||||
return;
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
svector<polynomial::var> vars;
|
||||
for (auto v : m.vars())
|
||||
vars.push_back(lp2nl(v));
|
||||
auto v = m.var();
|
||||
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.data()), pm);
|
||||
polynomial::monomial * mls[1] = { m1 };
|
||||
polynomial::scoped_numeral_vector coeffs(pm.m());
|
||||
coeffs.push_back(mpz(1));
|
||||
polynomial::polynomial_ref p(pm.mk_polynomial(1, coeffs.data(), mls), pm);
|
||||
if (lra.column_has_lower_bound(v))
|
||||
add_lb(lra.get_lower_bound(v), p, lra.get_column_lower_bound_witness(v));
|
||||
if (lra.column_has_upper_bound(v))
|
||||
add_ub(lra.get_upper_bound(v), p, lra.get_column_upper_bound_witness(v));
|
||||
}
|
||||
|
||||
void add_monic_eq(mon_eq const& m) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
svector<polynomial::var> vars;
|
||||
for (auto v : m.vars()) {
|
||||
for (auto v : m.vars())
|
||||
vars.push_back(lp2nl(v));
|
||||
}
|
||||
polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.data()), pm);
|
||||
polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.var()), 1), pm);
|
||||
polynomial::monomial * mls[2] = { m1, m2 };
|
||||
|
|
@ -132,7 +229,7 @@ struct solver::imp {
|
|||
}
|
||||
|
||||
void add_constraint(unsigned idx) {
|
||||
auto& c = s.constraints()[idx];
|
||||
auto& c = lra.constraints()[idx];
|
||||
auto& pm = m_nlsat->pm();
|
||||
auto k = c.kind();
|
||||
auto rhs = c.rhs();
|
||||
|
|
@ -140,9 +237,9 @@ struct solver::imp {
|
|||
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));
|
||||
for (auto [coeff, v] : lhs) {
|
||||
vars.push_back(lp2nl(v));
|
||||
den = lcm(den, denominator(coeff));
|
||||
}
|
||||
vector<rational> coeffs;
|
||||
for (auto kv : lhs) {
|
||||
|
|
@ -176,21 +273,128 @@ struct solver::imp {
|
|||
m_nlsat->mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
bool check_monic(mon_eq const& m) {
|
||||
scoped_anum val1(am()), val2(am());
|
||||
am().set(val1, value(m.var()));
|
||||
am().set(val2, rational::one().to_mpq());
|
||||
for (auto v : m.vars())
|
||||
am().mul(val2, value(v), val2);
|
||||
return am().eq(val1, val2);
|
||||
}
|
||||
|
||||
bool check_constraint(unsigned idx) {
|
||||
auto& c = lra.constraints()[idx];
|
||||
auto& pm = m_nlsat->pm();
|
||||
auto k = c.kind();
|
||||
auto offset = -c.rhs();
|
||||
auto lhs = c.coeffs();
|
||||
auto sz = lhs.size();
|
||||
|
||||
scoped_anum val(am()), mon(am());
|
||||
am().set(val, offset.to_mpq());
|
||||
for (auto [coeff, v] : lhs) {
|
||||
am().set(mon, coeff.to_mpq());
|
||||
am().mul(mon, value(v), mon);
|
||||
am().add(val, mon, val);
|
||||
}
|
||||
am().set(mon, rational::zero().to_mpq());
|
||||
switch (k) {
|
||||
case lp::lconstraint_kind::LE:
|
||||
return am().le(val, mon);
|
||||
case lp::lconstraint_kind::GE:
|
||||
return am().ge(val, mon);
|
||||
case lp::lconstraint_kind::LT:
|
||||
return am().lt(val, mon);
|
||||
case lp::lconstraint_kind::GT:
|
||||
return am().gt(val, mon);
|
||||
case lp::lconstraint_kind::EQ:
|
||||
return am().eq(val, mon);
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
lbool check(dd::solver::equation_vector const& eqs) {
|
||||
m_values = nullptr;
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_values = alloc(scoped_anum_vector, am());
|
||||
m_lp2nl.reset();
|
||||
m_term_set.reset();
|
||||
for (auto const& eq : eqs)
|
||||
add_eq(*eq);
|
||||
for (auto const& m : m_nla_core.emons())
|
||||
if (any_of(m.vars(), [&](lp::lpvar v) { return m_lp2nl.contains(v); }))
|
||||
add_monic_eq_bound(m);
|
||||
for (unsigned i : m_term_set)
|
||||
add_term(i);
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
if (lra.column_has_lower_bound(v))
|
||||
add_lb(lra.get_lower_bound(v), w, lra.get_column_lower_bound_witness(v));
|
||||
if (lra.column_has_upper_bound(v))
|
||||
add_ub(lra.get_upper_bound(v), w, lra.get_column_upper_bound_witness(v));
|
||||
}
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.is_canceled()) {
|
||||
r = l_undef;
|
||||
}
|
||||
else {
|
||||
throw;
|
||||
}
|
||||
}
|
||||
|
||||
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;
|
||||
break;
|
||||
case l_false: {
|
||||
lp::explanation ex;
|
||||
vector<nlsat::assumption, false> core;
|
||||
m_nlsat->get_core(core);
|
||||
u_dependency_manager dm;
|
||||
vector<unsigned, false> lv;
|
||||
for (auto c : core)
|
||||
dm.linearize(static_cast<u_dependency*>(c), lv);
|
||||
for (auto ci : lv)
|
||||
ex.push_back(ci);
|
||||
nla::new_lemma lemma(m_nla_core, __FUNCTION__);
|
||||
lemma &= ex;
|
||||
break;
|
||||
}
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool check(vector<dd::pdd> const& eqs) {
|
||||
m_zero = nullptr;
|
||||
m_values = nullptr;
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_values = alloc(scoped_anum_vector, am());
|
||||
m_lp2nl.reset();
|
||||
m_term_set.reset();
|
||||
for (auto const& eq : eqs)
|
||||
add_eq(eq);
|
||||
for (auto const& m : m_nla_core.emons())
|
||||
add_monic_eq(m);
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
add_lb(ls.get_lower_bound(v), w);
|
||||
if (ls.column_has_upper_bound(v))
|
||||
add_ub(ls.get_upper_bound(v), w);
|
||||
if (lra.column_has_lower_bound(v))
|
||||
add_lb(lra.get_lower_bound(v), w);
|
||||
if (lra.column_has_upper_bound(v))
|
||||
add_ub(lra.get_upper_bound(v), w);
|
||||
}
|
||||
|
||||
lbool r = l_undef;
|
||||
|
|
@ -212,63 +416,21 @@ struct solver::imp {
|
|||
IF_VERBOSE(0, verbose_stream() << "check-nra " << r << "\n";
|
||||
m_nlsat->display(verbose_stream());
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n";
|
||||
if (ls.column_has_upper_bound(v))
|
||||
verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n";
|
||||
if (lra.column_has_lower_bound(v))
|
||||
verbose_stream() << "x" << w << " >= " << lra.get_lower_bound(v) << "\n";
|
||||
if (lra.column_has_upper_bound(v))
|
||||
verbose_stream() << "x" << w << " <= " << lra.get_upper_bound(v) << "\n";
|
||||
});
|
||||
|
||||
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool check_tight(dd::pdd const& eq) {
|
||||
m_zero = nullptr;
|
||||
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
|
||||
m_zero = alloc(scoped_anum, am());
|
||||
m_lp2nl.reset();
|
||||
m_term_set.reset();
|
||||
add_eq(eq);
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
add_strict_lb(ls.get_lower_bound(v), w);
|
||||
if (ls.column_has_upper_bound(v))
|
||||
add_strict_ub(ls.get_upper_bound(v), w);
|
||||
}
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
if (m_limit.is_canceled()) {
|
||||
r = l_undef;
|
||||
}
|
||||
else {
|
||||
throw;
|
||||
}
|
||||
}
|
||||
|
||||
if (r == l_true)
|
||||
return r;
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "check-nra tight " << r << "\n";
|
||||
m_nlsat->display(verbose_stream());
|
||||
for (auto const& [v, w] : m_lp2nl) {
|
||||
auto& ls = m_nla_core.lra;
|
||||
if (ls.column_has_lower_bound(v))
|
||||
verbose_stream() << "x" << w << " >= " << ls.get_lower_bound(v) << "\n";
|
||||
if (ls.column_has_upper_bound(v))
|
||||
verbose_stream() << "x" << w << " <= " << ls.get_upper_bound(v) << "\n";
|
||||
});
|
||||
|
||||
|
||||
return r;
|
||||
void add_eq(dd::solver::equation const& eq) {
|
||||
add_eq(eq.poly(), eq.dep());
|
||||
}
|
||||
|
||||
void add_eq(dd::pdd const& eq) {
|
||||
void add_eq(dd::pdd const& eq, nlsat::assumption a = nullptr) {
|
||||
dd::pdd normeq = eq;
|
||||
rational lc(1);
|
||||
for (auto const& [c, m] : eq)
|
||||
|
|
@ -280,28 +442,35 @@ struct solver::imp {
|
|||
bool is_even[1] = { false };
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
m_nlsat->mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
void add_strict_lb(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, false, nlsat::atom::kind::GT);
|
||||
}
|
||||
void add_strict_ub(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, false, nlsat::atom::kind::LT);
|
||||
|
||||
void add_lb(lp::impq const& b, unsigned w, nlsat::assumption a = nullptr) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
polynomial::polynomial_ref p(pm.mk_polynomial(w), pm);
|
||||
add_lb(b, p, a);
|
||||
}
|
||||
|
||||
void add_lb(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, b.y <= 0, b.y > 0 ? nlsat::atom::kind::GT : nlsat::atom::kind::LT);
|
||||
void add_ub(lp::impq const& b, unsigned w, nlsat::assumption a = nullptr) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
polynomial::polynomial_ref p(pm.mk_polynomial(w), pm);
|
||||
add_ub(b, p, a);
|
||||
}
|
||||
void add_ub(lp::impq const& b, unsigned w) {
|
||||
add_bound(b.x, w, b.y >= 0, b.y < 0 ? nlsat::atom::kind::LT : nlsat::atom::kind::GT);
|
||||
|
||||
void add_lb(lp::impq const& b, polynomial::polynomial* p, nlsat::assumption a = nullptr) {
|
||||
add_bound(b.x, p, b.y <= 0, b.y > 0 ? nlsat::atom::kind::GT : nlsat::atom::kind::LT, a);
|
||||
}
|
||||
|
||||
void add_ub(lp::impq const& b, polynomial::polynomial* p, nlsat::assumption a = nullptr) {
|
||||
add_bound(b.x, p, b.y >= 0, b.y < 0 ? nlsat::atom::kind::LT : nlsat::atom::kind::GT, a);
|
||||
}
|
||||
|
||||
// w - bound < 0
|
||||
// w - bound > 0
|
||||
void add_bound(lp::mpq const& bound, unsigned w, bool neg, nlsat::atom::kind k) {
|
||||
|
||||
void add_bound(lp::mpq const& bound, polynomial::polynomial* p1, bool neg, nlsat::atom::kind k, nlsat::assumption a = nullptr) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
polynomial::polynomial_ref p1(pm.mk_polynomial(w), pm);
|
||||
polynomial::polynomial_ref p2(pm.mk_const(bound), pm);
|
||||
polynomial::polynomial_ref p(pm.sub(p1, p2), pm);
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
|
|
@ -309,7 +478,13 @@ struct solver::imp {
|
|||
nlsat::literal lit = m_nlsat->mk_ineq_literal(k, 1, ps, is_even);
|
||||
if (neg)
|
||||
lit.neg();
|
||||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
m_nlsat->mk_clause(1, &lit, a);
|
||||
}
|
||||
|
||||
void add_bound(lp::mpq const& bound, unsigned w, bool neg, nlsat::atom::kind k, nlsat::assumption a = nullptr) {
|
||||
polynomial::manager& pm = m_nlsat->pm();
|
||||
polynomial::polynomial_ref p1(pm.mk_polynomial(w), pm);
|
||||
add_bound(bound, p1, neg, k, a);
|
||||
}
|
||||
|
||||
polynomial::polynomial* pdd2polynomial(dd::pdd const& p) {
|
||||
|
|
@ -320,7 +495,7 @@ struct solver::imp {
|
|||
polynomial::polynomial_ref hi(pdd2polynomial(p.hi()), pm);
|
||||
unsigned w, v = p.var();
|
||||
if (!m_lp2nl.find(v, w)) {
|
||||
w = m_nlsat->mk_var(false);
|
||||
w = m_nlsat->mk_var(is_int(v));
|
||||
m_lp2nl.insert(v, w);
|
||||
}
|
||||
polynomial::polynomial_ref vp(pm.mk_polynomial(w, 1), pm);
|
||||
|
|
@ -329,16 +504,15 @@ struct solver::imp {
|
|||
}
|
||||
|
||||
bool is_int(lp::var_index v) {
|
||||
return s.var_is_int(v);
|
||||
return lra.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);
|
||||
if (!m_term_set.contains(v) && s.column_corresponds_to_term(v)) {
|
||||
if (!m_term_set.contains(v) && lra.column_corresponds_to_term(v)) {
|
||||
m_term_set.insert(v);
|
||||
}
|
||||
}
|
||||
|
|
@ -346,9 +520,9 @@ struct solver::imp {
|
|||
}
|
||||
//
|
||||
void add_term(unsigned term_column) {
|
||||
lp::tv ti = lp::tv::raw(s.column_to_reported_index(term_column));
|
||||
const lp::lar_term& t = s.get_term(ti);
|
||||
// code that creates a polynomial equality between the linear coefficients and
|
||||
lp::tv ti = lp::tv::raw(lra.column_to_reported_index(term_column));
|
||||
const lp::lar_term& t = lra.get_term(ti);
|
||||
// code that creates a polynomial equality between the linear coefficients and
|
||||
// variable representing the term.
|
||||
svector<polynomial::var> vars;
|
||||
rational den(1);
|
||||
|
|
@ -367,16 +541,22 @@ struct solver::imp {
|
|||
polynomial::polynomial_ref p(pm.mk_linear(coeffs.size(), coeffs.data(), vars.data(), rational(0)), pm);
|
||||
polynomial::polynomial* ps[1] = { p };
|
||||
bool is_even[1] = { false };
|
||||
nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even);
|
||||
m_nlsat->mk_clause(1, &lit, nullptr);
|
||||
}
|
||||
|
||||
nlsat::anum const& value(lp::var_index v) const {
|
||||
nlsat::anum const& value(lp::var_index v) {
|
||||
polynomial::var pv;
|
||||
if (m_lp2nl.find(v, pv))
|
||||
return m_nlsat->value(pv);
|
||||
else
|
||||
return *m_zero;
|
||||
else {
|
||||
for (unsigned w = m_values->size(); w <= v; ++w) {
|
||||
scoped_anum a(am());
|
||||
am().set(a, m_nla_core.val(w).to_mpq());
|
||||
m_values->push_back(a);
|
||||
}
|
||||
return (*m_values)[v];
|
||||
}
|
||||
}
|
||||
|
||||
nlsat::anum_manager& am() {
|
||||
|
|
@ -417,8 +597,8 @@ lbool solver::check(vector<dd::pdd> const& eqs) {
|
|||
return m_imp->check(eqs);
|
||||
}
|
||||
|
||||
lbool solver::check_tight(dd::pdd const& eq) {
|
||||
return m_imp->check_tight(eq);
|
||||
lbool solver::check(dd::solver::equation_vector const& eqs) {
|
||||
return m_imp->check(eqs);
|
||||
}
|
||||
|
||||
bool solver::need_check() {
|
||||
|
|
@ -429,7 +609,7 @@ std::ostream& solver::display(std::ostream& out) const {
|
|||
return m_imp->display(out);
|
||||
}
|
||||
|
||||
nlsat::anum const& solver::value(lp::var_index v) const {
|
||||
nlsat::anum const& solver::value(lp::var_index v) {
|
||||
return m_imp->value(v);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@
|
|||
#include "util/rlimit.h"
|
||||
#include "util/params.h"
|
||||
#include "nlsat/nlsat_solver.h"
|
||||
#include "math/grobner/pdd_solver.h"
|
||||
#include "math/dd/dd_pdd.h"
|
||||
|
||||
namespace lp {
|
||||
|
|
@ -43,9 +44,9 @@ namespace nra {
|
|||
lbool check(vector<dd::pdd> const& eqs);
|
||||
|
||||
/**
|
||||
\brief Check if equality is tight.
|
||||
\brief Check feasibility with respect to a set of reduced constraints.
|
||||
*/
|
||||
lbool check_tight(const dd::pdd& eq);
|
||||
lbool check(dd::solver::equation_vector const& eqs);
|
||||
|
||||
/*
|
||||
\brief determine whether nra check is needed.
|
||||
|
|
@ -55,7 +56,7 @@ namespace nra {
|
|||
/*
|
||||
\brief Access model.
|
||||
*/
|
||||
nlsat::anum const& value(lp::var_index v) const;
|
||||
nlsat::anum const& value(lp::var_index v);
|
||||
|
||||
nlsat::anum_manager& am();
|
||||
|
||||
|
|
|
|||
|
|
@ -78,7 +78,7 @@ def_module_params(module_name='smt',
|
|||
('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
|
||||
('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
|
||||
('arith.nl.grobner_subs_fixed', UINT, 1, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),
|
||||
('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),
|
||||
('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
|
||||
('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
|
||||
('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
|
||||
('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue