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 8616527362b..ad901449d99 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 @@ -90,7 +90,8 @@ public EqConstraint(final int id, final EqConstraintFactory factory) { public EqConstraint(final int id, final WeqCongruenceClosure cClosure, final EqConstraintFactory factory) { - this(id, factory, new WeqCongruenceClosure<>(cClosure)); + this(id, factory, factory.getCcManager().makeCopy(cClosure)); +// this(id, factory, new WeqCongruenceClosure<>(cClosure)); } /** @@ -99,7 +100,8 @@ public EqConstraint(final int id, final WeqCongruenceClosure cClosure, * @param constraint */ public EqConstraint(final int id, final EqConstraint constraint) { - this(id, constraint.mFactory, new WeqCongruenceClosure<>(constraint.mPartialArrangement)); + this(id, constraint.mFactory, constraint.mFactory.getCcManager().makeCopy(constraint.mPartialArrangement)); + //new WeqCongruenceClosure<>(constraint.mPartialArrangement)); } private EqConstraint(final int id, final EqConstraintFactory factory, 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 new file mode 100644 index 00000000000..bb7d61d39d4 --- /dev/null +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeakEquivalenceEdgeLabel.java @@ -0,0 +1,669 @@ +package de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.HashSet; +import java.util.List; +import java.util.Map; +import java.util.Map.Entry; +import java.util.Set; +import java.util.function.BiPredicate; +import java.util.function.Function; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import de.uni_freiburg.informatik.ultimate.logic.Script; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils; +import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure; +import de.uni_freiburg.informatik.ultimate.util.datastructures.poset.PartialOrderCache; + +/** + * Represents an edge label in the weak equivalence graph. + * An edge label connects two arrays of the same arity(dimensionality) #a. + * An edge label is a tuple of length #a. + * Each tuple element is a set of partial arrangements. The free variables in the partial arrangements are the + * variables of the EqConstraint together with #a special variables that are implicitly universally quantified + * and range over the array positions. + * + */ +class WeakEquivalenceEdgeLabel> { + + /** + * + */ + private final WeakEquivalenceGraph mWeakEquivalenceGraph; + final Set> mLabel; + + /** + * Copy constructor. + * + * @param original + * @param weakEquivalenceGraph TODO + */ + public WeakEquivalenceEdgeLabel(final WeakEquivalenceGraph weakEquivalenceGraph, + final WeakEquivalenceEdgeLabel original) { + mWeakEquivalenceGraph = weakEquivalenceGraph; + mLabel = new HashSet<>(original.getLabelContents().size()); + for (final CongruenceClosure l : original.getLabelContents()) { + assert !l.isInconsistent(); + assert !l.isTautological() || original.getLabelContents().size() == 1; + mLabel.add(new CongruenceClosure<>(l)); + } + assert sanityCheck(); + } + + /** + * + * @return a copy of this weq edge where all disjuncts have been joined into one + */ + public WeakEquivalenceEdgeLabel flatten(final WeakEquivalenceGraph weqGraphForFlattenedLabel) { + if (isInconsistent()) { + return this; + } + return new WeakEquivalenceEdgeLabel(weqGraphForFlattenedLabel, Collections.singleton( + mLabel.stream().reduce((cc1, cc2) -> cc1.join(cc1)).get())); + } + + public void setExternalRemInfo(final CongruenceClosure.RemoveElement remInfo) { + for (final CongruenceClosure lab : mLabel) { + lab.setExternalRemInfo(remInfo); + } + } + + public boolean hasExternalRemInfo() { + for (final CongruenceClosure l : mLabel) { + assert l.assertHasExternalRemInfo(); + } + return true; + } + + public boolean assertHasOnlyWeqVarConstraints(final Set weqVarsForThisEdge) { + for (final CongruenceClosure l : mLabel) { + if (!l.assertHasOnlyWeqVarConstraints(weqVarsForThisEdge)) { + assert false; + return false; + } + } + return true; + } + + /** + * Construct a weak equivalence edge from a list of label contents. + * + * Does some simplifications. + * + * @param newLabelContents + * @param weakEquivalenceGraph TODO + */ + public WeakEquivalenceEdgeLabel(final WeakEquivalenceGraph weakEquivalenceGraph, final Set> newLabelContents) { + mWeakEquivalenceGraph = weakEquivalenceGraph; + mLabel = mWeakEquivalenceGraph.mCcManager.filterRedundantCcs(newLabelContents); + if (mLabel.size() == 1 && mLabel.iterator().next().isInconsistent()) { + //case mLabel = "[False]" -- filterRedundantCcs leaves this case so we have to clean up manually to "[]" + mLabel.clear(); + } + assert sanityCheck(); + } + + /** + * Constructs an empty edge. (labeled "true") + * @param weakEquivalenceGraph TODO + */ + public WeakEquivalenceEdgeLabel(final WeakEquivalenceGraph weakEquivalenceGraph) { + mWeakEquivalenceGraph = weakEquivalenceGraph; + mLabel = new HashSet<>(); + mLabel.add(new CongruenceClosure<>()); + assert sanityCheck(); + } + + public void projectWeqVarNode(final NODE firstDimWeqVarNode) { + for (final CongruenceClosure lab : mLabel) { + lab.removeSimpleElementDontIntroduceNewNodes(firstDimWeqVarNode); + } + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + + public Set projectSimpleElement(final NODE elem, final boolean useWeqGpaMode) { + if (isTautological()) { + return Collections.emptySet(); + } + if (isInconsistent()) { + return Collections.emptySet(); + } + + final Set nodesToAddToGpa = new HashSet<>(); + + final List> newLabelContents = new ArrayList<>(mLabel.size()); + for (final CongruenceClosure lab : mLabel) { + assert lab.sanityCheckOnlyCc(mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + + /* + * just removing elem is not enough + * example: + * elem = a + * label has a[q] + * then a[q] needs to be removed, but mPartialArrangement cannot know that.. + * + * actually, even removeSimpleElement is not enough, because we might be removing + * a[i], a (in that order) + * then during removing a[i] we add a node a[q], but dont insert a, because it is in remInfo + * then when we remove a, the removeSimpleElement will just say the cc does not have a and do + * nothing + * + * plan: compute all dependents, and remove them one by one + */ + if (useWeqGpaMode) { + /* + * current label has been joined with WeqGpa + * (i.e. lab is a WeqCongruenceClosure, not only a CongruenceClosure) + * use CcGpa inside this remove.. (avoids endless recursion) + */ + final Set nodesAdded = lab.removeSimpleElementDontUseWeqGpaTrackAddedNodes(elem); + // some nodes may have been introduced + nodesAdded.stream() + .filter(n -> !CongruenceClosure.dependsOnAny(n, mWeakEquivalenceGraph.mFactory.getAllWeqPrimedNodes())) + .forEach(nodesToAddToGpa::add); + } else { + /* + * lightweight case, current label is a CongruenceClosure, not a WeqCongruenceClosure + * --> we do not allow introduction of new nodes during the remove operation in the labels here + */ + lab.removeSimpleElementDontIntroduceNewNodes(elem); + } + + assert lab.assertSingleElementIsFullyRemoved(elem); + + if (lab.isTautological()) { + // a disjunct became "true" through projection --> the whole disjunction is tautological + mLabel.clear(); + mLabel.add(new CongruenceClosure<>()); + return Collections.emptySet(); + } + assert lab.sanityCheckOnlyCc(mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + + final CongruenceClosure lab2; + if (useWeqGpaMode) { + // unprime weqvars + lab2 = new CongruenceClosure<>(lab); + lab2.transformElementsAndFunctions( + node -> node.renameVariables(mWeakEquivalenceGraph.mFactory.getWeqPrimedVarsToWeqVars())); + } else { + lab2 = lab; + } + + final CongruenceClosure newLab = lab2.projectToElements(mWeakEquivalenceGraph.mFactory.getAllWeqNodes(), + mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + assert newLab.assertSingleElementIsFullyRemoved(elem); + assert !newLab.isTautological(); + assert newLab.sanityCheckOnlyCc(mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + newLabelContents.add(newLab); + } + mLabel.clear(); + mLabel.addAll(newLabelContents); + assert mLabel.stream().allMatch(l -> l.assertSingleElementIsFullyRemoved(elem)); + assert sanityCheck(); + return nodesToAddToGpa; + } + + public WeakEquivalenceEdgeLabel projectToElements(final Set allWeqNodes) { + if (isInconsistent()) { + return this; + } + final Set> newLabelContents = new HashSet<>(); + for (final CongruenceClosure item : mLabel) { + newLabelContents.add(item.projectToElements(allWeqNodes, + mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved())); + } + assert newLabelContents.stream().allMatch(l -> l.sanityCheckOnlyCc()); + final WeakEquivalenceEdgeLabel result = + new WeakEquivalenceEdgeLabel(mWeakEquivalenceGraph, newLabelContents); + assert result.sanityCheck(); + return result; + } + + /** + * + * + * @param inOrDecrease how much to shift (negative value for decrease) + * @param weqVarsForThisEdge this edgeLabel does not know the function signature of its source and target; + * thus we pass a list of weqVars that belongs to that signature (those are the ones to be shifted..) + * they must be in correct order of dimensions according to source/target + */ + public void inOrDecreaseWeqVarIndices(final int inOrDecrease, final List weqVarsForThisEdge) { + assert inOrDecrease == 1 || inOrDecrease == -1 : "we don't expect any other cases"; + assert inOrDecrease != 1 || !this.getAppearingNodes() + .contains(weqVarsForThisEdge.get(weqVarsForThisEdge.size() - 1)) : "project the highest weqvar " + + "before increasing!"; + assert inOrDecrease != -1 || !this.getAppearingNodes() + .contains(weqVarsForThisEdge.get(0)) : "project the lowest weqvar before decreasing!"; + + final Map substitutionMapping = new HashMap<>(); + for (int i = 0; i < weqVarsForThisEdge.size(); i++) { + final NODE nodeI = weqVarsForThisEdge.get(i); + final int newDim = i + inOrDecrease; + // the others (newDim <0) should have been projected out of the formula before.. (in the calling method) + if (newDim >= 0 && newDim < weqVarsForThisEdge.size()) { + substitutionMapping.put(nodeI.getTerm(), + mWeakEquivalenceGraph.mFactory.getWeqVariableForDimension(newDim, nodeI.getSort())); + } + } + this.transformElements(e -> e.renameVariables(substitutionMapping)); + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + + public boolean isConstrained(final NODE elem) { + return mLabel.stream().anyMatch(l -> l.isConstrained(elem)); + } + + public Set> getLabelContents() { + return Collections.unmodifiableSet(mLabel); + } + + public boolean isInconsistent() { + for (final CongruenceClosure pa : getLabelContents()) { + if (!pa.isInconsistent()) { + // we found one consistent disjunct --> this label is consistent + return false; + } else { + // current cc is inconsistent + assert getLabelContents().size() == 1 : "we are filtering out all but one 'bottoms', right?"; + } + } + return true; + } + + /** + * Called when the ground partial arrangement (gpa) has changed. + * Checks if any entry of a weq label became inconsistent through the change, removes that entry, propagates + * an array equality if the whole edge became inconsistent + * + * --> does edge inconsistency based propagations (weak equivalences becoming strong ones) + * --> does not do congruence style weq propagations, those are done separately when an equality is added + * to the gpa + * + * @param reportX lambda, applying one of the CongruenceClosure.report functions to some nodes for a given + * CongruenceClosure object + * @return a fresh, updated WeqLabel, null if the label became inconsistent + */ + public WeakEquivalenceEdgeLabel reportChangeInGroundPartialArrangement( + final Predicate> reportX) { + assert this.sanityCheck(); + + + final Set> newLabel = new HashSet<>(); + + for (final CongruenceClosure l : mLabel) { + assert mWeakEquivalenceGraph.mPartialArrangement.sanityCheck(); + assert l.sanityCheckOnlyCc(); + final CongruenceClosure currentPaWgpa = mWeakEquivalenceGraph.mCcManager.getMeet(l, + mWeakEquivalenceGraph.mPartialArrangement, + mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + + if (currentPaWgpa.isInconsistent()) { + // label element became inconsistent, don't add it to the new label + continue; + } + + final boolean change = reportX.test(currentPaWgpa); + + if (!change) { + /* + * no change in mLabelWgpa[i] meet gpa -- this can happen, because labelWgpa might imply an + * equality that is not present in gpa.. + * + * no checks need to be made here, anyway + */ + newLabel.add(l); + assert !currentPaWgpa.isInconsistent(); + continue; + } + + // add the strengthened version as the new label element + newLabel.add(currentPaWgpa.projectToElements(mWeakEquivalenceGraph.mFactory.getAllWeqNodes(), + mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved())); + + assert this.sanityCheck(); + } + assert newLabel.stream().allMatch(CongruenceClosure::sanityCheckOnlyCc); + return new WeakEquivalenceEdgeLabel(mWeakEquivalenceGraph, newLabel); + } + + /** + * Computes a DNF from this label as a List of conjunctive Terms. + * The disjunction has the form \/_i pa_i + * + * @param script + * @return a DNF as a List of conjunctive Terms. + */ + public List toDNF(final Script script) { + final List result = new ArrayList<>(); + for (final CongruenceClosure cc : mLabel) { + final List cube = EqConstraint.partialArrangementToCube(script, cc); + final Term cubeTerm = SmtUtils.and(script, cube); + result.add(cubeTerm); + } + return result; + } + + public void transformElements(final Function transformer) { + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + // for (int i = 0; i < getLabelContents().size(); i++) { + for (final CongruenceClosure l : mLabel) { + l.transformElementsAndFunctions(transformer); + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + + /** + * Returns all NODEs that are used in this WeqEdgeLabel. + * Not including the special quantified variable's nodes. + * @return + */ + public Set getAppearingNodes() { + final Set res = new HashSet<>(); + getLabelContents().forEach(pa -> res.addAll(pa.getAllElements())); + return res; + } + + public WeakEquivalenceEdgeLabel meet(final WeakEquivalenceEdgeLabel otherLabel) { + return meet(otherLabel.getLabelContents()); + } + + WeakEquivalenceEdgeLabel meet(final Set> paList) { + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + return meetRec(paList); + } + + WeakEquivalenceEdgeLabel meetRec(final Set> paList) { + final Set> newLabelContent = new HashSet<>(); + for (final CongruenceClosure lc1 : mLabel) { + for (final CongruenceClosure lc2 : paList) { + newLabelContent.add(lc1.meetRec(lc2)); + } + } + + final Set> newLabel = mWeakEquivalenceGraph.mCcManager.filterRedundantCcs(newLabelContent); + assert newLabel.stream().allMatch(l -> l.sanityCheckOnlyCc()); + + final Set> newLabelProjected = newLabel.stream() + .map(l -> l.projectToElements(mWeakEquivalenceGraph.mFactory.getAllWeqNodes(), + mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved())).collect(Collectors.toSet()); + assert newLabelProjected.stream() + .allMatch(l -> l.sanityCheckOnlyCc(mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved())); + + final WeakEquivalenceEdgeLabel result = + new WeakEquivalenceEdgeLabel(mWeakEquivalenceGraph, newLabelProjected); + assert result.sanityCheck(); + return result; + } + + /** + * rule: A isStrongerThan B + * iff + * forall ai exists bi. ai subseteq bi + * @param ccPoCache + * @param value + * @return + */ + public boolean isStrongerThan(final WeakEquivalenceEdgeLabel other) { + return isStrongerThan(other, CongruenceClosure::isStrongerThan); + } + + public boolean isStrongerThan(final WeakEquivalenceEdgeLabel other, + final BiPredicate, CongruenceClosure> lowerOrEqual) { + for (final CongruenceClosure paThis : getLabelContents()) { + boolean existsWeaker = false; + for (final CongruenceClosure paOther : other.getLabelContents()) { + if (lowerOrEqual.test(paThis, paOther)) { + existsWeaker = true; + break; + } + } + if (!existsWeaker) { + return false; + } + } + return true; + } + + + + /** + * Computes a constraint which, for every dimension, has the union of the disjuncts of both input labels + * (this and other). + * @param ccPoCache + * @param correspondingWeqEdgeInOther + * @return + */ + public WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel other) { + return this.union(other, null); + } + + public WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel other, + final PartialOrderCache> ccPoCache) { + assert this.sanityCheck() && other.sanityCheck(); + // assert this.mLabel.size() < 10 && other.mLabel.size() < 10; + final List> unionList = new ArrayList<>( + mLabel.size() + other.getLabelContents().size()); + unionList.addAll(mLabel); + unionList.addAll(other.getLabelContents()); + + final Set> filtered = ccPoCache == null ? + mWeakEquivalenceGraph.mCcManager.filterRedundantCcs(new HashSet<>(unionList)) + : mWeakEquivalenceGraph.mCcManager.filterRedundantCcs(new HashSet<>(unionList), ccPoCache); + + final WeakEquivalenceEdgeLabel result = new WeakEquivalenceEdgeLabel<>(mWeakEquivalenceGraph, + filtered); + assert result.sanityCheck(); + return result; + } + + boolean isTautological() { + for (final CongruenceClosure l : getLabelContents()) { + if (l.isTautological()) { + assert getLabelContents().size() == 1; + return true; + } + } + return false; + } + + + @Override + public String toString() { + if (mLabel.size() < 3) { + return toLogString(); + } + return "weq edge label, size: " + mLabel.size(); + } + + public String toLogString() { + if (isInconsistent()) { + return "False"; + } + if (isTautological()) { + return "True"; + } + + + final StringBuilder sb = new StringBuilder(); + + mLabel.forEach(l -> sb.append(l.toLogString() + "\n")); + return sb.toString(); + } + + boolean sanityCheck() { + return sanityCheck(mWeakEquivalenceGraph.mPartialArrangement); + } + + private boolean sanityCheck(final WeqCongruenceClosure groundPartialArrangement) { + if (mWeakEquivalenceGraph.mFactory == null) { + return true; + } + if (mWeakEquivalenceGraph.isEmpty()) { + return true; + } + + if (mLabel.stream().anyMatch(l -> l.isTautological()) && mLabel.size() > 1) { + // not normalized + assert false; + return false; + } + + if (mLabel.stream().anyMatch(l -> l.isInconsistent())) { + // not normalized + assert false; + return false; + } + + // check that labels are free of weqPrimed vars + if (!groundPartialArrangement.mMeetWithGpaCase) { + for (final CongruenceClosure lab : mLabel) { + for (final NODE el : lab.getAllElements()) { + if (CongruenceClosure.dependsOnAny(el, mWeakEquivalenceGraph.mFactory.getAllWeqPrimedNodes())) { + assert false; + return false; + } + } + } + } + + // check that labels are free of constraints that don't contain weq nodes + for (final CongruenceClosure lab : mLabel) { + assert lab.assertHasOnlyWeqVarConstraints(mWeakEquivalenceGraph.mFactory.getAllWeqNodes()); + } + + return sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + + public void meetWithWeqGpa(final WeqCongruenceClosure originalPa) { + + final List> newLabelContents = new ArrayList<>(); + for (final CongruenceClosure l : mLabel) { + + // make a copy of the full abstract state (ground partial arrangement and weak equivalence graph, weqCc) + // final WeqCongruenceClosure paCopy = new WeqCongruenceClosure<>(originalPa, true); + final WeqCongruenceClosure paCopy = mWeakEquivalenceGraph.mCcManager.makeCopyForWeqMeet(originalPa); + + + // make a copy of the label, prime the weq vars + final CongruenceClosure lCopy = new CongruenceClosure<>(l); + lCopy.transformElementsAndFunctions(n -> n.renameVariables(mWeakEquivalenceGraph.mFactory.getWeqVarsToWeqPrimedVars())); + + // report all constraints from the label into the copy of the weqCc + for (final Entry eq : lCopy.getSupportingElementEqualities().entrySet()) { + if (paCopy.isInconsistent()) { + mLabel.clear(); + return; + } + paCopy.reportEquality(eq.getKey(), eq.getValue()); + } + for (final Entry deq : lCopy.getElementDisequalities().entrySet()) { + if (paCopy.isInconsistent()) { + mLabel.clear(); + return; + } + paCopy.reportDisequality(deq.getKey(), deq.getValue()); + } + + if (paCopy.isTautological()) { + mLabel.clear(); + mLabel.add(new CongruenceClosure()); + return; + } + newLabelContents.add(paCopy); + } + + mLabel.clear(); + mLabel.addAll(newLabelContents); + + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + + } + + public void meetWithCcGpa() { + meetWithGpa(false); + } + + public void meetWithGpa(final boolean meetWithFullWeqCc) { + + final Set> newLabelContents = new HashSet<>(); + // for (int i = 0; i < getLabelContents().size(); i++) { + for (final CongruenceClosure l : mLabel) { + if (l.isTautological()) { + // we have one "true" disjunct --> the whole disjunction is tautological + if (mLabel.size() == 1) { + return; + } + mLabel.clear(); + mLabel.add(new CongruenceClosure<>()); + return; + } + final CongruenceClosure meet; + if (meetWithFullWeqCc) { + meet = mWeakEquivalenceGraph.mCcManager.getWeqMeet(l, mWeakEquivalenceGraph.mPartialArrangement); + } else { + meet = mWeakEquivalenceGraph.mCcManager.getMeet(l, mWeakEquivalenceGraph.mPartialArrangement, mWeakEquivalenceGraph.mPartialArrangement.getElementCurrentlyBeingRemoved()); + } + + if (meet.isInconsistent()) { + /* label element is inconsistent with the current gpa + * --> omit it from the new label + */ + continue; + } + if (meet.isTautological()) { + assert false : "this should never happen because if the meet is tautological then mLabel.get(i)" + + "is, too, right?"; + // we have one "true" disjunct --> the whole disjunction is tautological + mLabel.clear(); + mLabel.add(new CongruenceClosure<>()); + return; + } + newLabelContents.add(meet); + } + assert newLabelContents.size() <= 1 || !newLabelContents.stream().anyMatch(c -> c.isTautological()); + + + mLabel.clear(); + mLabel.addAll(newLabelContents); + + assert sanityCheckDontEnforceProjectToWeqVars(mWeakEquivalenceGraph.mPartialArrangement); + } + + boolean sanityCheckDontEnforceProjectToWeqVars(final CongruenceClosure groundPartialArrangement) { + for (final CongruenceClosure lab : mLabel) { + if (!lab.sanityCheckOnlyCc(groundPartialArrangement.getElementCurrentlyBeingRemoved())) { + assert false; + return false; + } + } + + // check label normalization + if (mLabel.stream().anyMatch(pa -> pa.isTautological()) && mLabel.size() != 1) { + assert false : "missing normalization: if there is one 'true' disjunct, we can drop" + + "all other disjuncts"; + return false; + } + + if (mLabel.stream().anyMatch(pa -> pa.isInconsistent())) { + assert false : "missing normalization: contains 'false' disjuncts"; + return false; + } + + return true; + } + + public boolean assertElementIsFullyRemoved(final NODE elem) { + for (final CongruenceClosure lab : mLabel) { + if (!lab.assertSingleElementIsFullyRemoved(elem)) { + assert false; + return false; + } + } + return true; + } +} \ 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 1295280cb24..aa77c3b8bd2 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 @@ -35,6 +35,7 @@ import java.util.Map.Entry; import java.util.Optional; import java.util.Set; +import java.util.function.BiFunction; import java.util.function.BiPredicate; import java.util.function.Function; import java.util.function.Predicate; @@ -62,11 +63,11 @@ */ public class WeakEquivalenceGraph> { - private final WeqCcManager mCcManager; + final WeqCcManager mCcManager; - private final EqConstraintFactory mFactory; + final EqConstraintFactory mFactory; - private final Map, WeakEquivalenceEdgeLabel> mWeakEquivalenceEdges; + private final Map, WeakEquivalenceEdgeLabel> mWeakEquivalenceEdges; private final HashRelation mArrayEqualities; @@ -74,7 +75,7 @@ public class WeakEquivalenceGraph> { * The WeqCongruenceClosure that this weq graph is part of. This may be null, if we use this weq graph as an * intermediate, for example during a join or meet operation. */ - private final WeqCongruenceClosure mPartialArrangement; + final WeqCongruenceClosure mPartialArrangement; // private boolean mWeqMeetMode; @@ -103,7 +104,7 @@ public WeakEquivalenceGraph(final WeqCongruenceClosure pArr, * @param factory */ private WeakEquivalenceGraph( - final Map, WeakEquivalenceEdgeLabel> weakEquivalenceEdges, + final Map, WeakEquivalenceEdgeLabel> weakEquivalenceEdges, final HashRelation arrayEqualities, final EqConstraintFactory factory) { mPartialArrangement = null; @@ -117,6 +118,7 @@ private WeakEquivalenceGraph( /** * Copy constructor + * * @param weakEquivalenceGraph * @param factory */ @@ -127,7 +129,10 @@ public WeakEquivalenceGraph(final WeqCongruenceClosure pArr, mArrayEqualities = new HashRelation<>(weakEquivalenceGraph.mArrayEqualities); mWeakEquivalenceEdges = new HashMap<>(); - for (final Entry, WeakEquivalenceEdgeLabel> weqEdge + mFactory = weakEquivalenceGraph.mFactory; + mCcManager = mFactory.getCcManager(); + + for (final Entry, WeakEquivalenceEdgeLabel> weqEdge : weakEquivalenceGraph.mWeakEquivalenceEdges.entrySet()) { // make sure that the representatives in pArr and in our new weq edges are compatible @@ -136,14 +141,14 @@ public WeakEquivalenceGraph(final WeqCongruenceClosure pArr, pArr.getRepresentativeElement(weqEdge.getKey().getOtherElement())); if (flattenEdges) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel flattenedEdgeLabel = weqEdge.getValue().flatten(); + final WeakEquivalenceEdgeLabel flattenedEdgeLabel = + weqEdge.getValue().flatten(this); mWeakEquivalenceEdges.put(newSoureceAndTarget, flattenedEdgeLabel); } else { - mWeakEquivalenceEdges.put(newSoureceAndTarget, new WeakEquivalenceEdgeLabel(weqEdge.getValue())); + mWeakEquivalenceEdges.put(newSoureceAndTarget, new WeakEquivalenceEdgeLabel(this, + weqEdge.getValue())); } } - mFactory = weakEquivalenceGraph.mFactory; - mCcManager = mFactory.getCcManager(); assert sanityCheck(); } @@ -162,9 +167,9 @@ public boolean reportChangeInGroundPartialArrangement(final Predicate, WeakEquivalenceEdgeLabel> weqCopy = new HashMap<>(mWeakEquivalenceEdges); - for (final Entry, WeakEquivalenceEdgeLabel> edge : weqCopy.entrySet()) { - final WeakEquivalenceEdgeLabel newLabel = edge.getValue().reportChangeInGroundPartialArrangement(action); + final Map, WeakEquivalenceEdgeLabel> weqCopy = new HashMap<>(mWeakEquivalenceEdges); + for (final Entry, WeakEquivalenceEdgeLabel> edge : weqCopy.entrySet()) { + final WeakEquivalenceEdgeLabel newLabel = edge.getValue().reportChangeInGroundPartialArrangement(action); if (newLabel.isInconsistent()) { /* * edge label became inconsistent @@ -187,21 +192,21 @@ public boolean reportChangeInGroundPartialArrangement(final Predicate, WeakEquivalenceEdgeLabel> edgesCopy = new HashMap<>(mWeakEquivalenceEdges); + final Map, WeakEquivalenceEdgeLabel> edgesCopy = new HashMap<>(mWeakEquivalenceEdges); - for (final Entry, WeakEquivalenceEdgeLabel> en : edgesCopy.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> en : edgesCopy.entrySet()) { final NODE source = en.getKey().getOneElement(); final NODE target = en.getKey().getOtherElement(); if (source.equals(elem)) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel label = + final WeakEquivalenceEdgeLabel label = mWeakEquivalenceEdges.remove(en.getKey()); if (replacement != null) { mWeakEquivalenceEdges.put(new Doubleton(replacement, target), label); } } else if (target.equals(elem)) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel label = + final WeakEquivalenceEdgeLabel label = mWeakEquivalenceEdges.remove(en.getKey()); if (replacement != null) { mWeakEquivalenceEdges.put(new Doubleton(source, replacement), label); @@ -212,7 +217,7 @@ public void updateVerticesOnRemoveElement(final NODE elem, final NODE replacemen public Set projectSimpleElementInEdgeLabels(final NODE elem, final boolean useWeqGpa) { final Set nodesToAdd = new HashSet<>(); - for (final Entry, WeakEquivalenceEdgeLabel> en : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> en : mWeakEquivalenceEdges.entrySet()) { assert !elem.equals(en.getKey().getOneElement()); assert !elem.equals(en.getKey().getOtherElement()); @@ -223,9 +228,9 @@ public Set projectSimpleElementInEdgeLabels(final NODE elem, final boolean } public void transformElementsAndFunctions(final Function transformer) { - final HashMap, WeakEquivalenceEdgeLabel> weqEdgesCopy = + final HashMap, WeakEquivalenceEdgeLabel> weqEdgesCopy = new HashMap<>(mWeakEquivalenceEdges); - for (final Entry, WeakEquivalenceEdgeLabel> en : weqEdgesCopy.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> en : weqEdgesCopy.entrySet()) { mWeakEquivalenceEdges.remove(en.getKey()); final Doubleton newDton = new Doubleton<>( @@ -259,10 +264,10 @@ WeakEquivalenceGraph join(final WeakEquivalenceGraph other) { assert mPartialArrangement != null && other.mPartialArrangement != null : "we need the partial for the join" + "of the weq graphs, because strong equalities influence the weak ones.."; - final Map, WeakEquivalenceEdgeLabel> newWeakEquivalenceEdges = new HashMap<>(); - for (final Entry, WeakEquivalenceEdgeLabel> thisWeqEdge + final Map, WeakEquivalenceEdgeLabel> newWeakEquivalenceEdges = new HashMap<>(); + for (final Entry, WeakEquivalenceEdgeLabel> thisWeqEdge : this.mWeakEquivalenceEdges.entrySet()) { - final WeakEquivalenceEdgeLabel correspondingWeqEdgeLabelInOther = + final WeakEquivalenceEdgeLabel correspondingWeqEdgeLabelInOther = other.mWeakEquivalenceEdges.get(thisWeqEdge.getKey()); final NODE source = thisWeqEdge.getKey().getOneElement(); @@ -276,7 +281,7 @@ WeakEquivalenceGraph join(final WeakEquivalenceGraph other) { && other.mPartialArrangement.getEqualityStatus(source, target) == EqualityStatus.EQUAL) { // case "weak equivalence in this, strong equivalence in other" - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel newEdgeLabel = thisWeqEdge.getValue() + final WeakEquivalenceEdgeLabel newEdgeLabel = thisWeqEdge.getValue() .meet(Collections.singleton(this.mPartialArrangement)) .projectToElements(mFactory.getAllWeqNodes()); @@ -289,10 +294,10 @@ WeakEquivalenceGraph join(final WeakEquivalenceGraph other) { continue; } - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel thisNewEdgeLabel = thisWeqEdge.getValue() + final WeakEquivalenceEdgeLabel thisNewEdgeLabel = thisWeqEdge.getValue() .meet(Collections.singleton(this.mPartialArrangement)) .projectToElements(mFactory.getAllWeqNodes()); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel otherNewEdgeLabel = + final WeakEquivalenceEdgeLabel otherNewEdgeLabel = correspondingWeqEdgeLabelInOther .meet(Collections.singleton(other.mPartialArrangement)) .projectToElements(mFactory.getAllWeqNodes()); @@ -303,14 +308,14 @@ WeakEquivalenceGraph join(final WeakEquivalenceGraph other) { /* * for the case strong equivalence in this, weak equivalence in other, we iterate other's weak equivalence edges */ - for (final Entry, WeakEquivalenceEdgeLabel> otherWeqEdge + for (final Entry, WeakEquivalenceEdgeLabel> otherWeqEdge : other.mWeakEquivalenceEdges.entrySet()) { final NODE source = otherWeqEdge.getKey().getOneElement(); final NODE target = otherWeqEdge.getKey().getOtherElement(); if (this.mPartialArrangement.hasElements(source, target) && this.mPartialArrangement.getEqualityStatus(source, target) == EqualityStatus.EQUAL) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel newEdgeLabel = otherWeqEdge.getValue() + final WeakEquivalenceEdgeLabel newEdgeLabel = otherWeqEdge.getValue() .meet(Collections.singleton(other.mPartialArrangement)) .projectToElements(mFactory.getAllWeqNodes()); @@ -329,22 +334,36 @@ boolean hasArrayEqualities() { return !mArrayEqualities.isEmpty(); } - Map, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> close() { + Map, WeakEquivalenceEdgeLabel> close() { if (mWeakEquivalenceEdges.isEmpty()) { return Collections.emptyMap(); } final CachingWeqEdgeLabelPoComparator cwelpc = new CachingWeqEdgeLabelPoComparator(); - final FloydWarshall fw = - new FloydWarshall<>(cwelpc::isStrongerOrEqual, -// new FloydWarshall<>(WeakEquivalenceEdgeLabel::isStrongerThan, - cwelpc::union, -// WeakEquivalenceEdgeLabel::union, - WeakEquivalenceEdgeLabel::meet, - new WeakEquivalenceEdgeLabel(), - mWeakEquivalenceEdges, - WeakEquivalenceEdgeLabel::new); + final BiPredicate, WeakEquivalenceEdgeLabel> smallerThan = + cwelpc::isStrongerOrEqual; + final BiFunction, WeakEquivalenceEdgeLabel, WeakEquivalenceEdgeLabel> plus + = cwelpc::union; + final BiFunction, WeakEquivalenceEdgeLabel, WeakEquivalenceEdgeLabel> meet + = WeakEquivalenceEdgeLabel::meet; + final WeakEquivalenceEdgeLabel nullLabel = new WeakEquivalenceEdgeLabel<>(this); + final Map, WeakEquivalenceEdgeLabel> graph = mWeakEquivalenceEdges; + final Function, WeakEquivalenceEdgeLabel> labelCloner = + weqLabel -> new WeakEquivalenceEdgeLabel(this, weqLabel); + + final FloydWarshall> fw = + new FloydWarshall>( + smallerThan, plus, meet, nullLabel, graph, labelCloner); +// new FloydWarshall<>(this, +// cwelpc::isStrongerOrEqual, +//// new FloydWarshall<>(WeakEquivalenceEdgeLabel::isStrongerThan, +// cwelpc::union, +//// WeakEquivalenceEdgeLabel::union, +// WeakEquivalenceEdgeLabel::meet, +// new WeakEquivalenceEdgeLabel(this), +// mWeakEquivalenceEdges, +// WeakEquivalenceEdgeLabel::new); if (!fw.performedChanges()) { return Collections.emptyMap(); } @@ -356,7 +375,7 @@ Map, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> close( * @return true if this graph has no constraints/is tautological */ public boolean isEmpty() { - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> edge + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { if (!edge.getValue().isTautological()) { return false; @@ -366,9 +385,9 @@ public boolean isEmpty() { } public boolean isStrongerThan(final WeakEquivalenceGraph other) { - for (final Entry, WeakEquivalenceEdgeLabel> otherWeqEdgeAndLabel + for (final Entry, WeakEquivalenceEdgeLabel> otherWeqEdgeAndLabel : other.mWeakEquivalenceEdges.entrySet()) { - final WeakEquivalenceEdgeLabel correspondingWeqEdgeInThis = + final WeakEquivalenceEdgeLabel correspondingWeqEdgeInThis = this.mWeakEquivalenceEdges.get(otherWeqEdgeAndLabel.getKey()); if (correspondingWeqEdgeInThis == null) { // "other" has an edge that "this" does not -- this cannot be stronger @@ -392,7 +411,7 @@ public boolean isStrongerThan(final WeakEquivalenceGraph other) { public List getWeakEquivalenceConstraintsAsTerms(final Script script) { // assert mArrayEqualities == null || mArrayEqualities.isEmpty(); final List result = new ArrayList<>(); - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { final List dnfAsCubeList = new ArrayList<>(); dnfAsCubeList.addAll(edge.getValue().toDNF(script)); @@ -447,9 +466,9 @@ private List computeWeqIndicesForArray(final NODE array1) { return indexEntries; } - public Map getAdjacentWeqEdges(final NODE appliedFunction) { - final Map result = new HashMap<>(); - for (final Entry, WeakEquivalenceEdgeLabel> en : mWeakEquivalenceEdges.entrySet()) { + public Map> getAdjacentWeqEdges(final NODE appliedFunction) { + final Map> result = new HashMap<>(); + for (final Entry, WeakEquivalenceEdgeLabel> en : mWeakEquivalenceEdges.entrySet()) { if (en.getKey().getOneElement().equals(appliedFunction)) { result.put(en.getKey().getOtherElement(), en.getValue()); } @@ -460,7 +479,7 @@ public Map getAdjacentWeqEdges(final NODE appli return result; } - public Map, WeakEquivalenceEdgeLabel> getEdges() { + public Map, WeakEquivalenceEdgeLabel> getEdges() { return Collections.unmodifiableMap(mWeakEquivalenceEdges); } @@ -479,10 +498,10 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, assert paList.size() != 1 || !paList.iterator().next().isTautological() : "catch this case before?"; assert sanityCheck(); - final WeakEquivalenceEdgeLabel oldLabel = mWeakEquivalenceEdges.get(sourceAndTarget); + final WeakEquivalenceEdgeLabel oldLabel = mWeakEquivalenceEdges.get(sourceAndTarget); if (paList.isEmpty()) { - mWeakEquivalenceEdges.put(sourceAndTarget, new WeakEquivalenceEdgeLabel(paList)); + mWeakEquivalenceEdges.put(sourceAndTarget, new WeakEquivalenceEdgeLabel(this, paList)); mArrayEqualities.addPair(sourceAndTarget.getOneElement(), sourceAndTarget.getOtherElement()); return oldLabel == null || !oldLabel.isInconsistent(); } @@ -490,9 +509,9 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, if (oldLabel == null || oldLabel.isTautological()) { assert paList.size() != 1 || !paList.iterator().next().isTautological(); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel newLabel = new WeakEquivalenceEdgeLabel(paList); + final WeakEquivalenceEdgeLabel newLabel = new WeakEquivalenceEdgeLabel(this, paList); newLabel.meetWithCcGpa(); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel newLabelMeetProject = + final WeakEquivalenceEdgeLabel newLabelMeetProject = newLabel.projectToElements(mFactory.getAllWeqNodes()); mWeakEquivalenceEdges.put(sourceAndTarget, newLabelMeetProject); @@ -500,9 +519,9 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, return true; } - final WeakEquivalenceEdgeLabel oldLabelCopy = new WeakEquivalenceEdgeLabel(oldLabel); + final WeakEquivalenceEdgeLabel oldLabelCopy = new WeakEquivalenceEdgeLabel(this, oldLabel); - final WeakEquivalenceEdgeLabel labelToStrengthenWith = new WeakEquivalenceEdgeLabel(paList); + final WeakEquivalenceEdgeLabel labelToStrengthenWith = new WeakEquivalenceEdgeLabel(this, paList); assert labelToStrengthenWith.sanityCheck() : "input label not normalized??"; labelToStrengthenWith.meetWithCcGpa(); @@ -512,7 +531,7 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, return false; } - WeakEquivalenceEdgeLabel strengthenedEdgeLabel = oldLabelCopy.meet(labelToStrengthenWith); + WeakEquivalenceEdgeLabel strengthenedEdgeLabel = oldLabelCopy.meet(labelToStrengthenWith); // meet with gpa (done before) and project afterwards strengthenedEdgeLabel = strengthenedEdgeLabel.projectToElements(mFactory.getAllWeqNodes()); @@ -541,7 +560,7 @@ private boolean strengthenEdgeLabel(final Doubleton sourceAndTarget, * @param value */ private boolean reportWeakEquivalence(final Doubleton sourceAndTarget, - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel value) { + final WeakEquivalenceEdgeLabel value) { assert mPartialArrangement.isRepresentative(sourceAndTarget.getOneElement()) && mPartialArrangement.isRepresentative(sourceAndTarget.getOtherElement()); assert sourceAndTarget.getOneElement().getTerm().getSort().equals(sourceAndTarget.getOtherElement().getTerm().getSort()); @@ -559,13 +578,13 @@ public boolean reportWeakEquivalence(final NODE array1, final NODE array2, } final boolean result = reportWeakEquivalence(new Doubleton(array1, array2), - new WeakEquivalenceEdgeLabel(edgeLabelContents)); + new WeakEquivalenceEdgeLabel(this, edgeLabelContents)); assert sanityCheck(); return result; } public boolean isConstrained(final NODE elem) { - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { if (edge.getValue().isConstrained(elem)) { return true; } @@ -574,7 +593,7 @@ public boolean isConstrained(final NODE elem) { } public Set> getEdgeLabelContents(final NODE array1, final NODE array2) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel edge = + final WeakEquivalenceEdgeLabel edge = mWeakEquivalenceEdges.get(new Doubleton<>(array1, array2)); if (edge != null) { return edge.getLabelContents(); @@ -597,8 +616,8 @@ public Set> projectEdgeLabelToPoint( final Set> labelContents, final NODE value, final List weqVarsForThisEdge) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel originalEdgeLabel = - new WeakEquivalenceEdgeLabel(labelContents); + final WeakEquivalenceEdgeLabel originalEdgeLabel = + new WeakEquivalenceEdgeLabel(this, labelContents); final NODE firstDimWeqVarNode = weqVarsForThisEdge.get(0); @@ -606,13 +625,13 @@ public Set> projectEdgeLabelToPoint( qEqualsI.reportEquality(firstDimWeqVarNode, value); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel copy = - new WeakEquivalenceEdgeLabel(originalEdgeLabel); + final WeakEquivalenceEdgeLabel copy = + new WeakEquivalenceEdgeLabel(this, originalEdgeLabel); // copy.meetWithWeqGpa(); copy.meetWithCcGpa(); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel meet = + final WeakEquivalenceEdgeLabel meet = copy.meetRec(Collections.singleton(qEqualsI)); meet.setExternalRemInfo(mPartialArrangement.getElementCurrentlyBeingRemoved()); @@ -626,7 +645,7 @@ public Set> projectEdgeLabelToPoint( assert meet.sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel result = + final WeakEquivalenceEdgeLabel result = meet.projectToElements(new HashSet<>(weqVarsForThisEdge)); assert result.assertHasOnlyWeqVarConstraints(new HashSet<>(weqVarsForThisEdge)); @@ -648,8 +667,8 @@ public Set> shiftLabelAndAddException( final List weqVarsForResolventEdge) { assert !weqVarsForResolventEdge.isEmpty() : "because the array in the resolvent must have a dimension >= 1"; - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel meet = - new WeakEquivalenceEdgeLabel(labelContents); + final WeakEquivalenceEdgeLabel meet = + new WeakEquivalenceEdgeLabel(this, labelContents); // meet.meetWithWeqGpa(); meet.meetWithCcGpa(); @@ -657,7 +676,7 @@ public Set> shiftLabelAndAddException( meet.setExternalRemInfo(mPartialArrangement.getElementCurrentlyBeingRemoved()); meet.projectWeqVarNode(weqVarsForResolventEdge.get(weqVarsForResolventEdge.size() - 1)); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel labelToShiftAndAdd = + final WeakEquivalenceEdgeLabel labelToShiftAndAdd = meet.projectToElements(new HashSet<>(weqVarsForResolventEdge)); labelToShiftAndAdd.inOrDecreaseWeqVarIndices(1, weqVarsForResolventEdge); @@ -721,14 +740,14 @@ public void updateForNewRep(final NODE node1OldRep, final NODE node2OldRep, fina if (node1OldRep == newRep) { // node2OldRep is not representative anymore - for (final Entry.WeakEquivalenceEdgeLabel> edge + for (final Entry> edge : getAdjacentWeqEdges(node2OldRep).entrySet()) { mWeakEquivalenceEdges.remove(new Doubleton<>(node2OldRep, edge.getKey())); mWeakEquivalenceEdges.put(new Doubleton<>(newRep, edge.getKey()), edge.getValue()); } } else { // node1OldRep is not representative anymore - for (final Entry.WeakEquivalenceEdgeLabel> edge + for (final Entry> edge : getAdjacentWeqEdges(node1OldRep).entrySet()) { mWeakEquivalenceEdges.remove(new Doubleton<>(node1OldRep, edge.getKey())); mWeakEquivalenceEdges.put(new Doubleton<>(newRep, edge.getKey()), edge.getValue()); @@ -770,21 +789,21 @@ public Integer getMaxSizeOfEdgeLabelStatistic() { * edgeLabels in the gpa (mPartialArrangement)) */ public void meetEdgeLabelsWithWeqGpaBeforeRemove(final WeqCongruenceClosure originalPa) { - for (final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel edgeLabel : mWeakEquivalenceEdges.values()) { + for (final WeakEquivalenceEdgeLabel edgeLabel : mWeakEquivalenceEdges.values()) { edgeLabel.meetWithWeqGpa(originalPa); } // mWeqMeetMode = true; } public void meetEdgeLabelsWithCcGpaBeforeRemove() { - for (final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel edgeLabel : mWeakEquivalenceEdges.values()) { + for (final WeakEquivalenceEdgeLabel edgeLabel : mWeakEquivalenceEdges.values()) { edgeLabel.meetWithCcGpa(); } // mWeqMeetMode = false; } public boolean elementIsFullyRemoved(final NODE elem) { - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> edge + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { if (edge.getKey().getOneElement().equals(elem)) { assert false; @@ -833,7 +852,7 @@ public String toString() { sb.append(String.format("%s : %d\n", en.getKey(), en.getValue())); } sb.append("graph shape:\n"); - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> weq : + for (final Entry, WeakEquivalenceEdgeLabel> weq : mWeakEquivalenceEdges.entrySet()) { sb.append(weq.getKey()); sb.append("\n"); @@ -844,7 +863,7 @@ public String toString() { public String toLogString() { final StringBuilder sb = new StringBuilder(); - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> weq : + for (final Entry, WeakEquivalenceEdgeLabel> weq : mWeakEquivalenceEdges.entrySet()) { sb.append(weq.getKey()); sb.append("\n"); @@ -856,21 +875,25 @@ public String toLogString() { } boolean sanityCheck() { - // if (mPartialArrangement.mMeetWithGpaCase) { - // // TODO sharpen sanity check for this case - // return true; - // } - - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> en - : mWeakEquivalenceEdges.entrySet()) { - assert en.getValue().sanityCheck(); - } - - assert sanityAllNodesOnWeqLabelsAreKnownToGpa(null); + // if (mPartialArrangement.mMeetWithGpaCase) { + // // TODO sharpen sanity check for this case + // return true; + // } + if (mPartialArrangement != null && mPartialArrangement.isInconsistent()) { + // we will drop this weak equivalence graph anyway + return true; + } - return sanityCheckWithoutNodesComparison(); + for (final Entry, WeakEquivalenceEdgeLabel> en + : mWeakEquivalenceEdges.entrySet()) { + assert en.getValue().sanityCheck(); } + assert sanityAllNodesOnWeqLabelsAreKnownToGpa(null); + + return sanityCheckWithoutNodesComparison(); + } + boolean sanityCheckWithoutNodesComparison() { assert mFactory != null : "factory is needed for the sanity check.."; @@ -879,7 +902,7 @@ boolean sanityCheckWithoutNodesComparison() { * check that the edges only connect compatible arrays * compatible means having the same Sort, in particular: dimensionality */ - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { final NODE source = edge.getKey().getOneElement(); final NODE target = edge.getKey().getOtherElement(); if (!source.hasSameTypeAs(target)) { @@ -892,7 +915,7 @@ boolean sanityCheckWithoutNodesComparison() { * Check that all the edges are between equivalence representatives of mPartialArrangement */ if (mPartialArrangement != null) { - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { final NODE source = edge.getKey().getOneElement(); final NODE target = edge.getKey().getOtherElement(); if (!mPartialArrangement.hasElement(source)) { @@ -932,7 +955,7 @@ boolean sanityCheckWithoutNodesComparison() { /* * check that we have remembered every inconsistent edge label in mArrayEqualities (for later cleanup) */ - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { final NODE source = edge.getKey().getOneElement(); final NODE target = edge.getKey().getOtherElement(); if (edge.getValue().isInconsistent() @@ -952,9 +975,9 @@ boolean sanityCheckWithoutNodesComparison() { */ protected boolean sanityAllNodesOnWeqLabelsAreKnownToGpa(final Set nodesScheduledForAdding) { if (mPartialArrangement != null) { - for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { + for (final Entry, WeakEquivalenceEdgeLabel> edge : mWeakEquivalenceEdges.entrySet()) { - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel label = edge.getValue(); + final WeakEquivalenceEdgeLabel label = edge.getValue(); final Set nodesOnEdgeLabelWithoutWeqNodes = label.getAppearingNodes().stream() .filter(node -> !CongruenceClosure.dependsOnAny(node, mFactory.getAllWeqNodes())) @@ -981,12 +1004,12 @@ public CachingWeqEdgeLabelPoComparator() { mCcPoCache = new PartialOrderCache<>(mCcManager.getCcComparator()); } - boolean isStrongerOrEqual(final WeakEquivalenceEdgeLabel label1, - final WeakEquivalenceEdgeLabel label2) { + boolean isStrongerOrEqual(final WeakEquivalenceEdgeLabel label1, + final WeakEquivalenceEdgeLabel label2) { return label1.isStrongerThan(label2, mCcPoCache::lowerEqual); } - WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel label1, final WeakEquivalenceEdgeLabel label2) { + WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel label1, final WeakEquivalenceEdgeLabel label2) { return label1.union(label2, mCcPoCache); } @@ -996,631 +1019,8 @@ static class WeqSettings { static final boolean FLATTEN_WEQ_EDGES_BEFORE_JOIN = !false; } - /** - * Represents an edge label in the weak equivalence graph. - * An edge label connects two arrays of the same arity(dimensionality) #a. - * An edge label is a tuple of length #a. - * Each tuple element is a set of partial arrangements. The free variables in the partial arrangements are the - * variables of the EqConstraint together with #a special variables that are implicitly universally quantified - * and range over the array positions. - * - */ - class WeakEquivalenceEdgeLabel { - - private final Set> mLabel; - - /** - * Copy constructor. - * - * @param original - */ - public WeakEquivalenceEdgeLabel(final WeakEquivalenceEdgeLabel original) { - mLabel = new HashSet<>(original.getLabelContents().size()); - for (final CongruenceClosure l : original.getLabelContents()) { - assert !l.isInconsistent(); - assert !l.isTautological() || original.getLabelContents().size() == 1; - mLabel.add(new CongruenceClosure<>(l)); - } - assert sanityCheck(); - } - - /** - * - * @return a copy of this weq edge where all disjuncts have been joined into one - */ - public WeakEquivalenceGraph.WeakEquivalenceEdgeLabel flatten() { - if (isInconsistent()) { - return this; - } - return new WeakEquivalenceEdgeLabel(Collections.singleton( - mLabel.stream().reduce((cc1, cc2) -> cc1.join(cc1)).get())); - } - - public void setExternalRemInfo(final CongruenceClosure.RemoveElement remInfo) { - for (final CongruenceClosure lab : mLabel) { - lab.setExternalRemInfo(remInfo); - } - } - - public boolean hasExternalRemInfo() { - for (final CongruenceClosure l : mLabel) { - assert l.assertHasExternalRemInfo(); - } - return true; - } - - public boolean assertHasOnlyWeqVarConstraints(final Set weqVarsForThisEdge) { - for (final CongruenceClosure l : mLabel) { - if (!l.assertHasOnlyWeqVarConstraints(weqVarsForThisEdge)) { - assert false; - return false; - } - } - return true; - } - - /** - * Construct a weak equivalence edge from a list of label contents. - * - * Does some simplifications. - * - * @param newLabelContents - */ - public WeakEquivalenceEdgeLabel(final Set> newLabelContents) { - mLabel = mCcManager.filterRedundantCcs(newLabelContents); - if (mLabel.size() == 1 && mLabel.iterator().next().isInconsistent()) { - //case mLabel = "[False]" -- filterRedundantCcs leaves this case so we have to clean up manually to "[]" - mLabel.clear(); - } - assert sanityCheck(); - } - - /** - * Constructs an empty edge. (labeled "true") - */ - public WeakEquivalenceEdgeLabel() { - mLabel = new HashSet<>(); - mLabel.add(new CongruenceClosure<>()); - assert sanityCheck(); - } - - public void projectWeqVarNode(final NODE firstDimWeqVarNode) { - for (final CongruenceClosure lab : mLabel) { - lab.removeSimpleElementDontIntroduceNewNodes(firstDimWeqVarNode); - } - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - - public Set projectSimpleElement(final NODE elem, final boolean useWeqGpaMode) { - if (isTautological()) { - return Collections.emptySet(); - } - if (isInconsistent()) { - return Collections.emptySet(); - } - - final Set nodesToAddToGpa = new HashSet<>(); - - final List> newLabelContents = new ArrayList<>(mLabel.size()); - for (final CongruenceClosure lab : mLabel) { - assert lab.sanityCheckOnlyCc(mPartialArrangement.getElementCurrentlyBeingRemoved()); - - /* - * just removing elem is not enough - * example: - * elem = a - * label has a[q] - * then a[q] needs to be removed, but mPartialArrangement cannot know that.. - * - * actually, even removeSimpleElement is not enough, because we might be removing - * a[i], a (in that order) - * then during removing a[i] we add a node a[q], but dont insert a, because it is in remInfo - * then when we remove a, the removeSimpleElement will just say the cc does not have a and do - * nothing - * - * plan: compute all dependents, and remove them one by one - */ - if (useWeqGpaMode) { - /* - * current label has been joined with WeqGpa - * (i.e. lab is a WeqCongruenceClosure, not only a CongruenceClosure) - * use CcGpa inside this remove.. (avoids endless recursion) - */ - final Set nodesAdded = lab.removeSimpleElementDontUseWeqGpaTrackAddedNodes(elem); - // some nodes may have been introduced - nodesAdded.stream() - .filter(n -> !CongruenceClosure.dependsOnAny(n, mFactory.getAllWeqPrimedNodes())) - .forEach(nodesToAddToGpa::add); - } else { - /* - * lightweight case, current label is a CongruenceClosure, not a WeqCongruenceClosure - * --> we do not allow introduction of new nodes during the remove operation in the labels here - */ - lab.removeSimpleElementDontIntroduceNewNodes(elem); - } - - assert lab.assertSingleElementIsFullyRemoved(elem); - - if (lab.isTautological()) { - // a disjunct became "true" through projection --> the whole disjunction is tautological - mLabel.clear(); - mLabel.add(new CongruenceClosure<>()); - return Collections.emptySet(); - } - assert lab.sanityCheckOnlyCc(mPartialArrangement.getElementCurrentlyBeingRemoved()); - - final CongruenceClosure lab2; - if (useWeqGpaMode) { - // unprime weqvars - lab2 = new CongruenceClosure<>(lab); - lab2.transformElementsAndFunctions( - node -> node.renameVariables(mFactory.getWeqPrimedVarsToWeqVars())); - } else { - lab2 = lab; - } - - final CongruenceClosure newLab = lab2.projectToElements(mFactory.getAllWeqNodes(), - mPartialArrangement.getElementCurrentlyBeingRemoved()); - assert newLab.assertSingleElementIsFullyRemoved(elem); - assert !newLab.isTautological(); - assert newLab.sanityCheckOnlyCc(mPartialArrangement.getElementCurrentlyBeingRemoved()); - newLabelContents.add(newLab); - } - mLabel.clear(); - mLabel.addAll(newLabelContents); - assert mLabel.stream().allMatch(l -> l.assertSingleElementIsFullyRemoved(elem)); - assert sanityCheck(); - return nodesToAddToGpa; - } - - public WeakEquivalenceEdgeLabel projectToElements(final Set allWeqNodes) { - if (isInconsistent()) { - return this; - } - final Set> newLabelContents = new HashSet<>(); - for (final CongruenceClosure item : mLabel) { - newLabelContents.add(item.projectToElements(allWeqNodes, - mPartialArrangement.getElementCurrentlyBeingRemoved())); - } - assert newLabelContents.stream().allMatch(l -> l.sanityCheckOnlyCc()); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel result = - new WeakEquivalenceEdgeLabel(newLabelContents); - assert result.sanityCheck(); - return result; - } - - /** - * - * - * @param inOrDecrease how much to shift (negative value for decrease) - * @param weqVarsForThisEdge this edgeLabel does not know the function signature of its source and target; - * thus we pass a list of weqVars that belongs to that signature (those are the ones to be shifted..) - * they must be in correct order of dimensions according to source/target - */ - public void inOrDecreaseWeqVarIndices(final int inOrDecrease, final List weqVarsForThisEdge) { - assert inOrDecrease == 1 || inOrDecrease == -1 : "we don't expect any other cases"; - assert inOrDecrease != 1 || !this.getAppearingNodes() - .contains(weqVarsForThisEdge.get(weqVarsForThisEdge.size() - 1)) : "project the highest weqvar " - + "before increasing!"; - assert inOrDecrease != -1 || !this.getAppearingNodes() - .contains(weqVarsForThisEdge.get(0)) : "project the lowest weqvar before decreasing!"; - - final Map substitutionMapping = new HashMap<>(); - for (int i = 0; i < weqVarsForThisEdge.size(); i++) { - final NODE nodeI = weqVarsForThisEdge.get(i); - final int newDim = i + inOrDecrease; - // the others (newDim <0) should have been projected out of the formula before.. (in the calling method) - if (newDim >= 0 && newDim < weqVarsForThisEdge.size()) { - substitutionMapping.put(nodeI.getTerm(), - mFactory.getWeqVariableForDimension(newDim, nodeI.getSort())); - } - } - this.transformElements(e -> e.renameVariables(substitutionMapping)); - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - - public boolean isConstrained(final NODE elem) { - return mLabel.stream().anyMatch(l -> l.isConstrained(elem)); - } - - public Set> getLabelContents() { - return Collections.unmodifiableSet(mLabel); - } - - public boolean isInconsistent() { - for (final CongruenceClosure pa : getLabelContents()) { - if (!pa.isInconsistent()) { - // we found one consistent disjunct --> this label is consistent - return false; - } else { - // current cc is inconsistent - assert getLabelContents().size() == 1 : "we are filtering out all but one 'bottoms', right?"; - } - } - return true; - } - - /** - * Called when the ground partial arrangement (gpa) has changed. - * Checks if any entry of a weq label became inconsistent through the change, removes that entry, propagates - * an array equality if the whole edge became inconsistent - * - * --> does edge inconsistency based propagations (weak equivalences becoming strong ones) - * --> does not do congruence style weq propagations, those are done separately when an equality is added - * to the gpa - * - * @param reportX lambda, applying one of the CongruenceClosure.report functions to some nodes for a given - * CongruenceClosure object - * @return a fresh, updated WeqLabel, null if the label became inconsistent - */ - public WeakEquivalenceEdgeLabel reportChangeInGroundPartialArrangement( - final Predicate> reportX) { - assert this.sanityCheck(); - - - final Set> newLabel = new HashSet<>(); - - for (final CongruenceClosure l : mLabel) { - assert mPartialArrangement.sanityCheck(); - assert l.sanityCheckOnlyCc(); - final CongruenceClosure currentPaWgpa = mCcManager.getMeet(l, mPartialArrangement, - mPartialArrangement.getElementCurrentlyBeingRemoved()); - - if (currentPaWgpa.isInconsistent()) { - // label element became inconsistent, don't add it to the new label - continue; - } - - final boolean change = reportX.test(currentPaWgpa); - - if (!change) { - /* - * no change in mLabelWgpa[i] meet gpa -- this can happen, because labelWgpa might imply an - * equality that is not present in gpa.. - * - * no checks need to be made here, anyway - */ - newLabel.add(l); - assert !currentPaWgpa.isInconsistent(); - continue; - } - - // add the strengthened version as the new label element - newLabel.add(currentPaWgpa.projectToElements(mFactory.getAllWeqNodes(), - mPartialArrangement.getElementCurrentlyBeingRemoved())); - - assert WeakEquivalenceGraph.this.sanityCheck(); - } - assert newLabel.stream().allMatch(CongruenceClosure::sanityCheckOnlyCc); - return new WeakEquivalenceEdgeLabel(newLabel); - } - - /** - * Computes a DNF from this label as a List of conjunctive Terms. - * The disjunction has the form \/_i pa_i - * - * @param script - * @return a DNF as a List of conjunctive Terms. - */ - public List toDNF(final Script script) { - final List result = new ArrayList<>(); - for (final CongruenceClosure cc : mLabel) { - final List cube = EqConstraint.partialArrangementToCube(script, cc); - final Term cubeTerm = SmtUtils.and(script, cube); - result.add(cubeTerm); - } - return result; - } - - public void transformElements(final Function transformer) { - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); -// for (int i = 0; i < getLabelContents().size(); i++) { - for (final CongruenceClosure l : mLabel) { - l.transformElementsAndFunctions(transformer); - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - - /** - * Returns all NODEs that are used in this WeqEdgeLabel. - * Not including the special quantified variable's nodes. - * @return - */ - public Set getAppearingNodes() { - final Set res = new HashSet<>(); - getLabelContents().forEach(pa -> res.addAll(pa.getAllElements())); - return res; - } - - public WeakEquivalenceEdgeLabel meet(final WeakEquivalenceEdgeLabel otherLabel) { - return meet(otherLabel.getLabelContents()); - } - - private WeakEquivalenceEdgeLabel meet(final Set> paList) { - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - return meetRec(paList); - } - - private WeakEquivalenceEdgeLabel meetRec(final Set> paList) { - final Set> newLabelContent = new HashSet<>(); - for (final CongruenceClosure lc1 : mLabel) { - for (final CongruenceClosure lc2 : paList) { - newLabelContent.add(lc1.meetRec(lc2)); - } - } - - final Set> newLabel = mCcManager.filterRedundantCcs(newLabelContent); - assert newLabel.stream().allMatch(l -> l.sanityCheckOnlyCc()); - - final Set> newLabelProjected = newLabel.stream() - .map(l -> l.projectToElements(mFactory.getAllWeqNodes(), - mPartialArrangement.getElementCurrentlyBeingRemoved())).collect(Collectors.toSet()); - assert newLabelProjected.stream() - .allMatch(l -> l.sanityCheckOnlyCc(mPartialArrangement.getElementCurrentlyBeingRemoved())); - - final WeakEquivalenceEdgeLabel result = - new WeakEquivalenceEdgeLabel(newLabelProjected); - assert result.sanityCheck(); - return result; - } - - /** - * rule: A isStrongerThan B - * iff - * forall ai exists bi. ai subseteq bi - * @param ccPoCache - * @param value - * @return - */ - public boolean isStrongerThan(final WeakEquivalenceEdgeLabel other) { - return isStrongerThan(other, CongruenceClosure::isStrongerThan); - } - - public boolean isStrongerThan(final WeakEquivalenceEdgeLabel other, - final BiPredicate, CongruenceClosure> lowerOrEqual) { - for (final CongruenceClosure paThis : getLabelContents()) { - boolean existsWeaker = false; - for (final CongruenceClosure paOther : other.getLabelContents()) { - if (lowerOrEqual.test(paThis, paOther)) { - existsWeaker = true; - break; - } - } - if (!existsWeaker) { - return false; - } - } - return true; - } - - - - /** - * Computes a constraint which, for every dimension, has the union of the disjuncts of both input labels - * (this and other). - * @param ccPoCache - * @param correspondingWeqEdgeInOther - * @return - */ - public WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel other) { - return this.union(other, null); - } - - public WeakEquivalenceEdgeLabel union(final WeakEquivalenceEdgeLabel other, - final PartialOrderCache> ccPoCache) { - assert this.sanityCheck() && other.sanityCheck(); - // assert this.mLabel.size() < 10 && other.mLabel.size() < 10; - final List> unionList = new ArrayList<>( - mLabel.size() + other.getLabelContents().size()); - unionList.addAll(mLabel); - unionList.addAll(other.getLabelContents()); - - final Set> filtered = ccPoCache == null ? - mCcManager.filterRedundantCcs(new HashSet<>(unionList)) - : mCcManager.filterRedundantCcs(new HashSet<>(unionList), ccPoCache); - - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel result = new WeakEquivalenceEdgeLabel(filtered); - assert result.sanityCheck(); - return result; - } - - private boolean isTautological() { - for (final CongruenceClosure l : getLabelContents()) { - if (l.isTautological()) { - assert getLabelContents().size() == 1; - return true; - } - } - return false; - } - - - @Override - public String toString() { - if (mLabel.size() < 3) { - return toLogString(); - } - return "weq edge label, size: " + mLabel.size(); - } - - public String toLogString() { - final StringBuilder sb = new StringBuilder(); - - mLabel.forEach(l -> sb.append(l.toLogString() + "\n")); - return sb.toString(); - } - - private boolean sanityCheck() { - return sanityCheck(mPartialArrangement); - } - - private boolean sanityCheck(final WeqCongruenceClosure groundPartialArrangement) { - if (mFactory == null) { - return true; - } - if (isEmpty()) { - return true; - } - - if (mLabel.stream().anyMatch(l -> l.isTautological()) && mLabel.size() > 1) { - // not normalized - assert false; - return false; - } - - if (mLabel.stream().anyMatch(l -> l.isInconsistent())) { - // not normalized - assert false; - return false; - } - - // check that labels are free of weqPrimed vars - if (!groundPartialArrangement.mMeetWithGpaCase) { - for (final CongruenceClosure lab : mLabel) { - for (final NODE el : lab.getAllElements()) { - if (CongruenceClosure.dependsOnAny(el, mFactory.getAllWeqPrimedNodes())) { - assert false; - return false; - } - } - } - } - - // check that labels are free of constraints that don't contain weq nodes - for (final CongruenceClosure lab : mLabel) { - assert lab.assertHasOnlyWeqVarConstraints(mFactory.getAllWeqNodes()); - } - - return sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - - public void meetWithWeqGpa(final WeqCongruenceClosure originalPa) { - - final List> newLabelContents = new ArrayList<>(); - for (final CongruenceClosure l : mLabel) { - - // make a copy of the full abstract state (ground partial arrangement and weak equivalence graph, weqCc) - final WeqCongruenceClosure paCopy = new WeqCongruenceClosure<>(originalPa, true); - - - // make a copy of the label, prime the weq vars - final CongruenceClosure lCopy = new CongruenceClosure<>(l); - lCopy.transformElementsAndFunctions(n -> n.renameVariables(mFactory.getWeqVarsToWeqPrimedVars())); - - // report all constraints from the label into the copy of the weqCc - for (final Entry eq : lCopy.getSupportingElementEqualities().entrySet()) { - if (paCopy.isInconsistent()) { - mLabel.clear(); - return; - } - paCopy.reportEquality(eq.getKey(), eq.getValue()); - } - for (final Entry deq : lCopy.getElementDisequalities().entrySet()) { - if (paCopy.isInconsistent()) { - mLabel.clear(); - return; - } - paCopy.reportDisequality(deq.getKey(), deq.getValue()); - } - - if (paCopy.isTautological()) { - mLabel.clear(); - mLabel.add(new CongruenceClosure()); - return; - } - newLabelContents.add(paCopy); - } - - mLabel.clear(); - mLabel.addAll(newLabelContents); - - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - - } - - public void meetWithCcGpa() { - meetWithGpa(false); - } - - public void meetWithGpa(final boolean meetWithFullWeqCc) { - - final Set> newLabelContents = new HashSet<>(); -// for (int i = 0; i < getLabelContents().size(); i++) { - for (final CongruenceClosure l : mLabel) { - if (l.isTautological()) { - // we have one "true" disjunct --> the whole disjunction is tautological - if (mLabel.size() == 1) { - return; - } - mLabel.clear(); - mLabel.add(new CongruenceClosure<>()); - return; - } - final CongruenceClosure meet; - if (meetWithFullWeqCc) { - meet = mCcManager.getWeqMeet(l, mPartialArrangement); - } else { - meet = mCcManager.getMeet(l, mPartialArrangement, mPartialArrangement.getElementCurrentlyBeingRemoved()); - } - - if (meet.isInconsistent()) { - /* label element is inconsistent with the current gpa - * --> omit it from the new label - */ - continue; - } - if (meet.isTautological()) { - assert false : "this should never happen because if the meet is tautological then mLabel.get(i)" - + "is, too, right?"; - // we have one "true" disjunct --> the whole disjunction is tautological - mLabel.clear(); - mLabel.add(new CongruenceClosure<>()); - return; - } - newLabelContents.add(meet); - } - assert newLabelContents.size() <= 1 || !newLabelContents.stream().anyMatch(c -> c.isTautological()); - - - mLabel.clear(); - mLabel.addAll(newLabelContents); - - assert sanityCheckDontEnforceProjectToWeqVars(mPartialArrangement); - } - - private boolean sanityCheckDontEnforceProjectToWeqVars(final CongruenceClosure groundPartialArrangement) { - for (final CongruenceClosure lab : mLabel) { - if (!lab.sanityCheckOnlyCc(groundPartialArrangement.getElementCurrentlyBeingRemoved())) { - assert false; - return false; - } - } - - // check label normalization - if (mLabel.stream().anyMatch(pa -> pa.isTautological()) && mLabel.size() != 1) { - assert false : "missing normalization: if there is one 'true' disjunct, we can drop" - + "all other disjuncts"; - return false; - } - - if (mLabel.stream().anyMatch(pa -> pa.isInconsistent())) { - assert false : "missing normalization: contains 'false' disjuncts"; - return false; - } - - return true; - } - - public boolean assertElementIsFullyRemoved(final NODE elem) { - for (final CongruenceClosure lab : mLabel) { - if (!lab.assertSingleElementIsFullyRemoved(elem)) { - assert false; - return false; - } - } - return true; - } - } +// 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 60cd5616249..56b6b3d37a1 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 @@ -69,7 +69,8 @@ public WeqCongruenceClosure addNode(final NODE node, final WeqCongruenceCl } private WeqCongruenceClosure unfreeze(final WeqCongruenceClosure origWeqCc) { - return new WeqCongruenceClosure<>(origWeqCc); + assert origWeqCc.isFrozen(); + return new WeqCongruenceClosure<>(origWeqCc, false); } public Set> filterRedundantCcs(final Set> ccs) { @@ -98,4 +99,16 @@ public WeqCongruenceClosure reportEquality(final NODE node1, final NODE no unfrozen.freeze(); return unfrozen; } + + public WeqCongruenceClosure makeCopyForWeqMeet(final WeqCongruenceClosure originalPa) { + return new WeqCongruenceClosure<>(originalPa, true); + } + + public WeqCongruenceClosure makeCopy(final WeqCongruenceClosure original) { + if (original.isFrozen()) { + // original is frozen --> a copy should not be necessary (use unfreeze if an unfrozen copy is needed) + return original; + } + return new WeqCongruenceClosure<>(original, false); + } } 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 4c570cecf41..110c6cd55c1 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 @@ -39,6 +39,7 @@ import de.uni_freiburg.informatik.ultimate.logic.Script; import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.WeakEquivalenceGraph.WeqSettings; import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils; import de.uni_freiburg.informatik.ultimate.util.datastructures.CongruenceClosure; import de.uni_freiburg.informatik.ultimate.util.datastructures.DataStructureUtils; @@ -131,19 +132,19 @@ public WeqCongruenceClosure(final WeqCongruenceClosure original, final boo mMeetWithGpaCase = meetWGpaCase; mFactory = original.mFactory; mWeakEquivalenceGraph = new WeakEquivalenceGraph<>(this, original.mWeakEquivalenceGraph, - false); -// meetWGpaCase && WeqSettings.FLATTEN_WEQ_EDGES_BEFORE_JOIN); //TODO simplify +// false); + meetWGpaCase && WeqSettings.FLATTEN_WEQ_EDGES_BEFORE_JOIN); //TODO simplify assert sanityCheck(); } - /** - * copy constructor - * - * @param original - */ - public WeqCongruenceClosure(final WeqCongruenceClosure original) { - this(original, false); - } +// /** +// * copy constructor +// * +// * @param original +// */ +// public WeqCongruenceClosure(final WeqCongruenceClosure original) { +// this(original, false); +// } public Term getTerm(final Script script) { final List allConjuncts = new ArrayList<>(); @@ -175,7 +176,8 @@ private WeqCongruenceClosure alignElementsAndFunctionsWeqRec(final Congrue assert !this.isInconsistent() && !otherCC.isInconsistent(); assert remInfo == null; - final WeqCongruenceClosure result = new WeqCongruenceClosure<>(this); +// final WeqCongruenceClosure result = new WeqCongruenceClosure<>(this); + final WeqCongruenceClosure result = mFactory.getCcManager().makeCopy(this); assert result.sanityCheck(); for (final NODE e : otherCC.getAllElements()) { @@ -233,12 +235,13 @@ boolean executeFloydWarshallAndReportResultToWeqCc() { return false; } boolean fwmc = false; - final Map, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> fwResult = mWeakEquivalenceGraph + final Map, WeakEquivalenceEdgeLabel> fwResult = mWeakEquivalenceGraph .close(); - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> fwEdge : fwResult + for (final Entry, WeakEquivalenceEdgeLabel> fwEdge : fwResult .entrySet()) { fwmc |= reportWeakEquivalenceDoOnlyRoweqPropagations(fwEdge.getKey().getOneElement(), fwEdge.getKey().getOtherElement(), fwEdge.getValue().getLabelContents()); + assert sanityCheck(); } return fwmc; } @@ -420,10 +423,22 @@ protected boolean reportEqualityRec(final NODE node1, final NODE node2) { final NODE newRep = getRepresentativeElement(node1); mWeakEquivalenceGraph.updateForNewRep(node1OldRep, node2OldRep, newRep); + if (isInconsistent()) { + return true; + } + doFwccAndBwccPropagationsFromMerge(propInfo); + if (isInconsistent()) { + return true; + } + doRoweqPropagationsOnMerge(node1, node2, node1OldRep, node2OldRep, oldAuxData); + if (isInconsistent()) { + return true; + } + // executeFloydWarshallAndReportResult(); /* @@ -567,10 +582,10 @@ private boolean otherRoweqPropOnMerge(final NODE nodeOldRep, final CcAuxData old boolean madeChanges = false; for (final Entry ccc : oldAuxData.getCcChildren(nodeOldRep)) { // ccc = (b,j) , as in b[j] - for (final Entry.WeakEquivalenceEdgeLabel> edgeAdjacentToNode + for (final Entry> edgeAdjacentToNode : mWeakEquivalenceGraph .getAdjacentWeqEdges(nodeOldRep).entrySet()) { final NODE n = edgeAdjacentToNode.getKey(); - final WeakEquivalenceGraph.WeakEquivalenceEdgeLabel phi = edgeAdjacentToNode.getValue(); + final WeakEquivalenceEdgeLabel phi = edgeAdjacentToNode.getValue(); // TODO is it ok here to use that auxData from after the merge?? if (!oldAuxData.getArgCcPars(ccc.getValue()).contains(edgeAdjacentToNode.getKey())) { @@ -606,10 +621,13 @@ void reportAllArrayEqualitiesFromWeqGraph() { final Entry aeq = mWeakEquivalenceGraph.pollArrayEquality(); reportEquality(aeq.getKey(), aeq.getValue()); if (isInconsistent()) { + assert sanityCheck(); return; } + assert sanityCheck(); } assert weqGraphFreeOfArrayEqualities(); + assert sanityCheck(); } @Override @@ -638,6 +656,11 @@ protected boolean reportDisequalityRec(final NODE node1, final NODE node2) { reportGpaChangeToWeqGraphAndPropagateArrayEqualities( (final CongruenceClosure cc) -> cc.reportDisequality(node1, node2)); + if (isInconsistent()) { + // omit sanity checks + return true; + } + assert weqGraphFreeOfArrayEqualities(); return true; } @@ -688,7 +711,8 @@ public boolean isStrongerThan(final CongruenceClosure other) { @Override protected void prepareForRemove(final boolean useWeqGpa) { if (useWeqGpa) { - mWeakEquivalenceGraph.meetEdgeLabelsWithWeqGpaBeforeRemove(new WeqCongruenceClosure<>(this)); +// mWeakEquivalenceGraph.meetEdgeLabelsWithWeqGpaBeforeRemove(new WeqCongruenceClosure<>(this)); + mWeakEquivalenceGraph.meetEdgeLabelsWithWeqGpaBeforeRemove(mFactory.getCcManager().makeCopy(this)); } else { mWeakEquivalenceGraph.meetEdgeLabelsWithCcGpaBeforeRemove(); } @@ -764,7 +788,7 @@ protected Set getNodesToIntroduceBeforeRemoval(final NODE elemToRemove, final NODE j = iToBeRemovedToo ? jEqualToI : elemToRemove.getArgument(); // forall b --Phi(q)-- a - for (final Entry.WeakEquivalenceEdgeLabel> edge + for (final Entry> edge : mWeakEquivalenceGraph.getAdjacentWeqEdges(elemToRemove.getAppliedFunction()).entrySet()) { assert !edge.getKey().equals(elemToRemove.getAppliedFunction()); if (elemToRemoveToReplacement.keySet().contains(edge.getKey())) { @@ -848,6 +872,10 @@ public boolean isConstrained(final NODE elem) { protected void registerNewElement(final NODE elem, final RemoveElement remInfo) { super.registerNewElement(elem, remInfo); + if (isInconsistent()) { + // nothing more to do + return; + } if (!elem.isFunctionApplication()) { @@ -941,7 +969,8 @@ public WeqCongruenceClosure join(final CongruenceClosure otherCC) { throw new IllegalArgumentException(); } if (otherCC.isInconsistent()) { - return new WeqCongruenceClosure<>(this); +// return new WeqCongruenceClosure<>(this); + return mFactory.getCcManager().makeCopy(this); } final WeqCongruenceClosure other = (WeqCongruenceClosure) otherCC; @@ -995,7 +1024,7 @@ public WeqCongruenceClosure meetRec(final CongruenceClosure other) { assert otherWeqCc.sanityCheck(); // report all weq edges from other - for (final Entry, WeakEquivalenceGraph.WeakEquivalenceEdgeLabel> edge + for (final Entry, WeakEquivalenceEdgeLabel> edge : otherWeqCc.mWeakEquivalenceGraph.getEdges().entrySet()) { // assert gPaMeet.getAllElements().containsAll(edge.getValue().getAppearingNodes()); diff --git a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java index 1c68602184b..71f1ed9b41c 100644 --- a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java +++ b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java @@ -426,6 +426,10 @@ protected void registerNewElement(final ELEM elem, final CongruenceClosure if (remInfo == null) { for (final Entry eq : equalitiesToPropagate.entrySet()) { reportEqualityRec(eq.getKey(), eq.getValue()); + if (isInconsistent()) { + // propagated equality made this Cc inconsistent (break or return here?) + break; + } } } else { // do nothing in this case, right?.. @@ -631,6 +635,12 @@ public void doRemoval() { // add proxy elements for (final ELEM proxyElem : nodesToAdd) { addElementRec(proxyElem); + + if (isInconsistent()) { + // Cc became inconsistent through adding proxyElem --> nothing more to do + return; + } + assert sanityCheck(); } diff --git a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/relation/AbstractRelation.java b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/relation/AbstractRelation.java index d17a3e53d9d..8b32aed5de4 100644 --- a/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/relation/AbstractRelation.java +++ b/trunk/source/Library-UltimateUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/relation/AbstractRelation.java @@ -276,6 +276,13 @@ public Iterator> iterator() { return new MapToCollectionIterator<>(mMap); } + /** + * Remove all entries from this relation. + */ + public void clear() { + mMap.clear(); + } + @Override public int hashCode() { final int prime = 31;