#295, support introduction of loc-array inititalization in disjunctiv…

…e formulas, too (only if they are in DNF, however)
ultimate-pa · Aug 28, 2018 · c337f3a · c337f3a
1 parent 154ac10
commit c337f3a
Showing 1 changed file with 31 additions and 21 deletions.
diff --git a/...icfgtransformer/heapseparator/transformers/MemlocArrayUpdaterTransformulaTransformer.java b/...icfgtransformer/heapseparator/transformers/MemlocArrayUpdaterTransformulaTransformer.java
@@ -189,31 +189,41 @@ public TransformulaTransformationResult transform(final IIcfgTransition<? extend
 			transitionFormulaWithLocUpdates = tf.getFormula();
 		}
 
+
 		// conjoin initialization code for unconstrained loc array variables
-		if (!SmtUtils.isNNF(tf.getFormula()) || SmtUtils.containsFunctionApplication(tf.getFormula(), "or")) {
-			throw new AssertionError("the code below only works for conjunctive formulas");
-		}
-		final Term transitionFormulaWithLocUpdatesAndLocInitialization;
-		{
-			final Set<TermVariable> unconstrainedVars = mEdgeToUnconstrainedVars.getImage(edgeInfo);
-			final List<Term> tfWithUpdatesAndInitConjuncts = new ArrayList<>();
-			tfWithUpdatesAndInitConjuncts.add(transitionFormulaWithLocUpdates);
-			for (final TermVariable ucv : unconstrainedVars) {
-				final MultiDimensionalSort mds = new MultiDimensionalSort(ucv.getSort());
-				final int dimensionality = mds.getDimension();
-				assert dimensionality > 0;
-				for (int dim = 0; dim < dimensionality; dim++) {
-					final LocArrayInfo locArray = mLocArrayManager.getOrConstructLocArray(edgeInfo, ucv, dim);
-					final Term initConjunct = SmtUtils.binaryEquality(mMgdScript.getScript(),
-							locArray.getTerm(),
-							locArray.getInitializingConstantArray());
-//							mLocArrayManager.getInitConstantArrayForLocArray(locArray));
-					tfWithUpdatesAndInitConjuncts.add(initConjunct);
+
+		// assuming the formula is in DNF
+		final List<Term> disjunctsWithLocUpdatesAndLocInitialization = new ArrayList<>();
+		for (final Term disjunct : SmtUtils.getDisjuncts(tf.getFormula())) {
+			if (!SmtUtils.isNNF(disjunct) || SmtUtils.containsFunctionApplication(disjunct, "or")) {
+				throw new AssertionError("the code below only works for conjunctive formulas");
+			}
+
+			final Term disjunctWithLocUpdatesAndLocInitialization;
+			{
+				final Set<TermVariable> unconstrainedVars = mEdgeToUnconstrainedVars.getImage(edgeInfo);
+				final List<Term> tfWithUpdatesAndInitConjuncts = new ArrayList<>();
+				tfWithUpdatesAndInitConjuncts.add(transitionFormulaWithLocUpdates);
+				for (final TermVariable ucv : unconstrainedVars) {
+					final MultiDimensionalSort mds = new MultiDimensionalSort(ucv.getSort());
+					final int dimensionality = mds.getDimension();
+					assert dimensionality > 0;
+					for (int dim = 1; dim <= dimensionality; dim++) {
+						final LocArrayInfo locArray = mLocArrayManager.getOrConstructLocArray(edgeInfo, ucv, dim);
+						final Term initConjunct = SmtUtils.binaryEquality(mMgdScript.getScript(),
+								locArray.getTerm(),
+								locArray.getInitializingConstantArray());
+						//							mLocArrayManager.getInitConstantArrayForLocArray(locArray));
+						tfWithUpdatesAndInitConjuncts.add(initConjunct);
+					}
 				}
+				disjunctWithLocUpdatesAndLocInitialization =
+						SmtUtils.and(mMgdScript.getScript(), tfWithUpdatesAndInitConjuncts);
 			}
-			transitionFormulaWithLocUpdatesAndLocInitialization =
-					SmtUtils.and(mMgdScript.getScript(), tfWithUpdatesAndInitConjuncts);
+			disjunctsWithLocUpdatesAndLocInitialization.add(disjunctWithLocUpdatesAndLocInitialization);
 		}
+		final Term transitionFormulaWithLocUpdatesAndLocInitialization =
+				SmtUtils.or(mMgdScript.getScript(), disjunctsWithLocUpdatesAndLocInitialization);
 
 		final Map<IProgramVar, TermVariable> newInVars;
 		{