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

12 files changed, 49 insertions, 49 deletions

diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h
index 7e0cbff..6387adf 100644
--- a/include/atp/core/clause.h
+++ b/include/atp/core/clause.h
@@ -33,20 +33,20 @@ namespace atp {
 
 /// A clause: a disjunction of literals plus provenance for proof reconstruction.
 struct Clause {
-    ClauseId id = kInvalidId;
-    std::vector<Literal> literals;
+    ClauseId id_ = kInvalidId;
+    std::vector<Literal> literals_;
 
     // Provenance (for proof trace)
-    InferenceRule rule = InferenceRule::kInput;
-    ClauseId parent1 = kInvalidId;
-    ClauseId parent2 = kInvalidId;
-    uint16_t depth = 0;  ///< Derivation depth (for BFS scheduling)
+    InferenceRule rule_ = InferenceRule::kInput;
+    ClauseId parent1_ = kInvalidId;
+    ClauseId parent2_ = kInvalidId;
+    uint16_t depth_ = 0;  ///< Derivation depth (for BFS scheduling)
 
     /// True if the clause has no literals (contradiction).
-    [[nodiscard]] bool isEmpty() const { return literals.empty(); }
+    [[nodiscard]] bool isEmpty() const { return literals_.empty(); }
 
     /// Number of literals.
-    [[nodiscard]] size_t size() const { return literals.size(); }
+    [[nodiscard]] size_t size() const { return literals_.size(); }
 };
 
 }  // namespace atp
diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h
index 212c281..e58b185 100644
--- a/include/atp/core/literal.h
+++ b/include/atp/core/literal.h
@@ -27,11 +27,11 @@ namespace atp {
 
 /// A literal: a polarity flag plus the TermId of the atom.
 struct Literal {
-    TermId atom;       ///< TermId of the predicate application
-    bool is_positive;  ///< true = positive, false = negated
+    TermId atom_;       ///< TermId of the predicate application
+    bool is_positive_;  ///< true = positive, false = negated
 
     /// Complement: flip polarity, same atom.
-    [[nodiscard]] Literal complement() const { return {.atom = atom, .is_positive = !is_positive}; }
+    [[nodiscard]] Literal complement() const { return {.atom_ = atom_, .is_positive_ = !is_positive_}; }
 
     bool operator==(const Literal& other) const = default;
 };
diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h
index 30453fc..a646f78 100644
--- a/include/atp/core/symbol_table.h
+++ b/include/atp/core/symbol_table.h
@@ -33,10 +33,10 @@ namespace atp {
 
 /// Metadata associated with an interned symbol.
 struct SymbolInfo {
-    std::string name;
-    SymbolKind kind = SymbolKind::kFunction;
-    uint16_t arity = 0;
-    SortId sort = kUnsorted;  ///< Result sort (for sorted logic)
+    std::string name_;
+    SymbolKind kind_ = SymbolKind::kFunction;
+    uint16_t arity_ = 0;
+    SortId sort_ = kUnsorted;  ///< Result sort (for sorted logic)
 };
 
 /// Interns symbol names so that each unique string is stored exactly once.
diff --git a/include/atp/core/term.h b/include/atp/core/term.h
index 2be01e7..d35c753 100644
--- a/include/atp/core/term.h
+++ b/include/atp/core/term.h
@@ -33,11 +33,11 @@ namespace atp {
 /// A term is a function/predicate application: f(t1, t2, ..., tn).
 /// Variables are 0-arity terms whose symbol has SymbolKind::kVariable.
 struct Term {
-    SymbolId symbol_id;        ///< Index into the SymbolTable
-    std::vector<TermId> args;  ///< Argument sub-term IDs
+    SymbolId symbol_id_;        ///< Index into the SymbolTable
+    std::vector<TermId> args_;  ///< Argument sub-term IDs
 
     /// Number of arguments.
-    [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args.size()); }
+    [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args_.size()); }
 };
 
 }  // namespace atp
diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h
index f909e2f..3339ceb 100644
--- a/include/atp/core/term_bank.h
+++ b/include/atp/core/term_bank.h
@@ -61,17 +61,17 @@ class TermBank {
 
   private:
     struct TermKey {
-        SymbolId symbol;
-        std::vector<TermId> args;
+        SymbolId symbol_;
+        std::vector<TermId> args_;
 
         bool operator==(const TermKey& other) const = default;
     };
 
     struct TermKeyHash {
         size_t operator()(const TermKey& key) const {
-            size_t seed = std::hash<uint32_t>{}(key.symbol);
-            for (TermId arg : key.args) {
-                seed ^= std::hash<uint32_t>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+            size_t seed = std::hash<uint32_t>{}(key.symbol_);
+            for (const TermId kArg : key.args_) {
+                seed ^= std::hash<TermId>{}(kArg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
             }
             return seed;
         }
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index 738d34b..89eab6b 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -58,22 +58,22 @@ FormulaRole parseRole(std::string_view role_str);
 
 /// A parsed TPTP formula with its name and role.
 struct AnnotatedFormula {
-    std::string name;                  ///< Formula name (e.g., "axiom1")
-    FormulaRole role;                  ///< Semantic role
-    std::unique_ptr<Formula> formula;  ///< The FOL formula (for fof(...))
-    std::vector<Clause> clauses;       ///< Direct clauses (for cnf(...))
-    bool is_cnf = false;               ///< true if input was cnf(), false if fof()
+    std::string name_;                  ///< Formula name (e.g., "axiom1")
+    FormulaRole role_;                  ///< Semantic role
+    std::unique_ptr<Formula> formula_;  ///< The FOL formula (for fof(...))
+    std::vector<Clause> clauses_;       ///< Direct clauses (for cnf(...))
+    bool is_cnf_ = false;               ///< true if input was cnf(), false if fof()
 };
 
 /// A complete parsed TPTP problem.
 struct ParsedProblem {
-    std::vector<AnnotatedFormula> formulas;
+    std::vector<AnnotatedFormula> formulas_;
 
     /// Does any formula contain an equality predicate?
-    bool has_equality = false;
+    bool has_equality_ = false;
 
     /// Original file path (for error messages).
-    std::string source_file;
+    std::string source_file_;
 };
 
 /// Parse a TPTP file.
@@ -82,7 +82,7 @@ struct ParsedProblem {
 /// For `fof(...)` entries: Formula AST is built (clausification happens later).
 ///
 /// All symbols are interned into `symbols` and terms into `bank` during parsing.
-ParsedProblem parseTptpFile(const std::string& filepath, TermBank& bank, SymbolTable& symbols);
+ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols);
 
 /// Parse a TPTP string (for testing).
 ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols);
diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h
index c5954d7..5f8a206 100644
--- a/include/atp/index/discrim_tree.h
+++ b/include/atp/index/discrim_tree.h
@@ -37,8 +37,8 @@ namespace atp {
 
 /// A match result from the discrimination tree.
 struct IndexMatch {
-    ClauseId clause_id;
-    size_t lit_index;
+    ClauseId clause_id_;
+    size_t lit_index_;
 };
 
 /// A discrimination tree index over terms.
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index 9a4b6cc..870be66 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -28,7 +28,7 @@ namespace atp {
 
 /// Configuration for the unification algorithm.
 struct UnificationConfig {
-    bool enable_occurs_check = false;  ///< Set true for sound but slower unification
+    bool enable_occurs_check_ = false;  ///< Set true for sound but slower unification
 };
 
 /// Attempt to unify two terms, producing a most general unifier.
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index 1bcc021..5ee9b94 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -51,18 +51,18 @@ enum class FormulaKind : uint8_t {
 /// All identifiers are interned: atoms as TermIds, quantifier variables as
 /// SymbolIds. No raw strings survive past the parser.
 struct Formula {
-    FormulaKind kind;
+    FormulaKind kind_;
 
     /// For kAtom / kEquality: the predicate/equality term, already interned.
-    TermId atom = kInvalidId;
+    TermId atom_ = kInvalidId;
 
     /// For kForall / kExists: the bound variable, as an interned SymbolId.
     /// Using SymbolId (not string) so the clausifier can map bound variables
     /// back to term-bank variables without string lookups.
-    SymbolId bound_var = kInvalidId;
+    SymbolId bound_var_ = kInvalidId;
 
     /// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives).
-    std::vector<std::unique_ptr<Formula>> children;
+    std::vector<std::unique_ptr<Formula>> children_;
 
     // ── Factory methods ──
 
diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h
index 28099fe..4ea7aa1 100644
--- a/include/atp/proof/proof_trace.h
+++ b/include/atp/proof/proof_trace.h
@@ -32,10 +32,10 @@ namespace atp {
 
 /// A single step in a reconstructed proof.
 struct ProofStep {
-    ClauseId clause_id;
-    InferenceRule rule;
-    ClauseId parent1;
-    ClauseId parent2;
+    ClauseId clause_id_;
+    InferenceRule rule_;
+    ClauseId parent1_;
+    ClauseId parent2_;
 };
 
 /// Reconstruct the proof trace from the empty clause.
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.