aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/include/atp/search
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-08 03:23:16 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-08 03:23:16 +0800
commita26a9311ed6cc34860092252d1750428b741b116 (patch)
tree83eb5ccd5e94100a8e0368e8f25c977a2e2e6c03 /proofsearch/include/atp/search
parent598f364de0a809747714294326a0193788e0bdfb (diff)
downloadrcc-project-a26a9311ed6cc34860092252d1750428b741b116.tar.gz
rcc-project-a26a9311ed6cc34860092252d1750428b741b116.tar.xz
feat: enhance clang-tidy configuration and improve code quality across multiple files
Diffstat (limited to 'proofsearch/include/atp/search')
-rw-r--r--proofsearch/include/atp/search/prover.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h
index c1246ae..65ec7f0 100644
--- a/proofsearch/include/atp/search/prover.h
+++ b/proofsearch/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_;