diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-04 05:21:26 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-04 05:21:26 +0800 |
| commit | bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 (patch) | |
| tree | 8cff611e6dab7473c3bb601e58658fa44f0fd86f /tests/test_proof_trace.cc | |
| parent | 6fac8eb886f1e60a5a075c48a5f7648bb537f74e (diff) | |
| download | ratp-bf4f464cec8b6515d9e5131d43847ef9b2fd21d1.tar.gz ratp-bf4f464cec8b6515d9e5131d43847ef9b2fd21d1.tar.xz | |
style: reformat codebase with consistent indentation
Diffstat (limited to 'tests/test_proof_trace.cc')
| -rw-r--r-- | tests/test_proof_trace.cc | 25 |
1 files changed, 6 insertions, 19 deletions
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 <https://www.gnu.org/licenses/>. */ -#include <gtest/gtest.h> - #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 <gtest/gtest.h> #include <string> 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(); |
