From ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 04:52:36 +0800 Subject: feat: implement saturation-based resolution loop in Prover class --- include/atp/infer/resolution.h | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) (limited to 'include/atp/infer/resolution.h') 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 #include +#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 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 allResolvents(TermBank& bank, const Clause& c1, const Clause& c2); +std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, + const UnificationConfig& uconfig = {}); /// Attempt factoring on a single clause (merge two unifiable literals). -std::vector factor(TermBank& bank, const Clause& c); +std::vector 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. -- cgit v1.2.3