1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 asserted_formulas.cpp
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2008-06-11.
15
16 Revision History:
17
18 --*/
19 #include "util/warning.h"
20 #include "ast/ast_ll_pp.h"
21 #include "ast/ast_pp.h"
22 #include "ast/for_each_expr.h"
23 #include "ast/well_sorted.h"
24 #include "ast/rewriter/rewriter_def.h"
25 #include "ast/normal_forms/nnf.h"
26 #include "ast/pattern/pattern_inference.h"
27 #include "ast/macros/quasi_macros.h"
28 #include "ast/occurs.h"
29 #include "solver/assertions/asserted_formulas.h"
30
31
asserted_formulas(ast_manager & m,smt_params & sp,params_ref const & p)32 asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
33 m(m),
34 m_smt_params(sp),
35 m_params(p),
36 m_rewriter(m),
37 m_substitution(m),
38 m_scoped_substitution(m_substitution),
39 m_defined_names(m),
40 m_static_features(m),
41 m_qhead(0),
42 m_macro_manager(m),
43 m_bv_sharing(m),
44 m_inconsistent(false),
45 m_has_quantifiers(false),
46 m_reduce_asserted_formulas(*this),
47 m_distribute_forall(*this),
48 m_pattern_inference(*this),
49 m_refine_inj_axiom(*this),
50 m_max_bv_sharing_fn(*this),
51 m_elim_term_ite(*this),
52 m_pull_nested_quantifiers(*this),
53 m_elim_bvs_from_quantifiers(*this),
54 m_cheap_quant_fourier_motzkin(*this),
55 m_apply_bit2int(*this),
56 m_lift_ite(*this),
57 m_ng_lift_ite(*this),
58 m_find_macros(*this),
59 m_propagate_values(*this),
60 m_nnf_cnf(*this),
61 m_apply_quasi_macros(*this),
62 m_flatten_clauses(*this),
63 m_lazy_scopes(0) {
64
65 m_macro_finder = alloc(macro_finder, m, m_macro_manager);
66
67 m_elim_and = true;
68 set_eliminate_and(false);
69
70 }
71
setup()72 void asserted_formulas::setup() {
73 switch (m_smt_params.m_lift_ite) {
74 case LI_FULL:
75 m_smt_params.m_ng_lift_ite = LI_NONE;
76 break;
77 case LI_CONSERVATIVE:
78 if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
79 m_smt_params.m_ng_lift_ite = LI_NONE;
80 break;
81 default:
82 break;
83 }
84
85 if (m_smt_params.m_relevancy_lvl == 0)
86 m_smt_params.m_relevancy_lemma = false;
87 }
88
89
~asserted_formulas()90 asserted_formulas::~asserted_formulas() {
91 }
92
push_assertion(expr * e,proof * pr,vector<justified_expr> & result)93 void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_expr>& result) {
94 if (inconsistent()) {
95 return;
96 }
97 expr* e1 = nullptr;
98 if (m.is_false(e)) {
99 result.push_back(justified_expr(m, e, pr));
100 m_inconsistent = true;
101 }
102 else if (m.is_true(e)) {
103 // skip
104 }
105 else if (m.is_and(e)) {
106 for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
107 expr* arg = to_app(e)->get_arg(i);
108 proof_ref _pr(m.proofs_enabled() ? m.mk_and_elim(pr, i) : nullptr, m);
109 push_assertion(arg, _pr, result);
110 }
111 }
112 else if (m.is_not(e, e1) && m.is_or(e1)) {
113 for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
114 expr* arg = to_app(e1)->get_arg(i);
115 proof_ref _pr(m.proofs_enabled() ? m.mk_not_or_elim(pr, i) : nullptr, m);
116 expr_ref narg(mk_not(m, arg), m);
117 push_assertion(narg, _pr, result);
118 }
119 }
120 else {
121 result.push_back(justified_expr(m, e, pr));
122 }
123 }
124
updt_params(params_ref const & p)125 void asserted_formulas::updt_params(params_ref const& p) {
126 m_params.append(p);
127 }
128
set_eliminate_and(bool flag)129 void asserted_formulas::set_eliminate_and(bool flag) {
130 if (flag == m_elim_and) return;
131 m_elim_and = flag;
132 if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
133 m_params.set_bool("elim_and", flag);
134 m_params.set_bool("arith_ineq_lhs", true);
135 m_params.set_bool("sort_sums", true);
136 m_params.set_bool("rewrite_patterns", true);
137 m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
138 m_params.set_bool("gcd_rounding", true);
139 m_params.set_bool("expand_select_store", true);
140 //m_params.set_bool("expand_nested_stores", true);
141 m_params.set_bool("bv_sort_ac", true);
142 // seq theory solver keeps terms in normal form and has to interact with side-effect of rewriting
143 m_params.set_bool("coalesce_chars", m_smt_params.m_string_solver != symbol("seq"));
144 m_params.set_bool("som", true);
145 if (m_smt_params.m_arith_mode == arith_solver_id::AS_OLD_ARITH)
146 m_params.set_bool("flat", true);
147 m_rewriter.updt_params(m_params);
148 flush_cache();
149 }
150
151
assert_expr(expr * e,proof * _in_pr)152 void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
153 force_push();
154 proof_ref in_pr(_in_pr, m), pr(_in_pr, m);
155 expr_ref r(e, m);
156
157 if (inconsistent())
158 return;
159
160 if (m_smt_params.m_preprocess) {
161 TRACE("assert_expr_bug", tout << r << "\n";);
162 set_eliminate_and(false); // do not eliminate and before nnf.
163 m_rewriter(e, r, pr);
164 if (m.proofs_enabled()) {
165 if (e == r)
166 pr = in_pr;
167 else
168 pr = m.mk_modus_ponens(in_pr, pr);
169 }
170 TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
171 }
172
173 m_has_quantifiers |= ::has_quantifiers(e);
174
175 push_assertion(r, pr, m_formulas);
176 TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
177 }
178
assert_expr(expr * e)179 void asserted_formulas::assert_expr(expr * e) {
180 assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr);
181 }
182
get_assertions(ptr_vector<expr> & result) const183 void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
184 for (justified_expr const& je : m_formulas) result.push_back(je.get_fml());
185 }
186
push_scope()187 void asserted_formulas::push_scope() {
188 ++m_lazy_scopes;
189 }
190
push_scope_core()191 void asserted_formulas::push_scope_core() {
192 reduce();
193 commit();
194 SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
195 TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
196 m_scoped_substitution.push();
197 m_scopes.push_back(scope());
198 scope & s = m_scopes.back();
199 s.m_formulas_lim = m_formulas.size();
200 SASSERT(inconsistent() || s.m_formulas_lim == m_qhead || m.limit().is_canceled());
201 s.m_inconsistent_old = m_inconsistent;
202 m_defined_names.push();
203 m_elim_term_ite.push();
204 m_bv_sharing.push_scope();
205 m_macro_manager.push_scope();
206 commit();
207 TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
208 }
209
force_push()210 void asserted_formulas::force_push() {
211 for (; m_lazy_scopes > 0; --m_lazy_scopes)
212 push_scope_core();
213 }
214
pop_scope(unsigned num_scopes)215 void asserted_formulas::pop_scope(unsigned num_scopes) {
216 if (num_scopes <= m_lazy_scopes) {
217 m_lazy_scopes -= num_scopes;
218 return;
219 }
220 num_scopes -= m_lazy_scopes;
221 m_lazy_scopes = 0;
222
223 TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
224 m_bv_sharing.pop_scope(num_scopes);
225 m_macro_manager.pop_scope(num_scopes);
226 unsigned new_lvl = m_scopes.size() - num_scopes;
227 scope & s = m_scopes[new_lvl];
228 m_inconsistent = s.m_inconsistent_old;
229 m_defined_names.pop(num_scopes);
230 m_elim_term_ite.pop(num_scopes);
231 m_scoped_substitution.pop(num_scopes);
232 m_formulas.shrink(s.m_formulas_lim);
233 m_qhead = s.m_formulas_lim;
234 m_scopes.shrink(new_lvl);
235 flush_cache();
236 TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";);
237 }
238
reset()239 void asserted_formulas::reset() {
240 m_defined_names.reset();
241 m_qhead = 0;
242 m_formulas.reset();
243 m_macro_manager.reset();
244 m_bv_sharing.reset();
245 m_rewriter.reset();
246 m_inconsistent = false;
247 }
248
finalize()249 void asserted_formulas::finalize() {
250 reset();
251 m_substitution.cleanup();
252 }
253
check_well_sorted() const254 bool asserted_formulas::check_well_sorted() const {
255 for (justified_expr const& je : m_formulas) {
256 if (!is_well_sorted(m, je.get_fml())) return false;
257 }
258 return true;
259 }
260
reduce()261 void asserted_formulas::reduce() {
262 if (inconsistent())
263 return;
264 if (canceled())
265 return;
266 if (m_qhead == m_formulas.size())
267 return;
268 if (!m_has_quantifiers && !m_smt_params.m_preprocess)
269 return;
270 if (m_macro_manager.has_macros())
271 invoke(m_find_macros);
272
273 TRACE("before_reduce", display(tout););
274 CASSERT("well_sorted", check_well_sorted());
275
276 set_eliminate_and(false); // do not eliminate and before nnf.
277 if (!invoke(m_propagate_values)) return;
278 if (!invoke(m_find_macros)) return;
279 if (!invoke(m_nnf_cnf)) return;
280 set_eliminate_and(true);
281 if (!invoke(m_reduce_asserted_formulas)) return;
282 if (!invoke(m_pull_nested_quantifiers)) return;
283 if (!invoke(m_lift_ite)) return;
284 m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE);
285 m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE);
286 if (!invoke(m_ng_lift_ite)) return;
287 if (!invoke(m_elim_term_ite)) return;
288 if (!invoke(m_refine_inj_axiom)) return;
289 if (!invoke(m_distribute_forall)) return;
290 if (!invoke(m_find_macros)) return;
291 if (!invoke(m_apply_quasi_macros)) return;
292 if (!invoke(m_apply_bit2int)) return;
293 if (!invoke(m_cheap_quant_fourier_motzkin)) return;
294 if (!invoke(m_pattern_inference)) return;
295 if (!invoke(m_max_bv_sharing_fn)) return;
296 if (!invoke(m_elim_bvs_from_quantifiers)) return;
297 if (!invoke(m_reduce_asserted_formulas)) return;
298 if (!invoke(m_flatten_clauses)) return;
299 // if (!invoke(m_propagate_values)) return;
300
301 IF_VERBOSE(10, verbose_stream() << "(smt.simplifier-done)\n";);
302 TRACE("after_reduce", display(tout););
303 TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
304 TRACE("macros", m_macro_manager.display(tout););
305 flush_cache();
306 CASSERT("well_sorted",check_well_sorted());
307
308 }
309
310
get_formulas_last_level() const311 unsigned asserted_formulas::get_formulas_last_level() const {
312 if (m_scopes.empty()) {
313 return 0;
314 }
315 else {
316 return m_scopes.back().m_formulas_lim;
317 }
318 }
319
invoke(simplify_fmls & s)320 bool asserted_formulas::invoke(simplify_fmls& s) {
321 if (!s.should_apply()) return true;
322 IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
323 s();
324 IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
325 TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
326 CASSERT("well_sorted",check_well_sorted());
327 if (inconsistent() || canceled()) {
328 TRACE("after_reduce", display(tout););
329 TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
330 return false;
331 }
332 else {
333 return true;
334 }
335 }
336
display(std::ostream & out) const337 void asserted_formulas::display(std::ostream & out) const {
338 out << "asserted formulas:\n";
339 for (unsigned i = 0; i < m_formulas.size(); i++) {
340 if (i == m_qhead)
341 out << "[HEAD] ==>\n";
342 out << mk_pp(m_formulas[i].get_fml(), m) << "\n";
343 }
344 out << "inconsistent: " << inconsistent() << "\n";
345 }
346
display_ll(std::ostream & out,ast_mark & pp_visited) const347 void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
348 if (!m_formulas.empty()) {
349 for (justified_expr const& f : m_formulas)
350 ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
351 out << "asserted formulas:\n";
352 for (justified_expr const& f : m_formulas)
353 out << "#" << f.get_fml()->get_id() << " ";
354 out << "\n";
355 }
356 }
357
collect_statistics(statistics & st) const358 void asserted_formulas::collect_statistics(statistics & st) const {
359 }
360
361
swap_asserted_formulas(vector<justified_expr> & formulas)362 void asserted_formulas::swap_asserted_formulas(vector<justified_expr>& formulas) {
363 SASSERT(!inconsistent() || !formulas.empty());
364 m_formulas.shrink(m_qhead);
365 m_formulas.append(formulas);
366 }
367
368
find_macros_core()369 void asserted_formulas::find_macros_core() {
370 vector<justified_expr> new_fmls;
371 unsigned sz = m_formulas.size();
372 (*m_macro_finder)(sz - m_qhead, m_formulas.data() + m_qhead, new_fmls);
373 swap_asserted_formulas(new_fmls);
374 reduce_and_solve();
375 }
376
377 /**
378 \brief rewrite (a or (b & c)) to (a or b), (a or c) if the reference count of (b & c) is 1.
379 This avoids the literal for (b & c)
380 */
flatten_clauses()381 void asserted_formulas::flatten_clauses() {
382 if (m.proofs_enabled()) return;
383 bool change = true;
384 vector<justified_expr> new_fmls;
385 auto mk_not = [this](expr* e) { return m.is_not(e, e) ? e : m.mk_not(e); };
386 auto is_literal = [this](expr *e) { m.is_not(e, e); return !is_app(e) || to_app(e)->get_num_args() == 0; };
387 expr *a = nullptr, *b = nullptr, *c = nullptr;
388 while (change) {
389 change = false;
390 new_fmls.reset();
391 unsigned sz = m_formulas.size();
392 for (unsigned i = m_qhead; i < sz; ++i) {
393 auto const& j = m_formulas.get(i);
394 expr* f = j.get_fml();
395 bool decomposed = false;
396 if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
397 decomposed = true;
398 }
399 else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && (b->get_ref_count() == 1 || is_literal(a))) {
400 decomposed = true;
401 }
402 if (decomposed) {
403 for (expr* arg : *to_app(b)) {
404 justified_expr j1(m, m.mk_or(a, mk_not(arg)), nullptr);
405 new_fmls.push_back(j1);
406 }
407 change = true;
408 continue;
409 }
410 if (m.is_ite(f, a, b, c)) {
411 new_fmls.push_back(justified_expr(m, m.mk_or(mk_not(a), b), nullptr));
412 new_fmls.push_back(justified_expr(m, m.mk_or(a, c), nullptr));
413 change = true;
414 continue;
415 }
416 new_fmls.push_back(j);
417 }
418 swap_asserted_formulas(new_fmls);
419 }
420 }
421
422
apply_quasi_macros()423 void asserted_formulas::apply_quasi_macros() {
424 TRACE("before_quasi_macros", display(tout););
425 vector<justified_expr> new_fmls;
426 quasi_macros proc(m, m_macro_manager);
427 while (m_qhead == 0 &&
428 proc(m_formulas.size() - m_qhead,
429 m_formulas.data() + m_qhead,
430 new_fmls)) {
431 swap_asserted_formulas(new_fmls);
432 new_fmls.reset();
433 }
434 TRACE("after_quasi_macros", display(tout););
435 reduce_and_solve();
436 }
437
nnf_cnf()438 void asserted_formulas::nnf_cnf() {
439 nnf apply_nnf(m, m_defined_names);
440 vector<justified_expr> new_fmls;
441 expr_ref_vector push_todo(m);
442 proof_ref_vector push_todo_prs(m);
443
444 unsigned i = m_qhead;
445 unsigned sz = m_formulas.size();
446 TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
447 for (; i < sz; i++) {
448 expr * n = m_formulas[i].get_fml();
449 TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
450 proof_ref pr(m_formulas[i].get_proof(), m);
451 expr_ref r1(m);
452 proof_ref pr1(m);
453 push_todo.reset();
454 push_todo_prs.reset();
455 CASSERT("well_sorted", is_well_sorted(m, n));
456 apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
457 CASSERT("well_sorted",is_well_sorted(m, r1));
458 pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr;
459 push_todo.push_back(r1);
460 push_todo_prs.push_back(pr);
461
462 if (canceled()) {
463 return;
464 }
465 unsigned sz2 = push_todo.size();
466 for (unsigned k = 0; k < sz2; k++) {
467 expr * n = push_todo.get(k);
468 pr = nullptr;
469 m_rewriter(n, r1, pr1);
470 CASSERT("well_sorted",is_well_sorted(m, r1));
471 if (canceled()) {
472 return;
473 }
474 if (m.proofs_enabled())
475 pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
476 push_assertion(r1, pr, new_fmls);
477 }
478 }
479 swap_asserted_formulas(new_fmls);
480 }
481
operator ()()482 void asserted_formulas::simplify_fmls::operator()() {
483 vector<justified_expr> new_fmls;
484 unsigned sz = af.m_formulas.size();
485 for (unsigned i = af.m_qhead; i < sz; i++) {
486 auto& j = af.m_formulas[i];
487 expr_ref result(m);
488 proof_ref result_pr(m);
489 simplify(j, result, result_pr);
490 if (m.proofs_enabled()) {
491 if (!result_pr) result_pr = m.mk_rewrite(j.get_fml(), result);
492 result_pr = m.mk_modus_ponens(j.get_proof(), result_pr);
493 }
494 if (j.get_fml() == result) {
495 new_fmls.push_back(j);
496 }
497 else {
498 af.push_assertion(result, result_pr, new_fmls);
499 }
500 if (af.canceled()) return;
501 }
502 af.swap_asserted_formulas(new_fmls);
503 TRACE("asserted_formulas", af.display(tout););
504 post_op();
505 }
506
507
reduce_and_solve()508 void asserted_formulas::reduce_and_solve() {
509 IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
510 flush_cache(); // collect garbage
511 m_reduce_asserted_formulas();
512 }
513
514
commit()515 void asserted_formulas::commit() {
516 commit(m_formulas.size());
517 }
518
commit(unsigned new_qhead)519 void asserted_formulas::commit(unsigned new_qhead) {
520 m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead);
521 m_expr2depth.reset();
522 for (unsigned i = m_qhead; i < new_qhead; ++i) {
523 justified_expr const& j = m_formulas[i];
524 update_substitution(j.get_fml(), j.get_proof());
525 }
526 m_qhead = new_qhead;
527 }
528
propagate_values()529 void asserted_formulas::propagate_values() {
530 if (m.proofs_enabled())
531 return;
532 flush_cache();
533
534 unsigned num_prop = 0;
535 unsigned sz = m_formulas.size();
536 unsigned delta_prop = sz;
537 while (!inconsistent() && sz/20 < delta_prop) {
538 m_expr2depth.reset();
539 m_scoped_substitution.push();
540 unsigned prop = num_prop;
541 TRACE("propagate_values", display(tout << "before:\n"););
542 unsigned i = m_qhead;
543 for (; i < sz; i++) {
544 prop += propagate_values(i);
545 }
546 flush_cache();
547 m_scoped_substitution.pop(1);
548 m_expr2depth.reset();
549 m_scoped_substitution.push();
550 TRACE("propagate_values", tout << "middle:\n"; display(tout););
551 i = sz;
552 while (i > m_qhead) {
553 --i;
554 prop += propagate_values(i);
555 }
556 m_scoped_substitution.pop(1);
557 flush_cache();
558 TRACE("propagate_values", tout << "after:\n"; display(tout););
559 delta_prop = prop - num_prop;
560 num_prop = prop;
561 if (sz <= m_formulas.size())
562 break;
563 sz = m_formulas.size();
564 }
565 TRACE("asserted_formulas", tout << num_prop << "\n";);
566 if (num_prop > 0)
567 m_reduce_asserted_formulas();
568 }
569
propagate_values(unsigned i)570 unsigned asserted_formulas::propagate_values(unsigned i) {
571 expr_ref n(m_formulas[i].get_fml(), m);
572 expr_ref new_n(m);
573 proof_ref new_pr(m);
574 m_rewriter(n, new_n, new_pr);
575 if (m.proofs_enabled()) {
576 proof * pr = m_formulas[i].get_proof();
577 new_pr = m.mk_modus_ponens(pr, new_pr);
578 }
579 justified_expr j(m, new_n, new_pr);
580 m_formulas[i] = j;
581 if (m.is_false(j.get_fml())) {
582 m_inconsistent = true;
583 }
584 update_substitution(new_n, new_pr);
585 return (n != new_n) ? 1 : 0;
586 }
587
update_substitution(expr * n,proof * pr)588 bool asserted_formulas::update_substitution(expr* n, proof* pr) {
589 expr* lhs, *rhs, *n1;
590 proof_ref pr1(m);
591 if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
592 compute_depth(lhs);
593 compute_depth(rhs);
594 if (is_gt(lhs, rhs)) {
595 TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
596 m_scoped_substitution.insert(lhs, rhs, pr);
597 return true;
598 }
599 if (is_gt(rhs, lhs)) {
600 TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
601 pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr;
602 m_scoped_substitution.insert(rhs, lhs, pr1);
603 return true;
604 }
605 TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
606 }
607 if (m.is_not(n, n1)) {
608 pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr;
609 m_scoped_substitution.insert(n1, m.mk_false(), pr1);
610 }
611 else {
612 pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr;
613 m_scoped_substitution.insert(n, m.mk_true(), pr1);
614 }
615 return false;
616 }
617
618
619 /**
620 \brief implement a Knuth-Bendix ordering on expressions.
621 */
622
is_gt(expr * lhs,expr * rhs)623 bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
624 if (lhs == rhs) {
625 return false;
626 }
627 // values are always less in ordering than non-values.
628 bool v1 = m.is_value(lhs);
629 bool v2 = m.is_value(rhs);
630 if (!v1 && v2) {
631 return true;
632 }
633 if (v1 && !v2) {
634 return false;
635 }
636 SASSERT(is_ground(lhs) && is_ground(rhs));
637 if (depth(lhs) > depth(rhs)) {
638 return true;
639 }
640 if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) {
641 app* l = to_app(lhs);
642 app* r = to_app(rhs);
643 if (l->get_decl()->get_id() != r->get_decl()->get_id()) {
644 return l->get_decl()->get_id() > r->get_decl()->get_id();
645 }
646 if (l->get_num_args() != r->get_num_args()) {
647 return l->get_num_args() > r->get_num_args();
648 }
649 for (unsigned i = 0; i < l->get_num_args(); ++i) {
650 if (l->get_arg(i) != r->get_arg(i)) {
651 return is_gt(l->get_arg(i), r->get_arg(i));
652 }
653 }
654 UNREACHABLE();
655 }
656
657 return false;
658 }
659
compute_depth(expr * e)660 void asserted_formulas::compute_depth(expr* e) {
661 ptr_vector<expr> todo;
662 todo.push_back(e);
663 while (!todo.empty()) {
664 e = todo.back();
665 unsigned d = 0;
666 if (m_expr2depth.contains(e)) {
667 todo.pop_back();
668 continue;
669 }
670 if (is_app(e)) {
671 app* a = to_app(e);
672 bool visited = true;
673 for (expr* arg : *a) {
674 unsigned d1 = 0;
675 if (m_expr2depth.find(arg, d1)) {
676 d = std::max(d, d1);
677 }
678 else {
679 visited = false;
680 todo.push_back(arg);
681 }
682 }
683 if (!visited) {
684 continue;
685 }
686 }
687 todo.pop_back();
688 m_expr2depth.insert(e, d + 1);
689 }
690 }
691
get_inconsistency_proof() const692 proof * asserted_formulas::get_inconsistency_proof() const {
693 if (!inconsistent())
694 return nullptr;
695 if (!m.proofs_enabled())
696 return nullptr;
697 if (!m.inc())
698 return nullptr;
699 for (justified_expr const& j : m_formulas) {
700 if (m.is_false(j.get_fml()))
701 return j.get_proof();
702 }
703 return nullptr;
704 }
705
simplify(justified_expr const & j,expr_ref & n,proof_ref & p)706 void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
707 expr* f = j.get_fml();
708 if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) {
709 TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);
710 }
711 else {
712 n = j.get_fml();
713 }
714 }
715
716
get_total_size() const717 unsigned asserted_formulas::get_total_size() const {
718 expr_mark visited;
719 unsigned r = 0;
720 for (justified_expr const& j : m_formulas)
721 r += get_num_exprs(j.get_fml(), visited);
722 return r;
723 }
724
725
726 #ifdef Z3DEBUG
pp(asserted_formulas & f)727 void pp(asserted_formulas & f) {
728 f.display(std::cout);
729 }
730 #endif
731