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