diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
| commit | a26a9311ed6cc34860092252d1750428b741b116 (patch) | |
| tree | 83eb5ccd5e94100a8e0368e8f25c977a2e2e6c03 /proofsearch/include/atp/search | |
| parent | 598f364de0a809747714294326a0193788e0bdfb (diff) | |
| download | rcc-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.h | 9 |
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_; |
