refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components

2 files changed, 6 insertions, 6 deletions

diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h
index 6a8f9fc..dfb575c 100644
--- a/include/atp/search/clause_queue.h
+++ b/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/include/atp/search/prover.h b/include/atp/search/prover.h
index 6ee22f0..c1246ae 100644
--- a/include/atp/search/prover.h
+++ b/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.