feat: implement saturation-based resolution loop in Prover class

5 files changed, 349 insertions, 10 deletions

diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h
index c31ff0e..df9cab3 100644
--- a/include/atp/infer/resolution.h
+++ b/include/atp/infer/resolution.h
@@ -28,18 +28,23 @@
 #include <optional>
 #include <vector>
 
+#include "atp/infer/unification.h"
+
 namespace atp {
 
 /// Attempt binary resolution between two clauses on the specified literal indices.
 /// @return The resolvent clause if resolution succeeds, std::nullopt otherwise.
 std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
-                              const Clause& c2, size_t lit_idx2);
+                              const Clause& c2, size_t lit_idx2,
+                              const UnificationConfig& uconfig = {});
 
 /// Generate all possible resolvents between two clauses.
-std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2);
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
+                                  const UnificationConfig& uconfig = {});
 
 /// Attempt factoring on a single clause (merge two unifiable literals).
-std::vector<Clause> factor(TermBank& bank, const Clause& c);
+std::vector<Clause> factor(TermBank& bank, const Clause& c,
+                           const UnificationConfig& uconfig = {});
 
 /// Rename all variables in a clause to fresh ones, avoiding conflicts
 /// with variables already in the bank.
diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h
index 308e044..d84a647 100644
--- a/include/atp/search/prover.h
+++ b/include/atp/search/prover.h
@@ -32,6 +32,7 @@
 #include "atp/search/clause_queue.h"
 
 #include <optional>
+#include <queue>
 #include <vector>
 
 namespace atp {
@@ -75,7 +76,9 @@ class Prover {
     TermBank& bank_;
     ClauseStore& store_;
     ProverConfig config_;
-    // TODO: Phase 5 implementation — Unprocessed queue + Processed set
+    std::priority_queue<Clause, std::vector<Clause>, ClauseComparator> unprocessed_;
+    std::vector<ClauseId> processed_;
+    std::optional<ClauseId> empty_clause_id_;
 };
 
 }  // namespace atp
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index 89be520..3c82460 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -85,7 +85,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
 }
 
 std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
-                              const Clause& c2, size_t lit_idx2) {
+                              const Clause& c2, size_t lit_idx2,
+                              const UnificationConfig& uconfig) {
     // Must have opposite polarity
     if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) {
         return std::nullopt;
@@ -99,7 +100,7 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
 
     // Unify the complementary atoms
     Substitution subst;
-    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst)) {
+    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst, uconfig)) {
         return std::nullopt;
     }
 
@@ -126,12 +127,13 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
     return resolvent;
 }
 
-std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2) {
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
+                                  const UnificationConfig& uconfig) {
     std::vector<Clause> results;
     for (size_t i = 0; i < c1.literals.size(); ++i) {
         for (size_t j = 0; j < c2.literals.size(); ++j) {
             if (c1.literals[i].is_positive != c2.literals[j].is_positive) {
-                if (auto r = resolve(bank, c1, i, c2, j)) {
+                if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
                     results.push_back(std::move(*r));
                 }
             }
@@ -140,7 +142,8 @@ std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause
     return results;
 }
 
-std::vector<Clause> factor(TermBank& bank, const Clause& c) {
+std::vector<Clause> factor(TermBank& bank, const Clause& c,
+                           const UnificationConfig& uconfig) {
     std::vector<Clause> results;
     for (size_t i = 0; i < c.literals.size(); ++i) {
         for (size_t j = i + 1; j < c.literals.size(); ++j) {
@@ -148,7 +151,7 @@ std::vector<Clause> factor(TermBank& bank, const Clause& c) {
                 continue;  // Must have same polarity
             }
             Substitution subst;
-            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst)) {
+            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst, uconfig)) {
                 continue;
             }
             // Build factored clause: drop literal j, apply subst to all
diff --git a/src/search/prover.cc b/src/search/prover.cc
index b62ffd0..844f6c1 100644
--- a/src/search/prover.cc
+++ b/src/search/prover.cc
@@ -16,4 +16,153 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include "atp/search/prover.h"
+#include "atp/core/types.h"
+#include "atp/infer/resolution.h"
+#include "atp/infer/unification.h"
+#include "atp/simplify/subsumption.h"
+#include "atp/simplify/tautology.h"
 
+#include <algorithm>
+
+namespace atp {
+
+Prover::Prover(TermBank& bank, ClauseStore& store, ProverConfig config)
+    : bank_(bank),
+      store_(store),
+      config_(std::move(config)),
+      unprocessed_(config_.comparator) {}
+
+void Prover::addClauses(std::vector<Clause> clauses) {
+    for (auto& clause : clauses) {
+        clause.depth = 0;
+        ClauseId id = store_.addClause(clause);
+        unprocessed_.push(store_.getClause(id));
+    }
+}
+
+ProverResult Prover::prove() {
+    size_t iterations = 0;
+
+    while (!unprocessed_.empty()) {
+        // ─── Resource limits ──────────────────────────────────────────
+        if (iterations >= config_.max_iterations ||
+            store_.size() >= config_.max_clauses) {
+            return ProverResult::kTimeout;
+        }
+        ++iterations;
+
+        // ─── 1. Select the best clause from unprocessed ──────────────
+        Clause given = unprocessed_.top();
+        unprocessed_.pop();
+
+        // ─── 2. Check if given is itself the empty clause ────────────
+        if (given.isEmpty()) {
+            empty_clause_id_ = given.id;
+            return ProverResult::kTheorem;
+        }
+
+        // ─── 3. Forward redundancy checks ────────────────────────────
+        if (isTautology(given)) {
+            continue;
+        }
+
+        bool forward_subsumed = false;
+        for (ClauseId pid : processed_) {
+            if (subsumes(store_.getClause(pid), given)) {
+                forward_subsumed = true;
+                break;
+            }
+        }
+        if (forward_subsumed) {
+            continue;
+        }
+
+        // ─── 4. Backward subsumption ─────────────────────────────────
+        // Remove from processed all clauses that are subsumed by given.
+        // Use erase-remove idiom for O(n) scan instead of repeated erase.
+        std::erase_if(processed_, [&](ClauseId pid) {
+            return subsumes(given, store_.getClause(pid));
+        });
+
+        // ─── 5. Generate new clauses ─────────────────────────────────
+        // Inference BEFORE adding given to processed — matches doc §4.6.
+        std::vector<Clause> new_clauses;
+        const UnificationConfig uconfig{.enable_occurs_check = config_.enable_occurs_check};
+
+        // 5a. Resolve given with every processed clause (both directions)
+        for (ClauseId pid : processed_) {
+            const Clause& pc = store_.getClause(pid);
+
+            auto resolvents1 = allResolvents(bank_, given, pc, uconfig);
+            auto resolvents2 = allResolvents(bank_, pc, given, uconfig);
+
+            for (auto& r : resolvents1) {
+                new_clauses.push_back(std::move(r));
+            }
+            for (auto& r : resolvents2) {
+                new_clauses.push_back(std::move(r));
+            }
+        }
+
+        // 5b. Factor given (only once)
+        auto factors = factor(bank_, given, uconfig);
+        for (auto& f : factors) {
+            new_clauses.push_back(std::move(f));
+        }
+
+        // ─── 6. Add given to processed AFTER inference ───────────────
+        processed_.push_back(given.id);
+
+        // ─── 7. Process new clauses ──────────────────────────────────
+        for (auto& nc : new_clauses) {
+            // 7a. Check for empty clause → proof found!
+            if (nc.isEmpty()) {
+                ClauseId eid = store_.addClause(std::move(nc));
+                empty_clause_id_ = eid;
+                return ProverResult::kTheorem;
+            }
+
+            // 7b. Skip tautologies
+            if (isTautology(nc)) {
+                continue;
+            }
+
+            // 7c. Set depth
+            uint32_t d1 = (nc.parent1 != kInvalidId)
+                              ? store_.getClause(nc.parent1).depth
+                              : 0;
+            uint32_t d2 = (nc.parent2 != kInvalidId)
+                              ? store_.getClause(nc.parent2).depth
+                              : 0;
+            nc.depth = static_cast<uint16_t>(std::max(d1, d2) + 1);
+
+            // 7d. Store the clause (needed for forward subsumption check)
+            ClauseId nid = store_.addClause(nc);
+            const Clause& stored_nc = store_.getClause(nid);
+
+            // 7e. Forward subsumption on new clause
+            bool new_subsumed = false;
+            for (ClauseId pid : processed_) {
+                if (subsumes(store_.getClause(pid), stored_nc)) {
+                    new_subsumed = true;
+                    break;
+                }
+            }
+            if (new_subsumed) {
+                continue;
+            }
+
+            // 7f. Enqueue
+            unprocessed_.push(stored_nc);
+        }
+    }
+
+    return ProverResult::kSaturation;
+}
+
+std::optional<ClauseId> Prover::getEmptyClauseId() const {
+    return empty_clause_id_;
+}
+
+}  // namespace atp
\ No newline at end of file
diff --git a/tests/test_prover.cc b/tests/test_prover.cc
index b62ffd0..cec1c35 100644
--- a/tests/test_prover.cc
+++ b/tests/test_prover.cc
@@ -16,4 +16,183 @@
  * 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"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/search/prover.h"
+
+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}}); }
+
+    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
+    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+
+    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))})
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, 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))})
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, 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))})
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, 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))})
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, 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))})
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, ProverResult::kTimeout);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Chain reasoning: P(a), ¬P(X)∨Q(X), ¬Q(X)∨R(X), ¬R(a)
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProverTest, ThreeStepChain) {
+    SymbolId sym_S = symbols.intern("S", SymbolKind::kPredicate, 1);
+    auto S = [&](TermId arg) { return bank.makeTerm(sym_S, {{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)
+    });
+
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, 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
+    ProverResult result = prover.prove();
+    EXPECT_EQ(result, ProverResult::kTheorem);
+}
+
+}  // namespace
+}  // namespace atp