#239, pass WeakEquivalenceEdgeLabels around instead of their contents

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java

@@ -366,12 +366,15 @@ public EqConstraint<NODE> meet(final EqConstraint<NODE> other) {
 	 * @return true iff this is more or equally constraining than other
 	 */
 	public boolean isStrongerThan(final EqConstraint<NODE> other) {
-		return mPartialArrangement.isStrongerThan(other.mPartialArrangement);
+//		return mPartialArrangement.isStrongerThan(other.mPartialArrangement);
+		return mFactory.getWeqCcManager().isStrongerThan(mPartialArrangement, other.mPartialArrangement);
 	}
 
 	public void addNode(final NODE nodeToAdd) {
 		assert !mIsFrozen;
-		mPartialArrangement.getRepresentativeAndAddElementIfNeeded(nodeToAdd);
+//		mPartialArrangement.getRepresentativeAndAddElementIfNeeded(nodeToAdd);
+//		mPartialArrangement.addElement(nodeToAdd);
+		mFactory.getWeqCcManager().addNode(nodeToAdd, mPartialArrangement);
 	}
 
 	public void removeElement(final NODE elemToHavoc) {

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java

@@ -681,4 +681,8 @@ public boolean assertElementIsFullyRemoved(final NODE elem) {
 		}
 		return true;
 	}
+
+	public WeakEquivalenceGraph<NODE> getWeqGraph() {
+		return mWeakEquivalenceGraph;
+	}
 }

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceGraph.java

@@ -505,7 +505,6 @@ private boolean strengthenEdgeLabel(final Doubleton<NODE> sourceAndTarget,
 
 		if (paList.isEmpty()) {
 			mWeakEquivalenceEdges.put(sourceAndTarget, new WeakEquivalenceEdgeLabel<NODE>(this, paList));
-//			mArrayEqualities.addPair(sourceAndTarget.getOneElement(), sourceAndTarget.getOtherElement());
 			addArrayEquality(sourceAndTarget.getOneElement(), sourceAndTarget.getOtherElement());
 			return oldLabel == null || !oldLabel.isInconsistent();
 		}
@@ -542,7 +541,6 @@ private boolean strengthenEdgeLabel(final Doubleton<NODE> sourceAndTarget,
 
 		// inconsistency check
 		if (strengthenedEdgeLabel.isInconsistent()) {
-//			mArrayEqualities.addPair(sourceAndTarget.getOneElement(), sourceAndTarget.getOtherElement());
 			addArrayEquality(sourceAndTarget.getOneElement(), sourceAndTarget.getOtherElement());
 		}
 
@@ -576,14 +574,13 @@ private boolean reportWeakEquivalence(final Doubleton<NODE> sourceAndTarget,
 	}
 
 	public boolean reportWeakEquivalence(final NODE array1, final NODE array2,
-			final Set<CongruenceClosure<NODE>> edgeLabelContents) {
+			final WeakEquivalenceEdgeLabel<NODE> edgeLabel) {
 		assert mPartialArrangement.isRepresentative(array1) && mPartialArrangement.isRepresentative(array2);
-		if (edgeLabelContents.size() == 1 && edgeLabelContents.iterator().next().isTautological()) {
+		if (edgeLabel.isTautological()) {
 			return false;
 		}
 
-		final boolean result = reportWeakEquivalence(new Doubleton<NODE>(array1, array2),
-				new WeakEquivalenceEdgeLabel<NODE>(this, edgeLabelContents));
+		final boolean result = reportWeakEquivalence(new Doubleton<NODE>(array1, array2), edgeLabel);
 		assert sanityCheck();
 		return result;
 	}
@@ -597,13 +594,16 @@ public boolean isConstrained(final NODE elem) {
 		return false;
 	}
 
-	public Set<CongruenceClosure<NODE>> getEdgeLabelContents(final NODE array1, final NODE array2) {
+	public WeakEquivalenceEdgeLabel<NODE> getEdgeLabel(final NODE array1, final NODE array2) {
+		final NODE array1Rep = mPartialArrangement.getRepresentativeElement(array1);
+		final NODE array2Rep = mPartialArrangement.getRepresentativeElement(array2);
 		final WeakEquivalenceEdgeLabel<NODE> edge =
-				mWeakEquivalenceEdges.get(new Doubleton<>(array1, array2));
-		if (edge != null) {
-			return edge.getLabelContents();
+				mWeakEquivalenceEdges.get(new Doubleton<>(array1Rep, array2Rep));
+		if (edge == null) {
+			// if there is no edge in the graph between the given vertices, we return a tautological edge
+			return new WeakEquivalenceEdgeLabel<>(this);
 		}
-		return Collections.singleton(new CongruenceClosure<>(getLogger()));
+		return edge;
 	}
 
 	/**
@@ -617,9 +617,9 @@ public Set<CongruenceClosure<NODE>> getEdgeLabelContents(final NODE array1, fina
 	 *     is computed from the source or target of the edge the label contents belong to
 	 * @return
 	 */
-	public Set<CongruenceClosure<NODE>> projectEdgeLabelToPoint(
-			final Set<CongruenceClosure<NODE>> labelContents, final NODE value,
-			final List<NODE> weqVarsForThisEdge) {
+//	public Set<CongruenceClosure<NODE>> projectEdgeLabelToPoint(
+	public WeakEquivalenceEdgeLabel<NODE> projectEdgeLabelToPoint(
+			final WeakEquivalenceEdgeLabel<NODE> labelContents, final NODE value, final List<NODE> weqVarsForThisEdge) {
 
 		final WeakEquivalenceEdgeLabel<NODE> originalEdgeLabel =
 				new WeakEquivalenceEdgeLabel<NODE>(this, labelContents);
@@ -656,7 +656,7 @@ public Set<CongruenceClosure<NODE>> projectEdgeLabelToPoint(
 		assert result.assertHasOnlyWeqVarConstraints(new HashSet<>(weqVarsForThisEdge));
 
 		assert result.sanityCheck();
-		return result.getLabelContents();
+		return result;
 	}
 
 	/**
@@ -667,9 +667,8 @@ public Set<CongruenceClosure<NODE>> projectEdgeLabelToPoint(
 	 * @param weqVarsForResolventEdge
 	 * @return
 	 */
-	public Set<CongruenceClosure<NODE>> shiftLabelAndAddException(
-			final Set<CongruenceClosure<NODE>> labelContents, final NODE argument,
-			final List<NODE> weqVarsForResolventEdge) {
+	public WeakEquivalenceEdgeLabel<NODE> shiftLabelAndAddException(final WeakEquivalenceEdgeLabel<NODE> labelContents,
+			final NODE argument, final List<NODE> weqVarsForResolventEdge) {
 		assert !weqVarsForResolventEdge.isEmpty() : "because the array in the resolvent must have a dimension >= 1";
 
 		final WeakEquivalenceEdgeLabel<NODE> meet =
@@ -697,11 +696,16 @@ public Set<CongruenceClosure<NODE>> shiftLabelAndAddException(
 		shiftedLabelContents.add(firstWeqVarUnequalArgument);
 		assert shiftedLabelContents.stream().allMatch(l -> l.sanityCheckOnlyCc());
 
-		final Set<CongruenceClosure<NODE>> normalized = mWeqCcManager
-				.filterRedundantCcs(new HashSet<>(shiftedLabelContents));
-
-		assert normalized.stream().allMatch(l -> l.sanityCheckOnlyCc());
+		final WeakEquivalenceEdgeLabel<NODE> normalized = mWeqCcManager
+				.filterRedundantCcs(new WeakEquivalenceEdgeLabel<>(this, shiftedLabelContents));
+		assert normalized.getLabelContents().stream().allMatch(l -> l.sanityCheckOnlyCc());
 		return normalized;
+
+//		final Set<CongruenceClosure<NODE>> normalized = mWeqCcManager
+//				.filterRedundantCcs(new HashSet<>(shiftedLabelContents));
+//
+//		assert normalized.stream().allMatch(l -> l.sanityCheckOnlyCc());
+//		return normalized;
 	}
 
 //	private static <NODE extends ICongruenceClosureElement<NODE>> List<CongruenceClosure<NODE>> simplifyPaDisjunction(
@@ -1051,9 +1055,5 @@ public WeqCcManager<NODE> getWeqCcManager() {
 	public EqConstraintFactory<NODE> getFactory() {
 		return mFactory;
 	}
-
-//	public void resetArrayEqualities() {
-//		mArrayEqualities.clear();
-//	}
 }
 

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCcManager.java

@@ -26,6 +26,7 @@
  */
 package de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain;
 
+import java.util.Collections;
 import java.util.Set;
 
 import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure;
@@ -63,6 +64,11 @@ public WeqCongruenceClosure<NODE> getWeqMeet(final CongruenceClosure<NODE> cc,
 	}
 
 	public WeqCongruenceClosure<NODE> addNode(final NODE node, final WeqCongruenceClosure<NODE> origWeqCc) {
+		if (origWeqCc.hasElement(node)) {
+			// node is already present --> nothing to do
+			return origWeqCc;
+		}
+
 		final WeqCongruenceClosure<NODE> unfrozen = unfreeze(origWeqCc);
 		unfrozen.addElement(node);
 		unfrozen.freeze();
@@ -74,6 +80,11 @@ private WeqCongruenceClosure<NODE> unfreeze(final WeqCongruenceClosure<NODE> ori
 		return new WeqCongruenceClosure<>(origWeqCc);
 	}
 
+	public WeakEquivalenceEdgeLabel<NODE> filterRedundantCcs(final WeakEquivalenceEdgeLabel<NODE> label) {
+		final Set<CongruenceClosure<NODE>> filtered = mCcManager.filterRedundantCcs(label.getLabelContents());
+		return new WeakEquivalenceEdgeLabel<>(label.getWeqGraph(), filtered);
+	}
+
 	public Set<CongruenceClosure<NODE>> filterRedundantCcs(final Set<CongruenceClosure<NODE>> ccs) {
 		return mCcManager.filterRedundantCcs(ccs);
 	}
@@ -145,4 +156,19 @@ public WeqCongruenceClosure<NODE> join(final WeqCongruenceClosure<NODE> mPartial
 		return mPartialArrangement.join(partialArrangement);
 	}
 
+	public boolean isStrongerThan(final WeqCongruenceClosure<NODE> partialArrangement,
+			final WeqCongruenceClosure<NODE> partialArrangement2) {
+		return partialArrangement.isStrongerThan(partialArrangement2);
+	}
+
+	public WeakEquivalenceEdgeLabel<NODE> getSingletonEdgeLabel(final WeakEquivalenceGraph<NODE> weakEquivalenceGraph,
+			final CongruenceClosure<NODE> newConstraint) {
+		return new WeakEquivalenceEdgeLabel<>(weakEquivalenceGraph, Collections.singleton(newConstraint));
+	}
+
+	public WeakEquivalenceEdgeLabel<NODE> getSingletonEdgeLabel(final WeakEquivalenceGraph<NODE> weakEquivalenceGraph,
+			final Set<CongruenceClosure<NODE>> constraints) {
+		return new WeakEquivalenceEdgeLabel<>(weakEquivalenceGraph, constraints);
+	}
+
 }