mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix perf bugs in new value propagation

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-02 07:54:14 -08:00
parent 758c3b2c3b
commit 3ebbb8472a
2 changed files with 45 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

74
src/ast/simplifiers/propagate_values.cpp
View file

@ -22,44 +22,19 @@ Notes:
#include "params/tactic_params.hpp"
#include "ast/ast_pp.h"
#include "ast/ast_util.h"
#include "ast/shared_occs.h"
#include "ast/simplifiers/propagate_values.h"
propagate_values::propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
dependent_expr_simplifier(m, fmls),
m_rewriter(m) {
m_rewriter.set_order_eq(true);
m_rewriter(m),
m_shared(m, true),
m_subst(m, true, false) {
m_rewriter.set_flat_and_or(false);
updt_params(p);
}
void propagate_values::reduce() {
shared_occs shared(m, true);
expr_substitution subst(m, true, false);
expr* x, * y;
auto add_shared = [&]() {
shared_occs_mark visited;
shared.reset();
for (unsigned i = 0; i < qtail(); ++i)
shared(m_fmls[i].fml(), visited);
};
auto add_sub = [&](dependent_expr const& de) {
auto const& [f, dep] = de();
if (m.is_not(f, x) && shared.is_shared(x))
subst.insert(x, m.mk_false(), dep);
else if (shared.is_shared(f))
subst.insert(f, m.mk_true(), dep);
if (m.is_eq(f, x, y)) {
if (m.is_value(x) && shared.is_shared(y))
subst.insert(y, x, dep);
else if (m.is_value(y) && shared.is_shared(x))
subst.insert(x, y, dep);
}
};
auto process_fml = [&](unsigned i) {
void propagate_values::process_fml(unsigned i) {
if (!m_subst.empty()) {
auto [f, dep] = m_fmls[i]();
expr_ref fml(m);
proof_ref pr(m);
@ -70,14 +45,41 @@ void propagate_values::reduce() {
++m_stats.m_num_rewrites;
}
m_rewriter.reset_used_dependencies();
add_sub(m_fmls[i]);
};
}
add_sub(m_fmls[i]);
}
void propagate_values::add_sub(dependent_expr const& de) {
expr* x, * y;
auto const& [f, dep] = de();
if (m.is_not(f, x) && m_shared.is_shared(x))
m_subst.insert(x, m.mk_false(), dep);
if (m_shared.is_shared(f))
m_subst.insert(f, m.mk_true(), dep);
if (m.is_eq(f, x, y)) {
if (m.is_value(x) && m_shared.is_shared(y))
m_subst.insert(y, x, dep);
else if (m.is_value(y) && m_shared.is_shared(x))
m_subst.insert(x, y, dep);
}
};
void propagate_values::reduce() {
m_shared.reset();
m_subst.reset();
auto add_shared = [&]() {
shared_occs_mark visited;
m_shared.reset();
for (unsigned i = 0; i < qtail(); ++i)
m_shared(m_fmls[i].fml(), visited);
};
auto init_sub = [&]() {
add_shared();
subst.reset();
m_subst.reset();
m_rewriter.reset();
m_rewriter.set_substitution(&subst);
m_rewriter.set_substitution(&m_subst);
for (unsigned i = 0; i < qhead(); ++i)
add_sub(m_fmls[i]);
};
@ -91,12 +93,14 @@ void propagate_values::reduce() {
init_sub();
for (unsigned i = qtail(); i-- > qhead() && m.inc() && !m_fmls.inconsistent();)
process_fml(i);
if (subst.empty())
if (m_subst.empty())
break;
}
m_rewriter.set_substitution(nullptr);
m_rewriter.reset();
m_subst.reset();
m_shared.reset();
}
void propagate_values::collect_statistics(statistics& st) const {

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

@ -22,6 +22,7 @@ Notes:
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/shared_occs.h"
class propagate_values : public dependent_expr_simplifier {
@ -34,6 +35,11 @@ class propagate_values : public dependent_expr_simplifier {
th_rewriter m_rewriter;
stats m_stats;
unsigned m_max_rounds = 4;
shared_occs m_shared;
expr_substitution m_subst;
void process_fml(unsigned i);
void add_sub(dependent_expr const& de);
public:
propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls);