Skip to content

Commit

Permalink
#295, cleanup, revert slow setting for domain
Browse files Browse the repository at this point in the history
  • Loading branch information
@alexandernutz
alexandernutz committed Oct 14, 2018
1 parent 0e494e3 commit 093a8c0
Show file tree
Hide file tree
Showing 6 changed files with 62 additions and 118 deletions.
18 changes: 9 additions & 9 deletions .../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapPartitionManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -50,7 +50,7 @@
public class HeapPartitionManager {

// output
private final NestedMap2<SelectInfo, Integer, LocationBlock> mSelectInfoToDimensionToLocationBlock;
private final NestedMap2<SelectInfo, Integer, StoreLocationBlock> mSelectInfoToDimensionToLocationBlock;

private final NestedMap2<ArrayGroup, Integer, UnionFind<StoreInfo>>
mArrayGroupToDimensionToStoreIndexInfoPartition;
Expand All @@ -69,7 +69,7 @@ public class HeapPartitionManager {
/**
* map for caching/unifying LocationBlocks
*/
private final NestedMap3<Set<StoreInfo>, ArrayGroup, Integer, LocationBlock>
private final NestedMap3<Set<StoreInfo>, ArrayGroup, Integer, StoreLocationBlock>
mStoreIndexInfosToArrayGroupToDimensionToLocationBlock;

private final HeapSeparatorBenchmark mStatistics;
Expand Down Expand Up @@ -220,7 +220,7 @@ public void finish() {
mArrayGroupToDimensionToStoreIndexInfoPartition.get(arrayGroup, dim);
final Set<StoreInfo> 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);
Expand Down Expand Up @@ -265,11 +265,11 @@ public void finish() {
assert sanityCheck();
}

private LocationBlock getOrConstructLocationBlock(final Set<StoreInfo> eqc, final ArrayGroup arrayGroup,
private StoreLocationBlock getOrConstructLocationBlock(final Set<StoreInfo> 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);
Expand All @@ -285,14 +285,14 @@ private boolean sanityCheck() {
return true;
}

public NestedMap2<SelectInfo, Integer, LocationBlock> getSelectInfoToDimensionToLocationBlock() {
public NestedMap2<SelectInfo, Integer, StoreLocationBlock> 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();
}
Expand Down
12 changes: 6 additions & 6 deletions ...rc/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/SubArrayManager.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -59,7 +59,7 @@ public class SubArrayManager {
/**
* used for caching the sub arrays that this class manages
*/
private final NestedMap2<IProgramVarOrConst, List<LocationBlock>, IProgramVarOrConst>
private final NestedMap2<IProgramVarOrConst, List<StoreLocationBlock>, IProgramVarOrConst>
mArrayToLocationBlockListToSubArray;

Set<IProgramVarOrConst> mAllSubArrays;
Expand Down Expand Up @@ -91,7 +91,7 @@ public String toString() {
return "NewArrayIdProvider";// + mArrayToPartitionInformation.toString();
}

public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final List<LocationBlock> projectList) {
public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final List<StoreLocationBlock> projectList) {
final ArrayGroup arrayGroup = mCsiag.getArrayGroupForArrayPvoc(programVar);
assert Objects.nonNull(arrayGroup);
if (projectList.size() != arrayGroup.getDimensionality()) {
Expand Down Expand Up @@ -120,7 +120,7 @@ public IProgramVarOrConst getSubArray(final IProgramVarOrConst programVar, final
* @return
*/
private IProgramVarOrConst constructFreshProgramVarsForIndexPartition(final IProgramVarOrConst arrayPv,
final List<LocationBlock> projectList) {
final List<StoreLocationBlock> projectList) {

IProgramVarOrConst freshVar = null;
if (arrayPv instanceof LocalBoogieVar) {
Expand Down Expand Up @@ -180,10 +180,10 @@ private IProgramVarOrConst constructFreshProgramVarsForIndexPartition(final IPro
}
}

private String constructIndexName(final List<LocationBlock> projectList) {
private String constructIndexName(final List<StoreLocationBlock> 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 = "_";
Expand Down
38 changes: 12 additions & 26 deletions ...parator/datastructures/LocationBlock.java → ...or/datastructures/StoreLocationBlock.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,7 @@
* @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
*
*/
public class LocationBlock {
// Set<IProgramVarOrConst> mAssociatedArrayGroup;
public class StoreLocationBlock {

/**
* This LocationBlock considers writes only to arrays in mArrayGroup
Expand All @@ -53,36 +52,25 @@ public class LocationBlock {
*/
private final int mDimension;

private final Set<StoreInfo> mStoreIndexInfos;
private final Set<StoreInfo> mStoreInfos;

// private final Set<Integer> mArrayAccessDimensions;

public LocationBlock(final Set<StoreInfo> eqc, final ArrayGroup associatedArrayGroup, final int dimension) {
mStoreIndexInfos = Collections.unmodifiableSet(eqc);
public StoreLocationBlock(final Set<StoreInfo> 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<Integer> getAccessDimensions() {
// return Collections.unmodifiableSet(mArrayAccessDimensions);
// }

@Override
public String toString() {
return "locs_" + (mStoreIndexInfos.hashCode() % 100);
return "locs_" + (mStoreInfos.hashCode() % 100);
}

public Set<StoreInfo> getLocations() {
return mStoreIndexInfos;
return mStoreInfos;
}

public ArrayGroup getArrayGroup() {
Expand All @@ -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;
}

Expand All @@ -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;
Expand All @@ -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;
}


}
Loading

0 comments on commit 093a8c0

Please sign in to comment.