#295, reworking heap separator, intermediate commit

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayCellAccess.java

@@ -0,0 +1,59 @@
+package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
+
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.List;
+import java.util.Set;
+
+import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.ApplicationTermFinder;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArraySelect;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArraySelectOverStore;
+
+/**
+ * Union type of ArraySelect and ArraySelectOverStore.
+ *
+ * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
+ *
+ */
+public class ArrayCellAccess {
+
+	private final ArraySelect mArraySelect;
+	private final ArraySelectOverStore mArraySelectOverStore;
+
+	public ArrayCellAccess(final ArraySelect arraySelect) {
+		mArraySelect = arraySelect;
+		mArraySelectOverStore = null;
+	}
+
+	public ArrayCellAccess(final ArraySelectOverStore arraySelectOverStore) {
+		mArraySelect = null;
+		mArraySelectOverStore = arraySelectOverStore;
+	}
+
+	public static List<ArrayCellAccess> extractArrayCellAccesses(final Term formula) {
+		final List<ArrayCellAccess> result = new ArrayList<>();
+
+		final Set<String> functionSymbolNames = Collections.singleton("select");
+
+		final ApplicationTermFinder atf = new ApplicationTermFinder(functionSymbolNames, false);
+		for (final ApplicationTerm subterm : atf.findMatchingSubterms(formula)) {
+			final Term firstParam = subterm.getParameters()[0];
+			if (SmtUtils.isFunctionApplication(firstParam, "store")) {
+				result.add(new ArrayCellAccess(ArraySelectOverStore.convert(subterm)));
+			} else {
+				result.add(new ArrayCellAccess(ArraySelect.convert(subterm)));
+			}
+		}
+
+		return result;
+	}
+
+//	Term getTerm() {
+//		if (mArraySelect != null) {
+//			return SMT
+//		}
+//	}
+}

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/ArrayEqualityAllowStores.java

@@ -0,0 +1,134 @@
+package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
+import de.uni_freiburg.informatik.ultimate.logic.Script;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.ApplicationTermFinder;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayEquality;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayEquality.ArrayEqualityException;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayUpdate;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayUpdate.ArrayUpdateException;
+import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair;
+
+/**
+ * Union type for all ways of equating to Terms that have array type.
+ *
+ * Note: We assume that the only relation over array-type Terms is "=".
+ *
+ * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
+ *
+ */
+public class ArrayEqualityAllowStores {
+
+	ArrayUpdate mArrayUpdate;
+
+	ArrayEquality mArrayEquality;
+
+	boolean mOtherIsNegated;
+	Pair<Term, Term> mOther;
+
+	public ArrayEqualityAllowStores(final ArrayUpdate arrayUpdate) {
+		mArrayUpdate = arrayUpdate;
+		mArrayEquality = null;
+		mOtherIsNegated = false;
+		mOther = null;
+	}
+
+	public ArrayEqualityAllowStores(final ArrayEquality arrayEquality) {
+		mArrayUpdate = null;
+		mArrayEquality = arrayEquality;
+		mOtherIsNegated = false;
+		mOther = null;
+	}
+
+	public ArrayEqualityAllowStores(final Term lhs, final Term rhs, final boolean isNegated) {
+		mArrayUpdate = null;
+		mArrayEquality = null;
+		mOtherIsNegated = isNegated;
+		mOther = new Pair<>(lhs, rhs);
+	}
+
+	public Term getTerm(final Script script) {
+		if (mArrayUpdate != null) {
+			return mArrayUpdate.getArrayUpdateTerm();
+		}
+		if (mArrayEquality != null) {
+			return mArrayEquality.getOriginalTerm();
+		}
+		assert mOther != null;
+		Term result = SmtUtils.binaryEquality(script, mOther.getFirst(), mOther.getSecond());
+		if (mOtherIsNegated) {
+			result = SmtUtils.not(script, result);
+		}
+		return result;
+	}
+
+	public static List<ArrayEqualityAllowStores> extractArrayEqualityAllowStores(final Term formula) {
+		final HashSet<String> functionSymbolNames = new HashSet<>(3);
+		functionSymbolNames.add("=");
+		functionSymbolNames.add("distinct");
+		functionSymbolNames.add("not");
+
+		final List<ArrayEqualityAllowStores> result = new ArrayList<>();
+
+		final ApplicationTermFinder atf = new ApplicationTermFinder(functionSymbolNames, false);
+		for (final ApplicationTerm subterm : atf.findMatchingSubterms(formula)) {
+			ArrayEqualityAllowStores arrayRel = null;
+
+			final boolean isNegated = subterm.getFunction().getName().equals("not")
+					|| subterm.getFunction().getName().equals("distinct");
+
+			final Term lhs;
+			final Term rhs;
+			if (subterm.getFunction().getName().equals("not")) {
+				final Term notArg = subterm.getParameters()[0];
+				if (!(notArg instanceof ApplicationTerm)) {
+					continue;
+				}
+
+				final ApplicationTerm notArgAt = (ApplicationTerm) notArg;
+
+				if (!notArgAt.getFunction().getName().equals("=")) {
+					continue;
+				}
+				lhs = notArgAt.getParameters()[0];
+				rhs = notArgAt.getParameters()[1];
+
+				if (!lhs.getSort().isArraySort()) {
+					continue;
+				}
+			} else {
+				lhs = subterm.getParameters()[0];
+				rhs = subterm.getParameters()[1];
+				if (!lhs.getSort().isArraySort()) {
+					continue;
+				}
+			}
+
+			try {
+				arrayRel = new ArrayEqualityAllowStores(new ArrayUpdate(subterm, isNegated, false));
+				result.add(arrayRel);
+				continue;
+			} catch (final ArrayUpdateException e) {
+				// do nothing/fall through
+			}
+
+			try {
+				arrayRel = new ArrayEqualityAllowStores(new ArrayEquality(subterm, true, true));
+				result.add(arrayRel);
+				continue;
+			} catch (final ArrayEqualityException e) {
+				// do nothing/fall through
+			}
+
+			result.add(new ArrayEqualityAllowStores(lhs, rhs, isNegated));
+		}
+		return result;
+
+	}
+}

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java

@@ -104,7 +104,7 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		// TODO : where do we get this variable from?
 		final IProgramVar validArray = null;
 
-		final NestedMap2<Term, TfInfo, IProgramNonOldVar> writeIndexTermToTfInfoToFreezeVar;
+		final NestedMap2<Term, EdgeInfo, IProgramNonOldVar> writeIndexTermToTfInfoToFreezeVar;
 
 		/*
 		 * 1. Execute the preprocessing
@@ -161,13 +161,18 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		mEqualityProvider.preprocess(preprocessedIcfg);
 
 		/*
-		 * 3. compute an array partitioning
+		 * 3a. look up all locations where
+		 *  <li> an array cell is accessed
+		 *  <li> two arrays are related
 		 */
-
 		final HeapSepPreAnalysis heapSepPreanalysis = new HeapSepPreAnalysis(mLogger,
 				originalIcfg.getCfgSmtToolkit().getManagedScript());
 		new IcfgEdgeIterator(originalIcfg).forEachRemaining(edge -> heapSepPreanalysis.processEdge(edge));
 
+		/*
+		 * 3b. compute an array partitioning
+		 */
+
 		final NewArrayIdProvider newArrayIdProvider;
 		if (mPreprocessing == Preprocessing.FREEZE_VARIABLES) {
 			newArrayIdProvider = new NewArrayIdProvider(originalIcfg.getCfgSmtToolkit(),
@@ -181,22 +186,15 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		 *  Note that this transformation is done on the original input Icfg, not on the output of the
 		 *  ArrayIndexExposer, which we ran the equality analysis on.
 		 */
-//		final HeapSepTransFormulaTransformer hstftf = new HeapSepTransFormulaTransformer(csToolkit, services,
-//				equalityProvider);
-//
-//		hstftf.preprocessIcfg(originalIcfg);
 		final BasicIcfg<OUTLOC> resultIcfg =
 				new BasicIcfg<>(newIcfgIdentifier, originalIcfg.getCfgSmtToolkit(), outLocationClass);
-		final ITransformulaTransformer transformer = null;
+		final ITransformulaTransformer transformer = new HeapSepTransFormulaTransformer(originalIcfg.getCfgSmtToolkit(),
+				mLogger, newArrayIdProvider);
 		final TransformedIcfgBuilder<INLOC, OUTLOC> lst =
 				new TransformedIcfgBuilder<>(funLocFac, backtranslationTracker, transformer, originalIcfg, resultIcfg);
 		processLocations(originalIcfg.getInitialNodes(), lst);
 		lst.finish();
 		mResultIcfg = resultIcfg;
-//		return resultIcfg;
-//		final BasicIcfg<OUTLOC> resultIcfg =
-//				new BasicIcfg<>(newIcfgIdentifier, originalIcfg.getCfgSmtToolkit(), outLocationClass);
-//		mResultIcfg = null;
 	}
 
 	private void processLocations(final Set<INLOC> init, final TransformedIcfgBuilder<INLOC, OUTLOC> lst) {