From ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Sat, 4 Apr 2026 04:52:36 +0800
Subject: feat: implement saturation-based resolution loop in Prover class

---
 include/atp/infer/resolution.h | 11 ++++++++---
 include/atp/search/prover.h    |  5 ++++-
 2 files changed, 12 insertions(+), 4 deletions(-)

(limited to 'include')

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
-- 
cgit v1.2.3