Merge remote-tracking branch 'proofsearch-import/master'

1 files changed, 183 insertions, 0 deletions

diff --git a/proofsearch/tests/test_prover.cc b/proofsearch/tests/test_prover.cc
new file mode 100644
index 0000000..74d02ad
--- /dev/null
+++ b/proofsearch/tests/test_prover.cc
@@ -0,0 +1,183 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/search/prover.h"
+
+#include <gtest/gtest.h>
+#include <utility>
+#include <vector>
+
+namespace atp {
+namespace {
+
+class ProverTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols_;
+    TermBank bank_{symbols_};
+    ClauseStore store_;
+
+    SymbolId sym_a_{}, sym_b_{};
+    SymbolId sym_f_{};
+    SymbolId sym_p_{}, sym_q_{}, sym_r_{};
+    SymbolId sym_x_{}, sym_y_{};
+
+    TermId a_{}, b_{}, x_{}, y_{};
+
+
+    void SetUp() override {
+        sym_a_ = symbols_.intern("a", SymbolKind::kConstant);
+        sym_b_ = symbols_.intern("b", SymbolKind::kConstant);
+        sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1);
+        sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1);
+        sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1);
+        sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2);
+        sym_x_ = symbols_.intern("X", SymbolKind::kVariable);
+        sym_y_ = symbols_.intern("Y", SymbolKind::kVariable);
+
+        a_ = bank_.makeTerm(sym_a_, {});
+        b_ = bank_.makeTerm(sym_b_, {});
+        x_ = bank_.makeVar(sym_x_);
+        y_ = bank_.makeVar(sym_y_);
+    }
+
+    TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); }
+    TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); }
+    TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); }
+    TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); }
+
+    static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; }
+    static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; }
+
+    static Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals_ = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Trivial refutation: {P(a)} and {¬P(a)} → empty clause
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, TrivialRefutation) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({neg(p(a_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+    EXPECT_TRUE(prover.getEmptyClauseId().has_value());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Unification required: {P(X)} and {¬P(a)} → empty clause
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, RefutationWithUnification) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(x_))}), makeClause({neg(p(a_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Multi-step: {P(a)}, {¬P(X), Q(X)}, {¬Q(a)}
+// Step 1: resolve P(a) with ¬P(X)∨Q(X) → Q(a)
+// Step 2: resolve Q(a) with ¬Q(a) → empty
+// ═══════════════════════════════════════════════════════════════════════════
+
+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_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Saturation: {P(a)}, {Q(b)} — no complementary literals
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, Saturation) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({pos(p(a_))}), makeClause({pos(q(b_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kSaturation);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Timeout: set very low limits
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, Timeout) {
+    ProverConfig config;
+    config.max_iterations_ = 1;
+
+    // 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_))})});
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTimeout);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Chain reasoning: P(a), ¬P(X)∨Q(X), ¬Q(X)∨R(X), ¬R(a)
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, ThreeStepChain) {
+    const SymbolId kSymS = symbols_.intern("S", SymbolKind::kPredicate, 1);
+    auto s = [&](TermId arg) { return bank_.makeTerm(kSymS, {{arg}}); };
+
+    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)
+    });
+
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Empty clause in input directly
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, EmptyClauseInInput) {
+    Prover prover(bank_, store_);
+    prover.addClauses({makeClause({}),  // empty clause directly
+                       makeClause({pos(p(a_))})});
+
+    // Empty clause should be detected immediately when selected from queue
+    const ProverResult kResult = prover.prove();
+    EXPECT_EQ(kResult, ProverResult::kTheorem);
+}
+
+}  // namespace
+}  // namespace atp