mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

fix #4895

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-14 15:05:51 -08:00
parent 7fe8298479
commit 0ef8ebe89f
2 changed files with 19 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -231,7 +231,8 @@ struct purify_arith_proc {
void operator()(app* a) { void operator()(app* a) {
for (expr* arg : *a) { for (expr* arg : *a) {
if (!is_ground(arg)) { if (!is_ground(arg)) {
o.m_cannot_purify.insert(a->get_decl()); auto* f = a->get_decl();
o.m_cannot_purify.insert(f);
break; break;
} }
} }
@ -694,9 +695,13 @@ struct purify_arith_proc {
process_div(f, num, args, result, result_pr); process_div(f, num, args, result, result_pr);
return BR_DONE; return BR_DONE;
case OP_IDIV: case OP_IDIV:
if (!m_cannot_purify.empty())
return BR_FAILED;
process_idiv(f, num, args, result, result_pr); process_idiv(f, num, args, result, result_pr);
return BR_DONE; return BR_DONE;
case OP_MOD: case OP_MOD:
if (!m_cannot_purify.empty())
return BR_FAILED;
process_mod(f, num, args, result, result_pr); process_mod(f, num, args, result, result_pr);
return BR_DONE; return BR_DONE;
case OP_TO_INT: case OP_TO_INT:

20
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -209,23 +209,22 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
r = simplify_arg(e); r = simplify_arg(e);
} }
else { else {
for (expr * child : tree(ite)) { for (expr * child : tree(ite))
if (is_subexpr(child, t) && !is_subexpr(child, e)) { if (is_subexpr(child, t) && !is_subexpr(child, e))
simplify_rec(child); simplify_rec(child);
}
}
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t); expr_ref new_t = simplify_arg(t);
reset_cache();
if (!assert_expr(new_c, true)) { if (!assert_expr(new_c, true)) {
return new_t; return new_t;
} }
for (expr * child : tree(ite)) { for (expr * child : tree(ite))
if (is_subexpr(child, e) && !is_subexpr(child, t)) { if (is_subexpr(child, e) && !is_subexpr(child, t))
simplify_rec(child); simplify_rec(child);
}
}
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e); expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) { if (c == new_c && t == new_t && e == new_e) {
r = ite; r = ite;
} }
@ -278,6 +277,7 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
} }
else { else {
for (expr * child : tree(e)) { for (expr * child : tree(e)) {
if (child != e)
simplify_rec(child); simplify_rec(child);
} }
if (is_app(e)) { if (is_app(e)) {
@ -382,9 +382,11 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
SASSERT(scope_level() == 0); SASSERT(scope_level() == 0);
bool change = true; bool change = true;
unsigned n = 0;
m_depth = 0; m_depth = 0;
while (change) { while (change && n < 10) {
change = false; change = false;
++n;
// go forwards // go forwards
m_forward = true; m_forward = true;