aboutsummaryrefslogtreecommitdiff
path: root/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
commit4b31d8f59a6d3237f176a122c82f46fdaef4551d (patch)
tree917c9d42bb2cdbe96f5fc5416ae55789986029d7 /include/atp/search
parent5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 (diff)
downloadratp-master.tar.gz
ratp-master.tar.xz
feat: enhance clang-tidy configuration and improve code quality across multiple filesHEADmaster
Diffstat (limited to 'include/atp/search')
-rw-r--r--include/atp/search/prover.h9
1 files changed, 9 insertions, 0 deletions
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_;