1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     array_solver.h
7 
8 Abstract:
9 
10     Theory plugin for arrays
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2020-09-08
15 
16 --*/
17 #pragma once
18 
19 #include "ast/ast_trail.h"
20 #include "sat/smt/sat_th.h"
21 #include "ast/array_decl_plugin.h"
22 
23 namespace euf {
24     class solver;
25 }
26 
27 namespace array {
28 
29     class solver : public euf::th_euf_solver {
30         typedef euf::theory_var theory_var;
31         typedef euf::theory_id theory_id;
32         typedef sat::literal literal;
33         typedef sat::bool_var bool_var;
34         typedef sat::literal_vector literal_vector;
35         typedef union_find<solver, euf::solver>  array_union_find;
36 
37 
38         struct stats {
39             unsigned m_num_store_axiom, m_num_extensionality_axiom;
40             unsigned m_num_eq_splits, m_num_congruence_axiom;
41             unsigned m_num_select_store_axiom, m_num_select_as_array_axiom, m_num_select_map_axiom;
42             unsigned m_num_select_const_axiom, m_num_select_store_axiom_delayed;
43             unsigned m_num_default_store_axiom, m_num_default_map_axiom;
44             unsigned m_num_default_const_axiom, m_num_default_as_array_axiom;
45             unsigned m_num_select_lambda_axiom;
resetstats46             void reset() { memset(this, 0, sizeof(*this)); }
statsstats47             stats() { reset(); }
48         };
49 
50         // void log_drat(array_justification const& c);
51 
52         struct var_data {
53             bool                m_prop_upward{ false };
54             euf::enode_vector   m_lambdas;             // equivalent nodes that have beta reduction properties
55             euf::enode_vector   m_parent_lambdas;      // parents that have beta reduction properties
56             euf::enode_vector   m_parent_selects;      // parents that use array in select position
57         };
58 
59 
60         array_util        a;
61         stats             m_stats;
62         scoped_ptr_vector<var_data>          m_var_data;
63         ast2ast_trailmap<sort, app>          m_sort2epsilon;
64         ast2ast_trailmap<sort, func_decl>    m_sort2diag;
65         obj_map<sort, func_decl_ref_vector*> m_sort2diff;
66         array_union_find                     m_find;
67 
find(theory_var v)68         theory_var find(theory_var v) { return m_find.find(v); }
69         func_decl_ref_vector const& sort2diff(sort* s);
70 
71         // internalize
72         bool visit(expr* e) override;
73         bool visited(expr* e) override;
74         bool post_visit(expr* e, bool sign, bool root) override;
75         void ensure_var(euf::enode* n);
76         void internalize_store(euf::enode* n);
77         void internalize_select(euf::enode* n);
78         void internalize_lambda(euf::enode* n);
79         void internalize_ext(euf::enode* n);
80         void internalize_default(euf::enode* n);
81         void internalize_map(euf::enode* n);
82 
83         // axioms
84         struct axiom_record {
85             enum class kind_t {
86                 is_store,
87                 is_select,
88                 is_extensionality,
89                 is_default,
90                 is_congruence
91             };
92             enum class state_t {
93                 is_new,
94                 is_delayed,
95                 is_applied
96             };
97             kind_t      m_kind;
98             state_t     m_state { state_t::is_new };
99             euf::enode* n;
100             euf::enode* select;
m_kindaxiom_record101             axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(select) {}
102 
is_delayedaxiom_record103             bool is_delayed() const { return m_state == state_t::is_delayed; }
is_appliedaxiom_record104             bool is_applied() const { return m_state == state_t::is_applied; }
set_newaxiom_record105             void set_new() { m_state = state_t::is_new; }
set_appliedaxiom_record106             void set_applied() { m_state = state_t::is_applied; }
set_delayedaxiom_record107             void set_delayed() { m_state = state_t::is_delayed; }
108 
109             struct hash {
110                 solver& s;
hashaxiom_record::hash111                 hash(solver& s) :s(s) {}
hash_selectaxiom_record::hash112                 unsigned hash_select(axiom_record const& r) const {
113                     unsigned h = mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select->get_arg(1)->get_expr_id());
114                     for (unsigned i = 2; i < r.select->num_args(); ++i)
115                         h = mk_mix(h, h, r.select->get_arg(i)->get_expr_id());
116                     return h;
117                 }
operatoraxiom_record::hash118                 unsigned operator()(unsigned idx) const {
119                     auto const& r = s.m_axiom_trail[idx];
120                     if (r.m_kind == kind_t::is_select)
121                         return hash_select(r);
122                     return mk_mix(r.n->get_expr_id(), (unsigned)r.m_kind, r.select ? r.select->get_expr_id() : 1);
123                 }
124             };
125 
126             struct eq {
127                 solver& s;
eqaxiom_record::eq128                 eq(solver& s) :s(s) {}
eq_selectaxiom_record::eq129                 bool eq_select(axiom_record const& p, axiom_record const& r) const {
130                     if (p.m_kind != r.m_kind || p.n != r.n)
131                         return false;
132                     for (unsigned i = p.select->num_args(); i-- > 1; )
133                         if (p.select->get_arg(i) != r.select->get_arg(i))
134                             return false;
135                     return true;
136                 }
operatoraxiom_record::eq137                 unsigned operator()(unsigned a, unsigned b) const {
138                     auto const& p = s.m_axiom_trail[a];
139                     auto const& r = s.m_axiom_trail[b];
140                     if (p.m_kind == kind_t::is_select)
141                         return eq_select(p, r);
142                     return p.m_kind == r.m_kind && p.n == r.n && p.select == r.select;
143                 }
144             };
145         };
146         typedef hashtable<unsigned, axiom_record::hash, axiom_record::eq> axiom_table_t;
147         axiom_record::hash    m_hash;
148         axiom_record::eq      m_eq;
149         axiom_table_t         m_axioms;
150         svector<axiom_record> m_axiom_trail;
151         unsigned              m_qhead { 0 };
152         unsigned              m_delay_qhead { 0 };
153         bool                  m_enable_delay { true };
154         struct reset_new;
155         void push_axiom(axiom_record const& r);
156         bool propagate_axiom(unsigned idx);
157         bool assert_axiom(unsigned idx);
158         bool assert_select(unsigned idx, axiom_record & r);
159         bool assert_default(axiom_record & r);
160         bool is_relevant(axiom_record const& r) const;
set_applied(unsigned idx)161         void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); }
is_applied(unsigned idx)162         bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); }
is_delayed(unsigned idx)163         bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); }
164 
select_axiom(euf::enode * s,euf::enode * n)165         axiom_record select_axiom(euf::enode* s, euf::enode* n) { return axiom_record(axiom_record::kind_t::is_select, n, s); }
default_axiom(euf::enode * n)166         axiom_record default_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_default, n); }
store_axiom(euf::enode * n)167         axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); }
extensionality_axiom(euf::enode * x,euf::enode * y)168         axiom_record extensionality_axiom(euf::enode* x, euf::enode* y) { return axiom_record(axiom_record::kind_t::is_extensionality, x, y); }
congruence_axiom(euf::enode * a,euf::enode * b)169         axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); }
170 
171         scoped_ptr<sat::constraint_base> m_constraint;
172 
array_axiom()173         sat::ext_justification_idx array_axiom() { return m_constraint->to_index(); }
174 
175         bool assert_store_axiom(app* _e);
176         bool assert_select_store_axiom(app* select, app* store);
177         bool assert_select_const_axiom(app* select, app* cnst);
178         bool assert_select_as_array_axiom(app* select, app* arr);
179         bool assert_select_map_axiom(app* select, app* map);
180         bool assert_select_lambda_axiom(app* select, expr* lambda);
181         bool assert_extensionality(expr* e1, expr* e2);
182         bool assert_default_map_axiom(app* map);
183         bool assert_default_const_axiom(app* cnst);
184         bool assert_default_store_axiom(app* store);
185         bool assert_congruent_axiom(expr* e1, expr* e2);
186         bool add_delayed_axioms();
187         bool add_as_array_eqs(euf::enode* n);
188 
189         bool has_unitary_domain(app* array_term);
190         bool has_large_domain(expr* array_term);
191         std::pair<app*, func_decl*> mk_epsilon(sort* s);
192         void collect_shared_vars(sbuffer<theory_var>& roots);
193         bool add_interface_equalities();
194         bool is_shared_arg(euf::enode* r);
is_array(euf::enode * n)195         bool is_array(euf::enode* n) const { return a.is_array(n->get_expr()); }
196 
197         // solving
198         void add_parent_select(theory_var v_child, euf::enode* select);
199         void add_parent_default(theory_var v_child, euf::enode* def);
200         void add_lambda(theory_var v, euf::enode* lambda);
201         void add_parent_lambda(theory_var v_child, euf::enode* lambda);
202 
203         void propagate_select_axioms(var_data const& d, euf::enode* a);
204         void propagate_parent_select_axioms(theory_var v);
205         void propagate_parent_default(theory_var v);
206 
207         void set_prop_upward(theory_var v);
208         void set_prop_upward(var_data& d);
209         void set_prop_upward(euf::enode* n);
210         unsigned get_lambda_equiv_size(var_data const& d) const;
211         bool should_set_prop_upward(var_data const& d) const;
212         bool should_prop_upward(var_data const& d) const;
can_beta_reduce(euf::enode * n)213         bool can_beta_reduce(euf::enode* n) const { return can_beta_reduce(n->get_expr()); }
214         bool can_beta_reduce(expr* e) const;
215 
get_var_data(euf::enode * n)216         var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
get_var_data(theory_var v)217         var_data& get_var_data(theory_var v) { return *m_var_data[v]; }
get_var_data(theory_var v)218         var_data const& get_var_data(theory_var v) const { return *m_var_data[v]; }
219 
220         void pop_core(unsigned n) override;
221 
222         // models
223         euf::enode_vector   m_defaults;       // temporary field for model construction
224         ptr_vector<expr>    m_else_values;    //
225         svector<int>        m_parents;        // temporary field for model construction
226         bool must_have_different_model_values(theory_var v1, theory_var v2);
227         void collect_defaults();
228         void mg_merge(theory_var u, theory_var v);
229         theory_var mg_find(theory_var n);
230         void set_default(theory_var v, euf::enode* n);
231         euf::enode* get_default(theory_var v);
232         void set_else(theory_var v, expr* e);
233         expr* get_else(theory_var v);
234 
235         // diagnostics
236         std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const;
237         std::ostream& display(std::ostream& out, axiom_record const& r) const;
238         void validate_check() const;
239         void validate_select_store(euf::enode* n) const;
240         void validate_extensionality(euf::enode* s, euf::enode* t) const;
241     public:
242         solver(euf::solver& ctx, theory_id id);
243         ~solver() override;
is_external(bool_var v)244         bool is_external(bool_var v) override { return false; }
get_antecedents(literal l,sat::ext_justification_idx idx,literal_vector & r,bool probing)245         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) override {}
asserted(literal l)246         void asserted(literal l) override {}
247         sat::check_result check() override;
248 
249         std::ostream& display(std::ostream& out) const override;
250         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
251         std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
252         void collect_statistics(statistics& st) const override;
253         euf::th_solver* clone(euf::solver& ctx) override;
254         void new_eq_eh(euf::th_eq const& eq) override;
use_diseqs()255         bool use_diseqs() const override { return true; }
256         void new_diseq_eh(euf::th_eq const& eq) override;
257         bool unit_propagate() override;
258         void init_model() override;
259         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
260         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
261         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
262         void internalize(expr* e, bool redundant) override;
263         euf::theory_var mk_var(euf::enode* n) override;
264         void apply_sort_cnstr(euf::enode* n, sort* s) override;
265         bool is_shared(theory_var v) const override;
enable_self_propagate()266         bool enable_self_propagate() const override { return true; }
267 
268         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
after_merge_eh(theory_var r1,theory_var r2,theory_var v1,theory_var v2)269         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
unmerge_eh(theory_var v1,theory_var v2)270         void unmerge_eh(theory_var v1, theory_var v2) {}
271 
parent_selects(euf::enode * n)272         euf::enode_vector const& parent_selects(euf::enode* n) { return m_var_data[find(n->get_th_var(get_id()))]->m_parent_selects; }
273     };
274 }
275