Skip to content

Commit

Permalink
#239, cleanup, remove some functionality that is not needed
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexandernutz
alexandernutz committed Oct 9, 2017
1 parent dc822cb commit 1bb1c24
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 88 deletions.
22 changes: 0 additions & 22 deletions ...ate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/elements/EqNode.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,33 +98,11 @@ public Collection<EqNode> getSupportingNodes() {
throw new UnsupportedOperationException("check isDependent first");
}

// @Override
// public Collection<EqFunction> getSupportingFunctions() {
// // this is the default case NonAtomicBaseNode must override this
// throw new UnsupportedOperationException("check isDependent first");
// }



// @Override
// public String getFunctionName() {
// assert isFunction();
//// assert false : "what's the right string here?";
//// return mPvoc.toString();
// return mTerm.toString();
// }

@Override
public boolean isFunction() {
return mMdSort != null;
}

// @Override
// public int getArity() {
// assert isFunction();
// return mMdSort.getDimension();
// }

@Override
public String toString() {
return mTerm.toString();
Expand Down
12 changes: 3 additions & 9 deletions ...analysis/abstractinterpretationv2/domain/transformula/vp/states/WeakEquivalenceGraph.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1256,7 +1256,6 @@ public Set<NODE> projectElement(final NODE elem,// final NODE newRep,
return Collections.emptySet();
}
final CongruenceClosure<NODE> meet = mCcManager.getMeet(mLabel.get(i), groundPartialArrangement);
// final CongruenceClosure<NODE> meet = mCcManager.getMeet(mLabel.get(i), mPartialArrangement);
if (meet.isInconsistent()) {
/* label element is inconsistent with the current gpa
* --> omit it from the new label
Expand Down Expand Up @@ -1289,27 +1288,22 @@ public Set<NODE> projectElement(final NODE elem,// final NODE newRep,
* <li> and projectToElements would keep both blocks
*
* EDIT: actually, a fix to projectToElements, removes the necessity for
* removeSimpleElementWithReplacementPreference at this place (--> we keep the constraint
* "removeSimpleElementWithReplacementPreference" at this place (--> we keep the constraint
* {a[j] = i} by detecting that j = q)
*/
// meet.removeSimpleElementWithReplacementPreference(elem, mFactory.getAllWeqNodes());
meet.removeSimpleElement(elem);
// meet.transformElementsAndFunctions(node -> node.replaceSubNode(replacer, replacee));

/*
* the removeSimpleElement may have added elements (function applications) to meet that are not in
* the removeSimpleElement may have added elements (function applications) to meet that are not
* known to mPartialArrangement --> collect them here and add them later
*/
// result.addAll(DataStructureUtils.difference(meet.getAllElements(),
// DataStructureUtils.union(groundPartialArrangement.getAllElements(),
// mFactory.getAllWeqNodes())));
// TODO: seems hacky..
final Stream<NODE> nodeToAddToGpa = meet.getAllElements().stream().filter(e ->
!groundPartialArrangement.getAllElements().contains(e)
&& !CongruenceClosure.dependsOnAny(e, mFactory.getAllWeqNodes())
&& (mPartialArrangement.getElementCurrentlyBeingRemoved() == null ||
!CongruenceClosure.dependsOnAny(e, Collections.singleton(
mPartialArrangement.getElementCurrentlyBeingRemoved().getElem()))));
// Collections.singleton(e)));
nodeToAddToGpa.forEach(result::add);
assert result.stream().allMatch(n -> n.isFunctionApplication()) : "cannot think of another case "
+ "right now..";
Expand Down
32 changes: 16 additions & 16 deletions ...analysis/abstractinterpretationv2/domain/transformula/vp/states/WeqCongruenceClosure.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,21 +180,21 @@ public boolean addElement(final NODE elem) {
return result;
}

@Override
protected boolean addElementRec(final NODE elem) {
assert !mFactory.getAllWeqNodes().contains(elem);

final boolean elemIsNew = super.addElementRec(elem);
if (!elemIsNew) {
return false;
}

// executeFloydWarshallAndReportResult();
// reportAllArrayEqualitiesFromWeqGraph();

// assert weqGraphFreeOfArrayEqualities();
return true;
}
// @Override
// protected boolean addElementRec(final NODE elem) {
// assert !mFactory.getAllWeqNodes().contains(elem);
//
// final boolean elemIsNew = super.addElementRec(elem);
// if (!elemIsNew) {
// return false;
// }
//
//// executeFloydWarshallAndReportResult();
//// reportAllArrayEqualitiesFromWeqGraph();
//
//// assert weqGraphFreeOfArrayEqualities();
// return true;
// }

@Override
protected CongruenceClosure<NODE> alignElementsAndFunctions(final CongruenceClosure<NODE> otherCC) {
Expand Down Expand Up @@ -773,7 +773,7 @@ public boolean removeSimpleElement(final NODE elem) {


if (mElementCurrentlyBeingRemoved == null) {
mElementCurrentlyBeingRemoved = new RemovalInfo(elem, getOtherEquivalenceClassMember(elem, null));
mElementCurrentlyBeingRemoved = new RemovalInfo(elem, getOtherEquivalenceClassMember(elem));
} else {
// this may happen if elem is a dependent element, check that through the assert..
assert mNodeToDependents.entrySet().stream()
Expand Down
70 changes: 29 additions & 41 deletions ...teUtil/src/de/uni_freiburg/informatik/ultimate/util/datastructures/CongruenceClosure.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Optional;
import java.util.Set;
import java.util.function.Function;
import java.util.stream.Collectors;
Expand Down Expand Up @@ -372,38 +371,27 @@ public ELEM getRepresentativeElement(final ELEM elem) {

}

/**
* Remove a simple element, i.e., an element that is not a function application.
*
* @param elem
* @return
*/
public boolean removeSimpleElement(final ELEM elem) {
return removeSimpleElementWithReplacementPreference(elem, null);
}
// /**
// * Remove a simple element, i.e., an element that is not a function application.
// *
// * @param elem
// * @return
// */
// public boolean removeSimpleElement(final ELEM elem) {
// return removeSimpleElementWithReplacementPreference(elem, null);
// }

/**
* Remove a simple element, i.e., an element that is not a function application.
*
* During removal, CongruenceClosure attempts to add nodes in order to retain constraints that follow from the
* constraint but were not explicit before.
* The second parameter allows to give a set of preferred nodes to be chosen for this purpose if possible.
* Example:
* <li> state before this method call: {i, j, q} {a[i], x}
* <li> call this method with elem = i
* <li> we will have to remove a[i], too, thus the second partition block would be removed, thus without adding
* nodes we would arrive at {j, q}
* <li> if we introduce a[j] (or a[q]) before removing a[i], we still have a[j] = x (a[q] = x), the result would be
* {j, q}{a[j]=x}
* <li> giving q as a preferred replacement would enforce that we choose a[q] for this purpose, the result would be
* {j, q}{a[q]=x}
*
* @param elem
* @param preferredReplacements
* @return
*/
public boolean removeSimpleElementWithReplacementPreference(final ELEM elem, final Set<ELEM> preferredReplacements) {
// TODO Auto-generated method stub
public boolean removeSimpleElement(final ELEM elem) {
if (elem.isFunctionApplication()) {
throw new IllegalArgumentException();
}
Expand All @@ -418,10 +406,10 @@ public boolean removeSimpleElementWithReplacementPreference(final ELEM elem, fin
if (this.getClass().equals(CongruenceClosure.class)) {
assert mElementCurrentlyBeingRemoved == null;
mElementCurrentlyBeingRemoved = new RemovalInfo(elem,
getOtherEquivalenceClassMember(elem, preferredReplacements));
getOtherEquivalenceClassMember(elem));
}

final boolean result = removeAnyElement(elem, null, preferredReplacements);
final boolean result = removeAnyElement(elem, null);

if (this.getClass().equals(CongruenceClosure.class)) {
mElementCurrentlyBeingRemoved = null;
Expand All @@ -444,11 +432,11 @@ protected final Map<ELEM, ELEM> removeSimpleElementTrackNewReps(final ELEM elem)
// TODO: seems ugly
if (this.getClass().equals(CongruenceClosure.class)) {
assert mElementCurrentlyBeingRemoved == null;
mElementCurrentlyBeingRemoved = new RemovalInfo(elem, getOtherEquivalenceClassMember(elem, null));
mElementCurrentlyBeingRemoved = new RemovalInfo(elem, getOtherEquivalenceClassMember(elem));
}

final HashMap<ELEM, ELEM> removedElemToNewRep = new HashMap<>();
removeAnyElement(elem, removedElemToNewRep, null);
removeAnyElement(elem, removedElemToNewRep);

if (this.getClass().equals(CongruenceClosure.class)) {
mElementCurrentlyBeingRemoved = null;
Expand All @@ -464,13 +452,12 @@ protected final Map<ELEM, ELEM> removeSimpleElementTrackNewReps(final ELEM elem)
* @param allWeqNodes
* @return
*/
private boolean removeAnyElement(final ELEM elem, final Map<ELEM, ELEM> removedElemToNewRep,
final Set<ELEM> preferredReplacements) {
private boolean removeAnyElement(final ELEM elem, final Map<ELEM, ELEM> removedElemToNewRep) {
if (!hasElement(elem)) {
return false;
}

addNodesEquivalentToNodesWithRemovedElement(elem, preferredReplacements);
addNodesEquivalentToNodesWithRemovedElement(elem);
// assert sanityCheckOnlyCc();

final Collection<ELEM> oldAfParents = new ArrayList<>(mFaAuxData.getAfParents(elem));
Expand All @@ -486,10 +473,11 @@ private boolean removeAnyElement(final ELEM elem, final Map<ELEM, ELEM> removedE
// assert sanityCheckOnlyCc();

for (final ELEM parent : oldAfParents) {
removeAnyElement(parent, removedElemToNewRep, preferredReplacements);
removeAnyElement(parent, removedElemToNewRep);
}
assert elementIsFullyRemovedOnlyCc(elem);
for (final ELEM parent : oldArgParents) {
removeAnyElement(parent, removedElemToNewRep, preferredReplacements);
removeAnyElement(parent, removedElemToNewRep);
}
// removeParents(oldAfParents, oldArgParents);

Expand Down Expand Up @@ -622,8 +610,8 @@ protected ELEM updateElementTverAndAuxDataOnRemoveElement(final ELEM elem) {
* @param elem the element we are about to remove
* @param preferredReplacements
*/
protected void addNodesEquivalentToNodesWithRemovedElement(final ELEM elem, final Set<ELEM> preferredReplacements) {
final ELEM otherRep = getOtherEquivalenceClassMember(elem, preferredReplacements);
protected void addNodesEquivalentToNodesWithRemovedElement(final ELEM elem) {
final ELEM otherRep = getOtherEquivalenceClassMember(elem);
if (otherRep != null) {
for (final ELEM parent : new ArrayList<>(mFaAuxData.getAfParents(elem))) {
assert parent.getAppliedFunction() == elem;
Expand All @@ -648,19 +636,19 @@ protected void addNodesEquivalentToNodesWithRemovedElement(final ELEM elem, fina
* @param preferredReplacements
* @return
*/
protected ELEM getOtherEquivalenceClassMember(final ELEM elem, final Set<ELEM> preferredReplacements) {
protected ELEM getOtherEquivalenceClassMember(final ELEM elem) {
assert hasElement(elem);
final Set<ELEM> eqc = mElementTVER.getEquivalenceClass(elem);
if (eqc.size() == 1) {
return null;
}
if (preferredReplacements != null) {
final Optional<ELEM> preferred = eqc.stream()
.filter(e -> !e.equals(elem) && preferredReplacements.contains(e)).findFirst();
if (preferred.isPresent()) {
return preferred.get();
}
}
// if (preferredReplacements != null) {
// final Optional<ELEM> preferred = eqc.stream()
// .filter(e -> !e.equals(elem) && preferredReplacements.contains(e)).findFirst();
// if (preferred.isPresent()) {
// return preferred.get();
// }
// }
return eqc.stream().filter(e -> !e.equals(elem)).findFirst().get();
// return eqc.stream().filter(e -> e != elem).findAny().get();
}
Expand Down

0 comments on commit 1bb1c24

Please sign in to comment.