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_simplify.cc | 102 +++++++++++++++++++++++++------------------------ 1 file changed, 52 insertions(+), 50 deletions(-) (limited to 'tests/test_simplify.cc') diff --git a/tests/test_simplify.cc b/tests/test_simplify.cc index 98b0db9..968ab3b 100644 --- a/tests/test_simplify.cc +++ b/tests/test_simplify.cc @@ -25,46 +25,48 @@ #include "atp/simplify/tautology.h" #include +#include +#include namespace atp { namespace { class SimplifyTest : public ::testing::Test { protected: - SymbolTable symbols; - TermBank bank{symbols}; + SymbolTable symbols_; + TermBank bank_{symbols_}; - SymbolId sym_a{}, sym_b{}, sym_c{}; - SymbolId sym_P{}, sym_Q{}, sym_R{}; - SymbolId sym_X{}; + SymbolId sym_a_{}, sym_b_{}, sym_c_{}; + SymbolId sym_p_{}, sym_q_{}, sym_r_{}; + SymbolId sym_x_{}; - TermId a{}, b{}, c{}, X{}; + TermId a_{}, b_{}, c_{}, x_{}; 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_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); - - a = bank.makeTerm(sym_a, {}); - b = bank.makeTerm(sym_b, {}); - c = bank.makeTerm(sym_c, {}); - X = bank.makeVar(sym_X); + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_c_ = symbols_.intern("c", SymbolKind::kConstant); + 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); + + a_ = bank_.makeTerm(sym_a_, {}); + b_ = bank_.makeTerm(sym_b_, {}); + c_ = bank_.makeTerm(sym_c_, {}); + x_ = bank_.makeVar(sym_x_); } - 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 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}}); } - 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}; } - Clause makeClause(std::vector lits) { + static Clause makeClause(std::vector lits) { Clause cl; - cl.literals = std::move(lits); + cl.literals_ = std::move(lits); return cl; } }; @@ -75,53 +77,53 @@ class SimplifyTest : public ::testing::Test { TEST_F(SimplifyTest, TautologyComplementaryLiterals) { // {P(a), ¬P(a)} → tautology - Clause cl = makeClause({pos(P(a)), neg(P(a))}); + Clause const cl = makeClause({pos(p(a_)), neg(p(a_))}); EXPECT_TRUE(isTautology(cl)); } TEST_F(SimplifyTest, TautologyWithExtraLiterals) { // {Q(b), P(a), ¬P(a)} → tautology - Clause cl = makeClause({pos(Q(b)), pos(P(a)), neg(P(a))}); + Clause const cl = makeClause({pos(q(b_)), pos(p(a_)), neg(p(a_))}); EXPECT_TRUE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologySamePolarity) { // {P(a), P(a)} → NOT tautology (same polarity) - Clause cl = makeClause({pos(P(a)), pos(P(a))}); + Clause const cl = makeClause({pos(p(a_)), pos(p(a_))}); EXPECT_FALSE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologyDifferentAtoms) { // {P(a), ¬P(b)} → NOT tautology (different atoms) - Clause cl = makeClause({pos(P(a)), neg(P(b))}); + Clause const cl = makeClause({pos(p(a_)), neg(p(b_))}); EXPECT_FALSE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologyDifferentPredicates) { // {P(a), ¬Q(a)} → NOT tautology (different predicates) - Clause cl = makeClause({pos(P(a)), neg(Q(a))}); + Clause const cl = makeClause({pos(p(a_)), neg(q(a_))}); EXPECT_FALSE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologyEmptyClause) { - Clause cl = makeClause({}); + Clause const cl = makeClause({}); EXPECT_FALSE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologySingleLiteral) { - Clause cl = makeClause({pos(P(a))}); + Clause const cl = makeClause({pos(p(a_))}); EXPECT_FALSE(isTautology(cl)); } TEST_F(SimplifyTest, TautologyVariableAtom) { // {P(X), ¬P(X)} → tautology (same variable term) - Clause cl = makeClause({pos(P(X)), neg(P(X))}); + Clause const cl = makeClause({pos(p(x_)), neg(p(x_))}); EXPECT_TRUE(isTautology(cl)); } TEST_F(SimplifyTest, NotTautologyVarVsConst) { // {P(X), ¬P(a)} → NOT tautology (syntactically different) - Clause cl = makeClause({pos(P(X)), neg(P(a))}); + Clause const cl = makeClause({pos(p(x_)), neg(p(a_))}); EXPECT_FALSE(isTautology(cl)); } @@ -131,57 +133,57 @@ TEST_F(SimplifyTest, NotTautologyVarVsConst) { TEST_F(SimplifyTest, SubsumesSubset) { // {P(a)} subsumes {P(a), Q(b)} - Clause gen = makeClause({pos(P(a))}); - Clause spec = makeClause({pos(P(a)), pos(Q(b))}); + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({pos(p(a_)), pos(q(b_))}); EXPECT_TRUE(subsumes(gen, spec)); } TEST_F(SimplifyTest, SubsumesIdentical) { // {P(a), Q(b)} subsumes {P(a), Q(b)} - Clause c1 = makeClause({pos(P(a)), pos(Q(b))}); - Clause c2 = makeClause({pos(P(a)), pos(Q(b))}); + Clause const c1 = makeClause({pos(p(a_)), pos(q(b_))}); + Clause const c2 = makeClause({pos(p(a_)), pos(q(b_))}); EXPECT_TRUE(subsumes(c1, c2)); } TEST_F(SimplifyTest, SubsumesEmptyClause) { // {} subsumes everything - Clause empty = makeClause({}); - Clause cl = makeClause({pos(P(a)), neg(Q(b))}); + Clause const empty = makeClause({}); + Clause const cl = makeClause({pos(p(a_)), neg(q(b_))}); EXPECT_TRUE(subsumes(empty, cl)); } TEST_F(SimplifyTest, SubsumesNotLarger) { // {P(a), Q(b)} does NOT subsume {P(a)} - Clause gen = makeClause({pos(P(a)), pos(Q(b))}); - Clause spec = makeClause({pos(P(a))}); + Clause const gen = makeClause({pos(p(a_)), pos(q(b_))}); + Clause const spec = makeClause({pos(p(a_))}); EXPECT_FALSE(subsumes(gen, spec)); } TEST_F(SimplifyTest, SubsumesRequiresSamePolarity) { // {P(a)} does NOT subsume {¬P(a)} - Clause gen = makeClause({pos(P(a))}); - Clause spec = makeClause({neg(P(a))}); + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({neg(p(a_))}); EXPECT_FALSE(subsumes(gen, spec)); } TEST_F(SimplifyTest, SubsumesRequiresSameAtom) { // {P(a)} does NOT subsume {P(b)} - Clause gen = makeClause({pos(P(a))}); - Clause spec = makeClause({pos(P(b))}); + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({pos(p(b_))}); EXPECT_FALSE(subsumes(gen, spec)); } TEST_F(SimplifyTest, SubsumesNegativeLiterals) { // {¬P(a)} subsumes {¬P(a), Q(b)} - Clause gen = makeClause({neg(P(a))}); - Clause spec = makeClause({neg(P(a)), pos(Q(b))}); + Clause const gen = makeClause({neg(p(a_))}); + Clause const spec = makeClause({neg(p(a_)), pos(q(b_))}); EXPECT_TRUE(subsumes(gen, spec)); } TEST_F(SimplifyTest, SubsumesOrderIndependent) { // {Q(b), P(a)} subsumes {P(a), Q(b), R(a,b)} regardless of order - Clause gen = makeClause({pos(Q(b)), pos(P(a))}); - Clause spec = makeClause({pos(P(a)), pos(Q(b)), pos(R(a, b))}); + Clause const gen = makeClause({pos(q(b_)), pos(p(a_))}); + Clause const spec = makeClause({pos(p(a_)), pos(q(b_)), pos(r(a_, b_))}); EXPECT_TRUE(subsumes(gen, spec)); } -- cgit v1.2.3