#295, odds and ends for heap separator

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/arraytheory/SMTTheoryState.java

@@ -212,7 +212,7 @@ public boolean areUnequal(final Term t1, final Term t2) {
 	}
 
 	@Override
-	public IEqualityProvidingState union(final IEqualityProvidingState other) {
+	public IEqualityProvidingState join(final IEqualityProvidingState other) {
 		return union((SMTTheoryState) other);
 	}
 

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqState.java

@@ -42,14 +42,15 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.BoogieConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramOldVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingIntermediateState;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingState;
 
 /**
  *
  * @author Alexander Nutz (nutz@informatik.uni-freiburg.de)
  *
  */
-public class EqState implements IAbstractState<EqState>, IEqualityProvidingState {
+public class EqState implements IAbstractState<EqState>, IEqualityProvidingState, IEqualityProvidingIntermediateState {
 
 	/**
 	 * The variables and constants that this state has "for the abstract interpretation"/"as an IAbstractState". Note
@@ -291,7 +292,17 @@ public boolean equals(final Object obj) {
 	}
 
 	@Override
-	public IEqualityProvidingState union(final IEqualityProvidingState other) {
+	public IEqualityProvidingState join(final IEqualityProvidingState other) {
+		return union((EqState) other);
+	}
+
+	/**
+	 * Note that an EqState is a bad IEqualityProvidingIntermediateState because it does not contain information on any
+	 * auxVar.
+	 * TODO
+	 */
+	@Override
+	public IEqualityProvidingIntermediateState join(final IEqualityProvidingIntermediateState other) {
 		return union((EqState) other);
 	}
 

trunk/source/IcfgTransformation/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtransformation/AbsIntEqualityProvider.java

@@ -27,6 +27,7 @@
 package de.uni_freiburg.informatik.ultimate.plugins.icfgtransformation;
 
 import java.util.Collection;
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
@@ -42,7 +43,9 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.EqualityAnalysisResult;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityAnalysisResultProvider;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingIntermediateState;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingState;
+import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.domain.transformula.vp.EqState;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.tool.AbstractInterpreter;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.Doubleton;
 
@@ -125,8 +128,8 @@ public IEqualityProvidingState getEqualityProvidingStateForLocationSet(final Set
 				continue;
 			}
 			final IEqualityProvidingState unionStateForCurrentLoc =
-					mLoc2States.get(loc).stream().reduce((s1, s2) -> s1.union(s2)).get();
-			result = result == null ? unionStateForCurrentLoc : result.union(unionStateForCurrentLoc);
+					mLoc2States.get(loc).stream().reduce((s1, s2) -> s1.join(s2)).get();
+			result = result == null ? unionStateForCurrentLoc : result.join(unionStateForCurrentLoc);
 		}
 		if (result == null) {
 			result = mTopState;
@@ -135,4 +138,12 @@ public IEqualityProvidingState getEqualityProvidingStateForLocationSet(final Set
 		return result;
 	}
 
+	/**
+	 * TODO: implement intermediate states that contain auxVar information
+	 */
+	@Override
+	public IEqualityProvidingIntermediateState getEqualityProvidingIntermediateState(final IcfgEdge edge) {
+		return (EqState) getEqualityProvidingStateForLocationSet(Collections.singleton(edge.getSource()));
+	}
+
 }

trunk/source/IcfgTransformation/src/de/uni_freiburg/informatik/ultimate/plugins/icfgtransformation/IcfgTransformationObserver.java

@@ -30,14 +30,12 @@
 import java.util.ArrayList;
 import java.util.List;
 
-import de.uni_freiburg.informatik.ultimate.core.lib.results.GenericResult;
 import de.uni_freiburg.informatik.ultimate.core.lib.results.StatisticsResult;
 import de.uni_freiburg.informatik.ultimate.core.model.models.IElement;
 import de.uni_freiburg.informatik.ultimate.core.model.models.ModelType;
 import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils;
 import de.uni_freiburg.informatik.ultimate.core.model.observers.IUnmanagedObserver;
 import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider;
-import de.uni_freiburg.informatik.ultimate.core.model.results.IResultWithSeverity.Severity;
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
 import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IBacktranslationTracker;
@@ -68,6 +66,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transformations.ReplacementVarFactory;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramNonOldVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils.SimplificationTechnique;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils.XnfConversionTechnique;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.DefaultEqualityAnalysisProvider;
@@ -197,12 +196,24 @@ private <INLOC extends IcfgLocation, OUTLOC extends IcfgLocation> IIcfg<OUTLOC>
 			final IUltimateServiceProvider services,
 			final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider) {
 
+		// TODO: hacky
+		IProgramNonOldVar validArray = null;
+		for (final IProgramNonOldVar global : icfg.getCfgSmtToolkit().getSymbolTable().getGlobals()) {
+			if (global.getGloballyUniqueId().equals("#valid")) {
+				validArray = global;
+				break;
+			}
+		}
+		if (validArray == null) {
+			throw new AssertionError("TODO: what should we do in this case? maybe return the input icfg?");
+		}
+
 		final HeapSepIcfgTransformer<INLOC, OUTLOC> icfgTransformer =
-				new HeapSepIcfgTransformer<>(icfg, locFac, fac, backtranslationTracker, outlocClass,
-						"heap_separated_icfg", equalityProvider);
+				new HeapSepIcfgTransformer<>(mLogger, icfg, locFac, fac, backtranslationTracker, outlocClass,
+						"heap_separated_icfg", equalityProvider, validArray);
 
-		mServices.getResultService().reportResult(Activator.PLUGIN_ID, new GenericResult(Activator.PLUGIN_ID,
-				"HeapSeparationSummary", icfgTransformer.getHeapSeparationSummary(), Severity.INFO));
+//		mServices.getResultService().reportResult(Activator.PLUGIN_ID, new GenericResult(Activator.PLUGIN_ID,
+//				"HeapSeparationSummary", icfgTransformer.getHeapSeparationSummary(), Severity.INFO));
 		mServices.getResultService().reportResult(Activator.PLUGIN_ID,
 				new StatisticsResult<>(Activator.PLUGIN_ID, "HeapSeparatorStatistics",
 						icfgTransformer.getStatistics()));

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

@@ -1,6 +1,7 @@
 package de.uni_freiburg.informatik.ultimate.icfgtransformer;
 
 import java.util.ArrayList;
+import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
 
@@ -9,14 +10,13 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.BasicIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgCallTransition;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgInternalTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgReturnTransition;
-import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgCallTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdgeFactory;
-import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgInternalTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocationIterator;
-import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgReturnTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transformations.ReplacementVarFactory;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
@@ -41,24 +41,29 @@ public abstract class IcfgTransitionTransformer<INLOC extends IcfgLocation, OUTL
 	/**
 	 * TODO: it is important that any override of transform updates this map! (not nice, as it is now..)
 	 */
-	protected Map<IcfgCallTransition, IcfgCallTransition> mOldCallToNewCall;
+	protected final Map<IIcfgCallTransition<INLOC>, IIcfgCallTransition<OUTLOC>> mOldCallToNewCall;
 
 	protected final IIcfg<INLOC> mInputIcfg;
 
 	private final TransformedIcfgBuilder<INLOC, OUTLOC> mTransformedIcfgBuilder;
 	private final BasicIcfg<OUTLOC> mResult;
 
+	private boolean mProcessed;
+
 	public IcfgTransitionTransformer(final ILogger logger, final String resultName,
 			final Class<OUTLOC> outLocClazz, final IIcfg<INLOC> inputCfg,
 			final ILocationFactory<INLOC, OUTLOC> funLocFac,
 			final IBacktranslationTracker backtranslationTracker) {
+		assert logger != null;
 		mInputCfgCsToolkit = inputCfg.getCfgSmtToolkit();
 		mLogger = logger;
 		mInputIcfg = inputCfg;
 
 		mMgdScript = mInputCfgCsToolkit.getManagedScript();
 		mEdgeFactory = mInputCfgCsToolkit.getIcfgEdgeFactory();
 
+		mOldCallToNewCall = new HashMap<>();
+
 		/*
 		 * the csToolkit will be replaced in mResult by mTransformedIcfgBuilder.finish() (not a fan of this solution..)
 		 * the new csToolkit constructed there will get a new symbol table, too..
@@ -70,8 +75,14 @@ public IcfgTransitionTransformer(final ILogger logger, final String resultName,
 						mInputCfgCsToolkit.getSymbolTable(), new ReplacementVarFactory(mInputCfgCsToolkit, false));
 		mTransformedIcfgBuilder = new TransformedIcfgBuilder<>(funLocFac,
 				backtranslationTracker, noopTransformer, mInputIcfg, mResult);
+	}
+
+
+	private void process() {
+		assert !mProcessed : "only call this once!";
 		processGraph();
 		mTransformedIcfgBuilder.finish();
+		mProcessed = true;
 	}
 
 	private void processGraph() {
@@ -123,18 +134,19 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
 	 */
 	protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSource, final OUTLOC newTarget,
 			final UnmodifiableTransFormula newTransformula) {
-		if (oldTransition instanceof IcfgInternalTransition) {
+		if (oldTransition instanceof IIcfgInternalTransition) {
 			// TODO: is this the right payload?
 			return mEdgeFactory.createInternalTransition(newSource, newTarget, oldTransition.getPayload(),
 					newTransformula);
-		} else if (oldTransition instanceof IcfgCallTransition) {
-			final IcfgCallTransition newCallTransition = mEdgeFactory.createCallTransition(newSource, newTarget,
-					oldTransition.getPayload(), newTransformula);
-			mOldCallToNewCall.put((IcfgCallTransition) oldTransition, newCallTransition);
-			return newCallTransition;
-		} else if (oldTransition instanceof IcfgReturnTransition) {
-			final IcfgCallTransition correspondingNewCall =
-					mOldCallToNewCall.get(((IcfgReturnTransition) oldTransition).getCorrespondingCall());
+		} else if (oldTransition instanceof IIcfgCallTransition) {
+			// TODO: this casting business is ugly like this
+			final IIcfgCallTransition<OUTLOC> newCallTransition = (IIcfgCallTransition<OUTLOC>)
+					mEdgeFactory.createCallTransition(newSource, newTarget, oldTransition.getPayload(), newTransformula);
+			mOldCallToNewCall.put((IIcfgCallTransition<INLOC>) oldTransition, newCallTransition);
+			return (IcfgEdge) newCallTransition;
+		} else if (oldTransition instanceof IIcfgReturnTransition) {
+			final IIcfgCallTransition<IcfgLocation> correspondingNewCall =
+					(IIcfgCallTransition<IcfgLocation>) mOldCallToNewCall.get(((IIcfgReturnTransition) oldTransition).getCorrespondingCall());
 			assert correspondingNewCall != null;
 			return mEdgeFactory.createReturnTransition(newSource, newTarget, correspondingNewCall,
 					oldTransition.getPayload(), newTransformula, correspondingNewCall.getLocalVarsAssignment());
@@ -143,8 +155,14 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
 		}
 	}
 
+	/**
+	 * Triggers the necessary computations (once per instance) and returns the result
+	 */
 	@Override
 	public final IIcfg<OUTLOC> getResult() {
+		if (!mProcessed) {
+			process();
+		}
 		return mResult;
 	}
 }

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

@@ -6,6 +6,7 @@
 import java.util.Set;
 
 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;
@@ -52,19 +53,32 @@ public static List<ArrayCellAccess> extractArrayCellAccesses(final Term formula)
 	}
 
 	public Term getArray() {
-		// TODO Auto-generated method stub
-		return null;
+		if (mArraySelect != null) {
+			return mArraySelect.getArray();
+		}
+		if (mArraySelectOverStore != null) {
+			return mArraySelectOverStore.getArrayStore().getArray();
+		}
+		throw new AssertionError();
 	}
 
 	public Term getIndex() {
-		// TODO Auto-generated method stub
-		return null;
+		if (mArraySelect != null) {
+			return mArraySelect.getIndex();
+		}
+		if (mArraySelectOverStore != null) {
+			return mArraySelectOverStore.getIndex();
+		}
+		throw new AssertionError();
 	}
 
-
-//	Term getTerm() {
-//		if (mArraySelect != null) {
-//			return SMT
-//		}
-//	}
+	public Term getTerm(final Script script) {
+		if (mArraySelect != null) {
+			return mArraySelect.toTerm(script);
+		}
+		if (mArraySelectOverStore != null) {
+			return mArraySelectOverStore.toTerm(script);
+		}
+		throw new AssertionError();
+	}
 }

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

@@ -131,4 +131,30 @@ public static List<ArrayEqualityAllowStores> extractArrayEqualityAllowStores(fin
 		return result;
 
 	}
+
+	public Term getLhsArray() {
+		if (mArrayUpdate != null) {
+			return mArrayUpdate.getNewArray();
+		}
+		if (mArrayEquality != null) {
+			return mArrayEquality.getLhs();
+		}
+		if (mOther != null) {
+			throw new UnsupportedOperationException("implement this, when it occurs..");
+		}
+		throw new AssertionError();
+	}
+
+	public Term getRhsArray() {
+		if (mArrayUpdate != null) {
+			return mArrayUpdate.getOldArray();
+		}
+		if (mArrayEquality != null) {
+			return mArrayEquality.getRhs();
+		}
+		if (mOther != null) {
+			throw new UnsupportedOperationException("implement this, when it occurs..");
+		}
+		throw new AssertionError();
+	}
 }

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

@@ -1,11 +1,16 @@
 package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
 
+import java.util.Collections;
 import java.util.Set;
 
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 
 public class ArrayGroup {
-	Set<IProgramVarOrConst> mArraysInThisGroup;
+	private final Set<IProgramVarOrConst> mArraysInThisGroup;
+
+	public ArrayGroup(final Set<IProgramVarOrConst> block) {
+		mArraysInThisGroup = Collections.unmodifiableSet(block);
+	}
 
 	Set<IProgramVarOrConst> getArrays() {
 		return mArraysInThisGroup;

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

@@ -12,6 +12,7 @@
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IBacktranslationTracker;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.ILocationFactory;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IcfgTransitionTransformer;
+import de.uni_freiburg.informatik.ultimate.logic.Rational;
 import de.uni_freiburg.informatik.ultimate.logic.Script;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
 import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
@@ -71,15 +72,15 @@ private void computeInitializingTerm(final Map<IProgramNonOldVar, IProgramConst>
 					frzLit));
 			mFreezeVarOutVars.put(en.getKey(), frzVar);
 
-			// "valid[lit_frz_l_x] = 1"
+			/*
+			 *  "valid[lit_frz_l_x] = 1"
+			 */
+			// TODO have to get the valid Termvariable from the Transformula or make a new one!
 			final Term select = SmtUtils.select(mMgdScript.getScript(), validArray.getTermVariable(), frzLit);
-			final Term one = mMgdScript.getScript().term("1");
-			initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), select, one));
-		}
+			// TODO -- is this the right way to get a constant?
+			final Term one = Rational.ONE.toTerm(mMgdScript.getScript().sort("Real"));
 
-		if (!freezeVarTofreezeVarLit.isEmpty()) {
-			mFreezeVarInVars.put(validArray, validArray.getTermVariable());
-			mFreezeVarOutVars.put(validArray, validArray.getTermVariable());
+			initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), select, one));
 		}
 
 		mInitializingTerm = SmtUtils.and(mMgdScript.getScript(), initializingEquations);
@@ -105,8 +106,14 @@ protected IcfgEdge transform(final IcfgEdge oldTransition, final OUTLOC newSourc
 			 */
 			final UnmodifiableTransFormula oldTransformula = oldTransition.getTransformula();
 
+//					if (!freezeVarTofreezeVarLit.isEmpty()) {
+//			mFreezeVarInVars.put(validArray, validArray.getTermVariable());
+//			mFreezeVarOutVars.put(validArray, validArray.getTermVariable());
+//		}
+
 			final Map<IProgramVar, TermVariable> newInVars = new HashMap<>(oldTransformula.getInVars());
 			newInVars.putAll(mFreezeVarInVars);
+
 			final Map<IProgramVar, TermVariable> newOutVars = new HashMap<>(oldTransformula.getOutVars());
 			newOutVars.putAll(mFreezeVarOutVars);