Variability: Fixed issue with translation of AlternativeFeatures

Alternative features were not translated correctly to SMT for the
product-line analysis.

Issue-ref: 4240
Issue-Url: af3#4240



Signed-off-by: Andreas Bayha <bayha@fortiss.org>

org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java

@@ -74,6 +74,8 @@ public class GenericProductLineAnalysis {
 
 		addRawConstraints();
 
+		// Global.setParameter("parallel.enable", "true");
+
 		Solver solver = getSolver();
 
 		String modelName = ((INamedElement)model).getName();
@@ -109,7 +111,7 @@ public class GenericProductLineAnalysis {
 			//
 			// try {
 			// printWriter = new PrintWriter(
-			// "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "out");
+			// "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "unsat");
 			//
 			// for(BoolExpr b : unsatCore) {
 			// BoolExpr coreExpr = tracToExpr.get(b);
@@ -122,7 +124,7 @@ public class GenericProductLineAnalysis {
 			// // TODO Auto-generated catch block
 			// e.printStackTrace();
 			// }
-			//
+
 			// System.out.println(deepToString(unsatCore));
 		} else {
 
@@ -172,7 +174,7 @@ public class GenericProductLineAnalysis {
 
 	/** gets the Z3 solver to be used for analysis and adds all constraints. */
 	protected Solver getSolver() {
-		Solver solver = translation.createSolver();
+		Solver solver = translation.createSolver(tracToExpr);
 
 		if(rawConstraints.size() > 0) {
 			solver.add(rawConstraints.toArray(new BoolExpr[rawConstraints.size()]));

org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java

@@ -24,6 +24,7 @@ import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EReference;
 import org.eclipse.emf.ecore.EcorePackage;
 import org.fortiss.variability.model.features.AbstractAlternativeFeature;
+import org.fortiss.variability.model.features.AbstractCompositionalFeature;
 import org.fortiss.variability.model.features.AbstractCrossFeatureConstraint;
 import org.fortiss.variability.model.features.AbstractFeature;
 import org.fortiss.variability.model.features.AbstractFeatureModel;
@@ -300,6 +301,7 @@ public class GenericProductLineTranslation {
 
 	/** Translates the feature model to Z3. */
 	protected void translateFeatureModel(EObject model) {
+		// FIXME: Optimize!
 		EList<AbstractFeatureModel> featureModels =
 				getChildrenWithType(model, AbstractFeatureModel.class);
 
@@ -331,12 +333,14 @@ public class GenericProductLineTranslation {
 				if(f.isOptional()) {
 					featureModelAssertions.add(ctx.mkImplies(fExpr, parentExpr));
 				} else {
-					featureModelAssertions.add(ctx.mkImplies(parentExpr, fExpr));
+					if(fContainer instanceof AbstractCompositionalFeature) {
+						featureModelAssertions.add(ctx.mkImplies(parentExpr, fExpr));
+					}
 				}
 			}
 		}
 
-		// For alternatives also trabslate the alternative selection criteria
+		// For alternatives also translate the alternative selection criteria
 		for(AbstractAlternativeFeature af : getChildrenWithType(fm,
 				AbstractAlternativeFeature.class)) {
 			BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
@@ -378,26 +382,52 @@ public class GenericProductLineTranslation {
 	}
 
 	/** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
-	protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
+	// protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
 
 	/** Creates and initializes the Z3 solver to be used for analyis. */
-	protected Solver createSolver() {
-		Solver solver = ctx.mkSolver();
+	protected Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
+		Solver solver = ctx.mkSolver();// ctx.mkTactic("psmt"));
 
 		solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
 		solver.add(presenceConditionAssertions
 				.toArray(new BoolExpr[presenceConditionAssertions.size()]));
-		// solver.add(assertions.toArray(new BoolExpr[assertions.size()]));
-		BoolExpr[] assertionsArray = modelAssertions.toArray(new BoolExpr[modelAssertions.size()]);
-		List<BoolExpr> tracList = modelAssertions.stream()
-				.map(a -> ctx.mkBoolConst("tracVar" + a.getId())).collect(toList());
-		BoolExpr[] assertionsTracArray = tracList.toArray(new BoolExpr[modelAssertions.size()]);
-
-		for(int i = 0; i < modelAssertions.size(); i++) {
-			tracToExpr.put(tracList.get(i), modelAssertions.get(i));
-		}
-
-		solver.assertAndTrack(assertionsArray, assertionsTracArray);
+		solver.add(modelAssertions.toArray(new BoolExpr[modelAssertions.size()]));
+
+		//
+		// List<BoolExpr> tracFeaturesList = featureModelAssertions.stream()
+		// .map(a -> ctx.mkBoolConst("tracFeatureVar" + a.getId())).collect(toList());
+		//
+		// solver.assertAndTrack(
+		// featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]),
+		// tracFeaturesList.toArray(new BoolExpr[featureModelAssertions.size()]));
+
+		// for(int i = 0; i < featureModelAssertions.size(); i++) {
+		// tracToExpr.put(tracFeaturesList.get(i), featureModelAssertions.get(i));
+		// }
+		//
+		// List<BoolExpr> tracPresenceList = presenceConditionAssertions.stream()
+		// .map(a -> ctx.mkBoolConst("tracPresenceVar" + a.getId())).collect(toList());
+		//
+		// solver.assertAndTrack(
+		// presenceConditionAssertions
+		// .toArray(new BoolExpr[presenceConditionAssertions.size()]),
+		// tracPresenceList.toArray(new BoolExpr[presenceConditionAssertions.size()]));
+		//
+		// for(int i = 0; i < presenceConditionAssertions.size(); i++) {
+		// tracToExpr.put(tracPresenceList.get(i), presenceConditionAssertions.get(i));
+		// }
+
+		// BoolExpr[] assertionsArray = modelAssertions.toArray(new
+		// BoolExpr[modelAssertions.size()]);
+		// List<BoolExpr> tracList = modelAssertions.stream()
+		// .map(a -> ctx.mkBoolConst("tracModelVar" + a.getId())).collect(toList());
+		// BoolExpr[] assertionsTracArray = tracList.toArray(new BoolExpr[modelAssertions.size()]);
+		//
+		// for(int i = 0; i < modelAssertions.size(); i++) {
+		// tracToExpr.put(tracList.get(i), modelAssertions.get(i));
+		// }
+		//
+		// solver.assertAndTrack(assertionsArray, assertionsTracArray);
 
 		return solver;
 	}