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

---
 include/atp/core/term_bank.h       | 11 ++++++-----
 include/atp/frontend/tptp_parser.h |  2 +-
 include/atp/search/prover.h        |  9 +++++++++
 3 files changed, 16 insertions(+), 6 deletions(-)

(limited to 'include/atp')

diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h
index 3339ceb..ca12759 100644
--- a/include/atp/core/term_bank.h
+++ b/include/atp/core/term_bank.h
@@ -39,7 +39,7 @@ class TermBank {
   public:
     /// TermBank needs the SymbolTable to distinguish variables from constants
     /// (both have 0 args, but SymbolKind differs).
-    explicit TermBank(const SymbolTable& symbols) : symbols_(symbols) {}
+        explicit TermBank(SymbolTable& symbols) : symbols_(&symbols) {}
 
     /// Create or retrieve a term. Returns the canonical TermId.
     TermId makeTerm(SymbolId symbol, std::span<const TermId> args);
@@ -57,7 +57,8 @@ class TermBank {
     [[nodiscard]] size_t size() const;
 
     /// Access the underlying SymbolTable.
-    [[nodiscard]] const SymbolTable& symbols() const { return symbols_; }
+    [[nodiscard]] const SymbolTable& symbols() const { return *symbols_; }
+    [[nodiscard]] SymbolTable& mutableSymbols() { return *symbols_; }
 
   private:
     struct TermKey {
@@ -70,14 +71,14 @@ class TermBank {
     struct TermKeyHash {
         size_t operator()(const TermKey& key) const {
             size_t seed = std::hash<uint32_t>{}(key.symbol_);
-            for (const TermId kArg : key.args_) {
-                seed ^= std::hash<TermId>{}(kArg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+            for (const TermId arg : key.args_) {
+                seed ^= std::hash<TermId>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
             }
             return seed;
         }
     };
 
-    const SymbolTable& symbols_;
+    SymbolTable* symbols_;
     std::vector<Term> terms_;
     std::unordered_map<TermKey, TermId, TermKeyHash> term_to_id_;
 };
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index 89eab6b..68a5564 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -59,7 +59,7 @@ FormulaRole parseRole(std::string_view role_str);
 /// A parsed TPTP formula with its name and role.
 struct AnnotatedFormula {
     std::string name_;                  ///< Formula name (e.g., "axiom1")
-    FormulaRole role_;                  ///< Semantic role
+    FormulaRole role_ = FormulaRole::kPlain;  ///< Semantic role
     std::unique_ptr<Formula> formula_;  ///< The FOL formula (for fof(...))
     std::vector<Clause> clauses_;       ///< Direct clauses (for cnf(...))
     bool is_cnf_ = false;               ///< true if input was cnf(), false if fof()
diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h
index c1246ae..65ec7f0 100644
--- a/include/atp/search/prover.h
+++ b/include/atp/search/prover.h
@@ -72,6 +72,15 @@ class Prover {
     [[nodiscard]] const ClauseStore& clauseStore() const { return store_; }
 
   private:
+    [[nodiscard]] bool hitResourceLimit(size_t iterations) const;
+    [[nodiscard]] Clause popGivenClause();
+    [[nodiscard]] bool isForwardSubsumedByProcessed(const Clause& clause) const;
+    [[nodiscard]] bool shouldSkipGiven(const Clause& given) const;
+    void applyBackwardSubsumption(const Clause& given);
+    [[nodiscard]] std::vector<Clause> generateNewClauses(const Clause& given) const;
+    [[nodiscard]] uint16_t computeDepth(const Clause& clause) const;
+    [[nodiscard]] std::optional<ClauseId> processNewClauses(std::vector<Clause> new_clauses);
+
     TermBank& bank_;
     ClauseStore& store_;
     ProverConfig config_;
-- 
cgit v1.2.3