mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks).
This commit is contained in:
parent
a3e915fbea
commit
824ba14977
|
@ -594,25 +594,27 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
|
|||
}
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m().is_value(t)) {
|
||||
if (val == t) {
|
||||
result = m().mk_or(cond, m().mk_eq(val, e));
|
||||
if (m_ite_extra_rules) {
|
||||
if (m().is_value(t)) {
|
||||
if (val == t) {
|
||||
result = m().mk_or(cond, m().mk_eq(val, e));
|
||||
}
|
||||
else {
|
||||
mk_not(cond, result);
|
||||
result = m().mk_and(result, m().mk_eq(val, e));
|
||||
}
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
else {
|
||||
mk_not(cond, result);
|
||||
result = m().mk_and(result, m().mk_eq(val, e));
|
||||
if (m().is_value(e)) {
|
||||
if (val == e) {
|
||||
mk_not(cond, result);
|
||||
result = m().mk_or(result, m().mk_eq(val, t));
|
||||
}
|
||||
else {
|
||||
result = m().mk_and(cond, m().mk_eq(val, t));
|
||||
}
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
if (m().is_value(e)) {
|
||||
if (val == e) {
|
||||
mk_not(cond, result);
|
||||
result = m().mk_or(result, m().mk_eq(val, t));
|
||||
}
|
||||
else {
|
||||
result = m().mk_and(cond, m().mk_eq(val, t));
|
||||
}
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
expr* cond2, *t2, *e2;
|
||||
if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) {
|
||||
|
|
|
@ -538,6 +538,8 @@ struct ctx_simplify_tactic::imp {
|
|||
}
|
||||
pop(scope_level() - old_lvl);
|
||||
|
||||
m_occs(g);
|
||||
|
||||
// go backwards
|
||||
sz = g.size();
|
||||
for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
|
||||
|
|
Loading…
Reference in a new issue