From 4b31d8f59a6d3237f176a122c82f46fdaef4551d Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Wed, 8 Apr 2026 03:23:16 +0800
Subject: feat: enhance clang-tidy configuration and improve code quality
 across multiple files

---
 src/infer/resolution.cc   | 2 +-
 src/infer/substitution.cc | 9 +++------
 2 files changed, 4 insertions(+), 7 deletions(-)

(limited to 'src/infer')

diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index 82e59b7..5fb0d4a 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -98,7 +98,7 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
     // Rename c2's variables to avoid clashes with c1
     // Use a static counter — safe for single-threaded prover
     static uint32_t var_counter = 0;
-    auto& symbols = const_cast<SymbolTable&>(bank.symbols());
+    auto& symbols = bank.mutableSymbols();
     Clause c2r = renameVariables(c2, bank, symbols, var_counter);
 
     // Unify the complementary atoms
diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc
index 8710fb0..584008b 100644
--- a/src/infer/substitution.cc
+++ b/src/infer/substitution.cc
@@ -22,6 +22,7 @@
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 
+#include <algorithm>
 #include <vector>
 
 namespace atp {
@@ -107,12 +108,8 @@ bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const
     }
 
     const Term& t = bank.getTerm(term);
-    for (TermId const arg : t.args_) {
-        if (occursIn(var, arg, bank)) {
-            return true;
-        }
-    }
-    return false;
+    return std::any_of(t.args_.begin(), t.args_.end(),
+                       [&](TermId arg) { return occursIn(var, arg, bank); });
 }
 
 void Substitution::clear() {
-- 
cgit v1.2.3