mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 19:53:34 +00:00
315 lines
14 KiB
C++
315 lines
14 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
array_solver.h
|
|
|
|
Abstract:
|
|
|
|
Theory plugin for arrays
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2020-09-08
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "ast/ast_trail.h"
|
|
#include "sat/smt/sat_th.h"
|
|
#include "ast/array_decl_plugin.h"
|
|
|
|
namespace euf {
|
|
class solver;
|
|
}
|
|
|
|
namespace array {
|
|
|
|
class solver : public euf::th_euf_solver {
|
|
typedef euf::theory_var theory_var;
|
|
typedef euf::theory_id theory_id;
|
|
typedef sat::literal literal;
|
|
typedef sat::bool_var bool_var;
|
|
typedef sat::literal_vector literal_vector;
|
|
typedef union_find<solver, euf::solver> array_union_find;
|
|
|
|
|
|
struct stats {
|
|
unsigned m_num_store_axiom, m_num_extensionality_axiom;
|
|
unsigned m_num_eq_splits, m_num_congruence_axiom;
|
|
unsigned m_num_select_store_axiom, m_num_select_as_array_axiom, m_num_select_map_axiom;
|
|
unsigned m_num_select_const_axiom, m_num_select_store_axiom_delayed;
|
|
unsigned m_num_default_store_axiom, m_num_default_map_axiom;
|
|
unsigned m_num_default_const_axiom, m_num_default_as_array_axiom;
|
|
unsigned m_num_select_lambda_axiom;
|
|
void reset() { memset(this, 0, sizeof(*this)); }
|
|
stats() { reset(); }
|
|
};
|
|
|
|
// void log_drat(array_justification const& c);
|
|
|
|
struct var_data {
|
|
bool m_prop_upward{ false };
|
|
euf::enode_vector m_lambdas; // equivalent nodes that have beta reduction properties
|
|
euf::enode_vector m_parent_lambdas; // parents that have beta reduction properties
|
|
euf::enode_vector m_parent_selects; // parents that use array in select position
|
|
};
|
|
|
|
|
|
array_util a;
|
|
stats m_stats;
|
|
scoped_ptr_vector<var_data> m_var_data;
|
|
ast2ast_trailmap<sort, app> m_sort2epsilon;
|
|
ast2ast_trailmap<sort, func_decl> m_sort2diag;
|
|
obj_map<sort, func_decl_ref_vector*> m_sort2diff;
|
|
array_union_find m_find;
|
|
|
|
theory_var find(theory_var v) { return m_find.find(v); }
|
|
theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); }
|
|
func_decl_ref_vector const& sort2diff(sort* s);
|
|
|
|
// internalize
|
|
bool visit(expr* e) override;
|
|
bool visited(expr* e) override;
|
|
bool post_visit(expr* e, bool sign, bool root) override;
|
|
void ensure_var(euf::enode* n);
|
|
void internalize_eh(euf::enode* n);
|
|
void internalize_lambda_eh(euf::enode* n);
|
|
|
|
// axioms
|
|
struct axiom_record {
|
|
enum class kind_t {
|
|
is_store,
|
|
is_select,
|
|
is_extensionality,
|
|
is_diff,
|
|
is_diffselect,
|
|
is_default,
|
|
is_congruence
|
|
};
|
|
enum class state_t {
|
|
is_new,
|
|
is_delayed,
|
|
is_applied
|
|
};
|
|
kind_t m_kind;
|
|
state_t m_state { state_t::is_new };
|
|
euf::enode* n;
|
|
euf::enode* select;
|
|
axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(select) {}
|
|
|
|
bool is_delayed() const { return m_state == state_t::is_delayed; }
|
|
bool is_applied() const { return m_state == state_t::is_applied; }
|
|
void set_new() { m_state = state_t::is_new; }
|
|
void set_applied() { m_state = state_t::is_applied; }
|
|
void set_delayed() { m_state = state_t::is_delayed; }
|
|
|
|
struct hash {
|
|
solver& s;
|
|
hash(solver& s) :s(s) {}
|
|
unsigned hash_select(axiom_record const& r) const {
|
|
unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id());
|
|
for (unsigned i = 2; i < r.select->num_args(); ++i)
|
|
h = mk_mix(h, h, r.select->get_arg(i)->get_expr_id());
|
|
return h;
|
|
}
|
|
unsigned operator()(unsigned idx) const {
|
|
auto const& r = s.m_axiom_trail[idx];
|
|
if (r.m_kind == kind_t::is_select)
|
|
return hash_select(r);
|
|
return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1);
|
|
}
|
|
};
|
|
|
|
struct eq {
|
|
solver& s;
|
|
eq(solver& s) :s(s) {}
|
|
bool eq_select(axiom_record const& p, axiom_record const& r) const {
|
|
if (p.m_kind != r.m_kind || p.n != r.n)
|
|
return false;
|
|
for (unsigned i = p.select->num_args(); i-- > 1; )
|
|
if (p.select->get_arg(i) != r.select->get_arg(i))
|
|
return false;
|
|
return true;
|
|
}
|
|
unsigned operator()(unsigned a, unsigned b) const {
|
|
auto const& p = s.m_axiom_trail[a];
|
|
auto const& r = s.m_axiom_trail[b];
|
|
if (p.m_kind == kind_t::is_select)
|
|
return eq_select(p, r);
|
|
return p.m_kind == r.m_kind && p.n == r.n && p.select == r.select;
|
|
}
|
|
};
|
|
};
|
|
typedef hashtable<unsigned, axiom_record::hash, axiom_record::eq> axiom_table_t;
|
|
axiom_record::hash m_hash;
|
|
axiom_record::eq m_eq;
|
|
axiom_table_t m_axioms;
|
|
svector<axiom_record> m_axiom_trail;
|
|
unsigned m_qhead = 0;
|
|
unsigned m_delay_qhead = 0;
|
|
bool m_enable_delay = true;
|
|
struct reset_new;
|
|
void push_axiom(axiom_record const& r);
|
|
bool propagate_axiom(unsigned idx);
|
|
bool assert_axiom(unsigned idx);
|
|
bool assert_select(unsigned idx, axiom_record & r);
|
|
bool assert_default(axiom_record & r);
|
|
void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); }
|
|
bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); }
|
|
bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); }
|
|
|
|
axiom_record select_axiom(euf::enode* s, euf::enode* n) { return axiom_record(axiom_record::kind_t::is_select, n, s); }
|
|
axiom_record default_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_default, n); }
|
|
axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); }
|
|
axiom_record extensionality_axiom(euf::enode* x, euf::enode* y) { return axiom_record(axiom_record::kind_t::is_extensionality, x, y); }
|
|
axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); }
|
|
axiom_record diff_axiom(euf::enode* md) { return axiom_record(axiom_record::kind_t::is_diff, md); }
|
|
euf::enode_vector m_minmaxdiffs;
|
|
axiom_record diff_select_axiom(euf::enode* md, euf::enode* ai) { return axiom_record(axiom_record::kind_t::is_diffselect, md, ai); }
|
|
|
|
scoped_ptr<sat::constraint_base> m_constraint;
|
|
|
|
sat::ext_justification_idx array_axiom() { return m_constraint->to_index(); }
|
|
|
|
bool assert_store_axiom(app* _e);
|
|
bool assert_select_store_axiom(app* select, app* store);
|
|
bool assert_select_const_axiom(app* select, app* cnst);
|
|
bool assert_select_as_array_axiom(app* select, app* arr);
|
|
bool assert_select_map_axiom(app* select, app* map);
|
|
bool assert_select_lambda_axiom(app* select, expr* lambda);
|
|
bool assert_extensionality(expr* e1, expr* e2);
|
|
bool assert_diff(expr* md);
|
|
bool assert_diff_select(app* ai, app* md);
|
|
bool assert_default_map_axiom(app* map);
|
|
bool assert_default_const_axiom(app* cnst);
|
|
bool assert_default_store_axiom(app* store);
|
|
bool assert_congruent_axiom(expr* e1, expr* e2);
|
|
bool add_delayed_axioms();
|
|
bool add_as_array_eqs(euf::enode* n);
|
|
bool add_diff_select_axioms();
|
|
expr_ref apply_map(app* map, unsigned n, expr* const* args);
|
|
bool is_map_combinator(expr* e) const;
|
|
|
|
bool has_unitary_domain(app* array_term);
|
|
bool has_large_domain(expr* array_term);
|
|
std::pair<app*, func_decl*> mk_epsilon(sort* s);
|
|
void collect_shared_vars(sbuffer<theory_var>& roots);
|
|
bool add_interface_equalities();
|
|
bool is_shared_arg(euf::enode* r);
|
|
bool is_array(euf::enode* n) const { return a.is_array(n->get_expr()); }
|
|
|
|
// solving
|
|
void add_parent_select(theory_var v_child, euf::enode* select);
|
|
void add_parent_default(theory_var v_child, euf::enode* def);
|
|
void add_lambda(theory_var v, euf::enode* lambda);
|
|
void add_parent_lambda(theory_var v_child, euf::enode* lambda);
|
|
|
|
void propagate_select_axioms(var_data const& d, euf::enode* a);
|
|
void propagate_parent_select_axioms(theory_var v);
|
|
void propagate_parent_default(theory_var v);
|
|
|
|
void set_prop_upward(theory_var v);
|
|
void set_prop_upward(var_data& d);
|
|
void set_prop_upward_store(euf::enode* n);
|
|
unsigned get_lambda_equiv_size(var_data const& d) const;
|
|
bool should_set_prop_upward(var_data const& d) const;
|
|
bool should_prop_upward(var_data const& d) const;
|
|
bool can_beta_reduce(euf::enode* n) const { return can_beta_reduce(n->get_expr()); }
|
|
bool can_beta_reduce(expr* e) const;
|
|
bool check_lambdas();
|
|
|
|
var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
|
|
var_data& get_var_data(theory_var v) { return *m_var_data[v]; }
|
|
var_data const& get_var_data(theory_var v) const { return *m_var_data[v]; }
|
|
|
|
void pop_core(unsigned n) override;
|
|
|
|
// models
|
|
// I need a set of select enodes where select(A,i) = select(B,j) if i->get_root() == j->get_root()
|
|
struct sel_khasher {
|
|
unsigned operator()(euf::enode const * n) const { return 0; }
|
|
};
|
|
|
|
struct sel_chasher {
|
|
unsigned operator()(euf::enode const * n, unsigned idx) const {
|
|
return n->get_arg(idx+1)->get_root()->hash();
|
|
}
|
|
};
|
|
|
|
struct sel_hash {
|
|
unsigned operator()(euf::enode * n) const;
|
|
};
|
|
|
|
struct sel_eq {
|
|
bool operator()(euf::enode * n1, euf::enode * n2) const;
|
|
};
|
|
|
|
typedef ptr_hashtable<euf::enode, sel_hash, sel_eq> select_set;
|
|
euf::enode_vector m_defaults; // temporary field for model construction
|
|
ptr_vector<expr> m_else_values; //
|
|
svector<int> m_parents; // temporary field for model construction
|
|
obj_map<euf::enode, select_set*> m_selects; // mapping from array -> relevant selects
|
|
ptr_vector<euf::enode> m_selects_domain;
|
|
ptr_vector<select_set> m_selects_range;
|
|
|
|
bool must_have_different_model_values(theory_var v1, theory_var v2);
|
|
select_set* get_select_set(euf::enode* n);
|
|
void collect_defaults();
|
|
void collect_selects(); // mapping from array -> relevant selects
|
|
void propagate_select_to_store_parents(euf::enode* r, euf::enode* sel, euf::enode_pair_vector& todo);
|
|
|
|
void mg_merge(theory_var u, theory_var v);
|
|
theory_var mg_find(theory_var n);
|
|
void set_default(theory_var v, euf::enode* n);
|
|
euf::enode* get_default(theory_var v);
|
|
void set_else(theory_var v, expr* e);
|
|
expr* get_else(theory_var v);
|
|
|
|
// diagnostics
|
|
std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const;
|
|
std::ostream& display(std::ostream& out, axiom_record const& r) const;
|
|
void validate_check() const;
|
|
void validate_select_store(euf::enode* n) const;
|
|
void validate_extensionality(euf::enode* s, euf::enode* t) const;
|
|
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;
|
|
|
|
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;
|
|
void new_eq_eh(euf::th_eq const& eq) override;
|
|
bool use_diseqs() const override { return true; }
|
|
void new_diseq_eh(euf::th_eq const& eq) override;
|
|
bool unit_propagate() override;
|
|
void init_model() override;
|
|
void finalize_model(model& mdl) override;
|
|
bool include_func_interp(func_decl* f) const override { return a.is_ext(f); }
|
|
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, bool learned) override;
|
|
void internalize(expr* e, bool redundant) override;
|
|
euf::theory_var mk_var(euf::enode* n) override;
|
|
void apply_sort_cnstr(euf::enode* n, sort* s) override;
|
|
bool is_shared(theory_var v) const override;
|
|
bool is_beta_redex(euf::enode* p, euf::enode* n) const override;
|
|
bool enable_self_propagate() const override { return true; }
|
|
void relevant_eh(euf::enode* n) override;
|
|
bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); }
|
|
|
|
void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
|
|
void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
|
|
void unmerge_eh(theory_var v1, theory_var v2) {}
|
|
|
|
euf::enode_vector const& parent_selects(euf::enode* n) { return m_var_data[find(n->get_th_var(get_id()))]->m_parent_selects; }
|
|
};
|
|
}
|