new file: src/main/java/de/dhbwstuttgart/typeinference/unify/PartialOrderSet.java

modified:   src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java
	modified:   src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify2Task.java
	modified:   src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
PartialOrderSet implemetiert und in TypeUnify, TypeUnify2Task, TypeUnifyTask eingepasst

src/main/java/de/dhbwstuttgart/typeinference/unify/PartialOrderSet.java

@@ -0,0 +1,120 @@
+package de.dhbwstuttgart.typeinference.unify;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.Set;
+import java.util.Vector;
+
+import com.google.common.collect.Ordering;
+
+public class PartialOrderSet<E, F extends Ordering<E>> implements Set<E> {
+
+	HashSet<E> hs = new HashSet<>();
+	Vector<E> ve = new Vector<>();
+	F ordering;
+	
+	PartialOrderSet(F ordering) {
+		this.ordering= ordering;
+	}
+
+	PartialOrderSet(F ordering, Set<E> s) {
+		this.ordering= ordering;
+		this.addAll(s);
+	}
+	@Override
+	public int size() {
+		return ve.size();
+	}
+
+	@Override
+	public boolean isEmpty() {
+		return ve.isEmpty();
+	}
+
+	@Override
+	public boolean contains(Object o) {
+		return hs.contains(o);
+	}
+
+	@Override
+	public Iterator<E> iterator() {
+		return ve.iterator();
+	}
+
+	@Override
+	public Object[] toArray() {
+		return ve.toArray();
+	}
+
+	@Override
+	public <T> T[] toArray(T[] a) {
+		return ve.toArray(a);
+	}
+
+	public ArrayList<E> toArrayList() {
+		return new ArrayList<>(ve);
+	}
+	
+	@Override
+	public boolean add(E e) {
+		if (this.contains(e)) {
+			return false;
+		}
+		hs.add(e);
+		for(int i = 0; i< ve.size(); i++) { 
+			if (ordering.compare(e, ve.elementAt(i)) == -1) {
+				ve.insertElementAt(e, i);
+				return true;
+			}
+		}
+		ve.addElement(e);
+		return true;
+	}
+
+	@Override
+	public boolean remove(Object o) {
+		hs.remove(o);
+		return ve.remove(o);
+	}
+
+	@Override
+	public boolean containsAll(Collection<?> c) {
+		return hs.containsAll(c);
+	}
+
+	@Override
+	public boolean addAll(Collection<? extends E> c) {
+		Boolean ret = false;
+		Iterator<? extends E> cit = c.iterator(); 
+		while(cit.hasNext()) {
+			Boolean retnew = this.add(cit.next());
+			ret = ret || retnew;
+		}
+		return ret;
+	}
+
+	@Override
+	public boolean retainAll(Collection<?> c) {
+		hs.retainAll(c);
+		return ve.retainAll(c);
+	}
+
+	@Override
+	public boolean removeAll(Collection<?> c) {
+		hs.removeAll(c);
+		return ve.removeAll(c);
+	}
+
+	@Override
+	public void clear() {
+		hs.clear();
+		ve.clear();
+	}
+	
+	@Override
+	public String toString() {
+		return ve.toString();
+	}
+}

src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnify.java

@@ -1,20 +1,25 @@
 package de.dhbwstuttgart.typeinference.unify;
 
 import java.io.FileWriter;
+import java.util.ArrayList;
 import java.util.List;
 import java.util.Set;
 import java.util.concurrent.ForkJoinPool;
+import java.util.stream.Collectors;
 
 import de.dhbwstuttgart.typeinference.constraints.Constraint;
 import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
 import de.dhbwstuttgart.typeinference.constraints.Pair;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
 
 public class TypeUnify {
 	public Set<Set<UnifyPair>> unify(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, FileWriter logFile, Boolean log, ConstraintSet<Pair> cons) {
-		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, new UnifyResultModel(), cons);
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsPartial = 
+				oderConstraints.stream().map(x -> new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc),x)).collect(Collectors.toList());
+		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraintsPartial, fc, true, logFile, log, 0, new UnifyResultModel(), cons);
 		ForkJoinPool pool = new ForkJoinPool();
 		pool.invoke(unifyTask);
 		Set<Set<UnifyPair>> res =  unifyTask.join();
@@ -22,14 +27,18 @@ public class TypeUnify {
 	}
 	
 	public UnifyResultModel unifyAsync(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, FileWriter logFile, Boolean log, ConstraintSet<Pair> cons, UnifyResultModel ret) {
-		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, cons);
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsPartial = 
+				oderConstraints.stream().map(x -> new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc),x)).collect(Collectors.toList());
+		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraintsPartial, fc, true, logFile, log, 0, ret, cons);
 		ForkJoinPool pool = new ForkJoinPool();
 		pool.invoke(unifyTask);
 		return ret;
 	}
 	
 	public UnifyResultModel unifyParallel(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, FileWriter logFile, Boolean log, ConstraintSet<Pair> cons, UnifyResultModel ret) {
-		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, true, logFile, log, 0, ret, cons);
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsPartial = 
+				oderConstraints.stream().map(x -> new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc),x)).collect(Collectors.toList());
+		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraintsPartial, fc, true, logFile, log, 0, ret, cons);
 		ForkJoinPool pool = new ForkJoinPool();
 		pool.invoke(unifyTask);
 		Set<Set<UnifyPair>> res =  unifyTask.join();
@@ -45,7 +54,9 @@ public class TypeUnify {
 	*/
 	
 	public Set<Set<UnifyPair>> unifyOderConstraints(Set<UnifyPair> undConstrains, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, FileWriter logFile, Boolean log, ConstraintSet<Pair> cons) {
-		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraints, fc, false, logFile, log, 0, new UnifyResultModel(), cons);
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsPartial = 
+				oderConstraints.stream().map(x -> new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc),x)).collect(Collectors.toList());
+		TypeUnifyTask unifyTask = new TypeUnifyTask(undConstrains, oderConstraintsPartial, fc, false, logFile, log, 0, new UnifyResultModel(), cons);
 		Set<Set<UnifyPair>> res = unifyTask.compute();
 		return res;
 	}

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

@@ -9,13 +9,14 @@ import de.dhbwstuttgart.typeinference.constraints.Constraint;
 import de.dhbwstuttgart.typeinference.constraints.ConstraintSet;
 import de.dhbwstuttgart.typeinference.constraints.Pair;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.model.OrderingUnifyPair;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyPair;
 
 public class TypeUnify2Task extends TypeUnifyTask {
        
        Set<Set<UnifyPair>> setToFlatten;
 
-       public TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log, int rekTiefe, UnifyResultModel urm, ConstraintSet<Pair> cons) {
+       public TypeUnify2Task(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraints, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log, int rekTiefe, UnifyResultModel urm, ConstraintSet<Pair> cons) {
                super(eq, oderConstraints, fc, parallel, logFile, log, rekTiefe, urm, cons);
                this.setToFlatten = setToFlatten;
        }

src/main/java/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java

@@ -90,7 +90,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	protected Set<UnifyPair> eq; //und-constraints
 	
-	protected List<Set<Set<UnifyPair>>> oderConstraintsField;
+	protected List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsField;
 	
 	protected IFiniteClosure fc;
 	
@@ -128,7 +128,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	}
 	*/
 	
-	public TypeUnifyTask(Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log, int rekTiefe, UnifyResultModel urm, ConstraintSet<de.dhbwstuttgart.typeinference.constraints.Pair> cons2) {
+	public TypeUnifyTask(Set<UnifyPair> eq, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraints, IFiniteClosure fc, boolean parallel, FileWriter logFile, Boolean log, int rekTiefe, UnifyResultModel urm, ConstraintSet<de.dhbwstuttgart.typeinference.constraints.Pair> cons2) {
 		synchronized (this) { 
 			this.eq = eq;
 			//this.oderConstraints = oderConstraints.stream().map(x -> x.stream().map(y -> new HashSet<>(y)).collect(Collectors.toSet(HashSet::new))).collect(Collectors.toList(ArrayList::new));
@@ -203,7 +203,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		oderConstraintsField.stream()
         	.filter(x -> x.size()==1)
         	.map(y -> y.stream().findFirst().get()).forEach(x -> neweq.addAll(x));
-		ArrayList<Set<Set<UnifyPair>>> remainingOderconstraints = oderConstraintsField.stream()
+		ArrayList<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> remainingOderconstraints = oderConstraintsField.stream()
 				.filter(x -> x.size()>1)
 				.collect(Collectors.toCollection(ArrayList::new));
 		Set<Set<UnifyPair>> res = unify(neweq, remainingOderconstraints, fc, parallel, rekTiefeField);
@@ -477,7 +477,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	 * @param fc The finite closure
 	 * @return The set of all principal type unifiers
 	 */
-	protected Set<Set<UnifyPair>> unify(final Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe)  {
+	protected Set<Set<UnifyPair>> unify(final Set<UnifyPair> eq, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe)  {
 		//Set<UnifyPair> aas = eq.stream().filter(x -> x.getLhsType().getName().equals("AA") //&& x.getPairOp().equals(PairOperator.SMALLERDOT)
 		//		).collect(Collectors.toCollection(HashSet::new));
 		//writeLog(nOfUnify.toString() + " AA: " + aas.toString());
@@ -531,12 +531,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		
 		// There are up to 10 toplevel set. 8 of 10 are the result of the 
 		// cartesian product of the sets created by pattern matching.
-		List<Set<Set<UnifyPair>>> topLevelSets = new ArrayList<>();
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> topLevelSets = new ArrayList<>();
 		
 		//System.out.println(eq2s);
 		
 		if(eq1s.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
-			Set<Set<UnifyPair>> wrap = new HashSet<>();
+			PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> wrap = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 			wrap.add(eq1s);
 			topLevelSets.add(wrap); // Add Eq1'
 		}
@@ -547,7 +547,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				.collect(Collectors.toSet());
 		
 		if(bufferSet.size() != 0) { // Do not add empty sets or the cartesian product will always be empty.
-			Set<Set<UnifyPair>> wrap = new HashSet<>();
+			PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> wrap = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 			wrap.add(bufferSet);
 			topLevelSets.add(wrap);
 			eq2s.removeAll(bufferSet);
@@ -558,8 +558,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		Set<UnifyPair> undefinedPairs = new HashSet<>();
 		if (printtag) System.out.println("eq2s " + eq2s);
 		//writeLog("BufferSet: " + bufferSet.toString()+"\n");
-		List<Set<Set<UnifyPair>>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints);
+		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsOutput = new ArrayList<>();//new ArrayList<>(oderConstraints);
-		Set<Set<Set<Set<UnifyPair>>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput);
+		Set<Set<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>>> secondLevelSets = calculatePairSets(eq2s, oderConstraints, fc, undefinedPairs, oderConstraintsOutput);
 		                                                //PL 2017-09-20: Im calculatePairSets wird möglicherweise O .< java.lang.Integer 
 		                                                //nicht ausgewertet Faculty Beispiel im 1. Schritt
 		                                                //PL 2017-10-03 geloest, muesste noch mit FCs mit kleineren
@@ -606,8 +606,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		*/
 		
 		//Alternative KEIN KARTESISCHES PRODUKT der secondlevel Ebene bilden
-		for(Set<Set<Set<UnifyPair>>> secondLevelSet : secondLevelSets) {
+		for(Set<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> secondLevelSet : secondLevelSets) {
-			for (Set<Set<UnifyPair>> secondlevelelem : secondLevelSet) {
+			for (PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> secondlevelelem : secondLevelSet) {
 				topLevelSets.add(secondlevelelem);
 			}
 		}
@@ -622,7 +622,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	}
 	
 	
-	Set<Set<UnifyPair>> unify2(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
+	Set<Set<UnifyPair>> unify2(Set<Set<UnifyPair>> setToFlatten, Set<UnifyPair> eq, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
 		//Aufruf von computeCartesianRecursive ENDE
 		
 		//keine Ahnung woher das kommt
@@ -747,22 +747,22 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	
 	
 	
-	Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<Set<Set<UnifyPair>>> topLevelSets, Set<UnifyPair> eq, List<Set<Set<UnifyPair>>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
+	Set<Set<UnifyPair>> computeCartesianRecursive(Set<Set<UnifyPair>> fstElems, ArrayList<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> topLevelSets, Set<UnifyPair> eq, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraints, IFiniteClosure fc, boolean parallel, int rekTiefe) {
 		//ArrayList<Set<Set<UnifyPair>>> remainingSets = new ArrayList<>(topLevelSets);
 		fstElems.addAll(topLevelSets.stream()
 				                    .filter(x -> x.size()==1)
 				                    .map(y -> y.stream().findFirst().get())
 				                    .collect(Collectors.toCollection(HashSet::new)));
-		ArrayList<Set<Set<UnifyPair>>> remainingSets = topLevelSets.stream()
+		ArrayList<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> remainingSets = topLevelSets.stream()
 				                                                   .filter(x -> x.size()>1)
 				                                                   .collect(Collectors.toCollection(ArrayList::new));
 		if (remainingSets.isEmpty()) {//Alle Elemente sind 1-elementig
 			Set<Set<UnifyPair>> result = unify2(fstElems, eq, oderConstraints, fc, parallel, rekTiefe);
 			return result;
 		}
-		Set<Set<UnifyPair>> nextSet = remainingSets.remove(0);
+		PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> nextSet = remainingSets.remove(0);
 		writeLog("nextSet: " + nextSet.toString());
-		List<Set<UnifyPair>> nextSetasList =new ArrayList<>(nextSet);
+		List<Set<UnifyPair>> nextSetasList = nextSet.toArrayList();
 		try {
 		//List<Set<UnifyPair>> 
 			//nextSetasList = oup.sortedCopy(nextSet);//new ArrayList<>(nextSet);
@@ -819,7 +819,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			//List<Set<UnifyPair>> nextSetasListRestMin = new ArrayList<>();
 			//List<Set<UnifyPair>> nextSetasListRestOder = new ArrayList<>();
 			if (variance == 1) {
-				a = oup.max(nextSetasList.iterator());
+				//a = oup.max(nextSetasList.iterator());
+				a = nextSetasList.get(nextSetasList.size()-1);
 				nextSetasList.remove(a);
 				nextSetasListRest = new ArrayList<>(nextSetasList);
 				Iterator<Set<UnifyPair>> nextSetasListItRest = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
@@ -849,7 +850,8 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				
 			}
 			else if (variance == -1) {
-				a = oup.min(nextSetasList.iterator());
+				//a = oup.min(nextSetasList.iterator());
+				a = nextSetasList.get(0);
 				nextSetasList.remove(a);
 				nextSetasListRest = new ArrayList<>(nextSetasList);
 				Iterator<Set<UnifyPair>> nextSetasListItRest = new ArrayList<Set<UnifyPair>>(nextSetasListRest).iterator();
@@ -922,7 +924,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				Set<TypeUnifyTask> forks = new HashSet<>();
 				Set<UnifyPair> newEqOrig = new HashSet<>(eq);
 				Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
-				List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
+				List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
 				newElemsOrig.add(a);
 				
 				/* FORK ANFANG */
@@ -942,7 +944,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					}
 					Set<UnifyPair> newEq = new HashSet<>(eq);
 					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
-					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
+					List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraints = new ArrayList<>(oderConstraints);
 					newElems.add(nSaL);
 					TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, fc, parallel, logFile, log, rekTiefe, urm, cons);
 					forks.add(fork);
@@ -973,7 +975,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				Set<TypeUnifyTask> forks = new HashSet<>();
 				Set<UnifyPair> newEqOrig = new HashSet<>(eq);
 				Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
-				List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
+				List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
 				newElemsOrig.add(a);
 				
 				/* FORK ANFANG */
@@ -993,7 +995,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					}
 					Set<UnifyPair> newEq = new HashSet<>(eq);
 					Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
-					List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
+					List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraints = new ArrayList<>(oderConstraints);
 					newElems.add(nSaL);
 					TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, fc, parallel, logFile, log, rekTiefe, urm, cons);
 					forks.add(fork);
@@ -1025,7 +1027,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		    	Set<TypeUnifyTask> forks = new HashSet<>();
 		    	Set<UnifyPair> newEqOrig = new HashSet<>(eq);
 		    	Set<Set<UnifyPair>> newElemsOrig = new HashSet<>(elems);
-		    	List<Set<Set<UnifyPair>>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
+		    	List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraintsOrig = new ArrayList<>(oderConstraints);
 		    	newElemsOrig.add(a);
 				
 				/* FORK ANFANG */
@@ -1043,7 +1045,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		    		//nextSetasList.remove(nSaL);
 		    		Set<UnifyPair> newEq = new HashSet<>(eq);
 		    		Set<Set<UnifyPair>> newElems = new HashSet<>(elems);
-		    		List<Set<Set<UnifyPair>>> newOderConstraints = new ArrayList<>(oderConstraints);
+		    		List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> newOderConstraints = new ArrayList<>(oderConstraints);
 		    		newElems.add(nSaL);
 		    		TypeUnify2Task fork = new TypeUnify2Task(newElems, newEq, newOderConstraints, fc, parallel, logFile, log, rekTiefe, urm, cons);
 		    		forks.add(fork);
@@ -1665,9 +1667,9 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	 * from the pairs that matched the case. Each generated set contains singleton sets or sets with few elements
 	 * (as in case 1 where sigma is added to the innermost set).
 	 */
-	protected Set<Set<Set<Set<UnifyPair>>>> calculatePairSets(Set<UnifyPair> eq2s, List<Set<Set<UnifyPair>>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<Set<Set<UnifyPair>>> oderConstraintsOutput) {
+	protected Set<Set<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>>> calculatePairSets(Set<UnifyPair> eq2s, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsInput, IFiniteClosure fc, Set<UnifyPair> undefined, List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsOutput) {
 		oderConstraintsOutput.addAll(oderConstraintsInput);
-		List<Set<Set<Set<UnifyPair>>>> result = new ArrayList<>(9);
+		List<Set<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>>> result = new ArrayList<>(9);
 
 		// Init all 8 cases + 9. Case: oderConstraints
 		for(int i = 0; i < 9; i++)
@@ -1686,7 +1688,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			}
 		}
 		if (eq2sAsList.isEmpty()) {
-			List<Set<Set<UnifyPair>>> oderConstraintsVariance = oderConstraintsOutput.stream() //Alle Elemente rauswerfen, die Variance 0 haben oder keine TPH in LHS oder RHS sind
+			List<PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>> oderConstraintsVariance = oderConstraintsOutput.stream() //Alle Elemente rauswerfen, die Variance 0 haben oder keine TPH in LHS oder RHS sind
 			.filter(x -> x.stream()
 					.filter(y -> 
 						y.stream().filter(z -> ((z.getLhsType() instanceof PlaceholderType) 
@@ -1696,7 +1698,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 								     ).findFirst().isPresent()
 					).findFirst().isPresent()).collect(Collectors.toList());
 			if (!oderConstraintsVariance.isEmpty()) {
-				Set<Set<UnifyPair>> ret = oderConstraintsVariance.get(0);
+				PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> ret = oderConstraintsVariance.get(0);
 				oderConstraintsOutput.remove(ret);
 				//Set<UnifyPair> retFlat = new HashSet<>(); 
 			    //ret.stream().forEach(x -> retFlat.addAll(x)); 
@@ -1710,7 +1712,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 		
 		if (eq2sAsList.isEmpty() && first) {//Alle eq2s sind empty und alle oderConstraints mit Variance != 0 sind bearbeitet 
 			if (!oderConstraintsOutput.isEmpty()) {
-				Set<Set<UnifyPair>> ret = oderConstraintsOutput.remove(0);
+				PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> ret = oderConstraintsOutput.remove(0);
 				//if (ret.iterator().next().iterator().next().getLhsType().getName().equals("M"))
 				//	System.out.println("M");
 				//Set<UnifyPair> retFlat = new HashSet<>(); 
@@ -1736,7 +1738,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 					if (((PlaceholderType)(pair.getLhsType())).getName().equals("AR")) {
 						System.out.println("AR");
 					}
-					Set<Set<UnifyPair>> x1 = unifyCase1(pair, fc);
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> x1 = unifyCase1(pair, fc);
 					if (pairOp == PairOperator.SMALLERNEQDOT) {
 						Set<UnifyPair> remElem = new HashSet<>();
 						remElem.add(new UnifyPair(pair.getLhsType(), pair.getRhsType(), PairOperator.EQUALSDOT));
@@ -1757,7 +1759,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
 					s1.add(pair);
-					Set<Set<UnifyPair>> s2 = new HashSet<>();
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> s2 = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 					s2.add(s1);
 					result.get(0).add(s2);
 				}
@@ -1766,7 +1768,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 2: (a <.? ? ext Theta')
 			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					Set<Set<UnifyPair>> x1 = unifyCase2(pair, fc);
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> x1 = unifyCase2(pair, fc);
 					result.get(1).add(x1);
 					if (x1.isEmpty()) {
 						undefined.add(pair); //Theta ist nicht im FC
@@ -1775,7 +1777,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
 					s1.add(pair);
-					Set<Set<UnifyPair>> s2 = new HashSet<>();
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> s2 = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 					s2.add(s1);
 					result.get(1).add(s2);
 				}
@@ -1783,7 +1785,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 3: (a <.? ? sup Theta')
 			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					Set<Set<UnifyPair>> x1 = unifyCase3(pair, fc);
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> x1 = unifyCase3(pair, fc);
 					result.get(2).add(x1);
 					if (x1.isEmpty()) {
 						undefined.add(pair); //Theta ist nicht im FC
@@ -1792,7 +1794,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
 					s1.add(pair);
-					Set<Set<UnifyPair>> s2 = new HashSet<>();
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> s2 = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 					s2.add(s1);
 					result.get(2).add(s2);
 				}
@@ -1805,7 +1807,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 5: (Theta <. a)
 			else if ((pairOp == PairOperator.SMALLERDOT) && rhsType instanceof PlaceholderType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					Set<Set<UnifyPair>> x1 = unifyCase5(pair, fc);
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> x1 = unifyCase5(pair, fc);
 					result.get(4).add(x1);
 					if (x1.isEmpty()) {
 						undefined.add(pair); //Theta ist nicht im FC
@@ -1814,7 +1816,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
 					s1.add(pair);
-					Set<Set<UnifyPair>> s2 = new HashSet<>();
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> s2 = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 					s2.add(s1);
 					result.get(4).add(s2);
 				}
@@ -1832,7 +1834,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 8: (Theta <.? a)
 			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					Set<Set<UnifyPair>> x1 = unifyCase8(pair, fc);
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> x1 = unifyCase8(pair, fc);
 					result.get(7).add(x1);
 					if (x1.isEmpty()) {
 						undefined.add(pair); //Theta ist nicht im FC
@@ -1841,7 +1843,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
 					s1.add(pair);
-					Set<Set<UnifyPair>> s2 = new HashSet<>();
+					PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> s2 = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 					s2.add(s1);
 					result.get(7).add(s2);
 				}
@@ -1865,12 +1867,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian product Case 1: (a <. Theta') 
 	 */
-	protected Set<Set<UnifyPair>> unifyCase1(UnifyPair pair, IFiniteClosure fc) {
+	protected PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> unifyCase1(UnifyPair pair, IFiniteClosure fc) {
 		PlaceholderType a = (PlaceholderType)pair.getLhsType(); 
 		UnifyType thetaPrime = pair.getRhsType(); 
 		byte variance = pair.getVariance();
 		
-		Set<Set<UnifyPair>> result = new HashSet<>();
+		PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> result = new PartialOrderSet<Set<UnifyPair>, OrderingUnifyPair>(new OrderingUnifyPair(fc));
 		
 		boolean allGen = thetaPrime.getTypeParams().size() > 0;
 		for(UnifyType t : thetaPrime.getTypeParams())
@@ -2009,11 +2011,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 2: (a <.? ? ext Theta')
 	 */
-	private Set<Set<UnifyPair>> unifyCase2(UnifyPair pair, IFiniteClosure fc) {
+	private PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> unifyCase2(UnifyPair pair, IFiniteClosure fc) {
 		PlaceholderType a = (PlaceholderType) pair.getLhsType();
 		ExtendsType extThetaPrime = (ExtendsType) pair.getRhsType();
 		byte variance = pair.getVariance();
-		Set<Set<UnifyPair>> result = new HashSet<>();
+		PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> result = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 		
 		UnifyType aPrime = PlaceholderType.freshPlaceholder();
 		((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance());
@@ -2036,12 +2038,12 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 3: (a <.? ? sup Theta')
 	 */
-	private Set<Set<UnifyPair>> unifyCase3(UnifyPair pair, IFiniteClosure fc) {
+	private PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> unifyCase3(UnifyPair pair, IFiniteClosure fc) {
 		PlaceholderType a = (PlaceholderType) pair.getLhsType();
 		a.reversVariance();
 		SuperType subThetaPrime = (SuperType) pair.getRhsType();
 		byte variance = pair.getVariance();
-		Set<Set<UnifyPair>> result = new HashSet<>();
+		PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> result = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 		
 		UnifyType aPrime = PlaceholderType.freshPlaceholder();
 		((PlaceholderType)aPrime).setVariance(((PlaceholderType)a).getVariance());
@@ -2066,11 +2068,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 5: (Theta <. a)
 	 */
-	private Set<Set<UnifyPair>> unifyCase5(UnifyPair pair, IFiniteClosure fc) {
+	private PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> unifyCase5(UnifyPair pair, IFiniteClosure fc) {
 		UnifyType theta = pair.getLhsType();
 		PlaceholderType a = (PlaceholderType) pair.getRhsType();
 		byte variance = pair.getVariance();
-		Set<Set<UnifyPair>> result = new HashSet<>();
+		PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> result = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 		
 		boolean allGen = theta.getTypeParams().size() > 0;
 		for(UnifyType t : theta.getTypeParams())
@@ -2145,11 +2147,11 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 8: (Theta <.? a)
 	 */
-	private Set<Set<UnifyPair>> unifyCase8(UnifyPair pair, IFiniteClosure fc) {
+	private PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> unifyCase8(UnifyPair pair, IFiniteClosure fc) {
 		UnifyType theta = pair.getLhsType();
 	    PlaceholderType a = (PlaceholderType) pair.getRhsType();
 	    byte variance = pair.getVariance();
-		Set<Set<UnifyPair>> result = new HashSet<>();
+	    PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair> result = new PartialOrderSet<Set<UnifyPair>,OrderingUnifyPair>(new OrderingUnifyPair(fc));
 		//for(UnifyType thetaS : fc.grArg(theta)) {
 		Set<UnifyPair> resultPrime = new HashSet<>();
 		resultPrime.add(new UnifyPair(a, theta, PairOperator.EQUALSDOT, pair.getSubstitution(), pair));