see #108: use blockencoding in PathInvariantsGenerator (and fix a bug…

… in PathProgram and avoid a dependency cycle)

trunk/source/BlockEncodingV2/META-INF/MANIFEST.MF

@@ -11,7 +11,8 @@ Require-Bundle: de.uni_freiburg.informatik.ultimate.lib.core,
  de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils,
  de.uni_freiburg.informatik.ultimate.boogie.preprocessor,
  de.uni_freiburg.informatik.ultimate.lib.smtlib,
- de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder,
- de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer
+ de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder
+Export-Package: de.uni_freiburg.informatik.ultimate.plugins.blockencoding, 
+ de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences
 Bundle-ActivationPolicy: lazy
 Bundle-RequiredExecutionEnvironment: JavaSE-1.8

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/BlockEncoder.java

@@ -31,16 +31,22 @@
 import java.util.Set;
 import java.util.function.Supplier;
 
+import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.BuchiProgramAcceptingStateAnnotation;
 import de.uni_freiburg.informatik.ultimate.core.lib.results.TimeoutResult;
 import de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils;
 import de.uni_freiburg.informatik.ultimate.core.model.preferences.IPreferenceProvider;
 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.logic.Term;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.BasicIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.IcfgUtils;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
+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.structure.IcfgLocationIterator;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.TransFormula;
+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.plugins.blockencoding.encoding.AssumeMerger;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.IEncoder;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.IcfgEdgeBuilder;
@@ -53,18 +59,21 @@
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.RemoveInfeasibleEdges;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.RemoveSinkStates;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.Simplifier;
-import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.PreferenceInitializer;
-import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.PreferenceInitializer.MinimizeStates;
-import de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.annot.BuchiProgramAcceptingStateAnnotation;
+import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.BlockEncodingPreferences;
+import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.BlockEncodingPreferences.MinimizeStates;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.BoogieIcfgLocation;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.util.IcfgSizeBenchmark;
 
 /**
+ *
+ * The {@link BlockEncoder} provides different kinds of transformations for {@link IIcfg}s. These transformations
+ * transcode the {@link TransFormula}s and the structure of an {@link IIcfg} s.t. you may have more or less edges and
+ * nodes.
  *
  * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
  *
  */
-public class BlockEncoder {
+public final class BlockEncoder {
 
 	private static final BuchiProgramAcceptingStateAnnotation BUCHI_PROGRAM_ACCEPTING_STATE_ANNOTATION =
 			new BuchiProgramAcceptingStateAnnotation();
@@ -76,6 +85,20 @@ public class BlockEncoder {
 
 	private BasicIcfg<IcfgLocation> mIterationResult;
 
+	/**
+	 * Create a {@link BlockEncoder} for the BlockEncoding plugin.
+	 * 
+	 * @param logger
+	 *            The logger to use.
+	 * @param services
+	 *            A {@link IUltimateServiceProvider} instance.
+	 * @param backtranslator
+	 *            A backtranslator that is already registered with the toolchain
+	 * @param builder
+	 *            An edge builder
+	 * @param icfg
+	 *            An icfg
+	 */
 	public BlockEncoder(final ILogger logger, final IUltimateServiceProvider services,
 			final BlockEncodingBacktranslator backtranslator, final IcfgEdgeBuilder builder,
 			final BasicIcfg<IcfgLocation> icfg) {
@@ -87,23 +110,58 @@ public BlockEncoder(final ILogger logger, final IUltimateServiceProvider service
 		processIcfg(icfg);
 	}
 
-	public IIcfg<?> getResult() {
+	/**
+	 * Create a {@link BlockEncoder} instance for usage from anywhere. Does not register its backtranslation and does
+	 * create the necessary data structures for itself.
+	 * 
+	 * @param logger
+	 *            The logger we should use.
+	 * @param services
+	 *            A {@link IUltimateServiceProvider} instance that is used to get the preferences (use
+	 *            {@link IUltimateServiceProvider#registerPreferenceLayer(Class, String...) and
+	 *            BlockEncodingPreferences}.
+	 * @param originalIcfg
+	 *            The {@link IIcfg} you wish to encode.
+	 * @param simplificationTechnique
+	 *            The {@link SimplificationTechnique} that should be used.
+	 * @param xnfConversionTechnique
+	 *            The {@link XnfConversionTechnique} that should be used.
+	 */
+	public BlockEncoder(final ILogger logger, final IUltimateServiceProvider services, final IIcfg<?> originalIcfg,
+			final SimplificationTechnique simplificationTechnique,
+			final XnfConversionTechnique xnfConversionTechnique) {
+		mServices = services;
+		mLogger = logger;
+		mBacktranslator = new BlockEncodingBacktranslator(IcfgEdge.class, Term.class, mLogger);
+		mEdgeBuilder = new IcfgEdgeBuilder(originalIcfg.getCfgSmtToolkit(), mServices, simplificationTechnique,
+				xnfConversionTechnique);
+		final BasicIcfg<IcfgLocation> copiedIcfg =
+				new IcfgDuplicator(mLogger, mServices, mBacktranslator, simplificationTechnique, xnfConversionTechnique)
+						.copy(originalIcfg);
+		processIcfg(copiedIcfg);
+	}
+
+	public IIcfg<IcfgLocation> getResult() {
 		return mIterationResult;
 	}
 
+	public BlockEncodingBacktranslator getBacktranslator() {
+		return mBacktranslator;
+	}
+
 	private void processIcfg(final BasicIcfg<IcfgLocation> node) {
 		// measure size of rcfg
 		reportSizeBenchmark("Initial Icfg", node);
 
 		final IPreferenceProvider ups = mServices.getPreferenceProvider(Activator.PLUGIN_ID);
-		int maxIters = ups.getInt(PreferenceInitializer.FXP_MAX_ITERATIONS) - 1;
+		int maxIters = ups.getInt(BlockEncodingPreferences.FXP_MAX_ITERATIONS) - 1;
 		if (maxIters < 0) {
 			maxIters = -1;
 		}
 
 		mIterationResult = node;
 		final List<Supplier<IEncoder<IcfgLocation>>> encoderProviders = getEncoderProviders(ups, node);
-		final boolean optimizeUntilFixpoint = ups.getBoolean(PreferenceInitializer.FXP_UNTIL_FIXPOINT);
+		final boolean optimizeUntilFixpoint = ups.getBoolean(BlockEncodingPreferences.FXP_UNTIL_FIXPOINT);
 		int i = 1;
 
 		while (true) {
@@ -120,7 +178,7 @@ private void processIcfg(final BasicIcfg<IcfgLocation> node) {
 					mLogger.debug("Current error locations: " + IcfgUtils.getErrorLocations(currentResult.getIcfg()));
 					new IcfgLocationIterator<>(currentResult.getIcfg()).asStream().forEach(a -> {
 						mLogger.debug("Annotations of " + a);
-						ModelUtils.consumeAnnotations(a, x -> mLogger.debug(x.getClass()));
+						ModelUtils.consumeAnnotations(a, x -> mLogger.debug(x.getValue().getClass()));
 					});
 				}
 			}
@@ -145,12 +203,12 @@ private void processIcfg(final BasicIcfg<IcfgLocation> node) {
 			mLogger.debug("==== BE Post Processing ====");
 		}
 
-		if (ups.getBoolean(PreferenceInitializer.POST_USE_PARALLEL_COMPOSITION)) {
+		if (ups.getBoolean(BlockEncodingPreferences.POST_USE_PARALLEL_COMPOSITION)) {
 			mIterationResult =
 					new ParallelComposer(mEdgeBuilder, mServices, mBacktranslator).getResult(mIterationResult);
 		}
 
-		if (ups.getBoolean(PreferenceInitializer.POST_SIMPLIFY_CODEBLOCKS)) {
+		if (ups.getBoolean(BlockEncodingPreferences.POST_SIMPLIFY_CODEBLOCKS)) {
 			mIterationResult = new Simplifier(mEdgeBuilder, mServices, mBacktranslator).getResult(mIterationResult);
 		}
 
@@ -163,17 +221,17 @@ private List<Supplier<IEncoder<IcfgLocation>>> getEncoderProviders(final IPrefer
 
 		// note that the order is important
 
-		if (ups.getBoolean(PreferenceInitializer.FXP_REMOVE_INFEASIBLE_EDGES)) {
+		if (ups.getBoolean(BlockEncodingPreferences.FXP_REMOVE_INFEASIBLE_EDGES)) {
 			rtr.add(() -> new RemoveInfeasibleEdges(mServices, mBacktranslator));
 		}
 
-		if (ups.getBoolean(PreferenceInitializer.FXP_MAXIMIZE_FINAL_STATES)) {
+		if (ups.getBoolean(BlockEncodingPreferences.FXP_MAXIMIZE_FINAL_STATES)) {
 			rtr.add(() -> new MaximizeFinalStates(mServices, BlockEncoder::markBuchiProgramAccepting,
 					BlockEncoder::isBuchiProgramAccepting, mBacktranslator));
 		}
 
 		final MinimizeStates minimizeStates =
-				ups.getEnum(PreferenceInitializer.FXP_MINIMIZE_STATES, MinimizeStates.class);
+				ups.getEnum(BlockEncodingPreferences.FXP_MINIMIZE_STATES, MinimizeStates.class);
 		if (minimizeStates != MinimizeStates.NONE) {
 			switch (minimizeStates) {
 			case SINGLE:
@@ -194,11 +252,11 @@ private List<Supplier<IEncoder<IcfgLocation>>> getEncoderProviders(final IPrefer
 			}
 		}
 
-		if (ups.getBoolean(PreferenceInitializer.FXP_SIMPLIFY_ASSUMES)) {
+		if (ups.getBoolean(BlockEncodingPreferences.FXP_SIMPLIFY_ASSUMES)) {
 			rtr.add(() -> new AssumeMerger(mEdgeBuilder, mServices, mBacktranslator));
 		}
 
-		if (ups.getBoolean(PreferenceInitializer.FXP_REMOVE_SINK_STATES)) {
+		if (ups.getBoolean(BlockEncodingPreferences.FXP_REMOVE_SINK_STATES)) {
 			rtr.add(() -> new RemoveSinkStates(mServices, BlockEncoder::hasToBePreserved, mBacktranslator));
 		}
 

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/BlockEncoding.java

@@ -44,7 +44,7 @@
 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.plugins.blockencoding.encoding.SmallBlockEncoder;
-import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.PreferenceInitializer;
+import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.BlockEncodingPreferences;
 
 /**
  * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de)
@@ -84,9 +84,9 @@ public void setInputDefinition(final ModelType graphType) {
 	@Override
 	public List<IObserver> getObservers() {
 		final List<IObserver> observers = new ArrayList<>();
-		if (mServices.getPreferenceProvider(Activator.PLUGIN_ID).getBoolean(PreferenceInitializer.PRE_SBE)) {
+		if (mServices.getPreferenceProvider(Activator.PLUGIN_ID).getBoolean(BlockEncodingPreferences.PRE_SBE)) {
 			final boolean rewriteAssumes = mServices.getPreferenceProvider(Activator.PLUGIN_ID)
-					.getBoolean(PreferenceInitializer.PRE_SBE_REWRITENOTEQUALS);
+					.getBoolean(BlockEncodingPreferences.PRE_SBE_REWRITENOTEQUALS);
 			observers.add(new SmallBlockEncoder(mLogger, mBacktranslator, rewriteAssumes, mServices,
 					SIMPLIFICATION_TECHNIQUE, XNF_CONVERSION_TECHNIQUE));
 		}
@@ -123,7 +123,7 @@ public List<String> getDesiredToolIds() {
 
 	@Override
 	public IPreferenceInitializer getPreferences() {
-		return new PreferenceInitializer();
+		return new BlockEncodingPreferences();
 	}
 
 	@Override

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/BlockEncodingBacktranslator.java

@@ -27,6 +27,7 @@
 package de.uni_freiburg.informatik.ultimate.plugins.blockencoding;
 
 import java.util.ArrayList;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
@@ -115,4 +116,19 @@ public void mapEdges(final IcfgEdge newEdge, final IcfgEdge originalEdge) {
 		// mLogger.info("Mapped [" + newEdge.hashCode() + "] " + newEdge);
 		// mLogger.info("To [" + mEdgeMapping.get(newEdge).hashCode() + "] " + mEdgeMapping.get(newEdge));
 	}
+
+	public void mapLocations(final IcfgLocation newLoc, final IcfgLocation oldLoc) {
+		final IcfgLocation realOldLoc = mLocationMapping.get(oldLoc);
+		if (realOldLoc != null) {
+			// this means we replaced an edge which we already replaced again
+			// with something new, we have to map this to the real original
+			mLocationMapping.put(newLoc, realOldLoc);
+		} else {
+			mLocationMapping.put(newLoc, oldLoc);
+		}
+	}
+
+	public Map<IcfgLocation, IcfgLocation> getLocationMapping() {
+		return Collections.unmodifiableMap(mLocationMapping);
+	}
 }

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/IcfgDuplicator.java

@@ -90,8 +90,7 @@ private BasicIcfg<IcfgLocation> createIcfgCopy(final IcfgEdgeBuilder edgeBuilder
 		while (iter.hasNext()) {
 			final IcfgLocation oldLoc = iter.next();
 			final String proc = oldLoc.getProcedure();
-			final IcfgLocation newLoc = new IcfgLocation(oldLoc.getDebugIdentifier(), proc);
-			ModelUtils.copyAnnotations(oldLoc, newLoc);
+			final IcfgLocation newLoc = createLocCopy(oldLoc);
 
 			final boolean isError = icfg.getProcedureErrorNodes().get(proc) != null
 					&& icfg.getProcedureErrorNodes().get(proc).contains(oldLoc);
@@ -129,12 +128,19 @@ private BasicIcfg<IcfgLocation> createIcfgCopy(final IcfgEdgeBuilder edgeBuilder
 		if (mLogger.isDebugEnabled()) {
 			new IcfgLocationIterator<>(newIcfg).asStream().forEach(a -> {
 				mLogger.debug("Annotations of " + a);
-				ModelUtils.consumeAnnotations(a, x -> mLogger.debug(x.getClass()));
+				ModelUtils.consumeAnnotations(a, x -> mLogger.debug(x.getValue().getClass()));
 			});
 		}
 		return newIcfg;
 	}
 
+	private IcfgLocation createLocCopy(final IcfgLocation oldLoc) {
+		final IcfgLocation newLoc = new IcfgLocation(oldLoc.getDebugIdentifier(), oldLoc.getProcedure());
+		ModelUtils.copyAnnotations(oldLoc, newLoc);
+		mBacktranslator.mapLocations(newLoc, oldLoc);
+		return newLoc;
+	}
+
 	private boolean noEdges(final IIcfg<IcfgLocation> icfg) {
 
 		final Set<IcfgLocation> programPoints = icfg.getProgramPoints().entrySet().stream()

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/encoding/AssumeMerger.java

@@ -46,7 +46,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.Activator;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncodingBacktranslator;
-import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.PreferenceInitializer;
+import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.BlockEncodingPreferences;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CodeBlock;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.StatementSequence;
 
@@ -70,9 +70,9 @@ public AssumeMerger(final IcfgEdgeBuilder edgeBuilder, final IUltimateServicePro
 		super(services, backtranslator);
 		mAssumesMerged = 0;
 		mRewriteNotEquals = mServices.getPreferenceProvider(Activator.PLUGIN_ID)
-				.getBoolean(PreferenceInitializer.FXP_SIMPLIFY_ASSUMES_REWRITENOTEQUALS);
+				.getBoolean(BlockEncodingPreferences.FXP_SIMPLIFY_ASSUMES_REWRITENOTEQUALS);
 		mUseSBE = mServices.getPreferenceProvider(Activator.PLUGIN_ID)
-				.getBoolean(PreferenceInitializer.FXP_SIMPLIFY_ASSUMES_SBE);
+				.getBoolean(BlockEncodingPreferences.FXP_SIMPLIFY_ASSUMES_SBE);
 		mEdgeBuilder = edgeBuilder;
 	}
 

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/encoding/BaseMinimizeStates.java

@@ -45,7 +45,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.Activator;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncodingBacktranslator;
-import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.PreferenceInitializer;
+import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.preferences.BlockEncodingPreferences;
 
 /**
  * Base class for encoder that try to minimize the nodes/states/locations of an RCFG.
@@ -64,7 +64,7 @@ public BaseMinimizeStates(final IcfgEdgeBuilder edgeBuilder, final IUltimateServ
 			final BiPredicate<IIcfg<?>, IcfgLocation> funHasToBePreserved) {
 		super(services, backtranslator);
 		mIgnoreBlowup = mServices.getPreferenceProvider(Activator.PLUGIN_ID)
-				.getBoolean(PreferenceInitializer.FXP_MINIMIZE_STATES_IGNORE_BLOWUP);
+				.getBoolean(BlockEncodingPreferences.FXP_MINIMIZE_STATES_IGNORE_BLOWUP);
 		mFunHasToBePreserved = funHasToBePreserved;
 		mEdgeBuilder = edgeBuilder;
 	}

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/encoding/IcfgEdgeBuilder.java

@@ -197,7 +197,7 @@ public IcfgEdge constructCopy(final IcfgLocation source, final IcfgLocation targ
 			rtr = new IcfgReturnTransition(source, target, correspondingCall, null, rAction.getAssignmentOfReturn(),
 					rAction.getLocalVarsAssignmentOfCall());
 		} else {
-			throw new UnsupportedOperationException("Unknown IcfgEdge subtype");
+			throw new UnsupportedOperationException("Unknown IcfgEdge subtype: " + oldEdge.getClass());
 		}
 		source.addOutgoing(rtr);
 		target.addIncoming(rtr);

trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/preferences/PreferenceInitializer.java → trunk/source/BlockEncodingV2/src/de/uni_freiburg/informatik/ultimate/plugins/blockencoding/preferences/BlockEncodingPreferences.java

@@ -31,7 +31,9 @@
 import de.uni_freiburg.informatik.ultimate.core.model.preferences.UltimatePreferenceItem;
 import de.uni_freiburg.informatik.ultimate.plugins.blockencoding.Activator;
 
-public class PreferenceInitializer extends UltimatePreferenceInitializer {
+public class BlockEncodingPreferences extends UltimatePreferenceInitializer {
+
+	public static final String PLUGIN_ID = Activator.PLUGIN_ID;
 
 	public enum MinimizeStates {
 		NONE, SINGLE, SINGLE_NODE_MULTI_EDGE, MULTI
@@ -77,7 +79,7 @@ public enum MinimizeStates {
 	private static final String POST_USE_PARALLEL_COMPOSITION_DESC = null;
 	private static final String POST_SIMPLIFY_CODEBLOCKS_DESC = null;
 
-	public PreferenceInitializer() {
+	public BlockEncodingPreferences() {
 		super(Activator.PLUGIN_ID, Activator.PLUGIN_NAME);
 	}