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

perf improvements to solve-eqs and euf-completion

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-16 22:15:02 -08:00
parent 2c7799939e
commit 6662afdd26
4 changed files with 129 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

70
src/ast/simplifiers/euf_completion.cpp
View file

@ -58,31 +58,43 @@ namespace euf {
}
void completion::reduce() {
unsigned rounds = 0;
do {
++m_epoch;
++rounds;
m_has_new_eq = false;
add_egraph();
map_canonical();
read_egraph();
IF_VERBOSE(11, verbose_stream() << "(euf.completion :rounds " << rounds << ")\n");
}
while (m_has_new_eq);
while (m_has_new_eq && rounds <= 3);
}
void completion::add_egraph() {
m_nodes.reset();
m_nodes_to_canonize.reset();
unsigned sz = m_fmls.size();
auto add_children = [&](enode* n) {
for (auto* ch : enode_args(n))
m_nodes_to_canonize.push_back(ch);
};
for (unsigned i = m_qhead; i < sz; ++i) {
auto [f,d] = m_fmls[i]();
auto* n = mk_enode(f);
if (m.is_eq(f)) {
m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
m_nodes.push_back(n->get_arg(0));
m_nodes.push_back(n->get_arg(1));
add_children(n->get_arg(0));
add_children(n->get_arg(1));
}
if (m.is_not(f))
if (m.is_not(f)) {
m_egraph.merge(n->get_arg(0), m_ff, d);
else
add_children(n->get_arg(0));
}
else {
m_egraph.merge(n, m_tt, d);
add_children(n);
}
}
m_egraph.propagate();
}
@ -106,15 +118,7 @@ namespace euf {
m_fmls.update(i, dependent_expr(m, g, dep));
m_stats.m_num_rewrites++;
IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(f, m, 3) << " -> " << mk_bounded_pp(g, m, 3) << "\n");
expr* x, * y;
if (m.is_eq(g, x, y) && new_eq(x, y))
m_has_new_eq = true;
if (m.is_and(g) && !m_has_new_eq)
for (expr* arg : *to_app(g))
if (m.is_eq(arg, x, y))
m_has_new_eq |= new_eq(x, y);
else if (!m.is_true(arg))
m_has_new_eq = true;
update_has_new_eq(g);
}
CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n");
}
@ -122,12 +126,34 @@ namespace euf {
advance_qhead(m_fmls.size());
}
bool completion::new_eq(expr* a, expr* b) {
bool completion::is_new_eq(expr* a, expr* b) {
enode* na = m_egraph.find(a);
enode* nb = m_egraph.find(b);
if (!na)
IF_VERBOSE(11, verbose_stream() << "not internalied " << mk_bounded_pp(a, m) << "\n");
if (!nb)
IF_VERBOSE(11, verbose_stream() << "not internalied " << mk_bounded_pp(b, m) << "\n");
if (na && nb && na->get_root() != nb->get_root())
IF_VERBOSE(11, verbose_stream() << m_egraph.bpp(na) << " " << m_egraph.bpp(nb) << "\n");
return !na || !nb || na->get_root() != nb->get_root();
}
void completion::update_has_new_eq(expr* g) {
expr* x, * y;
if (m_has_new_eq)
return;
else if (m.is_eq(g, x, y))
m_has_new_eq |= is_new_eq(x, y);
else if (m.is_and(g)) {
for (expr* arg : *to_app(g))
update_has_new_eq(arg);
}
else if (m.is_not(g, g))
m_has_new_eq |= is_new_eq(g, m.mk_false());
else
m_has_new_eq |= is_new_eq(g, m.mk_true());
}
enode* completion::mk_enode(expr* e) {
m_todo.push_back(e);
enode* n;
@ -138,7 +164,7 @@ namespace euf {
continue;
}
if (!is_app(e)) {
m_nodes.push_back(m_egraph.mk(e, 0, 0, nullptr));
m_nodes_to_canonize.push_back(m_egraph.mk(e, 0, 0, nullptr));
m_todo.pop_back();
continue;
}
@ -152,7 +178,7 @@ namespace euf {
m_todo.push_back(arg);
}
if (sz == m_todo.size()) {
m_nodes.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data()));
m_nodes_to_canonize.push_back(m_egraph.mk(e, 0, m_args.size(), m_args.data()));
m_todo.pop_back();
}
}
@ -314,10 +340,10 @@ namespace euf {
void completion::map_canonical() {
m_todo.reset();
enode_vector roots;
if (m_nodes.empty())
if (m_nodes_to_canonize.empty())
return;
for (unsigned i = 0; i < m_nodes.size(); ++i) {
enode* n = m_nodes[i]->get_root();
for (unsigned i = 0; i < m_nodes_to_canonize.size(); ++i) {
enode* n = m_nodes_to_canonize[i]->get_root();
if (n->is_marked1())
continue;
n->mark1();
@ -334,7 +360,7 @@ namespace euf {
for (enode* arg : enode_args(n)) {
arg = arg->get_root();
if (!arg->is_marked1())
m_nodes.push_back(arg);
m_nodes_to_canonize.push_back(arg);
}
}
for (enode* r : roots)

6
src/ast/simplifiers/euf_completion.h
View file

@ -33,7 +33,7 @@ namespace euf {
egraph m_egraph;
enode* m_tt, *m_ff;
ptr_vector<expr> m_todo;
enode_vector m_args, m_reps, m_nodes;
enode_vector m_args, m_reps, m_nodes_to_canonize;
expr_ref_vector m_canonical, m_eargs;
expr_dependency_ref_vector m_deps;
unsigned m_epoch = 0;
@ -43,11 +43,11 @@ namespace euf {
bool m_has_new_eq = false;
enode* mk_enode(expr* e);
bool new_eq(expr* a, expr* b);
bool is_new_eq(expr* a, expr* b);
void update_has_new_eq(expr* g);
expr_ref mk_and(expr* a, expr* b);
void add_egraph();
void map_canonical();
void saturate();
void read_egraph();
expr_ref canonize(expr* f, expr_dependency_ref& dep);
expr_ref canonize_fml(expr* f, expr_dependency_ref& dep);

54
src/ast/simplifiers/solve_context_eqs.cpp
View file

@ -147,7 +147,8 @@ namespace euf {
void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) {
expr_mark visited;
for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i)
unsigned sz = m_fmls.size();
for (unsigned i = m_solve_eqs.m_qhead; i < sz; ++i)
collect_nested_equalities(m_fmls[i], visited, eqs);
if (eqs.empty())
@ -156,15 +157,37 @@ namespace euf {
std::stable_sort(eqs.begin(), eqs.end(), [&](dependent_eq const& e1, dependent_eq const& e2) {
return e1.var->get_id() < e2.var->get_id(); });
// quickly weed out variables that occur in more than two assertions.
unsigned_vector refcount;
// record the first and last occurrence of variables
// if the first and last occurrence coincide, the variable occurs in only one formula.
// otherwise it occurs in multiple formulas and should not be considered for solving.
unsigned_vector occurs1(m.get_num_asts() + 1, sz);
unsigned_vector occurs2(m.get_num_asts() + 1, sz);
struct visitor {
unsigned_vector& occurrence;
unsigned i = 0;
unsigned sz = 0;
visitor(unsigned_vector& occurrence) : occurrence(occurrence), i(0), sz(0) {}
void operator()(expr* t) {
occurrence.setx(t->get_id(), i, sz);
}
};
{
expr_mark visited;
for (unsigned i = m_solve_eqs.m_qhead; i < m_fmls.size(); ++i) {
visited.reset();
expr* f = m_fmls[i].fml();
for (expr* t : subterms::all(expr_ref(f, m), &m_todo, &visited))
refcount.setx(t->get_id(), refcount.get(t->get_id(), 0) + 1, 0);
visitor visitor1(occurs1);
visitor visitor2(occurs2);
visitor1.sz = sz;
visitor2.sz = sz;
expr_fast_mark1 fast_visited;
for (unsigned i = 0; i < sz; ++i) {
visitor1.i = i;
quick_for_each_expr(visitor1, fast_visited, m_fmls[i].fml());
}
fast_visited.reset();
for (unsigned i = sz; i-- > 0; ) {
visitor2.i = i;
quick_for_each_expr(visitor2, fast_visited, m_fmls[i].fml());
}
}
@ -172,13 +195,17 @@ namespace euf {
expr* last_var = nullptr;
bool was_unsafe = false;
for (auto const& eq : eqs) {
if (refcount.get(eq.var->get_id(), 0) > 1)
if (!eq.var)
continue;
unsigned occ1 = occurs1.get(eq.var->get_id(), sz);
unsigned occ2 = occurs2.get(eq.var->get_id(), sz);
if (occ1 >= sz)
continue;
if (occ1 != occ2)
continue;
SASSERT(!m.is_bool(eq.var));
if (eq.var != last_var) {
m_contains_v.reset();
@ -195,8 +222,7 @@ namespace euf {
}
// then mark occurrences
for (unsigned i = 0; i < m_fmls.size(); ++i)
m_todo.push_back(m_fmls[i].fml());
m_todo.push_back(m_fmls[occ1].fml());
mark_occurs(m_todo, eq.var, m_contains_v);
SASSERT(m_todo.empty());
}

50
src/ast/simplifiers/solve_eqs.cpp
View file

@ -75,13 +75,6 @@ namespace euf {
return m_id2level[id] != UINT_MAX;
};
auto is_safe = [&](unsigned lvl, expr* t) {
for (auto* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited))
if (is_var(e) && m_id2level[var2id(e)] < lvl)
return false;
return true;
};
unsigned init_level = UINT_MAX;
unsigned_vector todo;
@ -94,26 +87,59 @@ namespace euf {
init_level -= m_id2var.size() + 1;
unsigned curr_level = init_level;
todo.push_back(id);
while (!todo.empty()) {
unsigned j = todo.back();
todo.pop_back();
if (is_explored(j))
continue;
m_id2level[j] = curr_level++;
for (auto const& eq : m_next[j]) {
auto const& [orig, v, t, d] = eq;
SASSERT(j == var2id(v));
if (!is_safe(curr_level, t))
bool is_safe = true;
unsigned todo_sz = todo.size();
// determine if substitution is safe.
// all time-stamps must be at or above current level
// unexplored variables that are part of substitution are appended to work list.
SASSERT(m_todo.empty());
m_todo.push_back(t);
expr_fast_mark1 visited;
while (!m_todo.empty()) {
expr* e = m_todo.back();
m_todo.pop_back();
if (visited.is_marked(e))
continue;
visited.mark(e, true);
if (is_app(e)) {
for (expr* arg : *to_app(e))
m_todo.push_back(arg);
}
else if (is_quantifier(e))
m_todo.push_back(to_quantifier(e)->get_expr());
if (!is_var(e))
continue;
if (m_id2level[var2id(e)] < curr_level) {
is_safe = false;
break;
}
if (!is_explored(var2id(e)))
todo.push_back(var2id(e));
}
m_todo.reset();
if (!is_safe) {
todo.shrink(todo_sz);
continue;
}
SASSERT(!occurs(v, t));
m_next[j][0] = eq;
m_subst_ids.push_back(j);
for (expr* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited))
if (is_var(e) && !is_explored(var2id(e)))
todo.push_back(var2id(e));
break;
}
}
}
}
}