feat: enhance clang-tidy configuration and improve code quality across multiple files

2 files changed, 4 insertions, 7 deletions

diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc
index 82e59b7..5fb0d4a 100644
--- a/proofsearch/src/infer/resolution.cc
+++ b/proofsearch/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/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc
index 8710fb0..584008b 100644
--- a/proofsearch/src/infer/substitution.cc
+++ b/proofsearch/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() {