aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/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
commit593a94a3c13aff82b31fd6c61e0ae07b97a2e426 (patch)
treee58a8954b00d412c5f5c5e80bda6b31029dbe138 /proofsearch/tests/test_proof_trace.cc
parent9a5dd39accb75618dc40b5b4f4a3c059cacf6e04 (diff)
downloadrcc-project-593a94a3c13aff82b31fd6c61e0ae07b97a2e426.tar.gz
rcc-project-593a94a3c13aff82b31fd6c61e0ae07b97a2e426.tar.xz
style: reformat codebase with consistent indentation
Diffstat (limited to 'proofsearch/tests/test_proof_trace.cc')
-rw-r--r--proofsearch/tests/test_proof_trace.cc25
1 files changed, 6 insertions, 19 deletions
diff --git a/proofsearch/tests/test_proof_trace.cc b/proofsearch/tests/test_proof_trace.cc
index d7ff246..5e12060 100644
--- a/proofsearch/tests/test_proof_trace.cc
+++ b/proofsearch/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();