mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 03:16:21 +00:00
Code Activity

simplify ho_matcher::whnf: rename shadowed variable, remove commented-out debug code

Browse source 
- Rename local 'e' variable to 'subst_val' in whnf() to avoid shadowing the
  function parameter 'e', which could cause confusion and compiler warnings
- Remove commented-out verbose_stream() debug lines that add noise without value
- Remove redundant blank line after removing commented code in consume_work()

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
github-actions[bot] 2026-05-24 05:38:50 +00:00 • committed by GitHub
parent 459629c662
commit 591fd2b293
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/euf/ho_matcher.cpp
View file

@ -185,16 +185,15 @@ namespace euf {
// //
expr_ref ho_matcher::whnf(expr* e, unsigned offset) const { expr_ref ho_matcher::whnf(expr* e, unsigned offset) const {
expr_ref r(e, m), t(m); expr_ref r(e, m), t(m);
// verbose_stream() << "ho_matcher::whnf: " << r << "\n";
if (is_meta_var(r, offset)) { if (is_meta_var(r, offset)) {
auto v = to_var(e); auto v = to_var(e);
auto idx = v->get_idx(); auto idx = v->get_idx();
if (idx >= offset && m_subst.get(idx - offset)) { if (idx >= offset && m_subst.get(idx - offset)) {
auto e = m_subst.get(idx - offset); expr* subst_val = m_subst.get(idx - offset);
r = e; r = subst_val;
if (offset > 0) { if (offset > 0) {
var_shifter sh(m); var_shifter sh(m);
sh(e, offset, r); sh(subst_val, offset, r);
} }
return r; return r;
} }
@ -202,24 +201,21 @@ namespace euf {
while (m_array.is_select(r)) { while (m_array.is_select(r)) {
app* a = to_app(r); app* a = to_app(r);
auto arg0 = a->get_arg(0); auto arg0 = a->get_arg(0);
// apply substitution:
if (is_meta_var(arg0, offset)) { if (is_meta_var(arg0, offset)) {
auto v = to_var(arg0); auto v = to_var(arg0);
auto idx = v->get_idx(); auto idx = v->get_idx();
if (idx >= offset && m_subst.get(idx - offset)) { if (idx >= offset && m_subst.get(idx - offset)) {
auto e = m_subst.get(idx - offset); expr* subst_val = m_subst.get(idx - offset);
if (offset > 0) { if (offset > 0) {
var_shifter sh(m); var_shifter sh(m);
sh(e, offset, r); sh(subst_val, offset, r);
e = r; subst_val = r;
} }
expr_ref_vector args(m); expr_ref_vector args(m);
args.push_back(e); args.push_back(subst_val);
for (unsigned i = 1; i < a->get_num_args(); ++i) for (unsigned i = 1; i < a->get_num_args(); ++i)
args.push_back(a->get_arg(i)); args.push_back(a->get_arg(i));
r = m.mk_app(a->get_decl(), args.size(), args.data()); r = m.mk_app(a->get_decl(), args.size(), args.data());
// verbose_stream() << "ho_matcher::whnf: " << r << "\n";
continue; continue;
} }
} }
@ -229,7 +225,6 @@ namespace euf {
ptr_vector<expr> args(a->get_num_args(), a->get_args()); ptr_vector<expr> args(a->get_num_args(), a->get_args());
args[0] = t; args[0] = t;
r = m_array.mk_select(args.size(), args.data()); r = m_array.mk_select(args.size(), args.data());
// verbose_stream() << "ho_matcher::whnf-rec: " << r << "\n";
continue; continue;
} }
} }
@ -317,8 +312,6 @@ namespace euf {
} }
bool ho_matcher::consume_work(match_goal &wi) { bool ho_matcher::consume_work(match_goal &wi) {
// IF_VERBOSE(1, display(verbose_stream() << "ho_matcher::consume_work: " << wi.pat << " =?= " << wi.t << "\n"););
if (wi.in_scope()) if (wi.in_scope())
m_trail.pop_scope(1); m_trail.pop_scope(1);