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

---
 src/infer/resolution.cc | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'src/infer/resolution.cc')

diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index 89be520..3c82460 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -85,7 +85,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
 }
 
 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) {
     // Must have opposite polarity
     if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) {
         return std::nullopt;
@@ -99,7 +100,7 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
 
     // Unify the complementary atoms
     Substitution subst;
-    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst)) {
+    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst, uconfig)) {
         return std::nullopt;
     }
 
@@ -126,12 +127,13 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
     return resolvent;
 }
 
-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) {
     std::vector<Clause> results;
     for (size_t i = 0; i < c1.literals.size(); ++i) {
         for (size_t j = 0; j < c2.literals.size(); ++j) {
             if (c1.literals[i].is_positive != c2.literals[j].is_positive) {
-                if (auto r = resolve(bank, c1, i, c2, j)) {
+                if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
                     results.push_back(std::move(*r));
                 }
             }
@@ -140,7 +142,8 @@ std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause
     return results;
 }
 
-std::vector<Clause> factor(TermBank& bank, const Clause& c) {
+std::vector<Clause> factor(TermBank& bank, const Clause& c,
+                           const UnificationConfig& uconfig) {
     std::vector<Clause> results;
     for (size_t i = 0; i < c.literals.size(); ++i) {
         for (size_t j = i + 1; j < c.literals.size(); ++j) {
@@ -148,7 +151,7 @@ std::vector<Clause> factor(TermBank& bank, const Clause& c) {
                 continue;  // Must have same polarity
             }
             Substitution subst;
-            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst)) {
+            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst, uconfig)) {
                 continue;
             }
             // Build factored clause: drop literal j, apply subst to all
-- 
cgit v1.2.3