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

7 files changed, 163 insertions, 150 deletions

diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc
index 2e117b3..0dc166f 100644
--- a/src/core/term_bank.cc
+++ b/src/core/term_bank.cc
@@ -53,7 +53,7 @@ const Term& TermBank::getTerm(TermId id) const {
 
 bool TermBank::isVariable(TermId id) const {
     assert(id < terms_.size() && "TermId out of bounds!");
-    return symbols_.isVariable(terms_[id].symbol_id_);
+    return symbols_->isVariable(terms_[id].symbol_id_);
 }
 
 size_t TermBank::size() const {
diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc
index ddf8aad..10190b8 100644
--- a/src/frontend/tptp_parser.cc
+++ b/src/frontend/tptp_parser.cc
@@ -42,31 +42,31 @@ namespace atp {
 FormulaRole parseRole(std::string_view role_str) {
     if (role_str == "axiom") {
         return FormulaRole::kAxiom;
-}
+    }
     if (role_str == "hypothesis") {
         return FormulaRole::kHypothesis;
-}
+    }
     if (role_str == "definition") {
         return FormulaRole::kDefinition;
-}
+    }
     if (role_str == "assumption") {
         return FormulaRole::kAssumption;
-}
+    }
     if (role_str == "lemma") {
         return FormulaRole::kLemma;
-}
+    }
     if (role_str == "theorem") {
         return FormulaRole::kTheorem;
-}
+    }
     if (role_str == "conjecture") {
         return FormulaRole::kConjecture;
-}
+    }
     if (role_str == "negated_conjecture") {
         return FormulaRole::kNegatedConjecture;
-}
+    }
     if (role_str == "plain") {
         return FormulaRole::kPlain;
-}
+    }
     return FormulaRole::kPlain;
 }
 
@@ -215,7 +215,7 @@ class TptpParser {
     SymbolTable& symbols_;
     Token current_token_{};
     std::vector<Token> tokens_;
-    std::unordered_map<std::string_view, SymbolId> variable_cache_{};
+    std::unordered_map<std::string_view, SymbolId> variable_cache_;
 
     void advance() { current_token_ = lexer_.nextToken(); }
 
@@ -252,27 +252,28 @@ class TptpParser {
             TermId const var_id = bank_.makeVar(sym);
             variable_cache_[name] = var_id;
             return var_id;
-        }             // Check if this is a function/predicate (has args) or a constant (no parens)
-            if (current_token_.type_ == TokenType::kLParen) {
-                advance();  // consume '('
-                std::vector<TermId> args;
-                if (current_token_.type_ != TokenType::kRParen) {
+        }
+
+        // Check if this is a function/predicate (has args) or a constant (no parens)
+        if (current_token_.type_ == TokenType::kLParen) {
+            advance();  // consume '('
+            std::vector<TermId> args;
+            if (current_token_.type_ != TokenType::kRParen) {
+                args.push_back(parseTerm());
+                while (current_token_.type_ == TokenType::kComma) {
+                    advance();
                     args.push_back(parseTerm());
-                    while (current_token_.type_ == TokenType::kComma) {
-                        advance();
-                        args.push_back(parseTerm());
-                    }
                 }
-                expect(TokenType::kRParen);
-                SymbolId sym = symbols_.intern(name, SymbolKind::kFunction,
-                                               static_cast<uint16_t>(args.size()));
-                return bank_.makeTerm(sym, args);
-            } else {
-                // Constant: no parentheses (e.g., a, b, h0, s0)
-                SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
-                return bank_.makeTerm(sym, {});
             }
-       
+            expect(TokenType::kRParen);
+            const SymbolId sym = symbols_.intern(name, SymbolKind::kFunction,
+                                                 static_cast<uint16_t>(args.size()));
+            return bank_.makeTerm(sym, args);
+        }
+
+        // Constant: no parentheses (e.g., a, b, h0, s0)
+        const SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
+        return bank_.makeTerm(sym, {});
     }
 
     Literal parseLiteral() {
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() {
diff --git a/src/main.cc b/src/main.cc
index 81dbc91..c683d39 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -43,7 +43,7 @@ int main(int argc, char* argv[]) {
         return EXIT_FAILURE;
     }
 
-    const std::string kFilepath = argv[1];
+    const std::string filepath = argv[1];
 
     try {
         // 1. Initialize core modules
@@ -52,9 +52,9 @@ int main(int argc, char* argv[]) {
         atp::ClauseStore store;
 
         // 2. Parse TPTP input
-        auto problem = atp::parseTptpFile(kFilepath, bank, symbols);
+        auto problem = atp::parseTptpFile(filepath, bank, symbols);
 
-        std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << kFilepath
+        std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << filepath
                   << "\n";
 
         // 3. Prepare clauses for proving
@@ -70,23 +70,23 @@ int main(int argc, char* argv[]) {
         // 5. Output result (SZS format)
         switch (result) {
             case atp::ProverResult::kTheorem: {
-                std::cout << "% SZS status Theorem for " << kFilepath << "\n\n";
+                std::cout << "% SZS status Theorem for " << filepath << "\n\n";
 
                 // Extract and print proof
                 auto eid = prover.getEmptyClauseId();
                 if (eid.has_value()) {
                     auto proof = atp::extractProof(store, *eid);
-                    std::cout << "% SZS output start Proof for " << kFilepath << "\n";
+                    std::cout << "% SZS output start Proof for " << filepath << "\n";
                     std::cout << atp::formatProof(proof, store, bank);
-                    std::cout << "% SZS output end Proof for " << kFilepath << "\n";
+                    std::cout << "% SZS output end Proof for " << filepath << "\n";
                 }
                 break;
             }
             case atp::ProverResult::kSaturation:
-                std::cout << "% SZS status Satisfiable for " << kFilepath << "\n";
+                std::cout << "% SZS status Satisfiable for " << filepath << "\n";
                 break;
             case atp::ProverResult::kTimeout:
-                std::cout << "% SZS status Timeout for " << kFilepath << "\n";
+                std::cout << "% SZS status Timeout for " << filepath << "\n";
                 break;
         }
 
diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index a0d5a11..5fa4b04 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -26,7 +26,6 @@
 #include "atp/core/types.h"
 
 #include <algorithm>
-#include <array>
 #include <cstddef>
 #include <stack>
 #include <string>
@@ -47,20 +46,20 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
     worklist.push(empty_clause_id);
 
     while (!worklist.empty()) {
-        const ClauseId kCid = worklist.top();
+        const ClauseId cid = worklist.top();
         worklist.pop();
 
-        if (kCid == kInvalidId) {
+        if (cid == kInvalidId) {
             continue;
         }
-        if (visited.contains(kCid)) {
+        if (visited.contains(cid)) {
             continue;
         }
-        visited.insert(kCid);
+        visited.insert(cid);
 
-        const Clause& c = store.getClause(kCid);
+        const Clause& c = store.getClause(cid);
         steps.push_back({
-            .clause_id_ = kCid,
+            .clause_id_ = cid,
             .rule_ = c.rule_,
             .parent1_ = c.parent1_,
             .parent2_ = c.parent2_,
@@ -105,15 +104,32 @@ namespace {
 /// Generate a human-readable variable name from an index.
 /// 0→X, 1→Y, 2→Z, 3→W, 4→V, 5→U, 6→X1, 7→Y1, ...
 std::string prettyVarName(size_t index) {
-    static constexpr std::array<char, 6> kBaseNames = {'X', 'Y', 'Z', 'W', 'V', 'U'};
-    static constexpr size_t kBaseCount = kBaseNames.size();
+    constexpr size_t kBaseCount = 6;
+    const size_t base_index = index % kBaseCount;
+    const char base = [&]() {
+        switch (base_index) {
+            case 0:
+                return 'X';
+            case 1:
+                return 'Y';
+            case 2:
+                return 'Z';
+            case 3:
+                return 'W';
+            case 4:
+                return 'V';
+            case 5:
+                return 'U';
+            default:
+                return 'X';
+        }
+    }();
 
-    const char kBase = kBaseNames[index % kBaseCount];
-    const size_t kSuffix = index / kBaseCount;
-    if (kSuffix == 0) {
-        return std::string{kBase};
+    const size_t suffix = index / kBaseCount;
+    if (suffix == 0) {
+        return std::string{base};
     }
-    return std::string{kBase} + std::to_string(kSuffix);
+    return std::string{base} + std::to_string(suffix);
 }
 
 /// Pretty-print a term, renaming variables to readable names.
@@ -125,9 +141,9 @@ std::string termToPretty(TermId id, const TermBank& bank,
         if (it != var_map.end()) {
             return it->second;
         }
-        const std::string kName = prettyVarName(var_map.size());
-        var_map[id] = kName;
-        return kName;
+        const std::string name = prettyVarName(var_map.size());
+        var_map[id] = name;
+        return name;
     }
 
     const Term& t = bank.getTerm(id);
diff --git a/src/search/prover.cc b/src/search/prover.cc
index 2c2de40..f3f8bb0 100644
--- a/src/search/prover.cc
+++ b/src/search/prover.cc
@@ -47,114 +47,113 @@ void Prover::addClauses(std::vector<Clause> clauses) {
     }
 }
 
+bool Prover::hitResourceLimit(size_t iterations) const {
+    return iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_;
+}
+
+Clause Prover::popGivenClause() {
+    Clause given = unprocessed_.top();
+    unprocessed_.pop();
+    return given;
+}
+
+bool Prover::isForwardSubsumedByProcessed(const Clause& clause) const {
+    return std::ranges::any_of(processed_,
+                               [&](ClauseId pid) { return subsumes(store_.getClause(pid), clause); });
+}
+
+bool Prover::shouldSkipGiven(const Clause& given) const {
+    return isTautology(given) || isForwardSubsumedByProcessed(given);
+}
+
+void Prover::applyBackwardSubsumption(const Clause& given) {
+    std::erase_if(processed_, [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); });
+}
+
+std::vector<Clause> Prover::generateNewClauses(const Clause& given) const {
+    std::vector<Clause> new_clauses;
+    const UnificationConfig uconfig{.enable_occurs_check_ = config_.enable_occurs_check_};
+
+    for (ClauseId const pid : processed_) {
+        const Clause& pc = store_.getClause(pid);
+
+        auto resolvents1 = allResolvents(bank_, given, pc, uconfig);
+        auto resolvents2 = allResolvents(bank_, pc, given, uconfig);
+
+        for (auto& r : resolvents1) {
+            new_clauses.push_back(std::move(r));
+        }
+        for (auto& r : resolvents2) {
+            new_clauses.push_back(std::move(r));
+        }
+    }
+
+    auto factors = factor(bank_, given, uconfig);
+    for (auto& f : factors) {
+        new_clauses.push_back(std::move(f));
+    }
+
+    return new_clauses;
+}
+
+uint16_t Prover::computeDepth(const Clause& clause) const {
+    uint32_t const d1 = (clause.parent1_ != kInvalidId) ? store_.getClause(clause.parent1_).depth_ : 0;
+    uint32_t const d2 = (clause.parent2_ != kInvalidId) ? store_.getClause(clause.parent2_).depth_ : 0;
+    return static_cast<uint16_t>(std::max(d1, d2) + 1);
+}
+
+std::optional<ClauseId> Prover::processNewClauses(std::vector<Clause> new_clauses) {
+    for (auto& nc : new_clauses) {
+        if (nc.isEmpty()) {
+            return store_.addClause(std::move(nc));
+        }
+
+        if (isTautology(nc)) {
+            continue;
+        }
+
+        nc.depth_ = computeDepth(nc);
+
+        ClauseId const nid = store_.addClause(nc);
+        const Clause& stored_nc = store_.getClause(nid);
+        if (isForwardSubsumedByProcessed(stored_nc)) {
+            continue;
+        }
+
+        unprocessed_.push(stored_nc);
+    }
+
+    return std::nullopt;
+}
+
 ProverResult Prover::prove() {
     size_t iterations = 0;
 
     while (!unprocessed_.empty()) {
-        // Resource limits
-        if (iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_) {
+        if (hitResourceLimit(iterations)) {
             return ProverResult::kTimeout;
         }
         ++iterations;
 
-        // 1. Select the best clause from unprocessed
-        Clause given = unprocessed_.top();
-        unprocessed_.pop();
+        Clause given = popGivenClause();
 
-        // 2. Check if given is itself the empty clause
         if (given.isEmpty()) {
             empty_clause_id_ = given.id_;
             return ProverResult::kTheorem;
         }
 
-        // 3. Forward redundancy checks
-        if (isTautology(given)) {
-            continue;
-        }
-
-        bool forward_subsumed = false;
-        for (ClauseId const pid : processed_) {
-            if (subsumes(store_.getClause(pid), given)) {
-                forward_subsumed = true;
-                break;
-            }
-        }
-        if (forward_subsumed) {
+        if (shouldSkipGiven(given)) {
             continue;
         }
 
-        // 4. Backward subsumption
-        // Remove from processed all clauses that are subsumed by given.
-        // Use erase-remove idiom for O(n) scan instead of repeated erase.
-        std::erase_if(processed_,
-                      [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); });
-
-        // 5. Generate new clauses
-        // Inference BEFORE adding given to processed — matches doc §4.6.
-        std::vector<Clause> new_clauses;
-        const UnificationConfig kUconfig{.enable_occurs_check_ = config_.enable_occurs_check_};
-
-        // 5a. Resolve given with every processed clause (both directions)
-        for (ClauseId const pid : processed_) {
-            const Clause& pc = store_.getClause(pid);
-
-            auto resolvents1 = allResolvents(bank_, given, pc, kUconfig);
-            auto resolvents2 = allResolvents(bank_, pc, given, kUconfig);
-
-            for (auto& r : resolvents1) {
-                new_clauses.push_back(std::move(r));
-            }
-            for (auto& r : resolvents2) {
-                new_clauses.push_back(std::move(r));
-            }
-        }
-
-        // 5b. Factor given (only once)
-        auto factors = factor(bank_, given, kUconfig);
-        for (auto& f : factors) {
-            new_clauses.push_back(std::move(f));
-        }
-
-        // 6. Add given to processed AFTER inference
+        applyBackwardSubsumption(given);
+        std::vector<Clause> new_clauses = generateNewClauses(given);
         processed_.push_back(given.id_);
 
-        // 7. Process new clauses
-        for (auto& nc : new_clauses) {
-            // 7a. Check for empty clause → proof found!
-            if (nc.isEmpty()) {
-                ClauseId eid = store_.addClause(std::move(nc));
-                empty_clause_id_ = eid;
-                return ProverResult::kTheorem;
-            }
-
-            // 7b. Skip tautologies
-            if (isTautology(nc)) {
-                continue;
-            }
-
-            // 7c. Set depth
-            uint32_t const d1 = (nc.parent1_ != kInvalidId) ? store_.getClause(nc.parent1_).depth_ : 0;
-            uint32_t const d2 = (nc.parent2_ != kInvalidId) ? store_.getClause(nc.parent2_).depth_ : 0;
-            nc.depth_ = static_cast<uint16_t>(std::max(d1, d2) + 1);
-
-            // 7d. Store the clause (needed for forward subsumption check)
-            ClauseId const nid = store_.addClause(nc);
-            const Clause& stored_nc = store_.getClause(nid);
-
-            // 7e. Forward subsumption on new clause
-            bool new_subsumed = false;
-            for (ClauseId const pid : processed_) {
-                if (subsumes(store_.getClause(pid), stored_nc)) {
-                    new_subsumed = true;
-                    break;
-                }
-            }
-            if (new_subsumed) {
-                continue;
-            }
-
-            // 7f. Enqueue
-            unprocessed_.push(stored_nc);
+        const std::optional<ClauseId> derived_empty = processNewClauses(std::move(new_clauses));
+        if (derived_empty.has_value()) {
+            empty_clause_id_ = derived_empty;
+            return ProverResult::kTheorem;
         }
     }