1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     smt_justification.cpp
7 
8 Abstract:
9 
10     <abstract>
11 
12 Author:
13 
14     Leonardo de Moura (leonardo) 2008-02-25.
15 
16 Revision History:
17 
18 --*/
19 #include "smt/smt_context.h"
20 #include "smt/smt_conflict_resolution.h"
21 #include "ast/ast_pp.h"
22 #include "ast/ast_ll_pp.h"
23 #include <memory>
24 
25 namespace smt {
26 
27 
justification_proof_wrapper(context & ctx,proof * pr,bool in_region)28     justification_proof_wrapper::justification_proof_wrapper(context & ctx, proof * pr, bool in_region):
29         justification(in_region),
30         m_proof(pr) {
31         ctx.get_manager().inc_ref(pr);
32     }
33 
del_eh(ast_manager & m)34     void justification_proof_wrapper::del_eh(ast_manager & m) {
35         m.dec_ref(m_proof);
36         m_proof = nullptr;
37     }
38 
mk_proof(conflict_resolution & cr)39     proof * justification_proof_wrapper::mk_proof(conflict_resolution & cr) {
40         return m_proof;
41     }
42 
unit_resolution_justification(region & r,justification * js,unsigned num_lits,literal const * lits)43     unit_resolution_justification::unit_resolution_justification(region & r,
44                                                                  justification * js,
45                                                                  unsigned num_lits,
46                                                                  literal const * lits):
47         m_antecedent(js),
48         m_num_literals(num_lits) {
49         SASSERT(!js || js->in_region());
50         m_literals = new (r) literal[num_lits];
51         memcpy(m_literals, lits, sizeof(literal) * num_lits);
52         TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
53         SASSERT(m_num_literals > 0);
54     }
55 
unit_resolution_justification(justification * js,unsigned num_lits,literal const * lits)56     unit_resolution_justification::unit_resolution_justification(justification * js,
57                                                                  unsigned num_lits,
58                                                                  literal const * lits):
59         justification(false), // object is not allocated in a region
60         m_antecedent(js),
61         m_num_literals(num_lits) {
62         SASSERT(!js || !js->in_region());
63         m_literals = alloc_vect<literal>(num_lits);
64         memcpy(m_literals, lits, sizeof(literal) * num_lits);
65         TRACE("unit_resolution_justification_bug", tout << literal_vector(num_lits, lits) << "\n";);
66         SASSERT(num_lits != 0);
67     }
68 
~unit_resolution_justification()69     unit_resolution_justification::~unit_resolution_justification() {
70         if (!in_region()) {
71             dealloc_svect(m_literals); // I don't need to invoke destructor...
72             dealloc(m_antecedent);
73         }
74     }
75 
get_antecedents(conflict_resolution & cr)76     void unit_resolution_justification::get_antecedents(conflict_resolution & cr) {
77         if (m_antecedent)
78             cr.mark_justification(m_antecedent);
79         for (unsigned i = 0; i < m_num_literals; i++)
80             cr.mark_literal(m_literals[i]);
81     }
82 
mk_proof(conflict_resolution & cr)83     proof * unit_resolution_justification::mk_proof(conflict_resolution & cr) {
84         SASSERT(m_antecedent);
85         ast_manager& m = cr.get_manager();
86         proof_ref_vector prs(m);
87         proof * pr = cr.get_proof(m_antecedent);
88         if (!pr)
89             return pr;
90         prs.push_back(pr);
91         for (unsigned i = 0; i < m_num_literals; i++) {
92             proof * pr = cr.get_proof(m_literals[i]);
93             if (!pr)
94                 return pr;
95             else
96                 prs.push_back(pr);
97         }
98         TRACE("unit_resolution_justification_bug",
99             tout << "in mk_proof\n" << literal_vector(m_num_literals, m_literals) << "\n";
100             for (proof* p : prs) tout << mk_ll_pp(m.get_fact(p), m););
101         return m.mk_unit_resolution(prs.size(), prs.data());
102     }
103 
get_antecedents(conflict_resolution & cr)104     void eq_conflict_justification::get_antecedents(conflict_resolution & cr) {
105         SASSERT(m_node1->get_root()->is_interpreted());
106         SASSERT(m_node2->get_root()->is_interpreted());
107         cr.mark_eq(m_node1, m_node1->get_root());
108         cr.mark_eq(m_node2, m_node2->get_root());
109         cr.mark_justified_eq(m_node1, m_node2, m_js);
110     }
111 
mk_proof(conflict_resolution & cr)112     proof * eq_conflict_justification::mk_proof(conflict_resolution & cr) {
113         ast_manager & m = cr.get_manager();
114         bool visited = true;
115         ptr_buffer<proof> prs;
116 
117         if (m_node1 != m_node1->get_root()) {
118             proof * pr = cr.get_proof(m_node1, m_node1->get_root());
119             if (pr && m.proofs_enabled())
120                 pr = m.mk_symmetry(pr);
121             prs.push_back(pr);
122             if (!pr)
123                 visited = false;
124         }
125 
126         SASSERT(m_node1 != m_node2);
127         proof * pr = cr.get_proof(m_node1, m_node2, m_js);
128         prs.push_back(pr);
129         if (!pr)
130             visited = false;
131 
132         if (m_node2 != m_node2->get_root()) {
133             proof * pr = cr.get_proof(m_node2, m_node2->get_root());
134             prs.push_back(pr);
135             if (!pr)
136                 visited = false;
137         }
138 
139         if (!visited)
140             return nullptr;
141 
142         expr * lhs = m_node1->get_root()->get_expr();
143         expr * rhs = m_node2->get_root()->get_expr();
144         proof * pr1 = m.mk_transitivity(prs.size(), prs.data(), lhs, rhs);
145         proof * pr2 = m.mk_rewrite(m.mk_eq(lhs, rhs), m.mk_false());
146         return m.mk_modus_ponens(pr1, pr2);
147     }
148 
get_antecedents(conflict_resolution & cr)149     void eq_root_propagation_justification::get_antecedents(conflict_resolution & cr) {
150         cr.mark_eq(m_node, m_node->get_root());
151     }
152 
mk_proof(conflict_resolution & cr)153     proof * eq_root_propagation_justification::mk_proof(conflict_resolution & cr) {
154         ast_manager & m = cr.get_manager();
155         expr * var = m_node->get_expr();
156         expr * val = m_node->get_root()->get_expr();
157         SASSERT(m.is_true(val) || m.is_false(val));
158         proof * pr1 = cr.get_proof(m_node, m_node->get_root());
159         if (pr1) {
160             expr * lit;
161             if (m.is_true(val))
162                 lit = var;
163             else
164                 lit = m.mk_not(var);
165             proof * pr2 = m.mk_rewrite(m.get_fact(pr1), lit);
166             return m.mk_modus_ponens(pr1, pr2);
167         }
168         return nullptr;
169     }
170 
get_antecedents(conflict_resolution & cr)171     void eq_propagation_justification::get_antecedents(conflict_resolution & cr) {
172         if (m_node1 != m_node2) cr.mark_eq(m_node1, m_node2);
173     }
174 
mk_proof(conflict_resolution & cr)175     proof * eq_propagation_justification::mk_proof(conflict_resolution & cr) {
176         return cr.get_proof(m_node1, m_node2);
177     }
178 
179 
get_antecedents(conflict_resolution & cr)180     void mp_iff_justification::get_antecedents(conflict_resolution & cr) {
181         if (m_node1 == m_node2)
182             return;
183         cr.mark_eq(m_node1, m_node2);
184         context & ctx = cr.get_context();
185         bool_var v    = ctx.enode2bool_var(m_node1);
186         lbool val     = ctx.get_assignment(v);
187         literal l(v, val == l_false);
188         cr.mark_literal(l);
189     }
190 
mk_proof(conflict_resolution & cr)191     proof * mp_iff_justification::mk_proof(conflict_resolution & cr) {
192         ast_manager& m = cr.get_manager();
193         if (m_node1 == m_node2)
194             return m.mk_reflexivity(m_node1->get_expr());
195         proof * pr1   = cr.get_proof(m_node1, m_node2);
196         context & ctx = cr.get_context();
197         bool_var v    = ctx.enode2bool_var(m_node1);
198         lbool val     = ctx.get_assignment(v);
199         literal l(v, val == l_false);
200         proof * pr2   = cr.get_proof(l);
201         if (pr1 && pr2) {
202 
203             proof * pr;
204             SASSERT(m.has_fact(pr1));
205             SASSERT(m.has_fact(pr2));
206             app* fact1 = to_app(m.get_fact(pr1));
207             app* fact2 = to_app(m.get_fact(pr2));
208             SASSERT(m.is_iff(fact1));
209             if (fact1->get_arg(1) == fact2) {
210                 pr1 = m.mk_symmetry(pr1);
211                 fact1 = to_app(m.get_fact(pr1));
212             }
213             SASSERT(m.is_iff(fact1));
214 
215             if (l.sign()) {
216                 SASSERT(m.is_not(fact2));
217                 expr* lhs = fact1->get_arg(0);
218                 expr* rhs = fact1->get_arg(1);
219                 if (lhs != fact2->get_arg(0)) {
220                     pr1 = m.mk_symmetry(pr1);
221                     fact1 = to_app(m.get_fact(pr1));
222                     std::swap(lhs, rhs);
223                 }
224                 SASSERT(lhs == fact2->get_arg(0));
225                 app* new_lhs = fact2;
226                 app* new_rhs = m.mk_not(rhs);
227                 pr1 = m.mk_congruence(new_lhs, new_rhs, 1, &pr1);
228             }
229             pr = m.mk_modus_ponens(pr2, pr1);
230 
231             TRACE("mp_iff_justification", tout << mk_pp(fact1, m) << "\n" << mk_pp(fact2, m) << "\n" <<
232                   mk_pp(m.get_fact(pr), m) << "\n";);
233             return pr;
234         }
235         return nullptr;
236     }
237 
simple_justification(region & r,unsigned num_lits,literal const * lits)238     simple_justification::simple_justification(region & r, unsigned num_lits, literal const * lits):
239         m_num_literals(num_lits) {
240         if (num_lits != 0) {
241             m_literals = new (r) literal[num_lits];
242             memcpy(m_literals, lits, sizeof(literal) * num_lits);
243 #ifdef Z3DEBUG
244             for (unsigned i = 0; i < num_lits; i++) {
245                 SASSERT(lits[i] != null_literal);
246             }
247 #endif
248         }
249     }
250 
get_antecedents(conflict_resolution & cr)251     void simple_justification::get_antecedents(conflict_resolution & cr) {
252         for (unsigned i = 0; i < m_num_literals; i++)
253             cr.mark_literal(m_literals[i]);
254     }
255 
antecedent2proof(conflict_resolution & cr,ptr_buffer<proof> & result)256     bool simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) {
257         bool visited = true;
258         for (unsigned i = 0; i < m_num_literals; i++) {
259             proof * pr = cr.get_proof(m_literals[i]);
260             if (pr == nullptr)
261                 visited = false;
262             else
263                 result.push_back(pr);
264         }
265         return visited;
266     }
267 
mk_proof(conflict_resolution & cr)268     proof * theory_axiom_justification::mk_proof(conflict_resolution & cr) {
269         context & ctx   = cr.get_context();
270         ast_manager & m = cr.get_manager();
271         expr_ref_vector lits(m);
272         for (unsigned i = 0; i < m_num_literals; i++) {
273             expr_ref l(m);
274             ctx.literal2expr(m_literals[i], l);
275             lits.push_back(std::move(l));
276         }
277         if (lits.size() == 1)
278             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.data());
279         else
280             return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.data()), 0, nullptr, m_params.size(), m_params.data());
281     }
282 
mk_proof(conflict_resolution & cr)283     proof * theory_propagation_justification::mk_proof(conflict_resolution & cr) {
284         ptr_buffer<proof> prs;
285         if (!antecedent2proof(cr, prs))
286             return nullptr;
287         context & ctx = cr.get_context();
288         ast_manager & m = cr.get_manager();
289         expr_ref fact(m);
290         ctx.literal2expr(m_consequent, fact);
291         return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
292     }
293 
mk_proof(conflict_resolution & cr)294     proof * theory_conflict_justification::mk_proof(conflict_resolution & cr) {
295         ptr_buffer<proof> prs;
296         if (!antecedent2proof(cr, prs))
297             return nullptr;
298         ast_manager & m = cr.get_manager();
299         return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.data(), m_params.size(), m_params.data());
300     }
301 
ext_simple_justification(region & r,unsigned num_lits,literal const * lits,unsigned num_eqs,enode_pair const * eqs)302     ext_simple_justification::ext_simple_justification(region & r, unsigned num_lits, literal const * lits, unsigned num_eqs, enode_pair const * eqs):
303         simple_justification(r, num_lits, lits),
304         m_num_eqs(num_eqs) {
305         m_eqs = new (r) enode_pair[num_eqs];
306         std::uninitialized_copy(eqs, eqs + num_eqs, m_eqs);
307         DEBUG_CODE({
308             for (unsigned i = 0; i < num_eqs; i++) {
309                 SASSERT(eqs[i].first->get_root() == eqs[i].second->get_root());
310             }
311         });
312     }
313 
get_antecedents(conflict_resolution & cr)314     void ext_simple_justification::get_antecedents(conflict_resolution & cr) {
315         simple_justification::get_antecedents(cr);
316         for (unsigned i = 0; i < m_num_eqs; i++) {
317             enode_pair const & p = m_eqs[i];
318             cr.mark_eq(p.first, p.second);
319         }
320     }
321 
antecedent2proof(conflict_resolution & cr,ptr_buffer<proof> & result)322     bool ext_simple_justification::antecedent2proof(conflict_resolution & cr, ptr_buffer<proof> & result) {
323         bool visited = simple_justification::antecedent2proof(cr, result);
324         for (unsigned i = 0; i < m_num_eqs; i++) {
325             enode_pair const & p = m_eqs[i];
326             proof * pr = cr.get_proof(p.first, p.second);
327             if (pr == nullptr)
328                 visited = false;
329             else
330                 result.push_back(pr);
331         }
332         return visited;
333     }
334 
mk_proof(conflict_resolution & cr)335     proof * ext_theory_propagation_justification::mk_proof(conflict_resolution & cr) {
336         ptr_buffer<proof> prs;
337         if (!antecedent2proof(cr, prs))
338             return nullptr;
339         context & ctx = cr.get_context();
340         ast_manager & m = cr.get_manager();
341         expr_ref fact(m);
342         ctx.literal2expr(m_consequent, fact);
343         return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
344     }
345 
mk_proof(conflict_resolution & cr)346     proof * ext_theory_conflict_justification::mk_proof(conflict_resolution & cr) {
347         ptr_buffer<proof> prs;
348         if (!antecedent2proof(cr, prs))
349             return nullptr;
350         ast_manager & m = cr.get_manager();
351         return m.mk_th_lemma(m_th_id, m.mk_false(), prs.size(), prs.data(), m_params.size(), m_params.data());
352     }
353 
mk_proof(conflict_resolution & cr)354     proof * ext_theory_eq_propagation_justification::mk_proof(conflict_resolution & cr) {
355         ptr_buffer<proof> prs;
356         if (!antecedent2proof(cr, prs))
357             return nullptr;
358         ast_manager & m = cr.get_manager();
359         context & ctx   = cr.get_context();
360         expr * fact     = ctx.mk_eq_atom(m_lhs->get_expr(), m_rhs->get_expr());
361         return m.mk_th_lemma(m_th_id, fact, prs.size(), prs.data(), m_params.size(), m_params.data());
362     }
363 
364 
theory_lemma_justification(family_id fid,context & ctx,unsigned num_lits,literal const * lits,unsigned num_params,parameter * params)365     theory_lemma_justification::theory_lemma_justification(family_id fid, context & ctx, unsigned num_lits, literal const * lits,
366                                                            unsigned num_params, parameter* params):
367         justification(false),
368         m_th_id(fid),
369         m_params(num_params, params),
370         m_num_literals(num_lits) {
371         ast_manager& m = ctx.get_manager();
372         m_literals        = alloc_svect(expr*, num_lits);
373         for (unsigned i   = 0; i < num_lits; i++) {
374             bool sign     = lits[i].sign();
375             expr * v      = ctx.bool_var2expr(lits[i].var());
376             m.inc_ref(v);
377             m_literals[i] = TAG(expr*, v, sign);
378         }
379         SASSERT(!in_region());
380     }
381 
~theory_lemma_justification()382     theory_lemma_justification::~theory_lemma_justification() {
383         SASSERT(!in_region());
384         dealloc_svect(m_literals);
385     }
386 
del_eh(ast_manager & m)387     void theory_lemma_justification::del_eh(ast_manager & m) {
388         for (unsigned i = 0; i < m_num_literals; i++) {
389             expr* v = UNTAG(expr*, m_literals[i]);
390             m.dec_ref(v);
391         }
392         m_params.reset();
393     }
394 
mk_proof(conflict_resolution & cr)395     proof * theory_lemma_justification::mk_proof(conflict_resolution & cr) {
396         ast_manager & m = cr.get_manager();
397         expr_ref_vector lits(m);
398         for (unsigned i = 0; i < m_num_literals; i++) {
399             bool sign   = GET_TAG(m_literals[i]) != 0;
400             expr * v    = UNTAG(expr*, m_literals[i]);
401             lits.push_back(sign ? m.mk_not(v) : v);
402         }
403         if (lits.size() == 1)
404             return m.mk_th_lemma(m_th_id, lits.get(0), 0, nullptr, m_params.size(), m_params.data());
405         else
406             return m.mk_th_lemma(m_th_id, m.mk_or(lits.size(), lits.data()), 0, nullptr, m_params.size(), m_params.data());
407     }
408 
409 };
410 
411