feat: implement saturation-based resolution loop in Prover class

2 files changed, 12 insertions, 4 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