diff options
Diffstat (limited to 'tests/test_unification.cc')
| -rw-r--r-- | tests/test_unification.cc | 228 |
1 files changed, 114 insertions, 114 deletions
diff --git a/tests/test_unification.cc b/tests/test_unification.cc index 516058a..63ac9f0 100644 --- a/tests/test_unification.cc +++ b/tests/test_unification.cc @@ -33,47 +33,47 @@ namespace { class UnificationTest : public ::testing::Test { protected: - SymbolTable symbols; - TermBank bank{symbols}; + 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{}; + 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{}; + 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); + 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}}); } + 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}}); } + 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}}); } + 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}}); } + TermId p(TermId a1, TermId a2) { return bank_.makeTerm(sym_p_, {{a1, a2}}); } }; // ═══════════════════════════════════════════════════════════════════════════ @@ -82,90 +82,90 @@ class UnificationTest : public ::testing::Test { 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 + 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 + 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 + 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); + 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 + Substitution const 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 + 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 fx = f(X); - TermId result = subst.apply(fx, bank); - TermId expected = f(a); + 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 gxy = g(X, Y); - TermId result = subst.apply(gxy, bank); - TermId expected = g(a, Y); + 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 result = subst.apply(g(X, b), bank); - EXPECT_EQ(result, g(f(a), b)); + 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 subst; + Substitution const subst; // X occurs in f(X) - EXPECT_TRUE(subst.occursIn(X, f(X), bank)); + 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)); + 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)); + EXPECT_FALSE(subst.occursIn(x_, f(a_), bank_)); // X does NOT occur in Y (different variable) - EXPECT_FALSE(subst.occursIn(X, Y, bank)); + 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); + 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); + EXPECT_EQ(subst.lookup(x_), kInvalidId); } // ═══════════════════════════════════════════════════════════════════════════ @@ -174,104 +174,104 @@ TEST_F(UnificationTest, SubstClearAndSize) { TEST_F(UnificationTest, UnifyIdenticalConstants) { Substitution subst; - EXPECT_TRUE(unify(bank, a, a, 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)); + 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); + 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); + 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)); + 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); + 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); + 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); + 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)); + 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); + 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)); + 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)); + 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)); + 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)); + 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); + 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); + 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_); } // ═══════════════════════════════════════════════════════════════════════════ @@ -281,22 +281,22 @@ TEST_F(UnificationTest, UnifyChainedVariables) { 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)); + 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 config{.enable_occurs_check = false}; - EXPECT_TRUE(unify(bank, X, f(X), subst, config)); + 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 config{.enable_occurs_check = true}; - EXPECT_FALSE(unify(bank, X, f(g(X, a)), subst, config)); + UnificationConfig const config{.enable_occurs_check_ = true}; + EXPECT_FALSE(unify(bank_, x_, f(g(x_, a_)), subst, config)); } // ═══════════════════════════════════════════════════════════════════════════ @@ -305,50 +305,50 @@ TEST_F(UnificationTest, OccursCheckDeep) { TEST_F(UnificationTest, ApplySubstitutionSimple) { Substitution subst; - subst.bind(X, a); - EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); + 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)); + 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); + subst.bind(x_, a_); // Y is unbound → stays as Y - EXPECT_EQ(applySubstitution(subst, g(X, Y), bank), g(a, Y)); + EXPECT_EQ(applySubstitution(subst, g(x_, y_), bank_), g(a_, y_)); } TEST_F(UnificationTest, ApplySubstitutionToConstant) { Substitution subst; - subst.bind(X, a); + subst.bind(x_, a_); // Constant is unchanged - EXPECT_EQ(applySubstitution(subst, b, bank), b); + 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)); + 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)); + 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))); + 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)); + EXPECT_EQ(applySubstitution(subst, lhs, bank_), applySubstitution(subst, rhs, bank_)); } } // namespace |