From 5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Tue, 7 Apr 2026 03:59:58 +0800 Subject: refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components --- include/atp/core/clause.h | 16 ++++++++-------- include/atp/core/literal.h | 6 +++--- include/atp/core/symbol_table.h | 8 ++++---- include/atp/core/term.h | 6 +++--- include/atp/core/term_bank.h | 10 +++++----- include/atp/frontend/tptp_parser.h | 18 +++++++++--------- include/atp/index/discrim_tree.h | 4 ++-- include/atp/infer/unification.h | 2 +- include/atp/normalize/formula.h | 8 ++++---- include/atp/proof/proof_trace.h | 8 ++++---- include/atp/search/clause_queue.h | 4 ++-- include/atp/search/prover.h | 8 ++++---- 12 files changed, 49 insertions(+), 49 deletions(-) (limited to 'include') 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 literals; + ClauseId id_ = kInvalidId; + std::vector 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 args; ///< Argument sub-term IDs + SymbolId symbol_id_; ///< Index into the SymbolTable + std::vector args_; ///< Argument sub-term IDs /// Number of arguments. - [[nodiscard]] uint16_t arity() const { return static_cast(args.size()); } + [[nodiscard]] uint16_t arity() const { return static_cast(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 args; + SymbolId symbol_; + std::vector args_; bool operator==(const TermKey& other) const = default; }; struct TermKeyHash { size_t operator()(const TermKey& key) const { - size_t seed = std::hash{}(key.symbol); - for (TermId arg : key.args) { - seed ^= std::hash{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + size_t seed = std::hash{}(key.symbol_); + for (const TermId kArg : key.args_) { + seed ^= std::hash{}(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; ///< The FOL formula (for fof(...)) - std::vector 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_; ///< The FOL formula (for fof(...)) + std::vector 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 formulas; + std::vector 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> children; + std::vector> 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; /// 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. -- cgit v1.2.3