aboutsummaryrefslogtreecommitdiff
path: root/tests/test_proof_trace.cc
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-04 05:21:26 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-04 05:21:26 +0800
commitbf4f464cec8b6515d9e5131d43847ef9b2fd21d1 (patch)
tree8cff611e6dab7473c3bb601e58658fa44f0fd86f /tests/test_proof_trace.cc
parent6fac8eb886f1e60a5a075c48a5f7648bb537f74e (diff)
downloadratp-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.cc25
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();