aboutsummaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/test_clausifier.cc2
-rw-r--r--tests/test_discrim_tree.cc2
-rw-r--r--tests/test_end_to_end.cc9
-rw-r--r--tests/test_proof_trace.cc25
-rw-r--r--tests/test_prover.cc48
-rw-r--r--tests/test_resolution.cc4
-rw-r--r--tests/test_simplify.cc4
-rw-r--r--tests/test_term_bank.cc4
-rw-r--r--tests/test_unification.cc7
9 files changed, 34 insertions, 71 deletions
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 <https://www.gnu.org/licenses/>.
*/
-
-
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 <https://www.gnu.org/licenses/>.
*/
-
-
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 <gtest/gtest.h>
-
#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 <gtest/gtest.h>
#include <string>
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 <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();
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 <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"
@@ -26,6 +24,8 @@
#include "atp/core/types.h"
#include "atp/search/prover.h"
+#include <gtest/gtest.h>
+
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 <https://www.gnu.org/licenses/>.
*/
-#include <gtest/gtest.h>
-
#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 <gtest/gtest.h>
+
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 <https://www.gnu.org/licenses/>.
*/
-#include <gtest/gtest.h>
-
#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 <gtest/gtest.h>
+
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 <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"
@@ -26,6 +24,8 @@
#include "atp/core/term_bank.h"
#include "atp/core/types.h"
+#include <gtest/gtest.h>
+
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 <https://www.gnu.org/licenses/>.
*/
-#include <gtest/gtest.h>
-
#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 <gtest/gtest.h>
+
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
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-29 00:27:55 +0000