mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

fix #3286

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-14 11:42:26 -07:00
parent 9f6a0a0a48
commit c613ab0ba0
6 changed files with 18 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -2816,7 +2816,7 @@ proof * ast_manager::mk_goal(expr * f) {
} }
proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) { proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
if (!p1 || !p2) return nullptr; if (!p2 || !p1) return p1;
SASSERT(has_fact(p1)); SASSERT(has_fact(p1));
SASSERT(has_fact(p2)); SASSERT(has_fact(p2));
CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))), CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))),

5
src/tactic/arith/card2bv_tactic.cpp
View file

@ -68,11 +68,12 @@ public:
proof_ref new_pr1(m), new_pr2(m); proof_ref new_pr1(m), new_pr2(m);
for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) {
rw1(g->form(idx), new_f1, new_pr1); rw1(g->form(idx), new_f1, new_pr1);
TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); TRACE("card2bv", tout << "Rewriting " << new_f1 << "\n" << new_pr1 << std::endl;);
rw2(false, new_f1, new_f2, new_pr2); rw2(false, new_f1, new_f2, new_pr2);
TRACE("card2bv", tout << "Rewriting " << new_f2 << "\n" << new_pr2 << std::endl;);
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
new_pr1 = m.mk_transitivity(new_pr1, new_pr2);
new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1);
new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2);
} }
g->update(idx, new_f2, new_pr1, g->dep(idx)); g->update(idx, new_f2, new_pr1, g->dep(idx));
} }

14
src/tactic/arith/lia2card_tactic.cpp
View file

@ -195,15 +195,21 @@ public:
TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";); TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";);
} }
} }
for (unsigned i = 0; i < g->size(); i++) { for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {
checkpoint(); checkpoint();
expr_ref new_curr(m), tmp(m); expr_ref new_curr(m), tmp(m);
proof_ref new_pr(m); proof_ref pr1(m), pr2(m), new_pr(m);
rep(g->form(i), tmp); rep(g->form(i), tmp);
if (g->form(i) != tmp && m.proofs_enabled()) {
pr1 = m.mk_rewrite(g->form(i), tmp);
}
m_rw(tmp, new_curr, new_pr); m_rw(tmp, new_curr, new_pr);
if (m.proofs_enabled() && !new_pr) { if (m.proofs_enabled() && tmp != new_curr) {
new_pr = m.mk_rewrite(g->form(i), new_curr); pr2 = m.mk_rewrite(tmp, new_curr);
}
if (m.proofs_enabled()) {
new_pr = m.mk_transitivity(pr1, pr2);
new_pr = m.mk_modus_ponens(g->pr(i), new_pr); new_pr = m.mk_modus_ponens(g->pr(i), new_pr);
} }
// IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";); // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";);

4
src/tactic/core/simplify_tactic.cpp
View file

@ -44,7 +44,6 @@ struct simplify_tactic::imp {
void operator()(goal & g) { void operator()(goal & g) {
tactic_report report("simplifier", g); tactic_report report("simplifier", g);
TRACE("before_simplifier", g.display(tout););
m_num_steps = 0; m_num_steps = 0;
if (g.inconsistent()) if (g.inconsistent())
return; return;
@ -63,9 +62,8 @@ struct simplify_tactic::imp {
} }
g.update(idx, new_curr, new_pr, g.dep(idx)); g.update(idx, new_curr, new_pr, g.dep(idx));
} }
TRACE("after_simplifier_bug", g.display(tout);); TRACE("simplifier", g.display(tout););
g.elim_redundancies(); g.elim_redundancies();
TRACE("after_simplifier", g.display(tout););
TRACE("after_simplifier_detail", g.display_with_dependencies(tout);); TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
} }

2
src/tactic/goal.cpp
View file

@ -588,7 +588,7 @@ bool goal::is_well_formed() const {
expr * t = form(i); expr * t = form(i);
if (!::is_well_sorted(m(), t)) if (!::is_well_sorted(m(), t))
return false; return false;
#if 0 #if 1
SASSERT(m().get_fact(pr(i)) == form(i)); SASSERT(m().get_fact(pr(i)) == form(i));
if (m().get_fact(pr(i)) != form(i)) if (m().get_fact(pr(i)) != form(i))
return false; return false;

2
src/tactic/tactic.cpp
View file

@ -41,7 +41,6 @@ struct tactic_report::imp {
~imp() { ~imp() {
m_watch.stop(); m_watch.stop();
double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024); double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
SASSERT(m_goal.is_well_formed());
TRACE("tactic", m_goal.display(tout);); TRACE("tactic", m_goal.display(tout););
IF_VERBOSE(0, IF_VERBOSE(0,
verbose_stream() << "(" << m_id verbose_stream() << "(" << m_id
@ -51,6 +50,7 @@ struct tactic_report::imp {
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
<< " :after-memory " << std::fixed << std::setprecision(2) << end_memory << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
<< ")" << std::endl); << ")" << std::endl);
SASSERT(m_goal.is_well_formed());
} }
}; };