mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3843

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-08 11:08:45 -07:00
parent 40aa2f7cb2
commit 6e8d9001dc
4 changed files with 14 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/ast.cpp
View file

@ -2823,7 +2823,7 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
SASSERT(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2)));
CTRACE("mk_modus_ponens", to_app(get_fact(p2))->get_arg(0) != get_fact(p1),
tout << mk_pp(get_fact(p1), *this) << "\n" << mk_pp(get_fact(p2), *this) << "\n";);
SASSERT(to_app(get_fact(p2))->get_arg(0) == get_fact(p1));
SASSERT(!proofs_enabled() || to_app(get_fact(p2))->get_arg(0) == get_fact(p1));
CTRACE("mk_modus_ponens", !is_ground(p2) && !has_quantifiers(p2), tout << "Non-ground: " << mk_pp(p2, *this) << "\n";);
CTRACE("mk_modus_ponens", !is_ground(p1) && !has_quantifiers(p1), tout << "Non-ground: " << mk_pp(p1, *this) << "\n";);
if (is_reflexivity(p2))
@ -2887,6 +2887,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
return p2;
if (!p2)
return p1;
if (proofs_disabled())
return nullptr;
SASSERT(has_fact(p1));
SASSERT(has_fact(p2));
SASSERT(is_app(get_fact(p1)));

4
src/ast/rewriter/rewriter.cpp
View file

@ -43,11 +43,11 @@ void rewriter_core::del_cache_stack() {
}
bool rewriter_core::rewrites_from(expr* t, proof* p) {
return !p || (to_app(m().get_fact(p))->get_arg(0) == t);
return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(0) == t);
}
bool rewriter_core::rewrites_to(expr* t, proof* p) {
return !p || (to_app(m().get_fact(p))->get_arg(1) == t);
return !p || m().proofs_disabled() || (to_app(m().get_fact(p))->get_arg(1) == t);
}

14
src/ast/rewriter/rewriter_def.h
View file

@ -242,7 +242,6 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
// SASSERT(t->get_num_args() > 0);
SASSERT(!frame_stack().empty());
switch (fr.m_state) {
case PROCESS_CHILDREN: {
@ -311,13 +310,14 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
result_stack().push_back(m_r);
if (ProofGen) {
result_pr_stack().shrink(fr.m_spos);
if (!m_pr2)
if (!m_pr2) {
m_pr2 = m().mk_rewrite(new_t, m_r);
}
m_pr = m().mk_transitivity(m_pr, m_pr2);
m_pr2 = nullptr;
result_pr_stack().push_back(m_pr);
SASSERT(rewrites_to(m_r, m_pr));
SASSERT(rewrites_from(t, m_pr));
m_pr2 = nullptr;
}
if (st == BR_DONE) {
cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
@ -346,12 +346,14 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
result_pr_stack().pop_back();
pr1 = result_pr_stack().back();
result_pr_stack().pop_back();
SASSERT(rewrites_from(t, pr1));
SASSERT(rewrites_to(m_r, pr1));
SASSERT(rewrites_from(m_r, pr2));
SASSERT(rewrites_to(result_stack().back(), pr2));
m_pr = m().mk_transitivity(pr1, pr2);
result_pr_stack().push_back(m_pr);
}
m_r = result_stack().back();
SASSERT(rewrites_to(m_r, m_pr));
SASSERT(rewrites_from(t, m_pr));
m_r = result_stack().back();
result_stack().pop_back();
result_stack().pop_back();
result_stack().push_back(m_r);

2
src/muz/base/hnf.cpp
View file

@ -473,7 +473,7 @@ private:
p2 = m.mk_oeq_congruence(e2, fml, defs.size(), defs.c_ptr());
p3 = mk_transitivity(p1, p2);
defs.reset();
return proof_ref(p3, m);
return p3;
}
}