mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
fix proof mode related segfaults #1241
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
16bab71df2
commit
0f2b1ae7c8
2 changed files with 21 additions and 22 deletions
|
|
@ -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<expr> 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<parameter> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> args;
|
||||
vector<parameter> parameters;
|
||||
|
|
|
|||
|
|
@ -351,7 +351,6 @@ void rewriter_tpl<Config>::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<Config>::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());
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue