From 781945f230100df8267877f5564f04f4efe66ba3 Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Fri, 1 Dec 2017 16:41:35 +0100 Subject: [PATCH] #239, pass WeakEquivalenceEdgeLabels around instead of their contents --- .../absint/vpdomain/EqConstraint.java | 7 +- .../vpdomain/WeakEquivalenceEdgeLabel.java | 4 + .../absint/vpdomain/WeakEquivalenceGraph.java | 52 +++++------ .../absint/vpdomain/WeqCcManager.java | 26 ++++++ .../absint/vpdomain/WeqCongruenceClosure.java | 89 +++++++++++-------- 5 files changed, 113 insertions(+), 65 deletions(-) diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java index bf88f439b0a..1af6cbd14f9 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqConstraint.java @@ -366,12 +366,15 @@ public EqConstraint meet(final EqConstraint other) { * @return true iff this is more or equally constraining than other */ public boolean isStrongerThan(final EqConstraint 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) { diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java index fa16fecc40f..3d70ed80ba1 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java +++ b/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 getWeqGraph() { + return mWeakEquivalenceGraph; + } } \ No newline at end of file diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceGraph.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceGraph.java index 1e4dee820e8..cb2e49301be 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceGraph.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceGraph.java @@ -505,7 +505,6 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, if (paList.isEmpty()) { mWeakEquivalenceEdges.put(sourceAndTarget, new WeakEquivalenceEdgeLabel(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 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 sourceAndTarget, } public boolean reportWeakEquivalence(final NODE array1, final NODE array2, - final Set> edgeLabelContents) { + final WeakEquivalenceEdgeLabel 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(array1, array2), - new WeakEquivalenceEdgeLabel(this, edgeLabelContents)); + final boolean result = reportWeakEquivalence(new Doubleton(array1, array2), edgeLabel); assert sanityCheck(); return result; } @@ -597,13 +594,16 @@ public boolean isConstrained(final NODE elem) { return false; } - public Set> getEdgeLabelContents(final NODE array1, final NODE array2) { + public WeakEquivalenceEdgeLabel getEdgeLabel(final NODE array1, final NODE array2) { + final NODE array1Rep = mPartialArrangement.getRepresentativeElement(array1); + final NODE array2Rep = mPartialArrangement.getRepresentativeElement(array2); final WeakEquivalenceEdgeLabel 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> getEdgeLabelContents(final NODE array1, fina * is computed from the source or target of the edge the label contents belong to * @return */ - public Set> projectEdgeLabelToPoint( - final Set> labelContents, final NODE value, - final List weqVarsForThisEdge) { +// public Set> projectEdgeLabelToPoint( + public WeakEquivalenceEdgeLabel projectEdgeLabelToPoint( + final WeakEquivalenceEdgeLabel labelContents, final NODE value, final List weqVarsForThisEdge) { final WeakEquivalenceEdgeLabel originalEdgeLabel = new WeakEquivalenceEdgeLabel(this, labelContents); @@ -656,7 +656,7 @@ public Set> projectEdgeLabelToPoint( assert result.assertHasOnlyWeqVarConstraints(new HashSet<>(weqVarsForThisEdge)); assert result.sanityCheck(); - return result.getLabelContents(); + return result; } /** @@ -667,9 +667,8 @@ public Set> projectEdgeLabelToPoint( * @param weqVarsForResolventEdge * @return */ - public Set> shiftLabelAndAddException( - final Set> labelContents, final NODE argument, - final List weqVarsForResolventEdge) { + public WeakEquivalenceEdgeLabel shiftLabelAndAddException(final WeakEquivalenceEdgeLabel labelContents, + final NODE argument, final List weqVarsForResolventEdge) { assert !weqVarsForResolventEdge.isEmpty() : "because the array in the resolvent must have a dimension >= 1"; final WeakEquivalenceEdgeLabel meet = @@ -697,11 +696,16 @@ public Set> shiftLabelAndAddException( shiftedLabelContents.add(firstWeqVarUnequalArgument); assert shiftedLabelContents.stream().allMatch(l -> l.sanityCheckOnlyCc()); - final Set> normalized = mWeqCcManager - .filterRedundantCcs(new HashSet<>(shiftedLabelContents)); - - assert normalized.stream().allMatch(l -> l.sanityCheckOnlyCc()); + final WeakEquivalenceEdgeLabel normalized = mWeqCcManager + .filterRedundantCcs(new WeakEquivalenceEdgeLabel<>(this, shiftedLabelContents)); + assert normalized.getLabelContents().stream().allMatch(l -> l.sanityCheckOnlyCc()); return normalized; + +// final Set> normalized = mWeqCcManager +// .filterRedundantCcs(new HashSet<>(shiftedLabelContents)); +// +// assert normalized.stream().allMatch(l -> l.sanityCheckOnlyCc()); +// return normalized; } // private static > List> simplifyPaDisjunction( @@ -1051,9 +1055,5 @@ public WeqCcManager getWeqCcManager() { public EqConstraintFactory getFactory() { return mFactory; } - -// public void resetArrayEqualities() { -// mArrayEqualities.clear(); -// } } diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCcManager.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCcManager.java index 3206b737675..d7d001d5915 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCcManager.java +++ b/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 getWeqMeet(final CongruenceClosure cc, } public WeqCongruenceClosure addNode(final NODE node, final WeqCongruenceClosure origWeqCc) { + if (origWeqCc.hasElement(node)) { + // node is already present --> nothing to do + return origWeqCc; + } + final WeqCongruenceClosure unfrozen = unfreeze(origWeqCc); unfrozen.addElement(node); unfrozen.freeze(); @@ -74,6 +80,11 @@ private WeqCongruenceClosure unfreeze(final WeqCongruenceClosure ori return new WeqCongruenceClosure<>(origWeqCc); } + public WeakEquivalenceEdgeLabel filterRedundantCcs(final WeakEquivalenceEdgeLabel label) { + final Set> filtered = mCcManager.filterRedundantCcs(label.getLabelContents()); + return new WeakEquivalenceEdgeLabel<>(label.getWeqGraph(), filtered); + } + public Set> filterRedundantCcs(final Set> ccs) { return mCcManager.filterRedundantCcs(ccs); } @@ -145,4 +156,19 @@ public WeqCongruenceClosure join(final WeqCongruenceClosure mPartial return mPartialArrangement.join(partialArrangement); } + public boolean isStrongerThan(final WeqCongruenceClosure partialArrangement, + final WeqCongruenceClosure partialArrangement2) { + return partialArrangement.isStrongerThan(partialArrangement2); + } + + public WeakEquivalenceEdgeLabel getSingletonEdgeLabel(final WeakEquivalenceGraph weakEquivalenceGraph, + final CongruenceClosure newConstraint) { + return new WeakEquivalenceEdgeLabel<>(weakEquivalenceGraph, Collections.singleton(newConstraint)); + } + + public WeakEquivalenceEdgeLabel getSingletonEdgeLabel(final WeakEquivalenceGraph weakEquivalenceGraph, + final Set> constraints) { + return new WeakEquivalenceEdgeLabel<>(weakEquivalenceGraph, constraints); + } + } diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCongruenceClosure.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCongruenceClosure.java index a7ac001cf2e..cb356135a82 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCongruenceClosure.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqCongruenceClosure.java @@ -232,12 +232,15 @@ public void reportWeakEquivalence(final NODE array1, final NODE array2, final NO final CongruenceClosure newConstraint = computeWeqConstraintForIndex( Collections.singletonList(storeIndex)); - reportWeakEquivalence(array1, array2, Collections.singleton(newConstraint)); +// reportWeakEquivalence(array1, array2, Collections.singleton(newConstraint)); + reportWeakEquivalence(array1, array2, + mFactory.getWeqCcManager().getSingletonEdgeLabel(mWeakEquivalenceGraph, newConstraint)); assert sanityCheck(); } private void reportWeakEquivalence(final NODE array1, final NODE array2, - final Set> edgeLabel) { + final WeakEquivalenceEdgeLabel edgeLabel) { +// final Set> edgeLabel) { assert !isFrozen(); if (isInconsistent()) { return; @@ -275,7 +278,7 @@ boolean executeFloydWarshallAndReportResultToWeqCc() { for (final Entry, WeakEquivalenceEdgeLabel> fwEdge : fwResult .entrySet()) { fwmc |= reportWeakEquivalenceDoOnlyRoweqPropagations(fwEdge.getKey().getOneElement(), - fwEdge.getKey().getOtherElement(), fwEdge.getValue().getLabelContents()); + fwEdge.getKey().getOtherElement(), fwEdge.getValue()); assert sanityCheck(); } assert sanityCheck(); @@ -283,12 +286,15 @@ boolean executeFloydWarshallAndReportResultToWeqCc() { } private boolean reportWeakEquivalenceDoOnlyRoweqPropagations(final NODE array1, final NODE array2, - final Set> edgeLabel) { - assert edgeLabel.stream().allMatch(l -> l.assertHasOnlyWeqVarConstraints(mFactory.getAllWeqNodes())); + final WeakEquivalenceEdgeLabel edgeLabel) { +// final Set> edgeLabel) { + assert edgeLabel.getLabelContents().stream() + .allMatch(l -> l.assertHasOnlyWeqVarConstraints(mFactory.getAllWeqNodes())); if (isInconsistent()) { return false; } - if (isLabelTautological(edgeLabel)) { +// if (isLabelTautological(edgeLabel)) { + if (edgeLabel.isTautological()) { return false; } @@ -313,12 +319,15 @@ private boolean reportWeakEquivalenceDoOnlyRoweqPropagations(final NODE array1, return false; } - Set> strengthenedEdgeLabelContents = mWeakEquivalenceGraph - .getEdgeLabelContents(array1Rep, array2Rep); +// Set> strengthenedEdgeLabelContents = mWeakEquivalenceGraph +// .getEdgeLabelContents(array1Rep, array2Rep); + final WeakEquivalenceEdgeLabel strengthenedEdgeLabel = + mWeakEquivalenceGraph.getEdgeLabel(array1Rep, array2Rep); - if (strengthenedEdgeLabelContents == null) { + if (strengthenedEdgeLabel == null) { // edge became "false"; - strengthenedEdgeLabelContents = Collections.emptySet(); + assert false : "TODO : check this case, this does not happen, right? (and the comment above is nonsense..)"; +// strengthenedEdgeLabel = Collections.emptySet(); } /* @@ -349,8 +358,9 @@ private boolean reportWeakEquivalenceDoOnlyRoweqPropagations(final NODE array1, * arrayX[Y] nodes, possibly -- EDIT: not..) */ - final Set> projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( - strengthenedEdgeLabelContents, ccp1.getArgument(), +// final Set> projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( + final WeakEquivalenceEdgeLabel projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( + strengthenedEdgeLabel, ccp1.getArgument(), mFactory.getAllWeqVarsNodeForFunction(array1)); // recursive call @@ -369,8 +379,8 @@ private boolean reportWeakEquivalenceDoOnlyRoweqPropagations(final NODE array1, continue; } - final Set> shiftedLabelWithException = mWeakEquivalenceGraph - .shiftLabelAndAddException(strengthenedEdgeLabelContents, ccc1.getValue(), + final WeakEquivalenceEdgeLabel shiftedLabelWithException = mWeakEquivalenceGraph + .shiftLabelAndAddException(strengthenedEdgeLabel, ccc1.getValue(), mFactory.getAllWeqVarsNodeForFunction(ccc1.getKey())); // recursive call @@ -542,7 +552,8 @@ private void doRoweqPropagationsOnMerge(final NODE node1, final NODE node2, fina final CongruenceClosure qUnequalI = new CongruenceClosure<>(mLogger); qUnequalI.reportDisequality(firstWeqVar, ccc1ArgReplaced); reportWeakEquivalenceDoOnlyRoweqPropagations(ccc1AfReplaced, ccc2AfReplaced, - Collections.singleton(qUnequalI)); + mFactory.getWeqCcManager().getSingletonEdgeLabel(mWeakEquivalenceGraph, qUnequalI)); +// Collections.singleton(qUnequalI)); } } @@ -563,9 +574,12 @@ private void doRoweqPropagationsOnMerge(final NODE node1, final NODE node2, fina /* * roweq: */ - final Set> aToBLabel = mWeakEquivalenceGraph - .getEdgeLabelContents(ccp1.getAppliedFunction(), ccp2.getAppliedFunction()); - final Set> projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( +// final Set> aToBLabel = mWeakEquivalenceGraph +// .getEdgeLabelContents(ccp1.getAppliedFunction(), ccp2.getAppliedFunction()); + final WeakEquivalenceEdgeLabel aToBLabel = mWeakEquivalenceGraph + .getEdgeLabel(ccp1.getAppliedFunction(), ccp2.getAppliedFunction()); +// final Set> projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( + final WeakEquivalenceEdgeLabel projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( aToBLabel, ccp1.getArgument(), mFactory.getAllWeqVarsNodeForFunction(ccp1.getAppliedFunction())); // recursive call @@ -574,9 +588,9 @@ private void doRoweqPropagationsOnMerge(final NODE node1, final NODE node2, fina /* * roweq-1: */ - final Set> aiToBjLabel = mWeakEquivalenceGraph.getEdgeLabelContents(ccp1, + final WeakEquivalenceEdgeLabel aiToBjLabel = mWeakEquivalenceGraph.getEdgeLabel(ccp1, ccp2); - final Set> shiftedLabelWithException = mWeakEquivalenceGraph + final WeakEquivalenceEdgeLabel shiftedLabelWithException = mWeakEquivalenceGraph .shiftLabelAndAddException(aiToBjLabel, node1, mFactory.getAllWeqVarsNodeForFunction(ccp1.getAppliedFunction())); // recursive call @@ -597,8 +611,9 @@ assert getEqualityStatus(ccp2.getArgument(), ccp1.getArgument()) == EqualityStat final CongruenceClosure qUnequalI = new CongruenceClosure<>(mLogger); qUnequalI.reportDisequality(firstWeqVar, ccp1.getArgument()); - reportWeakEquivalenceDoOnlyRoweqPropagations(ccp1.getAppliedFunction(), - ccp2.getAppliedFunction(), Collections.singleton(qUnequalI)); + reportWeakEquivalenceDoOnlyRoweqPropagations(ccp1.getAppliedFunction(), ccp2.getAppliedFunction(), + //Collections.singleton(qUnequalI)); + mFactory.getWeqCcManager().getSingletonEdgeLabel(mWeakEquivalenceGraph, qUnequalI)); } } @@ -645,8 +660,8 @@ private boolean otherRoweqPropOnMerge(final NODE nodeOldRep, final CcAuxData> shiftedLabelWithException = mWeakEquivalenceGraph - .shiftLabelAndAddException(phi.getLabelContents(), ccc.getValue(), + final WeakEquivalenceEdgeLabel shiftedLabelWithException = mWeakEquivalenceGraph + .shiftLabelAndAddException(phi, ccc.getValue(), mFactory.getAllWeqVarsNodeForFunction(ccc.getKey())); // recursive call madeChanges |= reportWeakEquivalenceDoOnlyRoweqPropagations(ccc.getKey(), aj.getKey(), @@ -838,12 +853,12 @@ public Set getNodesToIntroduceBeforeRemoval(final NODE elemToRemove, continue; } - final Set> projectedLabel = mWeakEquivalenceGraph - .projectEdgeLabelToPoint(edge.getValue().getLabelContents(), + final WeakEquivalenceEdgeLabel projectedLabel = mWeakEquivalenceGraph + .projectEdgeLabelToPoint(edge.getValue(), elemToRemove.getArgument(), mFactory.getAllWeqVarsNodeForFunction(elemToRemove.getAppliedFunction())); - if (isLabelTautological(projectedLabel)) { + if (projectedLabel.isTautological()) { continue; } @@ -851,7 +866,7 @@ public Set getNodesToIntroduceBeforeRemoval(final NODE elemToRemove, * best case: projectedLabel is inconsistent, this means if we introduce b[i] we can later propagate * a[i] = b[i], this also means we don't need to introduce any other node */ - if (projectedLabel.isEmpty()) { + if (projectedLabel.isInconsistent()) { final NODE bi = mFactory.getEqNodeAndFunctionFactory() .getOrConstructFuncAppElement(edge.getKey(), j); assert !mCongruenceClosure.getElementCurrentlyBeingRemoved().getRemovedElements().contains(bi); @@ -868,11 +883,11 @@ public Set getNodesToIntroduceBeforeRemoval(final NODE elemToRemove, * node (we would get a weak equivalence with a ground disjunct * EDIT: this case should be treatable via check for tautology (see also assert below) */ - if (isLabelTautological(projectedLabel)) { + if (projectedLabel.isTautological()) { continue; } // if a disjunct was ground, the the projectToElem(weqvars) operation should have made it "true" - assert !projectedLabel.stream().anyMatch(l -> + assert !projectedLabel.getLabelContents().stream().anyMatch(l -> DataStructureUtils.intersection(l.getAllElements(), mFactory.getAllWeqNodes()).isEmpty()); @@ -953,10 +968,10 @@ protected void registerNewElement(final NODE elem, final RemoveCcElement remInfo } // get label of edge between a and b - final Set> weqEdgeLabelContents = - mWeakEquivalenceGraph.getEdgeLabelContents(ccp.getAppliedFunction(), elem.getAppliedFunction()); + final WeakEquivalenceEdgeLabel weqEdgeLabelContents = + mWeakEquivalenceGraph.getEdgeLabel(ccp.getAppliedFunction(), elem.getAppliedFunction()); - final Set> projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( + final WeakEquivalenceEdgeLabel projectedLabel = mWeakEquivalenceGraph.projectEdgeLabelToPoint( weqEdgeLabelContents, ccp.getArgument(), mFactory.getAllWeqVarsNodeForFunction(ccp.getAppliedFunction())); @@ -1094,7 +1109,7 @@ public WeqCongruenceClosure meetRec(final WeqCongruenceClosure other newWeqCc.reportWeakEquivalenceDoOnlyRoweqPropagations(edge.getKey().getOneElement(), edge.getKey().getOtherElement(), - edge.getValue().getLabelContents()); + edge.getValue()); assert newWeqCc.sanityCheck(); } @@ -1240,9 +1255,9 @@ public boolean addElementRec(final NODE node) { return mCongruenceClosure.addElementRec(node); } - public NODE getRepresentativeAndAddElementIfNeeded(final NODE nodeToAdd) { - return mCongruenceClosure.getRepresentativeAndAddElementIfNeeded(nodeToAdd); - } +// public NODE getRepresentativeAndAddElementIfNeeded(final NODE nodeToAdd) { +// return mCongruenceClosure.getRepresentativeAndAddElementIfNeeded(nodeToAdd); +// } // public void removeSimpleElement(final NODE elem) { // CongruenceClosure.removeSimpleElement(this, elem);