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