modified: src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java

modified:   src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
methodsignature so eingerichtet, dass die Constraints erst am Ende hinzugefuegt werden.
This commit is contained in:
pl@gohorb.ba-horb.de 2023-02-08 16:52:23 +01:00
parent d39fd64f0f
commit 2d117e24cf
2 changed files with 57 additions and 43 deletions

View File

@ -17,11 +17,13 @@ import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
public class TypeUnify2Task extends TypeUnifyTask { public class TypeUnify2Task extends TypeUnifyTask {
Set<Set<UnifyPair>> setToFlatten; Set<Set<UnifyPair>> setToFlatten;
Set<UnifyPair> methodSignatureConstraintUebergabe;
public TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, Set<UnifyPair> nextSetElement, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks) { public TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, Set<UnifyPair> nextSetElement, IFiniteClosure fc, boolean parallel, Writer logFile, Boolean log, int rekTiefe, UnifyResultModel urm, UnifyTaskModel usedTasks, Set<UnifyPair> methodSignatureConstraintUebergabe) {
super(eq, oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); super(eq, oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, usedTasks);
this.setToFlatten = setToFlatten; this.setToFlatten = setToFlatten;
this.nextSetElement = nextSetElement; this.nextSetElement = nextSetElement;
this.methodSignatureConstraintUebergabe = methodSignatureConstraintUebergabe;
} }
Set<UnifyPair> getNextSetElement() { Set<UnifyPair> getNextSetElement() {
@ -34,7 +36,7 @@ public class TypeUnify2Task extends TypeUnifyTask {
System.out.println("two"); System.out.println("two");
} }
one = true; one = true;
Set<Set<UnifyPair>> res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField, false); Set<Set<UnifyPair>> res = unify2(setToFlatten, eq, oderConstraintsField, fc, parallel, rekTiefeField, methodSignatureConstraintUebergabe);
/*if (isUndefinedPairSetSet(res)) { /*if (isUndefinedPairSetSet(res)) {
return new HashSet<>(); } return new HashSet<>(); }
else else

View File

@ -260,7 +260,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
ArrayList<Set<Constraint<UnifyPair>>> remainingOderconstraints = oderConstraintsField.stream() ArrayList<Set<Constraint<UnifyPair>>> remainingOderconstraints = oderConstraintsField.stream()
.filter(x -> x.size()>1) .filter(x -> x.size()>1)
.collect(Collectors.toCollection(ArrayList::new)); .collect(Collectors.toCollection(ArrayList::new));
Set<Set<UnifyPair>> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField, false); Set<Set<UnifyPair>> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField, new HashSet<>());
noOfThread--; noOfThread--;
try { try {
logFile.close(); logFile.close();
@ -305,7 +305,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
* @param fc The finite closure * @param fc The finite closure
* @return The set of all principal type unifiers * @return The set of all principal type unifiers
*/ */
protected Set<Set<UnifyPair>> unify(final Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, boolean sameEq) { protected Set<Set<UnifyPair>> unify(final Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set<UnifyPair> methodSignatureConstraint) {
//Set<UnifyPair> aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT) //Set<UnifyPair> aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT)
// ).collect(Collectors.toCollection(HashSet::new)); // ).collect(Collectors.toCollection(HashSet::new));
//writeLog(nOfUnify.toString() + " AA: " + aas.toString()); //writeLog(nOfUnify.toString() + " AA: " + aas.toString());
@ -484,12 +484,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
//Aufruf von computeCartesianRecursive ANFANG //Aufruf von computeCartesianRecursive ANFANG
//writeLog("topLevelSets: " + topLevelSets.toString()); //writeLog("topLevelSets: " + topLevelSets.toString());
return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, sameEq); return computeCartesianRecursive(new ArrayList<>(topLevelSets), eq, oderConstraintsOutput, fc, parallel, rekTiefe, methodSignatureConstraint);
} }
Set<Set<UnifyPair>> unify2(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, boolean sameEq) { Set<Set<UnifyPair>> unify2(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set<UnifyPair> methodSignatureConstraint) {
//Aufruf von computeCartesianRecursive ENDE //Aufruf von computeCartesianRecursive ENDE
//keine Ahnung woher das kommt //keine Ahnung woher das kommt
@ -574,16 +574,34 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
eqPrimePrimeSet.add(eqPrime); eqPrimePrimeSet.add(eqPrime);
if (finalresult && isSolvedForm(eqPrime)) { if (finalresult && isSolvedForm(eqPrime)) {
writeLog("eqPrime:" + eqPrime.toString()+"\n"); writeLog("eqPrime:" + eqPrime.toString()+"\n");
/* methodconstraintsets werden zum Ergebnis hinzugefuegt
* Anfang
*/
//System.out.println("methodSignatureConstraint Return: " + methodSignatureConstraint);
eqPrimePrimeSet.forEach(x -> x.addAll(methodSignatureConstraint));
//Substitutionen in methodcontraintsets werdne ausgeführt
eqPrimePrimeSet = eqPrimePrimeSet.stream().map(
x -> { Optional<Set<UnifyPair>> help = rules.subst(x);
return help.isPresent() ?
help.get():
x; }).collect(Collectors.toSet());
/*
* Ende
*/
urm.notify(eqPrimePrimeSet); urm.notify(eqPrimePrimeSet);
} }
} }
else if(eqPrimePrime.isPresent()) { else if(eqPrimePrime.isPresent()) {
Set<Set<UnifyPair>> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe, sameEq); Set<Set<UnifyPair>> unifyres = unifyres1 = unify(eqPrimePrime.get(), newOderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint);
eqPrimePrimeSet.addAll(unifyres); eqPrimePrimeSet.addAll(unifyres);
} }
else { else {
Set<Set<UnifyPair>> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe, sameEq); Set<Set<UnifyPair>> unifyres = unifyres2 = unify(eqPrime, newOderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint);
eqPrimePrimeSet.addAll(unifyres); eqPrimePrimeSet.addAll(unifyres);
@ -625,7 +643,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
* @param rekTiefe Deep of recursive calls * @param rekTiefe Deep of recursive calls
* @return The set of all principal type unifiers * @return The set of all principal type unifiers
*/ */
Set<Set<UnifyPair>> computeCartesianRecursive(ArrayList<Set<? extends Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, boolean sameEq) { Set<Set<UnifyPair>> computeCartesianRecursive(ArrayList<Set<? extends Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Constraint<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe, Set<UnifyPair> methodSignatureConstraint) {
//oneElems: Alle 1-elementigen Mengen, die nur ein Paar //oneElems: Alle 1-elementigen Mengen, die nur ein Paar
//a <. theta, theta <. a oder a =. theta enthalten //a <. theta, theta <. a oder a =. theta enthalten
@ -639,7 +657,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Optional<Set<? extends Set<UnifyPair>>> optNextSet = topLevelSets.stream().filter(x -> x.size()>1).findAny(); Optional<Set<? extends Set<UnifyPair>>> optNextSet = topLevelSets.stream().filter(x -> x.size()>1).findAny();
if (!optNextSet.isPresent()) {//Alle Elemente sind 1-elementig if (!optNextSet.isPresent()) {//Alle Elemente sind 1-elementig
Set<Set<UnifyPair>> result = unify2(oneElems, eq, oderConstraints, fc, parallel, rekTiefe, sameEq); Set<Set<UnifyPair>> result = unify2(oneElems, eq, oderConstraints, fc, parallel, rekTiefe, methodSignatureConstraint);
return result; return result;
} }
@ -849,6 +867,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
} }
} }
if (oderConstraint) {
methodSignatureConstraint.addAll(((Constraint<UnifyPair>)a).getmethodSignatureConstraint());
System.out.println("ERSTELLUNG: " +methodSignatureConstraint);
}
i++; i++;
Set<Set<UnifyPair>> elems = new HashSet<Set<UnifyPair>>(oneElems); Set<Set<UnifyPair>> elems = new HashSet<Set<UnifyPair>>(oneElems);
writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n"); writeLog("a1: " + rekTiefe + " "+ "variance: "+ variance + " " + a.toString()+ "\n");
@ -882,7 +905,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
newElemsOrig.add(a); newElemsOrig.add(a);
/* FORK ANFANG */ /* FORK ANFANG */
TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraint);
//forks.add(forkOrig); //forks.add(forkOrig);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -917,7 +940,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Set<Set<UnifyPair>> newElems = new HashSet<>(elems); Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints); List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
newElems.add(nSaL); newElems.add(nSaL);
TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint));
forks.add(fork); forks.add(fork);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -981,7 +1004,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
newElemsOrig.add(a); newElemsOrig.add(a);
/* FORK ANFANG */ /* FORK ANFANG */
TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint));
//forks.add(forkOrig); //forks.add(forkOrig);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -1016,7 +1039,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Set<Set<UnifyPair>> newElems = new HashSet<>(elems); Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints); List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
newElems.add(nSaL); newElems.add(nSaL);
TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint));
forks.add(fork); forks.add(fork);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -1081,7 +1104,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
newElemsOrig.add(a); newElemsOrig.add(a);
/* FORK ANFANG */ /* FORK ANFANG */
TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task forkOrig = new TypeUnify2Task(newElemsOrig, newEqOrig, newOderConstraintsOrig, a, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, new HashSet<>(methodSignatureConstraint));
//forks.add(forkOrig); //forks.add(forkOrig);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -1102,7 +1125,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
Set<Set<UnifyPair>> newElems = new HashSet<>(elems); Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints); List<Set<Constraint<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
newElems.add(nSaL); newElems.add(nSaL);
TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks); TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, nSaL, fc, parallel, logFile, log, rekTiefe, urm, usedTasks, methodSignatureConstraint);
forks.add(fork); forks.add(fork);
synchronized(usedTasks) { synchronized(usedTasks) {
if (this.myIsCancelled()) { if (this.myIsCancelled()) {
@ -1153,16 +1176,13 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
//noOfThread++; //noOfThread++;
} else {//parallel = false oder MaxNoOfThreads ist erreicht, sequentiell weiterarbeiten } else {//parallel = false oder MaxNoOfThreads ist erreicht, sequentiell weiterarbeiten
elems.add(a); //PL 2019-01-16 muss das wirklich hin steht schon in Zeile 859 ja braucht man siehe Zeile 859 elems.add(a); //PL 2019-01-16 muss das wirklich hin steht schon in Zeile 859 ja braucht man siehe Zeile 859
res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe, sameEq); res = unify2(elems, eq, oderConstraints, fc, parallel, rekTiefe, new HashSet<>(methodSignatureConstraint));
}}} }}}
//Ab hier alle parallele Berechnungen wieder zusammengeführt. //Ab hier alle parallele Berechnungen wieder zusammengeführt.
Set<UnifyPair> methodSignatureConstraint =
oderConstraint ?
((Constraint<UnifyPair>)a).getmethodSignatureConstraint()
: new HashSet<>();
if (oderConstraint) { if (oderConstraint) {
System.out.println("ERSTELLUNG: " +methodSignatureConstraint); methodSignatureConstraint.removeAll(((Constraint<UnifyPair>)a).getmethodSignatureConstraint());
System.out.println("REMOVE: " +methodSignatureConstraint);
} }
if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) { if (!isUndefinedPairSetSet(res) && isUndefinedPairSetSet(result)) {
//wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen //wenn korrektes Ergebnis gefunden alle Fehlerfaelle loeschen
@ -1456,6 +1476,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
System.out.println(); System.out.println();
} }
writeLog("nextSetasList vor filter-Aufruf: " + nextSetasList); writeLog("nextSetasList vor filter-Aufruf: " + nextSetasList);
if (!oderConstraint) {
nextSetasList = nextSetasList.stream().filter(x -> { nextSetasList = nextSetasList.stream().filter(x -> {
//Boolean ret = false; //Boolean ret = false;
//for (PlaceholderType var : vars) { //for (PlaceholderType var : vars) {
@ -1464,6 +1485,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
return (!x.containsAll(durchschnitt)); return (!x.containsAll(durchschnitt));
})//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) //fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10 })//.filter(y -> couldBecorrect(reducedUndefResSubstGroundedBasePair, y)) //fuer testzwecke auskommentiert um nofstred zu bestimmen PL 2018-10-10
.collect(Collectors.toCollection(ArrayList::new)); .collect(Collectors.toCollection(ArrayList::new));
}
writeLog("nextSetasList nach filter-Aufruf: " + nextSetasList); writeLog("nextSetasList nach filter-Aufruf: " + nextSetasList);
nofstred = nextSetasList.size(); nofstred = nextSetasList.size();
//NOCH NICHT korrekt PL 2018-10-12 //NOCH NICHT korrekt PL 2018-10-12
@ -1492,17 +1514,6 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
//} //}
//else result.stream().filter(y -> !isUndefinedPairSet(y)); //else result.stream().filter(y -> !isUndefinedPairSet(y));
writeLog("res: " + res.toString()); writeLog("res: " + res.toString());
if (oderConstraint && !sameEq && !isUndefinedPairSetSet(result)) {
System.out.println("methodSignatureConstraint Return: " + methodSignatureConstraint);
result.forEach(x -> x.addAll(methodSignatureConstraint));
/*
result = result.stream().map(
x -> { Optional<Set<UnifyPair>> help = rules.subst(x);
return help.isPresent() ?
help.get():
x; }).collect(Collectors.toSet());
*/
}
} }
//2020-02-02: if (variance ==2) Hier Aufruf von filterOverriding einfuegen //2020-02-02: if (variance ==2) Hier Aufruf von filterOverriding einfuegen
writeLog("Return computeCR: " + result.toString()); writeLog("Return computeCR: " + result.toString());
@ -1542,7 +1553,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
unitedSubst.addAll(sameEq.getAllBases()); unitedSubst.addAll(sameEq.getAllBases());
localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); localEq.add(new UnifyPair(aPair.getRhsType(), sameEq.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
finalresult = false; finalresult = false;
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, true); Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, new HashSet<>());
finalresult = true; finalresult = true;
if (isUndefinedPairSetSet(localRes)) { if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) { if (result.isEmpty() || isUndefinedPairSetSet(result)) {
@ -1560,7 +1571,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
unitedSubst.addAll(sameEq.getAllBases()); unitedSubst.addAll(sameEq.getAllBases());
localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null)); localEq.add(new UnifyPair(sameEq.getLhsType(), aPair.getRhsType(), sameEq.getPairOp(), unitedSubst, null));
finalresult = false; finalresult = false;
Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, true); Set<Set<UnifyPair>> localRes = unify(localEq, new ArrayList<>(), fc, false, 0, new HashSet<>());
finalresult = true; finalresult = true;
if (isUndefinedPairSetSet(localRes)) { if (isUndefinedPairSetSet(localRes)) {
if (result.isEmpty() || isUndefinedPairSetSet(result)) { if (result.isEmpty() || isUndefinedPairSetSet(result)) {
@ -1971,6 +1982,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>> {
.findAny()).isPresent() .findAny()).isPresent()
&& optElem.get().getRhsType() instanceof ExtendsType);}) && optElem.get().getRhsType() instanceof ExtendsType);})
.collect(Collectors.toSet()); .collect(Collectors.toSet());
ret.stream().forEach(x -> x.stream().forEach(y -> { Set<UnifyPair> x_new = new HashSet<>(x); //PL 2020-03-18: y selbst darf nicht in die Substitutionen ret.stream().forEach(x -> x.stream().forEach(y -> { Set<UnifyPair> x_new = new HashSet<>(x); //PL 2020-03-18: y selbst darf nicht in die Substitutionen
x_new.remove(y); x_new.remove(y);
y.addSubstitutions(x_new); y.addSubstitutions(x_new);