From bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 05:21:26 +0800 Subject: style: reformat codebase with consistent indentation --- tests/test_clausifier.cc | 2 -- tests/test_discrim_tree.cc | 2 -- tests/test_end_to_end.cc | 9 ++++----- tests/test_proof_trace.cc | 25 ++++++------------------ tests/test_prover.cc | 48 +++++++++++++++------------------------------- tests/test_resolution.cc | 4 ++-- tests/test_simplify.cc | 4 ++-- tests/test_term_bank.cc | 4 ++-- tests/test_unification.cc | 7 +++---- 9 files changed, 34 insertions(+), 71 deletions(-) (limited to 'tests') diff --git a/tests/test_clausifier.cc b/tests/test_clausifier.cc index b62ffd0..17c63f8 100644 --- a/tests/test_clausifier.cc +++ b/tests/test_clausifier.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/tests/test_discrim_tree.cc b/tests/test_discrim_tree.cc index b62ffd0..17c63f8 100644 --- a/tests/test_discrim_tree.cc +++ b/tests/test_discrim_tree.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/tests/test_end_to_end.cc b/tests/test_end_to_end.cc index 44a44c2..d45a101 100644 --- a/tests/test_end_to_end.cc +++ b/tests/test_end_to_end.cc @@ -19,8 +19,6 @@ /// @file test_end_to_end.cc /// @brief End-to-end tests: TPTP string → parse → prove → verify result. -#include - #include "atp/core/clause_store.h" #include "atp/core/symbol_table.h" #include "atp/core/term_bank.h" @@ -28,6 +26,7 @@ #include "atp/proof/proof_trace.h" #include "atp/search/prover.h" +#include #include namespace atp { @@ -175,9 +174,9 @@ TEST(EndToEnd, MonkeyBanana) { cnf(negated_goal, negated_conjecture, ~goal_reached(S)). )"); - EXPECT_EQ(result, ProverResult::kTheorem) - << "ATP should prove the monkey can get the banana!\n" - << "Proof output:\n" << proof; + EXPECT_EQ(result, ProverResult::kTheorem) << "ATP should prove the monkey can get the banana!\n" + << "Proof output:\n" + << proof; } } // namespace diff --git a/tests/test_proof_trace.cc b/tests/test_proof_trace.cc index d7ff246..5e12060 100644 --- a/tests/test_proof_trace.cc +++ b/tests/test_proof_trace.cc @@ -16,8 +16,6 @@ * along with this program. If not, see . */ -#include - #include "atp/core/clause.h" #include "atp/core/clause_store.h" #include "atp/core/literal.h" @@ -27,6 +25,7 @@ #include "atp/proof/proof_trace.h" #include "atp/search/prover.h" +#include #include namespace atp { @@ -125,10 +124,7 @@ TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) { TEST_F(ProofTraceTest, ExtractProofTrivial) { // Run a trivial proof: {P(a)} + {¬P(a)} → □ Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a_term))}), - makeClause({neg(P(a_term))}) - }); + prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})}); ProverResult result = prover.prove(); ASSERT_EQ(result, ProverResult::kTheorem); @@ -149,11 +145,8 @@ TEST_F(ProofTraceTest, ExtractProofTrivial) { TEST_F(ProofTraceTest, ExtractProofTwoStep) { // {P(a)}, {¬P(X), Q(X)}, {¬Q(a)} → □ in 2 resolution steps Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a_term))}), - makeClause({neg(P(X_term)), pos(Q(X_term))}), - makeClause({neg(Q(a_term))}) - }); + prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(X_term)), pos(Q(X_term))}), + makeClause({neg(Q(a_term))})}); ProverResult result = prover.prove(); ASSERT_EQ(result, ProverResult::kTheorem); @@ -174,10 +167,7 @@ TEST_F(ProofTraceTest, ExtractProofTwoStep) { TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a_term))}), - makeClause({neg(P(a_term))}) - }); + prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})}); prover.prove(); auto eid = prover.getEmptyClauseId(); @@ -197,10 +187,7 @@ TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) { TEST_F(ProofTraceTest, FormatProofNoParentsForAxioms) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a_term))}), - makeClause({neg(P(a_term))}) - }); + prover.addClauses({makeClause({pos(P(a_term))}), makeClause({neg(P(a_term))})}); prover.prove(); auto eid = prover.getEmptyClauseId(); diff --git a/tests/test_prover.cc b/tests/test_prover.cc index cec1c35..ada1af2 100644 --- a/tests/test_prover.cc +++ b/tests/test_prover.cc @@ -16,8 +16,6 @@ * along with this program. If not, see . */ -#include - #include "atp/core/clause.h" #include "atp/core/clause_store.h" #include "atp/core/literal.h" @@ -26,6 +24,8 @@ #include "atp/core/types.h" #include "atp/search/prover.h" +#include + namespace atp { namespace { @@ -79,10 +79,7 @@ class ProverTest : public ::testing::Test { TEST_F(ProverTest, TrivialRefutation) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a))}), - makeClause({neg(P(a))}) - }); + prover.addClauses({makeClause({pos(P(a))}), makeClause({neg(P(a))})}); ProverResult result = prover.prove(); EXPECT_EQ(result, ProverResult::kTheorem); @@ -95,10 +92,7 @@ TEST_F(ProverTest, TrivialRefutation) { TEST_F(ProverTest, RefutationWithUnification) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(X))}), - makeClause({neg(P(a))}) - }); + prover.addClauses({makeClause({pos(P(X))}), makeClause({neg(P(a))})}); ProverResult result = prover.prove(); EXPECT_EQ(result, ProverResult::kTheorem); @@ -112,11 +106,8 @@ TEST_F(ProverTest, RefutationWithUnification) { TEST_F(ProverTest, TwoStepRefutation) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a))}), - makeClause({neg(P(X)), pos(Q(X))}), - makeClause({neg(Q(a))}) - }); + prover.addClauses( + {makeClause({pos(P(a))}), makeClause({neg(P(X)), pos(Q(X))}), makeClause({neg(Q(a))})}); ProverResult result = prover.prove(); EXPECT_EQ(result, ProverResult::kTheorem); @@ -128,10 +119,7 @@ TEST_F(ProverTest, TwoStepRefutation) { TEST_F(ProverTest, Saturation) { Prover prover(bank, store); - prover.addClauses({ - makeClause({pos(P(a))}), - makeClause({pos(Q(b))}) - }); + prover.addClauses({makeClause({pos(P(a))}), makeClause({pos(Q(b))})}); ProverResult result = prover.prove(); EXPECT_EQ(result, ProverResult::kSaturation); @@ -147,12 +135,8 @@ TEST_F(ProverTest, Timeout) { // Need enough clauses to not saturate in 1 iteration Prover prover(bank, store, config); - prover.addClauses({ - makeClause({pos(P(X)), pos(Q(X))}), - makeClause({neg(P(a)), pos(Q(a))}), - makeClause({neg(Q(X)), pos(P(f(X)))}), - makeClause({neg(P(X)), neg(Q(X))}) - }); + prover.addClauses({makeClause({pos(P(X)), pos(Q(X))}), makeClause({neg(P(a)), pos(Q(a))}), + makeClause({neg(Q(X)), pos(P(f(X)))}), makeClause({neg(P(X)), neg(Q(X))})}); ProverResult result = prover.prove(); EXPECT_EQ(result, ProverResult::kTimeout); @@ -168,10 +152,10 @@ TEST_F(ProverTest, ThreeStepChain) { Prover prover(bank, store); prover.addClauses({ - makeClause({pos(P(a))}), // P(a) - makeClause({neg(P(X)), pos(Q(X))}), // ¬P(X) ∨ Q(X) - makeClause({neg(Q(X)), pos(S(X))}), // ¬Q(X) ∨ S(X) - makeClause({neg(S(a))}) // ¬S(a) + makeClause({pos(P(a))}), // P(a) + makeClause({neg(P(X)), pos(Q(X))}), // ¬P(X) ∨ Q(X) + makeClause({neg(Q(X)), pos(S(X))}), // ¬Q(X) ∨ S(X) + makeClause({neg(S(a))}) // ¬S(a) }); ProverResult result = prover.prove(); @@ -184,10 +168,8 @@ TEST_F(ProverTest, ThreeStepChain) { TEST_F(ProverTest, EmptyClauseInInput) { Prover prover(bank, store); - prover.addClauses({ - makeClause({}), // empty clause directly - makeClause({pos(P(a))}) - }); + prover.addClauses({makeClause({}), // empty clause directly + makeClause({pos(P(a))})}); // Empty clause should be detected immediately when selected from queue ProverResult result = prover.prove(); diff --git a/tests/test_resolution.cc b/tests/test_resolution.cc index 767e865..931635d 100644 --- a/tests/test_resolution.cc +++ b/tests/test_resolution.cc @@ -16,8 +16,6 @@ * along with this program. If not, see . */ -#include - #include "atp/core/clause.h" #include "atp/core/literal.h" #include "atp/core/symbol_table.h" @@ -27,6 +25,8 @@ #include "atp/infer/substitution.h" #include "atp/infer/unification.h" +#include + namespace atp { namespace { diff --git a/tests/test_simplify.cc b/tests/test_simplify.cc index 07875de..98b0db9 100644 --- a/tests/test_simplify.cc +++ b/tests/test_simplify.cc @@ -16,8 +16,6 @@ * along with this program. If not, see . */ -#include - #include "atp/core/clause.h" #include "atp/core/literal.h" #include "atp/core/symbol_table.h" @@ -26,6 +24,8 @@ #include "atp/simplify/subsumption.h" #include "atp/simplify/tautology.h" +#include + namespace atp { namespace { diff --git a/tests/test_term_bank.cc b/tests/test_term_bank.cc index 63acc34..3ea15ac 100644 --- a/tests/test_term_bank.cc +++ b/tests/test_term_bank.cc @@ -16,8 +16,6 @@ * along with this program. If not, see . */ -#include - #include "atp/core/clause.h" #include "atp/core/clause_store.h" #include "atp/core/literal.h" @@ -26,6 +24,8 @@ #include "atp/core/term_bank.h" #include "atp/core/types.h" +#include + namespace atp { namespace { diff --git a/tests/test_unification.cc b/tests/test_unification.cc index 3ee6f00..516058a 100644 --- a/tests/test_unification.cc +++ b/tests/test_unification.cc @@ -16,14 +16,14 @@ * along with this program. If not, see . */ -#include - #include "atp/core/symbol_table.h" #include "atp/core/term_bank.h" #include "atp/core/types.h" #include "atp/infer/substitution.h" #include "atp/infer/unification.h" +#include + namespace atp { namespace { @@ -348,8 +348,7 @@ TEST_F(UnificationTest, UnifyThenApply) { EXPECT_EQ(applySubstitution(subst, lhs, bank), P(a, f(b))); EXPECT_EQ(applySubstitution(subst, rhs, bank), P(a, f(b))); // Both sides should produce the same term after applying the MGU - EXPECT_EQ(applySubstitution(subst, lhs, bank), - applySubstitution(subst, rhs, bank)); + EXPECT_EQ(applySubstitution(subst, lhs, bank), applySubstitution(subst, rhs, bank)); } } // namespace -- cgit v1.2.3