#239, cleanup: remove VPDomainPreanalysis

ultimate-pa · Oct 23, 2017 · 5f350b4 · 5f350b4
1 parent 6d67c4c
commit 5f350b4
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 685 deletions.
diff --git a/...mate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqPostOperator.java b/...mate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqPostOperator.java
@@ -78,7 +78,6 @@ public class EqPostOperator<ACTION extends IIcfgTransition<IcfgLocation>>
 	private final CfgSmtToolkit mCfgSmtToolkit;
 	private final EqConstraintFactory<EqNode> mEqConstraintFactory;
 	private final EqNodeAndFunctionFactory mEqNodeAndFunctionFactory;
-	private final VPDomainPreanalysis mPreAnalysis;
 
 	private final boolean mDebug = true;
 
@@ -87,15 +86,14 @@ public class EqPostOperator<ACTION extends IIcfgTransition<IcfgLocation>>
 
 	private final EqStateFactory mEqStateFactory;
 
-	public EqPostOperator(final IUltimateServiceProvider services, final ILogger logger,
+	public EqPostOperator(final IUltimateServiceProvider services, final ILogger logger, final CfgSmtToolkit csToolkit,
 			final EqNodeAndFunctionFactory eqNodeAndFunctionFactory,
-			final EqConstraintFactory<EqNode> eqConstraintFactory, final VPDomainPreanalysis preAnalysis,
+			final EqConstraintFactory<EqNode> eqConstraintFactory,
 			final EqStateFactory eqStateFactory) {
 		mEqNodeAndFunctionFactory = eqNodeAndFunctionFactory;
 		mEqConstraintFactory = eqConstraintFactory;
-		mPreAnalysis = preAnalysis;
-		mMgdScript = preAnalysis.getManagedScript();
-		mCfgSmtToolkit = preAnalysis.getCfgSmtToolkit();
+		mCfgSmtToolkit = csToolkit;
+		mMgdScript = csToolkit.getManagedScript();
 		mEqStateFactory = eqStateFactory;
 
 		mServices = services;
@@ -112,7 +110,7 @@ public EqPostOperator(final IUltimateServiceProvider services, final ILogger log
 
 	@Override
 	public List<EqState> apply(final EqState oldState, final ACTION transition) {
-		if (!mPreAnalysis.getServices().getProgressMonitorService().continueProcessing()) {
+		if (!mServices.getProgressMonitorService().continueProcessing()) {
 			return toEqStates(mEqConstraintFactory.getTopDisjunctiveConstraint(), oldState.getVariables());
 		}
 
@@ -138,14 +136,14 @@ assert preciseStrongestPostImpliesAbstractPost(oldState, transition,
 	 * @param variablesThatTheFrameworkLikesToSee
 	 * @return
 	 */
-	public List<EqState> toEqStates(final EqDisjunctiveConstraint<EqNode> disjunctiveConstraint,
+	private List<EqState> toEqStates(final EqDisjunctiveConstraint<EqNode> disjunctiveConstraint,
 			final Set<IProgramVarOrConst> variablesThatTheFrameworkLikesToSee) {
-		// /*
-		// * The AbstractInterpretation framework demands that all EqStates here have the same Pvocs
-		// * Thus we set the Pvocs of all the disjunct-states to be the union of the pvocs that each
-		// * disjunct-state/constraint talks about.
-		// EDIT: the variables are now determined externally (by the oldstate of the post operator..)
-		// */
+		/*
+		 * The AbstractInterpretation framework demands that all EqStates here have the same Pvocs
+		 * Thus we set the Pvocs of all the disjunct-states to be the union of the pvocs that each
+		 * disjunct-state/constraint talks about.
+		 * EDIT: the variables are now determined externally (by the oldstate of the post operator..)
+		 */
 		return disjunctiveConstraint.getConstraints().stream()
 				.map(cons -> mEqStateFactory.getEqState(cons, variablesThatTheFrameworkLikesToSee))
 				.collect(Collectors.toList());
@@ -173,7 +171,7 @@ public List<EqState> apply(final EqState stateBeforeLeaving, final EqState hiera
 		// assert hierarchicalPrestate.getVariables()
 		// .containsAll(mCfgSmtToolkit.getSymbolTable().getLocals(transition.getSucceedingProcedure()));
 
-		if (!mPreAnalysis.getServices().getProgressMonitorService().continueProcessing()) {
+		if (!mServices.getProgressMonitorService().continueProcessing()) {
 			return toEqStates(mEqConstraintFactory.getTopDisjunctiveConstraint(), hierarchicalPrestate.getVariables());
 		}
 

diff --git a/...k/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java b/...k/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java
@@ -46,7 +46,6 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.plugins.analysis.abstractinterpretationv2.Activator;
-import de.uni_freiburg.informatik.ultimate.util.statistics.Benchmark;
 
 /**
  * Domain of variable partition.
@@ -63,9 +62,8 @@ public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
 	private final ILogger mLogger;
 
 	private final ManagedScript mManagedScript;
-	private final VPDomainPreanalysis mPreAnalysis;
 	private final IIcfgSymbolTable mSymboltable;
-	private final boolean mDebugMode;
+	private boolean mDebugMode;
 
 	private final EqConstraintFactory<EqNode> mEqConstraintFactory;
 	private final EqNodeAndFunctionFactory mEqNodeAndFunctionFactory;
@@ -75,10 +73,8 @@ public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
 
 	private final VPDomainBenchmark mBenchmark;
 
-	public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit,
-			final VPDomainPreanalysis preAnalysis) {
+	public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit) {
 		mLogger = logger;
-		mPreAnalysis = preAnalysis;
 		mManagedScript = csToolkit.getManagedScript();
 		mMerge = new VPMergeOperator();
 		mSymboltable = csToolkit.getSymbolTable();
@@ -89,13 +85,10 @@ public VPDomain(final ILogger logger, final IUltimateServiceProvider services, f
 		mEqConstraintFactory = new EqConstraintFactory<>(mEqNodeAndFunctionFactory, mServices, mManagedScript);
 		mEqStateFactory = new EqStateFactory(mEqNodeAndFunctionFactory, mEqConstraintFactory, mSymboltable,
 				mManagedScript);
-//		mEqConstraintFactory.setEqStateFactory(mEqStateFactory);
 
-		mPost = new EqPostOperator<>(mServices, mLogger, mEqNodeAndFunctionFactory, mEqConstraintFactory, mPreAnalysis,
+		mPost = new EqPostOperator<>(mServices, mLogger, mCsToolkit, mEqNodeAndFunctionFactory, mEqConstraintFactory,
 				mEqStateFactory);
 
-		mDebugMode = mPreAnalysis.isDebugMode();
-
 		mBenchmark = new VPDomainBenchmark();
 	}
 
@@ -124,10 +117,6 @@ public ILogger getLogger() {
 		return mLogger;
 	}
 
-	public VPDomainPreanalysis getPreAnalysis() {
-		return mPreAnalysis;
-	}
-
 	public IIcfgSymbolTable getSymbolTable() {
 		return mSymboltable;
 	}
@@ -146,11 +135,6 @@ public boolean isDebugMode() {
 		return mDebugMode;
 	}
 
-	public Benchmark getVpBenchmark() {
-		return mPreAnalysis.getBenchmark();
-	}
-
-
 	public EqStateFactory getEqStateFactory() {
 		return mEqStateFactory;
 	}