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

replace costly ite reduction by disjointnes check

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-25 21:15:03 -07:00
parent 392bc166a3
commit 4fd6ba442a
2 changed files with 20 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

82
src/ast/rewriter/bool_rewriter.cpp
View file

@ -690,84 +690,36 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
return BR_FAILED;
}
// check that all leaves are disjoint.
expr_ref bool_rewriter::simplify_eq_ite(expr* value, expr* ite) {
SASSERT(m().is_value(value));
SASSERT(m().is_ite(ite));
expr* c = nullptr, * t = nullptr, * e = nullptr;
expr_ref r(m());
auto& todo = m_todo1;
todo.reset();
auto& values = m_values;
auto& pinned = m_pinned;
auto& indices = m_indices;
expr* result = nullptr;
SASSERT(indices.empty());
todo.push_back(ite);
bool is_disjoint = true;
while (!todo.empty()) {
expr* arg = todo.back();
unsigned id = arg->get_id();
if (m().is_value(arg)) {
if (m().are_equal(arg, value)) {
todo.pop_back();
values.setx(id, m().mk_true(), nullptr);
indices.push_back(id);
continue;
}
if (m().are_distinct(arg, value)) {
todo.pop_back();
values.setx(id, m().mk_false(), nullptr);
indices.push_back(id);
continue;
}
goto bail;
}
todo.pop_back();
if (m_marked.is_marked(arg))
continue;
m_marked.mark(arg, true);
if (m().is_value(arg) && m().are_distinct(arg, value))
continue;
if (m().is_ite(arg, c, t, e)) {
unsigned sz = todo.size();
auto th = values.get(t->get_id(), nullptr);
auto el = values.get(e->get_id(), nullptr);
if (!th)
todo.push_back(t);
if (!el)
todo.push_back(e);
if (sz < todo.size())
continue;
if (m().is_false(th) && m().is_false(el))
r = m().mk_false();
else if (m().is_true(th) && m().is_true(el))
r = m().mk_true();
else if (m().is_true(th) && m().is_false(el))
r = c;
else if (m().is_false(th) && m().is_true(el))
r = m().mk_not(c);
else if (m().is_true(th))
r = m().mk_or(c, el);
else if (m().is_false(th))
r = m().mk_and(m().mk_not(c), el);
else if (m().is_false(el))
r = m().mk_and(c, th);
else if (m().is_true(el))
r = m().mk_or(m().mk_not(c), th);
else
r = m().mk_ite(c, th, el);
todo.pop_back();
values.setx(id, r, nullptr);
indices.push_back(id);
pinned.push_back(r);
if (!m_marked.is_marked(t))
todo.push_back(t);
if (!m_marked.is_marked(e))
todo.push_back(e);
continue;
}
IF_VERBOSE(10, verbose_stream() << "bail " << mk_bounded_pp(arg, m()) << "\n");
goto bail;
is_disjoint = false;
break;
}
bail:
if (todo.empty())
result = values[ite->get_id()];
for (auto idx : indices)
values[idx] = nullptr;
indices.reset();
return expr_ref(result, m());
m_marked.reset();
todo.reset();
return expr_ref(is_disjoint ? m().mk_false() : nullptr, m());
}

7
src/ast/rewriter/bool_rewriter.h
View file

@ -63,9 +63,8 @@ class bool_rewriter {
bool m_elim_ite;
bool m_elim_ite_value_tree;
ptr_vector<expr> m_todo1, m_todo2;
unsigned_vector m_counts1, m_counts2, m_indices;
ptr_vector<expr> m_values;
expr_ref_vector m_pinned;
unsigned_vector m_counts1, m_counts2;
expr_fast_mark1 m_marked;
br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);
@ -89,7 +88,7 @@ class bool_rewriter {
expr_ref simplify_eq_ite(expr* value, expr* ite);
public:
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0), m_pinned(m) {
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) {
updt_params(p);
}
ast_manager & m() const { return m_manager; }