feat: implement variable renaming and update resolution logic to prevent variable collisions

3 files changed, 399 insertions, 3 deletions

diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h
index 2d73b06..c31ff0e 100644
--- a/include/atp/infer/resolution.h
+++ b/include/atp/infer/resolution.h
@@ -32,13 +32,19 @@ 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(const TermBank& bank, const Clause& c1, size_t lit_idx1,
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
                               const Clause& c2, size_t lit_idx2);
 
 /// Generate all possible resolvents between two clauses.
-std::vector<Clause> allResolvents(const TermBank& bank, const Clause& c1, const Clause& c2);
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2);
 
 /// Attempt factoring on a single clause (merge two unifiable literals).
-std::vector<Clause> factor(const TermBank& bank, const Clause& c);
+std::vector<Clause> factor(TermBank& bank, const Clause& c);
+
+/// Rename all variables in a clause to fresh ones, avoiding conflicts
+/// with variables already in the bank.
+Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
+                       uint32_t& next_var_id);
+
 
 }  // namespace atp
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index b62ffd0..89be520 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -16,4 +16,156 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include "atp/infer/resolution.h"
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/substitution.h"
+#include "atp/infer/unification.h"
 
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+namespace atp {
+
+namespace {
+
+/// Recursively collect all variable TermIds appearing in a term.
+void collectVariables(TermId term, const TermBank& bank,
+                      std::unordered_map<TermId, bool>& seen) {
+    if (bank.isVariable(term)) {
+        seen[term] = true;
+        return;
+    }
+    // Copy args to avoid dangling ref (bank is const here, but be safe)
+    const Term& t = bank.getTerm(term);
+    for (TermId arg : t.args) {
+        collectVariables(arg, bank, seen);
+    }
+}
+
+}  // namespace
+
+Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
+                       uint32_t& next_var_id) {
+    // 1. Collect all variables in the clause
+    std::unordered_map<TermId, bool> var_set;
+    for (const auto& lit : c.literals) {
+        collectVariables(lit.atom, bank, var_set);
+    }
+
+    if (var_set.empty()) {
+        return c;  // Ground clause — nothing to rename
+    }
+
+    // 2. Create fresh variables and build a substitution
+    Substitution rename_subst;
+    for (auto& [old_var_id, _] : var_set) {
+        std::string fresh_name = "_R" + std::to_string(next_var_id++);
+        SymbolId fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
+        TermId fresh_var = bank.makeVar(fresh_sym);
+        rename_subst.bind(old_var_id, fresh_var);
+    }
+
+    // 3. Apply the renaming substitution to all literals
+    Clause renamed;
+    renamed.id = c.id;
+    renamed.rule = c.rule;
+    renamed.parent1 = c.parent1;
+    renamed.parent2 = c.parent2;
+    renamed.depth = c.depth;
+    for (const auto& lit : c.literals) {
+        TermId new_atom = applySubstitution(rename_subst, lit.atom, bank);
+        renamed.literals.push_back({.atom = new_atom, .is_positive = lit.is_positive});
+    }
+    return renamed;
+}
+
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
+                              const Clause& c2, size_t lit_idx2) {
+    // Must have opposite polarity
+    if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) {
+        return std::nullopt;
+    }
+
+    // Rename c2's variables to avoid clashes with c1
+    // Use a static counter — safe for single-threaded prover
+    static uint32_t var_counter = 0;
+    auto& symbols = const_cast<SymbolTable&>(bank.symbols());
+    Clause c2r = renameVariables(c2, bank, symbols, var_counter);
+
+    // Unify the complementary atoms
+    Substitution subst;
+    if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst)) {
+        return std::nullopt;
+    }
+
+    // Build the resolvent: all literals except the resolved pair, with subst applied
+    Clause resolvent;
+    resolvent.rule = InferenceRule::kResolution;
+    resolvent.parent1 = c1.id;
+    resolvent.parent2 = c2.id;
+
+    for (size_t i = 0; i < c1.literals.size(); ++i) {
+        if (i != lit_idx1) {
+            TermId new_atom = applySubstitution(subst, c1.literals[i].atom, bank);
+            resolvent.literals.push_back(
+                {.atom = new_atom, .is_positive = c1.literals[i].is_positive});
+        }
+    }
+    for (size_t i = 0; i < c2r.literals.size(); ++i) {
+        if (i != lit_idx2) {
+            TermId new_atom = applySubstitution(subst, c2r.literals[i].atom, bank);
+            resolvent.literals.push_back(
+                {.atom = new_atom, .is_positive = c2r.literals[i].is_positive});
+        }
+    }
+    return resolvent;
+}
+
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2) {
+    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)) {
+                    results.push_back(std::move(*r));
+                }
+            }
+        }
+    }
+    return results;
+}
+
+std::vector<Clause> factor(TermBank& bank, const Clause& c) {
+    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) {
+            if (c.literals[i].is_positive != c.literals[j].is_positive) {
+                continue;  // Must have same polarity
+            }
+            Substitution subst;
+            if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst)) {
+                continue;
+            }
+            // Build factored clause: drop literal j, apply subst to all
+            Clause factored;
+            factored.rule = InferenceRule::kFactoring;
+            factored.parent1 = c.id;
+            for (size_t k = 0; k < c.literals.size(); ++k) {
+                if (k != j) {
+                    TermId new_atom = applySubstitution(subst, c.literals[k].atom, bank);
+                    factored.literals.push_back(
+                        {.atom = new_atom, .is_positive = c.literals[k].is_positive});
+                }
+            }
+            results.push_back(std::move(factored));
+        }
+    }
+    return results;
+}
+
+}  // namespace atp
diff --git a/tests/test_resolution.cc b/tests/test_resolution.cc
index b62ffd0..767e865 100644
--- a/tests/test_resolution.cc
+++ b/tests/test_resolution.cc
@@ -16,4 +16,242 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include <gtest/gtest.h>
 
+#include "atp/core/clause.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/resolution.h"
+#include "atp/infer/substitution.h"
+#include "atp/infer/unification.h"
+
+namespace atp {
+namespace {
+
+class ResolutionTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols;
+    TermBank bank{symbols};
+
+    SymbolId sym_a{}, sym_b{}, sym_c{};
+    SymbolId sym_f{};
+    SymbolId sym_P{}, sym_Q{}, sym_R{};
+    SymbolId sym_X{}, sym_Y{}, sym_Z{};
+
+    TermId a{}, b{}, c{};
+    TermId X{}, Y{}, Z{};
+
+    void SetUp() override {
+        sym_a = symbols.intern("a", SymbolKind::kConstant);
+        sym_b = symbols.intern("b", SymbolKind::kConstant);
+        sym_c = symbols.intern("c", SymbolKind::kConstant);
+        sym_f = symbols.intern("f", SymbolKind::kFunction, 1);
+        sym_P = symbols.intern("P", SymbolKind::kPredicate, 1);
+        sym_Q = symbols.intern("Q", SymbolKind::kPredicate, 1);
+        sym_R = symbols.intern("R", SymbolKind::kPredicate, 2);
+        sym_X = symbols.intern("X", SymbolKind::kVariable);
+        sym_Y = symbols.intern("Y", SymbolKind::kVariable);
+        sym_Z = symbols.intern("Z", SymbolKind::kVariable);
+
+        a = bank.makeTerm(sym_a, {});
+        b = bank.makeTerm(sym_b, {});
+        c = bank.makeTerm(sym_c, {});
+        X = bank.makeVar(sym_X);
+        Y = bank.makeVar(sym_Y);
+        Z = bank.makeVar(sym_Z);
+    }
+
+    TermId P(TermId arg) { return bank.makeTerm(sym_P, {{arg}}); }
+    TermId Q(TermId arg) { return bank.makeTerm(sym_Q, {{arg}}); }
+    TermId R(TermId a1, TermId a2) { return bank.makeTerm(sym_R, {{a1, a2}}); }
+    TermId f(TermId arg) { return bank.makeTerm(sym_f, {{arg}}); }
+
+    // Helper: make a clause from literals
+    Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) {
+        Clause c;
+        c.id = id;
+        c.literals = std::move(lits);
+        return c;
+    }
+
+    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
+    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Basic Resolution Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, SimpleGroundResolution) {
+    // {P(a)} and {¬P(a), Q(b)}  → {Q(b)}
+    Clause c1 = makeClause({pos(P(a))}, 0);
+    Clause c2 = makeClause({neg(P(a)), pos(Q(b))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals.size(), 1);
+    EXPECT_EQ(result->literals[0].atom, Q(b));
+    EXPECT_TRUE(result->literals[0].is_positive);
+}
+
+TEST_F(ResolutionTest, ResolutionWithUnification) {
+    // {P(X)} and {¬P(a)} → {} (empty clause!)
+    Clause c1 = makeClause({pos(P(X))}, 0);
+    Clause c2 = makeClause({neg(P(a))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_TRUE(result->isEmpty()) << "Should derive empty clause (contradiction)";
+}
+
+TEST_F(ResolutionTest, ResolutionFailsSamePolarity) {
+    // {P(a)} and {P(b)} → no resolution (both positive)
+    Clause c1 = makeClause({pos(P(a))}, 0);
+    Clause c2 = makeClause({pos(P(b))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    EXPECT_FALSE(result.has_value());
+}
+
+TEST_F(ResolutionTest, ResolutionFailsNoUnifier) {
+    // {P(a)} and {¬P(b)} → can't unify a with b
+    Clause c1 = makeClause({pos(P(a))}, 0);
+    Clause c2 = makeClause({neg(P(b))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    EXPECT_FALSE(result.has_value());
+}
+
+TEST_F(ResolutionTest, ResolutionAppliesSubstToRemainingLiterals) {
+    // {P(X), Q(X)} and {¬P(a)} → {Q(a)}
+    Clause c1 = makeClause({pos(P(X)), pos(Q(X))}, 0);
+    Clause c2 = makeClause({neg(P(a))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals.size(), 1);
+    EXPECT_EQ(result->literals[0].atom, Q(a));
+}
+
+TEST_F(ResolutionTest, ResolutionMultipleLiterals) {
+    // {P(X), Q(b)} and {¬P(a), R(a, c)} → {Q(b), R(a, c)}
+    Clause c1 = makeClause({pos(P(X)), pos(Q(b))}, 0);
+    Clause c2 = makeClause({neg(P(a)), pos(R(a, c))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals.size(), 2);
+}
+
+TEST_F(ResolutionTest, VariableRenamingWorks) {
+    // Both clauses use variable X
+    // {P(X)} and {¬P(X), Q(X)} → {Q(a)} only if X is renamed in c2
+    Clause c1 = makeClause({pos(P(a))}, 0);
+    Clause c2 = makeClause({neg(P(X)), pos(Q(X))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->literals.size(), 1);
+    // Q(X) should become Q(a) after substitution {X→a}
+    EXPECT_EQ(result->literals[0].atom, Q(a));
+}
+
+TEST_F(ResolutionTest, VariableRenamingPreventsClash) {
+    // {R(X, a)} and {¬R(b, X)}
+    // Without renaming: X would clash between c1 and c2
+    // With renaming: c2's X → _R0, then unify R(X,a) with R(b,_R0) → {X→b, _R0→a}
+    Clause c1 = makeClause({pos(R(X, a))}, 0);
+    Clause c2 = makeClause({neg(R(b, X))}, 1);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_TRUE(result->isEmpty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// AllResolvents Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, AllResolventsFindsAll) {
+    // {P(a), Q(a)} and {¬P(a), ¬Q(a)}
+    // Can resolve on P or Q → 2 resolvents
+    Clause c1 = makeClause({pos(P(a)), pos(Q(a))}, 0);
+    Clause c2 = makeClause({neg(P(a)), neg(Q(a))}, 1);
+
+    auto results = allResolvents(bank, c1, c2);
+    EXPECT_EQ(results.size(), 2);
+}
+
+TEST_F(ResolutionTest, AllResolventsEmpty) {
+    // {P(a)} and {Q(b)} → no complementary pairs
+    Clause c1 = makeClause({pos(P(a))}, 0);
+    Clause c2 = makeClause({pos(Q(b))}, 1);
+
+    auto results = allResolvents(bank, c1, c2);
+    EXPECT_TRUE(results.empty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Factoring Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, SimpleFactoring) {
+    // {P(X), P(a), Q(X)} → factor P(X) with P(a): {P(a), Q(a)}
+    Clause c = makeClause({pos(P(X)), pos(P(a)), pos(Q(X))}, 0);
+
+    auto results = factor(bank, c);
+    ASSERT_EQ(results.size(), 1);
+    EXPECT_EQ(results[0].literals.size(), 2);
+    // After factoring: {P(a), Q(a)}
+    EXPECT_EQ(results[0].literals[0].atom, P(a));
+    EXPECT_EQ(results[0].literals[1].atom, Q(a));
+}
+
+TEST_F(ResolutionTest, NoFactoring) {
+    // {P(a), Q(b)} → different predicates, can't factor
+    Clause c = makeClause({pos(P(a)), pos(Q(b))}, 0);
+    auto results = factor(bank, c);
+    EXPECT_TRUE(results.empty());
+}
+
+TEST_F(ResolutionTest, FactoringDifferentPolarity) {
+    // {P(a), ¬P(a)} → different polarity, can't factor
+    Clause c = makeClause({pos(P(a)), neg(P(a))}, 0);
+    auto results = factor(bank, c);
+    EXPECT_TRUE(results.empty());
+}
+
+TEST_F(ResolutionTest, FactoringNonUnifiable) {
+    // {P(a), P(b)} → can't unify a with b
+    Clause c = makeClause({pos(P(a)), pos(P(b))}, 0);
+    auto results = factor(bank, c);
+    EXPECT_TRUE(results.empty());
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Provenance Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ResolutionTest, ResolventHasProvenance) {
+    Clause c1 = makeClause({pos(P(X))}, 5);
+    Clause c2 = makeClause({neg(P(a))}, 7);
+
+    auto result = resolve(bank, c1, 0, c2, 0);
+    ASSERT_TRUE(result.has_value());
+    EXPECT_EQ(result->rule, InferenceRule::kResolution);
+    EXPECT_EQ(result->parent1, 5);
+    EXPECT_EQ(result->parent2, 7);
+}
+
+TEST_F(ResolutionTest, FactoredHasProvenance) {
+    Clause c = makeClause({pos(P(X)), pos(P(a))}, 3);
+    auto results = factor(bank, c);
+    ASSERT_FALSE(results.empty());
+    EXPECT_EQ(results[0].rule, InferenceRule::kFactoring);
+    EXPECT_EQ(results[0].parent1, 3);
+}
+
+}  // namespace
+}  // namespace atp