From 093a8c091187f74480a9df3bb8c0f996b9a38ead Mon Sep 17 00:00:00 2001 From: Alexander Nutz Date: Sun, 14 Oct 2018 15:50:50 +0200 Subject: [PATCH] #295, cleanup, revert slow setting for domain --- .../heapseparator/HeapPartitionManager.java | 18 ++-- .../heapseparator/SubArrayManager.java | 12 +-- ...tionBlock.java => StoreLocationBlock.java} | 38 +++---- .../PartitionProjectionTermTransformer.java | 98 ++++++------------- ...titionProjectionTransitionTransformer.java | 12 +-- .../absint/vpdomain/WeqSettings.java | 2 +- 6 files changed, 62 insertions(+), 118 deletions(-) rename trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/{LocationBlock.java => StoreLocationBlock.java} (73%) diff --git a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java index a741f771de5..e563d51b920 100644 --- a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java +++ b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java @@ -32,7 +32,7 @@ import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayGroup; -import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.LocationBlock; +import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreLocationBlock; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.NoStoreInfo; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.SelectInfo; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreInfo; @@ -50,7 +50,7 @@ public class HeapPartitionManager { // output - private final NestedMap2 mSelectInfoToDimensionToLocationBlock; + private final NestedMap2 mSelectInfoToDimensionToLocationBlock; private final NestedMap2> mArrayGroupToDimensionToStoreIndexInfoPartition; @@ -69,7 +69,7 @@ public class HeapPartitionManager { /** * map for caching/unifying LocationBlocks */ - private final NestedMap3, ArrayGroup, Integer, LocationBlock> + private final NestedMap3, ArrayGroup, Integer, StoreLocationBlock> mStoreIndexInfosToArrayGroupToDimensionToLocationBlock; private final HeapSeparatorBenchmark mStatistics; @@ -220,7 +220,7 @@ public void finish() { mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim); final Set eqc = partition.getEquivalenceClassMembers(sampleSii); - final LocationBlock locationBlock = getOrConstructLocationBlock(eqc, arrayGroup, dim); + final StoreLocationBlock locationBlock = getOrConstructLocationBlock(eqc, arrayGroup, dim); mSelectInfoToDimensionToLocationBlock.put(selectInfo, dim, locationBlock); mLogger.debug("adding LocationBlock " + locationBlock); mLogger.debug("\t at dimension " + dim + " for " + selectInfo); @@ -265,11 +265,11 @@ public void finish() { assert sanityCheck(); } - private LocationBlock getOrConstructLocationBlock(final Set eqc, final ArrayGroup arrayGroup, + private StoreLocationBlock getOrConstructLocationBlock(final Set eqc, final ArrayGroup arrayGroup, final Integer dim) { - LocationBlock result = mStoreIndexInfosToArrayGroupToDimensionToLocationBlock.get(eqc, arrayGroup, dim); + StoreLocationBlock result = mStoreIndexInfosToArrayGroupToDimensionToLocationBlock.get(eqc, arrayGroup, dim); if (result == null) { - result = new LocationBlock(eqc, arrayGroup, dim); + result = new StoreLocationBlock(eqc, arrayGroup, dim); mStoreIndexInfosToArrayGroupToDimensionToLocationBlock.put(eqc, arrayGroup, dim, result); mLogger.debug("creating LocationBlock " + result); @@ -285,14 +285,14 @@ private boolean sanityCheck() { return true; } - public NestedMap2 getSelectInfoToDimensionToLocationBlock() { + public NestedMap2 getSelectInfoToDimensionToLocationBlock() { if (!mIsFinished) { throw new AssertionError(); } return mSelectInfoToDimensionToLocationBlock; } - public LocationBlock getLocationBlock(final SelectInfo si, final Integer dim) { + public StoreLocationBlock getLocationBlock(final SelectInfo si, final Integer dim) { if (!mIsFinished) { throw new AssertionError(); } diff --git a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SubArrayManager.java b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SubArrayManager.java index 73438c82ba2..89c561d7238 100644 --- a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SubArrayManager.java +++ b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SubArrayManager.java @@ -32,7 +32,7 @@ import java.util.Set; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayGroup; -import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.LocationBlock; +import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreLocationBlock; import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; @@ -59,7 +59,7 @@ public class SubArrayManager { /** * used for caching the sub arrays that this class manages */ - private final NestedMap2, IProgramVarOrConst> + private final NestedMap2, IProgramVarOrConst> mArrayToLocationBlockListToSubArray; Set mAllSubArrays; @@ -91,7 +91,7 @@ public String toString() { return "NewArrayIdProvider";// + mArrayToPartitionInformation.toString(); } - public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final List projectList) { + public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final List projectList) { final ArrayGroup arrayGroup = mCsiag.getArrayGroupForArrayPvoc(programVar); assert Objects.nonNull(arrayGroup); if (projectList.size() != arrayGroup.getDimensionality()) { @@ -120,7 +120,7 @@ public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final * @return */ private IProgramVarOrConst constructFreshProgramVarsForIndexPartition(final IProgramVarOrConst arrayPv, - final List projectList) { + final List projectList) { IProgramVarOrConst freshVar = null; if (arrayPv instanceof LocalBoogieVar) { @@ -180,10 +180,10 @@ private IProgramVarOrConst constructFreshProgramVarsForIndexPartition(final IPro } } - private String constructIndexName(final List projectList) { + private String constructIndexName(final List projectList) { final StringBuilder sb = new StringBuilder(); String sep = ""; - for (final LocationBlock lb : projectList) { + for (final StoreLocationBlock lb : projectList) { sb.append(sep); sb.append(lb.toString()); sep = "_"; diff --git a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/LocationBlock.java b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/StoreLocationBlock.java similarity index 73% rename from trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/LocationBlock.java rename to trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/StoreLocationBlock.java index a4dc566bb17..c6acb440ad6 100644 --- a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/LocationBlock.java +++ b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/datastructures/StoreLocationBlock.java @@ -40,8 +40,7 @@ * @author Alexander Nutz (nutz@informatik.uni-freiburg.de) * */ -public class LocationBlock { -// Set mAssociatedArrayGroup; +public class StoreLocationBlock { /** * This LocationBlock considers writes only to arrays in mArrayGroup @@ -53,36 +52,25 @@ public class LocationBlock { */ private final int mDimension; - private final Set mStoreIndexInfos; + private final Set mStoreInfos; -// private final Set mArrayAccessDimensions; - - public LocationBlock(final Set eqc, final ArrayGroup associatedArrayGroup, final int dimension) { - mStoreIndexInfos = Collections.unmodifiableSet(eqc); + public StoreLocationBlock(final Set eqc, final ArrayGroup associatedArrayGroup, final int dimension) { + mStoreInfos = Collections.unmodifiableSet(eqc); mArrayGroup = associatedArrayGroup; mDimension = dimension; - -// mArrayAccessDimensions = new HashSet<>(); -// for (final StoreIndexInfo sii : eqc) { -// mArrayAccessDimensions.addAll(sii.getAccessDimensions()); -// } } public boolean contains(final StoreInfo sii) { - return mStoreIndexInfos.contains(sii); + return mStoreInfos.contains(sii); } -// public Set getAccessDimensions() { -// return Collections.unmodifiableSet(mArrayAccessDimensions); -// } - @Override public String toString() { - return "locs_" + (mStoreIndexInfos.hashCode() % 100); + return "locs_" + (mStoreInfos.hashCode() % 100); } public Set getLocations() { - return mStoreIndexInfos; + return mStoreInfos; } public ArrayGroup getArrayGroup() { @@ -99,7 +87,7 @@ public int hashCode() { int result = 1; result = prime * result + ((mArrayGroup == null) ? 0 : mArrayGroup.hashCode()); result = prime * result + mDimension; - result = prime * result + ((mStoreIndexInfos == null) ? 0 : mStoreIndexInfos.hashCode()); + result = prime * result + ((mStoreInfos == null) ? 0 : mStoreInfos.hashCode()); return result; } @@ -114,7 +102,7 @@ public boolean equals(final Object obj) { if (getClass() != obj.getClass()) { return false; } - final LocationBlock other = (LocationBlock) obj; + final StoreLocationBlock other = (StoreLocationBlock) obj; if (mArrayGroup == null) { if (other.mArrayGroup != null) { return false; @@ -125,15 +113,13 @@ public boolean equals(final Object obj) { if (mDimension != other.mDimension) { return false; } - if (mStoreIndexInfos == null) { - if (other.mStoreIndexInfos != null) { + if (mStoreInfos == null) { + if (other.mStoreInfos != null) { return false; } - } else if (!mStoreIndexInfos.equals(other.mStoreIndexInfos)) { + } else if (!mStoreInfos.equals(other.mStoreInfos)) { return false; } return true; } - - } diff --git a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTermTransformer.java b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTermTransformer.java index f394221325d..5fcbee2a6c6 100644 --- a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTermTransformer.java +++ b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTermTransformer.java @@ -45,7 +45,7 @@ import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayCellAccess; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayGroup; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.EdgeInfo; -import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.LocationBlock; +import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreLocationBlock; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreInfo; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.SubtreePosition; import de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm; @@ -81,7 +81,7 @@ public class PartitionProjectionTermTransformer extends PositionAwareTermTransfo /** * keeps track of the LocationBlocks that guide the projection in each scope. */ - private final Stack> mProjectLists; + private final Stack> mProjectLists; private final ManagedScript mMgdScript; @@ -94,12 +94,12 @@ public class PartitionProjectionTermTransformer extends PositionAwareTermTransfo *

* Note: this may be null if the edge has no selects to a heap array */ - private final NestedMap2 mArrayCellAccessToIntegerToLocationBlock; + private final NestedMap2 mArrayCellAccessToIntegerToLocationBlock; /** * All the location blocks that belong to one array group, divided by dimension they belong to.. */ - private final HashRelation3 mArrayGroupToDimensionToLocationBlocks; + private final HashRelation3 mArrayGroupToDimensionToLocationBlocks; private final SubArrayManager mSubArrayManager; @@ -152,19 +152,16 @@ public class PartitionProjectionTermTransformer extends PositionAwareTermTransfo */ public PartitionProjectionTermTransformer(final ILogger logger, final ManagedScript mgdScript, final SubArrayManager subArrayManager, - final NestedMap2 arrayCellAccessToDimensionToLocationBlock, + final NestedMap2 arrayCellAccessToDimensionToLocationBlock, final EdgeInfo edgeInfo, - final HashRelation3 arrayGroupToDimensionToLocationBlocks, + final HashRelation3 arrayGroupToDimensionToLocationBlocks, final ComputeStoreInfosAndArrayGroups csiag, -// final Map arrayToArrayGroup, -// final NestedMap2 edgeToIndexToStoreIndexInfo, final List heapArrays) { mLogger = Objects.requireNonNull(logger); mMgdScript = Objects.requireNonNull(mgdScript); mSubArrayManager = Objects.requireNonNull(subArrayManager); mHeapArrays = Objects.requireNonNull(heapArrays); -// mArrayToArrayGroup = Objects.requireNonNull(arrayToArrayGroup); mCsiag = csiag; @@ -176,8 +173,6 @@ public PartitionProjectionTermTransformer(final ILogger logger, final ManagedScr mArrayGroupToDimensionToLocationBlocks = arrayGroupToDimensionToLocationBlocks; -// mEdgeToIndexToStoreIndexInfo = edgeToIndexToStoreIndexInfo; - mEdgeInfo = edgeInfo; mNewInVars = new HashMap<>(); @@ -197,7 +192,7 @@ public PartitionProjectionTermTransformer(final ILogger logger, final ManagedScr @Override protected void convert(final Term term, final SubtreePosition pos) { assert mProjectLists.stream().allMatch(l -> l.stream().allMatch(Objects::nonNull)); - final List projectList = mProjectLists.peek(); + final List projectList = mProjectLists.peek(); if (term instanceof ConstantTerm || term instanceof TermVariable) { final IProgramVar invar = mEdgeInfo.getInVar(term); @@ -229,12 +224,9 @@ protected void convert(final Term term, final SubtreePosition pos) { final Term lhs = at.getParameters()[0]; final Term rhs = at.getParameters()[1]; -// final IProgramVarOrConst lhsPvoc = mEdgeInfo.getProgramVarOrConstForTerm(extractSimpleArrayTerm(lhs)); -// final IProgramVarOrConst rhsPvoc = mEdgeInfo.getProgramVarOrConstForTerm(extractSimpleArrayTerm(rhs)); final Term lhsBaseArray = extractSimpleArrayTerm(lhs); final Term rhsBaseArray = extractSimpleArrayTerm(rhs); -// if (!mHeapArrays.contains(lhsPvoc) && !mHeapArrays.contains(rhsPvoc)) { if (!mCsiag.isArrayTermSubjectToSeparation(mEdgeInfo, lhsBaseArray)) { assert !mCsiag.isArrayTermSubjectToSeparation(mEdgeInfo, rhsBaseArray); super.convert(term, pos); @@ -242,19 +234,15 @@ protected void convert(final Term term, final SubtreePosition pos) { } assert mCsiag.isArrayTermSubjectToSeparation(mEdgeInfo, rhsBaseArray); -// final IProgramVarOrConst lhsArray = mEdgeInfo.getProgramVarOrConstForTerm(extractSimpleArrayTerm(lhs)); -// final ArrayGroup arrayGroup = mArrayToArrayGroup.get(lhsArray); final ArrayGroup arrayGroup = mCsiag.getArrayGroupForTermInEdge(mEdgeInfo, lhsBaseArray); -// assert arrayGroup.equals(getArrayGroup(extractSimpleArrayTerm(rhs))); // holds the combinations of L1i .. Lni we will build a conjunct for each - final List> locationBlockTuples = -// getAllLocationBlockTuplesForHeapArray(lhsArray); + final List> locationBlockTuples = getAllLocationBlockTuplesForHeapArray(arrayGroup); enqueueWalker(new BuildConjunction(locationBlockTuples.size(), mMgdScript.getScript())); - for (final List lbt : locationBlockTuples) { + for (final List lbt : locationBlockTuples) { enqueueWalker(new EndScope()); enqueueWalker(new BuildApplicationTerm((ApplicationTerm) term, pos)); @@ -289,13 +277,13 @@ protected void convert(final Term term, final SubtreePosition pos) { enqueueWalker(new BeginScope(Collections.emptyList())); // construct a list of location blocks according to the indices - final List locationBlockList = new ArrayList<>(); + final List locationBlockList = new ArrayList<>(); for (int dim = 1; dim <= aca.getIndex().size(); dim++) { /* * TODO: indeed for this field it might be nicer to use Map> * instead of a NestedMap2... */ - final LocationBlock locationBlock = mArrayCellAccessToIntegerToLocationBlock.get(aca, dim); + final StoreLocationBlock locationBlock = mArrayCellAccessToIntegerToLocationBlock.get(aca, dim); assert locationBlock != null; locationBlockList.add(locationBlock); } @@ -317,7 +305,6 @@ protected void convert(final Term term, final SubtreePosition pos) { } assert projectList.size() > 0 : "(IndexOutOfBoundsExceptions are hard to catch somehow.."; -// if (fallsInto(indexSubterm, projectList.get(0))) { if (fallsInto(pos, term, projectList.get(0))) { // i in L1 --> keep the store @@ -368,39 +355,20 @@ protected void convert(final Term term, final SubtreePosition pos) { // no extra scoping needed, right? enqueueWalker(new BuildApplicationTerm((ApplicationTerm) term, pos)); pushTerms(((ApplicationTerm) term).getParameters(), pos); -// pushNLocationBlockLists(at.getParameters().length, Collections.emptyList()); } } else if (term instanceof LetTerm) { -// enqueueWalker(new StartLetTerm((LetTerm) term, pos)); -// pushTerms(((LetTerm) term).getValues(), pos); super.convert(term, pos); } else if (term instanceof QuantifiedFormula) { -// enqueueWalker(new BuildQuantifier((QuantifiedFormula) term, pos)); -// pushTerm(((QuantifiedFormula) term).getSubformula(), pos.append(0)); -// beginScope(); super.convert(term, pos); } else if (term instanceof AnnotatedTerm) { -// final AnnotatedTerm annterm = (AnnotatedTerm) term; -// enqueueWalker(new BuildAnnotation(annterm, pos)); -// final Annotation[] annots = annterm.getAnnotations(); -// for (int i = annots.length - 1; i >= 0; i--) { -// final Object value = annots[i].getValue(); -// if (value instanceof Term) { -// pushTerm((Term) value); -// } else if (value instanceof Term[]) { -// pushTerms((Term[]) value); -// } -// } -// pushTerm(annterm.getSubterm()); -// return; super.convert(term, pos); } else { throw new AssertionError("Unknown Term: " + term.toStringDirect()); } } - private List append(final List locationBlockList, final List projectList) { - final List result = new ArrayList<>(); + private List append(final List locationBlockList, final List projectList) { + final List result = new ArrayList<>(); result.addAll(locationBlockList); result.addAll(projectList); assert assertIsSortedByDimensions(result); @@ -426,7 +394,7 @@ private Term extractSimpleArrayTerm(final Term term) { return currentTerm; } - private Term getSubArrayReplacementTerm(final Term originalTerm, final List projectList) { + private Term getSubArrayReplacementTerm(final Term originalTerm, final List projectList) { final IProgramVarOrConst originalTermPvoc = mEdgeInfo.getProgramVarOrConstForTerm(originalTerm); @@ -475,7 +443,6 @@ private boolean isPartitionedArray(final Term term) { return false; } // the given array term is not in an array group with one of the heap arrays -// if (!mArrayToArrayGroup.containsKey(mEdgeInfo.getProgramVarOrConstForTerm(term))) { if (!mCsiag.isArrayTermSubjectToSeparation(mEdgeInfo, term)) { // the given array term is not in an array group with one of the heap arrays return false; @@ -490,19 +457,14 @@ private boolean isPartitionedArray(final Term term) { * @param arrayGroup * @return */ - private List> getLocationBlocksForArrayGroup(final ArrayGroup arrayGroup) { - final List> result = new ArrayList<>(); + private List> getLocationBlocksForArrayGroup(final ArrayGroup arrayGroup) { + final List> result = new ArrayList<>(); for (int dim = 1; dim <= arrayGroup.getDimensionality(); dim++) { result.add(mArrayGroupToDimensionToLocationBlocks.projectToTrd(arrayGroup, dim)); } return result; } -// private ArrayGroup getArrayGroup(final Term term) { -// assert isPartitionedArray(term); -// return mArrayToArrayGroup.get(mEdgeInfo.getProgramVarOrConstForTerm(term)); -// } - private static List addToFront(final E locationBlockForIndex, final List projectList) { final List newList = new ArrayList<>(); newList.add(locationBlockForIndex); @@ -523,15 +485,14 @@ private static List dropFirst(final List projectList) { * @param locationBlock * @return */ - private boolean fallsInto(final SubtreePosition pos, final Term storeTerm, final LocationBlock locationBlock) { + private boolean fallsInto(final SubtreePosition pos, final Term storeTerm, final StoreLocationBlock locationBlock) { // look up the StoreIndexInfo for the given term and mEdgeInfo assert SmtUtils.isFunctionApplication(storeTerm, "store"); -//mEdgeToIndexToStoreIndexInfo.get(mEdgeInfo, indexSubterm); final StoreInfo sii = mCsiag.getStoreInfoForStoreTermAtPositionInEdge(mEdgeInfo, pos); return locationBlock.contains(sii); } - private void pushLocationBlockList(final List newList) { + private void pushLocationBlockList(final List newList) { assert Objects.nonNull(newList); assert newList.stream().allMatch(Objects::nonNull); mProjectLists.push(Collections.unmodifiableList(newList)); @@ -603,7 +564,7 @@ public String toString() { } } - static boolean assertIsSortedByDimensions(final List list) { + static boolean assertIsSortedByDimensions(final List list) { return isSorted(list.stream().map(lb -> lb.getDimension()).collect(Collectors.toList())); } @@ -611,9 +572,9 @@ static boolean assertIsSortedByDimensions(final List list) { protected static class BeginScope implements Walker { - private final List mLocBlockList; + private final List mLocBlockList; - public BeginScope(final List locBlockList) { + public BeginScope(final List locBlockList) { assert Objects.nonNull(locBlockList); assert locBlockList.stream().allMatch(Objects::nonNull); assert assertIsSortedByDimensions(locBlockList); @@ -693,10 +654,10 @@ public void finish() { /* heap array invar whose termvariable does not occur in the formula * --> add invar entries for all subarrays (with fresh Termvars) */ - final List> locationBlockTuples = + final List> locationBlockTuples = // getAllLocationBlockTuplesForHeapArray(en.getKey()); getAllLocationBlockTuplesForHeapArray(mCsiag.getArrayGroupForArrayPvoc(en.getKey())); - for (final List lbt : locationBlockTuples) { + for (final List lbt : locationBlockTuples) { final IProgramVar subarray = (IProgramVar) mSubArrayManager.getSubArray(en.getKey(), lbt); final TermVariable freshTv = mMgdScript.constructFreshCopy(subarray.getTermVariable()); assert !mNewInVars.containsKey(subarray); @@ -712,10 +673,9 @@ public void finish() { /* heap array outvar whose termvariable does not occur in the formula * --> add invar entries for all subarrays (with fresh Termvars) */ - final List> locationBlockTuples = -// getAllLocationBlockTuplesForHeapArray(en.getKey()); + final List> locationBlockTuples = getAllLocationBlockTuplesForHeapArray(mCsiag.getArrayGroupForArrayPvoc(en.getKey())); - for (final List lbt : locationBlockTuples) { + for (final List lbt : locationBlockTuples) { final IProgramVar subarray = (IProgramVar) mSubArrayManager.getSubArray(en.getKey(), lbt); final TermVariable freshTv = mMgdScript.constructFreshCopy(subarray.getTermVariable()); assert !mNewOutVars.containsKey(subarray); @@ -738,13 +698,11 @@ public void finish() { mIsFinished = true; } -// private List> getAllLocationBlockTuplesForHeapArray(final IProgramVarOrConst array) { - private List> getAllLocationBlockTuplesForHeapArray(final ArrayGroup arrayGroup) { -// final ArrayGroup arrayGroup = mArrayToArrayGroup.get(array); + private List> getAllLocationBlockTuplesForHeapArray(final ArrayGroup arrayGroup) { assert arrayGroup != null && !DataStructureUtils.intersection(new HashSet<>(mHeapArrays), arrayGroup.getArrays()).isEmpty(); - final List> locationBlocks = getLocationBlocksForArrayGroup(arrayGroup); - final List> locationBlockTuples = CrossProducts.crossProductOfSets(locationBlocks); + final List> locationBlocks = getLocationBlocksForArrayGroup(arrayGroup); + final List> locationBlockTuples = CrossProducts.crossProductOfSets(locationBlocks); return locationBlockTuples; } diff --git a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTransitionTransformer.java b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTransitionTransformer.java index 15531ba1b81..b3a17ed5817 100644 --- a/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTransitionTransformer.java +++ b/trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/transformers/PartitionProjectionTransitionTransformer.java @@ -41,7 +41,7 @@ import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayCellAccess; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.ArrayGroup; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.EdgeInfo; -import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.LocationBlock; +import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.StoreLocationBlock; import de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator.datastructures.SelectInfo; import de.uni_freiburg.informatik.ultimate.logic.Term; import de.uni_freiburg.informatik.ultimate.logic.TermVariable; @@ -83,7 +83,7 @@ public class PartitionProjectionTransitionTransformer mArrayGroupToDimensionToLocationBlocks; + private final HashRelation3 mArrayGroupToDimensionToLocationBlocks; // private final NestedMap2 mEdgeToIndexToStoreIndexInfo; // private final Map mArrayToArrayGroup; @@ -93,7 +93,7 @@ public class PartitionProjectionTransitionTransformer + private final NestedMap3 mEdgeInfoToArrayCellAccessToDimensionToLocationBlock; private final List mHeapArrays; @@ -130,7 +130,7 @@ public class PartitionProjectionTransitionTransformer selectInfoToDimensionToLocationBlock, + final NestedMap2 selectInfoToDimensionToLocationBlock, // final NestedMap2 edgeToIndexToStoreIndexInfo, // final Map arrayToArrayGroup, final ComputeStoreInfosAndArrayGroups csiag, @@ -158,7 +158,7 @@ public PartitionProjectionTransitionTransformer(final ILogger logger, */ mEdgeInfoToArrayCellAccessToDimensionToLocationBlock = new NestedMap3<>(); mArrayGroupToDimensionToLocationBlocks = new HashRelation3<>(); - for (final Triple triple + for (final Triple triple : selectInfoToDimensionToLocationBlock.entrySet()) { mEdgeInfoToArrayCellAccessToDimensionToLocationBlock.put(triple.getFirst().getEdgeInfo(), triple.getFirst().getArrayCellAccess(), triple.getSecond(), triple.getThird()); @@ -188,7 +188,7 @@ public TransformulaTransformationResult transform(final IIcfgTransition arrayCellAccessToDimensionToLocationBlock = + final NestedMap2 arrayCellAccessToDimensionToLocationBlock = mEdgeInfoToArrayCellAccessToDimensionToLocationBlock.get(edgeInfo); final Term transformedFormula; diff --git a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqSettings.java b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqSettings.java index f2756294b7d..f83b4716899 100644 --- a/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqSettings.java +++ b/trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/WeqSettings.java @@ -74,7 +74,7 @@ public class WeqSettings { /** * See {@link #closeAfterInplaceMeet()}. */ - private final boolean mCloseAfterInplaceMeet = !false; + private final boolean mCloseAfterInplaceMeet = false; private final boolean mCloseBeforeIsInconsistentCheck = false;