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 #3612

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 15:09:12 -07:00
parent 7ada20c65d
commit a1f68a619d
3 changed files with 16 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -83,6 +83,8 @@ protected:
void reduce(goal& g) {
if (m.proofs_enabled())
return;
TRACE("ctx_solver_simplify_tactic", g.display(tout););
expr_ref fml(m);
tactic_report report("ctx-solver-simplify", g);

16
src/tactic/core/propagate_values_tactic.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "tactic/core/propagate_values_tactic.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/expr_substitution.h"
#include "tactic/goal_shared_occs.h"
#include "tactic/tactic_params.hpp"
@ -52,18 +53,20 @@ class propagate_values_tactic : public tactic {
return is_shared(atom);
}
bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
bool is_shared_eq(expr * t, expr * & lhs, expr * & value, bool& inverted) {
expr* arg1, *arg2;
if (!m.is_eq(t, arg1, arg2))
return false;
if (m.is_value(arg1) && is_shared(arg2)) {
lhs = arg2;
value = arg1;
inverted = false;
return true;
}
if (m.is_value(arg2) && is_shared(arg1)) {
lhs = arg1;
value = arg2;
inverted = true;
return true;
}
return false;
@ -71,7 +74,7 @@ class propagate_values_tactic : public tactic {
void push_result(expr * new_curr, proof * new_pr) {
if (m_goal->proofs_enabled()) {
proof * pr = m_goal->pr(m_idx);
proof * pr = m_goal->pr(m_idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
@ -95,8 +98,10 @@ class propagate_values_tactic : public tactic {
m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
}
expr * lhs, * value;
if (is_shared_eq(new_curr, lhs, value)) {
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
bool inverted = false;
if (is_shared_eq(new_curr, lhs, value, inverted)) {
TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n" << mk_ismt2_pp(new_pr, m) << "\n";);
if (inverted && new_pr) new_pr = m.mk_symmetry(new_pr);
m_subst->insert(lhs, value, new_pr, new_d);
}
}
@ -105,6 +110,7 @@ class propagate_values_tactic : public tactic {
expr * curr = m_goal->form(m_idx);
expr_ref new_curr(m);
proof_ref new_pr(m);
std::cout << m_goal->pr(m_idx) << "\n";
if (!m_subst->empty()) {
m_r(curr, new_curr, new_pr);
@ -115,7 +121,7 @@ class propagate_values_tactic : public tactic {
new_pr = m.mk_reflexivity(curr);
}
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << new_curr << "\n" << new_pr << "\n";);
if (new_curr != curr) {
m_modified = true;
}

3
src/tactic/goal.cpp
View file

@ -115,6 +115,7 @@ void goal::copy_to(goal & target) const {
}
void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
SASSERT(!m().proofs_enabled() || pr);
if (m().is_true(f))
return;
if (m().is_false(f)) {
@ -252,6 +253,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
if (m_inconsistent) {
return;
}
SASSERT(!m().proofs_enabled() || pr);
if (pr) {
SASSERT(f == m().get_fact(pr));
slow_process(f, pr, d);
@ -301,6 +303,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
}
}
else {
SASSERT(!m().proofs_enabled());
expr_ref fr(f, m());
quick_process(true, fr, d);
if (!m_inconsistent) {