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/search/prover.h | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'include/atp/search/prover.h')

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