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/search/prover.h | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'include/atp/search')

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