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 --- tests/test_resolution.cc | 190 +++++++++++++++++++++++------------------------ 1 file changed, 95 insertions(+), 95 deletions(-) (limited to 'tests/test_resolution.cc') 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 +#include +#include 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 lits, ClauseId id = kInvalidId) { + static Clause makeClause(std::vector 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 -- cgit v1.2.3