diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/test_unification.cc | 337 |
1 files changed, 337 insertions, 0 deletions
diff --git a/tests/test_unification.cc b/tests/test_unification.cc index b62ffd0..3ee6f00 100644 --- a/tests/test_unification.cc +++ b/tests/test_unification.cc @@ -16,4 +16,341 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. */ +#include <gtest/gtest.h> +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" +#include "atp/infer/unification.h" + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// Test Fixture +// ═══════════════════════════════════════════════════════════════════════════ + +class UnificationTest : public ::testing::Test { + protected: + SymbolTable symbols; + TermBank bank{symbols}; + + // Symbols + SymbolId sym_a{}, sym_b{}, sym_c{}; + SymbolId sym_f{}, sym_g{}, sym_h{}; + SymbolId sym_P{}; + SymbolId sym_X{}, sym_Y{}, sym_Z{}; + + // Terms (created in SetUp) + 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_g = symbols.intern("g", SymbolKind::kFunction, 2); + sym_h = symbols.intern("h", SymbolKind::kFunction, 1); + sym_P = symbols.intern("P", 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); + } + + // Helper: make f(arg) + TermId f(TermId arg) { return bank.makeTerm(sym_f, {{arg}}); } + // Helper: make g(arg1, arg2) + TermId g(TermId a1, TermId a2) { return bank.makeTerm(sym_g, {{a1, a2}}); } + // Helper: make h(arg) + TermId h(TermId arg) { return bank.makeTerm(sym_h, {{arg}}); } + // Helper: make P(arg1, arg2) + TermId P(TermId a1, TermId a2) { return bank.makeTerm(sym_P, {{a1, a2}}); } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Substitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, SubstBindAndLookup) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_EQ(subst.lookup(X), a); + EXPECT_EQ(subst.lookup(Y), kInvalidId); // unbound +} + +TEST_F(UnificationTest, SubstBindSameTermSucceeds) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_TRUE(subst.bind(X, a)); // same binding → OK +} + +TEST_F(UnificationTest, SubstBindDifferentTermFails) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_FALSE(subst.bind(X, b)); // different binding → fail +} + +TEST_F(UnificationTest, SubstResolveChain) { + // X → Y → a + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, SubstResolveUnbound) { + Substitution subst; + EXPECT_EQ(subst.resolve(X, bank), X); // unbound → returns itself +} + +TEST_F(UnificationTest, SubstResolveNonVariable) { + Substitution subst; + EXPECT_EQ(subst.resolve(a, bank), a); // constant → returns itself +} + +TEST_F(UnificationTest, SubstApplySimple) { + // σ = {X → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, a); + TermId fx = f(X); + TermId result = subst.apply(fx, bank); + TermId expected = f(a); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyLeavesUnbound) { + // σ = {X → a} apply to g(X, Y) → g(a, Y) + Substitution subst; + subst.bind(X, a); + TermId gxy = g(X, Y); + TermId result = subst.apply(gxy, bank); + TermId expected = g(a, Y); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyNested) { + // σ = {X → f(a)} apply to g(X, b) → g(f(a), b) + Substitution subst; + subst.bind(X, f(a)); + TermId result = subst.apply(g(X, b), bank); + EXPECT_EQ(result, g(f(a), b)); +} + +TEST_F(UnificationTest, SubstOccursIn) { + Substitution subst; + // X occurs in f(X) + EXPECT_TRUE(subst.occursIn(X, f(X), bank)); + // X occurs in g(a, f(X)) + EXPECT_TRUE(subst.occursIn(X, g(a, f(X)), bank)); + // X does NOT occur in f(a) + EXPECT_FALSE(subst.occursIn(X, f(a), bank)); + // X does NOT occur in Y (different variable) + EXPECT_FALSE(subst.occursIn(X, Y, bank)); +} + +TEST_F(UnificationTest, SubstClearAndSize) { + Substitution subst; + EXPECT_TRUE(subst.empty()); + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(subst.size(), 2); + subst.clear(); + EXPECT_TRUE(subst.empty()); + EXPECT_EQ(subst.lookup(X), kInvalidId); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Unification Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, UnifyIdenticalConstants) { + Substitution subst; + EXPECT_TRUE(unify(bank, a, a, subst)); + EXPECT_TRUE(subst.empty()); +} + +TEST_F(UnificationTest, UnifyDifferentConstants) { + Substitution subst; + EXPECT_FALSE(unify(bank, a, b, subst)); +} + +TEST_F(UnificationTest, UnifyVarWithConstant) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, a, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyConstantWithVar) { + // Symmetric: unify(a, X) should also work + Substitution subst; + EXPECT_TRUE(unify(bank, a, X, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyTwoVariables) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, Y, subst)); + // One should be bound to the other + TermId rx = subst.resolve(X, bank); + TermId ry = subst.resolve(Y, bank); + EXPECT_EQ(rx, ry); +} + +TEST_F(UnificationTest, UnifyCompoundTerms) { + // f(X) =? f(a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(X), f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyMultipleArgs) { + // g(X, Y) =? g(a, b) → {X → a, Y → b} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(a, b), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), b); +} + +TEST_F(UnificationTest, UnifyConflictingBindings) { + // g(X, X) =? g(a, b) → fails (X can't be both a and b) + Substitution subst; + EXPECT_FALSE(unify(bank, g(X, X), g(a, b), subst)); +} + +TEST_F(UnificationTest, UnifyConsistentRepeatedVar) { + // g(X, X) =? g(a, a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, X), g(a, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyDifferentHeadSymbols) { + // f(X) =? h(X) → fails + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), h(X), subst)); +} + +TEST_F(UnificationTest, UnifyDifferentArity) { + // f(X) =? g(X, Y) → fails (arity 1 vs 2) + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), g(X, Y), subst)); +} + +TEST_F(UnificationTest, UnifyNestedTerms) { + // f(g(X, a)) =? f(Y) → {Y → g(X, a)} + Substitution subst; + EXPECT_TRUE(unify(bank, f(g(X, a)), f(Y), subst)); + EXPECT_EQ(subst.resolve(Y, bank), g(X, a)); +} + +TEST_F(UnificationTest, UnifyVarWithCompound) { + // X =? f(a) → {X → f(a)} + Substitution subst; + EXPECT_TRUE(unify(bank, X, f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), f(a)); +} + +TEST_F(UnificationTest, UnifyDeepNesting) { + // f(f(f(X))) =? f(f(f(a))) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(f(f(X))), f(f(f(a))), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyChainedVariables) { + // g(X, Y) =? g(Y, a) → {X → Y, Y → a} effectively X → a + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(Y, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), a); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Occurs Check Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, OccursCheckBlocks) { + // X =? f(X) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDisabledAllows) { + // X =? f(X) without occurs check → succeeds (unsound but fast) + Substitution subst; + UnificationConfig config{.enable_occurs_check = false}; + EXPECT_TRUE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDeep) { + // X =? f(g(X, a)) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(g(X, a)), subst, config)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// applySubstitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, ApplySubstitutionSimple) { + Substitution subst; + subst.bind(X, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, ApplySubstitutionNested) { + Substitution subst; + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(applySubstitution(subst, g(f(X), Y), bank), g(f(a), b)); +} + +TEST_F(UnificationTest, ApplySubstitutionPreservesUnbound) { + Substitution subst; + subst.bind(X, a); + // Y is unbound → stays as Y + EXPECT_EQ(applySubstitution(subst, g(X, Y), bank), g(a, Y)); +} + +TEST_F(UnificationTest, ApplySubstitutionToConstant) { + Substitution subst; + subst.bind(X, a); + // Constant is unchanged + EXPECT_EQ(applySubstitution(subst, b, bank), b); +} + +TEST_F(UnificationTest, ApplySubstitutionChain) { + // σ = {X → Y, Y → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, UnifyThenApply) { + // Full round-trip: unify P(X, f(Y)) with P(a, f(b)), then apply + Substitution subst; + TermId lhs = P(X, f(Y)); + TermId rhs = P(a, f(b)); + ASSERT_TRUE(unify(bank, lhs, rhs, subst)); + + EXPECT_EQ(applySubstitution(subst, lhs, bank), P(a, f(b))); + EXPECT_EQ(applySubstitution(subst, rhs, bank), P(a, f(b))); + // Both sides should produce the same term after applying the MGU + EXPECT_EQ(applySubstitution(subst, lhs, bank), + applySubstitution(subst, rhs, bank)); +} + +} // namespace +} // namespace atp |