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

remove compute depth in favor of already existing get_depth

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-23 18:49:54 -08:00
parent e332904fb2
commit 09825edcd8
2 changed files with 1 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/solver/assertions/asserted_formulas.cpp
View file

@ -528,7 +528,6 @@ void asserted_formulas::commit() {
void asserted_formulas::commit(unsigned new_qhead) { void asserted_formulas::commit(unsigned new_qhead) {
m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead); m_macro_manager.mark_forbidden(new_qhead - m_qhead, m_formulas.data() + m_qhead);
m_expr2depth.reset();
for (unsigned i = m_qhead; i < new_qhead; ++i) { for (unsigned i = m_qhead; i < new_qhead; ++i) {
justified_expr const& j = m_formulas[i]; justified_expr const& j = m_formulas[i];
update_substitution(j.get_fml(), j.get_proof()); update_substitution(j.get_fml(), j.get_proof());
@ -545,7 +544,6 @@ void asserted_formulas::propagate_values() {
unsigned sz = m_formulas.size(); unsigned sz = m_formulas.size();
unsigned delta_prop = sz; unsigned delta_prop = sz;
while (!inconsistent() && sz/20 < delta_prop) { while (!inconsistent() && sz/20 < delta_prop) {
m_expr2depth.reset();
m_scoped_substitution.push(); m_scoped_substitution.push();
unsigned prop = num_prop; unsigned prop = num_prop;
TRACE("propagate_values", display(tout << "before:\n");); TRACE("propagate_values", display(tout << "before:\n"););
@ -555,7 +553,6 @@ void asserted_formulas::propagate_values() {
} }
flush_cache(); flush_cache();
m_scoped_substitution.pop(1); m_scoped_substitution.pop(1);
m_expr2depth.reset();
m_scoped_substitution.push(); m_scoped_substitution.push();
TRACE("propagate_values", tout << "middle:\n"; display(tout);); TRACE("propagate_values", tout << "middle:\n"; display(tout););
i = sz; i = sz;
@ -599,8 +596,6 @@ bool asserted_formulas::update_substitution(expr* n, proof* pr) {
expr* lhs, *rhs, *n1; expr* lhs, *rhs, *n1;
proof_ref pr1(m); proof_ref pr1(m);
if (is_ground(n) && m.is_eq(n, lhs, rhs)) { if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
compute_depth(lhs);
compute_depth(rhs);
if (is_gt(lhs, rhs)) { if (is_gt(lhs, rhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";); TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
m_scoped_substitution.insert(lhs, rhs, pr); m_scoped_substitution.insert(lhs, rhs, pr);
@ -667,38 +662,6 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
return false; return false;
} }
void asserted_formulas::compute_depth(expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
unsigned d = 0;
if (m_expr2depth.contains(e)) {
todo.pop_back();
continue;
}
if (is_app(e)) {
app* a = to_app(e);
bool visited = true;
for (expr* arg : *a) {
unsigned d1 = 0;
if (m_expr2depth.find(arg, d1)) {
d = std::max(d, d1);
}
else {
visited = false;
todo.push_back(arg);
}
}
if (!visited) {
continue;
}
}
todo.pop_back();
m_expr2depth.insert(e, d + 1);
}
}
proof * asserted_formulas::get_inconsistency_proof() const { proof * asserted_formulas::get_inconsistency_proof() const {
if (!inconsistent()) if (!inconsistent())
return nullptr; return nullptr;

4
src/solver/assertions/asserted_formulas.h
View file

@ -64,7 +64,6 @@ class asserted_formulas {
bool m_inconsistent_old; bool m_inconsistent_old;
}; };
svector<scope> m_scopes; svector<scope> m_scopes;
obj_map<expr, unsigned> m_expr2depth;
class simplify_fmls { class simplify_fmls {
protected: protected:
@ -247,8 +246,7 @@ class asserted_formulas {
unsigned propagate_values(unsigned i); unsigned propagate_values(unsigned i);
bool update_substitution(expr* n, proof* p); bool update_substitution(expr* n, proof* p);
bool is_gt(expr* lhs, expr* rhs); bool is_gt(expr* lhs, expr* rhs);
void compute_depth(expr* e); unsigned depth(expr* e) { return get_depth(e); }
unsigned depth(expr* e) { return m_expr2depth[e]; }
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs); void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);