CongruenceClosure.removeElement is now capable of adding some nodes t…

…o retain information that would otherwise be lost through the remove, (was only done in WeqCongruenceClosure before..)

also: fixes to bwcc propagation
 #224

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/elements/EqFunctionApplicationNode.java

@@ -88,4 +88,16 @@ public boolean isFunctionApplication() {
 	public String toString() {
 		return mFunction.toString() + "[" + mArg.toString() + "]";
 	}
+
+	@Override
+	public EqNode replaceAppliedFunction(final EqNode replacer) {
+		return mEqNodeFactory.getOrConstructFuncAppElement(replacer, mArg);
+	}
+
+	@Override
+	public EqNode replaceArgument(final EqNode replacer) {
+		return mEqNodeFactory.getOrConstructFuncAppElement(mFunction, replacer);
+	}
+
+
 }

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/elements/EqNode.java

@@ -154,12 +154,19 @@ public EqNode getArgument() {
 	}
 
 	/**
-	 * unclear if we really want to have this method..
+	 * default implementation, override in EqFunctionApplicationNode
 	 */
 	@Override
-	public int getHeight() {
+	public EqNode replaceAppliedFunction(final EqNode replacer) {
 		throw new UnsupportedOperationException();
 	}
 
+	/**
+	 * default implementation, override in EqFunctionApplicationNode
+	 */
+	@Override
+	public EqNode replaceArgument(final EqNode replacer) {
+		throw new UnsupportedOperationException();
+	}
 
 }

trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java

@@ -162,13 +162,22 @@ protected Pair<HashRelation<ELEM, ELEM>, HashRelation<ELEM, ELEM>> doMergeAndCom
 		final ELEM e1OldRep = mElementTVER.getRepresentative(elem1);
 		final ELEM e2OldRep = mElementTVER.getRepresentative(elem2);
 
+		/*
+		 * These sets are used for bwcc propagations, there the special case for the disequalities introduced through
+		 * transitivity.
+		 * Should save some useless propagations, and avoid some weirdness in debugging..
+		 */
+		final Set<ELEM> oldUnequalRepsForElem1 = mElementTVER.getRepresentativesUnequalTo(e1OldRep);
+		final Set<ELEM> oldUnequalRepsForElem2 = mElementTVER.getRepresentativesUnequalTo(e2OldRep);
+
 		mElementTVER.reportEquality(elem1, elem2);
 		if (mElementTVER.isInconsistent()) {
 			return null;
 		}
 
 		final Pair<HashRelation<ELEM, ELEM>, HashRelation<ELEM, ELEM>> propInfo =
-				mAuxData.updateAndGetPropagationsOnMerge(elem1, elem2, e1OldRep, e2OldRep);
+				mAuxData.updateAndGetPropagationsOnMerge(elem1, elem2, e1OldRep, e2OldRep, oldUnequalRepsForElem1,
+						oldUnequalRepsForElem2);
 		return propInfo;
 	}
 
@@ -282,6 +291,27 @@ public boolean removeElement(final ELEM elem) {
 		final ELEM newRep = mElementTVER.removeElement(elem);
 		mAuxData.removeElement(elem, elemWasRepresentative, newRep);
 
+		/*
+		 * before removing the parents:
+		 * if there is a newRep, insert a node where the subnode elem is replaced by newRep
+		 * (this may introduce fresh nodes!)
+		 */
+		if (newRep != null) {
+			for (final ELEM parent : new ArrayList<>(mFaAuxData.getAfParents(elem))) {
+				assert parent.getAppliedFunction() == elem;
+				final ELEM replaced = parent.replaceAppliedFunction(newRep);
+				addElement(replaced);
+			}
+			for (final ELEM parent : new ArrayList<>(mFaAuxData.getArgParents(elem))) {
+				assert parent.getArgument() == elem;
+				final ELEM replaced = parent.replaceArgument(newRep);
+				addElement(replaced);
+			}
+		}
+
+		/*
+		 *
+		 */
 		for (final ELEM parent : new ArrayList<>(mFaAuxData.getAfParents(elem))) {
 			removeElement(parent);
 		}
@@ -803,10 +833,13 @@ public CcAuxData(final CcAuxData auxData, final boolean omitRepresentativeChecks
 		 *
 		 * @param e1
 		 * @param e2
+		 * @param oldUnequalRepsForElem2
+		 * @param oldUnequalRepsForElem1
 		 * @return
 		 */
 		Pair<HashRelation<ELEM, ELEM>, HashRelation<ELEM, ELEM>> updateAndGetPropagationsOnMerge(final ELEM e1,
-				final ELEM e2, final ELEM e1OldRep, final ELEM e2OldRep) {
+				final ELEM e2, final ELEM e1OldRep, final ELEM e2OldRep, final Set<ELEM> oldUnequalRepsForElem1,
+				final Set<ELEM> oldUnequalRepsForElem2) {
 
 			final ELEM newRep = mElementTVER.getRepresentative(e1);
 			assert mElementTVER.getRepresentative(e2) == newRep : "we merged before calling this method, right?";
@@ -826,8 +859,8 @@ Pair<HashRelation<ELEM, ELEM>, HashRelation<ELEM, ELEM>> updateAndGetPropagation
 			collectCcParBasedPropagations(afccpar1, afccpar2, congruentResult, unequalResult);
 			collectCcParBasedPropagations(argccpar1, argccpar2, congruentResult, unequalResult);
 
-			collectPropagationsForImplicitlyAddedDisequalities(e1OldRep, e2OldRep, unequalResult);
-			collectPropagationsForImplicitlyAddedDisequalities(e2OldRep, e1OldRep, unequalResult);
+			collectPropagationsForImplicitlyAddedDisequalities(oldUnequalRepsForElem1, e2OldRep, unequalResult);
+			collectPropagationsForImplicitlyAddedDisequalities(oldUnequalRepsForElem2, e1OldRep, unequalResult);
 
 			/*
 			 * update ccPars, ccChildren entries
@@ -922,24 +955,20 @@ && getEqualityStatus(parent1.getArgument(), parent2.getArgument())
 		 * <li>one call of this method will be with (preState, i, f(x))
 		 * <li>we will get the output state: (i = f(y)) , (j != f(x)), (i = j), (x != y)
 		 *
-		 * @param e1OldRep
+		 * @param oldUnequalRepsForElem1
 		 * @param e2OldRep
 		 * @param e2OldRep
 		 * @param oldCcChild
 		 */
-		private void collectPropagationsForImplicitlyAddedDisequalities(final ELEM e1OldRep,
+		private void collectPropagationsForImplicitlyAddedDisequalities(final Set<ELEM> oldUnequalRepsForElem1,
 					final ELEM e2OldRep, final HashRelation<ELEM, ELEM> disequalitiesToPropagate) {
 
-			if (mCcChildren.get(e1OldRep) == null || mCcChildren.get(e1OldRep).isEmpty()) {
-				return;
-			}
-
-			for (final ELEM repUnequalToE1 : mElementTVER.getRepresentativesUnequalTo(e1OldRep)) {
-				final HashRelation<ELEM, ELEM> unequalRepCccs = mCcChildren.get(repUnequalToE1);
-				if (unequalRepCccs == null) {
+			for (final ELEM repUnequalToE1 : oldUnequalRepsForElem1) {
+				final HashRelation<ELEM, ELEM> unequalRep1Cccs = mCcChildren.get(repUnequalToE1);
+				if (unequalRep1Cccs == null) {
 						continue;
 				}
-				for (final Entry<ELEM, ELEM> ccc2 : unequalRepCccs) {
+				for (final Entry<ELEM, ELEM> ccc2 : unequalRep1Cccs) {
 					final HashRelation<ELEM, ELEM> mergePartnerOldRepCccs = mCcChildren.get(e2OldRep);
 					if (mergePartnerOldRepCccs == null) {
 						continue;

trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/ICongruenceClosureElement.java

@@ -22,5 +22,9 @@ public interface ICongruenceClosureElement<ELEM extends ICongruenceClosureElemen
 //
 //	Set<ELEM> getArgParents();
 
-	int getHeight();
+	ELEM replaceAppliedFunction(ELEM replacer);
+
+	ELEM replaceArgument(ELEM replacer);
+
+//	int getHeight();
 }

trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/ThreeValuedEquivalenceRelation.java

@@ -329,13 +329,14 @@ public Set<E> getAllElements() {
 		return mUnionFind.getAllElements();
 	}
 
-	public Set<E> getRepresentativesUnequalTo(final E elem) {
+	public Set<E> getRepresentativesUnequalTo(final E rep) {
+		assert isRepresentative(rep);
 		final Set<E> result = new HashSet<>();
 
-		result.addAll(mDisequalities.getImage(elem));
+		result.addAll(mDisequalities.getImage(rep));
 
 		for (final E domEl : mDisequalities.getDomain()) {
-			if (mDisequalities.getImage(domEl).contains(elem)) {
+			if (mDisequalities.getImage(domEl).contains(rep)) {
 				result.add(domEl);
 			}
 		}

trunk/source/Library-UltimateUtilTest/src/de/uni_freiburg/informatik/ultimate/util/CongruenceClosureTest.java

@@ -670,7 +670,7 @@ class StringCcElement implements ICongruenceClosureElement<StringCcElement>{
 	private final String mName;
 	private final StringCcElement mAppliedFunction;
 	private final StringCcElement mArgument;
-	private final int mHeight;
+//	private final int mHeight;
 	private final Set<StringCcElement> mAfParents;
 	private final Set<StringCcElement> mArgParents;
 
@@ -685,7 +685,7 @@ public StringCcElement(final String name) {
 		mName = name;
 		mAppliedFunction = null;
 		mArgument = null;
-		mHeight = 0;
+//		mHeight = 0;
 		mAfParents = new HashSet<>();
 		mArgParents = new HashSet<>();
 	}
@@ -704,7 +704,7 @@ public StringCcElement(final StringCcElement appliedFunction, final StringCcElem
 //		assert mAppliedFunction.isFunction();
 		mArgument = argument;
 //		assert !argument.isFunction();
-		mHeight = appliedFunction.getHeight() + 1;
+//		mHeight = appliedFunction.getHeight() + 1;
 		mAfParents = new HashSet<>();
 		mArgParents = new HashSet<>();
 
@@ -752,10 +752,18 @@ public boolean hasSameTypeAs(final StringCcElement other) {
 	}
 
 	@Override
-	public int getHeight() {
-		return mHeight;
+	public StringCcElement replaceAppliedFunction(final StringCcElement replacer) {
+		throw new UnsupportedOperationException();
 	}
 
+	@Override
+	public StringCcElement replaceArgument(final StringCcElement replacer) {
+		throw new UnsupportedOperationException();
+	}
+
+
+
+
 //	@Override
 //	public StringCcElement[] getArguments() {
 //		final StringCcElement[] result = new StringCcElement[mHeight + 1];