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

micro-tuning

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-08 09:11:08 -07:00
parent c6cd25c822
commit 0fec7efc7b
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/th_rewriter.cpp
View file

@ -59,6 +59,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bv_util m_bv_util; bv_util m_bv_util;
der m_der; der m_der;
expr_safe_replace m_rep; expr_safe_replace m_rep;
unused_vars_eliminator m_elim_unused_vars;
expr_ref_vector m_pinned; expr_ref_vector m_pinned;
// substitution support // substitution support
expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
@ -829,8 +830,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
} }
} }
SASSERT(old_q->get_sort() == q1->get_sort()); SASSERT(old_q->get_sort() == q1->get_sort());
result = elim_unused_vars(m(), q1, params_ref()); result = m_elim_unused_vars(q1);
result_pr = nullptr; result_pr = nullptr;
@ -887,6 +887,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_bv_util(m), m_bv_util(m),
m_der(m), m_der(m),
m_rep(m), m_rep(m),
m_elim_unused_vars(m, params_ref()),
m_pinned(m), m_pinned(m),
m_used_dependencies(m) { m_used_dependencies(m) {
updt_local_params(p); updt_local_params(p);