Accelerated Interpolation: Do not use fresh variables

ultimate-pa · Apr 16, 2021 · 70eefee · 70eefee · JonasWerner · Apr 16, 2021
1 parent 51c6806
commit 70eefee
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 22 deletions.
diff --git a/...eiburg/informatik/ultimate/lib/acceleratedinterpolation/AcceleratedInterpolationCore.java b/...eiburg/informatik/ultimate/lib/acceleratedinterpolation/AcceleratedInterpolationCore.java
@@ -190,7 +190,7 @@ public LBool acceleratedInterpolationCoreIsCorrect() {
 				Term t = mPredHelper.makeReflexive(acceleratedLoopRelation.getFormula(), acceleratedLoopRelation);
 				t = PartialQuantifierElimination.tryToEliminate(mServices, mLogger, mScript, t,
 						mSimplificationTechnique, XnfConversionTechnique.BOTTOM_UP_WITH_LOCAL_SIMPLIFICATION);
-				final UnmodifiableTransFormula tf = mPredHelper.normalizeTerm(t, acceleratedLoopRelation, true);
+				final UnmodifiableTransFormula tf = mPredHelper.normalizeTerm(t, acceleratedLoopRelation, false);
 
 				if (mLogger.isDebugEnabled()) {
 					mLogger.debug("Computed Acceleration: " + tf.getFormula().toStringDirect());

diff --git a/...src/de/uni_freiburg/informatik/ultimate/lib/acceleratedinterpolation/PredicateHelper.java b/...src/de/uni_freiburg/informatik/ultimate/lib/acceleratedinterpolation/PredicateHelper.java
@@ -127,32 +127,32 @@ public UnmodifiableTransFormula normalizeTerm(final Term t, final UnmodifiableTr
 		final HashMap<Term, Term> subMap = new HashMap<>();
 		final Term tTerm = t;
 
-		final Map<IProgramVar, TermVariable> inVars = new HashMap<>();
-		final Map<IProgramVar, TermVariable> outVars = new HashMap<>();
-
-		for (final Entry<IProgramVar, TermVariable> outVar : tf.getOutVars().entrySet()) {
-			final TermVariable newTV;
-			if (fresh) {
+		final Map<IProgramVar, TermVariable> inVars;
+		final Map<IProgramVar, TermVariable> outVars;
+
+		final Term newTerm;
+		if (fresh) {
+			inVars = new HashMap<>();
+			outVars = new HashMap<>();
+			for (final Entry<IProgramVar, TermVariable> outVar : tf.getOutVars().entrySet()) {
+				final TermVariable newTV;
 				newTV = mScript.constructFreshCopy(outVar.getKey().getTermVariable());
-			} else {
-				newTV = outVar.getKey().getTermVariable();
+				subMap.put(outVar.getValue(), newTV);
+				outVars.put(outVar.getKey(), newTV);
 			}
-			subMap.put(outVar.getValue(), newTV);
-			outVars.put(outVar.getKey(), newTV);
-		}
-		for (final Entry<IProgramVar, TermVariable> inVar : tf.getInVars().entrySet()) {
-			final TermVariable newTV;
-			if (fresh) {
+			for (final Entry<IProgramVar, TermVariable> inVar : tf.getInVars().entrySet()) {
+				final TermVariable newTV;
 				newTV = mScript.constructFreshCopy(inVar.getKey().getTermVariable());
-			} else {
-				newTV = inVar.getKey().getTermVariable();
+				subMap.put(inVar.getValue(), newTV);
+				inVars.put(inVar.getKey(), newTV);
 			}
-			subMap.put(inVar.getValue(), newTV);
-			inVars.put(inVar.getKey(), newTV);
+			final Substitution sub = new Substitution(mScript, subMap);
+			newTerm = sub.transform(tTerm);
+		} else {
+			inVars = new HashMap<>(tf.getInVars());
+			outVars = new HashMap<>(tf.getOutVars());
+			newTerm = tTerm;
 		}
-		final Substitution sub = new Substitution(mScript, subMap);
-		final Term newTerm = sub.transform(tTerm);
-
 		final TransFormulaBuilder tfb = new TransFormulaBuilder(inVars, outVars, true, Collections.emptySet(), true,
 				Collections.emptySet(), false);
 		tfb.setFormula(newTerm);