diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-04 04:52:36 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-04 04:52:36 +0800 |
| commit | ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66 (patch) | |
| tree | 7bf8499249ae7141e9a9a938fb7241f8aeb157d6 /include/atp/search | |
| parent | 6e974168ecc487d99cbe51df569d52304907900c (diff) | |
| download | ratp-ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66.tar.gz ratp-ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66.tar.xz | |
feat: implement saturation-based resolution loop in Prover class
Diffstat (limited to 'include/atp/search')
| -rw-r--r-- | include/atp/search/prover.h | 5 |
1 files changed, 4 insertions, 1 deletions
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 |