From 0f2b1ae7c81f1c381332a5aafddd29c73856f0c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Nov 2017 02:35:10 -0800 Subject: [PATCH] fix proof mode related segfaults #1241 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 40 ++++++++++++++++----------------- src/ast/rewriter/rewriter_def.h | 3 +-- 2 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 8c74cbe83..7eae396ff 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2626,7 +2626,7 @@ bool ast_manager::is_fully_interp(sort * s) const { proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(fid, k, num_args, args); } @@ -2843,19 +2843,19 @@ proof * ast_manager::mk_distributivity(expr * s, expr * r) { proof * ast_manager::mk_rewrite(expr * s, expr * t) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t)); } proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t)); } proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_eq(s, t)); @@ -2864,37 +2864,37 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q)); } proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q)); } proof * ast_manager::mk_push_quant(quantifier * q, expr * e) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e)); } proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e)); } proof * ast_manager::mk_der(quantifier * q, expr * e) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e)); } proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; vector params; for (unsigned i = 0; i < num_bind; ++i) { params.push_back(parameter(binding[i])); @@ -2929,7 +2929,7 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const { proof * ast_manager::mk_def_axiom(expr * ax) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax); } @@ -3067,7 +3067,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) { proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(n, def)); @@ -3100,7 +3100,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; check_nnf_proof_parents(num_proofs, proofs); ptr_buffer args; args.append(num_proofs, (expr**) proofs); @@ -3110,7 +3110,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; check_nnf_proof_parents(num_proofs, proofs); ptr_buffer args; args.append(num_proofs, (expr**) proofs); @@ -3120,7 +3120,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(s, t)); @@ -3129,7 +3129,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof proof * ast_manager::mk_skolemization(expr * q, expr * e) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(is_bool(q)); SASSERT(is_bool(e)); return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e)); @@ -3137,7 +3137,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) { proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(s, t)); @@ -3146,7 +3146,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof proof * ast_manager::mk_and_elim(proof * p, unsigned i) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(has_fact(p)); SASSERT(is_and(get_fact(p))); CTRACE("mk_and_elim", i >= to_app(get_fact(p))->get_num_args(), tout << "i: " << i << "\n" << mk_pp(get_fact(p), *this) << "\n";); @@ -3157,7 +3157,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) { proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(has_fact(p)); SASSERT(is_not(get_fact(p))); SASSERT(is_or(to_app(get_fact(p))->get_arg(0))); @@ -3180,7 +3180,7 @@ proof * ast_manager::mk_th_lemma( ) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; vector parameters; diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index f5f72674d..2abd6d467 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -351,7 +351,6 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (is_ground(def)) { m_r = def; if (ProofGen) { - SASSERT(def_pr); m_pr = m().mk_transitivity(m_pr, def_pr); } } @@ -510,7 +509,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { new_no_pats = q->get_no_patterns(); } if (ProofGen) { - quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body); + quantifier_ref new_q(m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body), m()); m_pr = q == new_q ? 0 : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos)); m_r = new_q; proof_ref pr2(m());