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 | dbd35e0081c600822a2069fd7b393e085b0c00c9 (patch) | |
| tree | 9fb1c5ffa8813f2e77ceccf5339500a3a6c11eb7 /proofsearch/include/atp/search | |
| parent | 2713bbcb4044ca18eb3071a8efea7ad097a6693b (diff) | |
| download | rcc-project-dbd35e0081c600822a2069fd7b393e085b0c00c9.tar.gz rcc-project-dbd35e0081c600822a2069fd7b393e085b0c00c9.tar.xz | |
feat: implement saturation-based resolution loop in Prover class
Diffstat (limited to 'proofsearch/include/atp/search')
| -rw-r--r-- | proofsearch/include/atp/search/prover.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h index 308e044..d84a647 100644 --- a/proofsearch/include/atp/search/prover.h +++ b/proofsearch/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 |