#pragma once
#include "util/obj_pair_set.h"
#include "ast/ast_trail.h"
#include "ast/arith_decl_plugin.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 "sat/smt/sat_th.h"
namespace euf {
class solver;
}
namespace arith {
typedef ptr_vector<lp_api::bound<sat::literal>> lp_bounds;
typedef lp::lpvar lpvar;
typedef euf::theory_var theory_var;
typedef euf::theory_id theory_id;
typedef euf::enode enode;
typedef euf::enode_pair enode_pair;
typedef sat::literal literal;
typedef sat::bool_var bool_var;
typedef sat::literal_vector literal_vector;
typedef lp_api::bound<sat::literal> api_bound;
enum class hint_type {
farkas_h,
bound_h,
cut_h,
implied_eq_h,
nla_h
};
struct arith_proof_hint : public euf::th_proof_hint {
hint_type m_ty;
unsigned m_lit_head, m_lit_tail, m_eq_head, m_eq_tail;
arith_proof_hint(hint_type t, unsigned lh, unsigned lt, unsigned eh, unsigned et):
m_ty(t), m_lit_head(lh), m_lit_tail(lt), m_eq_head(eh), m_eq_tail(et) {}
expr* get_hint(euf::solver& s) const override;
};
class arith_proof_hint_builder {
vector<std::pair<rational, literal>> m_literals;
svector<std::tuple<euf::enode*,euf::enode*,bool>> m_eqs;
hint_type m_ty;
unsigned m_lit_head = 0, m_lit_tail = 0, m_eq_head = 0, m_eq_tail = 0;
void reset() { m_lit_head = m_lit_tail; m_eq_head = m_eq_tail; }
void add(euf::enode* a, euf::enode* b, bool is_eq) {
if (m_eq_tail < m_eqs.size())
m_eqs[m_eq_tail] = { a, b, is_eq };
else
m_eqs.push_back({a, b, is_eq });
m_eq_tail++;
}
public:
void set_type(euf::solver& ctx, hint_type ty);
void add_eq(euf::enode* a, euf::enode* b) { add(a, b, true); }
void add_diseq(euf::enode* a, euf::enode* b) { add(a, b, false); }
void add_lit(rational const& coeff, literal lit) {
if (m_lit_tail < m_literals.size())
m_literals[m_lit_tail] = {coeff, lit};
else
m_literals.push_back({coeff, lit});
m_lit_tail++;
}
std::pair<rational, literal> const& lit(unsigned i) const { return m_literals[i]; }
std::tuple<enode*, enode*, bool> const& eq(unsigned i) const { return m_eqs[i]; }
arith_proof_hint* mk(euf::solver& s);
};
class solver : public euf::th_euf_solver {
friend struct arith_proof_hint;
friend class sls;
struct scope {
unsigned m_bounds_lim;
unsigned m_asserted_qhead;
unsigned m_asserted_lim;
};
class resource_limit : public lp::lp_resource_limit {
solver& m_imp;
public:
resource_limit(solver& i) : m_imp(i) { }
bool get_cancel_flag() override { return !m_imp.m.inc(); }
};
struct var_value_eq {
solver& m_th;
var_value_eq(solver& th) :m_th(th) {}
bool operator()(theory_var v1, theory_var v2) const {
if (m_th.is_int(v1) != m_th.is_int(v2)) {
return false;
}
return m_th.is_eq(v1, v2);
}
};
struct var_value_hash {
solver& m_th;
var_value_hash(solver& 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;
bool m_new_eq = false;
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();
}
};
scoped_ptr_vector<internalize_state> m_internalize_states;
unsigned m_internalize_head = 0;
class scoped_internalize_state {
solver& m_imp;
internalize_state& m_st;
internalize_state& push_internalize(solver& 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(solver& 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;
vector<rational> m_columns;
var_coeffs m_left_side;
lpvar m_one_var = UINT_MAX;
lpvar m_zero_var = UINT_MAX;
lpvar m_rone_var = UINT_MAX;
lpvar m_rzero_var = UINT_MAX;
enum constraint_source {
inequality_source,
equality_source,
definition_source,
null_source
};
svector<constraint_source> m_constraint_sources;
svector<literal> m_inequalities; svector<euf::enode_pair> m_equalities; svector<theory_var> m_definitions; svector<std::pair<euf::th_eq, bool>> m_delayed_eqs;
literal_vector m_asserted;
expr* m_not_handled = nullptr;
ptr_vector<app> m_underspecified;
ptr_vector<expr> m_idiv_terms;
ptr_vector<app> m_bv_terms;
vector<ptr_vector<api_bound> > m_use_list;
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 = 0;
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head = 0;
indexed_uint_set m_tmp_var_set;
unsigned m_num_conflicts = 0;
lp_api::stats m_stats;
svector<scope> m_scopes;
scoped_ptr<nla::solver> m_nla;
bool m_use_nra_model = false;
scoped_ptr<lp::int_solver> m_lia;
scoped_ptr<lp::lar_solver> m_solver;
resource_limit m_resource_limit;
lp_bounds m_new_bounds;
symbol m_farkas;
std_vector<lp::implied_bound> m_implied_bounds;
lp::lp_bound_propagator<solver> m_bp;
mutable vector<std::pair<lp::lpvar, rational>> m_todo_terms;
lp::explanation m_explanation;
literal_vector m_core, m_core2;
vector<rational> m_coeffs;
svector<enode_pair> m_eqs;
vector<parameter> m_params;
nla::lemma m_lemma;
arith_util a;
bool is_int(theory_var v) const { return is_int(var2enode(v)); }
bool is_int(euf::enode* n) const { return a.is_int(n->get_expr()); }
bool is_real(theory_var v) const { return is_real(var2enode(v)); }
bool is_real(euf::enode* n) const { return a.is_real(n->get_expr()); }
bool is_bool(theory_var v) const { return is_bool(var2enode(v)); }
bool is_bool(euf::enode* n) const { return m.is_bool(n->get_expr()); }
bool m_internalize_initialized { false };
void init_internalize();
lpvar add_const(int c, lpvar& var, bool is_int);
lpvar get_one(bool is_int);
lpvar get_zero(bool is_int);
void ensure_nla();
void found_unsupported(expr* n);
void found_underspecified(expr* n);
void linearize_term(expr* term, scoped_internalize_state& st);
void linearize_ineq(expr* lhs, expr* rhs, scoped_internalize_state& st);
void linearize(scoped_internalize_state& st);
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2);
void add_ineq_constraint(lp::constraint_index index, literal lit);
void add_def_constraint(lp::constraint_index index);
void add_def_constraint(lp::constraint_index index, theory_var v);
void add_def_constraint_and_equality(lpvar vi, lp::lconstraint_kind kind, const rational& bound);
void internalize_args(app* t, bool force = false);
void ensure_arg_vars(app* t);
theory_var internalize_power(app* t, app* n, unsigned p);
theory_var internalize_mul(app* t);
theory_var internalize_numeral(app* t, rational const& v);
theory_var internalize_def(expr* term);
theory_var internalize_def(expr* term, scoped_internalize_state& st);
theory_var internalize_linearized_def(expr* term, scoped_internalize_state& st);
void init_left_side(scoped_internalize_state& st);
bool internalize_term(expr* term);
bool internalize_atom(expr* atom);
bool is_unit_var(scoped_internalize_state& st);
bool is_one(scoped_internalize_state& st);
bool is_zero(scoped_internalize_state& st);
expr* mk_sub(expr* a, expr* b);
enode* mk_enode(expr* e);
lpvar register_theory_var_in_lar_solver(theory_var v);
theory_var mk_evar(expr* e);
bool has_var(expr* e);
bool reflect(expr* n) const;
lpvar get_lpvar(theory_var v) const;
lp::lpvar get_column(theory_var v) const;
void mk_div_axiom(expr* p, expr* q);
void mk_to_int_axiom(app* n);
void mk_abs_axiom(app* n);
void mk_is_int_axiom(expr* n);
void mk_idiv_mod_axioms(expr* p, expr* q);
void mk_rem_axiom(expr* dividend, expr* divisor);
void mk_power_axiom(expr* t, expr* n, expr* p);
void mk_bound_axioms(api_bound& b);
void mk_bound_axiom(api_bound& b1, api_bound& b2);
void mk_power0_axioms(app* t, app* n);
void mk_bv_axiom(app* n);
void flush_bound_axioms();
void add_farkas_clause(sat::literal l1, sat::literal l2);
struct compare_bounds {
bool operator()(api_bound* a1, api_bound* a2) const { return a1->get_value() < a2->get_value(); }
};
typedef lp_bounds::iterator iterator;
lp_bounds::iterator first(
lp_api::bound_kind kind,
iterator it,
iterator end);
lp_bounds::iterator next_inf(
api_bound* a1,
lp_api::bound_kind kind,
iterator it,
iterator end,
bool& found_compatible);
lp_bounds::iterator next_sup(
api_bound* a1,
lp_api::bound_kind kind,
iterator it,
iterator end,
bool& found_compatible);
void propagate_eqs(lp::lpvar t, lp::constraint_index ci, lp::lconstraint_kind k, api_bound& b, rational const& value);
void propagate_basic_bounds(unsigned qhead);
void propagate_bounds_with_lp_solver();
void propagate_bound(literal lit, api_bound& b);
void propagate_lp_solver_bound(const lp::implied_bound& be);
void refine_bound(theory_var v, const lp::implied_bound& be);
literal is_bound_implied(lp::lconstraint_kind k, rational const& value, api_bound const& b) const;
void assert_bound(bool is_true, api_bound& b);
void mk_eq_axiom(bool is_eq, euf::th_eq const& eq);
void mk_diseq_axiom(theory_var v1, theory_var v2);
void assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r);
api_bound* mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound);
lp::lconstraint_kind bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true);
void fixed_var_eh(theory_var v1, u_dependency* dep, rational const& bound);
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); }
bool set_bound(lp::lpvar tv, lp::constraint_index ci, rational const& v, bool is_lower);
typedef std::pair<lp::constraint_index, rational> constraint_bound;
vector<constraint_bound> m_lower_terms;
vector<constraint_bound> m_upper_terms;
vector<constraint_bound> m_history;
bool can_get_value(theory_var v) const {
return is_registered_var(v) && m_model_is_initialized;
}
vector<rational> m_fixed_values;
map<rational, theory_var, rational::hash_proc, rational::eq_proc> m_value2var;
struct undo_value;
void register_fixed_var(theory_var v, rational const& value);
void report_equality_of_fixed_vars(unsigned vi1, unsigned vi2);
void reserve_bounds(theory_var v);
void updt_unassigned_bounds(theory_var v, int inc);
void pop_core(unsigned n) override;
void push_core() override;
void del_bounds(unsigned old_size);
bool all_zeros(vector<rational> const& v) const;
bound_prop_mode propagation_mode() const;
bool is_registered_var(theory_var v) const;
void ensure_column(theory_var v);
lp::impq get_ivalue(theory_var v) const;
rational get_value(theory_var v) const;
void random_update();
bool assume_eqs();
bool delayed_assume_eqs();
bool is_eq(theory_var v1, theory_var v2);
bool use_nra_model();
bool include_func_interp(enode* n) const;
lbool make_feasible();
bool check_delayed_eqs();
lbool check_lia();
lbool check_nla(unsigned level);
bool check_bv_terms();
bool check_bv_term(app* n);
void add_lemmas();
void propagate_nla();
void add_equality(lpvar v, rational const& k, lp::explanation const& exp);
bool is_infeasible() const;
nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const;
bool has_bound(lpvar vi, u_dependency*& ci, rational const& bound, bool is_lower);
bool has_lower_bound(lpvar vi, u_dependency*& ci, rational const& bound);
bool has_upper_bound(lpvar vi, u_dependency*& ci, rational const& bound);
unsigned m_bounded_range_idx; literal m_bounded_range_lit; expr_ref_vector m_bound_terms; expr_ref m_bound_predicate;
bool m_model_is_initialized = false;
unsigned small_lemma_size() const { return get_config().m_arith_small_lemma_size; }
bool propagate_eqs() const { return get_config().m_arith_propagate_eqs && m_num_conflicts < get_config().m_arith_propagation_threshold; }
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() && s().at_search_lvl(); }
unsigned init_range() const { return 5; }
unsigned max_range() const { return 20; }
void reset_evidence();
bool check_idiv_bounds();
bool is_bounded(expr* n);
app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound);
app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound, rational& offset, expr_ref& t);
literal mk_eq(lp::lar_term const& term, rational const& offset);
rational gcd_reduce(u_map<rational>& coeffs);
app_ref mk_term(lp::lar_term const& term, bool is_int);
app_ref coeffs2app(u_map<rational> const& coeffs, rational const& offset, bool is_int);
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff);
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs);
void get_infeasibility_explanation_and_set_conflict();
void set_conflict(hint_type ty);
void set_conflict_or_lemma(hint_type ty, literal_vector const& core, bool is_conflict);
void set_evidence(lp::constraint_index idx);
void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, euf::th_proof_hint const* pma);
sat::literal mk_ineq_literal(nla::ineq const& ineq);
void false_case_of_check_nla(const nla::lemma& l);
void dbg_finalize_model(model& mdl);
arith_proof_hint_builder m_arith_hint;
arith_proof_hint const* explain(hint_type ty, sat::literal lit = sat::null_literal);
arith_proof_hint const* explain_implied_eq(lp::explanation const& e, euf::enode* a, euf::enode* b);
arith_proof_hint const* explain_trichotomy(sat::literal le, sat::literal ge, sat::literal eq);
arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
void explain_assumptions(lp::explanation const& e);
bool validate_conflict();
public:
solver(euf::solver& ctx, theory_id id);
~solver() override;
bool is_external(bool_var v) override { return false; }
void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override;
void asserted(literal l) override;
sat::check_result check() override;
void simplify() override {}
void init_search() override {}
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
euf::th_solver* clone(euf::solver& ctx) override;
bool use_diseqs() const override { return true; }
void new_eq_eh(euf::th_eq const& eq) override;
void new_diseq_eh(euf::th_eq const& de) override;
bool unit_propagate() override;
void init_model() override;
void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
sat::literal internalize(expr* e, bool sign, bool root) override;
void internalize(expr* e) override;
void eq_internalized(euf::enode* n) override;
void apply_sort_cnstr(euf::enode* n, sort* s) override {}
void initialize_value(expr* var, expr* value) override;
bool is_shared(theory_var v) const override;
lbool get_phase(bool_var v) override;
bool include_func_interp(func_decl* f) const override;
bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
bool has_unhandled() const override { return m_not_handled != nullptr; }
lp::lar_solver& lp() { return *m_solver; }
lp::lar_solver const& lp() const { return *m_solver; }
bool is_equal(theory_var x, theory_var y) const;
bool add_eq(lpvar u, lpvar v, lp::explanation const& e, bool is_fixed);
void consume(rational const& v, lp::constraint_index j);
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational& bval) const;
bool get_value(euf::enode* n, expr_ref& val);
};
}