mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

remove asserts for proof generation to enable mode switch in spacer virtual solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-06 02:18:55 -08:00
parent 53ed1bb862
commit 16bab71df2
1 changed files with 0 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast.cpp
View file

@ -2842,21 +2842,18 @@ proof * ast_manager::mk_distributivity(expr * s, expr * r) {
}
proof * ast_manager::mk_rewrite(expr * s, expr * t) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
}
proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
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) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
ptr_buffer<expr> args;
@ -2866,42 +2863,36 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
}
proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
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) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
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) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
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) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
}
proof * ast_manager::mk_der(quantifier * q, expr * e) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
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) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
vector<parameter> params;
@ -2937,7 +2928,6 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
}
proof * ast_manager::mk_def_axiom(expr * ax) {
SASSERT(proofs_enabled());
if (proofs_disabled())
return m_undef_proof;
return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);