diff --git a/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java b/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
index 03838af3..f2508d1d 100644
--- a/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
+++ b/reactor/unification/code/src/jetbrains/mps/unification/UnionFindTermGraphUnifier.java
@@ -29,11 +29,13 @@ import static jetbrains.mps.unification.Unification.*;
* This is an implementation of the "near linear" algorithm for solving syntactic unification
* as described in the paper linked below and also in the textbook of the same author.1 2
*
- * No recursive terms are allowed as a solution, meaning the "occurrs check" for variables
- * is performed on the input. However, cyclic terms are allowed as input and can be unified, producing
- * solutions binding variables to cyclic terms. Variables can also be passed by reference without altering the
+ * No recursive terms are allowed as a solution, meaning the "occurs check" for variables
+ * is performed on the input. Variables can also be passed by reference without altering the
* intuitive behaviour of the algorithm.
*
+ * The "REF" terms are an extension of the term algebra used in [1]. For the purposes of this algorithm, the "REF"
+ * terms are treated as pre-bound variables.
+ *
* If successful, the returned {@link Substitution} contains
* the variable bindings.
*
@@ -68,46 +70,29 @@ public class UnionFindTermGraphUnifier {
s = find(s);
t = find(t);
- if (s == t) return true;
+ if (s == t) {
+ return true;
+ }
InnerTerm zs = s.mySchema;
InnerTerm zt = t.mySchema;
+ while (zs.myOrigin.is(REF)) {
+ s = union(s, getRef(zs));
+ zs = s.mySchema;
+ }
+
+ while (zt.myOrigin.is(REF)) {
+ t = union(t, getRef(zt));
+ zt = t.mySchema;
+ }
+
// a VAR always matches another node
if(zs.myOrigin.is(VAR) || zt.myOrigin.is(VAR)) {
union(s, t);
return true;
}
- // dereference REF nodes
- InnerTerm ds = deref(zs);
- InnerTerm dt = deref(zt);
-
- if (ds.myOrigin.is(VAR)) {
- union(s, find(ds));
- union(s, t);
- return true;
- }
- else
- {
- zs = ds;
- }
-
- if (dt.myOrigin.is(VAR)) {
- union(t, find(dt));
- union(t, s);
- return true;
- }
- else
- {
- zt = dt;
- }
-
- // use find 2nd time to account for dereferenced nodes
- if (find(zs) == find(zt)) {
- return true;
- }
-
if (zs.myOrigin.is(FUN) && zt.myOrigin.is(FUN))
{
if (!eq(zs.myOrigin.symbol(), zt.myOrigin.symbol())) {
@@ -116,7 +101,7 @@ public class UnionFindTermGraphUnifier {
return false; // symbol clash
}
- // union REF nodes only to each other
+ // union REF nodes only if they are the same node
if (s.myOrigin.is(REF) == t.myOrigin.is(REF)) {
union(s, t);
}
@@ -138,7 +123,14 @@ public class UnionFindTermGraphUnifier {
}
}
- private void union(InnerTerm s, InnerTerm t) {
+ private InnerTerm union(InnerTerm s, InnerTerm t) {
+ s = find(s);
+ t = find(t);
+
+ if (s == t) {
+ return s;
+ }
+
int ssize = s.mySize;
int tsize = t.mySize;
@@ -154,19 +146,21 @@ public class UnionFindTermGraphUnifier {
}
// union s and t classes by moving t under s
-
s.mySize = ssize + tsize;
prependVars(s, t.myVars);
+ t.myClass = s;
+ // copy the schema
InnerTerm zs = s.mySchema;
InnerTerm zt = t.mySchema;
- if (zs.myOrigin.is(VAR) ||
- (zs.myOrigin.is(REF) && !zt.myOrigin.is(VAR)))
- {
+ if (zs.myOrigin.is(REF)) {
+ s.mySchema = zt;
+
+ } else if (zs.myOrigin.is(VAR) && !(zt.myOrigin.is(VAR))) {
s.mySchema = zt;
}
- t.myClass = s;
+ return s;
}
private InnerTerm find(InnerTerm term) {
@@ -176,7 +170,6 @@ public class UnionFindTermGraphUnifier {
}
// find representative and compress paths
-
List path = new ArrayList(4);
path.add(term.myClass);
for (InnerTerm t; (t = term.myClass) != repr; ) {
@@ -191,12 +184,7 @@ public class UnionFindTermGraphUnifier {
}
private Substitution findSolution(InnerTerm s) {
- mySolutionQueue.add(s);
- Substitution solution = EMPTY_SUBSTITUTION;
- while(!mySolutionQueue.isEmpty() && solution.isSuccessful()) {
- solution = findSolution(mySolutionQueue.removeFirst(), solution);
- }
- return solution;
+ return findSolution(s, EMPTY_SUBSTITUTION);
}
private Substitution findSolution(InnerTerm s, Substitution substitution) {
@@ -213,49 +201,38 @@ public class UnionFindTermGraphUnifier {
z.myVisited = true;
for (Term c : z.myOrigin.arguments()) {
- substitution = findSolution(toInner(c), substitution);
-
- if (!substitution.isSuccessful()) {
+ if (!(substitution = findSolution(toInner(c), substitution)).isSuccessful()) {
break;
}
}
z.myVisited = false;
-
- }
- else if(z.myOrigin.is(REF)) {
- InnerTerm trg = deref(z);
- if (!trg.myAcyclic) {
- mySolutionQueue.add(trg);
- }
}
- if (!substitution.isSuccessful()) {
- return substitution;
- }
+ if (substitution.isSuccessful()) {
+ z.myAcyclic = true;
- z.myAcyclic = true;
+ // avoid unnecessary instantiation
+ SuccessfulSubstitution success =
+ (substitution instanceof SuccessfulSubstitution) ?
+ (SuccessfulSubstitution) substitution : new SuccessfulSubstitution(substitution);
- // avoid unnecessary instantiation
- SuccessfulSubstitution success =
- (substitution instanceof SuccessfulSubstitution) ?
- (SuccessfulSubstitution) substitution : new SuccessfulSubstitution(substitution);
+ for (InnerTerm var : find(z).myVars) {
+ if (var != z) {
+ // Keep the order of variables within a binding
+ if (z.myOrigin.is(VAR) && z.myOrigin.compareTo(var.myOrigin) < 0) {
+ success.addBinding(fromInner(z), fromInner(var));
- for (InnerTerm var : find(z).myVars) {
- if (var != z) {
- InnerTerm trg = deref(z);
-
- // Keep the order of variables within a binding
- if (trg.myOrigin.is(VAR) && trg.myOrigin.compareTo(var.myOrigin) < 0) {
- success.addBinding(fromInner(trg), fromInner(var));
- }
- else {
- success.addBinding(fromInner(var), fromInner(trg));
+ } else {
+ success.addBinding(fromInner(var), fromInner(z));
+ }
}
}
+
+ substitution = success;
}
- return success;
+ return substitution;
}
private void prependVars(InnerTerm t, List vars) {
@@ -266,12 +243,11 @@ public class UnionFindTermGraphUnifier {
t.myVars = newVars;
}
- private InnerTerm deref(InnerTerm zs) {
- InnerTerm tmp = zs;
- while (tmp.myOrigin.is(REF)) {
- tmp = toInner(tmp.myOrigin.get());
+ private InnerTerm getRef(InnerTerm zs) {
+ if (zs.myOrigin.is(REF)) {
+ return toInner(zs.myOrigin.get());
}
- return tmp;
+ return zs;
}
private InnerTerm toInner(Term term) {
@@ -298,13 +274,8 @@ public class UnionFindTermGraphUnifier {
}
private TermWrapper wrapper = TermWrapper.ID;
-
private Map myTermCache = new IdentityHashMap();
-
private FailureCause myFailureCause = UKNOWN;
-
- private LinkedList mySolutionQueue = new LinkedList();
-
private Object[] myFailureDetails = null;
private static boolean eq(Object a, Object b) {
diff --git a/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java b/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java
index 85117330..db74a08d 100644
--- a/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java
+++ b/reactor/unification/tests/test/jetbrains/mps/unification/test/SolverTests.java
@@ -19,7 +19,9 @@ package jetbrains.mps.unification.test;
import jetbrains.mps.unification.Term;
import jetbrains.mps.unification.TermWrapper;
import org.jetbrains.annotations.NotNull;
+import org.junit.Ignore;
import org.junit.Test;
+import org.omg.CORBA.UNKNOWN;
import java.util.Collection;
import java.util.Collections;
@@ -283,103 +285,8 @@ public class SolverTests {
);
}
- @Test
- public void testCyclic() throws Exception {
- assertUnifiesWithBindings(
- parse("@1 a{b ^1}"),
- parse("@2 a{b a{b ^2}}")
-
- );
- assertUnifiesWithBindings(
- parse("@1 a{b ^1}"),
- parse(" a{b @3 a{b ^3}}")
-
- );
- assertUnifiesWithBindings(
- parse("@1 a{b ^1}"),
- parse("@2 a{b ^2}")
- );
- // the following tests are not very strict, but they suffice to convey a message
- // that cyclic terms can be safely unified
- assertUnifiesWithBindings(
- parse("a{@1 b{c{^2}} @2 b{c{^1}}}"),
- parse("a{ b{Y} b{Y} }"),
-
- // TODO: the innermost "b" must actually contain a ref to the top level
- // FIXME: AssertStructurallyEquivalent
- bind(var("Y"), parse("@1 c{b{c{b }}}"))
- );
- assertUnifiesWithBindings(
- parse("a{@1 b{c{^1}} @2 c{b{^2}}}"),
- parse("a{ b{Y} Y }"),
-
- // TODO: the innermost "b" must actually contain a ref to the top level
- // FIXME: AssertStructurallyEquivalent
- bind(var("Y"), parse("c{b }"))
- );
- assertUnifiesWithBindings(
- parse("a{@1 b{c{@3 b{c{^3}}}} @2 c{b{^2}}}"),
- parse("a{ b{Y} Y }"),
-
- // TODO: the innermost "c" must actually contain a ref to the top level
- // FIXME: AssertStructurallyEquivalent
- bind(var("Y"), parse("c{b{c }}"))
- );
- assertUnifiesWithBindings(
- parse("@1 a{c{d} b{e{^1 f}}}"),
- parse(" a{c{X} b{Y}}"),
-
- bind(var("X"), parse("d")),
-
- // TODO: the innermost "b" must actually contain a ref to the top level
- // FIXME: AssertStructurallyEquivalent
- bind(var("Y"), parse("e{a{c{d} b } f}"))
- );
- assertUnifiesWithBindings(
- parse("@1 a{c{d} b{e{@2 a{c{d} b{e{^2 f}}} f}}}"),
- parse(" a{c{X} b{Y}}"),
-
- bind(var("X"), parse("d")),
-
- // TODO: the innermost "e" must actually contain a ref to the top level
- // FIXME: AssertStructurallyEquivalent
- bind(var("Y"), parse("e{a{c{d} b{e{ f}}} f}"))
- );
- }
-
- @Test
- public void testCyclicExt() throws Exception {
- Term left = parse("@1 j{^1}");
- Term right = term("j", term("j", ref(left)));
- assertUnifiesWithBindings(
- left,
- right
- );
- assertUnifiesWithBindings(
- parse("a{@1 b{c{^1}} b{c{Z}} @2 c{b{^2}}}"),
- parse("a{ Z b{Y} Y }"),
-
- bind(var("Y"), parse("@2 c{Z}")),
- bind(var("Z"), parse("@1 b{c{^1}}"))
- );
- assertUnifiesWithBindings(
- parse("@1 a{c{d} b{e{Z f}} ^1}"),
- parse(" a{c{X} b{Y} Z}"),
-
- bind(var("X"), parse("d")),
- bind(var("Y"), parse("e{Z f}")),
- bind(var("Z"), parse("@1 a{c{d} b{e{Z f}} ^1}"))
- );
- }
-
@Test
public void testCyclicVar() throws Exception {
- assertUnifiesWithBindings(
- parse("@1 a{b ^1}"),
- parse("@1 a{b X}"),
-
- bind(var("X"), parse("@1 a{b ^1}"))
- );
assertUnifiesWithBindings(
parse("@1 a{b ^1}"),
parse("X"),
@@ -392,12 +299,6 @@ public class SolverTests {
bind(var("X"), parse("@1 a{^1 b c}"))
);
- assertUnifiesWithBindings(
- parse("@1 a{b ^1}"),
- parse("@1 a{b a{b X}}"),
-
- bind(var("X"), parse("@1 a{b ^1}"))
- );
assertUnifiesWithBindings(
parse("a{X c{X} }"),
parse("a{b{Y} c{@1 b{@2 c{b{^2}}}}}"),
@@ -441,35 +342,6 @@ public class SolverTests {
);
}
- @Test
- public void testCyclic_TermRewriting() throws Exception {
- // The original problem is to unify two cyclic terms:
- //
- // +->f +--->f
- // |_/ \ | / \
- // X | f f<-+
- // |_/ \ / \_|
- // Y
- //
- // -- which would be equivalent to the following:
- //
- // "@1 f {^1 X}" "@2 f {f {^2 Y} @3 f {Y ^3}}"
- //
- // Unfortunately, although the algorithm can successfully unify these
- // two terms, no solution exists that is not recursive. That is,
- // we cannot produce a list of variable bindings that do not include a
- // variable itself in the substitution. Thus, we resort to a simplified test.
-
- assertUnifiesWithBindings(
- parse("@1 f {^1 X}"),
- parse("@2 f {f {^2 Y} @3 f {Z ^3}}"),
-
- bind(var("X"), parse("@1 f{Z ^1}")),
- bind(var("Y"), parse("@1 f{Z ^1}"))
- );
- }
-
-
@Test
public void testUnifyExternalRef() throws Exception {
Term termRef = ref(parse("f {a f{b f{c d}}}"));
@@ -604,12 +476,36 @@ public class SolverTests {
@Test
public void testFailCyclic() throws Exception {
+ assertUnificationFails(
+ term("g", ref(parse("f {h X}"))),
+ term("g", var("X")),
+
+ CYCLE_DETECTED
+ );
+ assertUnificationFails(
+ parse("t {@1 f {h X} g {f {h X}}}"),
+ parse("t {Y g {X}}"),
+
+ CYCLE_DETECTED
+ );
+ assertUnificationFails(
+ parse("a{b X}"),
+ parse("X"),
+
+ CYCLE_DETECTED
+ );
assertUnificationFails(
parse("f{X}"),
parse("X"),
CYCLE_DETECTED
);
+ assertUnificationFails(
+ parse("X"),
+ parse("f{X}"),
+
+ CYCLE_DETECTED
+ );
assertUnificationFails(
parse("f{f{X}}"),
parse("f{X}"),
@@ -632,6 +528,18 @@ public class SolverTests {
parse("a{ b{c{b{c{b{c{^2}}}}}} @2 b{c{b{c{^2}}}}}"),
parse("a{ b{Y} b{Y} }"),
+ CYCLE_DETECTED
+ );
+ assertUnificationFails(
+ parse("t {@1 f {h X} g {f {h X}}}"),
+ parse("t {Y g {X}}"),
+
+ CYCLE_DETECTED
+ );
+ assertUnificationFails(
+ parse("t {@1 f {h X} g {^1}}"),
+ parse("t {Y g {X}}"),
+
CYCLE_DETECTED
);
}