aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/include/atp/search
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
commit598f364de0a809747714294326a0193788e0bdfb (patch)
tree1ab77a340ab0930b41ffc6291d06b12d1b302a88 /proofsearch/include/atp/search
parent593a94a3c13aff82b31fd6c61e0ae07b97a2e426 (diff)
downloadrcc-project-598f364de0a809747714294326a0193788e0bdfb.tar.gz
rcc-project-598f364de0a809747714294326a0193788e0bdfb.tar.xz
refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components
Diffstat (limited to 'proofsearch/include/atp/search')
-rw-r--r--proofsearch/include/atp/search/clause_queue.h4
-rw-r--r--proofsearch/include/atp/search/prover.h8
2 files changed, 6 insertions, 6 deletions
diff --git a/proofsearch/include/atp/search/clause_queue.h b/proofsearch/include/atp/search/clause_queue.h
index 6a8f9fc..dfb575c 100644
--- a/proofsearch/include/atp/search/clause_queue.h
+++ b/proofsearch/include/atp/search/clause_queue.h
@@ -32,12 +32,12 @@ using ClauseComparator = std::function<bool(const Clause& a, const Clause& b)>;
/// BFS comparator: prioritize shallower derivation depth.
inline bool bfsCompare(const Clause& a, const Clause& b) {
- return a.depth > b.depth; // min-heap by depth
+ return a.depth_ > b.depth_; // min-heap by depth
}
/// Weight comparator: prioritize shorter (fewer literals) clauses.
inline bool weightCompare(const Clause& a, const Clause& b) {
- return a.literals.size() > b.literals.size(); // min-heap by literal count
+ return a.literals_.size() > b.literals_.size(); // min-heap by literal count
}
} // namespace atp
diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h
index 6ee22f0..c1246ae 100644
--- a/proofsearch/include/atp/search/prover.h
+++ b/proofsearch/include/atp/search/prover.h
@@ -46,10 +46,10 @@ enum class ProverResult : uint8_t {
/// V1 configuration — simple and direct.
/// Future: replaced by strategy::Calculus for dynamic rule loading.
struct ProverConfig {
- ClauseComparator comparator = bfsCompare;
- size_t max_clauses = 100000; ///< Safety limit
- size_t max_iterations = 500000; ///< Safety limit
- bool enable_occurs_check = false;
+ ClauseComparator comparator_ = bfsCompare;
+ size_t max_clauses_ = 100000; ///< Safety limit
+ size_t max_iterations_ = 500000; ///< Safety limit
+ bool enable_occurs_check_ = false;
};
/// Main prover class implementing the Given Clause Loop.