natas_hw
/
mps-coderules
mirror of https://github.com/JetBrains/mps-coderules
0
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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.
This commit is contained in:
Fedor Isakov 2020-06-02 15:25:21 +02:00
parent c5d9e798a3
commit 18933cfcf2
4 changed files with 252 additions and 185 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

119
reactor/Core/src/jetbrains/mps/unification/TermGraphUnifier.kt
View File

@ -55,34 +55,15 @@ import java.util.*
typealias IntList = TIntArrayList
typealias IntAnyHashMap<V> = TIntObjectHashMap<V>
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<Any?>()
private val backref = IdentityHashMap<Any?, Int>()
private val origin = ArrayList<Term>()
private val innerClass = IntList()
private val innerSchema = IntList()
private val innerSize = IntList()
private val innerVars = IntAnyHashMap<IntList?>()
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<Int, Int> {
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<Any?>()
private val backref = IdentityHashMap<Any?, Int>()
private val innerVars = IntAnyHashMap<IntList?>()
private val origin = ArrayList<Term>()
private val innerClass = IntList()
private val innerSchema = IntList()
private val innerSize = IntList()
private val innerAcyclic = IntList()
private val innerVisited = IntList()
}

12
reactor/Core/src/jetbrains/mps/unification/Unification.kt
View File

@ -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)

16
reactor/Test/test/jetbrains/mps/unification/test/AssertUnification.java
View File

@ -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);

290
reactor/Test/test/jetbrains/mps/unification/test/SolverTests.java
View File

@ -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
);