mirror of
https://github.com/Z3Prover/z3
synced 2026-02-19 23:14:40 +00:00
e4697fe18e
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation. To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
4471 lines
159 KiB
C++
4471 lines
159 KiB
C++
/*++
|
|
Copyright (c) 2016 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
theory_lra.cpp
|
|
|
|
Abstract:
|
|
|
|
<abstract>
|
|
|
|
Author:
|
|
|
|
Lev Nachmanson (levnach) 2016-25-3
|
|
Nikolaj Bjorner (nbjorner)
|
|
|
|
Revision History:
|
|
|
|
|
|
--*/
|
|
#include "util/stopwatch.h"
|
|
#include "math/lp/indexed_value.h"
|
|
#include "math/lp/lar_solver.h"
|
|
#include "math/lp/nla_solver.h"
|
|
#include "math/lp/lp_types.h"
|
|
#include "math/lp/lp_api.h"
|
|
#include "math/polynomial/algebraic_numbers.h"
|
|
#include "math/polynomial/polynomial.h"
|
|
#include "util/nat_set.h"
|
|
#include "util/optional.h"
|
|
#include "util/inf_rational.h"
|
|
#include "util/cancel_eh.h"
|
|
#include "util/scoped_timer.h"
|
|
#include "util/nat_set.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "model/numeral_factory.h"
|
|
#include "smt/smt_theory.h"
|
|
#include "smt/smt_context.h"
|
|
#include "smt/theory_lra.h"
|
|
#include "smt/smt_model_generator.h"
|
|
#include "smt/arith_eq_adapter.h"
|
|
#include "util/nat_set.h"
|
|
#include "ast/converters/generic_model_converter.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "ast/ast_ll_pp.h"
|
|
#include "util/cancel_eh.h"
|
|
#include "util/scoped_timer.h"
|
|
#include "util/distribution.h"
|
|
|
|
typedef lp::lpvar lpvar;
|
|
|
|
|
|
namespace smt {
|
|
|
|
typedef lp_api::bound<literal> api_bound;
|
|
|
|
typedef ptr_vector<api_bound> lp_bounds;
|
|
|
|
class theory_lra::imp {
|
|
|
|
struct scope {
|
|
unsigned m_bounds_lim;
|
|
unsigned m_asserted_qhead;
|
|
unsigned m_asserted_atoms_lim;
|
|
};
|
|
|
|
struct delayed_atom {
|
|
unsigned m_bv;
|
|
bool m_is_true;
|
|
delayed_atom(unsigned b, bool t): m_bv(b), m_is_true(t) {}
|
|
};
|
|
|
|
class resource_limit : public lp::lp_resource_limit {
|
|
imp& m_imp;
|
|
public:
|
|
resource_limit(imp& i): m_imp(i) { }
|
|
bool get_cancel_flag() override { return !m_imp.m.inc(); }
|
|
};
|
|
|
|
theory_lra& th;
|
|
ast_manager& m;
|
|
arith_util a;
|
|
arith_eq_adapter m_arith_eq_adapter;
|
|
vector<rational> m_columns;
|
|
|
|
|
|
// temporary values kept during internalization
|
|
struct internalize_state {
|
|
expr_ref_vector m_terms;
|
|
vector<rational> m_coeffs;
|
|
svector<theory_var> m_vars;
|
|
ptr_vector<expr> m_to_ensure_enode, m_to_ensure_var;
|
|
internalize_state(ast_manager& m): m_terms(m) {}
|
|
void reset() {
|
|
m_terms.reset();
|
|
m_coeffs.reset();
|
|
m_vars.reset();
|
|
m_to_ensure_enode.reset();
|
|
m_to_ensure_var.reset();
|
|
}
|
|
};
|
|
ptr_vector<internalize_state> m_internalize_states;
|
|
unsigned m_internalize_head;
|
|
|
|
class scoped_internalize_state {
|
|
imp& m_imp;
|
|
internalize_state& m_st;
|
|
|
|
internalize_state& push_internalize(imp& i) {
|
|
if (i.m_internalize_head == i.m_internalize_states.size()) {
|
|
i.m_internalize_states.push_back(alloc(internalize_state, i.m));
|
|
}
|
|
internalize_state& st = *i.m_internalize_states[i.m_internalize_head++];
|
|
st.reset();
|
|
return st;
|
|
}
|
|
public:
|
|
scoped_internalize_state(imp& i): m_imp(i), m_st(push_internalize(i)) {}
|
|
~scoped_internalize_state() { --m_imp.m_internalize_head; }
|
|
expr_ref_vector& terms() { return m_st.m_terms; }
|
|
vector<rational>& coeffs() { return m_st.m_coeffs; }
|
|
svector<theory_var>& vars() { return m_st.m_vars; }
|
|
ptr_vector<expr>& to_ensure_enode() { return m_st.m_to_ensure_enode; }
|
|
ptr_vector<expr>& to_ensure_var() { return m_st.m_to_ensure_var; }
|
|
void push(expr* e, rational c) { m_st.m_terms.push_back(e); m_st.m_coeffs.push_back(c); }
|
|
void set_back(unsigned i) {
|
|
if (terms().size() == i + 1) return;
|
|
terms()[i] = terms().back();
|
|
coeffs()[i] = coeffs().back();
|
|
terms().pop_back();
|
|
coeffs().pop_back();
|
|
}
|
|
};
|
|
|
|
typedef vector<std::pair<rational, lpvar>> var_coeffs;
|
|
|
|
var_coeffs m_left_side; // constraint left side
|
|
lpvar m_one_var;
|
|
lpvar m_zero_var;
|
|
lpvar m_rone_var;
|
|
lpvar m_rzero_var;
|
|
|
|
enum constraint_source {
|
|
inequality_source,
|
|
equality_source,
|
|
definition_source,
|
|
null_source
|
|
};
|
|
svector<constraint_source> m_constraint_sources;
|
|
svector<literal> m_inequalities; // asserted rows corresponding to inequality literals.
|
|
svector<enode_pair> m_equalities; // asserted rows corresponding to equalities.
|
|
svector<theory_var> m_definitions; // asserted rows corresponding to definitions
|
|
|
|
svector<delayed_atom> m_asserted_atoms;
|
|
ptr_vector<expr> m_not_handled;
|
|
ptr_vector<app> m_underspecified;
|
|
ptr_vector<app> m_bv_terms;
|
|
vector<ptr_vector<api_bound> > m_use_list; // bounds where variables are used.
|
|
|
|
// attributes for incremental version:
|
|
u_map<api_bound*> m_bool_var2bound;
|
|
vector<lp_bounds> m_bounds;
|
|
unsigned_vector m_unassigned_bounds;
|
|
unsigned_vector m_bounds_trail;
|
|
unsigned m_asserted_qhead;
|
|
|
|
svector<unsigned> m_bv_to_propagate; // Boolean variables that can be propagated
|
|
|
|
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
|
|
unsigned m_assume_eq_head;
|
|
indexed_uint_set m_tmp_var_set;
|
|
|
|
unsigned m_num_conflicts;
|
|
|
|
// non-linear arithmetic
|
|
scoped_ptr<nla::solver> m_nla;
|
|
|
|
// integer arithmetic
|
|
scoped_ptr<lp::int_solver> m_lia;
|
|
|
|
// temporary lemma storage
|
|
nla::lemma m_lemma;
|
|
|
|
|
|
struct var_value_eq {
|
|
imp & m_th;
|
|
var_value_eq(imp & th):m_th(th) {}
|
|
bool operator()(theory_var v1, theory_var v2) const {
|
|
return m_th.is_int(v1) == m_th.is_int(v2) && m_th.is_eq(v1, v2);
|
|
}
|
|
};
|
|
|
|
bool use_nra_model() const {
|
|
return m_nla && m_nla->use_nra_model();
|
|
}
|
|
|
|
struct var_value_hash {
|
|
imp & m_th;
|
|
var_value_hash(imp & th):m_th(th) {}
|
|
unsigned operator()(theory_var v) const {
|
|
if (m_th.use_nra_model())
|
|
return m_th.is_int(v);
|
|
else
|
|
return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v));
|
|
}
|
|
};
|
|
int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
|
|
|
|
|
|
svector<scope> m_scopes;
|
|
lp_api::stats m_stats;
|
|
arith_factory* m_factory;
|
|
scoped_ptr<lp::lar_solver> m_solver;
|
|
resource_limit m_resource_limit;
|
|
lp_bounds m_new_bounds;
|
|
symbol m_farkas;
|
|
vector<parameter> m_bound_params;
|
|
std_vector<lp::implied_bound> m_implied_bounds;
|
|
lp::lp_bound_propagator<imp> m_bp;
|
|
|
|
context& ctx() const { return th.get_context(); }
|
|
theory_id get_id() const { return th.get_id(); }
|
|
theory_arith_params const& params() const { return ctx().get_fparams(); }
|
|
bool is_int(theory_var v) const { return is_int(get_enode(v)); }
|
|
bool is_int(enode* n) const { return a.is_int(n->get_expr()); }
|
|
bool is_real(theory_var v) const { return is_real(get_enode(v)); }
|
|
bool is_real(enode* n) const { return a.is_real(n->get_expr()); }
|
|
enode* get_enode(theory_var v) const { return th.get_enode(v); }
|
|
enode* get_enode(expr* e) const { return ctx().get_enode(e); }
|
|
expr* get_owner(theory_var v) const { return get_enode(v)->get_expr(); }
|
|
enode_pp pp(enode* n) const { return enode_pp(n, ctx()); }
|
|
enode_pp pp(theory_var v) const { return pp(get_enode(v)); }
|
|
mk_bounded_pp bpp(expr* e) { return mk_bounded_pp(e, m); }
|
|
|
|
lpvar add_const(int c, lpvar& var, bool is_int) {
|
|
if (var != UINT_MAX)
|
|
return var;
|
|
app_ref cnst(a.mk_numeral(rational(c), is_int), m);
|
|
mk_enode(cnst);
|
|
theory_var v = mk_var(cnst);
|
|
var = lp().add_var(v, is_int);
|
|
lp().push();
|
|
add_def_constraint_and_equality(var, lp::GE, rational(c));
|
|
add_def_constraint_and_equality(var, lp::LE, rational(c));
|
|
TRACE(arith, tout << "add " << cnst << ", var = " << var << "\n";);
|
|
return var;
|
|
}
|
|
|
|
lpvar get_one(bool is_int) {
|
|
return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
|
|
}
|
|
|
|
lpvar get_zero(bool is_int) {
|
|
return add_const(0, is_int ? m_zero_var : m_rzero_var, is_int);
|
|
}
|
|
|
|
void ensure_nla() {
|
|
if (!m_nla) {
|
|
m_nla = alloc(nla::solver, *m_solver.get(), ctx().get_params(), m.limit());
|
|
for (auto const& _s : m_scopes) {
|
|
(void)_s;
|
|
m_nla->push();
|
|
}
|
|
std::function<bool(lpvar)> is_relevant = [&](lpvar v) {
|
|
theory_var u = lp().local_to_external(v);
|
|
return ctx().is_relevant(th.get_enode(u));
|
|
};
|
|
m_nla->set_relevant(is_relevant);
|
|
m_nla->updt_params(ctx().get_params());
|
|
}
|
|
}
|
|
|
|
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");
|
|
m_not_handled.push_back(n);
|
|
}
|
|
|
|
void found_underspecified(expr* n) {
|
|
if (a.is_underspecified(n)) {
|
|
TRACE(arith, tout << "Unhandled: " << mk_pp(n, m) << "\n";);
|
|
ctx().push_trail(push_back_vector<ptr_vector<app>>(m_underspecified));
|
|
m_underspecified.push_back(to_app(n));
|
|
}
|
|
expr* e = nullptr, *x = nullptr, *y = nullptr;
|
|
if (a.is_div(n, x, y)) {
|
|
e = a.mk_div0(x, y);
|
|
}
|
|
else if (a.is_idiv(n, x, y)) {
|
|
e = a.mk_idiv0(x, y);
|
|
}
|
|
else if (a.is_rem(n, x, y)) {
|
|
n = a.mk_rem(x, a.mk_int(0));
|
|
e = a.mk_rem0(x, a.mk_int(0));
|
|
}
|
|
else if (a.is_mod(n, x, y)) {
|
|
n = a.mk_mod(x, a.mk_int(0));
|
|
e = a.mk_mod0(x, a.mk_int(0));
|
|
}
|
|
else if (a.is_power(n, x, y)) {
|
|
e = a.mk_power0(x, y);
|
|
}
|
|
if (e) {
|
|
literal lit = th.mk_eq(e, n, false);
|
|
ctx().mark_as_relevant(lit);
|
|
ctx().assign(lit, nullptr);
|
|
}
|
|
|
|
}
|
|
|
|
void linearize_term(expr* term, scoped_internalize_state& st) {
|
|
st.push(term, rational::one());
|
|
linearize(st);
|
|
}
|
|
|
|
void linearize_ineq(expr* lhs, expr* rhs, scoped_internalize_state& st) {
|
|
st.push(lhs, rational::one());
|
|
st.push(rhs, rational::minus_one());
|
|
linearize(st);
|
|
}
|
|
|
|
theory_var internalize_numeral(app* n, rational const& val) {
|
|
|
|
if (!ctx().e_internalized(n))
|
|
mk_enode(n);
|
|
theory_var v = mk_var(n);
|
|
lpvar vi = get_lpvar(v);
|
|
if (vi == UINT_MAX) {
|
|
vi = lp().add_var(v, a.is_int(n));
|
|
add_def_constraint_and_equality(vi, lp::GE, val);
|
|
add_def_constraint_and_equality(vi, lp::LE, val);
|
|
register_fixed_var(v, val);
|
|
}
|
|
return v;
|
|
}
|
|
|
|
|
|
void linearize(scoped_internalize_state& st) {
|
|
expr_ref_vector & terms = st.terms();
|
|
svector<theory_var>& vars = st.vars();
|
|
vector<rational>& coeffs = st.coeffs();
|
|
rational r;
|
|
expr* n1, *n2;
|
|
unsigned index = 0;
|
|
while (index < terms.size()) {
|
|
SASSERT(index >= vars.size());
|
|
expr* n = terms.get(index);
|
|
st.to_ensure_enode().push_back(n);
|
|
if (a.is_add(n)) {
|
|
for (expr* arg : *to_app(n)) {
|
|
st.push(arg, coeffs[index]);
|
|
}
|
|
st.set_back(index);
|
|
}
|
|
else if (a.is_sub(n)) {
|
|
unsigned sz = to_app(n)->get_num_args();
|
|
terms[index] = to_app(n)->get_arg(0);
|
|
for (unsigned i = 1; i < sz; ++i) {
|
|
st.push(to_app(n)->get_arg(i), -coeffs[index]);
|
|
}
|
|
}
|
|
else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n1, r)) {
|
|
coeffs[index] *= r;
|
|
terms[index] = n2;
|
|
st.to_ensure_enode().push_back(n1);
|
|
}
|
|
else if (a.is_mul(n, n1, n2) && a.is_extended_numeral(n2, r)) {
|
|
coeffs[index] *= r;
|
|
terms[index] = n1;
|
|
st.to_ensure_enode().push_back(n2);
|
|
}
|
|
else if (a.is_mul(n)) {
|
|
theory_var v = internalize_mul(to_app(n));
|
|
coeffs[vars.size()] = coeffs[index];
|
|
vars.push_back(v);
|
|
++index;
|
|
}
|
|
else if (a.is_power(n, n1, n2) && is_app(n1) && a.is_extended_numeral(n2, r) && r.is_unsigned() && r.is_pos() && r <= 10) {
|
|
theory_var v = internalize_power(to_app(n), to_app(n1), r.get_unsigned());
|
|
coeffs[vars.size()] = coeffs[index];
|
|
vars.push_back(v);
|
|
++index;
|
|
}
|
|
else if (a.is_numeral(n, r)) {
|
|
theory_var v = internalize_numeral(to_app(n), r);
|
|
coeffs[vars.size()] = coeffs[index];
|
|
vars.push_back(v);
|
|
++index;
|
|
}
|
|
else if (a.is_uminus(n, n1)) {
|
|
coeffs[index].neg();
|
|
terms[index] = n1;
|
|
}
|
|
else if (a.is_to_real(n, n1)) {
|
|
terms[index] = n1;
|
|
if (!ctx().e_internalized(n)) {
|
|
app* t = to_app(n);
|
|
VERIFY(internalize_term(to_app(n1)));
|
|
mk_enode(t);
|
|
theory_var v = mk_var(n);
|
|
theory_var w = mk_var(n1);
|
|
lpvar vj = register_theory_var_in_lar_solver(v);
|
|
lpvar wj = register_theory_var_in_lar_solver(w);
|
|
auto lu_constraints = lp().add_equality(vj, wj);
|
|
add_def_constraint(lu_constraints.first);
|
|
add_def_constraint(lu_constraints.second);
|
|
}
|
|
}
|
|
else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) {
|
|
bool is_first = !ctx().e_internalized(n);
|
|
app* t = to_app(n);
|
|
internalize_args(t);
|
|
mk_enode(t);
|
|
theory_var v = mk_var(n);
|
|
coeffs[vars.size()] = coeffs[index];
|
|
vars.push_back(v);
|
|
++index;
|
|
if (!is_first) {
|
|
// skip recursive internalization
|
|
}
|
|
else if (a.is_to_int(n, n1)) {
|
|
if (!ctx().relevancy())
|
|
mk_to_int_axiom(t);
|
|
}
|
|
else if (a.is_idiv(n, n1, n2)) {
|
|
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
|
|
app_ref mod(a.mk_mod(n1, n2), m);
|
|
ctx().internalize(mod, false);
|
|
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
|
|
if (m_nla && !a.is_numeral(n2)) {
|
|
// shortcut to create non-linear division axioms.
|
|
internalize_term(to_app(n));
|
|
internalize_term(to_app(n1));
|
|
internalize_term(to_app(n2));
|
|
theory_var q = mk_var(n);
|
|
theory_var x = mk_var(n1);
|
|
theory_var y = mk_var(n2);
|
|
m_nla->add_idivision(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y));
|
|
}
|
|
if (a.is_numeral(n2) && a.is_bounded(n1)) {
|
|
ensure_nla();
|
|
internalize_term(to_app(n));
|
|
internalize_term(to_app(n1));
|
|
internalize_term(to_app(n2));
|
|
theory_var q = mk_var(n);
|
|
theory_var x = mk_var(n1);
|
|
theory_var y = mk_var(n2);
|
|
m_nla->add_bounded_division(register_theory_var_in_lar_solver(q), register_theory_var_in_lar_solver(x), register_theory_var_in_lar_solver(y));
|
|
}
|
|
}
|
|
else if (a.is_mod(n, n1, n2)) {
|
|
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
|
|
if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);
|
|
}
|
|
else if (a.is_rem(n, n1, n2)) {
|
|
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
|
|
if (!ctx().relevancy()) mk_rem_axiom(n1, n2);
|
|
}
|
|
else if (a.is_div(n, n1, n2)) {
|
|
if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
|
|
if (!ctx().relevancy()) mk_div_axiom(n1, n2);
|
|
st.to_ensure_var().push_back(n1);
|
|
st.to_ensure_var().push_back(n2);
|
|
}
|
|
else if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2)) {
|
|
st.to_ensure_var().push_back(n1);
|
|
st.to_ensure_var().push_back(n2);
|
|
}
|
|
else if (a.is_power(n, n1, n2)) {
|
|
ensure_nla();
|
|
found_unsupported(n);
|
|
if (!ctx().relevancy()) mk_power_axiom(n, n1, n2);
|
|
st.to_ensure_var().push_back(n1);
|
|
st.to_ensure_var().push_back(n2);
|
|
}
|
|
else if (a.is_band(n) || a.is_shl(n) || a.is_ashr(n) || a.is_lshr(n)) {
|
|
m_bv_terms.push_back(to_app(n));
|
|
ctx().push_trail(push_back_vector(m_bv_terms));
|
|
mk_bv_axiom(to_app(n));
|
|
for (expr* arg : *to_app(n))
|
|
st.to_ensure_var().push_back(arg);
|
|
}
|
|
else if (!a.is_div0(n)) {
|
|
found_unsupported(n);
|
|
}
|
|
else {
|
|
// no-op
|
|
}
|
|
}
|
|
else {
|
|
if (is_app(n)) {
|
|
internalize_args(to_app(n));
|
|
}
|
|
if (m.is_ite(n)) {
|
|
if (!ctx().relevancy()) mk_ite_axiom(n);
|
|
}
|
|
theory_var v = mk_var(n);
|
|
coeffs[vars.size()] = coeffs[index];
|
|
vars.push_back(v);
|
|
++index;
|
|
}
|
|
}
|
|
for (unsigned i = st.to_ensure_enode().size(); i-- > 0; ) {
|
|
expr* n = st.to_ensure_enode()[i];
|
|
if (is_app(n)) {
|
|
mk_enode(to_app(n));
|
|
}
|
|
}
|
|
st.to_ensure_enode().reset();
|
|
for (unsigned i = st.to_ensure_var().size(); i-- > 0; ) {
|
|
expr* n = st.to_ensure_var()[i];
|
|
if (is_app(n)) {
|
|
internalize_term(to_app(n));
|
|
}
|
|
}
|
|
st.to_ensure_var().reset();
|
|
|
|
}
|
|
|
|
void internalize_args(app* t, bool force = false) {
|
|
if (!force && !reflect(t))
|
|
return;
|
|
for (expr* arg : *t) {
|
|
if (!ctx().e_internalized(arg)) {
|
|
ctx().internalize(arg, false);
|
|
}
|
|
}
|
|
}
|
|
|
|
theory_var internalize_power(app* t, app* n, unsigned p) {
|
|
internalize_args(t, true);
|
|
bool _has_var = has_var(t);
|
|
mk_enode(t);
|
|
theory_var v = mk_var(t);
|
|
if (_has_var)
|
|
return v;
|
|
VERIFY(internalize_term(n));
|
|
theory_var w = mk_var(n);
|
|
svector<lpvar> vars;
|
|
for (unsigned i = 0; i < p; ++i)
|
|
vars.push_back(register_theory_var_in_lar_solver(w));
|
|
ensure_nla();
|
|
m_solver->register_existing_terms();
|
|
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data());
|
|
return v;
|
|
}
|
|
|
|
theory_var internalize_mul(app* t) {
|
|
SASSERT(a.is_mul(t));
|
|
internalize_args(t, true);
|
|
bool _has_var = has_var(t);
|
|
mk_enode(t);
|
|
theory_var v = mk_var(t);
|
|
|
|
if (!_has_var) {
|
|
svector<lpvar> vars;
|
|
for (expr* n : *t) {
|
|
if (is_app(n)) VERIFY(internalize_term(to_app(n)));
|
|
SASSERT(ctx().e_internalized(n));
|
|
theory_var v = mk_var(n);
|
|
vars.push_back(register_theory_var_in_lar_solver(v));
|
|
}
|
|
TRACE(arith, tout << "v" << v << " := " << bpp(t) << "\n" << vars << "\n";);
|
|
m_solver->register_existing_terms();
|
|
ensure_nla();
|
|
m_nla->add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.data());
|
|
}
|
|
return v;
|
|
}
|
|
|
|
enode * mk_enode(app * n) {
|
|
TRACE(arith_verbose, tout << bpp(n) << " internalized: " << ctx().e_internalized(n) << "\n";);
|
|
if (reflect(n))
|
|
for (expr* arg : *n)
|
|
if (!ctx().e_internalized(arg))
|
|
th.ensure_enode(arg);
|
|
if (ctx().e_internalized(n)) {
|
|
return get_enode(n);
|
|
}
|
|
else {
|
|
return ctx().mk_enode(n, !reflect(n), false, enable_cgc_for(n));
|
|
}
|
|
}
|
|
|
|
bool enable_cgc_for(app * n) const {
|
|
// Congruence closure is not enabled for (+ ...) and (* ...) applications.
|
|
return !(n->get_family_id() == get_id() && (n->get_decl_kind() == OP_ADD || n->get_decl_kind() == OP_MUL));
|
|
}
|
|
|
|
|
|
void mk_clause(literal l1, literal l2, unsigned num_params, parameter * params) {
|
|
TRACE(arith, literal lits[2]; lits[0] = l1; lits[1] = l2; ctx().display_literals_verbose(tout, 2, lits); tout << "\n";);
|
|
ctx().mk_th_axiom(get_id(), l1, l2, num_params, params);
|
|
}
|
|
|
|
void mk_clause(literal l1, literal l2, literal l3, unsigned num_params, parameter * params) {
|
|
TRACE(arith, literal lits[3]; lits[0] = l1; lits[1] = l2; lits[2] = l3; ctx().display_literals_smt2(tout, 3, lits); tout << "\n";);
|
|
ctx().mk_th_axiom(get_id(), l1, l2, l3, num_params, params);
|
|
}
|
|
|
|
void mk_clause(literal l1, literal l2, literal l3, literal l4, unsigned num_params, parameter* params) {
|
|
literal clause[4] = { l1, l2, l3, l4 };
|
|
TRACE(arith, ctx().display_literals_smt2(tout, 4, clause); tout << "\n";);
|
|
ctx().mk_th_axiom(get_id(), 4, clause, num_params, params);
|
|
}
|
|
|
|
|
|
bool reflect(app* n) const {
|
|
return params().m_arith_reflect || a.is_underspecified(n);
|
|
}
|
|
|
|
bool has_var(expr* n) {
|
|
return ctx().e_internalized(n) && th.is_attached_to_var(get_enode(n));
|
|
}
|
|
|
|
void reserve_bounds(theory_var v) {
|
|
while (m_bounds.size() <= static_cast<unsigned>(v)) {
|
|
m_bounds.push_back(lp_bounds());
|
|
m_unassigned_bounds.push_back(0);
|
|
}
|
|
}
|
|
|
|
theory_var mk_var(expr* n) {
|
|
if (!ctx().e_internalized(n))
|
|
ctx().internalize(n, false);
|
|
enode* e = get_enode(n);
|
|
theory_var v;
|
|
if (th.is_attached_to_var(e))
|
|
v = e->get_th_var(get_id());
|
|
else {
|
|
v = th.mk_var(e);
|
|
SASSERT(m_bounds.size() <= static_cast<unsigned>(v) || m_bounds[v].empty());
|
|
reserve_bounds(v);
|
|
ctx().attach_th_var(e, &th, v);
|
|
}
|
|
SASSERT(null_theory_var != v);
|
|
return v;
|
|
}
|
|
|
|
bool has_int() const { return lp().has_int_var(); }
|
|
|
|
lpvar register_theory_var_in_lar_solver(theory_var v) {
|
|
lpvar lpv = lp().external_to_local(v);
|
|
if (lpv != lp::null_lpvar)
|
|
return lpv;
|
|
return lp().add_var(v, is_int(v));
|
|
}
|
|
|
|
void init_left_side(scoped_internalize_state& st) {
|
|
SASSERT(all_zeros(m_columns));
|
|
svector<theory_var> const& vars = st.vars();
|
|
vector<rational> const& coeffs = st.coeffs();
|
|
for (unsigned i = 0; i < vars.size(); ++i) {
|
|
theory_var var = vars[i];
|
|
rational const& coeff = coeffs[i];
|
|
if (m_columns.size() <= static_cast<unsigned>(var))
|
|
m_columns.setx(var, coeff, rational::zero());
|
|
else
|
|
m_columns[var] += coeff;
|
|
}
|
|
m_left_side.clear();
|
|
// reset the coefficients after they have been used.
|
|
for (unsigned i = 0; i < vars.size(); ++i) {
|
|
theory_var var = vars[i];
|
|
rational const& r = m_columns[var];
|
|
if (!r.is_zero()) {
|
|
m_left_side.push_back({r, register_theory_var_in_lar_solver(var)});
|
|
m_columns[var].reset();
|
|
}
|
|
}
|
|
SASSERT(all_zeros(m_columns));
|
|
}
|
|
|
|
bool all_zeros(vector<rational> const& v) const {
|
|
return all_of(v, [](rational const& r) { return r.is_zero(); });
|
|
}
|
|
|
|
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) {
|
|
m_constraint_sources.setx(index, equality_source, null_source);
|
|
m_equalities.setx(index, enode_pair(n1, n2), enode_pair(0, 0));
|
|
}
|
|
|
|
void add_ineq_constraint(lp::constraint_index index, literal lit) {
|
|
m_constraint_sources.setx(index, inequality_source, null_source);
|
|
m_inequalities.setx(index, lit, null_literal);
|
|
}
|
|
|
|
void add_def_constraint(lp::constraint_index index) {
|
|
m_constraint_sources.setx(index, definition_source, null_source);
|
|
m_definitions.setx(index, null_theory_var, null_theory_var);
|
|
}
|
|
|
|
void add_def_constraint(lp::constraint_index index, theory_var v) {
|
|
m_constraint_sources.setx(index, definition_source, null_source);
|
|
m_definitions.setx(index, v, null_theory_var);
|
|
}
|
|
|
|
bool is_infeasible() const {
|
|
return lp().get_status() == lp::lp_status::INFEASIBLE;
|
|
}
|
|
|
|
vector<rational> m_fixed_values;
|
|
map<rational, theory_var, rational::hash_proc, rational::eq_proc> m_value2var;
|
|
struct undo_value : public trail {
|
|
imp& s;
|
|
undo_value(imp& s):s(s) {}
|
|
void undo() override {
|
|
s.m_value2var.erase(s.m_fixed_values.back());
|
|
s.m_fixed_values.pop_back();
|
|
}
|
|
};
|
|
|
|
void register_fixed_var(theory_var v, rational const& value) {
|
|
if (m_value2var.contains(value))
|
|
return;
|
|
m_fixed_values.push_back(value);
|
|
m_value2var.insert(value, v);
|
|
ctx().push_trail(undo_value(*this));
|
|
}
|
|
|
|
void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind,
|
|
const rational& bound) {
|
|
lpvar vi_equal;
|
|
lp::constraint_index ci = lp().add_var_bound_check_on_equal(vi, kind, bound, vi_equal);
|
|
add_def_constraint(ci);
|
|
if (vi_equal != lp::null_lpvar)
|
|
report_equality_of_fixed_vars(vi, vi_equal);
|
|
m_new_def = true;
|
|
}
|
|
|
|
|
|
void del_bounds(unsigned old_size) {
|
|
for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) {
|
|
unsigned v = m_bounds_trail[i];
|
|
api_bound* b = m_bounds[v].back();
|
|
// del_use_lists(b);
|
|
dealloc(b);
|
|
m_bounds[v].pop_back();
|
|
}
|
|
m_bounds_trail.shrink(old_size);
|
|
}
|
|
|
|
void updt_unassigned_bounds(theory_var v, int inc) {
|
|
TRACE(arith_verbose, tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
|
|
ctx().push_trail(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
|
|
m_unassigned_bounds[v] += inc;
|
|
}
|
|
|
|
bool is_unit_var(scoped_internalize_state& st) {
|
|
return st.vars().size() == 1 && st.coeffs()[0].is_one();
|
|
}
|
|
|
|
|
|
theory_var internalize_def(app* term, scoped_internalize_state& st) {
|
|
TRACE(arith, tout << expr_ref(term, m) << "\n";);
|
|
if (ctx().e_internalized(term)) {
|
|
IF_VERBOSE(0, verbose_stream() << "repeated term\n";);
|
|
return mk_var(term);
|
|
}
|
|
linearize_term(term, st);
|
|
if (is_unit_var(st)) {
|
|
return st.vars()[0];
|
|
}
|
|
else {
|
|
theory_var v = mk_var(term);
|
|
SASSERT(null_theory_var != v);
|
|
st.coeffs().resize(st.vars().size() + 1);
|
|
st.coeffs()[st.vars().size()] = rational::minus_one();
|
|
st.vars().push_back(v);
|
|
return v;
|
|
}
|
|
}
|
|
|
|
// term - v = 0
|
|
theory_var internalize_def(app* term) {
|
|
scoped_internalize_state st(*this);
|
|
linearize_term(term, st);
|
|
return internalize_linearized_def(term, st);
|
|
}
|
|
|
|
lpvar get_lpvar(expr* e) {
|
|
theory_var v = mk_var(e);
|
|
m_solver->register_existing_terms();
|
|
return register_theory_var_in_lar_solver(v);
|
|
}
|
|
|
|
lpvar get_lpvar(enode* n) {
|
|
return get_lpvar(n->get_expr());
|
|
}
|
|
|
|
lpvar get_lpvar(theory_var v) const {
|
|
return v == null_theory_var ? lp::null_lpvar : lp().external_to_local(v);
|
|
}
|
|
|
|
theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) {
|
|
theory_var v = mk_var(term);
|
|
TRACE(arith_internalize, tout << "v" << v << " " << bpp(term) << "\n";);
|
|
|
|
if (is_unit_var(st) && v == st.vars()[0])
|
|
return st.vars()[0];
|
|
|
|
init_left_side(st);
|
|
lpvar vi = get_lpvar(v);
|
|
|
|
if (vi == UINT_MAX) {
|
|
if (m_left_side.empty()) {
|
|
vi = lp().add_var(v, a.is_int(term));
|
|
add_def_constraint_and_equality(vi, lp::GE, rational(0));
|
|
add_def_constraint_and_equality(vi, lp::LE, rational(0));
|
|
}
|
|
else {
|
|
vi = lp().add_term(m_left_side, v);
|
|
SASSERT(lp().column_has_term(vi));
|
|
TRACE(arith_verbose,
|
|
tout << "v" << v << " := " << mk_pp(term, m)
|
|
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n";
|
|
lp().print_term(lp().get_term(vi), tout) << "\n";);
|
|
}
|
|
}
|
|
|
|
return v;
|
|
}
|
|
|
|
|
|
public:
|
|
imp(theory_lra& th, ast_manager& m):
|
|
th(th), m(m),
|
|
a(m),
|
|
m_arith_eq_adapter(th, a),
|
|
m_internalize_head(0),
|
|
m_one_var(UINT_MAX),
|
|
m_zero_var(UINT_MAX),
|
|
m_rone_var(UINT_MAX),
|
|
m_rzero_var(UINT_MAX),
|
|
m_asserted_qhead(0),
|
|
m_assume_eq_head(0),
|
|
m_num_conflicts(0),
|
|
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
|
|
m_solver(nullptr),
|
|
m_resource_limit(*this),
|
|
m_farkas("farkas"),
|
|
m_bp(*this, m_implied_bounds),
|
|
m_bounded_range_idx(0),
|
|
m_bounded_range_lit(null_literal),
|
|
m_bound_terms(m),
|
|
m_bound_predicate(m)
|
|
{
|
|
m_bound_params.push_back(parameter(m_farkas));
|
|
m_bound_params.push_back(parameter(rational(1)));
|
|
m_bound_params.push_back(parameter(rational(1)));
|
|
|
|
}
|
|
|
|
~imp() {
|
|
del_bounds(0);
|
|
std::for_each(m_internalize_states.begin(), m_internalize_states.end(), delete_proc<internalize_state>());
|
|
}
|
|
|
|
lp::lar_solver& lp(){ return *m_solver.get(); }
|
|
const lp::lar_solver& lp() const { return *m_solver.get(); }
|
|
|
|
void init() {
|
|
if (m_solver) return;
|
|
|
|
m_model_is_initialized = false;
|
|
m_solver = alloc(lp::lar_solver);
|
|
// initialize 0, 1 variables:
|
|
get_one(true);
|
|
get_one(false);
|
|
get_zero(true);
|
|
get_zero(false);
|
|
|
|
|
|
lp().updt_params(ctx().get_params());
|
|
lp().settings().set_resource_limit(m_resource_limit);
|
|
lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode();
|
|
lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
|
|
m_lia = alloc(lp::int_solver, *m_solver.get());
|
|
}
|
|
|
|
void internalize_is_int(app * n) {
|
|
SASSERT(a.is_is_int(n));
|
|
(void) mk_enode(n);
|
|
if (!ctx().relevancy())
|
|
mk_is_int_axiom(n);
|
|
}
|
|
|
|
ptr_vector<expr> m_delay_ineqs;
|
|
unsigned m_delay_ineqs_qhead = 0;
|
|
|
|
bool internalize_atom(app * atom, bool gate_ctx) {
|
|
TRACE(arith_internalize, tout << bpp(atom) << "\n";);
|
|
SASSERT(!ctx().b_internalized(atom));
|
|
expr* n1, *n2;
|
|
rational r;
|
|
lp_api::bound_kind k;
|
|
theory_var v = null_theory_var;
|
|
bool_var bv = ctx().mk_bool_var(atom);
|
|
m_bool_var2bound.erase(bv);
|
|
ctx().set_var_theory(bv, get_id());
|
|
if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) {
|
|
v = internalize_def(to_app(n1));
|
|
k = lp_api::upper_t;
|
|
}
|
|
else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n2, r) && is_app(n1)) {
|
|
v = internalize_def(to_app(n1));
|
|
k = lp_api::lower_t;
|
|
}
|
|
else if (a.is_le(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) {
|
|
v = internalize_def(to_app(n2));
|
|
k = lp_api::lower_t;
|
|
}
|
|
else if (a.is_ge(atom, n1, n2) && a.is_extended_numeral(n1, r) && is_app(n2)) {
|
|
v = internalize_def(to_app(n2));
|
|
k = lp_api::upper_t;
|
|
}
|
|
else if (a.is_is_int(atom)) {
|
|
internalize_is_int(atom);
|
|
return true;
|
|
}
|
|
else if (a.is_le(atom) || a.is_ge(atom)) {
|
|
m_delay_ineqs.push_back(atom);
|
|
ctx().push_trail(push_back_vector<ptr_vector<expr>>(m_delay_ineqs));
|
|
return true;
|
|
}
|
|
else {
|
|
TRACE(arith, tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
|
|
found_unsupported(atom);
|
|
return true;
|
|
}
|
|
|
|
if (is_int(v) && !r.is_int())
|
|
r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
|
|
|
|
api_bound* b = mk_var_bound(bv, v, k, r);
|
|
m_bounds[v].push_back(b);
|
|
updt_unassigned_bounds(v, +1);
|
|
m_bounds_trail.push_back(v);
|
|
m_bool_var2bound.insert(bv, b);
|
|
mk_bound_axioms(*b);
|
|
TRACE(arith_internalize, tout << "Internalized " << bv << ": " << bpp(atom) << "\n";);
|
|
return true;
|
|
}
|
|
|
|
bool internalize_term(app * term) {
|
|
if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) {
|
|
// skip
|
|
}
|
|
else {
|
|
internalize_def(term);
|
|
}
|
|
return true;
|
|
}
|
|
|
|
bool is_arith(enode* n) {
|
|
return n && n->get_th_var(get_id()) != null_theory_var;
|
|
}
|
|
|
|
void internalize_eq_eh(app * atom, bool_var) {
|
|
if (!ctx().get_fparams().m_arith_eager_eq_axioms)
|
|
return;
|
|
expr* lhs = nullptr, *rhs = nullptr;
|
|
VERIFY(m.is_eq(atom, lhs, rhs));
|
|
enode * n1 = get_enode(lhs);
|
|
enode * n2 = get_enode(rhs);
|
|
|
|
if (is_arith(n1) && is_arith(n2) && n1 != n2)
|
|
m_arith_eq_adapter.mk_axioms(n1, n2);
|
|
}
|
|
|
|
void assign_eh(bool_var v, bool is_true) {
|
|
TRACE(arith, tout << "assign p" << literal(v, !is_true) << ": " << bpp(ctx().bool_var2expr(v)) << "\n";);
|
|
m_asserted_atoms.push_back(delayed_atom(v, is_true));
|
|
}
|
|
|
|
lbool get_phase(bool_var v) {
|
|
api_bound* b;
|
|
if (!m_bool_var2bound.find(v, b)) {
|
|
return l_undef;
|
|
}
|
|
lp::lconstraint_kind k = lp::EQ;
|
|
switch (b->get_bound_kind()) {
|
|
case lp_api::lower_t:
|
|
k = lp::GE;
|
|
break;
|
|
case lp_api::upper_t:
|
|
k = lp::LE;
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
auto vi = register_theory_var_in_lar_solver(b->get_var());
|
|
if (vi == lp::null_lpvar) {
|
|
return l_undef;
|
|
}
|
|
return lp().compare_values(vi, k, b->get_value()) ? l_true : l_false;
|
|
}
|
|
|
|
void initialize_value(expr* var, expr* value) {
|
|
rational r;
|
|
if (!a.is_numeral(value, r)) {
|
|
IF_VERBOSE(5, verbose_stream() << "numeric constant expected in initialization " << mk_pp(var, m) << " := " << mk_pp(value, m) << "\n");
|
|
return;
|
|
}
|
|
lp().move_lpvar_to_value(get_lpvar(var), r);
|
|
}
|
|
|
|
void new_eq_eh(theory_var v1, theory_var v2) {
|
|
TRACE(arith, tout << "eq " << v1 << " == " << v2 << "\n";);
|
|
if (!is_int(v1) && !is_real(v1))
|
|
return;
|
|
m_arith_eq_adapter.new_eq_eh(v1, v2);
|
|
}
|
|
|
|
bool use_diseqs() const {
|
|
return true;
|
|
}
|
|
|
|
void new_diseq_eh(theory_var v1, theory_var v2) {
|
|
TRACE(arith, tout << "v" << v1 << " != " << "v" << v2 << "\n";);
|
|
++m_stats.m_assert_diseq;
|
|
m_arith_eq_adapter.new_diseq_eh(v1, v2);
|
|
}
|
|
|
|
void apply_sort_cnstr(enode* n, sort*) {
|
|
TRACE(arith, tout << "sort constraint: " << pp(n) << "\n";);
|
|
#if 0
|
|
if (!th.is_attached_to_var(n))
|
|
mk_var(n->get_owner());
|
|
#endif
|
|
}
|
|
|
|
void push_scope_eh() {
|
|
m_scopes.push_back(scope());
|
|
scope& sc = m_scopes.back();
|
|
sc.m_bounds_lim = m_bounds_trail.size();
|
|
sc.m_asserted_qhead = m_asserted_qhead;
|
|
sc.m_asserted_atoms_lim = m_asserted_atoms.size();
|
|
lp().push();
|
|
if (m_nla)
|
|
m_nla->push();
|
|
}
|
|
|
|
void pop_scope_eh(unsigned num_scopes) {
|
|
if (num_scopes == 0)
|
|
return;
|
|
unsigned old_size = m_scopes.size() - num_scopes;
|
|
del_bounds(m_scopes[old_size].m_bounds_lim);
|
|
m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim);
|
|
m_asserted_qhead = m_scopes[old_size].m_asserted_qhead;
|
|
m_scopes.resize(old_size);
|
|
lp().pop(num_scopes);
|
|
// VERIFY(l_false != make_feasible());
|
|
m_new_bounds.reset();
|
|
m_bv_to_propagate.reset();
|
|
if (m_nla)
|
|
m_nla->pop(num_scopes);
|
|
TRACE(arith, tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";);
|
|
}
|
|
|
|
void restart_eh() {
|
|
m_arith_eq_adapter.restart_eh();
|
|
#if 1
|
|
// experiment
|
|
if (m_lia) {
|
|
std::function<bool(unsigned)> is_root = [&](unsigned j) {
|
|
theory_var v = lp().local_to_external(j);
|
|
if (v < 0)
|
|
return false;
|
|
auto* n = get_enode(v);
|
|
if (!th.is_relevant_and_shared(n))
|
|
return false;
|
|
if (n->is_root())
|
|
return true;
|
|
theory_var w = n->get_root()->get_th_var(get_id());
|
|
return w == v;
|
|
};
|
|
m_lia->simplify(is_root);
|
|
for (auto const& [i, j, e] : m_lia->equalities())
|
|
add_eq(i, j, e, false);
|
|
}
|
|
#endif
|
|
if (m_nla)
|
|
m_nla->simplify();
|
|
}
|
|
|
|
void relevant_eh(app* n) {
|
|
expr* n1, *n2;
|
|
if (a.is_mod(n, n1, n2))
|
|
mk_idiv_mod_axioms(n1, n2);
|
|
else if (a.is_rem(n, n1, n2))
|
|
mk_rem_axiom(n1, n2);
|
|
else if (a.is_div(n, n1, n2))
|
|
mk_div_axiom(n1, n2);
|
|
else if (a.is_to_int(n))
|
|
mk_to_int_axiom(n);
|
|
else if (a.is_is_int(n))
|
|
mk_is_int_axiom(n);
|
|
else if (m.is_ite(n))
|
|
mk_ite_axiom(n);
|
|
else if (a.is_power(n, n1, n2))
|
|
mk_power_axiom(n, n1, n2);
|
|
}
|
|
|
|
void mk_power_axiom(expr* p, expr* x, expr* y) {
|
|
rational r;
|
|
// r > 0 => r^y > 0
|
|
if (a.is_extended_numeral(x, r) && r > 0) {
|
|
expr_ref zero(a.mk_real(0), m);
|
|
mk_axiom(~mk_literal(a.mk_le(p, zero)));
|
|
}
|
|
if (a.is_extended_numeral(y, r) && r > 0) {
|
|
// r is 1/n then x >= 0 => x = p^n
|
|
if (numerator(r) == 1 && denominator(r) > 1) {
|
|
expr_ref x_ge_0(a.mk_ge(x, a.mk_real(0)), m);
|
|
expr_ref x_eq_pn(a.mk_eq(x, a.mk_power(p, a.mk_real(denominator(r)))), m);
|
|
mk_axiom(~mk_literal(x_ge_0), mk_literal(x_eq_pn));
|
|
}
|
|
}
|
|
bool can_be_underspecified = false;
|
|
if (a.is_numeral(x, r) && r == 0 && (!a.is_numeral(y, r) || r == 0))
|
|
can_be_underspecified = true;
|
|
if (!a.is_extended_numeral(x, r) &&
|
|
!a.is_extended_numeral(y, r))
|
|
can_be_underspecified = true;
|
|
if (can_be_underspecified) {
|
|
literal lit = th.mk_eq(p, a.mk_power0(x, y), false);
|
|
ctx().mark_as_relevant(lit);
|
|
ctx().assign(lit, nullptr);
|
|
}
|
|
}
|
|
|
|
// n < 0 || rem(a, n) = mod(a, n)
|
|
// !n < 0 || rem(a, n) = -mod(a, n)
|
|
void mk_rem_axiom(expr* dividend, expr* divisor) {
|
|
expr_ref zero(a.mk_int(0), m);
|
|
expr_ref rem(a.mk_rem(dividend, divisor), m);
|
|
expr_ref mod(a.mk_mod(dividend, divisor), m);
|
|
expr_ref mmod(a.mk_uminus(mod), m);
|
|
expr_ref degz_expr(a.mk_ge(divisor, zero), m);
|
|
literal dgez = mk_literal(degz_expr);
|
|
literal pos = th.mk_eq(rem, mod, false);
|
|
literal neg = th.mk_eq(rem, mmod, false);
|
|
{
|
|
scoped_trace_stream ts(th, ~dgez, pos);
|
|
mk_axiom(~dgez, pos);
|
|
}
|
|
{
|
|
scoped_trace_stream ts(th, dgez, neg);
|
|
mk_axiom( dgez, neg);
|
|
}
|
|
}
|
|
|
|
// q = 0 or q * (p div q) = p
|
|
void mk_div_axiom(expr* p, expr* q) {
|
|
if (a.is_zero(q)) return;
|
|
literal eqz = th.mk_eq(q, a.mk_real(0), false);
|
|
literal eq = th.mk_eq(a.mk_mul(q, a.mk_div(p, q)), p, false);
|
|
scoped_trace_stream ts(th, eqz, eq);
|
|
mk_axiom(eqz, eq);
|
|
}
|
|
|
|
// to_int (to_real x) = x
|
|
// to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
|
|
void mk_to_int_axiom(app* n) {
|
|
expr* x = nullptr, *y = nullptr;
|
|
VERIFY (a.is_to_int(n, x));
|
|
if (a.is_to_real(x, y)) {
|
|
literal eq = th.mk_eq(y, n, false);
|
|
scoped_trace_stream ts(th, eq);
|
|
mk_axiom(eq);
|
|
}
|
|
else {
|
|
expr_ref to_r(a.mk_to_real(n), m);
|
|
expr_ref lo(a.mk_le(a.mk_sub(to_r, x), a.mk_real(0)), m);
|
|
expr_ref hi(a.mk_ge(a.mk_sub(x, to_r), a.mk_real(1)), m);
|
|
literal llo = mk_literal(lo);
|
|
literal lhi = mk_literal(hi);
|
|
{
|
|
scoped_trace_stream ts(th, llo);
|
|
mk_axiom(llo);
|
|
}
|
|
{
|
|
scoped_trace_stream ts(th, lhi);
|
|
mk_axiom(~lhi);
|
|
}
|
|
}
|
|
}
|
|
|
|
void mk_ite_axiom(expr* n) {
|
|
return;
|
|
expr* c = nullptr, *t = nullptr, *e = nullptr;
|
|
rational b1, b2;
|
|
VERIFY(m.is_ite(n, c, t, e));
|
|
if (!a.is_numeral(t, b1) || !a.is_numeral(e, b2))
|
|
return;
|
|
auto v = mk_var(n);
|
|
auto vi = register_theory_var_in_lar_solver(v);
|
|
add_def_constraint_and_equality(vi, lp::GE, std::min(b1, b2));
|
|
add_def_constraint_and_equality(vi, lp::LE, std::max(b1, b2));
|
|
}
|
|
|
|
// is_int(x) <=> to_real(to_int(x)) = x
|
|
void mk_is_int_axiom(app* n) {
|
|
expr* x = nullptr;
|
|
VERIFY(a.is_is_int(n, x));
|
|
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
|
|
literal is_int = ctx().get_literal(n);
|
|
scoped_trace_stream _sts1(th, ~is_int, eq);
|
|
scoped_trace_stream _sts2(th, is_int, ~eq);
|
|
mk_axiom(~is_int, eq);
|
|
mk_axiom(is_int, ~eq);
|
|
|
|
}
|
|
|
|
// create axiom for
|
|
// u = v + r*w,
|
|
/// abs(r) > r >= 0
|
|
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
|
|
app_ref term(m);
|
|
term = a.mk_mul(a.mk_numeral(r, true), get_enode(w)->get_expr());
|
|
term = a.mk_add(get_enode(v)->get_expr(), term);
|
|
term = a.mk_sub(get_enode(u)->get_expr(), term);
|
|
theory_var z = internalize_def(term);
|
|
lpvar zi = register_theory_var_in_lar_solver(z);
|
|
lpvar vi = register_theory_var_in_lar_solver(v);
|
|
add_def_constraint_and_equality(zi, lp::GE, rational::zero());
|
|
add_def_constraint_and_equality(zi, lp::LE, rational::zero());
|
|
add_def_constraint_and_equality(vi, lp::GE, rational::zero());
|
|
add_def_constraint_and_equality(vi, lp::LT, abs(r));
|
|
SASSERT(!is_infeasible());
|
|
TRACE(arith, tout << term << "\n" << lp().constraints(););
|
|
}
|
|
|
|
void mk_idiv_mod_axioms(expr * p, expr * q) {
|
|
if (a.is_zero(q)) {
|
|
return;
|
|
}
|
|
TRACE(arith, tout << expr_ref(p, m) << " " << expr_ref(q, m) << "\n";);
|
|
// if q is zero, then idiv and mod are uninterpreted functions.
|
|
expr_ref div(a.mk_idiv(p, q), m);
|
|
expr_ref mod(a.mk_mod(p, q), m);
|
|
expr_ref zero(a.mk_int(0), m);
|
|
if (a.is_zero(p)) {
|
|
// q != 0 => (= (div 0 q) 0)
|
|
// q != 0 => (= (mod 0 q) 0)
|
|
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
|
|
literal q_le_0 = mk_literal(a.mk_le(q, zero));
|
|
literal d_ge_0 = mk_literal(a.mk_ge(div, zero));
|
|
literal d_le_0 = mk_literal(a.mk_le(div, zero));
|
|
literal m_ge_0 = mk_literal(a.mk_ge(mod, zero));
|
|
literal m_le_0 = mk_literal(a.mk_le(mod, zero));
|
|
mk_axiom(q_ge_0, d_ge_0);
|
|
mk_axiom(q_ge_0, d_le_0);
|
|
mk_axiom(q_ge_0, m_ge_0);
|
|
mk_axiom(q_ge_0, m_le_0);
|
|
mk_axiom(q_le_0, d_ge_0);
|
|
mk_axiom(q_le_0, d_le_0);
|
|
mk_axiom(q_le_0, m_ge_0);
|
|
mk_axiom(q_le_0, m_le_0);
|
|
return;
|
|
}
|
|
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
|
|
expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
|
|
ctx().internalize(eq_r, false);
|
|
literal eq = ctx().get_literal(eq_r);
|
|
|
|
rational k(0);
|
|
expr_ref upper(m);
|
|
|
|
if (!a.is_numeral(q, k))
|
|
;
|
|
else if (k.is_pos())
|
|
upper = a.mk_numeral(k - 1, true);
|
|
else if (k.is_neg())
|
|
upper = a.mk_numeral(-k - 1, true);
|
|
|
|
context& c = ctx();
|
|
if (!k.is_zero()) {
|
|
mk_axiom(eq);
|
|
m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
|
|
mk_axiom(mk_literal(a.mk_ge(mod, zero)));
|
|
mk_axiom(mk_literal(a.mk_le(mod, upper)));
|
|
|
|
{
|
|
std::function<void(void)> log = [&,this]() {
|
|
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_ge(mod, zero)));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)));
|
|
};
|
|
if_trace_stream _ts(m, log);
|
|
}
|
|
}
|
|
else {
|
|
|
|
expr_ref mone(a.mk_int(-1), m);
|
|
expr_ref minus_q(a.mk_mul(mone, q), m);
|
|
literal eqz = mk_literal(m.mk_eq(q, zero));
|
|
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
|
|
|
|
|
|
// q = 0 or p = (p mod q) + q * (p div q)
|
|
// q = 0 or (p mod q) >= 0
|
|
// q >= 0 or (p mod q) + q <= -1
|
|
// q <= 0 or (p mod q) - q <= -1
|
|
|
|
mk_axiom(eqz, eq);
|
|
mk_axiom(eqz, mod_ge_0);
|
|
mk_axiom(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, minus_q), mone)));
|
|
mk_axiom(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, q), mone)));
|
|
|
|
|
|
expr* x = nullptr, * y = nullptr;
|
|
if (false && !(a.is_mul(q, x, y) && mone == x))
|
|
mk_axiom(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_mul(mone, q)))));
|
|
|
|
m_arith_eq_adapter.mk_axioms(th.ensure_enode(mod_r), th.ensure_enode(p));
|
|
|
|
if (a.is_zero(p)) {
|
|
mk_axiom(eqz, mk_literal(m.mk_eq(div, zero)));
|
|
mk_axiom(eqz, mk_literal(m.mk_eq(mod, zero)));
|
|
}
|
|
// (or (= y 0) (<= (* y (div x y)) x))
|
|
else if (!a.is_numeral(q)) {
|
|
expr_ref div_ge(m);
|
|
div_ge = a.mk_ge(a.mk_sub(p, a.mk_mul(q, div)), zero);
|
|
ctx().get_rewriter()(div_ge);
|
|
mk_axiom(eqz, mk_literal(div_ge));
|
|
TRACE(arith, tout << eqz << " " << div_ge << "\n");
|
|
}
|
|
|
|
|
|
#if 0
|
|
|
|
/*literal div_ge_0 = */ mk_literal(a.mk_ge(div, zero));
|
|
/*literal div_le_0 = */ mk_literal(a.mk_le(div, zero));
|
|
/*literal p_ge_0 = */ mk_literal(a.mk_ge(p, zero));
|
|
/*literal p_le_0 = */ mk_literal(a.mk_le(p, zero));
|
|
|
|
// q >= 0 or p = (p mod q) + q * (p div q)
|
|
// q <= 0 or p = (p mod q) + q * (p div q)
|
|
// q >= 0 or (p mod q) >= 0
|
|
// q <= 0 or (p mod q) >= 0
|
|
// q <= 0 or (p mod q) < q
|
|
// q >= 0 or (p mod q) < -q
|
|
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
|
|
literal q_le_0 = mk_literal(a.mk_le(q, zero));
|
|
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
|
|
|
|
mk_axiom(q_ge_0, eq);
|
|
mk_axiom(q_le_0, eq);
|
|
mk_axiom(q_ge_0, mod_ge_0);
|
|
mk_axiom(q_le_0, mod_ge_0);
|
|
mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero)));
|
|
mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero)));
|
|
#endif
|
|
|
|
#if 0
|
|
// seem expensive
|
|
|
|
mk_axiom(q_le_0, ~p_ge_0, div_ge_0);
|
|
mk_axiom(q_le_0, ~p_le_0, div_le_0);
|
|
mk_axiom(q_ge_0, ~p_ge_0, div_le_0);
|
|
mk_axiom(q_ge_0, ~p_le_0, div_ge_0);
|
|
|
|
mk_axiom(q_le_0, p_ge_0, ~div_ge_0);
|
|
mk_axiom(q_le_0, p_le_0, ~div_le_0);
|
|
mk_axiom(q_ge_0, p_ge_0, ~div_le_0);
|
|
mk_axiom(q_ge_0, p_le_0, ~div_ge_0);
|
|
#endif
|
|
|
|
#if 0
|
|
std::function<void(void)> log = [&,this]() {
|
|
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(eq.var())));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_not(m.mk_eq(q, zero)), c.bool_var2expr(mod_ge_0.var())));
|
|
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_sub(mod, q), zero)));
|
|
th.log_axiom_unit(m.mk_implies(a.mk_lt(q, zero), a.mk_lt(a.mk_add(mod, q), zero)));
|
|
};
|
|
if_trace_stream _ts(m, log);
|
|
#endif
|
|
#if 0
|
|
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_ge_0.var())));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_gt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_le_0.var())));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_ge_0.var())), c.bool_var2expr(div_le_0.var())));
|
|
th.log_axiom_unit(m.mk_implies(m.mk_and(a.mk_lt(q, zero), c.bool_var2expr(p_le_0.var())), c.bool_var2expr(div_ge_0.var())));
|
|
#endif
|
|
}
|
|
if (params().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
|
|
unsigned _k = k.get_unsigned();
|
|
literal_buffer lits;
|
|
expr_ref_vector exprs(m);
|
|
for (unsigned j = 0; j < _k; ++j) {
|
|
literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
|
|
lits.push_back(mod_j);
|
|
exprs.push_back(c.bool_var2expr(mod_j.var()));
|
|
ctx().mark_as_relevant(mod_j);
|
|
}
|
|
scoped_trace_stream _st(th, lits);
|
|
ctx().mk_th_axiom(get_id(), lits.size(), lits.begin());
|
|
}
|
|
}
|
|
|
|
void mk_axiom(literal l) {
|
|
ctx().mk_th_axiom(get_id(), false_literal, l);
|
|
if (ctx().relevancy()) {
|
|
ctx().mark_as_relevant(l);
|
|
}
|
|
}
|
|
|
|
void mk_axiom(literal l1, literal l2) {
|
|
if (l1 == false_literal) {
|
|
mk_axiom(l2);
|
|
return;
|
|
}
|
|
mk_clause(l1, l2, 0, nullptr);
|
|
if (ctx().relevancy()) {
|
|
ctx().mark_as_relevant(l1);
|
|
ctx().add_rel_watch(~l1, ctx().bool_var2expr(l2.var())); // mark consequent as relevant if antecedent is false.
|
|
}
|
|
}
|
|
|
|
void mk_axiom(literal l1, literal l2, literal l3) {
|
|
mk_clause(l1, l2, l3, 0, nullptr);
|
|
if (ctx().relevancy()) {
|
|
ctx().mark_as_relevant(l1);
|
|
ctx().mark_as_relevant(l2);
|
|
ctx().mark_as_relevant(l3);
|
|
}
|
|
}
|
|
|
|
void mk_axiom(literal l1, literal l2, literal l3, literal l4) {
|
|
mk_clause(l1, l2, l3, l4, 0, nullptr);
|
|
if (ctx().relevancy()) {
|
|
ctx().mark_as_relevant(l1);
|
|
ctx().mark_as_relevant(l2);
|
|
ctx().mark_as_relevant(l3);
|
|
ctx().mark_as_relevant(l4);
|
|
}
|
|
}
|
|
|
|
literal mk_literal(expr* e) {
|
|
expr_ref pinned(e, m);
|
|
TRACE(mk_bool_var, tout << pinned << " " << pinned->get_id() << "\n";);
|
|
if (!ctx().e_internalized(e))
|
|
ctx().internalize(e, false);
|
|
return ctx().get_literal(e);
|
|
}
|
|
|
|
|
|
void init_search_eh() {
|
|
m_arith_eq_adapter.init_search_eh();
|
|
m_num_conflicts = 0;
|
|
}
|
|
|
|
bool can_get_value(theory_var v) const {
|
|
return is_registered_var(v) && m_model_is_initialized;
|
|
}
|
|
|
|
bool is_registered_var(theory_var v) const {
|
|
return v != null_theory_var && lp().external_is_used(v);
|
|
}
|
|
|
|
void ensure_column(enode* n) {
|
|
ensure_column(n->get_th_var(get_id()));
|
|
}
|
|
|
|
void ensure_column(theory_var v) {
|
|
if (!lp().external_is_used(v) && v != null_theory_var)
|
|
register_theory_var_in_lar_solver(v);
|
|
}
|
|
|
|
mutable vector<std::pair<lp::lpvar, rational>> m_todo_terms;
|
|
|
|
lp::impq get_ivalue(theory_var v) const {
|
|
SASSERT(is_registered_var(v));
|
|
return lp().get_column_value(get_lpvar(v));
|
|
}
|
|
|
|
rational get_value(theory_var v) const {
|
|
return is_registered_var(v) ? lp().get_value(get_lpvar(v)) : rational::zero();
|
|
}
|
|
|
|
bool m_model_is_initialized{ false };
|
|
|
|
void init_variable_values() {
|
|
m_model_is_initialized = false;
|
|
if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {
|
|
ctx().push_trail(value_trail<bool>(m_model_is_initialized));
|
|
m_model_is_initialized = lp().init_model();
|
|
TRACE(arith, display(tout << "update variable values " << m_model_is_initialized << "\n"););
|
|
}
|
|
}
|
|
|
|
void random_update() {
|
|
if (m_nla && m_nla->need_check())
|
|
return;
|
|
m_tmp_var_set.reset();
|
|
m_model_eqs.reset();
|
|
svector<lpvar> vars;
|
|
theory_var sz = static_cast<theory_var>(th.get_num_vars());
|
|
for (theory_var v = 0; v < sz; ++v) {
|
|
enode * n1 = get_enode(v);
|
|
if (!th.is_relevant_and_shared(n1)) {
|
|
continue;
|
|
}
|
|
ensure_column(v);
|
|
lp::lpvar vj = lp().external_to_local(v);
|
|
SASSERT(vj != lp::null_lpvar);
|
|
theory_var other = m_model_eqs.insert_if_not_there(v);
|
|
if (other == v) {
|
|
continue;
|
|
}
|
|
enode * n2 = get_enode(other);
|
|
if (n1->get_root() == n2->get_root())
|
|
continue;
|
|
if (!lp().column_is_fixed(vj)) {
|
|
vars.push_back(vj);
|
|
}
|
|
else if (!m_tmp_var_set.contains(other) ) {
|
|
lp::lpvar other_j = lp().external_to_local(other);
|
|
if (!lp().column_is_fixed(other_j)) {
|
|
m_tmp_var_set.insert(other);
|
|
vars.push_back(other_j);
|
|
}
|
|
}
|
|
}
|
|
TRACE(arith,
|
|
for (theory_var v = 0; v < sz; ++v)
|
|
if (th.is_relevant_and_shared(get_enode(v)))
|
|
tout << "v" << v << " ";
|
|
tout << "\n"; );
|
|
if (!vars.empty()) {
|
|
lp().random_update(vars.size(), vars.data());
|
|
}
|
|
}
|
|
|
|
bool assume_eqs() {
|
|
|
|
if (delayed_assume_eqs())
|
|
return true;
|
|
|
|
TRACE(arith_verbose, display(tout););
|
|
random_update();
|
|
m_model_eqs.reset();
|
|
|
|
theory_var sz = static_cast<theory_var>(th.get_num_vars());
|
|
unsigned old_sz = m_assume_eq_candidates.size();
|
|
unsigned num_candidates = 0;
|
|
int start = ctx().get_random_value();
|
|
for (theory_var i = 0; i < sz; ++i) {
|
|
theory_var v = (i + start) % sz;
|
|
enode* n1 = get_enode(v);
|
|
if (!th.is_relevant_and_shared(n1))
|
|
continue;
|
|
ensure_column(v);
|
|
if (!is_registered_var(v))
|
|
continue;
|
|
theory_var other = m_model_eqs.insert_if_not_there(v);
|
|
if (other == v)
|
|
continue;
|
|
enode* n2 = get_enode(other);
|
|
if (n1->get_root() == n2->get_root())
|
|
continue;
|
|
m_assume_eq_candidates.push_back({v, other});
|
|
num_candidates++;
|
|
}
|
|
|
|
if (num_candidates > 0)
|
|
ctx().push_trail(restore_vector(m_assume_eq_candidates, old_sz));
|
|
|
|
return delayed_assume_eqs();
|
|
}
|
|
|
|
bool delayed_assume_eqs() {
|
|
if (m_assume_eq_head == m_assume_eq_candidates.size())
|
|
return false;
|
|
|
|
ctx().push_trail(value_trail<unsigned>(m_assume_eq_head));
|
|
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
|
|
auto const [v1, v2] = m_assume_eq_candidates[m_assume_eq_head];
|
|
enode* n1 = get_enode(v1);
|
|
enode* n2 = get_enode(v2);
|
|
m_assume_eq_head++;
|
|
CTRACE(arith,
|
|
is_eq(v1, v2) && n1->get_root() != n2->get_root(),
|
|
tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";);
|
|
if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) {
|
|
++m_stats.m_assume_eqs;
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool is_eq(theory_var v1, theory_var v2) {
|
|
if (use_nra_model())
|
|
return m_nla->am().eq(nl_value(v1, m_nla->tmp1()), nl_value(v2, m_nla->tmp2()));
|
|
else
|
|
return get_ivalue(v1) == get_ivalue(v2);
|
|
}
|
|
|
|
bool has_delayed_constraints() const {
|
|
return !m_asserted_atoms.empty();
|
|
}
|
|
|
|
final_check_status eval_power(expr* e) {
|
|
expr* x = nullptr, * y = nullptr;
|
|
rational r;
|
|
VERIFY(a.is_power(e, x, y));
|
|
if (a.is_numeral(x, r) && r == 0 && a.is_numeral(y, r) && r == 0)
|
|
return FC_DONE;
|
|
if (!m_nla)
|
|
return FC_GIVEUP;
|
|
switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y))) {
|
|
case l_true:
|
|
return FC_DONE;
|
|
case l_false:
|
|
add_lemmas();
|
|
return FC_CONTINUE;
|
|
case l_undef:
|
|
return FC_GIVEUP;
|
|
default:
|
|
break;
|
|
}
|
|
return FC_GIVEUP;
|
|
}
|
|
|
|
final_check_status eval_unsupported(expr* e) {
|
|
if (a.is_power(e))
|
|
return eval_power(e);
|
|
if (a.is_power0(e))
|
|
return FC_DONE;
|
|
return FC_GIVEUP;
|
|
}
|
|
|
|
/**
|
|
* Check if a set of equalities are lp feasible.
|
|
* push local scope
|
|
* internalize ineqs
|
|
* assert ineq constraints
|
|
* check lp feasibility
|
|
* extract core
|
|
* pop local scope
|
|
* return verdict
|
|
*/
|
|
|
|
lbool check_lp_feasible(vector<std::pair<bool, expr_ref>> &ineqs, literal_vector& lit_core, enode_pair_vector& eq_core) {
|
|
lbool st = l_undef;
|
|
push_scope_eh(); // pushes an arithmetic scope
|
|
u_map<unsigned> ci2index;
|
|
unsigned index = 0;
|
|
for (auto &[in_core, f] : ineqs) {
|
|
expr *x, *y;
|
|
rational r;
|
|
in_core = false;
|
|
if (m.is_eq(f, x, y) && a.is_numeral(y, r)) {
|
|
internalize_term(to_app(x));
|
|
auto j = get_lpvar(th.get_th_var(x));
|
|
auto ci = lp().add_var_bound(j, lp::EQ, r);
|
|
ci2index.insert(ci, index);
|
|
lp().activate(ci);
|
|
if (is_infeasible()) {
|
|
st = l_false;
|
|
break;
|
|
}
|
|
}
|
|
else {
|
|
NOT_IMPLEMENTED_YET();
|
|
}
|
|
++index;
|
|
}
|
|
if (st != l_false) {
|
|
st = make_feasible();
|
|
SASSERT(st != l_false || is_infeasible());
|
|
}
|
|
if (st == l_false) {
|
|
m_explanation.clear();
|
|
lp().get_infeasibility_explanation(m_explanation);
|
|
for (auto ev : m_explanation) {
|
|
unsigned index;
|
|
if (ci2index.find(ev.ci(), index))
|
|
ineqs[index].first = true;
|
|
else
|
|
set_evidence(ev.ci(), lit_core, eq_core);
|
|
}
|
|
}
|
|
pop_scope_eh(1);
|
|
return st;
|
|
}
|
|
|
|
final_check_status final_check_eh(unsigned level) {
|
|
if (propagate_core())
|
|
return FC_CONTINUE;
|
|
m_model_is_initialized = false;
|
|
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
|
|
lbool is_sat = l_true;
|
|
SASSERT(lp().ax_is_correct());
|
|
if (!lp().is_feasible() || lp().has_changed_columns())
|
|
is_sat = make_feasible();
|
|
final_check_status st = FC_DONE;
|
|
bool int_undef = false;
|
|
switch (is_sat) {
|
|
case l_true:
|
|
TRACE(arith, display(tout));
|
|
|
|
switch (check_lia()) {
|
|
case FC_DONE:
|
|
break;
|
|
case FC_CONTINUE:
|
|
return FC_CONTINUE;
|
|
case FC_GIVEUP:
|
|
int_undef = true;
|
|
TRACE(arith, tout << "check-lia giveup\n";);
|
|
if (ctx().get_fparams().m_arith_ignore_int)
|
|
st = FC_CONTINUE;
|
|
break;
|
|
}
|
|
|
|
switch (check_nla(level)) {
|
|
case FC_DONE:
|
|
break;
|
|
case FC_CONTINUE:
|
|
return FC_CONTINUE;
|
|
case FC_GIVEUP:
|
|
TRACE(arith, tout << "check-nra giveup\n";);
|
|
st = FC_GIVEUP;
|
|
break;
|
|
}
|
|
|
|
if (assume_eqs()) {
|
|
++m_stats.m_assume_eqs;
|
|
return FC_CONTINUE;
|
|
}
|
|
|
|
if (!int_undef && !check_bv_terms())
|
|
return FC_CONTINUE;
|
|
|
|
if (!m_not_handled.empty())
|
|
init_variable_values();
|
|
for (expr* e : m_not_handled) {
|
|
if (!ctx().is_relevant(e))
|
|
continue;
|
|
switch (eval_unsupported(e)) {
|
|
case FC_CONTINUE:
|
|
st = FC_CONTINUE;
|
|
break;
|
|
case FC_GIVEUP:
|
|
TRACE(arith, tout << "give up " << mk_pp(e, m) << "\n");
|
|
if (st != FC_CONTINUE)
|
|
st = FC_GIVEUP;
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
if (st == FC_CONTINUE)
|
|
break;
|
|
}
|
|
return st;
|
|
case l_false:
|
|
get_infeasibility_explanation_and_set_conflict();
|
|
return FC_CONTINUE;
|
|
case l_undef:
|
|
TRACE(arith, tout << "check feasible is undef\n";);
|
|
return m.inc() ? FC_CONTINUE : FC_GIVEUP;
|
|
default:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
TRACE(arith, tout << "default giveup\n";);
|
|
return FC_GIVEUP;
|
|
}
|
|
|
|
// create an eq atom representing "term = offset"
|
|
app_ref mk_eq(lp::lar_term const& term, rational const& offset) {
|
|
u_map<rational> coeffs;
|
|
term2coeffs(term, coeffs);
|
|
bool isint = offset.is_int();
|
|
for (auto const& kv : coeffs) isint &= is_int(kv.m_key) && kv.m_value.is_int();
|
|
app_ref t = coeffs2app(coeffs, rational::zero(), isint);
|
|
app_ref s(a.mk_numeral(offset, isint), m);
|
|
if (s == t) {
|
|
return app_ref(m.mk_true(), m);
|
|
}
|
|
else {
|
|
app_ref atom(m.mk_eq(t, s), m);
|
|
ctx().internalize(atom, true);
|
|
ctx().mark_as_relevant(atom.get());
|
|
return atom;
|
|
}
|
|
}
|
|
// create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false
|
|
expr_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) {
|
|
rational offset;
|
|
expr_ref t(m);
|
|
return mk_bound(term, k, lower_bound, offset, t);
|
|
}
|
|
|
|
expr_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound, rational& offset, expr_ref& t) {
|
|
offset = k;
|
|
u_map<rational> coeffs;
|
|
term2coeffs(term, coeffs);
|
|
bool is_int = true;
|
|
rational lc = denominator(k);
|
|
for (auto const& kv : coeffs) {
|
|
theory_var w = kv.m_key;
|
|
expr* o = get_enode(w)->get_expr();
|
|
is_int = a.is_int(o);
|
|
if (!is_int) break;
|
|
lc = lcm(lc, denominator(kv.m_value));
|
|
}
|
|
|
|
// ensure that coefficients are integers when all variables are integers as well.
|
|
if (is_int && !lc.is_one()) {
|
|
SASSERT(lc.is_pos());
|
|
offset *= lc;
|
|
for (auto& kv : coeffs) kv.m_value *= lc;
|
|
}
|
|
|
|
if (is_int) {
|
|
// 3x + 6y >= 5 -> x + 3y >= 5/3, then x + 3y >= 2
|
|
// 3x + 6y <= 5 -> x + 3y <= 1
|
|
rational g = gcd_reduce(coeffs);
|
|
if (!g.is_one()) {
|
|
if (lower_bound) {
|
|
TRACE(arith, tout << "lower: " << offset << " / " << g << " = " << offset / g << " >= " << ceil(offset / g) << "\n";);
|
|
offset = ceil(offset / g);
|
|
}
|
|
else {
|
|
TRACE(arith, tout << "upper: " << offset << " / " << g << " = " << offset / g << " <= " << floor(offset / g) << "\n";);
|
|
offset = floor(offset / g);
|
|
}
|
|
}
|
|
}
|
|
if (!coeffs.empty() && coeffs.begin()->m_value.is_neg()) {
|
|
offset.neg();
|
|
lower_bound = !lower_bound;
|
|
for (auto& kv : coeffs) kv.m_value.neg();
|
|
}
|
|
|
|
// CTRACE(arith, is_int,
|
|
// lp().print_term(term, tout << "term: ") << "\n";
|
|
// tout << "offset: " << offset << " gcd: " << g << "\n";);
|
|
|
|
expr_ref atom(m);
|
|
t = coeffs2app(coeffs, rational::zero(), is_int);
|
|
if (lower_bound)
|
|
atom = a.mk_ge(t, a.mk_numeral(offset, is_int));
|
|
else
|
|
atom = a.mk_le(t, a.mk_numeral(offset, is_int));
|
|
|
|
// ctx().get_rewriter()(atom);
|
|
// Note: it is not safe to rewrite atom because the rewriter can
|
|
// destroy structure, such as (div x 24) >= 0 becomes x >= 0 and the internal variable
|
|
// corresponding to (div x 24) is not constrained.
|
|
TRACE(arith, tout << t << ": " << atom << "\n";
|
|
lp().print_term(term, tout << "bound atom: ") << (lower_bound?" >= ":" <= ") << k << "\n";);
|
|
ctx().internalize(atom, true);
|
|
ctx().mark_as_relevant(atom.get());
|
|
return atom;
|
|
}
|
|
|
|
|
|
/**
|
|
* n = (div p q)
|
|
*
|
|
* (div p q) * q + (mod p q) = p, (mod p q) >= 0
|
|
*
|
|
* 0 < q => (p/q <= v(p)/v(q) => n <= floor(v(p)/v(q)))
|
|
* 0 < q => (v(p)/v(q) <= p/q => v(p)/v(q) - 1 < n)
|
|
*
|
|
*/
|
|
|
|
bool check_idiv_bounds() {
|
|
if (!m_nla)
|
|
return true;
|
|
m_nla->check_bounded_divisions();
|
|
add_lemmas();
|
|
return m_nla->lemmas().empty();
|
|
}
|
|
|
|
expr_ref var2expr(lpvar v) {
|
|
std::ostringstream name;
|
|
name << "v" << lp().local_to_external(v);
|
|
return expr_ref(m.mk_const(symbol(name.str()), a.mk_int()), m);
|
|
}
|
|
|
|
expr_ref multerm(rational const& r, expr* e) {
|
|
if (r.is_one()) return expr_ref(e, m);
|
|
return expr_ref(a.mk_mul(a.mk_numeral(r, true), e), m);
|
|
}
|
|
|
|
expr_ref term2expr(lp::lar_term const& term) {
|
|
expr_ref t(m);
|
|
expr_ref_vector ts(m);
|
|
for (lp::lar_term::ival p : term) {
|
|
auto ti = p.j();
|
|
if (lp().column_has_term(ti)) {
|
|
ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(ti))));
|
|
}
|
|
else {
|
|
ts.push_back(multerm(p.coeff(), var2expr(ti)));
|
|
}
|
|
}
|
|
if (ts.size() == 1) {
|
|
t = ts.back();
|
|
}
|
|
else {
|
|
t = a.mk_add(ts.size(), ts.data());
|
|
}
|
|
return t;
|
|
}
|
|
|
|
expr_ref constraint2fml(lp::constraint_index ci) {
|
|
lp::lar_base_constraint const& c = lp().constraints()[ci];
|
|
expr_ref fml(m);
|
|
expr_ref_vector ts(m);
|
|
rational rhs = c.rhs();
|
|
for (auto cv : c.coeffs()) {
|
|
ts.push_back(multerm(cv.first, var2expr(cv.second)));
|
|
}
|
|
switch (c.kind()) {
|
|
case lp::LE: fml = a.mk_le(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
|
|
case lp::LT: fml = a.mk_lt(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
|
|
case lp::GE: fml = a.mk_ge(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
|
|
case lp::GT: fml = a.mk_gt(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
|
|
case lp::EQ: fml = m.mk_eq(a.mk_add(ts.size(), ts.data()), a.mk_numeral(rhs, true)); break;
|
|
case lp::NE:
|
|
SASSERT(false); // unexpected
|
|
break;
|
|
}
|
|
return fml;
|
|
}
|
|
|
|
void dump_cut_lemma(std::ostream& out, lp::lar_term const& term, lp::mpq const& k, lp::explanation const& ex, bool upper) {
|
|
lp().print_term(term, out << "bound: ");
|
|
out << (upper?" <= ":" >= ") << k << "\n";
|
|
for (lp::lar_term::ival p : term) {
|
|
auto ti = p.j();
|
|
out << p.coeff() << " * ";
|
|
if (lp().column_has_term(ti)) {
|
|
lp().print_term(lp().get_term(ti), out) << "\n";
|
|
}
|
|
else {
|
|
out << "v" << lp().local_to_external(ti) << "\n";
|
|
}
|
|
}
|
|
for (auto ev : ex) {
|
|
lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
|
|
}
|
|
expr_ref_vector fmls(m);
|
|
for (auto ev : ex) {
|
|
fmls.push_back(constraint2fml(ev.ci()));
|
|
}
|
|
expr_ref t(term2expr(term), m);
|
|
if (upper) {
|
|
fmls.push_back(m.mk_not(a.mk_ge(t, a.mk_numeral(k, true))));
|
|
}
|
|
else {
|
|
fmls.push_back(m.mk_not(a.mk_le(t, a.mk_numeral(k, true))));
|
|
}
|
|
ast_pp_util visitor(m);
|
|
visitor.collect(fmls);
|
|
visitor.display_decls(out);
|
|
visitor.display_asserts(out, fmls, true);
|
|
out << "(check-sat)\n";
|
|
}
|
|
|
|
final_check_status check_lia() {
|
|
TRACE(arith,);
|
|
if (!m.inc()) {
|
|
TRACE(arith, tout << "canceled\n";);
|
|
return FC_CONTINUE;
|
|
}
|
|
auto cr = m_lia->check(&m_explanation);
|
|
if (cr != lp::lia_move::sat && ctx().get_fparams().m_arith_ignore_int)
|
|
return FC_GIVEUP;
|
|
|
|
switch (cr) {
|
|
case lp::lia_move::sat:
|
|
break;
|
|
|
|
case lp::lia_move::branch: {
|
|
TRACE(arith, tout << "branch\n";);
|
|
bool u = m_lia->is_upper();
|
|
auto const & k = m_lia->offset();
|
|
rational offset;
|
|
expr_ref t(m);
|
|
expr_ref b = mk_bound(m_lia->get_term(), k, !u, offset, t);
|
|
if (m.has_trace_stream()) {
|
|
app_ref body(m);
|
|
body = m.mk_or(b, m.mk_not(b));
|
|
th.log_axiom_instantiation(body);
|
|
m.trace_stream() << "[end-of-instance]\n";
|
|
}
|
|
IF_VERBOSE(4, verbose_stream() << "branch " << b << "\n";);
|
|
// branch on term >= k + 1
|
|
// branch on term <= k
|
|
// TBD: ctx().force_phase(ctx().get_literal(b));
|
|
// at this point we have a new unassigned atom that the
|
|
// SAT core assigns a value to
|
|
++m_stats.m_branch;
|
|
return FC_CONTINUE;
|
|
}
|
|
case lp::lia_move::cut: {
|
|
if (ctx().get_fparams().m_arith_ignore_int)
|
|
return FC_GIVEUP;
|
|
TRACE(arith, tout << "cut\n";);
|
|
// m_explanation implies term <= k
|
|
reset_evidence();
|
|
for (auto ev : m_explanation) {
|
|
set_evidence(ev.ci(), m_core, m_eqs);
|
|
}
|
|
// The call mk_bound() can set the m_infeasible_column in lar_solver
|
|
// so the explanation is safer to take before this call.
|
|
expr_ref b = mk_bound(m_lia->get_term(), m_lia->offset(), !m_lia->is_upper());
|
|
if (m.has_trace_stream()) {
|
|
th.log_axiom_instantiation(b);
|
|
m.trace_stream() << "[end-of-instance]\n";
|
|
}
|
|
IF_VERBOSE(4, verbose_stream() << "cut " << b << "\n");
|
|
TRACE(arith, dump_cut_lemma(tout, m_lia->get_term(), m_lia->offset(), m_explanation, m_lia->is_upper()););
|
|
literal lit(ctx().get_bool_var(b), false);
|
|
TRACE(arith,
|
|
ctx().display_lemma_as_smt_problem(tout << "new cut:\n", m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
|
|
display(tout););
|
|
assign(lit, m_core, m_eqs, m_params);
|
|
return FC_CONTINUE;
|
|
}
|
|
case lp::lia_move::conflict:
|
|
TRACE(arith, tout << "conflict\n";);
|
|
// ex contains unsat core
|
|
set_conflict();
|
|
return FC_CONTINUE;
|
|
case lp::lia_move::undef:
|
|
TRACE(arith, tout << "lia undef\n";);
|
|
return FC_CONTINUE;
|
|
case lp::lia_move::continue_with_check:
|
|
return FC_CONTINUE;
|
|
default:
|
|
UNREACHABLE();
|
|
}
|
|
if (!check_idiv_bounds())
|
|
return FC_CONTINUE;
|
|
|
|
return FC_DONE;
|
|
}
|
|
|
|
literal mk_literal(nla::ineq const& ineq) {
|
|
bool is_lower = true, pos = true, is_eq = false;
|
|
switch (ineq.cmp()) {
|
|
case lp::LE:
|
|
is_lower = false;
|
|
pos = false;
|
|
break;
|
|
case lp::LT:
|
|
is_lower = true;
|
|
pos = true;
|
|
break;
|
|
case lp::GE:
|
|
is_lower = true;
|
|
pos = false;
|
|
break;
|
|
case lp::GT:
|
|
is_lower = false;
|
|
pos = true;
|
|
break;
|
|
case lp::EQ:
|
|
is_eq = true;
|
|
pos = false;
|
|
break;
|
|
case lp::NE:
|
|
is_eq = true;
|
|
pos = true;
|
|
break;
|
|
default:
|
|
UNREACHABLE();
|
|
}
|
|
TRACE(arith, tout << "is_lower: " << is_lower << " pos " << pos << "\n";);
|
|
expr_ref atom(m);
|
|
// TBD utility: lp::lar_term term = mk_term(ineq.m_poly);
|
|
// then term is used instead of ineq.m_term
|
|
if (is_eq)
|
|
atom = mk_eq(ineq.term(), ineq.rs());
|
|
else
|
|
// create term >= 0 (or term <= 0)
|
|
atom = mk_bound(ineq.term(), ineq.rs(), is_lower);
|
|
return literal(ctx().get_bool_var(atom), pos);
|
|
}
|
|
|
|
void false_case_of_check_nla(const nla::lemma & l) {
|
|
m_lemma = l; //todo avoid the copy
|
|
m_explanation = l.expl();
|
|
literal_vector core;
|
|
SASSERT(!m_lemma.is_empty());
|
|
for (auto const& ineq : m_lemma.ineqs()) {
|
|
auto lit = mk_literal(ineq);
|
|
core.push_back(~lit);
|
|
}
|
|
set_conflict_or_lemma(core, false);
|
|
}
|
|
|
|
void assume_literal(nla::ineq const& i) {
|
|
auto lit = mk_literal(i);
|
|
ctx().mark_as_relevant(lit);
|
|
ctx().set_true_first_flag(lit.var());
|
|
}
|
|
|
|
final_check_status check_nla_continue(unsigned level) {
|
|
#if Z3DEBUG
|
|
flet f(lp().validate_blocker(), true);
|
|
#endif
|
|
lbool r = m_nla->check(level);
|
|
switch (r) {
|
|
case l_false:
|
|
add_lemmas();
|
|
return FC_CONTINUE;
|
|
case l_true:
|
|
return FC_DONE;
|
|
default:
|
|
return FC_GIVEUP;
|
|
}
|
|
}
|
|
|
|
final_check_status check_nla(unsigned level) {
|
|
// TODO - enable or remove if found useful internals are corrected:
|
|
// lp::lar_solver::scoped_auxiliary _sa(lp()); // new atoms are auxilairy and are not used in nra_solver
|
|
if (!m.inc()) {
|
|
TRACE(arith, tout << "canceled\n";);
|
|
return FC_GIVEUP;
|
|
}
|
|
CTRACE(arith,!m_nla, tout << "no nla\n";);
|
|
if (!m_nla)
|
|
return FC_DONE;
|
|
if (!m_nla->need_check())
|
|
return FC_DONE;
|
|
return check_nla_continue(level);
|
|
}
|
|
|
|
/**
|
|
\brief We must redefine this method, because theory of arithmetic contains
|
|
underspecified operators such as division by 0.
|
|
(/ a b) is essentially an uninterpreted function when b = 0.
|
|
Thus, 'a' must be considered a shared var if it is the child of an underspecified operator.
|
|
|
|
if merge(a / b, x + y) and a / b is root, then x + y become shared and all z + u in equivalence class of x + y.
|
|
|
|
|
|
TBD: when the set of underspecified subterms is small, compute the shared variables below it.
|
|
Recompute the set if there are merges that invalidate it.
|
|
Use the set to determine if a variable is shared.
|
|
*/
|
|
bool is_shared(theory_var v) const {
|
|
if (m_underspecified.empty())
|
|
return false;
|
|
enode * n = get_enode(v);
|
|
enode * r = n->get_root();
|
|
unsigned usz = m_underspecified.size();
|
|
TRACE(shared, tout << ctx().get_scope_level() << " " << enode_pp(n, ctx()) << " " << v << " underspecified " << usz << " parents " << r->get_num_parents() << "\n";);
|
|
if (r->get_num_parents() > 2*usz) {
|
|
for (unsigned i = 0; i < usz; ++i) {
|
|
app* u = m_underspecified[i];
|
|
unsigned sz = u->get_num_args();
|
|
for (unsigned j = 0; j < sz; ++j)
|
|
if (ctx().get_enode(u->get_arg(j))->get_root() == r)
|
|
return true;
|
|
}
|
|
}
|
|
else {
|
|
for (enode * parent : r->get_const_parents())
|
|
if (a.is_underspecified(parent->get_expr()))
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool m_new_def = false ;
|
|
|
|
bool adaptive() const { return ctx().get_fparams().m_arith_adaptive; }
|
|
double adaptive_assertion_threshold() const { return ctx().get_fparams().m_arith_adaptive_assertion_threshold; }
|
|
|
|
bool process_atoms() const {
|
|
if (!adaptive())
|
|
return true;
|
|
unsigned total_conflicts = ctx().get_num_conflicts();
|
|
if (total_conflicts < 10)
|
|
return true;
|
|
if (m_delay_ineqs_qhead < m_delay_ineqs.size())
|
|
return true;
|
|
double f = static_cast<double>(m_num_conflicts)/static_cast<double>(total_conflicts);
|
|
return f >= adaptive_assertion_threshold();
|
|
}
|
|
|
|
bool can_propagate() {
|
|
return process_atoms() && can_propagate_core();
|
|
}
|
|
|
|
bool can_propagate_core() {
|
|
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def || lp().has_changed_columns() ||
|
|
m_delay_ineqs_qhead < m_delay_ineqs.size();
|
|
}
|
|
|
|
bool propagate() {
|
|
return process_atoms() && propagate_core();
|
|
}
|
|
|
|
bool propagate_core() {
|
|
m_model_is_initialized = false;
|
|
flush_bound_axioms();
|
|
propagate_nla();
|
|
if (ctx().inconsistent())
|
|
return true;
|
|
if (!can_propagate_core())
|
|
return false;
|
|
|
|
for (; m_delay_ineqs_qhead < m_delay_ineqs.size() && !ctx().inconsistent() && m.inc(); ++m_delay_ineqs_qhead) {
|
|
auto atom = m_delay_ineqs[m_delay_ineqs_qhead];
|
|
ctx().push_trail(value_trail(m_delay_ineqs_qhead));
|
|
if (!ctx().is_relevant(atom))
|
|
continue;
|
|
expr *x, *y;
|
|
if (a.is_le(atom, x, y)) {
|
|
auto lit1 = mk_literal(atom);
|
|
auto lit2 = mk_literal(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), a.is_int(x->get_sort()))));
|
|
mk_axiom(~lit1, lit2);
|
|
mk_axiom(lit1, ~lit2);
|
|
}
|
|
else if (a.is_ge(atom, x, y)) {
|
|
auto lit1 = mk_literal(atom);
|
|
auto lit2 = mk_literal(a.mk_ge(a.mk_sub(x, y), a.mk_numeral(rational(0), a.is_int(x->get_sort()))));
|
|
mk_axiom(~lit1, lit2);
|
|
mk_axiom(lit1, ~lit2);
|
|
}
|
|
else {
|
|
UNREACHABLE();
|
|
}
|
|
}
|
|
|
|
m_new_def = false;
|
|
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
|
|
auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead];
|
|
|
|
api_bound* b = nullptr;
|
|
TRACE(arith, tout << "propagate: " << literal(bv, !is_true) << "\n";
|
|
if (!m_bool_var2bound.contains(bv)) tout << "not found\n");
|
|
if (m_bool_var2bound.find(bv, b) && !assert_bound(bv, is_true, *b)) {
|
|
get_infeasibility_explanation_and_set_conflict();
|
|
return true;
|
|
}
|
|
++m_asserted_qhead;
|
|
}
|
|
if (ctx().inconsistent())
|
|
return true;
|
|
|
|
lbool lbl = make_feasible();
|
|
if (!m.inc())
|
|
return true;
|
|
|
|
switch(lbl) {
|
|
case l_false:
|
|
TRACE(arith, tout << "propagation conflict\n";);
|
|
get_infeasibility_explanation_and_set_conflict();
|
|
break;
|
|
case l_true:
|
|
propagate_bounds_with_lp_solver();
|
|
break;
|
|
case l_undef:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
void propagate_nla() {
|
|
if (m_nla) {
|
|
m_nla->propagate();
|
|
add_lemmas();
|
|
lp().collect_more_rows_for_lp_propagation();
|
|
}
|
|
}
|
|
|
|
void add_equality(lpvar j, rational const& k, lp::explanation const& exp) {
|
|
TRACE(arith, tout << "equality " << j << " " << k << "\n");
|
|
theory_var v;
|
|
if (k == 1)
|
|
v = m_one_var;
|
|
else if (k == 0)
|
|
v = m_zero_var;
|
|
else if (!m_value2var.find(k, v))
|
|
return;
|
|
theory_var w = lp().local_to_external(j);
|
|
if (w < 0)
|
|
return;
|
|
lpvar i = register_theory_var_in_lar_solver(v);
|
|
add_eq(i, j, exp, true);
|
|
}
|
|
|
|
void add_lemmas() {
|
|
if (m_nla->should_check_feasible()) {
|
|
auto is_sat = make_feasible();
|
|
if (l_false == is_sat) {
|
|
get_infeasibility_explanation_and_set_conflict();
|
|
return;
|
|
}
|
|
}
|
|
for (const nla::ineq& i : m_nla->literals())
|
|
assume_literal(i);
|
|
for (const nla::lemma & l : m_nla->lemmas())
|
|
false_case_of_check_nla(l);
|
|
if (!propagate_eqs())
|
|
return;
|
|
for (auto const& [v, k, e] : m_nla->fixed_equalities())
|
|
add_equality(v, k, e);
|
|
for (auto const& [i, j, e] : m_nla->equalities())
|
|
add_eq(i, j, e, false);
|
|
}
|
|
|
|
bool should_propagate() const {
|
|
return bound_prop_mode::BP_NONE != propagation_mode();
|
|
}
|
|
|
|
bool should_refine_bounds() const {
|
|
return bound_prop_mode::BP_REFINE == propagation_mode() && ctx().at_search_level();
|
|
}
|
|
|
|
void consume(rational const& v, lp::constraint_index j) {
|
|
set_evidence(j, m_core, m_eqs);
|
|
m_explanation.add_pair(j, v);
|
|
}
|
|
|
|
void propagate_bounds_with_lp_solver() {
|
|
if (!should_propagate())
|
|
return;
|
|
|
|
m_bp.init();
|
|
lp().propagate_bounds_for_touched_rows(m_bp);
|
|
|
|
if (!m.inc())
|
|
return;
|
|
if (is_infeasible()) {
|
|
get_infeasibility_explanation_and_set_conflict();
|
|
}
|
|
else {
|
|
for (auto& ib : m_bp.ibounds()) {
|
|
m.inc();
|
|
if (ctx().inconsistent())
|
|
break;
|
|
propagate_lp_solver_bound(ib);
|
|
}
|
|
}
|
|
}
|
|
|
|
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
|
|
theory_var v = lp().local_to_external(vi);
|
|
if (v == null_theory_var)
|
|
return false;
|
|
|
|
if (should_refine_bounds())
|
|
return true;
|
|
|
|
if (static_cast<unsigned>(v) < m_bounds.size())
|
|
for (api_bound* b : m_bounds[v])
|
|
if (ctx().get_assignment(b->get_lit()) == l_undef &&
|
|
null_literal != is_bound_implied(kind, bval, *b))
|
|
return true;
|
|
|
|
return false;
|
|
}
|
|
|
|
#if 0
|
|
unsigned propagate_lp_solver_bound_dry_run(const lp::implied_bound& be) {
|
|
lpvar vi = be.m_j;
|
|
theory_var v = lp().local_to_external(vi);
|
|
|
|
if (v == null_theory_var)
|
|
return 0;
|
|
|
|
TRACE(arith, tout << "v" << v << " " << be.kind() << " " << be.m_bound << "\n";);
|
|
|
|
reserve_bounds(v);
|
|
|
|
if (m_unassigned_bounds[v] == 0 && !should_refine_bounds()) {
|
|
TRACE(arith, tout << "return\n";);
|
|
return 0;
|
|
}
|
|
lp_bounds const& bounds = m_bounds[v];
|
|
bool first = true;
|
|
unsigned count = 0;
|
|
for (unsigned i = 0; i < bounds.size(); ++i) {
|
|
api_bound* b = bounds[i];
|
|
if (ctx().get_assignment(b->get_lit()) != l_undef)
|
|
continue;
|
|
literal lit = is_bound_implied(be.kind(), be.m_bound, *b);
|
|
if (lit == null_literal)
|
|
continue;
|
|
TRACE(arith, tout << lit << " bound: " << *b << " first: " << first << "\n";);
|
|
ctx().display_literal_verbose(verbose_stream() << "miss ", lit) << "\n";
|
|
display(verbose_stream());
|
|
TRACE(arith, ctx().display_literal_verbose(tout << "miss ", lit) << "\n");
|
|
exit(0);
|
|
|
|
++count;
|
|
}
|
|
return count;
|
|
}
|
|
#endif
|
|
|
|
unsigned propagate_lp_solver_bound(const lp::implied_bound& be) {
|
|
lpvar vi = be.m_j;
|
|
theory_var v = lp().local_to_external(vi);
|
|
|
|
if (v == null_theory_var)
|
|
return 0;
|
|
|
|
TRACE(arith, tout << "v" << v << " " << be.kind() << " " << be.m_bound << "\n";);
|
|
|
|
reserve_bounds(v);
|
|
|
|
if (m_unassigned_bounds[v] == 0 && !should_refine_bounds()) {
|
|
TRACE(arith, tout << "return\n";);
|
|
return 0;
|
|
}
|
|
lp_bounds const& bounds = m_bounds[v];
|
|
bool first = true;
|
|
unsigned count = 0;
|
|
for (unsigned i = 0; i < bounds.size(); ++i) {
|
|
api_bound* b = bounds[i];
|
|
if (ctx().get_assignment(b->get_lit()) != l_undef)
|
|
continue;
|
|
literal lit = is_bound_implied(be.kind(), be.m_bound, *b);
|
|
if (lit == null_literal)
|
|
continue;
|
|
TRACE(arith, tout << lit << " bound: " << *b << " first: " << first << "\n";);
|
|
|
|
++count;
|
|
|
|
lp().settings().stats().m_num_of_implied_bounds ++;
|
|
if (first) {
|
|
first = false;
|
|
reset_evidence();
|
|
m_explanation.clear();
|
|
lp().explain_implied_bound(be, m_bp);
|
|
}
|
|
CTRACE(arith, m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
|
|
updt_unassigned_bounds(v, -1);
|
|
TRACE(arith,
|
|
ctx().display_literals_verbose(tout, m_core);
|
|
tout << "\n --> ";
|
|
ctx().display_literal_verbose(tout, lit);
|
|
tout << "\n";
|
|
display_evidence(tout, m_explanation);
|
|
lp().print_implied_bound(be, tout);
|
|
);
|
|
|
|
|
|
DEBUG_CODE(
|
|
for (auto& lit : m_core) {
|
|
VERIFY(ctx().get_assignment(lit) == l_true);
|
|
});
|
|
++m_stats.m_bound_propagations1;
|
|
assign(lit, m_core, m_eqs, m_params);
|
|
}
|
|
|
|
if (should_refine_bounds() && first)
|
|
refine_bound(v, be);
|
|
|
|
return count;
|
|
}
|
|
|
|
void refine_bound(theory_var v, const lp::implied_bound& be) {
|
|
lpvar vi = be.m_j;
|
|
if (lp().column_has_term(vi))
|
|
return;
|
|
expr_ref w(get_enode(v)->get_expr(), m);
|
|
if (a.is_add(w) || a.is_numeral(w) || m.is_ite(w))
|
|
return;
|
|
literal bound = null_literal;
|
|
switch (be.kind()) {
|
|
case lp::LE:
|
|
if (is_int(v) && (lp().column_has_lower_bound(vi) || !lp().column_has_upper_bound(vi)))
|
|
bound = mk_literal(a.mk_le(w, a.mk_numeral(floor(be.m_bound), a.is_int(w))));
|
|
if (is_real(v) && !lp().column_has_upper_bound(vi))
|
|
bound = mk_literal(a.mk_le(w, a.mk_numeral(be.m_bound, a.is_int(w))));
|
|
break;
|
|
case lp::GE:
|
|
if (is_int(v) && (lp().column_has_upper_bound(vi) || !lp().column_has_lower_bound(vi)))
|
|
bound = mk_literal(a.mk_ge(w, a.mk_numeral(ceil(be.m_bound), a.is_int(w))));
|
|
if (is_real(v) && !lp().column_has_lower_bound(vi))
|
|
bound = mk_literal(a.mk_ge(w, a.mk_numeral(be.m_bound, a.is_int(w))));
|
|
break;
|
|
default:
|
|
break;
|
|
}
|
|
if (bound == null_literal)
|
|
return;
|
|
if (ctx().get_assignment(bound) == l_true)
|
|
return;
|
|
|
|
++m_stats.m_bound_propagations1;
|
|
reset_evidence();
|
|
m_explanation.clear();
|
|
lp().explain_implied_bound(be, m_bp);
|
|
ctx().mark_as_relevant(bound);
|
|
assign(bound, m_core, m_eqs, m_params);
|
|
}
|
|
|
|
bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed) {
|
|
if (ctx().inconsistent())
|
|
return false;
|
|
theory_var uv = lp().local_to_external(u); // variables that are returned should have external representations
|
|
theory_var vv = lp().local_to_external(v); // so maybe better to have them already transformed to external form
|
|
if (uv == null_theory_var)
|
|
return false;
|
|
if (vv == null_theory_var)
|
|
return false;
|
|
enode* n1 = get_enode(uv);
|
|
enode* n2 = get_enode(vv);
|
|
|
|
TRACE(arith, tout << "add-eq " << pp(n1) << " == " << pp(n2) << "\n";);
|
|
if (n1->get_root() == n2->get_root())
|
|
return false;
|
|
expr* e1 = n1->get_expr();
|
|
expr* e2 = n2->get_expr();
|
|
if (e1->get_sort() != e2->get_sort())
|
|
return false;
|
|
if (!is_fixed && !a.is_numeral(e1) && !a.is_numeral(e2) && (m.is_ite(e1) || m.is_ite(e2)))
|
|
return false;
|
|
reset_evidence();
|
|
for (auto ev : e)
|
|
set_evidence(ev.ci(), m_core, m_eqs);
|
|
assign_eq(uv, vv);
|
|
return true;
|
|
}
|
|
|
|
literal_vector m_core2;
|
|
|
|
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& ps) {
|
|
if (params().m_arith_validate)
|
|
VERIFY(validate_assign(lit));
|
|
if (params().m_arith_dump_lemmas)
|
|
dump_assign_lemma(lit);
|
|
if (false && core.size() < small_lemma_size() && eqs.empty()) {
|
|
m_core2.reset();
|
|
for (auto const& c : core) {
|
|
m_core2.push_back(~c);
|
|
}
|
|
m_core2.push_back(lit);
|
|
justification * js = nullptr;
|
|
if (proofs_enabled()) {
|
|
js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(),
|
|
ps.size(), ps.data());
|
|
}
|
|
ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA, nullptr);
|
|
}
|
|
else {
|
|
ctx().assign(
|
|
lit, ctx().mk_justification(
|
|
ext_theory_propagation_justification(
|
|
get_id(), ctx(), core.size(), core.data(),
|
|
eqs.size(), eqs.data(), lit, ps.size(), ps.data())));
|
|
}
|
|
}
|
|
|
|
literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const {
|
|
if ((k == lp::LE || k == lp::LT) && b.get_bound_kind() == lp_api::upper_t && value <= b.get_value()) {
|
|
return b.get_lit();
|
|
}
|
|
if ((k == lp::GE || k == lp::GT) && b.get_bound_kind() == lp_api::lower_t && b.get_value() <= value) {
|
|
return b.get_lit();
|
|
}
|
|
if (k == lp::LE && b.get_bound_kind() == lp_api::lower_t && value < b.get_value()) {
|
|
return ~b.get_lit();
|
|
}
|
|
if (k == lp::LT && b.get_bound_kind() == lp_api::lower_t && value <= b.get_value()) {
|
|
return ~b.get_lit();
|
|
}
|
|
if (k == lp::GE && b.get_bound_kind() == lp_api::upper_t && b.get_value() < value) {
|
|
return ~b.get_lit();
|
|
}
|
|
if (k == lp::GT && b.get_bound_kind() == lp_api::upper_t && b.get_value() <= value) {
|
|
return ~b.get_lit();
|
|
}
|
|
|
|
return null_literal;
|
|
}
|
|
|
|
bool check_bv_terms() {
|
|
for (app* n : m_bv_terms) {
|
|
if (!check_bv_term(n)) {
|
|
++m_stats.m_bv_axioms;
|
|
return false;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
|
|
bool check_bv_term(app* n) {
|
|
unsigned sz = 0;
|
|
expr* _x = nullptr, * _y = nullptr;
|
|
if (!ctx().is_relevant(ctx().get_enode(n)))
|
|
return true;
|
|
expr_ref vx(m), vy(m),vn(m);
|
|
rational valn, valx, valy;
|
|
bool is_int;
|
|
VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
|
|
if (!get_value(ctx().get_enode(_x), vx) || !get_value(ctx().get_enode(_y), vy) || !get_value(ctx().get_enode(n), vn)) {
|
|
IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
|
|
found_unsupported(n);
|
|
return true;
|
|
}
|
|
if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) {
|
|
IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
|
|
found_unsupported(n);
|
|
return true;
|
|
}
|
|
rational N = rational::power_of_two(sz);
|
|
valx = mod(valx, N);
|
|
valy = mod(valy, N);
|
|
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
|
|
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
|
|
SASSERT(0 <= valn && valn < N);
|
|
|
|
// x mod 2^{i + 1} >= 2^i means the i'th bit is 1.
|
|
auto bitof = [&](expr* x, unsigned i) {
|
|
expr_ref r(m);
|
|
r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i)));
|
|
return mk_literal(r);
|
|
};
|
|
|
|
if (a.is_band(n)) {
|
|
IF_VERBOSE(2, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n");
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
bool xb = valx.get_bit(i);
|
|
bool yb = valy.get_bit(i);
|
|
bool nb = valn.get_bit(i);
|
|
if (xb && yb && !nb)
|
|
ctx().mk_th_axiom(get_id(), ~bitof(x, i), ~bitof(y, i), bitof(n, i));
|
|
else if (nb && !xb)
|
|
ctx().mk_th_axiom(get_id(), ~bitof(n, i), bitof(x, i));
|
|
else if (nb && !yb)
|
|
ctx().mk_th_axiom(get_id(), ~bitof(n, i), bitof(y, i));
|
|
else
|
|
continue;
|
|
return false;
|
|
}
|
|
}
|
|
if (a.is_shl(n)) {
|
|
SASSERT(valy >= 0);
|
|
if (valy >= sz || valy == 0)
|
|
return true;
|
|
unsigned k = valy.get_unsigned();
|
|
sat::literal eq = th.mk_eq(n, a.mk_mod(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), a.mk_int(N)), false);
|
|
if (ctx().get_assignment(eq) == l_true)
|
|
return true;
|
|
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
|
|
IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
|
|
return false;
|
|
}
|
|
if (a.is_lshr(n)) {
|
|
SASSERT(valy >= 0);
|
|
if (valy >= sz || valy == 0)
|
|
return true;
|
|
unsigned k = valy.get_unsigned();
|
|
sat::literal eq = th.mk_eq(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))), false);
|
|
if (ctx().get_assignment(eq) == l_true)
|
|
return true;
|
|
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), eq);
|
|
IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
|
|
return false;
|
|
}
|
|
if (a.is_ashr(n)) {
|
|
SASSERT(valy >= 0);
|
|
if (valy >= sz || valy == 0)
|
|
return true;
|
|
unsigned k = valy.get_unsigned();
|
|
sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
|
|
sat::literal eq;
|
|
expr* xdiv2k;
|
|
switch (ctx().get_assignment(signx)) {
|
|
case l_true:
|
|
// x < 0 & y = k -> n = (x div 2^k - 2^{N-k}) mod 2^N
|
|
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
|
|
eq = th.mk_eq(n, a.mk_mod(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), a.mk_int(N)), false);
|
|
if (ctx().get_assignment(eq) == l_true)
|
|
return true;
|
|
break;
|
|
case l_false:
|
|
// x >= 0 & y = k -> n = x div 2^k
|
|
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
|
|
eq = th.mk_eq(n, xdiv2k, false);
|
|
if (ctx().get_assignment(eq) == l_true)
|
|
return true;
|
|
break;
|
|
case l_undef:
|
|
ctx().mark_as_relevant(signx);
|
|
return false;
|
|
}
|
|
ctx().mk_th_axiom(get_id(), ~th.mk_eq(y, a.mk_int(k), false), ~signx, eq);
|
|
return false;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
expr_ref mk_le(expr* x, expr* y) {
|
|
if (a.is_numeral(y))
|
|
return expr_ref(a.mk_le(x, y), m);
|
|
if (a.is_numeral(x))
|
|
return expr_ref(a.mk_ge(y, x), m);
|
|
return expr_ref(a.mk_le(a.mk_sub(x, y), a.mk_numeral(rational(0), x->get_sort())), m);
|
|
}
|
|
|
|
void mk_bv_axiom(app* n) {
|
|
unsigned sz = 0;
|
|
expr* _x = nullptr, * _y = nullptr;
|
|
VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
|
|
rational N = rational::power_of_two(sz);
|
|
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
|
|
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
|
|
|
|
// 0 <= n < 2^sz
|
|
|
|
ctx().mk_th_axiom(get_id(), mk_literal(a.mk_ge(n, a.mk_int(0))));
|
|
ctx().mk_th_axiom(get_id(), mk_literal(a.mk_le(n, a.mk_int(N - 1))));
|
|
|
|
if (a.is_band(n)) {
|
|
|
|
// 0 <= x => x&y <= x
|
|
// 0 <= y => x&y <= y
|
|
// TODO? x = y => x&y = x
|
|
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(x, a.mk_int(0))), mk_literal(a.mk_le(n, x)));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(0))), mk_literal(a.mk_le(n, y)));
|
|
}
|
|
else if (a.is_shl(n)) {
|
|
// y >= sz => n = 0
|
|
// y = 0 => n = x
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0))));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
|
|
}
|
|
else if (a.is_lshr(n)) {
|
|
// y >= sz => n = 0
|
|
// y = 0 => n = x
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(sz))), mk_literal(m.mk_eq(n, a.mk_int(0))));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(y, a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
|
|
}
|
|
else if (a.is_ashr(n)) {
|
|
// y >= sz & x < 2^{sz-1} => n = 0
|
|
// y >= sz & x >= 2^{sz-1} => n = -1
|
|
// y = 0 => n = x
|
|
auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0))));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1))));
|
|
ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x)));
|
|
}
|
|
else
|
|
UNREACHABLE();
|
|
}
|
|
|
|
|
|
void mk_bound_axioms(api_bound& b) {
|
|
if (!ctx().is_searching()) {
|
|
//
|
|
// NB. We make an assumption that user push calls propagation
|
|
// before internal scopes are pushed. This flushes all newly
|
|
// asserted atoms into the right context.
|
|
//
|
|
m_new_bounds.push_back(&b);
|
|
return;
|
|
}
|
|
theory_var v = b.get_var();
|
|
lp_api::bound_kind kind1 = b.get_bound_kind();
|
|
rational const& k1 = b.get_value();
|
|
lp_bounds & bounds = m_bounds[v];
|
|
|
|
api_bound* end = nullptr;
|
|
api_bound* lo_inf = end, *lo_sup = end;
|
|
api_bound* hi_inf = end, *hi_sup = end;
|
|
|
|
for (api_bound* other : bounds) {
|
|
if (other == &b) continue;
|
|
if (b.get_lit() == other->get_lit()) continue;
|
|
lp_api::bound_kind kind2 = other->get_bound_kind();
|
|
rational const& k2 = other->get_value();
|
|
if (k1 == k2 && kind1 == kind2) {
|
|
// the bounds are equivalent.
|
|
continue;
|
|
}
|
|
|
|
SASSERT(k1 != k2 || kind1 != kind2);
|
|
if (kind2 == lp_api::lower_t) {
|
|
if (k2 < k1) {
|
|
if (lo_inf == end || k2 > lo_inf->get_value()) {
|
|
lo_inf = other;
|
|
}
|
|
}
|
|
else if (lo_sup == end || k2 < lo_sup->get_value()) {
|
|
lo_sup = other;
|
|
}
|
|
}
|
|
else if (k2 < k1) {
|
|
if (hi_inf == end || k2 > hi_inf->get_value()) {
|
|
hi_inf = other;
|
|
}
|
|
}
|
|
else if (hi_sup == end || k2 < hi_sup->get_value()) {
|
|
hi_sup = other;
|
|
}
|
|
}
|
|
if (lo_inf != end) mk_bound_axiom(b, *lo_inf);
|
|
if (lo_sup != end) mk_bound_axiom(b, *lo_sup);
|
|
if (hi_inf != end) mk_bound_axiom(b, *hi_inf);
|
|
if (hi_sup != end) mk_bound_axiom(b, *hi_sup);
|
|
}
|
|
|
|
|
|
void mk_bound_axiom(api_bound& b1, api_bound& b2) {
|
|
literal l1 = b1.get_lit();
|
|
literal l2 = b2.get_lit();
|
|
rational const& k1 = b1.get_value();
|
|
rational const& k2 = b2.get_value();
|
|
lp_api::bound_kind kind1 = b1.get_bound_kind();
|
|
lp_api::bound_kind kind2 = b2.get_bound_kind();
|
|
bool v_is_int = b1.is_int();
|
|
SASSERT(b1.get_var() == b2.get_var());
|
|
if (k1 == k2 && kind1 == kind2) return;
|
|
SASSERT(k1 != k2 || kind1 != kind2);
|
|
parameter coeffs[3] = { parameter(symbol("farkas")),
|
|
parameter(rational(1)), parameter(rational(1)) };
|
|
|
|
if (kind1 == lp_api::lower_t) {
|
|
if (kind2 == lp_api::lower_t) {
|
|
if (k2 <= k1) {
|
|
mk_clause(~l1, l2, 3, coeffs);
|
|
}
|
|
else {
|
|
mk_clause(l1, ~l2, 3, coeffs);
|
|
}
|
|
}
|
|
else if (k1 <= k2) {
|
|
// k1 <= k2, k1 <= x or x <= k2
|
|
mk_clause(l1, l2, 3, coeffs);
|
|
}
|
|
else {
|
|
// k1 > hi_inf, k1 <= x => ~(x <= hi_inf)
|
|
mk_clause(~l1, ~l2, 3, coeffs);
|
|
if (v_is_int && k1 == k2 + rational(1)) {
|
|
// k1 <= x or x <= k1-1
|
|
mk_clause(l1, l2, 3, coeffs);
|
|
}
|
|
}
|
|
}
|
|
else if (kind2 == lp_api::lower_t) {
|
|
if (k1 >= k2) {
|
|
// k1 >= lo_inf, k1 >= x or lo_inf <= x
|
|
mk_clause(l1, l2, 3, coeffs);
|
|
}
|
|
else {
|
|
// k1 < k2, k2 <= x => ~(x <= k1)
|
|
mk_clause(~l1, ~l2, 3, coeffs);
|
|
if (v_is_int && k1 == k2 - rational(1)) {
|
|
// x <= k1 or k1+l <= x
|
|
mk_clause(l1, l2, 3, coeffs);
|
|
}
|
|
|
|
}
|
|
}
|
|
else {
|
|
// kind1 == A_UPPER, kind2 == A_UPPER
|
|
if (k1 >= k2) {
|
|
// k1 >= k2, x <= k2 => x <= k1
|
|
mk_clause(l1, ~l2, 3, coeffs);
|
|
}
|
|
else {
|
|
// k1 <= hi_sup , x <= k1 => x <= hi_sup
|
|
mk_clause(~l1, l2, 3, coeffs);
|
|
}
|
|
}
|
|
}
|
|
|
|
typedef lp_bounds::iterator iterator;
|
|
|
|
void flush_bound_axioms() {
|
|
|
|
CTRACE(arith, !m_new_bounds.empty(), tout << "flush bound axioms\n";);
|
|
|
|
while (!m_new_bounds.empty()) {
|
|
lp_bounds atoms;
|
|
atoms.push_back(m_new_bounds.back());
|
|
m_new_bounds.pop_back();
|
|
theory_var v = atoms.back()->get_var();
|
|
for (unsigned i = 0; i < m_new_bounds.size(); ++i) {
|
|
if (m_new_bounds[i]->get_var() == v) {
|
|
atoms.push_back(m_new_bounds[i]);
|
|
m_new_bounds[i] = m_new_bounds.back();
|
|
m_new_bounds.pop_back();
|
|
--i;
|
|
}
|
|
}
|
|
CTRACE(arith, atoms.size() > 1,
|
|
for (auto* a : atoms) a->display(tout) << "\n";);
|
|
lp_bounds occs(m_bounds[v]);
|
|
|
|
std::sort(atoms.begin(), atoms.end(), compare_bounds());
|
|
std::sort(occs.begin(), occs.end(), compare_bounds());
|
|
|
|
iterator begin1 = occs.begin();
|
|
iterator begin2 = occs.begin();
|
|
iterator end = occs.end();
|
|
begin1 = first(lp_api::lower_t, begin1, end);
|
|
begin2 = first(lp_api::upper_t, begin2, end);
|
|
|
|
iterator lo_inf = begin1, lo_sup = begin1;
|
|
iterator hi_inf = begin2, hi_sup = begin2;
|
|
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
|
|
ptr_addr_hashtable<api_bound> visited;
|
|
for (unsigned i = 0; i < atoms.size(); ++i) {
|
|
api_bound* a1 = atoms[i];
|
|
iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
|
|
iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
|
|
iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
|
|
iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
|
|
if (lo_inf1 != end) lo_inf = lo_inf1;
|
|
if (lo_sup1 != end) lo_sup = lo_sup1;
|
|
if (hi_inf1 != end) hi_inf = hi_inf1;
|
|
if (hi_sup1 != end) hi_sup = hi_sup1;
|
|
if (!flo_inf) lo_inf = end;
|
|
if (!fhi_inf) hi_inf = end;
|
|
if (!flo_sup) lo_sup = end;
|
|
if (!fhi_sup) hi_sup = end;
|
|
visited.insert(a1);
|
|
if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(*a1, **lo_inf);
|
|
if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(*a1, **lo_sup);
|
|
if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(*a1, **hi_inf);
|
|
if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(*a1, **hi_sup);
|
|
}
|
|
}
|
|
}
|
|
|
|
struct compare_bounds {
|
|
bool operator()(api_bound* a1, api_bound* a2) const { return a1->get_value() < a2->get_value(); }
|
|
};
|
|
|
|
|
|
lp_bounds::iterator first(
|
|
lp_api::bound_kind kind,
|
|
iterator it,
|
|
iterator end) {
|
|
for (; it != end; ++it) {
|
|
api_bound* a = *it;
|
|
if (a->get_bound_kind() == kind) return it;
|
|
}
|
|
return end;
|
|
}
|
|
|
|
lp_bounds::iterator next_inf(
|
|
api_bound* a1,
|
|
lp_api::bound_kind kind,
|
|
iterator it,
|
|
iterator end,
|
|
bool& found_compatible) {
|
|
rational const & k1(a1->get_value());
|
|
iterator result = end;
|
|
found_compatible = false;
|
|
for (; it != end; ++it) {
|
|
api_bound * a2 = *it;
|
|
if (a1 == a2) continue;
|
|
if (a2->get_bound_kind() != kind) continue;
|
|
rational const & k2(a2->get_value());
|
|
found_compatible = true;
|
|
if (k2 <= k1) {
|
|
result = it;
|
|
}
|
|
else {
|
|
break;
|
|
}
|
|
}
|
|
return result;
|
|
}
|
|
|
|
lp_bounds::iterator next_sup(
|
|
api_bound* a1,
|
|
lp_api::bound_kind kind,
|
|
iterator it,
|
|
iterator end,
|
|
bool& found_compatible) {
|
|
rational const & k1(a1->get_value());
|
|
found_compatible = false;
|
|
for (; it != end; ++it) {
|
|
api_bound * a2 = *it;
|
|
if (a1 == a2) continue;
|
|
if (a2->get_bound_kind() != kind) continue;
|
|
rational const & k2(a2->get_value());
|
|
found_compatible = true;
|
|
if (k1 < k2) {
|
|
return it;
|
|
}
|
|
}
|
|
return end;
|
|
}
|
|
|
|
// for glb lo': lo' < lo:
|
|
// lo <= x -> lo' <= x
|
|
// lo <= x -> ~(x <= lo')
|
|
// for lub hi': hi' > hi
|
|
// x <= hi -> x <= hi'
|
|
// x <= hi -> ~(x >= hi')
|
|
|
|
void propagate_bound(bool_var bv, bool is_true, api_bound& b) {
|
|
if (bound_prop_mode::BP_NONE == propagation_mode()) {
|
|
return;
|
|
}
|
|
lp_api::bound_kind k = b.get_bound_kind();
|
|
theory_var v = b.get_var();
|
|
inf_rational val = b.get_value(is_true);
|
|
lp_bounds const& bounds = m_bounds[v];
|
|
SASSERT(!bounds.empty());
|
|
if (bounds.size() == 1) return;
|
|
if (m_unassigned_bounds[v] == 0) return;
|
|
bool v_is_int = b.is_int();
|
|
literal lit1(bv, !is_true);
|
|
literal lit2 = null_literal;
|
|
bool find_glb = (is_true == (k == lp_api::lower_t));
|
|
TRACE(arith_verbose, tout << "v" << v << " find_glb: " << find_glb << " is_true: " << is_true << " k: " << k << " is_lower: " << (k == lp_api::lower_t) << "\n";);
|
|
if (find_glb) {
|
|
rational glb;
|
|
api_bound* lb = nullptr;
|
|
for (api_bound* b2 : bounds) {
|
|
if (b2 == &b) continue;
|
|
rational const& val2 = b2->get_value();
|
|
if (((is_true || v_is_int) ? val2 < val : val2 <= val) && (!lb || glb < val2)) {
|
|
lb = b2;
|
|
glb = val2;
|
|
}
|
|
}
|
|
if (!lb) return;
|
|
bool sign = lb->get_bound_kind() != lp_api::lower_t;
|
|
lit2 = lb->get_lit();
|
|
if (sign)
|
|
lit2.neg();
|
|
}
|
|
else {
|
|
rational lub;
|
|
api_bound* ub = nullptr;
|
|
for (api_bound* b2 : bounds) {
|
|
if (b2 == &b) continue;
|
|
rational const& val2 = b2->get_value();
|
|
if (((is_true || v_is_int) ? val < val2 : val <= val2) && (!ub || val2 < lub)) {
|
|
ub = b2;
|
|
lub = val2;
|
|
}
|
|
}
|
|
if (!ub) return;
|
|
bool sign = ub->get_bound_kind() != lp_api::upper_t;
|
|
lit2 = ub->get_lit();
|
|
if (sign)
|
|
lit2.neg();
|
|
}
|
|
updt_unassigned_bounds(v, -1);
|
|
++m_stats.m_bound_propagations2;
|
|
reset_evidence();
|
|
m_core.push_back(lit1);
|
|
TRACE(arith,
|
|
ctx().display_literals_verbose(tout, m_core);
|
|
ctx().display_literal_verbose(tout << " => ", lit2);
|
|
tout << "\n";);
|
|
assign(lit2, m_core, m_eqs, m_bound_params);
|
|
++m_stats.m_bounds_propagations;
|
|
}
|
|
|
|
svector<lp::lpvar> m_todo_vars;
|
|
|
|
void add_use_lists(api_bound* b) {
|
|
theory_var v = b->get_var();
|
|
lpvar vi = register_theory_var_in_lar_solver(v);
|
|
if (!lp().column_has_term(vi)) {
|
|
return;
|
|
}
|
|
m_todo_vars.push_back(vi);
|
|
while (!m_todo_vars.empty()) {
|
|
auto ti = m_todo_vars.back();
|
|
SASSERT(lp().column_has_term(ti));
|
|
m_todo_vars.pop_back();
|
|
lp::lar_term const& term = lp().get_term(ti);
|
|
for (auto p : term) {
|
|
lp::lpvar wi = p.j();
|
|
if (lp().column_has_term(wi)) {
|
|
m_todo_vars.push_back(wi);
|
|
}
|
|
else {
|
|
unsigned w = lp().local_to_external(wi);
|
|
m_use_list.reserve(w + 1, ptr_vector<api_bound>());
|
|
m_use_list[w].push_back(b);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
void del_use_lists(api_bound* b) {
|
|
theory_var v = b->get_var();
|
|
lpvar vi = get_lpvar(v);
|
|
if (!lp().column_has_term(vi)) {
|
|
return;
|
|
}
|
|
m_todo_vars.push_back(vi);
|
|
while (!m_todo_vars.empty()) {
|
|
auto ti = m_todo_vars.back();
|
|
SASSERT(lp().column_has_term(ti));
|
|
m_todo_vars.pop_back();
|
|
lp::lar_term const& term = lp().get_term(ti);
|
|
for (auto coeff : term) {
|
|
auto wi = coeff.j();
|
|
if (lp().column_has_term(wi)) {
|
|
m_todo_vars.push_back(wi);
|
|
}
|
|
else {
|
|
unsigned w = lp().local_to_external(wi);
|
|
SASSERT(m_use_list[w].back() == b);
|
|
m_use_list[w].pop_back();
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
//
|
|
// propagate bounds to compound terms
|
|
// The idea is that if bounds on all variables in an inequality ax + by + cz >= k
|
|
// have been assigned we may know the truth value of the inequality by using simple
|
|
// bounds propagation.
|
|
//
|
|
void propagate_bound_compound(bool_var bv, bool is_true, api_bound& b) {
|
|
theory_var v = b.get_var();
|
|
TRACE(arith, tout << pp(v) << "\n";);
|
|
if (static_cast<unsigned>(v) >= m_use_list.size()) {
|
|
return;
|
|
}
|
|
for (auto const& vb : m_use_list[v]) {
|
|
if (ctx().get_assignment(vb->get_lit()) != l_undef) {
|
|
TRACE(arith_verbose, display_bound(tout << "assigned ", *vb) << "\n";);
|
|
continue;
|
|
}
|
|
inf_rational r;
|
|
// x + y
|
|
// x >= 0, y >= 1 -> x + y >= 1
|
|
// x <= 0, y <= 2 -> x + y <= 2
|
|
literal lit = null_literal;
|
|
if (lp_api::lower_t == vb->get_bound_kind()) {
|
|
if (get_glb(*vb, r) && r >= vb->get_value()) { // vb is assigned true
|
|
lit = vb->get_lit();
|
|
}
|
|
else if (get_lub(*vb, r) && r < vb->get_value()) { // vb is assigned false
|
|
lit = ~vb->get_lit();
|
|
}
|
|
}
|
|
else {
|
|
if (get_glb(*vb, r) && r > vb->get_value()) { // VB <= value < val(VB)
|
|
lit = ~vb->get_lit();
|
|
}
|
|
else if (get_lub(*vb, r) && r <= vb->get_value()) { // val(VB) <= value
|
|
lit = vb->get_lit();
|
|
}
|
|
}
|
|
|
|
// get_glb and get_lub set m_core, m_eqs, m_params
|
|
if (lit != null_literal) {
|
|
TRACE(arith,
|
|
ctx().display_literals_verbose(tout, m_core);
|
|
ctx().display_literal_verbose(tout << "\n --> ", lit) << "\n";
|
|
);
|
|
|
|
|
|
assign(lit, m_core, m_eqs, m_params);
|
|
}
|
|
else {
|
|
TRACE(arith_verbose, display_bound(tout << "skip ", *vb) << "\n";);
|
|
}
|
|
}
|
|
}
|
|
|
|
bool get_lub(api_bound const& b, inf_rational& lub) {
|
|
return get_bound(b, lub, true);
|
|
}
|
|
|
|
bool get_glb(api_bound const& b, inf_rational& glb) {
|
|
return get_bound(b, glb, false);
|
|
}
|
|
|
|
std::ostream& display_bound(std::ostream& out, api_bound const& b) {
|
|
return out << mk_pp(ctx().bool_var2expr(b.get_lit().var()), m);
|
|
}
|
|
|
|
bool get_bound(api_bound const& b, inf_rational& r, bool is_lub) {
|
|
reset_evidence();
|
|
r.reset();
|
|
theory_var v = b.get_var();
|
|
lp::lpvar ti = get_lpvar(v);
|
|
SASSERT(lp().column_has_term(ti));
|
|
lp::lar_term const& term = lp().get_term(ti);
|
|
for (auto const mono : term) {
|
|
auto wi = mono.j();
|
|
u_dependency* ci = nullptr;
|
|
rational value;
|
|
bool is_strict;
|
|
if (lp().column_has_term(wi)) {
|
|
return false;
|
|
}
|
|
if (mono.coeff().is_neg() == is_lub) {
|
|
// -3*x ... <= lub based on lower bound for x.
|
|
if (!lp().has_lower_bound(wi, ci, value, is_strict)) {
|
|
return false;
|
|
}
|
|
if (is_strict) {
|
|
r += inf_rational(rational::zero(), mono.coeff().is_pos());
|
|
}
|
|
}
|
|
else {
|
|
if (!lp().has_upper_bound(wi, ci, value, is_strict)) {
|
|
return false;
|
|
}
|
|
if (is_strict) {
|
|
r += inf_rational(rational::zero(), mono.coeff().is_pos());
|
|
}
|
|
}
|
|
r += value * mono.coeff();
|
|
set_evidence(ci, m_core, m_eqs);
|
|
}
|
|
TRACE(arith_verbose, tout << (is_lub?"lub":"glb") << " is " << r << "\n";);
|
|
return true;
|
|
}
|
|
|
|
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true) {
|
|
switch (bk) {
|
|
case lp_api::lower_t:
|
|
return is_true ? lp::GE : (is_int ? lp::LE : lp::LT);
|
|
case lp_api::upper_t:
|
|
return is_true ? lp::LE : (is_int ? lp::GE : lp::GT);
|
|
}
|
|
UNREACHABLE();
|
|
return lp::EQ;
|
|
}
|
|
|
|
bool assert_bound(bool_var bv, bool is_true, api_bound& b) {
|
|
TRACE(arith, tout << b << "\n";);
|
|
lp::constraint_index ci = b.get_constraint(is_true);
|
|
lp().activate(ci);
|
|
if (is_infeasible())
|
|
return false;
|
|
lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true);
|
|
if (k == lp::LT || k == lp::LE) {
|
|
++m_stats.m_assert_lower;
|
|
}
|
|
else {
|
|
++m_stats.m_assert_upper;
|
|
}
|
|
inf_rational value = b.get_value(is_true);
|
|
if (propagate_eqs() && value.is_rational())
|
|
propagate_eqs(b.column_index(), ci, k, b, value.get_rational());
|
|
return true;
|
|
#if 0
|
|
if (should_propagate())
|
|
lp().add_column_rows_to_touched_rows(b.tv().id());
|
|
#endif
|
|
}
|
|
|
|
api_bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) {
|
|
scoped_internalize_state st(*this);
|
|
st.vars().push_back(v);
|
|
st.coeffs().push_back(rational::one());
|
|
init_left_side(st);
|
|
lp::constraint_index cT, cF;
|
|
bool v_is_int = is_int(v);
|
|
auto vi = register_theory_var_in_lar_solver(v);
|
|
|
|
lp::lconstraint_kind kT = bound2constraint_kind(v_is_int, bk, true);
|
|
lp::lconstraint_kind kF = bound2constraint_kind(v_is_int, bk, false);
|
|
|
|
cT = lp().mk_var_bound(vi, kT, bound);
|
|
if (v_is_int) {
|
|
rational boundF = (bk == lp_api::lower_t) ? bound - 1 : bound + 1;
|
|
cF = lp().mk_var_bound(vi, kF, boundF);
|
|
}
|
|
else {
|
|
cF = lp().mk_var_bound(vi, kF, bound);
|
|
}
|
|
add_ineq_constraint(cT, literal(bv, false));
|
|
add_ineq_constraint(cF, literal(bv, true));
|
|
|
|
return alloc(api_bound, literal(bv, false), v, vi, v_is_int, bound, bk, cT, cF);
|
|
}
|
|
|
|
//
|
|
// fixed equalities.
|
|
// A fixed equality is inferred if there are two variables v1, v2 whose
|
|
// upper and lower bounds coincide.
|
|
// Then the equality v1 == v2 is propagated to the core.
|
|
//
|
|
|
|
typedef std::pair<lp::constraint_index, rational> constraint_bound;
|
|
vector<constraint_bound> m_lower_terms;
|
|
vector<constraint_bound> m_upper_terms;
|
|
|
|
void propagate_eqs(lp::lpvar t, lp::constraint_index ci1, lp::lconstraint_kind k, api_bound& b, rational const& value) {
|
|
u_dependency* ci2 = nullptr;
|
|
auto pair = [&]() { return lp().dep_manager().mk_join(lp().dep_manager().mk_leaf(ci1), ci2); };
|
|
if (k == lp::GE && set_lower_bound(t, ci1, value) && has_upper_bound(t, ci2, value)) {
|
|
fixed_var_eh(b.get_var(), t, pair(), value);
|
|
}
|
|
else if (k == lp::LE && set_upper_bound(t, ci1, value) && has_lower_bound(t, ci2, value)) {
|
|
fixed_var_eh(b.get_var(), t, pair(), value);
|
|
}
|
|
}
|
|
|
|
|
|
bool propagate_eqs() const { return params().m_arith_propagate_eqs && m_num_conflicts < params().m_arith_propagation_threshold; }
|
|
|
|
bound_prop_mode propagation_mode() const { return m_num_conflicts < params().m_arith_propagation_threshold ? params().m_arith_bound_prop : bound_prop_mode::BP_NONE; }
|
|
|
|
unsigned small_lemma_size() const { return params().m_arith_small_lemma_size; }
|
|
|
|
bool proofs_enabled() const { return m.proofs_enabled(); }
|
|
|
|
bool set_upper_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); }
|
|
|
|
bool set_lower_bound(lp::lpvar t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); }
|
|
|
|
vector<constraint_bound> m_history;
|
|
|
|
bool set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower) {
|
|
if (lp().column_has_term(tv)) {
|
|
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
|
|
if (vec.size() <= tv) {
|
|
vec.resize(tv + 1, constraint_bound(UINT_MAX, rational()));
|
|
}
|
|
constraint_bound& b = vec[tv];
|
|
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
|
|
TRACE(arith, tout << "tighter bound " << tv << "\n";);
|
|
m_history.push_back(vec[tv]);
|
|
ctx().push_trail(history_trail<constraint_bound>(vec, tv, m_history));
|
|
b.first = ci;
|
|
b.second = v;
|
|
}
|
|
return true;
|
|
}
|
|
else {
|
|
// m_solver already tracks bounds on proper variables, but not on terms.
|
|
bool is_strict = false;
|
|
rational b;
|
|
u_dependency* dep = nullptr;
|
|
if (is_lower) {
|
|
return lp().has_lower_bound(tv, dep, b, is_strict) && !is_strict && b == v;
|
|
}
|
|
else {
|
|
return lp().has_upper_bound(tv, dep, b, is_strict) && !is_strict && b == v;
|
|
}
|
|
}
|
|
}
|
|
|
|
bool var_has_bound(lpvar vi, bool is_lower) {
|
|
bool is_strict = false;
|
|
rational b;
|
|
u_dependency* dep;
|
|
if (is_lower) {
|
|
return lp().has_lower_bound(vi, dep, b, is_strict);
|
|
}
|
|
else {
|
|
return lp().has_upper_bound(vi, dep, b, is_strict);
|
|
}
|
|
}
|
|
|
|
bool has_upper_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
|
|
|
|
bool has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
|
|
|
|
bool has_bound(lpvar vi, u_dependency*& dep, rational const& bound, bool is_lower) {
|
|
if (lp().column_has_term(vi)) {
|
|
theory_var v = lp().local_to_external(vi);
|
|
rational val;
|
|
TRACE(arith, tout << lp().get_variable_name(vi) << " " << v << "\n";);
|
|
if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) {
|
|
dep = nullptr;
|
|
return bound == val;
|
|
}
|
|
|
|
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
|
|
if (vec.size() > vi) {
|
|
auto const& [ci, coeff] = vec[vi];
|
|
if (ci == UINT_MAX)
|
|
return false;
|
|
dep = lp().dep_manager().mk_leaf(ci);
|
|
return bound == coeff;
|
|
}
|
|
else {
|
|
return false;
|
|
}
|
|
}
|
|
else {
|
|
bool is_strict = false;
|
|
rational b;
|
|
if (is_lower) {
|
|
return lp().has_lower_bound(vi, dep, b, is_strict) && b == bound && !is_strict;
|
|
}
|
|
else {
|
|
return lp().has_upper_bound(vi, dep, b, is_strict) && b == bound && !is_strict;
|
|
}
|
|
}
|
|
}
|
|
|
|
bool is_equal(theory_var x, theory_var y) const {
|
|
return get_enode(x)->get_root() == get_enode(y)->get_root();
|
|
}
|
|
|
|
unsigned get_num_vars() const { return th.get_num_vars(); }
|
|
|
|
void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2) {
|
|
rational bound(0);
|
|
u_dependency* ci1 = nullptr, *ci2 = nullptr, *ci3 = nullptr, *ci4 = nullptr;
|
|
theory_var v1 = lp().local_to_external(vi1);
|
|
theory_var v2 = lp().local_to_external(vi2);
|
|
TRACE(arith, tout << "fixed: " << pp(v1) << " " << pp(v2) << "\n";);
|
|
// we expect lp() to ensure that none of these returns happen.
|
|
if (is_equal(v1, v2))
|
|
return;
|
|
if (is_int(v1) != is_int(v2))
|
|
return;
|
|
if (!has_lower_bound(vi1, ci1, bound))
|
|
return;
|
|
if (!has_upper_bound(vi1, ci2, bound))
|
|
return;
|
|
if (!has_lower_bound(vi2, ci3, bound))
|
|
return;
|
|
if (!has_upper_bound(vi2, ci4, bound))
|
|
return;
|
|
|
|
reset_evidence();
|
|
set_evidence(ci1, m_core, m_eqs);
|
|
set_evidence(ci2, m_core, m_eqs);
|
|
set_evidence(ci3, m_core, m_eqs);
|
|
set_evidence(ci4, m_core, m_eqs);
|
|
++m_stats.m_fixed_eqs;
|
|
assign_eq(v1, v2);
|
|
}
|
|
|
|
void assign_eq(theory_var v1, theory_var v2) {
|
|
enode* x = get_enode(v1);
|
|
enode* y = get_enode(v2);
|
|
justification* js =
|
|
ctx().mk_justification(
|
|
ext_theory_eq_propagation_justification(
|
|
get_id(), ctx(), m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), x, y));
|
|
|
|
TRACE(arith,
|
|
for (auto c : m_core)
|
|
ctx().display_detailed_literal(tout << ctx().get_assign_level(c.var()) << " " << c << " ", c) << "\n";
|
|
for (auto e : m_eqs)
|
|
tout << pp(e.first) << " = " << pp(e.second) << "\n";
|
|
tout << " ==> " << pp(x) << " = " << pp(y) << "\n";
|
|
);
|
|
|
|
std::function<expr*(void)> fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); };
|
|
scoped_trace_stream _sts(th, fn);
|
|
|
|
if (params().m_arith_validate)
|
|
VERIFY(validate_eq(x, y));
|
|
ctx().assign_eq(x, y, eq_justification(js));
|
|
}
|
|
|
|
void fixed_var_eh(theory_var v, lp::lpvar t, u_dependency* dep, rational const& bound) {
|
|
theory_var w = null_theory_var;
|
|
enode* x = get_enode(v);
|
|
if (m_value2var.find(bound, w))
|
|
;
|
|
else if (bound.is_zero())
|
|
w = lp().local_to_external(get_zero(a.is_int(x->get_expr())));
|
|
else if (bound.is_one())
|
|
w = lp().local_to_external(get_one(a.is_int(x->get_expr())));
|
|
else
|
|
return;
|
|
enode* y = get_enode(w);
|
|
TRACE(arith, tout << pp(x) << " == " << pp(y) << "\n");
|
|
if (x->get_sort() != y->get_sort())
|
|
return;
|
|
if (x->get_root() == y->get_root())
|
|
return;
|
|
reset_evidence();
|
|
set_evidence(dep, m_core, m_eqs);
|
|
++m_stats.m_fixed_eqs;
|
|
assign_eq(v, w);
|
|
}
|
|
|
|
lbool make_feasible() {
|
|
TRACE(pcs, tout << lp().constraints(););
|
|
TRACE(arith_verbose, tout << "before calling lp().find_feasible_solution()\n"; display(tout););
|
|
auto status = lp().find_feasible_solution();
|
|
TRACE(arith_verbose, display(tout););
|
|
if (lp().is_feasible())
|
|
return l_true;
|
|
if (status == lp::lp_status::INFEASIBLE)
|
|
return l_false;
|
|
TRACE(arith, tout << "status treated as inconclusive: " << status << "\n";);
|
|
// TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED,
|
|
// TIME_EXAUSTED, EMPTY, UNSTABLE
|
|
return l_undef;
|
|
}
|
|
|
|
lp::explanation m_explanation;
|
|
literal_vector m_core;
|
|
svector<enode_pair> m_eqs;
|
|
vector<parameter> m_params;
|
|
|
|
void reset_evidence() {
|
|
m_core.reset();
|
|
m_eqs.reset();
|
|
m_params.reset();
|
|
}
|
|
|
|
// lp::constraint_index const null_constraint_index = UINT_MAX; // not sure what a correct fix is
|
|
|
|
void set_evidence(u_dependency* dep, literal_vector& core, svector<enode_pair>& eqs) {
|
|
for (auto ci : lp().flatten(dep))
|
|
set_evidence(ci, core, eqs);
|
|
}
|
|
|
|
void set_evidence(lp::constraint_index idx, literal_vector& core, svector<enode_pair>& eqs) {
|
|
if (idx == UINT_MAX)
|
|
return;
|
|
switch (m_constraint_sources[idx]) {
|
|
case inequality_source: {
|
|
literal lit = m_inequalities[idx];
|
|
SASSERT(lit != null_literal);
|
|
core.push_back(lit);
|
|
break;
|
|
}
|
|
case equality_source: {
|
|
SASSERT(m_equalities[idx].first != nullptr);
|
|
SASSERT(m_equalities[idx].second != nullptr);
|
|
m_eqs.push_back(m_equalities[idx]);
|
|
break;
|
|
}
|
|
case definition_source: {
|
|
// skip definitions (these are treated as hard constraints)
|
|
break;
|
|
}
|
|
default:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
}
|
|
|
|
void get_infeasibility_explanation_and_set_conflict() {
|
|
m_explanation.clear();
|
|
lp().get_infeasibility_explanation(m_explanation);
|
|
set_conflict();
|
|
}
|
|
|
|
void set_conflict() {
|
|
literal_vector core;
|
|
set_conflict_or_lemma(core, true);
|
|
}
|
|
|
|
void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
|
|
reset_evidence();
|
|
for (literal lit : core) {
|
|
m_core.push_back(lit);
|
|
}
|
|
// lp().shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed
|
|
++m_num_conflicts;
|
|
++m_stats.m_conflicts;
|
|
TRACE(arith_conflict,
|
|
tout << "@" << ctx().get_scope_level() << (is_conflict ? " conflict":" lemma");
|
|
for (auto const& p : m_params) tout << " " << p;
|
|
tout << "\n";
|
|
display_evidence(tout << core << " ", m_explanation););
|
|
for (auto ev : m_explanation)
|
|
set_evidence(ev.ci(), m_core, m_eqs);
|
|
|
|
|
|
if (params().m_arith_validate)
|
|
VERIFY(validate_conflict());
|
|
if (params().m_arith_dump_lemmas)
|
|
dump_conflict();
|
|
|
|
if (is_conflict) {
|
|
ctx().set_conflict(
|
|
ctx().mk_justification(
|
|
ext_theory_conflict_justification(
|
|
get_id(), ctx(),
|
|
m_core.size(), m_core.data(),
|
|
m_eqs.size(), m_eqs.data(), m_params.size(), m_params.data())));
|
|
}
|
|
else {
|
|
for (auto const& eq : m_eqs) {
|
|
m_core.push_back(th.mk_eq(eq.first->get_expr(), eq.second->get_expr(), false));
|
|
}
|
|
for (literal & c : m_core) {
|
|
c.neg();
|
|
ctx().mark_as_relevant(c);
|
|
if (ctx().get_assignment(c) == l_true)
|
|
return;
|
|
}
|
|
TRACE(arith, ctx().display_literals_verbose(tout, m_core) << "\n";);
|
|
ctx().mk_th_axiom(get_id(), m_core.size(), m_core.data());
|
|
}
|
|
}
|
|
|
|
justification * why_is_diseq(theory_var v1, theory_var v2) {
|
|
return nullptr;
|
|
}
|
|
|
|
void reset_eh() {
|
|
m_arith_eq_adapter.reset_eh();
|
|
m_solver = nullptr;
|
|
m_internalize_head = 0;
|
|
m_not_handled.reset();
|
|
del_bounds(0);
|
|
m_unassigned_bounds.reset();
|
|
m_asserted_qhead = 0;
|
|
m_assume_eq_head = 0;
|
|
m_scopes.reset();
|
|
m_stats.reset();
|
|
m_model_is_initialized = false;
|
|
}
|
|
|
|
void init_model(model_generator & mg) {
|
|
init_variable_values();
|
|
m_factory = alloc(arith_factory, m);
|
|
mg.register_factory(m_factory);
|
|
if (m_model_is_initialized) {
|
|
expr_ref val(m);
|
|
unsigned nv = th.get_num_vars();
|
|
for (unsigned v = 0; v < nv; ++v)
|
|
if (get_value(get_enode(v), val))
|
|
m_factory->register_value(val);
|
|
|
|
}
|
|
TRACE(arith, display(tout););
|
|
}
|
|
|
|
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
|
|
SASSERT(use_nra_model());
|
|
auto t = get_lpvar(v);
|
|
if (!lp().column_has_term(t))
|
|
m_nla->am().set(r, m_nla->am_value(t));
|
|
else {
|
|
|
|
m_todo_terms.push_back({t, rational::one()});
|
|
TRACE(nl_value, tout << "v" << v << " " << t << "\n";);
|
|
TRACE(nl_value, tout << "v" << v << " := w" << t << "\n";
|
|
lp().print_term(lp().get_term(t), tout) << "\n";);
|
|
|
|
m_nla->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(nl_value, lp().print_term(term, tout) << "\n";);
|
|
scoped_anum r1(m_nla->am());
|
|
rational c1(0);
|
|
m_nla->am().set(r1, c1.to_mpq());
|
|
m_nla->am().add(r, r1, r);
|
|
for (lp::lar_term::ival arg : term) {
|
|
auto wi = arg.j();
|
|
c1 = arg.coeff() * wcoeff;
|
|
if (lp().column_has_term(wi)) {
|
|
m_todo_terms.push_back({wi, c1});
|
|
}
|
|
else {
|
|
m_nla->am().set(r1, c1.to_mpq());
|
|
m_nla->am().mul(m_nla->am_value(wi), r1, r1);
|
|
m_nla->am().add(r1, r, r);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
return r;
|
|
}
|
|
|
|
model_value_proc * mk_value(enode * n, model_generator & mg) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
expr* o = n->get_expr();
|
|
if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) {
|
|
anum const& an = nl_value(v, m_nla->tmp1());
|
|
if (a.is_int(o) && !m_nla->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(m_nla->am(), nl_value(v, m_nla->tmp1()), 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().is_canceled()));
|
|
if (a.is_int(o) && !r.is_int()) r = floor(r);
|
|
return alloc(expr_wrapper_proc, m_factory->mk_value(r, o->get_sort()));
|
|
}
|
|
}
|
|
|
|
bool get_value(enode* n, rational& val) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (!is_registered_var(v)) return false;
|
|
lpvar vi = get_lpvar(v);
|
|
if (lp().has_value(vi, val)) {
|
|
TRACE(arith, tout << expr_ref(n->get_expr(), m) << " := " << val << "\n";);
|
|
if (is_int(n) && !val.is_int()) return false;
|
|
return true;
|
|
}
|
|
else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool get_value(enode* n, expr_ref& r) {
|
|
rational val;
|
|
if (get_value(n, val)) {
|
|
r = a.mk_numeral(val, is_int(n));
|
|
return true;
|
|
}
|
|
else {
|
|
return false;
|
|
}
|
|
}
|
|
|
|
bool include_func_interp(func_decl* f) {
|
|
return
|
|
a.is_div0(f) ||
|
|
a.is_idiv0(f) ||
|
|
a.is_power0(f) ||
|
|
a.is_rem0(f) ||
|
|
a.is_mod0(f);
|
|
}
|
|
|
|
bool include_func_interp(enode* n) {
|
|
return include_func_interp(n->get_decl());
|
|
}
|
|
|
|
bool get_lower(enode* n, rational& val, bool& is_strict) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (!is_registered_var(v))
|
|
return false;
|
|
lpvar vi = get_lpvar(v);
|
|
u_dependency* ci;
|
|
return lp().has_lower_bound(vi, ci, val, is_strict);
|
|
}
|
|
|
|
bool get_lower(enode* n, expr_ref& r) {
|
|
bool is_strict;
|
|
rational val;
|
|
if (get_lower(n, val, is_strict) && !is_strict) {
|
|
r = a.mk_numeral(val, is_int(n));
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
bool get_upper(enode* n, rational& val, bool& is_strict) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (!is_registered_var(v))
|
|
return false;
|
|
lpvar vi = get_lpvar(v);
|
|
u_dependency* dep = nullptr;
|
|
return lp().has_upper_bound(vi, dep, val, is_strict);
|
|
}
|
|
|
|
void solve_fixed(enode* n, lpvar j, expr_ref& term, expr_ref& guard) {
|
|
term = a.mk_numeral(lp().get_value(j), a.is_int(n->get_expr()));
|
|
reset_evidence();
|
|
add_explain(j);
|
|
guard = mk_and(extract_explain());
|
|
}
|
|
|
|
void add_explain(unsigned j) {
|
|
auto d = lp().get_bound_constraint_witnesses_for_column(j);
|
|
set_evidence(d, m_core, m_eqs);
|
|
}
|
|
|
|
expr_ref_vector extract_explain() {
|
|
expr_ref_vector es(m);
|
|
for (auto [l, r] : m_eqs)
|
|
es.push_back(a.mk_eq(l->get_expr(), r->get_expr()));
|
|
for (auto l : m_core)
|
|
es.push_back(ctx().literal2expr(l));
|
|
// remove duplicats from es:
|
|
std::stable_sort(es.data(), es.data() + es.size());
|
|
unsigned j = 0;
|
|
for (unsigned i = 0; i < es.size(); ++i) {
|
|
if (i > 0 && es.get(i) == es.get(i - 1))
|
|
continue;
|
|
es[j++] = es.get(i);
|
|
}
|
|
es.shrink(j);
|
|
return es;
|
|
}
|
|
|
|
void solve_term(enode* n, lp::lar_term & lt, expr_ref& term, expr_ref& guard) {
|
|
bool is_int = a.is_int(n->get_expr());
|
|
bool all_int = is_int;
|
|
lp::lar_term t;
|
|
rational coeff(0), lc(1);
|
|
expr_ref_vector guards(m);
|
|
reset_evidence();
|
|
// extract coeff
|
|
for (auto const& cv : lt) {
|
|
all_int &= lp().column_is_int(cv.j());
|
|
if (lp().column_is_fixed(cv.j())) {
|
|
coeff += lp().get_value(cv.j()) * cv.coeff();
|
|
add_explain(cv.j());
|
|
}
|
|
else {
|
|
t.add_monomial(cv.coeff(), cv.j());
|
|
lc = lcm(denominator(cv.coeff()), lc);
|
|
}
|
|
}
|
|
// extract lc
|
|
lc = lcm(lc, denominator(coeff));
|
|
|
|
guards.append(extract_explain());
|
|
if (lc != 1)
|
|
t *= lc, coeff *= lc;
|
|
term = mk_term(t, is_int);
|
|
if (coeff != 0)
|
|
term = a.mk_add(term, a.mk_numeral(coeff, is_int));
|
|
|
|
if (lc == 1) {
|
|
guard = mk_and(guards);
|
|
return;
|
|
}
|
|
expr_ref lce(a.mk_numeral(lc, is_int), m);
|
|
if (all_int)
|
|
guards.push_back(m.mk_eq(a.mk_mod(term, lce), a.mk_int(0)));
|
|
else if (is_int)
|
|
guards.push_back(a.mk_is_int(a.mk_div(term, lce)));
|
|
if (is_int)
|
|
term = a.mk_idiv(term, lce);
|
|
else
|
|
term = a.mk_div(term, lce);
|
|
guard = mk_and(guards);
|
|
}
|
|
|
|
void solve_for(vector<solution>& solutions) {
|
|
unsigned_vector vars;
|
|
unsigned j = 0;
|
|
for (auto [e, t, g] : solutions) {
|
|
if (!ctx().e_internalized(e))
|
|
continue;
|
|
auto n = get_enode(e);
|
|
if (!n) {
|
|
solutions[j++] = { e, t, g };
|
|
continue;
|
|
}
|
|
|
|
theory_var v = n->get_th_var(get_id());
|
|
if (!is_registered_var(v))
|
|
solutions[j++] = { e, t, g };
|
|
else
|
|
vars.push_back(get_lpvar(v));
|
|
}
|
|
solutions.shrink(j);
|
|
|
|
expr_ref term(m), guard(m);
|
|
vector<lp::lar_solver::solution> sols;
|
|
lp().solve_for(vars, sols);
|
|
uint_set seen;
|
|
for (auto& s : sols) {
|
|
auto n = get_enode(lp().local_to_external(s.j));
|
|
if (lp().column_is_fixed(s.j))
|
|
solve_fixed(n, s.j, term, guard);
|
|
else
|
|
solve_term(n, s.t, term, guard);
|
|
solutions.push_back({ n->get_expr(), term, guard});
|
|
seen.insert(s.j);
|
|
}
|
|
for (auto j : vars) {
|
|
if (seen.contains(j) || !lp().column_is_fixed(j))
|
|
continue;
|
|
auto n = get_enode(lp().local_to_external(j));
|
|
solve_fixed(n, j, term, guard);
|
|
solutions.push_back({ n->get_expr(), term, guard });
|
|
}
|
|
}
|
|
|
|
bool get_upper(enode* n, expr_ref& r) {
|
|
bool is_strict;
|
|
rational val;
|
|
if (get_upper(n, val, is_strict) && !is_strict) {
|
|
r = a.mk_numeral(val, is_int(n));
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
// Auxiliary verification utilities.
|
|
|
|
struct scoped_arith_mode {
|
|
smt_params& p;
|
|
scoped_arith_mode(smt_params& p) : p(p) {
|
|
p.m_arith_mode = arith_solver_id::AS_OLD_ARITH;
|
|
}
|
|
~scoped_arith_mode() {
|
|
p.m_arith_mode = arith_solver_id::AS_NEW_ARITH;
|
|
}
|
|
};
|
|
|
|
unsigned m_num_dumped_lemmas = 0;
|
|
|
|
void dump_assign_lemma(literal lit) {
|
|
std::cout << "(echo \"assign lemma " << (m_num_dumped_lemmas++) << "\")\n";
|
|
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
|
|
std::cout << "(reset)\n";
|
|
}
|
|
|
|
void dump_conflict() {
|
|
std::cout << "(echo \"conflict " << (m_num_dumped_lemmas++) << "\")\n";
|
|
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data());
|
|
std::cout << "(reset)\n";
|
|
}
|
|
|
|
void dump_eq(enode* x, enode* y) {
|
|
std::cout << "(echo \"equality propagation " << (m_num_dumped_lemmas++) << "\")\n";
|
|
ctx().display_lemma_as_smt_problem(std::cout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal, symbol::null, x, y);
|
|
std::cout << "(reset)\n";
|
|
}
|
|
|
|
|
|
bool validate_conflict() {
|
|
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
|
|
|
|
VERIFY(!m_core.empty() || !m_eqs.empty());
|
|
scoped_arith_mode _sa(ctx().get_fparams());
|
|
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
|
add_background(nctx);
|
|
cancel_eh<reslimit> eh(m.limit());
|
|
scoped_timer timer(1000, &eh);
|
|
bool result = l_true != nctx.check();
|
|
CTRACE(arith, !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), false_literal););
|
|
return result;
|
|
}
|
|
|
|
bool validate_assign(literal lit) {
|
|
if (params().m_arith_mode != arith_solver_id::AS_NEW_ARITH) return true;
|
|
scoped_arith_mode _sa(ctx().get_fparams());
|
|
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
|
m_core.push_back(~lit);
|
|
add_background(nctx);
|
|
m_core.pop_back();
|
|
cancel_eh<reslimit> eh(m.limit());
|
|
scoped_timer timer(1000, &eh);
|
|
bool result = l_true != nctx.check();
|
|
CTRACE(arith, !result, ctx().display_lemma_as_smt_problem(tout, m_core.size(), m_core.data(), m_eqs.size(), m_eqs.data(), lit);
|
|
display(tout););
|
|
return result;
|
|
}
|
|
|
|
bool validate_eq(enode* x, enode* y) {
|
|
static bool s_validating = false;
|
|
if (s_validating)
|
|
return true;
|
|
flet<bool> _svalid(s_validating, true);
|
|
context nctx(m, ctx().get_fparams(), ctx().get_params());
|
|
add_background(nctx);
|
|
expr_ref neq(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())), m);
|
|
nctx.assert_expr(neq);
|
|
cancel_eh<reslimit> eh(m.limit());
|
|
scoped_timer timer(1000, &eh);
|
|
lbool r = nctx.check();
|
|
if (r == l_true) {
|
|
nctx.display_asserted_formulas(std::cout);
|
|
std::cout.flush();
|
|
}
|
|
return l_true != r;
|
|
}
|
|
|
|
void add_background(context& nctx) {
|
|
for (literal c : m_core) {
|
|
expr_ref tmp(m);
|
|
ctx().literal2expr(c, tmp);
|
|
nctx.assert_expr(tmp);
|
|
}
|
|
for (auto const& eq : m_eqs) {
|
|
nctx.assert_expr(m.mk_eq(eq.first->get_expr(), eq.second->get_expr()));
|
|
}
|
|
}
|
|
|
|
theory_lra::inf_eps value(theory_var v) {
|
|
lp::impq ival = get_ivalue(v);
|
|
return inf_eps(rational(0), inf_rational(ival.x, ival.y));
|
|
}
|
|
|
|
theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
|
|
unsigned level = 2;
|
|
lp::impq term_max;
|
|
lp::lp_status st;
|
|
lpvar vi = 0;
|
|
if (has_int()) {
|
|
lp().backup_x();
|
|
}
|
|
if (!is_registered_var(v)) {
|
|
TRACE(arith, tout << "cannot get bound for v" << v << "\n";);
|
|
st = lp::lp_status::UNBOUNDED;
|
|
}
|
|
else if (!m.limit().inc()) {
|
|
st = lp::lp_status::UNBOUNDED;
|
|
}
|
|
else {
|
|
if (!lp().is_feasible() || lp().has_changed_columns())
|
|
make_feasible();
|
|
|
|
vi = get_lpvar(v);
|
|
|
|
st = lp().maximize_term(vi, term_max);
|
|
|
|
if (has_int() && lp().has_inf_int()) {
|
|
st = lp::lp_status::FEASIBLE;
|
|
lp().restore_x();
|
|
}
|
|
if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
|
|
switch (check_nla(level)) {
|
|
case FC_DONE:
|
|
st = lp::lp_status::FEASIBLE;
|
|
break;
|
|
case FC_GIVEUP:
|
|
case FC_CONTINUE:
|
|
st = lp::lp_status::UNBOUNDED;
|
|
break;
|
|
}
|
|
lp().restore_x();
|
|
}
|
|
}
|
|
switch (st) {
|
|
case lp::lp_status::OPTIMAL: {
|
|
init_variable_values();
|
|
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
|
|
auto val = value(v);
|
|
blocker = mk_gt(v);
|
|
return val;
|
|
}
|
|
case lp::lp_status::FEASIBLE: {
|
|
auto val = value(v);
|
|
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
|
|
blocker = mk_gt(v);
|
|
return val;
|
|
}
|
|
default:
|
|
SASSERT(st == lp::lp_status::UNBOUNDED);
|
|
TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
|
|
has_shared = false;
|
|
blocker = m.mk_false();
|
|
return inf_eps(rational::one(), inf_rational());
|
|
}
|
|
}
|
|
|
|
expr_ref mk_gt(theory_var v) {
|
|
lp::impq val = get_ivalue(v);
|
|
expr* obj = get_enode(v)->get_expr();
|
|
rational r = val.x;
|
|
expr_ref e(m);
|
|
if (a.is_int(obj->get_sort())) {
|
|
if (r.is_int())
|
|
r += rational::one();
|
|
else
|
|
r = ceil(r);
|
|
e = a.mk_numeral(r, obj->get_sort());
|
|
e = a.mk_ge(obj, e);
|
|
}
|
|
else {
|
|
e = a.mk_numeral(r, obj->get_sort());
|
|
if (val.y.is_neg())
|
|
e = a.mk_ge(obj, e);
|
|
else
|
|
e = a.mk_gt(obj, e);
|
|
}
|
|
TRACE(opt, tout << "v" << v << " " << val << " " << r << " " << e << "\n";);
|
|
return e;
|
|
}
|
|
|
|
theory_var add_objective(app* term) {
|
|
TRACE(opt, tout << expr_ref(term, m) << "\n";);
|
|
theory_var v = internalize_def(term);
|
|
register_theory_var_in_lar_solver(v);
|
|
return v;
|
|
}
|
|
|
|
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs) {
|
|
term2coeffs(term, coeffs, rational::one());
|
|
}
|
|
|
|
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
|
|
TRACE(arith, lp().print_term(term, tout) << "\n";);
|
|
for (lp::lar_term::ival ti : term) {
|
|
theory_var w;
|
|
auto tv = ti.j();
|
|
if (lp().column_has_term(tv)) {
|
|
lp::lar_term const& term1 = lp().get_term(tv);
|
|
rational coeff2 = coeff * ti.coeff();
|
|
term2coeffs(term1, coeffs, coeff2);
|
|
continue;
|
|
}
|
|
else {
|
|
w = lp().local_to_external(tv);
|
|
SASSERT(w >= 0);
|
|
TRACE(arith, tout << tv << ": " << w << "\n";);
|
|
}
|
|
rational c0(0);
|
|
coeffs.find(w, c0);
|
|
coeffs.insert(w, c0 + ti.coeff() * coeff);
|
|
}
|
|
}
|
|
|
|
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int) {
|
|
expr_ref_vector args(m);
|
|
for (auto const& [w, coeff] : coeffs) {
|
|
expr* o = get_enode(w)->get_expr();
|
|
if (coeff.is_zero()) {
|
|
// continue
|
|
}
|
|
else if (coeff.is_one()) {
|
|
args.push_back(o);
|
|
}
|
|
else {
|
|
args.push_back(a.mk_mul(a.mk_numeral(coeff, is_int), o));
|
|
}
|
|
}
|
|
if (!offset.is_zero()) {
|
|
args.push_back(a.mk_numeral(offset, is_int));
|
|
}
|
|
switch (args.size()) {
|
|
case 0:
|
|
return app_ref(a.mk_numeral(rational::zero(), is_int), m);
|
|
case 1:
|
|
return app_ref(to_app(args[0].get()), m);
|
|
default:
|
|
return app_ref(a.mk_add(args.size(), args.data()), m);
|
|
}
|
|
}
|
|
|
|
app_ref mk_term(lp::lar_term const& term, bool is_int) {
|
|
u_map<rational> coeffs;
|
|
term2coeffs(term, coeffs);
|
|
return coeffs2app(coeffs, rational::zero(), is_int);
|
|
}
|
|
|
|
rational gcd_reduce(u_map<rational>& coeffs) {
|
|
rational g(0);
|
|
for (auto const& kv : coeffs) {
|
|
g = gcd(g, kv.m_value);
|
|
}
|
|
if (g.is_zero())
|
|
return rational::one();
|
|
if (!g.is_one()) {
|
|
for (auto& kv : coeffs) {
|
|
kv.m_value /= g;
|
|
}
|
|
}
|
|
return g;
|
|
}
|
|
|
|
app_ref mk_obj(theory_var v) {
|
|
auto t = get_lpvar(v);
|
|
bool is_int = a.is_int(get_enode(v)->get_expr());
|
|
if (lp().column_has_term(t)) {
|
|
return mk_term(lp().get_term(t), is_int);
|
|
}
|
|
else {
|
|
// theory_var w = lp().external_to_local(vi);
|
|
return app_ref(get_enode(v)->get_expr(), m);
|
|
}
|
|
}
|
|
|
|
expr_ref mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
|
|
rational r = val.get_rational();
|
|
bool is_strict = val.get_infinitesimal().is_pos();
|
|
app_ref b(m);
|
|
bool is_int = a.is_int(get_enode(v)->get_expr());
|
|
TRACE(arith, display(tout << "v" << v << "\n"););
|
|
if (is_strict) {
|
|
b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int));
|
|
}
|
|
else {
|
|
b = a.mk_ge(mk_obj(v), a.mk_numeral(r, is_int));
|
|
}
|
|
if (!ctx().b_internalized(b)) {
|
|
fm.hide(b->get_decl());
|
|
bool_var bv = ctx().mk_bool_var(b);
|
|
m_bool_var2bound.erase(bv);
|
|
ctx().set_var_theory(bv, get_id());
|
|
// ctx().set_enode_flag(bv, true);
|
|
lp_api::bound_kind bkind = lp_api::bound_kind::lower_t;
|
|
if (is_strict) bkind = lp_api::bound_kind::upper_t;
|
|
api_bound* a = mk_var_bound(bv, v, bkind, r);
|
|
mk_bound_axioms(*a);
|
|
updt_unassigned_bounds(v, +1);
|
|
m_bounds[v].push_back(a);
|
|
m_bounds_trail.push_back(v);
|
|
m_bool_var2bound.insert(bv, a);
|
|
|
|
TRACE(arith, tout << "internalized " << bv << ": " << mk_pp(b, m) << "\n";);
|
|
}
|
|
if (is_strict) {
|
|
b = m.mk_not(b);
|
|
}
|
|
TRACE(arith, tout << b << "\n";);
|
|
return expr_ref(b, m);
|
|
}
|
|
|
|
|
|
void display(std::ostream & out) const {
|
|
out << "Theory arithmetic:\n";
|
|
if (m_solver) {
|
|
m_solver->display(out);
|
|
}
|
|
if (m_nla) {
|
|
m_nla->display(out);
|
|
}
|
|
unsigned nv = th.get_num_vars();
|
|
for (unsigned v = 0; v < nv; ++v) {
|
|
auto vi = get_lpvar(v);
|
|
if (!ctx().is_relevant(get_enode(v))) out << "irr: ";
|
|
out << "v" << v << " ";
|
|
if (vi == lp::null_lpvar) out << "null"; else out << (lp().column_has_term(vi) ? "t":"j") << vi;
|
|
if (use_nra_model() && is_registered_var(v)) m_nla->am().display(out << " = ", nl_value(v, m_nla->tmp1()));
|
|
else if (can_get_value(v)) out << " = " << get_value(v);
|
|
if (is_int(v)) out << ", int";
|
|
if (ctx().is_shared(get_enode(v))) out << ", shared";
|
|
out << " := " << pp(v) << "\n";
|
|
}
|
|
}
|
|
|
|
void display_evidence(std::ostream& out, lp::explanation const& evidence) {
|
|
for (auto ev : evidence) {
|
|
expr_ref e(m);
|
|
SASSERT(!ev.coeff().is_zero());
|
|
if (ev.coeff().is_zero()) {
|
|
continue;
|
|
}
|
|
unsigned idx = ev.ci();
|
|
switch (m_constraint_sources.get(idx, null_source)) {
|
|
case inequality_source: {
|
|
literal lit = m_inequalities[idx];
|
|
ctx().literal2expr(lit, e);
|
|
out << bpp(e) << " " << ctx().get_assignment(lit) << "\n";
|
|
break;
|
|
}
|
|
case equality_source:
|
|
out << pp(m_equalities[idx].first) << " = "
|
|
<< pp(m_equalities[idx].second) << "\n";
|
|
break;
|
|
case definition_source: {
|
|
theory_var v = m_definitions[idx];
|
|
if (v != null_theory_var)
|
|
out << "def: v" << v << " := " << pp(th.get_enode(v)) << "\n";
|
|
break;
|
|
}
|
|
case null_source:
|
|
out << idx << " null";
|
|
break;
|
|
default:
|
|
UNREACHABLE();
|
|
break;
|
|
}
|
|
}
|
|
for (lp::explanation::cimpq ev : evidence)
|
|
lp().constraints().display(out << ev.coeff() << ": ", ev.ci());
|
|
}
|
|
|
|
void collect_statistics(::statistics & st) const {
|
|
m_arith_eq_adapter.collect_statistics(st);
|
|
m_stats.collect_statistics(st);
|
|
lp().settings().stats().collect_statistics(st);
|
|
}
|
|
|
|
/*
|
|
* Facility to put a small box around integer variables used in branch and bounds.
|
|
*/
|
|
|
|
unsigned m_bounded_range_idx; // current size of bounded range.
|
|
literal m_bounded_range_lit; // current bounded range literal
|
|
expr_ref_vector m_bound_terms; // predicates used for bounds
|
|
expr_ref m_bound_predicate;
|
|
|
|
unsigned init_range() const { return 5; }
|
|
unsigned max_range() const { return 20; }
|
|
|
|
|
|
void setup() {
|
|
m_bounded_range_lit = null_literal;
|
|
m_bound_terms.reset();
|
|
m_bound_predicate = nullptr;
|
|
}
|
|
|
|
void updt_params() {
|
|
if (m_solver)
|
|
m_solver->updt_params(ctx().get_params());
|
|
if (m_nla)
|
|
m_nla->updt_params(ctx().get_params());
|
|
}
|
|
|
|
|
|
void validate_model(proto_model& mdl) {
|
|
|
|
rational r1, r2;
|
|
expr_ref res(m);
|
|
if (!m_model_is_initialized)
|
|
return;
|
|
for (unsigned v = 0; v < th.get_num_vars(); ++v) {
|
|
if (!is_registered_var(v))
|
|
continue;
|
|
enode* n = get_enode(v);
|
|
if (!n)
|
|
continue;
|
|
if (!th.is_relevant_and_shared(n))
|
|
continue;
|
|
rational r1 = get_value(v);
|
|
if (!mdl.eval(n->get_expr(), res, false))
|
|
continue;
|
|
if (!a.is_numeral(res, r2))
|
|
continue;
|
|
if (r1 != r2)
|
|
IF_VERBOSE(1, verbose_stream() << enode_pp(n, ctx()) << " evaluates to " << r2 << " but arith solver has " << r1 << "\n");
|
|
}
|
|
}
|
|
|
|
};
|
|
|
|
theory_lra::theory_lra(context& ctx):
|
|
theory(ctx, ctx.get_manager().get_family_id("arith")) {
|
|
m_imp = alloc(imp, *this, ctx.get_manager());
|
|
}
|
|
theory_lra::~theory_lra() {
|
|
dealloc(m_imp);
|
|
}
|
|
theory* theory_lra::mk_fresh(context* new_ctx) {
|
|
return alloc(theory_lra, *new_ctx);
|
|
}
|
|
void theory_lra::init() {
|
|
m_imp->init();
|
|
}
|
|
bool theory_lra::internalize_atom(app * atom, bool gate_ctx) {
|
|
return m_imp->internalize_atom(atom, gate_ctx);
|
|
}
|
|
bool theory_lra::internalize_term(app * term) {
|
|
return m_imp->internalize_term(term);
|
|
}
|
|
void theory_lra::internalize_eq_eh(app * atom, bool_var v) {
|
|
m_imp->internalize_eq_eh(atom, v);
|
|
}
|
|
void theory_lra::assign_eh(bool_var v, bool is_true) {
|
|
m_imp->assign_eh(v, is_true);
|
|
}
|
|
lbool theory_lra::get_phase(bool_var v) {
|
|
return m_imp->get_phase(v);
|
|
}
|
|
void theory_lra::initialize_value(expr* var, expr* value) {
|
|
m_imp->initialize_value(var, value);
|
|
}
|
|
void theory_lra::new_eq_eh(theory_var v1, theory_var v2) {
|
|
m_imp->new_eq_eh(v1, v2);
|
|
}
|
|
bool theory_lra::use_diseqs() const {
|
|
return m_imp->use_diseqs();
|
|
}
|
|
void theory_lra::new_diseq_eh(theory_var v1, theory_var v2) {
|
|
m_imp->new_diseq_eh(v1, v2);
|
|
}
|
|
void theory_lra::apply_sort_cnstr(enode* n, sort* s) {
|
|
m_imp->apply_sort_cnstr(n, s);
|
|
}
|
|
void theory_lra::push_scope_eh() {
|
|
theory::push_scope_eh();
|
|
m_imp->push_scope_eh();
|
|
}
|
|
void theory_lra::pop_scope_eh(unsigned num_scopes) {
|
|
m_imp->pop_scope_eh(num_scopes);
|
|
theory::pop_scope_eh(num_scopes);
|
|
}
|
|
void theory_lra::restart_eh() {
|
|
m_imp->restart_eh();
|
|
}
|
|
void theory_lra::relevant_eh(app* e) {
|
|
m_imp->relevant_eh(e);
|
|
}
|
|
void theory_lra::init_search_eh() {
|
|
m_imp->init_search_eh();
|
|
}
|
|
final_check_status theory_lra::final_check_eh(unsigned level) {
|
|
return m_imp->final_check_eh(level);
|
|
}
|
|
bool theory_lra::is_shared(theory_var v) const {
|
|
return m_imp->is_shared(v);
|
|
}
|
|
bool theory_lra::can_propagate() {
|
|
return m_imp->can_propagate();
|
|
}
|
|
void theory_lra::propagate() {
|
|
m_imp->propagate();
|
|
}
|
|
justification * theory_lra::why_is_diseq(theory_var v1, theory_var v2) {
|
|
return m_imp->why_is_diseq(v1, v2);
|
|
}
|
|
void theory_lra::reset_eh() {
|
|
m_imp->reset_eh();
|
|
}
|
|
void theory_lra::init_model(model_generator & m) {
|
|
m_imp->init_model(m);
|
|
}
|
|
model_value_proc * theory_lra::mk_value(enode * n, model_generator & mg) {
|
|
return m_imp->mk_value(n, mg);
|
|
}
|
|
bool theory_lra::get_value(enode* n, rational& r) {
|
|
return m_imp->get_value(n, r);
|
|
}
|
|
bool theory_lra::get_value(enode* n, expr_ref& r) {
|
|
return m_imp->get_value(n, r);
|
|
}
|
|
bool theory_lra::include_func_interp(func_decl* f) {
|
|
return m_imp->include_func_interp(f);
|
|
}
|
|
bool theory_lra::get_lower(enode* n, expr_ref& r) {
|
|
return m_imp->get_lower(n, r);
|
|
}
|
|
bool theory_lra::get_upper(enode* n, expr_ref& r) {
|
|
return m_imp->get_upper(n, r);
|
|
}
|
|
bool theory_lra::get_lower(enode* n, rational& r, bool& is_strict) {
|
|
return m_imp->get_lower(n, r, is_strict);
|
|
}
|
|
bool theory_lra::get_upper(enode* n, rational& r, bool& is_strict) {
|
|
return m_imp->get_upper(n, r, is_strict);
|
|
}
|
|
|
|
void theory_lra::solve_for(vector<solution>& sol) {
|
|
m_imp->solve_for(sol);
|
|
}
|
|
|
|
void theory_lra::display(std::ostream & out) const {
|
|
m_imp->display(out);
|
|
}
|
|
void theory_lra::collect_statistics(::statistics & st) const {
|
|
m_imp->collect_statistics(st);
|
|
}
|
|
theory_lra::inf_eps theory_lra::value(theory_var v) {
|
|
return m_imp->value(v);
|
|
}
|
|
theory_lra::inf_eps theory_lra::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
|
|
return m_imp->maximize(v, blocker, has_shared);
|
|
}
|
|
theory_var theory_lra::add_objective(app* term) {
|
|
return m_imp->add_objective(term);
|
|
}
|
|
expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_rational const& val) {
|
|
return m_imp->mk_ge(fm, v, val);
|
|
}
|
|
|
|
void theory_lra::setup() {
|
|
m_imp->setup();
|
|
}
|
|
|
|
void theory_lra::updt_params() {
|
|
m_imp->updt_params();
|
|
}
|
|
|
|
void theory_lra::validate_model(proto_model& mdl) {
|
|
m_imp->validate_model(mdl);
|
|
}
|
|
|
|
lbool theory_lra::check_lp_feasible(vector<std::pair<bool, expr_ref>>& ineqs, literal_vector& lit_core, enode_pair_vector& eq_core) {
|
|
return m_imp->check_lp_feasible(ineqs, lit_core, eq_core);
|
|
}
|
|
|
|
}
|
|
template class lp::lp_bound_propagator<smt::theory_lra::imp>;
|
|
template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
|
|
template void lp::lar_solver::check_missed_propagations<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
|
|
template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(const lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
|
|
template unsigned lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned, lp::lp_bound_propagator<smt::theory_lra::imp>&);
|