From 18933cfcf235cbefd5841904bdc417d35827567f Mon Sep 17 00:00:00 2001 From: Fedor Isakov Date: Tue, 2 Jun 2020 15:25:21 +0200 Subject: [PATCH] Support trivial bindings in unification results. Minor refactoring. Trivial substitutions such as [X->X] are optionally available. May prove usable when discovering variables within a term. --- .../mps/unification/TermGraphUnifier.kt | 119 +++---- .../jetbrains/mps/unification/Unification.kt | 12 + .../unification/test/AssertUnification.java | 16 + .../mps/unification/test/SolverTests.java | 290 ++++++++++-------- 4 files changed, 252 insertions(+), 185 deletions(-) diff --git a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt index 2e95de2d..26363ca2 100644 --- a/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt +++ b/reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt @@ -55,34 +55,15 @@ import java.util.* typealias IntList = TIntArrayList typealias IntAnyHashMap = TIntObjectHashMap -class TermGraphUnifier { +class TermGraphUnifier(private val wrapper: TermWrapper = TermWrapper.ID, + private val trivialBindings: Boolean = false) { + + constructor(trivialBindings: Boolean) : this(TermWrapper.ID, trivialBindings) {} companion object { val EMPTY_LIST = TIntArrayList.wrap(kotlin.IntArray(0)) } - private var wrapper: TermWrapper - - private var failureCause: Substitution.FailureCause = Substitution.FailureCause.UKNOWN - private var failureDetails = emptyArray() - - private val backref = IdentityHashMap() - private val origin = ArrayList() - private val innerClass = IntList() - private val innerSchema = IntList() - private val innerSize = IntList() - private val innerVars = IntAnyHashMap() - private val innerAcyclic = BitSet() - private val innerVisited = BitSet() - - constructor() { - this.wrapper = TermWrapper.ID - } - - constructor(wrapper: TermWrapper) { - this.wrapper = wrapper - } - fun unify(a: Term, b: Term): Substitution { return if (unifClosure(toInner(a), toInner(b))) { findSolution(toInner(a)) @@ -100,30 +81,29 @@ class TermGraphUnifier { val (_, z) = findSchema(s) val vars = innerVars[find(z)] - if (innerAcyclic[z]) { return defSubs } // not part of a cycle - if (innerVisited[z]) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle + if (isAcyclic(z)) { return defSubs } // not part of a cycle + if (isVisited(z)) { return failedSubstitution(CYCLE_DETECTED) } // there exists a cycle var subs = defSubs if (origin[z].`is`(FUN)) { - innerVisited.set(z) + setVisited(z) for (c in origin[z].arguments()) { - val (_, zc) = findSchema(toInner(c)) - subs = findSolution(zc, subs) + subs = findSolution(toInner(c), subs) if (!subs.isSuccessful) break } - innerVisited.clear(z) + clearVisited(z) } if (subs.isSuccessful) { - innerAcyclic.set(z) - + setAcyclic(z) + // avoid unnecessary instatiation val success = if (subs is SuccessfulSubstitution) subs as SuccessfulSubstitution else SuccessfulSubstitution(subs) if (vars != null) { for (v in vars) { - if (v != z) { + if (trivialBindings || v != z) { // Keep the order of variables within a binding if (origin[z].`is`(VAR) && origin[z].compareTo(origin[v]) < 0) { success.addBinding(fromInner(z), fromInner(v)) @@ -188,8 +168,8 @@ class TermGraphUnifier { if (s == t) { return s } - val ssize = innerSize[s] - val tsize = innerSize[t] + val ssize = size(s) + val tsize = size(t) // keep the order: the smaller class gets inserted under the bigger one if (ssize < tsize) { @@ -206,18 +186,18 @@ class TermGraphUnifier { } } - innerSize[s] = ssize + tsize + setSize(s, ssize + tsize) prependVars(s, innerVars[t]) - innerClass[t] = s - + setKlass(t, s) + // copy the schema - val zs = innerSchema[s] - val zt = innerSchema[t] + val zs = schema(s) + val zt = schema(t) if (origin[zs].`is`(REF)) { - innerSchema[s] = zt + setSchema(s, zt) } else if (origin[zs].`is`(VAR) && (origin[zt].`is`(FUN))) { - innerSchema[s] = zt + setSchema(s, zt) } return s @@ -225,19 +205,15 @@ class TermGraphUnifier { private fun find(t: Int): Int { - var repr = innerClass[t] + var repr = klass(t) if (repr == t) { return repr } - if (repr != innerClass[repr]) { + if (repr != klass(repr)) { // find representative and compress paths - val path = IntList() - path.add(t) - while (repr != innerClass[repr]) { - path.add(repr) - repr = innerClass[repr] - } - for (p in path) { - innerClass[p] = repr + while (repr != klass(repr)) { + val tmp = repr + repr = klass(repr) + setKlass(tmp, repr) } } @@ -255,10 +231,10 @@ class TermGraphUnifier { private fun findSchema(s: Int): Pair { var t = find(s) - var zt = innerSchema[t] + var zt = schema(t) while (origin[zt].`is`(REF)) { t = union(t, getRef(zt)) - zt = innerSchema[t] + zt = schema(t) } return t to zt } @@ -279,9 +255,14 @@ class TermGraphUnifier { val wrapped = wrapper.wrap(term) val next = origin.size origin.add(wrapped) + + // initialize internal structures innerSchema.add(next) innerClass.add(next) innerSize.add(1) + innerAcyclic.add(0) + innerVisited.add(0) + if (wrapped.`is`(VAR)) { innerVars.put(next, IntList(intArrayOf(next))) } @@ -305,4 +286,36 @@ class TermGraphUnifier { return if (this == null) that == null else this.equals(that) } + private fun klass(t: Int): Int = innerClass[t] + + private fun setKlass(t: Int, klass: Int): Unit { innerClass[t] = klass } + + private fun schema(t: Int): Int = innerSchema[t] + + private fun setSchema(t: Int, schema: Int): Unit { innerSchema[t] = schema } + + private fun size(t: Int): Int = innerSize[t] + + private fun setSize(t: Int, size: Int): Unit { innerSize[t] = size } + + private fun isAcyclic(t: Int): Boolean = innerAcyclic[t] != 0 + + private fun setAcyclic(t: Int): Unit { innerAcyclic[t] = 1 } + + private fun isVisited(t: Int): Boolean = innerVisited[t] != 0 + + private fun setVisited(t: Int): Unit { innerVisited[t] = 1 } + + private fun clearVisited(t: Int): Unit { innerVisited[t] = 0 } + + private var failureCause: Substitution.FailureCause = Substitution.FailureCause.UKNOWN + private var failureDetails = emptyArray() + private val backref = IdentityHashMap() + private val innerVars = IntAnyHashMap() + private val origin = ArrayList() + private val innerClass = IntList() + private val innerSchema = IntList() + private val innerSize = IntList() + private val innerAcyclic = IntList() + private val innerVisited = IntList() } \ No newline at end of file diff --git a/reactor/Core/src/jetbrains/mps/unification/Unification.kt b/reactor/Core/src/jetbrains/mps/unification/Unification.kt index 3efb4f11..d51aa5d4 100644 --- a/reactor/Core/src/jetbrains/mps/unification/Unification.kt +++ b/reactor/Core/src/jetbrains/mps/unification/Unification.kt @@ -46,6 +46,18 @@ object Unification { return dagUnifier.unify(a, b) } + /** + * Returns also the trivial bindings. + * Example: + * f{g{}, X} = f{Y, X} yields [Y->g{}, X->X] + * f{Y} = X yields [X->f{Y}, Y->Y] + */ + fun unifyAll(a: Term, b: Term): Substitution { + val dagUnifier = TermGraphUnifier(true) + + return dagUnifier.unify(a, b) + } + fun unify(a: Term, b: Term, wrapper: TermWrapper): Substitution { val dagUnifier = TermGraphUnifier(wrapper) diff --git a/reactor/Test/test/jetbrains/mps/unification/test/AssertUnification.java b/reactor/Test/test/jetbrains/mps/unification/test/AssertUnification.java index 450ea07b..607c1f16 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/AssertUnification.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/AssertUnification.java @@ -80,6 +80,22 @@ public class AssertUnification { assertSameBindings(subs.bindings(), subs2.bindings()); } + public static void assertUnifiesAllWithBindings(Term s, Term t, Substitution.Binding ... bindings) throws Exception{ + Substitution subs = Unification.INSTANCE.unifyAll(s, t); + + assertTrue(subs.isSuccessful()); + assertSameBindings( + Arrays.asList( + bindings + ), + subs.bindings()); + + Substitution subs2 = Unification.INSTANCE.unifyAll(t, s); + + assertTrue(subs2.isSuccessful()); + assertSameBindings(subs.bindings(), subs2.bindings()); + } + public static void assertUnifiesWithBindings(Term s, Term t, TermWrapper wrapper, Substitution.Binding ... bindings) throws Exception{ Substitution subs = Unification.INSTANCE.unify(s, t, wrapper); diff --git a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java index 9d5b730b..cb2cb377 100644 --- a/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java +++ b/reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java @@ -43,10 +43,10 @@ public class SolverTests { @Test public void test1() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("a"), + parseTerm("a"), var("X"), - bind(var("X"), MockTermsParser.parseTerm("a")) + bind(var("X"), parseTerm("a")) ); assertUnifiesWithBindings( var("Y"), @@ -55,8 +55,8 @@ public class SolverTests { bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{Y}"), - MockTermsParser.parseTerm("a{X}"), + parseTerm("a{Y}"), + parseTerm("a{X}"), bind(var("X"), var("Y")) ); @@ -65,56 +65,56 @@ public class SolverTests { @Test public void test2() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b c}"), - MockTermsParser.parseTerm("a{X Y}"), + parseTerm("a{b c}"), + parseTerm("a{X Y}"), - bind(var("X"), MockTermsParser.parseTerm("b")), - bind(var("Y"), MockTermsParser.parseTerm("c")) + bind(var("X"), parseTerm("b")), + bind(var("Y"), parseTerm("c")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b Y}"), - MockTermsParser.parseTerm("a{X c}"), + parseTerm("a{b Y}"), + parseTerm("a{X c}"), - bind(var("X"), MockTermsParser.parseTerm("b")), - bind(var("Y"), MockTermsParser.parseTerm("c")) + bind(var("X"), parseTerm("b")), + bind(var("Y"), parseTerm("c")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{c} X Y Z}"), - MockTermsParser.parseTerm("a{X Y Z b{c}}"), + parseTerm("a{b{c} X Y Z}"), + parseTerm("a{X Y Z b{c}}"), - bind(var("X"), MockTermsParser.parseTerm("b{c}")), - bind(var("Y"), MockTermsParser.parseTerm("b{c}")), - bind(var("Z"), MockTermsParser.parseTerm("b{c}")) + bind(var("X"), parseTerm("b{c}")), + bind(var("Y"), parseTerm("b{c}")), + bind(var("Z"), parseTerm("b{c}")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{c} Z Y X}"), - MockTermsParser.parseTerm("a{Z Y X b{W}}"), + parseTerm("a{b{c} Z Y X}"), + parseTerm("a{Z Y X b{W}}"), - bind(var("X"), MockTermsParser.parseTerm("b{c}")), - bind(var("Y"), MockTermsParser.parseTerm("b{c}")), - bind(var("Z"), MockTermsParser.parseTerm("b{c}")), - bind(var("W"), MockTermsParser.parseTerm("c")) + bind(var("X"), parseTerm("b{c}")), + bind(var("Y"), parseTerm("b{c}")), + bind(var("Z"), parseTerm("b{c}")), + bind(var("W"), parseTerm("c")) ); } @Test public void test3() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{X} c{Y}}"), - MockTermsParser.parseTerm("a{V W}"), + parseTerm("a{b{X} c{Y}}"), + parseTerm("a{V W}"), bind(var("V"), parseTerm("b{X}")), bind(var("W"), parseTerm("c{Y}")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{X}"), - MockTermsParser.parseTerm("a{Y}"), + parseTerm("a{X}"), + parseTerm("a{Y}"), bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{X} c{Y}}"), - MockTermsParser.parseTerm("a{b{V} c{W}}"), + parseTerm("a{b{X} c{Y}}"), + parseTerm("a{b{V} c{W}}"), bind(var("V"), var("X")), bind(var("W"), var("Y")) @@ -124,8 +124,8 @@ public class SolverTests { @Test public void test4() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{X} c{Y}}"), - MockTermsParser.parseTerm("a{Y Z}"), + parseTerm("a{b{X} c{Y}}"), + parseTerm("a{Y Z}"), bind(var("Y"), parseTerm("b{X}")), bind(var("Z"), parseTerm("c{Y}")) @@ -139,7 +139,7 @@ public class SolverTests { parseTerm("a{Y b{X}}"), bind(var("Y"), parseTerm("b{c}")), - bind(var("X"), MockTermsParser.parseTerm("c")) + bind(var("X"), parseTerm("c")) ); } @@ -150,7 +150,7 @@ public class SolverTests { parseTerm("a{Y c{b{d}}}"), bind(var("Y"), parseTerm("b{X}")), - bind(var("X"), MockTermsParser.parseTerm("d")) + bind(var("X"), parseTerm("d")) ); } @@ -215,8 +215,8 @@ public class SolverTests { @Test public void test12() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("node{name{foo} child{X}}"), - MockTermsParser.parseTerm("node{name{foo} child{Y}}"), + parseTerm("node{name{foo} child{X}}"), + parseTerm("node{name{foo} child{Y}}"), bind(var("X"), var("Y")) ); @@ -225,8 +225,8 @@ public class SolverTests { @Test public void test13() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("node{name{foo} child{node{name{bar}}}}"), - MockTermsParser.parseTerm("node{name{foo} child{X}}"), + parseTerm("node{name{foo} child{node{name{bar}}}}"), + parseTerm("node{name{foo} child{X}}"), bind(var("X"), parseTerm("node{name{bar}}")) ); @@ -235,8 +235,8 @@ public class SolverTests { @Test public void test14() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("f{X g{a}}"), - MockTermsParser.parseTerm("f{g{Y} g{Y}}"), + parseTerm("f{X g{a}}"), + parseTerm("f{g{Y} g{Y}}"), bind(var("X"), parseTerm("g{Y}")), bind(var("Y"), parseTerm("a")) @@ -246,8 +246,8 @@ public class SolverTests { @Test public void test15() throws Exception { assertUnifiesWithBindingsAsymm( - MockTermsParser.parseTerm("h{X1 f{Y0 Y0} Y1}"), - MockTermsParser.parseTerm("h{f{X0 X0} Y1 X1}"), + parseTerm("h{X1 f{Y0 Y0} Y1}"), + parseTerm("h{f{X0 X0} Y1 X1}"), bind(var("X0"), parseTerm("Y0")), bind(var("X1"), parseTerm("f{Y0 Y0}")), @@ -262,9 +262,9 @@ public class SolverTests { // substitution instead of the "triangular" form used here. assertUnifiesWithBindingsAsymm( - MockTermsParser.parseTerm("h{X1 X2 X3 X4 X5 X6 X7 X8 X9 " + + parseTerm("h{X1 X2 X3 X4 X5 X6 X7 X8 X9 " + "f{Y0 Y0} f{Y1 Y1} f{Y2 Y2} f{Y3 Y3} f{Y4 Y4} f{Y5 Y5} f{Y6 Y6} f{Y7 Y7} f{Y8 Y8} Y9}"), - MockTermsParser.parseTerm("h{f{X0 X0} f{X1 X1} f{X2 X2} f{X3 X3} f{X4 X4} f{X5 X5} f{X6 X6} f{X7 X7} f{X8 X8} " + + parseTerm("h{f{X0 X0} f{X1 X1} f{X2 X2} f{X3 X3} f{X4 X4} f{X5 X5} f{X6 X6} f{X7 X7} f{X8 X8} " + "Y1 Y2 Y3 Y4 Y5 Y6 Y7 Y8 Y9 X9}"), bind(var("X0"), parseTerm("Y0")), @@ -294,69 +294,69 @@ public class SolverTests { @Ignore public void testCyclicVar() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("@1 a{b ^1}"), - MockTermsParser.parseTerm("X"), + parseTerm("@1 a{b ^1}"), + parseTerm("X"), - bind(var("X"), MockTermsParser.parseTerm("@1 a{b ^1}")) + bind(var("X"), parseTerm("@1 a{b ^1}")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("@1 a{^1 b c}"), - MockTermsParser.parseTerm("X"), + parseTerm("@1 a{^1 b c}"), + parseTerm("X"), - bind(var("X"), MockTermsParser.parseTerm("@1 a{^1 b c}")) + bind(var("X"), parseTerm("@1 a{^1 b c}")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{X c{X} }"), - MockTermsParser.parseTerm("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"), + parseTerm("a{X c{X} }"), + parseTerm("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"), - bind(var("X"), MockTermsParser.parseTerm("b{Y}")), - bind(var("Y"), MockTermsParser.parseTerm("@1 c{b{^1}}")) + bind(var("X"), parseTerm("b{Y}")), + bind(var("Y"), parseTerm("@1 c{b{^1}}")) ); } @Test public void testVarRef() throws Exception { assertUnifiesWithBindings( - MockTermsParser.parseTerm("^X"), - MockTermsParser.parseTerm("Y"), + parseTerm("^X"), + parseTerm("Y"), bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("f{^X}"), - MockTermsParser.parseTerm("f{ Y}"), + parseTerm("f{^X}"), + parseTerm("f{ Y}"), bind(var("X"), var("Y")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b ^X}"), - MockTermsParser.parseTerm("a{b c{d}}"), + parseTerm("a{b ^X}"), + parseTerm("a{b c{d}}"), - bind(var("X"), MockTermsParser.parseTerm("c{d}")) + bind(var("X"), parseTerm("c{d}")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b c{X} ^X}"), - MockTermsParser.parseTerm("a{b c{d} d}"), + parseTerm("a{b c{X} ^X}"), + parseTerm("a{b c{d} d}"), - bind(var("X"), MockTermsParser.parseTerm("d")) + bind(var("X"), parseTerm("d")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{d} c{X} ^X}"), - MockTermsParser.parseTerm("a{b{^X} c{d} d}"), + parseTerm("a{b{d} c{X} ^X}"), + parseTerm("a{b{^X} c{d} d}"), - bind(var("X"), MockTermsParser.parseTerm("d")) + bind(var("X"), parseTerm("d")) ); assertUnifiesWithBindings( - MockTermsParser.parseTerm("a{b{d} c{X}}"), - MockTermsParser.parseTerm("a{b{^X} c{d}}"), + parseTerm("a{b{d} c{X}}"), + parseTerm("a{b{^X} c{d}}"), - bind(var("X"), MockTermsParser.parseTerm("d")) + bind(var("X"), parseTerm("d")) ); } @Test public void testUnifyExternalRef() throws Exception { - Term termRef = ref(MockTermsParser.parseTerm("f {a f{b f{c d}}}")); + Term termRef = ref(parseTerm("f {a f{b f{c d}}}")); Term varRef = ref(var("TAIL")); Term a = term("g", termRef); @@ -366,14 +366,40 @@ public class SolverTests { a, b, - bind(var("HEAD"), MockTermsParser.parseTerm("a")), - bind(var("TAIL"), MockTermsParser.parseTerm("f{b f{c d}}")) + bind(var("HEAD"), parseTerm("a")), + bind(var("TAIL"), parseTerm("f{b f{c d}}")) + ); + } + + @Test + public void testTrivialBindings() throws Exception { + Term a = parseTerm("f {a g{X h}}"); + Term b = parseTerm("f {Y g{X Z}}"); + + assertUnifiesAllWithBindings( + a, + b, + + bind(var("X"), var("X")), + bind(var("Y"), parseTerm("a")), + bind(var("Z"), parseTerm("h")) + ); + + Term c = parseTerm("f {a Y}"); + Term d = parseTerm("X"); + + assertUnifiesAllWithBindings( + c, + d, + + bind(var("X"), parseTerm("f {a Y}")), + bind(var("Y"), var("Y")) ); } @Test public void testUnifyExternalRef2() throws Exception { - Term list = MockTermsParser.parseTerm("f {a f{b f{c d}}}"); + Term list = parseTerm("f {a f{b f{c d}}}"); Term termRef = ref(list); Term varRef = ref(var("TAIL")); @@ -387,15 +413,15 @@ public class SolverTests { aa, bb, - bind(var("LIST"), MockTermsParser.parseTerm("f {a f{b f{c d}}}")), - bind(var("HEAD"), MockTermsParser.parseTerm("a")), - bind(var("TAIL"), MockTermsParser.parseTerm("f{b f{c d}}")) + bind(var("LIST"), parseTerm("f {a f{b f{c d}}}")), + bind(var("HEAD"), parseTerm("a")), + bind(var("TAIL"), parseTerm("f{b f{c d}}")) ); } @Test public void testUnifyExternalRef3() throws Exception { - Term empty = MockTermsParser.parseTerm("f {nil}"); + Term empty = parseTerm("f {nil}"); Term varRef = ref(var("TAIL")); Term aa = term("g", empty); @@ -405,16 +431,16 @@ public class SolverTests { aa, bb, - bind(var("TAIL"), MockTermsParser.parseTerm("nil")) + bind(var("TAIL"), parseTerm("nil")) ); } @Test public void testWrapper() throws Exception { - Term t1 = MockTermsParser.parseTerm("a{b c{X}}"); - Term t2 = MockTermsParser.parseTerm("a{X c{Y}}"); - Term p1 = MockTermsParser.parseTerm("a{META c{d}}"); - Term p2 = MockTermsParser.parseTerm("a{b c{META}}"); + Term t1 = parseTerm("a{b c{X}}"); + Term t2 = parseTerm("a{X c{Y}}"); + Term p1 = parseTerm("a{META c{d}}"); + Term p2 = parseTerm("a{b c{META}}"); class Wrapper implements Term { Term wrapped; @@ -464,34 +490,34 @@ public class SolverTests { }; assertUnifiesWithBindings(t1, p1, - bind(var("META"), MockTermsParser.parseTerm("b")), - bind(var("X"), MockTermsParser.parseTerm("d")) + bind(var("META"), parseTerm("b")), + bind(var("X"), parseTerm("d")) ); assertUnificationFails(t1, p1, wrapper); assertUnifiesWithBindings(t1, p2, wrapper, - bind(var("X"), MockTermsParser.parseTerm("META")) + bind(var("X"), parseTerm("META")) ); assertUnifiesWithBindings(t2, p2, wrapper, - bind(var("X"), MockTermsParser.parseTerm("b")), - bind(var("Y"), MockTermsParser.parseTerm("META")) + bind(var("X"), parseTerm("b")), + bind(var("Y"), parseTerm("META")) ); } @Test public void testFailConflict() throws Exception { assertUnificationFails( - MockTermsParser.parseTerm("a"), - MockTermsParser.parseTerm("b"), + parseTerm("a"), + parseTerm("b"), SYMBOL_CLASH, "a", "b" ); assertUnificationFails( - MockTermsParser.parseTerm("node{name{X} child{abc}}"), - MockTermsParser.parseTerm("node{name{foo} child{X}}"), + parseTerm("node{name{X} child{abc}}"), + parseTerm("node{name{foo} child{X}}"), SYMBOL_CLASH, "abc", @@ -502,76 +528,76 @@ public class SolverTests { @Test public void testFailCard() throws Exception { assertUnificationFails( - MockTermsParser.parseTerm("a{b c}"), - MockTermsParser.parseTerm("a{X}") + parseTerm("a{b c}"), + parseTerm("a{X}") ); } @Test public void testFailCyclic() throws Exception { assertUnificationFails( - term("g", ref(MockTermsParser.parseTerm("f {h X}"))), + term("g", ref(parseTerm("f {h X}"))), term("g", var("X")), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t {@1 f {h X} g {f {h X}}}"), - MockTermsParser.parseTerm("t {Y g {X}}"), + parseTerm("t {@1 f {h X} g {f {h X}}}"), + parseTerm("t {Y g {X}}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("a{b X}"), - MockTermsParser.parseTerm("X"), + parseTerm("a{b X}"), + parseTerm("X"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("f{X}"), - MockTermsParser.parseTerm("X"), + parseTerm("f{X}"), + parseTerm("X"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("X"), - MockTermsParser.parseTerm("f{X}"), + parseTerm("X"), + parseTerm("f{X}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("f{f{X}}"), - MockTermsParser.parseTerm("f{X}"), + parseTerm("f{f{X}}"), + parseTerm("f{X}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("f{a{X} Y }"), - MockTermsParser.parseTerm("f{Y a{b{X}}}"), + parseTerm("f{a{X} Y }"), + parseTerm("f{Y a{b{X}}}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("a{X c{X}}"), - MockTermsParser.parseTerm("a{b{Y} Y }"), + parseTerm("a{X c{X}}"), + parseTerm("a{b{Y} Y }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"), - MockTermsParser.parseTerm("a{ b{Y} b{Y} }"), + parseTerm("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"), + parseTerm("a{ b{Y} b{Y} }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t {@1 f {h X} g {f {h X}}}"), - MockTermsParser.parseTerm("t {Y g {X}}"), + parseTerm("t {@1 f {h X} g {f {h X}}}"), + parseTerm("t {Y g {X}}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t {@1 f {h X} g {^1}}"), - MockTermsParser.parseTerm("t {Y g {X}}"), + parseTerm("t {@1 f {h X} g {^1}}"), + parseTerm("t {Y g {X}}"), CYCLE_DETECTED ); @@ -580,56 +606,56 @@ public class SolverTests { @Test public void testFailCyclicVarRef() throws Exception { assertUnificationFails( - MockTermsParser.parseTerm("X"), - MockTermsParser.parseTerm("f{^X}"), + parseTerm("X"), + parseTerm("f{^X}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("f{X}"), - MockTermsParser.parseTerm("f{f{^X}}"), + parseTerm("f{X}"), + parseTerm("f{f{^X}}"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"), - MockTermsParser.parseTerm("t { f{X} X }"), + parseTerm("t {@1 f{X} g{^1}}"), + parseTerm("t { f{X} X }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t {@1 f{X} g{^1}}"), - MockTermsParser.parseTerm("t { f{Y} Y }"), + parseTerm("t {@1 f{X} g{^1}}"), + parseTerm("t { f{Y} Y }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t { f{^X} X }"), - MockTermsParser.parseTerm("t { Y g{^Y} }"), + parseTerm("t { f{^X} X }"), + parseTerm("t { Y g{^Y} }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t { ^X Y }"), - MockTermsParser.parseTerm("t { Y f{X} }"), + parseTerm("t { ^X Y }"), + parseTerm("t { Y f{X} }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t { X Y }"), - MockTermsParser.parseTerm("t { f{Y} ^X }"), + parseTerm("t { X Y }"), + parseTerm("t { f{Y} ^X }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t { ^X Y }"), - MockTermsParser.parseTerm("t { f{Y} ^X }"), + parseTerm("t { ^X Y }"), + parseTerm("t { f{Y} ^X }"), CYCLE_DETECTED ); assertUnificationFails( - MockTermsParser.parseTerm("t { ^X ^Y }"), - MockTermsParser.parseTerm("t { Y f{X} }"), + parseTerm("t { ^X ^Y }"), + parseTerm("t { Y f{X} }"), CYCLE_DETECTED );