1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 q_ematch.h 7 8 Abstract: 9 10 E-matching quantifier instantiation plugin 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2021-01-24 15 16 --*/ 17 #pragma once 18 19 #include "util/nat_set.h" 20 #include "ast/quantifier_stat.h" 21 #include "ast/pattern/pattern_inference.h" 22 #include "ast/normal_forms/nnf.h" 23 #include "solver/solver.h" 24 #include "sat/smt/sat_th.h" 25 #include "sat/smt/q_mam.h" 26 #include "sat/smt/q_clause.h" 27 #include "sat/smt/q_queue.h" 28 #include "sat/smt/q_eval.h" 29 30 namespace euf { 31 class solver; 32 } 33 34 namespace q { 35 36 class solver; 37 38 class ematch { 39 struct stats { 40 unsigned m_num_instantiations; 41 unsigned m_num_propagations; 42 unsigned m_num_conflicts; 43 unsigned m_num_redundant; 44 unsigned m_num_delayed_bindings; 45 statsstats46 stats() { reset(); } 47 resetstats48 void reset() { 49 memset(this, 0, sizeof(*this)); 50 } 51 }; 52 53 struct prop { 54 bool is_conflict; 55 unsigned idx; 56 sat::ext_justification_idx j; propprop57 prop(bool is_conflict, unsigned idx, sat::ext_justification_idx j) : is_conflict(is_conflict), idx(idx), j(j) {} 58 }; 59 60 struct remove_binding; 61 struct insert_binding; 62 struct pop_clause; 63 struct scoped_mark_reset; 64 struct reset_in_queue; 65 66 67 euf::solver& ctx; 68 solver& m_qs; 69 ast_manager& m; 70 eval m_eval; 71 quantifier_stat_gen m_qstat_gen; 72 bindings m_bindings; 73 scoped_ptr<binding> m_tmp_binding; 74 unsigned m_tmp_binding_capacity = 0; 75 queue m_inst_queue; 76 svector<prop> m_prop_queue; 77 pattern_inference_rw m_infer_patterns; 78 scoped_ptr<q::mam> m_mam, m_lazy_mam; 79 ptr_vector<clause> m_clauses; 80 obj_map<quantifier, unsigned> m_q2clauses; 81 vector<unsigned_vector> m_watch; // expr_id -> clause-index* 82 stats m_stats; 83 expr_fast_mark1 m_mark; 84 unsigned m_generation_propagation_threshold = 3; 85 ptr_vector<app> m_ground; 86 bool m_in_queue_set = false; 87 nat_set m_node_in_queue; 88 nat_set m_clause_in_queue; 89 unsigned m_qhead = 0; 90 unsigned_vector m_clause_queue; 91 euf::enode_pair_vector m_evidence; 92 93 euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding); 94 binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding); 95 binding* alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); 96 97 sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); 98 99 void ensure_ground_enodes(expr* e); 100 void ensure_ground_enodes(clause const& c); 101 102 void instantiate(binding& b); 103 sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l); 104 105 // register as callback into egraph. 106 void on_merge(euf::enode* root, euf::enode* other); 107 void insert_to_propagate(unsigned node_id); 108 void insert_clause_in_queue(unsigned idx); 109 110 void add_watch(euf::enode* root, unsigned clause_idx); 111 void init_watch(expr* e, unsigned clause_idx); 112 void init_watch(clause& c); 113 114 void attach_ground_pattern_terms(expr* pat); 115 clause* clausify(quantifier* q); 116 lit clausify_literal(expr* arg); 117 118 bool flush_prop_queue(); 119 void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx); 120 121 bool propagate(bool flush); 122 123 expr_ref_vector m_new_defs; 124 proof_ref_vector m_new_proofs; 125 defined_names m_dn; 126 nnf m_nnf; 127 128 quantifier_ref nnf_skolem(quantifier* q); 129 130 public: 131 132 ematch(euf::solver& ctx, solver& s); 133 134 bool operator()(); 135 136 bool unit_propagate(); 137 138 139 void add(quantifier* q); 140 141 void collect_statistics(statistics& st) const; 142 143 void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing); 144 145 // callback from mam 146 void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen); 147 148 // callbacks from queue evaluate(euf::enode * const * binding,clause & c)149 lbool evaluate(euf::enode* const* binding, clause& c) { m_evidence.reset(); return m_eval(binding, c, m_evidence); } 150 151 void add_instantiation(clause& c, binding& b, sat::literal lit); 152 153 bool propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& new_propagation); 154 155 std::ostream& display(std::ostream& out) const; 156 157 std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const; 158 159 }; 160 161 } 162