mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

cleanup

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-24 22:46:35 +07:00
parent b0247d8201
commit eb812e47be
2 changed files with 22 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/shared_occs.h
View file

@ -32,11 +32,8 @@ public:
void reset_mark(ast * n) { n->reset_mark_so(); }
void mark(ast * n) { if (is_marked(n)) return; n->mark_so(true); m_to_unmark.push_back(n); }
void reset() {
ptr_buffer<ast>::iterator it = m_to_unmark.begin();
ptr_buffer<ast>::iterator end = m_to_unmark.end();
for (; it != end; ++it) {
reset_mark(*it);
}
for (auto* t : m_to_unmark)
reset_mark(t);
m_to_unmark.reset();
}
void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); }

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

@ -36,7 +36,7 @@ void propagate_values::reduce() {
shared_occs shared(m, true);
expr_substitution subst(m, true, false);
expr* x, * y;
expr_ref_buffer args(m);
auto add_shared = [&]() {
shared_occs_mark visited;
shared.reset();
@ -50,15 +50,16 @@ void propagate_values::reduce() {
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) && m.is_value(x) && shared.is_shared(y))
subst.insert(y, x, dep);
else if (m.is_eq(f, x, y) && m.is_value(y) && shared.is_shared(x))
subst.insert(x, y, 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) {
expr* f = m_fmls[i].fml();
expr_dependency* dep = m_fmls[i].dep();
auto [f, dep] = m_fmls[i]();
expr_ref fml(m);
proof_ref pr(m);
m_rewriter(f, fml, pr);
@ -70,24 +71,23 @@ void propagate_values::reduce() {
m_rewriter.reset_used_dependencies();
add_sub(m_fmls[i]);
};
auto init_sub = [&]() {
add_shared();
subst.reset();
m_rewriter.reset();
m_rewriter.set_substitution(&subst);
for (unsigned i = 0; i < m_qhead; ++i)
add_sub(m_fmls[i]);
};
unsigned rw = m_stats.m_num_rewrites + 1;
for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) {
rw = m_stats.m_num_rewrites;
add_shared();
subst.reset();
m_rewriter.reset();
m_rewriter.set_substitution(&subst);
for (unsigned i = 0; i < m_qhead; ++i)
add_sub(m_fmls[i]);
init_sub();
for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i)
process_fml(i);
add_shared();
subst.reset();
m_rewriter.reset();
m_rewriter.set_substitution(&subst);
for (unsigned i = 0; i < m_qhead; ++i)
add_sub(m_fmls[i]);
init_sub();
for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();)
process_fml(i);
if (subst.empty())
@ -107,6 +107,7 @@ void propagate_values::collect_statistics(statistics& st) const {
void propagate_values::updt_params(params_ref const& p) {
tactic_params tp(p);
m_max_rounds = p.get_uint("max_rounds", tp.propagate_values_max_rounds());
m_rewriter.updt_params(p);
}
void propagate_values::collect_param_descrs(param_descrs& r) {