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

1 files changed, 95 insertions, 95 deletions

diff --git a/tests/test_resolution.cc b/tests/test_resolution.cc
index 931635d..02250d9 100644
--- a/tests/test_resolution.cc
+++ b/tests/test_resolution.cc
@@ -22,62 +22,62 @@
 #include "atp/core/term_bank.h"
 #include "atp/core/types.h"
 #include "atp/infer/resolution.h"
-#include "atp/infer/substitution.h"
-#include "atp/infer/unification.h"
 
 #include <gtest/gtest.h>
+#include <utility>
+#include <vector>
 
 namespace atp {
 namespace {
 
 class ResolutionTest : public ::testing::Test {
   protected:
-    SymbolTable symbols;
-    TermBank bank{symbols};
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
 
-    SymbolId sym_a{}, sym_b{}, sym_c{};
-    SymbolId sym_f{};
-    SymbolId sym_P{}, sym_Q{}, sym_R{};
-    SymbolId sym_X{}, sym_Y{}, sym_Z{};
+    SymbolId sym_a_{}, sym_b_{}, sym_c_{};
+    SymbolId sym_f_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{}, sym_y_{}, sym_z_{};
 
-    TermId a{}, b{}, c{};
-    TermId X{}, Y{}, Z{};
+    TermId a_{}, b_{}, c_{};
+    TermId x_{}, y_{}, z_{};
 
     void SetUp() override {
-        sym_a = symbols.intern("a", SymbolKind::kConstant);
-        sym_b = symbols.intern("b", SymbolKind::kConstant);
-        sym_c = symbols.intern("c", SymbolKind::kConstant);
-        sym_f = symbols.intern("f", SymbolKind::kFunction, 1);
-        sym_P = symbols.intern("P", SymbolKind::kPredicate, 1);
-        sym_Q = symbols.intern("Q", SymbolKind::kPredicate, 1);
-        sym_R = symbols.intern("R", SymbolKind::kPredicate, 2);
-        sym_X = symbols.intern("X", SymbolKind::kVariable);
-        sym_Y = symbols.intern("Y", SymbolKind::kVariable);
-        sym_Z = symbols.intern("Z", SymbolKind::kVariable);
-
-        a = bank.makeTerm(sym_a, {});
-        b = bank.makeTerm(sym_b, {});
-        c = bank.makeTerm(sym_c, {});
-        X = bank.makeVar(sym_X);
-        Y = bank.makeVar(sym_Y);
-        Z = bank.makeVar(sym_Z);
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_c_ = symbols_.intern("c", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_ = symbols_.intern("Y", SymbolKind::kVariable);
+        sym_z_ = symbols_.intern("Z", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        c_ = bank_.makeTerm(sym_c_, {});
+        x_ = bank_.makeVar(sym_x_);
+        y_ = bank_.makeVar(sym_y_);
+        z_ = bank_.makeVar(sym_z_);
     }
 
-    TermId P(TermId arg) { return bank.makeTerm(sym_P, {{arg}}); }
-    TermId Q(TermId arg) { return bank.makeTerm(sym_Q, {{arg}}); }
-    TermId R(TermId a1, TermId a2) { return bank.makeTerm(sym_R, {{a1, a2}}); }
-    TermId f(TermId arg) { return bank.makeTerm(sym_f, {{arg}}); }
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+    TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); }
+    TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); }
 
     // Helper: make a clause from literals
-    Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
+    static Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
         Clause c;
-        c.id = id;
-        c.literals = std::move(lits);
+        c.id_ = id;
+        c.literals_ = std::move(lits);
         return c;
     }
 
-    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
-    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
 };
 
 // ═══════════════════════════════════════════════════════════════════════════
@@ -86,86 +86,86 @@ class ResolutionTest : public ::testing::Test {
 
 TEST_F(ResolutionTest, SimpleGroundResolution) {
     // {P(a)} and {¬P(a), Q(b)}  → {Q(b)}
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(a)), pos(Q(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), pos(q(b_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 1);
-    EXPECT_EQ(result->literals[0].atom, Q(b));
-    EXPECT_TRUE(result->literals[0].is_positive);
+    EXPECT_EQ(result->literals_.size(), 1);
+    EXPECT_EQ(result->literals_[0].atom_, q(b_));
+    EXPECT_TRUE(result->literals_[0].is_positive_);
 }
 
 TEST_F(ResolutionTest, ResolutionWithUnification) {
     // {P(X)} and {¬P(a)} → {} (empty clause!)
-    Clause c1 = makeClause({pos(P(X))}, 0);
-    Clause c2 = makeClause({neg(P(a))}, 1);
+    Clause const c1 = makeClause({pos(p(x_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
     EXPECT_TRUE(result->isEmpty()) << "Should derive empty clause (contradiction)";
 }
 
 TEST_F(ResolutionTest, ResolutionFailsSamePolarity) {
     // {P(a)} and {P(b)} → no resolution (both positive)
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({pos(P(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(p(b_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     EXPECT_FALSE(result.has_value());
 }
 
 TEST_F(ResolutionTest, ResolutionFailsNoUnifier) {
     // {P(a)} and {¬P(b)} → can't unify a with b
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(b_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     EXPECT_FALSE(result.has_value());
 }
 
 TEST_F(ResolutionTest, ResolutionAppliesSubstToRemainingLiterals) {
     // {P(X), Q(X)} and {¬P(a)} → {Q(a)}
-    Clause c1 = makeClause({pos(P(X)), pos(Q(X))}, 0);
-    Clause c2 = makeClause({neg(P(a))}, 1);
+    Clause const c1 = makeClause({pos(p(x_)), pos(q(x_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 1);
-    EXPECT_EQ(result->literals[0].atom, Q(a));
+    EXPECT_EQ(result->literals_.size(), 1);
+    EXPECT_EQ(result->literals_[0].atom_, q(a_));
 }
 
 TEST_F(ResolutionTest, ResolutionMultipleLiterals) {
     // {P(X), Q(b)} and {¬P(a), R(a, c)} → {Q(b), R(a, c)}
-    Clause c1 = makeClause({pos(P(X)), pos(Q(b))}, 0);
-    Clause c2 = makeClause({neg(P(a)), pos(R(a, c))}, 1);
+    Clause const c1 = makeClause({pos(p(x_)), pos(q(b_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), pos(r(a_, c_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 2);
+    EXPECT_EQ(result->literals_.size(), 2);
 }
 
 TEST_F(ResolutionTest, VariableRenamingWorks) {
     // Both clauses use variable X
     // {P(X)} and {¬P(X), Q(X)} → {Q(a)} only if X is renamed in c2
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({neg(P(X)), pos(Q(X))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(x_)), pos(q(x_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->literals.size(), 1);
+    EXPECT_EQ(result->literals_.size(), 1);
     // Q(X) should become Q(a) after substitution {X→a}
-    EXPECT_EQ(result->literals[0].atom, Q(a));
+    EXPECT_EQ(result->literals_[0].atom_, q(a_));
 }
 
 TEST_F(ResolutionTest, VariableRenamingPreventsClash) {
     // {R(X, a)} and {¬R(b, X)}
     // Without renaming: X would clash between c1 and c2
     // With renaming: c2's X → _R0, then unify R(X,a) with R(b,_R0) → {X→b, _R0→a}
-    Clause c1 = makeClause({pos(R(X, a))}, 0);
-    Clause c2 = makeClause({neg(R(b, X))}, 1);
+    Clause const c1 = makeClause({pos(r(x_, a_))}, 0);
+    Clause const c2 = makeClause({neg(r(b_, x_))}, 1);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
     EXPECT_TRUE(result->isEmpty());
 }
@@ -177,19 +177,19 @@ TEST_F(ResolutionTest, VariableRenamingPreventsClash) {
 TEST_F(ResolutionTest, AllResolventsFindsAll) {
     // {P(a), Q(a)} and {¬P(a), ¬Q(a)}
     // Can resolve on P or Q → 2 resolvents
-    Clause c1 = makeClause({pos(P(a)), pos(Q(a))}, 0);
-    Clause c2 = makeClause({neg(P(a)), neg(Q(a))}, 1);
+    Clause const c1 = makeClause({pos(p(a_)), pos(q(a_))}, 0);
+    Clause const c2 = makeClause({neg(p(a_)), neg(q(a_))}, 1);
 
-    auto results = allResolvents(bank, c1, c2);
+    auto results = allResolvents(bank_, c1, c2);
     EXPECT_EQ(results.size(), 2);
 }
 
 TEST_F(ResolutionTest, AllResolventsEmpty) {
     // {P(a)} and {Q(b)} → no complementary pairs
-    Clause c1 = makeClause({pos(P(a))}, 0);
-    Clause c2 = makeClause({pos(Q(b))}, 1);
+    Clause const c1 = makeClause({pos(p(a_))}, 0);
+    Clause const c2 = makeClause({pos(q(b_))}, 1);
 
-    auto results = allResolvents(bank, c1, c2);
+    auto results = allResolvents(bank_, c1, c2);
     EXPECT_TRUE(results.empty());
 }
 
@@ -199,34 +199,34 @@ TEST_F(ResolutionTest, AllResolventsEmpty) {
 
 TEST_F(ResolutionTest, SimpleFactoring) {
     // {P(X), P(a), Q(X)} → factor P(X) with P(a): {P(a), Q(a)}
-    Clause c = makeClause({pos(P(X)), pos(P(a)), pos(Q(X))}, 0);
+    Clause const c = makeClause({pos(p(x_)), pos(p(a_)), pos(q(x_))}, 0);
 
-    auto results = factor(bank, c);
+    auto results = factor(bank_, c);
     ASSERT_EQ(results.size(), 1);
-    EXPECT_EQ(results[0].literals.size(), 2);
+    EXPECT_EQ(results[0].literals_.size(), 2);
     // After factoring: {P(a), Q(a)}
-    EXPECT_EQ(results[0].literals[0].atom, P(a));
-    EXPECT_EQ(results[0].literals[1].atom, Q(a));
+    EXPECT_EQ(results[0].literals_[0].atom_, p(a_));
+    EXPECT_EQ(results[0].literals_[1].atom_, q(a_));
 }
 
 TEST_F(ResolutionTest, NoFactoring) {
     // {P(a), Q(b)} → different predicates, can't factor
-    Clause c = makeClause({pos(P(a)), pos(Q(b))}, 0);
-    auto results = factor(bank, c);
+    Clause const c = makeClause({pos(p(a_)), pos(q(b_))}, 0);
+    auto results = factor(bank_, c);
     EXPECT_TRUE(results.empty());
 }
 
 TEST_F(ResolutionTest, FactoringDifferentPolarity) {
     // {P(a), ¬P(a)} → different polarity, can't factor
-    Clause c = makeClause({pos(P(a)), neg(P(a))}, 0);
-    auto results = factor(bank, c);
+    Clause const c = makeClause({pos(p(a_)), neg(p(a_))}, 0);
+    auto results = factor(bank_, c);
     EXPECT_TRUE(results.empty());
 }
 
 TEST_F(ResolutionTest, FactoringNonUnifiable) {
     // {P(a), P(b)} → can't unify a with b
-    Clause c = makeClause({pos(P(a)), pos(P(b))}, 0);
-    auto results = factor(bank, c);
+    Clause const c = makeClause({pos(p(a_)), pos(p(b_))}, 0);
+    auto results = factor(bank_, c);
     EXPECT_TRUE(results.empty());
 }
 
@@ -235,22 +235,22 @@ TEST_F(ResolutionTest, FactoringNonUnifiable) {
 // ═══════════════════════════════════════════════════════════════════════════
 
 TEST_F(ResolutionTest, ResolventHasProvenance) {
-    Clause c1 = makeClause({pos(P(X))}, 5);
-    Clause c2 = makeClause({neg(P(a))}, 7);
+    Clause const c1 = makeClause({pos(p(x_))}, 5);
+    Clause const c2 = makeClause({neg(p(a_))}, 7);
 
-    auto result = resolve(bank, c1, 0, c2, 0);
+    auto result = resolve(bank_, c1, 0, c2, 0);
     ASSERT_TRUE(result.has_value());
-    EXPECT_EQ(result->rule, InferenceRule::kResolution);
-    EXPECT_EQ(result->parent1, 5);
-    EXPECT_EQ(result->parent2, 7);
+    EXPECT_EQ(result->rule_, InferenceRule::kResolution);
+    EXPECT_EQ(result->parent1_, 5);
+    EXPECT_EQ(result->parent2_, 7);
 }
 
 TEST_F(ResolutionTest, FactoredHasProvenance) {
-    Clause c = makeClause({pos(P(X)), pos(P(a))}, 3);
-    auto results = factor(bank, c);
+    Clause const c = makeClause({pos(p(x_)), pos(p(a_))}, 3);
+    auto results = factor(bank_, c);
     ASSERT_FALSE(results.empty());
-    EXPECT_EQ(results[0].rule, InferenceRule::kFactoring);
-    EXPECT_EQ(results[0].parent1, 3);
+    EXPECT_EQ(results[0].rule_, InferenceRule::kFactoring);
+    EXPECT_EQ(results[0].parent1_, 3);
 }
 
 }  // namespace