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 | |
| 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')
| -rw-r--r-- | include/atp/infer/resolution.h | 11 | ||||
| -rw-r--r-- | include/atp/search/prover.h | 5 |
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 |