1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 --*/
5
6 #include "ast/proofs/proof_checker.h"
7 #include "ast/ast_ll_pp.h"
8 #include "ast/ast_pp.h"
9 #include "ast/ast_smt_pp.h"
10 #include "ast/arith_decl_plugin.h"
11 #include "ast/rewriter/th_rewriter.h"
12 #include "ast/rewriter/var_subst.h"
13
14 #define IS_EQUIV(_e_) m.is_eq(_e_)
15
16 #define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
17
hyp_decl_plugin()18 proof_checker::hyp_decl_plugin::hyp_decl_plugin() :
19 m_cons(nullptr),
20 m_atom(nullptr),
21 m_nil(nullptr),
22 m_cell(nullptr) {
23 }
24
finalize()25 void proof_checker::hyp_decl_plugin::finalize() {
26 m_manager->dec_ref(m_cons);
27 m_manager->dec_ref(m_atom);
28 m_manager->dec_ref(m_nil);
29 m_manager->dec_ref(m_cell);
30 }
31
set_manager(ast_manager * m,family_id id)32 void proof_checker::hyp_decl_plugin::set_manager(ast_manager* m, family_id id) {
33 decl_plugin::set_manager(m,id);
34 m_cell = m->mk_sort(symbol("cell"), sort_info(id, CELL_SORT));
35 m_cons = m->mk_func_decl(symbol("cons"), m_cell, m_cell, m_cell, func_decl_info(id, OP_CONS));
36 m_atom = m->mk_func_decl(symbol("atom"), m->mk_bool_sort(), m_cell, func_decl_info(id, OP_ATOM));
37 m_nil = m->mk_const_decl(symbol("nil"), m_cell, func_decl_info(id, OP_NIL));
38 m->inc_ref(m_cell);
39 m->inc_ref(m_cons);
40 m->inc_ref(m_atom);
41 m->inc_ref(m_nil);
42 }
43
mk_sort(decl_kind k,unsigned num_parameters,parameter const * parameters)44 sort * proof_checker::hyp_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) {
45 SASSERT(k == CELL_SORT);
46 return m_cell;
47 }
48
mk_func_decl(decl_kind k)49 func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(decl_kind k) {
50 switch(k) {
51 case OP_CONS: return m_cons;
52 case OP_ATOM: return m_atom;
53 case OP_NIL: return m_nil;
54 default:
55 UNREACHABLE();
56 return nullptr;
57 }
58 }
59
mk_func_decl(decl_kind k,unsigned num_parameters,parameter const * parameters,unsigned arity,sort * const * domain,sort * range)60 func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(
61 decl_kind k, unsigned num_parameters, parameter const * parameters,
62 unsigned arity, sort * const * domain, sort * range) {
63 return mk_func_decl(k);
64 }
65
mk_func_decl(decl_kind k,unsigned num_parameters,parameter const * parameters,unsigned num_args,expr * const * args,sort * range)66 func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(
67 decl_kind k, unsigned num_parameters, parameter const * parameters,
68 unsigned num_args, expr * const * args, sort * range) {
69 return mk_func_decl(k);
70 }
71
get_op_names(svector<builtin_name> & op_names,symbol const & logic)72 void proof_checker::hyp_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
73 if (logic == symbol::null) {
74 op_names.push_back(builtin_name("cons", OP_CONS));
75 op_names.push_back(builtin_name("atom", OP_ATOM));
76 op_names.push_back(builtin_name("nil", OP_NIL));
77 }
78 }
79
get_sort_names(svector<builtin_name> & sort_names,symbol const & logic)80 void proof_checker::hyp_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
81 if (logic == symbol::null) {
82 sort_names.push_back(builtin_name("cell", CELL_SORT));
83 }
84 }
85
proof_checker(ast_manager & m)86 proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m),
87 m_dump_lemmas(false), m_logic("AUFLIRA"), m_proof_lemma_id(0) {
88 symbol fam_name("proof_hypothesis");
89 if (!m.has_plugin(fam_name)) {
90 m.register_plugin(fam_name, alloc(hyp_decl_plugin));
91 }
92 m_hyp_fid = m.mk_family_id(fam_name);
93 // m_spc_fid = m.get_family_id("spc");
94 m_nil = m.mk_const(m_hyp_fid, OP_NIL);
95 }
96
check(proof * p,expr_ref_vector & side_conditions)97 bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
98 proof_ref curr(m);
99 m_todo.push_back(p);
100
101 bool result = true;
102 while (result && !m_todo.empty()) {
103 curr = m_todo.back();
104 m_todo.pop_back();
105 result = check1(curr.get(), side_conditions);
106 if (!result) {
107 IF_VERBOSE(1, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););
108 }
109 }
110
111 m_hypotheses.reset();
112 m_pinned.reset();
113 m_todo.reset();
114 m_marked.reset();
115
116 return result;
117 }
118
check1(proof * p,expr_ref_vector & side_conditions)119 bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) {
120 if (p->get_family_id() == m.get_basic_family_id()) {
121 return check1_basic(p, side_conditions);
122 }
123 #if 0
124 if (p->get_family_id() == m_spc_fid) {
125 return check1_spc(p, side_conditions);
126 }
127 #endif
128 return false;
129 }
130
check1_spc(proof * p,expr_ref_vector & side_conditions)131 bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
132 #if 0
133 decl_kind k = p->get_decl_kind();
134 bool is_univ = false;
135 expr_ref fact(m), fml(m);
136 expr_ref body(m), fml1(m), fml2(m);
137 sort_ref_vector sorts(m);
138 proof_ref p1(m), p2(m);
139 proof_ref_vector proofs(m);
140
141 if (match_proof(p, proofs)) {
142 for (proof* pr : proofs) {
143 add_premise(pr);
144 }
145 }
146 switch(k) {
147 case PR_DEMODULATION: {
148 if (match_proof(p, p1) &&
149 match_fact(p, fact) &&
150 match_fact(p1.get(), fml) &&
151 match_quantifier(fml.get(), is_univ, sorts, body) &&
152 is_univ) {
153 // TBD: check that fml is an instance of body.
154 return true;
155 }
156 return false;
157 }
158 case PR_SPC_REWRITE:
159 case PR_SUPERPOSITION:
160 case PR_EQUALITY_RESOLUTION:
161 case PR_SPC_RESOLUTION:
162 case PR_FACTORING:
163 case PR_SPC_DER: {
164 if (match_fact(p, fact)) {
165 expr_ref_vector rewrite_eq(m);
166 rewrite_eq.push_back(fact.get());
167 for (unsigned i = 0; i < proofs.size(); ++i) {
168 if (match_fact(proofs[i].get(), fml)) {
169 rewrite_eq.push_back(m.mk_not(fml.get()));
170 }
171 }
172 expr_ref rewrite_cond(m);
173 rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
174 side_conditions.push_back(rewrite_cond.get());
175 return true;
176 }
177 return false;
178 }
179 default:
180 UNREACHABLE();
181 }
182 return false;
183 #else
184 return true;
185 #endif
186 }
187
check1_basic(proof * p,expr_ref_vector & side_conditions)188 bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
189 decl_kind k = p->get_decl_kind();
190 expr* fml0 = nullptr, *fml1 = nullptr, *fml2 = nullptr, *fml = nullptr;
191 expr* t1 = nullptr, *t2 = nullptr;
192 expr* s1 = nullptr, *s2 = nullptr;
193 expr* u1 = nullptr, *u2 = nullptr;
194 expr* fact = nullptr, *body1 = nullptr;
195 expr* l1 = nullptr, *l2 = nullptr, *r1 = nullptr, *r2 = nullptr;
196 func_decl* d1 = nullptr, *d2 = nullptr, *d3 = nullptr;
197 proof* p0 = nullptr, *p1 = nullptr, *p2 = nullptr;
198 proof_ref_vector proofs(m);
199 func_decl* f1 = nullptr, *f2 = nullptr;
200 ptr_vector<expr> terms1, terms2, terms;
201 sort_ref_vector decls1(m), decls2(m);
202
203 if (match_proof(p, proofs)) {
204 for (proof* pr : proofs) {
205 add_premise(pr);
206 }
207 }
208
209 switch(k) {
210 case PR_UNDEF:
211 return true;
212 case PR_TRUE:
213 return true;
214 case PR_ASSERTED:
215 return true;
216 case PR_GOAL:
217 return true;
218 case PR_MODUS_PONENS: {
219 if (match_fact(p, fact) &&
220 match_proof(p, p0, p1) &&
221 match_fact(p0, fml0) &&
222 match_fact(p1, fml1) &&
223 (match_implies(fml1, t1, t2) || match_iff(fml1, t1, t2)) &&
224 (fml0 == t1) &&
225 (fact == t2)) {
226 return true;
227 }
228 UNREACHABLE();
229 return false;
230 }
231 case PR_REFLEXIVITY: {
232 if (match_fact(p, fact) &&
233 match_proof(p) &&
234 (match_equiv(fact, t1, t2) || match_oeq(fact, t1, t2)) &&
235 (t1 == t2)) {
236 return true;
237 }
238 UNREACHABLE();
239 return false;
240 }
241 case PR_SYMMETRY: {
242 if (match_fact(p, fact) &&
243 match_proof(p, p1) &&
244 match_fact(p1, fml) &&
245 match_binary(fact, d1, l1, r1) &&
246 match_binary(fml, d2, l2, r2) &&
247 SAME_OP(d1, d2) &&
248 l1 == r2 &&
249 r1 == l2) {
250 // TBD d1, d2 is a symmetric predicate
251 return true;
252 }
253 UNREACHABLE();
254 return false;
255 }
256 case PR_TRANSITIVITY: {
257 if (match_fact(p, fact) &&
258 match_proof(p, p1, p2) &&
259 match_fact(p1, fml1) &&
260 match_fact(p2, fml2) &&
261 match_binary(fact, d1, t1, t2) &&
262 match_binary(fml1, d2, s1, s2) &&
263 match_binary(fml2, d3, u1, u2) &&
264 d1 == d2 &&
265 d2 == d3 &&
266 t1 == s1 &&
267 s2 == u1 &&
268 u2 == t2) {
269 // TBD d1 is some transitive predicate.
270 return true;
271 }
272 UNREACHABLE();
273 return false;
274 }
275 case PR_TRANSITIVITY_STAR: {
276 if (match_fact(p, fact) &&
277 match_binary(fact, d1, t1, t2)) {
278 u_map<bool> vertices;
279 // TBD check that d1 is transitive, symmetric.
280 for (proof* pr : proofs) {
281 if (match_fact(pr, fml) &&
282 match_binary(fml, d2, s1, s2) &&
283 d1 == d2) {
284 unsigned id1 = s1->get_id();
285 unsigned id2 = s2->get_id();
286 #define INSERT(_id) if (vertices.contains(_id)) vertices.remove(_id); else vertices.insert(_id, true);
287 INSERT(id1);
288 INSERT(id2);
289 }
290 else {
291 UNREACHABLE();
292 return false;
293 }
294 }
295 return
296 vertices.size() == 2 &&
297 vertices.contains(t1->get_id()) &&
298 vertices.contains(t2->get_id());
299 }
300 UNREACHABLE();
301 return false;
302 }
303 case PR_MONOTONICITY: {
304 TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
305 if (match_fact(p, fact) &&
306 match_binary(fact, d1, t1, t2) &&
307 match_app(t1, f1, terms1) &&
308 match_app(t2, f2, terms2) &&
309 f1 == f2 &&
310 terms1.size() == terms2.size()) {
311 // TBD: d1 is monotone.
312 for (unsigned i = 0; i < terms1.size(); ++i) {
313 expr* term1 = terms1[i];
314 expr* term2 = terms2[i];
315 if (term1 != term2) {
316 bool found = false;
317 for (proof* pr : proofs) {
318 found |=
319 match_fact(pr, fml) &&
320 match_binary(fml, d2, s1, s2) &&
321 SAME_OP(d1, d2) &&
322 s1 == term1 &&
323 s2 == term2;
324 }
325 if (!found) {
326 UNREACHABLE();
327 return false;
328 }
329 }
330 }
331 return true;
332 }
333 UNREACHABLE();
334 return false;
335 }
336 case PR_QUANT_INTRO: {
337 if (match_proof(p, p1) &&
338 match_fact(p, fact) &&
339 match_fact(p1, fml) &&
340 (is_lambda(fact) || is_lambda(fml)))
341 return true;
342
343 if (match_proof(p, p1) &&
344 match_fact(p, fact) &&
345 match_fact(p1, fml) &&
346 (match_iff(fact, t1, t2) || match_oeq(fact, t1, t2)) &&
347 (match_iff(fml, s1, s2) || match_oeq(fml, s1, s2)) &&
348 m.is_oeq(fact) == m.is_oeq(fml) &&
349 is_quantifier(t1) &&
350 is_quantifier(t2) &&
351 to_quantifier(t1)->get_expr() == s1 &&
352 to_quantifier(t2)->get_expr() == s2 &&
353 to_quantifier(t1)->get_num_decls() == to_quantifier(t2)->get_num_decls() &&
354 to_quantifier(t1)->get_kind() == to_quantifier(t2)->get_kind()) {
355 quantifier* q1 = to_quantifier(t1);
356 quantifier* q2 = to_quantifier(t2);
357 for (unsigned i = 0; i < q1->get_num_decls(); ++i) {
358 if (q1->get_decl_sort(i) != q2->get_decl_sort(i)) {
359 // term is not well-typed.
360 UNREACHABLE();
361 return false;
362 }
363 }
364 return true;
365 }
366 UNREACHABLE();
367 return false;
368 }
369 case PR_BIND:
370 // it is a lambda expression returning a proof object.
371 if (!is_lambda(to_app(p)->get_arg(0)))
372 return false;
373 // check that body is a proof object.
374 return true;
375
376 case PR_DISTRIBUTIVITY: {
377 if (match_fact(p, fact) &&
378 match_proof(p) &&
379 match_equiv(fact, t1, t2)) {
380 side_conditions.push_back(fact);
381 return true;
382 }
383 UNREACHABLE();
384 return false;
385 }
386 case PR_AND_ELIM: {
387 if (match_proof(p, p1) &&
388 match_fact(p, fact) &&
389 match_fact(p1, fml) &&
390 match_and(fml, terms)) {
391 for (expr* t : terms)
392 if (t == fact) return true;
393 }
394 UNREACHABLE();
395 return false;
396 }
397 case PR_NOT_OR_ELIM: {
398
399 if (match_proof(p, p1) &&
400 match_fact(p, fact) &&
401 match_fact(p1, fml) &&
402 match_not(fml, fml1) &&
403 match_or(fml1, terms)) {
404 for (expr* t : terms) {
405 if (match_negated(t, fact)) {
406 return true;
407 }
408 }
409 }
410 UNREACHABLE();
411 return false;
412 }
413 case PR_REWRITE: {
414 if (match_fact(p, fact) &&
415 match_proof(p) &&
416 match_equiv(fact, t1, t2)) {
417 side_conditions.push_back(fact);
418 return true;
419 }
420 IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
421 return false;
422 }
423 case PR_REWRITE_STAR: {
424 if (match_fact(p, fact) &&
425 match_equiv(fact, t1, t2)) {
426 expr_ref_vector rewrite_eq(m);
427 rewrite_eq.push_back(fact);
428 for (proof* pr : proofs) {
429 if (match_fact(pr, fml)) {
430 rewrite_eq.push_back(m.mk_not(fml));
431 }
432 }
433 expr_ref rewrite_cond(m);
434 rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.data());
435 side_conditions.push_back(rewrite_cond.get());
436 return true;
437 }
438 IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m););
439 return false;
440 }
441 case PR_PULL_QUANT: {
442 if (match_proof(p) &&
443 match_fact(p, fact) &&
444 match_iff(fact, t1, t2) &&
445 is_quantifier(t2)) {
446 // TBD: check the enchilada.
447 return true;
448 }
449 IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
450 return false;
451 }
452 case PR_PUSH_QUANT: {
453 if (match_proof(p) &&
454 match_fact(p, fact) &&
455 match_iff(fact, t1, t2) &&
456 is_quantifier(t1) &&
457 match_and(to_quantifier(t1)->get_expr(), terms1) &&
458 match_and(t2, terms2) &&
459 terms1.size() == terms2.size()) {
460 quantifier * q1 = to_quantifier(t1);
461 for (unsigned i = 0; i < terms1.size(); ++i) {
462 if (is_quantifier(terms2[i]) &&
463 to_quantifier(terms2[i])->get_expr() == terms1[i] &&
464 to_quantifier(terms2[i])->get_num_decls() == q1->get_num_decls()) {
465 // ok.
466 }
467 else {
468 return false;
469 }
470 }
471 }
472 UNREACHABLE();
473 return false;
474 }
475 case PR_ELIM_UNUSED_VARS: {
476 if (match_proof(p) &&
477 match_fact(p, fact) &&
478 match_iff(fact, t1, t2)) {
479 // TBD:
480 // match_quantifier(t1, is_forall1, decls1, body1)
481 // filter out decls1 that occur in body1.
482 // if list is empty, then t2 could be just body1.
483 // otherwise t2 is also a quantifier.
484 return true;
485 }
486 IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
487 return false;
488 }
489 case PR_DER: {
490 bool is_forall = false;
491 if (match_proof(p) &&
492 match_fact(p, fact) &&
493 match_iff(fact, t1, t2) &&
494 match_quantifier(t1, is_forall, decls1, body1) &&
495 is_forall) {
496 // TBD: check that terms are set of equalities.
497 // t2 is an instance of a predicate in terms1
498 return true;
499 }
500 IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";);
501 return false;
502 }
503 case PR_HYPOTHESIS: {
504 // TBD all branches with hypotheses must be closed by a later lemma.
505 if (match_proof(p) &&
506 match_fact(p, fml)) {
507 return true;
508 }
509 return false;
510 }
511 case PR_LEMMA: {
512 if (match_proof(p, p1) &&
513 match_fact(p, fact) &&
514 match_fact(p1, fml) &&
515 m.is_false(fml)) {
516 expr_ref_vector hypotheses(m);
517 expr_ref_vector ors(m);
518 get_hypotheses(p1, hypotheses);
519 if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
520 // Suppose fact is (or a b c) and hypothesis is (not (or a b c))
521 // That is, (or a b c) should be viewed as a 'quoted expression' and a unary clause,
522 // instead of a clause with three literals.
523 return true;
524 }
525 get_ors(fact, ors);
526 for (unsigned i = 0; i < hypotheses.size(); ++i) {
527 bool found = false;
528 unsigned j;
529 for (j = 0; !found && j < ors.size(); ++j) {
530 found = match_negated(ors[j].get(), hypotheses[i].get());
531 }
532 if (!found) {
533 TRACE("pr_lemma_bug",
534 tout << "i: " << i << "\n";
535 tout << "ORs:\n" << ors << "\n";
536 tout << "HYPOTHESIS:\n" << hypotheses << "\n";
537 );
538 UNREACHABLE();
539 return false;
540 }
541 TRACE("proof_checker", tout << "Matched:\n";
542 ast_ll_pp(tout, m, hypotheses[i].get());
543 ast_ll_pp(tout, m, ors[j-1].get()););
544 }
545 return true;
546 }
547 UNREACHABLE();
548 return false;
549 }
550 case PR_UNIT_RESOLUTION: {
551 if (match_fact(p, fact) &&
552 proofs.size() == 2 &&
553 match_fact(proofs[0].get(), fml1) &&
554 match_fact(proofs[1].get(), fml2) &&
555 m.is_complement(fml1, fml2) &&
556 m.is_false(fact)) {
557 return true;
558 }
559 if (match_fact(p, fact) &&
560 proofs.size() > 1 &&
561 match_fact(proofs.get(0), fml) &&
562 match_or(fml, terms1)) {
563 for (unsigned i = 1; i < proofs.size(); ++i) {
564 if (!match_fact(proofs.get(i), fml2)) {
565 return false;
566 }
567 bool found = false;
568 for (unsigned j = 0; !found && j < terms1.size(); ++j) {
569 if (m.is_complement(terms1.get(j), fml2)) {
570 found = true;
571 if (j + 1 < terms1.size()) {
572 terms1[j] = terms1.get(terms1.size()-1);
573 }
574 terms1.resize(terms1.size()-1);
575 }
576 }
577 if (!found) {
578 TRACE("pr_unit_bug",
579 tout << "Parents:\n";
580 for (unsigned i = 0; i < proofs.size(); i++) {
581 expr* p = nullptr;
582 match_fact(proofs.get(i), p);
583 tout << mk_pp(p, m) << "\n";
584 }
585 tout << "Fact:\n";
586 tout << mk_pp(fact, m) << "\n";
587 tout << "Clause:\n";
588 tout << mk_pp(fml, m) << "\n";
589 tout << "Could not find premise " << mk_pp(fml2, m) << "\n";
590 );
591
592 UNREACHABLE();
593 return false;
594 }
595 }
596 switch(terms1.size()) {
597 case 0:
598 return m.is_false(fact);
599 case 1:
600 return fact == terms1[0];
601 default: {
602 if (match_or(fact, terms2)) {
603 for (expr* term1 : terms1) {
604 bool found = false;
605 for (expr* term2 : terms2) {
606 found = term1 == term2;
607 if (found) break;
608 }
609 if (!found) {
610 IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
611 return false;
612 }
613 }
614 return true;
615 }
616 IF_VERBOSE(0, verbose_stream() << "Conclusion is not a disjunction:\n";
617 verbose_stream() << mk_pp(fml, m) << "\n";
618 verbose_stream() << mk_pp(fact, m) << "\n";);
619
620 return false;
621 }
622
623 }
624 }
625 UNREACHABLE();
626 return false;
627 }
628 case PR_IFF_TRUE: {
629 // iff_true(?rule(?p1, ?fml), (iff ?fml true))
630 if (match_proof(p, p1) &&
631 match_fact(p, fact) &&
632 match_fact(p1, fml1) &&
633 match_iff(fact, l1, r1) &&
634 fml1 == l1 &&
635 r1 == m.mk_true()) {
636 return true;
637 }
638 UNREACHABLE();
639 return false;
640 }
641 case PR_IFF_FALSE: {
642 // iff_false(?rule(?p1, (not ?fml)), (iff ?fml false))
643 if (match_proof(p, p1) &&
644 match_fact(p, fact) &&
645 match_fact(p1, fml1) &&
646 match_iff(fact, l1, r1) &&
647 match_not(fml1, t1) &&
648 t1 == l1 &&
649 r1 == m.mk_false()) {
650 return true;
651 }
652 UNREACHABLE();
653 return false;
654 }
655 case PR_COMMUTATIVITY: {
656 // commutativity(= (?c ?t1 ?t2) (?c ?t2 ?t1))
657 if (match_fact(p, fact) &&
658 match_proof(p) &&
659 match_equiv(fact, t1, t2) &&
660 match_binary(t1, d1, s1, s2) &&
661 match_binary(t2, d2, u1, u2) &&
662 s1 == u2 &&
663 s2 == u1 &&
664 d1 == d2 &&
665 d1->is_commutative()) {
666 return true;
667 }
668 UNREACHABLE();
669 return false;
670 }
671 case PR_DEF_AXIOM: {
672 // axiom(?fml)
673 if (match_fact(p, fact) &&
674 match_proof(p) &&
675 m.is_bool(fact)) {
676 return true;
677 }
678 UNREACHABLE();
679 return false;
680 }
681 case PR_DEF_INTRO: {
682 // def_intro(?fml)
683 //
684 // ?fml: forall x . ~p(x) or e(x) and forall x . ~e(x) or p(x)
685 // : forall x . ~cond(x) or f(x) = then(x) and forall x . cond(x) or f(x) = else(x)
686 // : forall x . f(x) = e(x)
687 //
688 if (match_fact(p, fact) &&
689 match_proof(p) &&
690 m.is_bool(fact)) {
691 return true;
692 }
693 UNREACHABLE();
694 return false;
695 }
696 case PR_APPLY_DEF: {
697 if (match_fact(p, fact) &&
698 match_oeq(fact, t1, t2)) {
699 // TBD: must definitions be in proofs?
700 return true;
701 }
702 UNREACHABLE();
703 return false;
704 }
705 case PR_IFF_OEQ: {
706 // axiom(?rule(?p1,(iff ?t1 ?t2)), (~ ?t1 ?t2))
707 if (match_fact(p, fact) &&
708 match_proof(p, p1) &&
709 match_oeq(fact, t1, t2) &&
710 match_fact(p1, fml) &&
711 match_iff(fml, s1, s2) &&
712 s1 == t1 &&
713 s2 == t2) {
714 return true;
715 }
716 UNREACHABLE();
717 return false;
718 }
719 case PR_NNF_POS: {
720 // TBD:
721 return true;
722 }
723 case PR_NNF_NEG: {
724 // TBD:
725 return true;
726 }
727 case PR_SKOLEMIZE: {
728 // (exists ?x (p ?x y)) -> (p (sk y) y)
729 // (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
730 if (match_fact(p, fact) &&
731 match_oeq(fact, t1, t2)) {
732 quantifier* q = nullptr;
733 expr* e = t1;
734 bool is_forall = false;
735 if (match_not(t1, s1)) {
736 e = s1;
737 is_forall = true;
738 }
739 if (is_quantifier(e)) {
740 SASSERT(!is_lambda(e));
741 q = to_quantifier(e);
742 // TBD check that quantifier is properly instantiated
743 return is_forall == ::is_forall(q);
744 }
745 }
746 UNREACHABLE();
747 return false;
748 }
749 case PR_MODUS_PONENS_OEQ: {
750 if (match_fact(p, fact) &&
751 match_proof(p, p0, p1) &&
752 match_fact(p0, fml0) &&
753 match_fact(p1, fml1) &&
754 match_oeq(fml1, t1, t2) &&
755 fml0 == t1 &&
756 fact == t2) {
757 return true;
758 }
759 UNREACHABLE();
760 return false;
761 }
762 case PR_TH_LEMMA: {
763 SASSERT(p->get_decl()->get_num_parameters() > 0);
764 SASSERT(p->get_decl()->get_parameter(0).is_symbol());
765 if (symbol("arith") == p->get_decl()->get_parameter(0).get_symbol()) {
766 return check_arith_proof(p);
767 }
768 dump_proof(p);
769 return true;
770 }
771 case PR_QUANT_INST: {
772 // TODO
773 return true;
774 }
775 case PR_HYPER_RESOLVE: {
776 proof_ref_vector premises(m);
777 expr_ref_vector fmls(m);
778 expr_ref conclusion(m), premise(m), premise0(m), premise1(m);
779 svector<std::pair<unsigned, unsigned> > positions;
780 vector<expr_ref_vector> substs;
781 VERIFY(m.is_hyper_resolve(p, premises, conclusion, positions, substs));
782 var_subst vs(m, false);
783 for (unsigned i = 0; i < premises.size(); ++i) {
784 expr_ref_vector const& sub = substs[i];
785 premise = m.get_fact(premises[i].get());
786 if (!sub.empty()) {
787 if (is_forall(premise)) {
788 // SASSERT(to_quantifier(premise)->get_num_decls() == sub.size());
789 premise = to_quantifier(premise)->get_expr();
790 }
791 premise = vs(premise, sub.size(), sub.data());
792 }
793 fmls.push_back(premise.get());
794 TRACE("proof_checker",
795 tout << mk_pp(premise.get(), m) << "\n";
796 for (unsigned j = 0; j < sub.size(); ++j) {
797 tout << mk_pp(sub[j], m) << " ";
798 }
799 tout << "\n";);
800 }
801 premise0 = fmls[0].get();
802 for (unsigned i = 1; i < fmls.size(); ++i) {
803 expr_ref lit1(m), lit2(m);
804 expr* lit3 = nullptr;
805 std::pair<unsigned, unsigned> pos = positions[i-1];
806 premise1 = fmls[i].get();
807 set_false(premise0, pos.first, lit1);
808 set_false(premise1, pos.second, lit2);
809 if (m.is_not(lit1, lit3) && lit3 == lit2) {
810 // ok
811 }
812 else if (m.is_not(lit2, lit3) && lit3 == lit1) {
813 // ok
814 }
815 else {
816 IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" <<
817 mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";);
818 }
819 fmls[i] = premise1;
820 }
821 fmls[0] = premise0;
822 premise0 = m.mk_or(fmls.size(), fmls.data());
823 if (is_forall(conclusion)) {
824 quantifier* q = to_quantifier(conclusion);
825 premise0 = m.mk_iff(premise0, q->get_expr());
826 premise0 = m.mk_forall(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), premise0);
827 }
828 else {
829 premise0 = m.mk_iff(premise0, conclusion);
830 }
831 side_conditions.push_back(premise0);
832 return true;
833 }
834 default:
835 UNREACHABLE();
836 return false;
837 }
838 }
839
840 /**
841 \brief Premises of the rules are of the form
842 (or l0 l1 l2 .. ln)
843 or
844 (=> (and ln+1 ln+2 .. ln+m) l0)
845 or in the most general (ground) form:
846 (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
847 In other words we use the following (Prolog style) convention for Horn
848 implications:
849 The head of a Horn implication is position 0,
850 the first conjunct in the body of an implication is position 1
851 the second conjunct in the body of an implication is position 2
852
853 Set the position provided in the argument to 'false'.
854 */
set_false(expr_ref & e,unsigned position,expr_ref & lit)855 void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
856 app* a = to_app(e);
857 expr* head, *body;
858 expr_ref_vector args(m);
859 if (m.is_or(e)) {
860 SASSERT(position < a->get_num_args());
861 args.append(a->get_num_args(), a->get_args());
862 lit = args[position].get();
863 args[position] = m.mk_false();
864 e = m.mk_or(args.size(), args.data());
865 }
866 else if (m.is_implies(e, body, head)) {
867 expr* const* heads = &head;
868 unsigned num_heads = 1;
869 if (m.is_or(head)) {
870 num_heads = to_app(head)->get_num_args();
871 heads = to_app(head)->get_args();
872 }
873 expr*const* bodies = &body;
874 unsigned num_bodies = 1;
875 if (m.is_and(body)) {
876 num_bodies = to_app(body)->get_num_args();
877 bodies = to_app(body)->get_args();
878 }
879 if (position < num_heads) {
880 args.append(num_heads, heads);
881 lit = args[position].get();
882 args[position] = m.mk_false();
883 e = m.mk_implies(body, m.mk_or(args.size(), args.data()));
884 }
885 else {
886 position -= num_heads;
887 args.append(num_bodies, bodies);
888 lit = m.mk_not(args[position].get());
889 args[position] = m.mk_true();
890 e = m.mk_implies(m.mk_and(args.size(), args.data()), head);
891 }
892 }
893 else if (position == 0) {
894 lit = e;
895 e = m.mk_false();
896 }
897 else {
898 IF_VERBOSE(0, verbose_stream() << position << "\n" << mk_pp(e, m) << "\n";);
899 UNREACHABLE();
900 }
901 }
902
match_fact(proof const * p,expr * & fact) const903 bool proof_checker::match_fact(proof const* p, expr*& fact) const {
904 if (m.is_proof(p) &&
905 m.has_fact(p)) {
906 fact = m.get_fact(p);
907 return true;
908 }
909 return false;
910 }
911
add_premise(proof * p)912 void proof_checker::add_premise(proof* p) {
913 if (!m_marked.is_marked(p)) {
914 m_marked.mark(p, true);
915 m_todo.push_back(p);
916 }
917 }
918
match_proof(proof const * p) const919 bool proof_checker::match_proof(proof const* p) const {
920 return
921 m.is_proof(p) &&
922 m.get_num_parents(p) == 0;
923 }
924
match_proof(proof const * p,proof * & p0) const925 bool proof_checker::match_proof(proof const* p, proof*& p0) const {
926 if (m.is_proof(p) &&
927 m.get_num_parents(p) == 1) {
928 p0 = m.get_parent(p, 0);
929 return true;
930 }
931 return false;
932 }
933
match_proof(proof const * p,proof * & p0,proof * & p1) const934 bool proof_checker::match_proof(proof const* p, proof*& p0, proof*& p1) const {
935 if (m.is_proof(p) &&
936 m.get_num_parents(p) == 2) {
937 p0 = m.get_parent(p, 0);
938 p1 = m.get_parent(p, 1);
939 return true;
940 }
941 return false;
942 }
943
match_proof(proof const * p,proof_ref_vector & parents) const944 bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
945 if (m.is_proof(p)) {
946 for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
947 parents.push_back(m.get_parent(p, i));
948 }
949 return true;
950 }
951 return false;
952 }
953
954
match_binary(expr const * e,func_decl * & d,expr * & t1,expr * & t2) const955 bool proof_checker::match_binary(expr const* e, func_decl*& d, expr*& t1, expr*& t2) const {
956 if (e->get_kind() == AST_APP &&
957 to_app(e)->get_num_args() == 2) {
958 d = to_app(e)->get_decl();
959 t1 = to_app(e)->get_arg(0);
960 t2 = to_app(e)->get_arg(1);
961 return true;
962 }
963 return false;
964 }
965
966
match_app(expr const * e,func_decl * & d,ptr_vector<expr> & terms) const967 bool proof_checker::match_app(expr const* e, func_decl*& d, ptr_vector<expr>& terms) const {
968 if (e->get_kind() == AST_APP) {
969 d = to_app(e)->get_decl();
970 for (expr* arg : *to_app(e)) {
971 terms.push_back(arg);
972 }
973 return true;
974 }
975 return false;
976 }
977
match_quantifier(expr const * e,bool & is_univ,sort_ref_vector & sorts,expr * & body) const978 bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr*& body) const {
979 if (is_quantifier(e)) {
980 quantifier const* q = to_quantifier(e);
981 is_univ = is_forall(q);
982 body = q->get_expr();
983 for (unsigned i = 0; i < q->get_num_decls(); ++i) {
984 sorts.push_back(q->get_decl_sort(i));
985 }
986 return true;
987 }
988 return false;
989 }
990
match_op(expr const * e,decl_kind k,expr * & t1,expr * & t2) const991 bool proof_checker::match_op(expr const* e, decl_kind k, expr*& t1, expr*& t2) const {
992 if (e->get_kind() == AST_APP &&
993 to_app(e)->get_family_id() == m.get_basic_family_id() &&
994 to_app(e)->get_decl_kind() == k &&
995 to_app(e)->get_num_args() == 2) {
996 t1 = to_app(e)->get_arg(0);
997 t2 = to_app(e)->get_arg(1);
998 return true;
999 }
1000 return false;
1001 }
1002
match_op(expr const * e,decl_kind k,ptr_vector<expr> & terms) const1003 bool proof_checker::match_op(expr const* e, decl_kind k, ptr_vector<expr>& terms) const {
1004 if (e->get_kind() == AST_APP &&
1005 to_app(e)->get_family_id() == m.get_basic_family_id() &&
1006 to_app(e)->get_decl_kind() == k) {
1007 for (expr* arg : *to_app(e))
1008 terms.push_back(arg);
1009 return true;
1010 }
1011 return false;
1012 }
1013
1014
match_op(expr const * e,decl_kind k,expr * & t) const1015 bool proof_checker::match_op(expr const* e, decl_kind k, expr*& t) const {
1016 if (e->get_kind() == AST_APP &&
1017 to_app(e)->get_family_id() == m.get_basic_family_id() &&
1018 to_app(e)->get_decl_kind() == k &&
1019 to_app(e)->get_num_args() == 1) {
1020 t = to_app(e)->get_arg(0);
1021 return true;
1022 }
1023 return false;
1024 }
1025
match_not(expr const * e,expr * & t) const1026 bool proof_checker::match_not(expr const* e, expr*& t) const {
1027 return match_op(e, OP_NOT, t);
1028 }
1029
match_or(expr const * e,ptr_vector<expr> & terms) const1030 bool proof_checker::match_or(expr const* e, ptr_vector<expr>& terms) const {
1031 return match_op(e, OP_OR, terms);
1032 }
1033
match_and(expr const * e,ptr_vector<expr> & terms) const1034 bool proof_checker::match_and(expr const* e, ptr_vector<expr>& terms) const {
1035 return match_op(e, OP_AND, terms);
1036 }
1037
match_iff(expr const * e,expr * & t1,expr * & t2) const1038 bool proof_checker::match_iff(expr const* e, expr*& t1, expr*& t2) const {
1039 return match_op(e, OP_EQ, t1, t2) && m.is_bool(t1);
1040 }
1041
match_equiv(expr const * e,expr * & t1,expr * & t2) const1042 bool proof_checker::match_equiv(expr const* e, expr*& t1, expr*& t2) const {
1043 return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
1044 }
1045
match_implies(expr const * e,expr * & t1,expr * & t2) const1046 bool proof_checker::match_implies(expr const* e, expr*& t1, expr*& t2) const {
1047 return match_op(e, OP_IMPLIES, t1, t2);
1048 }
1049
match_eq(expr const * e,expr * & t1,expr * & t2) const1050 bool proof_checker::match_eq(expr const* e, expr*& t1, expr*& t2) const {
1051 return match_op(e, OP_EQ, t1, t2);
1052 }
1053
match_oeq(expr const * e,expr * & t1,expr * & t2) const1054 bool proof_checker::match_oeq(expr const* e, expr*& t1, expr*& t2) const {
1055 return match_op(e, OP_OEQ, t1, t2);
1056 }
1057
match_negated(expr const * a,expr * b) const1058 bool proof_checker::match_negated(expr const* a, expr* b) const {
1059 expr* t = nullptr;
1060 return
1061 (match_not(a, t) && t == b) ||
1062 (match_not(b, t) && t == a);
1063 }
1064
get_ors(expr * e,expr_ref_vector & ors)1065 void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
1066 ptr_buffer<expr> buffer;
1067 if (m.is_or(e)) {
1068 app* a = to_app(e);
1069 ors.append(a->get_num_args(), a->get_args());
1070 }
1071 else {
1072 ors.push_back(e);
1073 }
1074 }
1075
1076
get_hypotheses(proof * p,expr_ref_vector & ante)1077 void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
1078 ptr_vector<proof> stack;
1079 expr* h = nullptr, *hyp = nullptr;
1080
1081 stack.push_back(p);
1082 while (!stack.empty()) {
1083 p = stack.back();
1084 SASSERT(m.is_proof(p));
1085 if (m_hypotheses.contains(p)) {
1086 stack.pop_back();
1087 continue;
1088 }
1089 if (is_hypothesis(p) && match_fact(p, hyp)) {
1090 hyp = mk_atom(hyp);
1091 m_pinned.push_back(hyp);
1092 m_hypotheses.insert(p, hyp);
1093 stack.pop_back();
1094 continue;
1095 }
1096 // in this system all hypotheses get bound by lemmas.
1097 if (m.is_lemma(p)) {
1098 m_hypotheses.insert(p, mk_nil());
1099 stack.pop_back();
1100 continue;
1101 }
1102 bool all_found = true;
1103 ptr_vector<expr> hyps;
1104 for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
1105 proof* p_i = m.get_parent(p, i);
1106 if (m_hypotheses.find(p_i, h)) {
1107 hyps.push_back(h);
1108 }
1109 else {
1110 stack.push_back(p_i);
1111 all_found = false;
1112 }
1113 }
1114 if (all_found) {
1115 h = mk_hyp(hyps.size(), hyps.data());
1116 m_pinned.push_back(h);
1117 m_hypotheses.insert(p, h);
1118 stack.pop_back();
1119 }
1120 }
1121
1122 //
1123 // dis-assemble the set of obtained hypotheses.
1124 //
1125 if (!m_hypotheses.find(p, h)) {
1126 UNREACHABLE();
1127 }
1128
1129 ptr_buffer<expr> hyps;
1130 ptr_buffer<expr> todo;
1131 expr_mark mark;
1132 todo.push_back(h);
1133 expr* a = nullptr, *b = nullptr;
1134
1135 while (!todo.empty()) {
1136 h = todo.back();
1137
1138 todo.pop_back();
1139 if (mark.is_marked(h)) {
1140 continue;
1141 }
1142 mark.mark(h, true);
1143 if (match_cons(h, a, b)) {
1144 todo.push_back(a);
1145 todo.push_back(b);
1146 }
1147 else if (match_atom(h, a)) {
1148 ante.push_back(a);
1149 }
1150 else {
1151 SASSERT(match_nil(h));
1152 }
1153 }
1154 TRACE("proof_checker",
1155 {
1156 ast_ll_pp(tout << "Getting hypotheses from: ", m, p);
1157 tout << "Found hypotheses:\n";
1158 for (unsigned i = 0; i < ante.size(); ++i) {
1159 ast_ll_pp(tout, m, ante[i].get());
1160 }
1161 });
1162
1163 }
1164
match_nil(expr const * e) const1165 bool proof_checker::match_nil(expr const* e) const {
1166 return
1167 is_app(e) &&
1168 to_app(e)->get_family_id() == m_hyp_fid &&
1169 to_app(e)->get_decl_kind() == OP_NIL;
1170 }
1171
match_cons(expr const * e,expr * & a,expr * & b) const1172 bool proof_checker::match_cons(expr const* e, expr*& a, expr*& b) const {
1173 if (is_app(e) &&
1174 to_app(e)->get_family_id() == m_hyp_fid &&
1175 to_app(e)->get_decl_kind() == OP_CONS) {
1176 a = to_app(e)->get_arg(0);
1177 b = to_app(e)->get_arg(1);
1178 return true;
1179 }
1180 return false;
1181 }
1182
1183
match_atom(expr const * e,expr * & a) const1184 bool proof_checker::match_atom(expr const* e, expr*& a) const {
1185 if (is_app(e) &&
1186 to_app(e)->get_family_id() == m_hyp_fid &&
1187 to_app(e)->get_decl_kind() == OP_ATOM) {
1188 a = to_app(e)->get_arg(0);
1189 return true;
1190 }
1191 return false;
1192 }
1193
mk_atom(expr * e)1194 expr* proof_checker::mk_atom(expr* e) {
1195 return m.mk_app(m_hyp_fid, OP_ATOM, e);
1196 }
1197
mk_cons(expr * a,expr * b)1198 expr* proof_checker::mk_cons(expr* a, expr* b) {
1199 return m.mk_app(m_hyp_fid, OP_CONS, a, b);
1200 }
1201
mk_nil()1202 expr* proof_checker::mk_nil() {
1203 return m_nil.get();
1204 }
1205
is_hypothesis(proof const * p) const1206 bool proof_checker::is_hypothesis(proof const* p) const {
1207 return
1208 m.is_proof(p) &&
1209 p->get_decl_kind() == PR_HYPOTHESIS;
1210 }
1211
mk_hyp(unsigned num_hyps,expr * const * hyps)1212 expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
1213 expr* result = nullptr;
1214 for (unsigned i = 0; i < num_hyps; ++i) {
1215 if (!match_nil(hyps[i])) {
1216 if (result) {
1217 result = mk_cons(result, hyps[i]);
1218 }
1219 else {
1220 result = hyps[i];
1221 }
1222 }
1223 }
1224 if (result == nullptr) {
1225 return mk_nil();
1226 }
1227 else {
1228 return result;
1229 }
1230 }
1231
dump_proof(proof const * pr)1232 void proof_checker::dump_proof(proof const* pr) {
1233 if (!m_dump_lemmas)
1234 return;
1235 SASSERT(m.has_fact(pr));
1236 expr * consequent = m.get_fact(pr);
1237 unsigned num = m.get_num_parents(pr);
1238 ptr_buffer<expr> antecedents;
1239 for (unsigned i = 0; i < num; i++) {
1240 proof * a = m.get_parent(pr, i);
1241 SASSERT(m.has_fact(a));
1242 antecedents.push_back(m.get_fact(a));
1243 }
1244 dump_proof(antecedents.size(), antecedents.data(), consequent);
1245 }
1246
dump_proof(unsigned num_antecedents,expr * const * antecedents,expr * consequent)1247 void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent) {
1248 char buffer[128];
1249 #ifdef _WINDOWS
1250 sprintf_s(buffer, Z3_ARRAYSIZE(buffer), "proof_lemma_%d.smt2", m_proof_lemma_id);
1251 #else
1252 sprintf(buffer, "proof_lemma_%d.smt2", m_proof_lemma_id);
1253 #endif
1254 std::ofstream out(buffer);
1255 ast_smt_pp pp(m);
1256 pp.set_benchmark_name("lemma");
1257 pp.set_status("unsat");
1258 pp.set_logic(symbol(m_logic.c_str()));
1259 for (unsigned i = 0; i < num_antecedents; i++)
1260 pp.add_assumption(antecedents[i]);
1261 expr_ref n(m);
1262 n = m.mk_not(consequent);
1263 pp.display_smt2(out, n);
1264 out.close();
1265 m_proof_lemma_id++;
1266 }
1267
check_arith_literal(bool is_pos,app * lit0,rational const & coeff,expr_ref & sum,bool & is_strict)1268 bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) {
1269 arith_util a(m);
1270 app* lit = lit0;
1271
1272 if (m.is_not(lit)) {
1273 lit = to_app(lit->get_arg(0));
1274 is_pos = !is_pos;
1275 }
1276 if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
1277 IF_VERBOSE(2, verbose_stream() << "Not arith literal: " << mk_pp(lit, m) << "\n";);
1278 return false;
1279 }
1280 SASSERT(lit->get_num_args() == 2);
1281 sort* s = lit->get_arg(0)->get_sort();
1282 bool is_int = a.is_int(s);
1283 if (!is_int && a.is_int_expr(lit->get_arg(0))) {
1284 is_int = true;
1285 s = a.mk_int();
1286 }
1287
1288 if (!is_int && is_pos && (a.is_gt(lit) || a.is_lt(lit))) {
1289 is_strict = true;
1290 }
1291 if (!is_int && !is_pos && (a.is_ge(lit) || a.is_le(lit))) {
1292 is_strict = true;
1293 }
1294
1295
1296 SASSERT(a.is_int(s) || a.is_real(s));
1297 expr_ref sign1(m), sign2(m), term(m);
1298 sign1 = a.mk_numeral(m.is_eq(lit)?coeff:abs(coeff), s);
1299 sign2 = a.mk_numeral(m.is_eq(lit)?-coeff:-abs(coeff), s);
1300 if (!sum.get()) {
1301 sum = a.mk_numeral(rational(0), s);
1302 }
1303
1304 expr* a0 = lit->get_arg(0);
1305 expr* a1 = lit->get_arg(1);
1306
1307 if (is_pos && (a.is_ge(lit) || a.is_gt(lit))) {
1308 std::swap(a0, a1);
1309 }
1310 if (!is_pos && (a.is_le(lit) || a.is_lt(lit))) {
1311 std::swap(a0, a1);
1312 }
1313
1314 //
1315 // Multiplying by coefficients over strict
1316 // and non-strict inequalities:
1317 //
1318 // (a <= b) * 2
1319 // (a - b <= 0) * 2
1320 // (2a - 2b <= 0)
1321
1322 // (a < b) * 2 <=>
1323 // (a +1 <= b) * 2 <=>
1324 // 2a + 2 <= 2b <=>
1325 // 2a+2-2b <= 0
1326
1327 bool strict_ineq =
1328 is_pos?(a.is_gt(lit) || a.is_lt(lit)):(a.is_ge(lit) || a.is_le(lit));
1329
1330 if (is_int && strict_ineq) {
1331 sum = a.mk_add(sum, sign1);
1332 }
1333
1334 term = a.mk_mul(sign1, a0);
1335 sum = a.mk_add(sum, term);
1336 term = a.mk_mul(sign2, a1);
1337 sum = a.mk_add(sum, term);
1338
1339 #if 1
1340 {
1341 th_rewriter rw(m);
1342 rw(sum);
1343 }
1344
1345 IF_VERBOSE(2, verbose_stream() << "coeff,lit,sum " << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
1346 #endif
1347
1348 return true;
1349 }
1350
check_arith_proof(proof * p)1351 bool proof_checker::check_arith_proof(proof* p) {
1352 func_decl* d = p->get_decl();
1353 SASSERT(PR_TH_LEMMA == p->get_decl_kind());
1354 SASSERT(d->get_parameter(0).get_symbol() == "arith");
1355 unsigned num_params = d->get_num_parameters();
1356 arith_util autil(m);
1357
1358 SASSERT(num_params > 0);
1359 if (num_params == 1) {
1360 dump_proof(p);
1361 return true;
1362 }
1363 expr* fact = nullptr;
1364 proof_ref_vector proofs(m);
1365
1366 if (!match_fact(p, fact)) {
1367 UNREACHABLE();
1368 return false;
1369 }
1370
1371 if (d->get_parameter(1).get_symbol() != symbol("farkas")) {
1372 dump_proof(p);
1373 return true;
1374 }
1375 expr_ref sum(m);
1376 bool is_strict = false;
1377 unsigned offset = 0;
1378 vector<rational> coeffs;
1379 rational lc(1);
1380 for (unsigned i = 2; i < d->get_num_parameters(); ++i) {
1381 parameter const& p = d->get_parameter(i);
1382 if (!p.is_rational()) {
1383 UNREACHABLE();
1384 return false;
1385 }
1386 coeffs.push_back(p.get_rational());
1387 lc = lcm(lc, denominator(coeffs.back()));
1388 }
1389 if (!lc.is_one()) {
1390 for (unsigned i = 0; i < coeffs.size(); ++i) {
1391 coeffs[i] = lc*coeffs[i];
1392 }
1393 }
1394
1395 unsigned num_parents = m.get_num_parents(p);
1396 for (unsigned i = 0; i < num_parents; i++) {
1397 proof * a = m.get_parent(p, i);
1398 SASSERT(m.has_fact(a));
1399 if (!check_arith_literal(true, to_app(m.get_fact(a)), coeffs[offset++], sum, is_strict)) {
1400 return false;
1401 }
1402 }
1403 TRACE("proof_checker",
1404 for (unsigned i = 0; i < num_parents; i++)
1405 tout << coeffs[i] << " * " << mk_bounded_pp(m.get_fact(m.get_parent(p, i)), m) << "\n";
1406 tout << "fact:" << mk_bounded_pp(fact, m) << "\n";);
1407
1408 if (m.is_or(fact)) {
1409 app* disj = to_app(fact);
1410 unsigned num_args = disj->get_num_args();
1411 for (unsigned i = 0; i < num_args; ++i) {
1412 app* lit = to_app(disj->get_arg(i));
1413 if (!check_arith_literal(false, lit, coeffs[offset++], sum, is_strict)) {
1414 return false;
1415 }
1416 }
1417 }
1418 else if (!m.is_false(fact)) {
1419 if (!check_arith_literal(false, to_app(fact), coeffs[offset++], sum, is_strict)) {
1420 return false;
1421 }
1422 }
1423
1424 if (!sum.get()) {
1425 return false;
1426 }
1427
1428 sort* s = sum->get_sort();
1429
1430
1431 if (is_strict) {
1432 sum = autil.mk_lt(sum, autil.mk_numeral(rational(0), s));
1433 }
1434 else {
1435 sum = autil.mk_le(sum, autil.mk_numeral(rational(0), s));
1436 }
1437
1438 th_rewriter rw(m);
1439 rw(sum);
1440
1441 if (!m.is_false(sum)) {
1442 IF_VERBOSE(1, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
1443 m_dump_lemmas = true;
1444 dump_proof(p);
1445 return false;
1446 }
1447
1448 return true;
1449 }
1450