diff options
Diffstat (limited to 'proofsearch/tests/test_unification.cc')
| -rw-r--r-- | proofsearch/tests/test_unification.cc | 355 |
1 files changed, 355 insertions, 0 deletions
diff --git a/proofsearch/tests/test_unification.cc b/proofsearch/tests/test_unification.cc new file mode 100644 index 0000000..63ac9f0 --- /dev/null +++ b/proofsearch/tests/test_unification.cc @@ -0,0 +1,355 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + */ + +#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" + +#include <gtest/gtest.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 const subst; + EXPECT_EQ(subst.resolve(x_, bank_), x_); // unbound → returns itself +} + +TEST_F(UnificationTest, SubstResolveNonVariable) { + Substitution const 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 const fx = f(x_); + TermId const result = subst.apply(fx, bank_); + TermId const 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 const gxy = g(x_, y_); + TermId const result = subst.apply(gxy, bank_); + TermId const 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 const result = subst.apply(g(x_, b_), bank_); + EXPECT_EQ(result, g(f(a_), b_)); +} + +TEST_F(UnificationTest, SubstOccursIn) { + Substitution const 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 const rx = subst.resolve(x_, bank_); + TermId const 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 const 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 const 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 const 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 const lhs = p(x_, f(y_)); + TermId const 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 |