Variability: Refactoring and clean-up of optimized EMF translation

Removed unused and commented out code. Added comments.

Issue-ref: 4240
Issue-URL: af3#4240



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

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

@@ -63,50 +63,28 @@ import com.microsoft.z3.Symbol;
  */
 public class EMFProductLineTranslation implements IProductLineTranslation {
 
-	/** Mapping of attributes to their translated Z3 function. */
+	/*
+	 * FIXME: These should be
+	 * easier now, since we do not translate objects for all inheritance levels. Multiple
+	 * properties??.
+	 */
+
+	/**
+	 * Mapping of attributes to their translated Z3 function.
+	 */
 	protected DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl =
 			new DualKeyMap<EAttribute, EClass, FuncDecl<?>>();
 	/** Mapping of references to their translated Z3 function. */
 	protected DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl =
 			new DualKeyMap<EReference, EClass, FuncDecl<?>>();
 
-	/** Mapping of references to the respective translated Z3 type. FIXME: Still required? */
-	protected Map<EReference, Sort> eReference2Sort = new HashMap<EReference, Sort>();
-
-	/** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
-	protected Map<EDataType, Sort> eDataType2Sort = new HashMap<EDataType, Sort>();
-	/** Mapping for classes to their respective Z3 type. */
-	protected Map<EClass, EnumSort<?>> eClass2z3Sort = new HashMap<EClass, EnumSort<?>>();
-
-	/** Mapping of class.reference to the respective z3 function. FIXME: REMOVE */
-	protected DualKeyMap<EClass, String, FuncDecl<?>> attRefNames2FuncDecl =
-			new DualKeyMap<EClass, String, FuncDecl<?>>();
-
 	/**
 	 * Mapping of objects with types to their translated Z3 expressions. (EClass is necessary as an
-	 * object is translated for all classes in the inheritance hierarchy). FIXME: This should be
-	 * easier now, since we do not translate objects for all inheritance levels. Multiple
-	 * properties??.
+	 * object is translated for all classes in the inheritance hierarchy).
 	 */
 	protected DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr =
 			new DualKeyMap<EObject, EClass, Expr<?>>();
 
-	/** Mapping of enumeration literals to the translated Z3 expression. */
-	protected Map<Enum<?>, Expr<?>> eLiteral2Expr = new HashMap<Enum<?>, Expr<?>>();
-	/** Mapping of classes to their respective z3 expression for 'null' */
-	protected Map<EClass, Expr<?>> eClass2NullElement = new HashMap<EClass, Expr<?>>();
-	/** Mapping of enumerations to their respective z3 expression for 'null' */
-	protected Map<EEnum, Expr<?>> eEnum2NullElement = new HashMap<EEnum, Expr<?>>();
-
-	/**
-	 * Mapping of feature names to corresponding Z3 Expr. FIXME: Is this still necessary? Feature
-	 * Ref should be okay.
-	 */
-	protected Map<String, BoolExpr> featureName2BoolExpr = new HashMap<String, BoolExpr>();
-	/** Mapping of classes to the selection function (lambda) for this type. */
-	protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction =
-			new HashMap<EClass, FuncDecl<?>>();
-
 	/* Refactoring */
 
 	/** {@link Context} to capture the translated model. */
@@ -120,13 +98,28 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	protected BoolSort boolSort;
 
 	/** List of all translated assertions for the model. */
-	protected List<BoolExpr> modelAssertions = new ArrayList<BoolExpr>();
+	protected List<BoolExpr> modelAssertions;
 	/** List of all assertions for the feature model. */
-	protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
+	protected List<BoolExpr> featureModelAssertions;
 	/** List of all assertions which encode the presence conditions. */
-	protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
+	protected List<BoolExpr> presenceConditionAssertions;
 	/** List of all assertions which encode the constraints. */
-	protected List<BoolExpr> constraintAssertions = new ArrayList<BoolExpr>();
+	protected List<BoolExpr> constraintAssertions;
+
+	/** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
+	protected Map<EDataType, Sort> eDataType2Sort;
+	/** Mapping for classes to their respective Z3 type. */
+	protected Map<EClass, EnumSort<?>> eClass2z3Sort;
+
+	/** Mapping of enumeration literals to the translated Z3 expression. */
+	protected Map<Enum<?>, Expr<?>> eLiteral2Expr;
+	/** Mapping of classes to their respective z3 expression for 'null' */
+	protected Map<EClass, Expr<?>> eClass2NullElement;
+	/** Mapping of enumerations to their respective z3 expression for 'null' */
+	protected Map<EEnum, Expr<?>> eEnum2NullElement;
+
+	/** Mapping of classes to the selection function for this type. */
+	protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction;
 
 	/** The set to specify all {@link EClass} to be translated by this translation. */
 	protected Set<EClass> translatedClasses;
@@ -135,12 +128,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	/** The set to specify all {@link EAttribute} to be translated by this translation. */
 	protected Set<EAttribute> translatedAttributes;
 
-	/** The set of all {@link EObject} that are collected by this translation to be translated. */
-	protected Set<EObject> translatedObjects;
 	/** The mapping of translated {@link EClass} to the objects that have been collected. */
 	protected BucketSetMap<EClass, EObject> class2TranslatedEObjects;
+
 	/** The {@link AbstractFeatureModel} collected by this translation */
 	protected AbstractFeatureModel featureModel;
+	/** Mapping of features to corresponding Z3 {@link BoolExpr}. */
+	protected Map<AbstractFeature, BoolExpr> feature2BoolExpr;
 
 	/** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */
 	protected Map<EObject, PresenceConditionTerm> object2presenceCondition;
@@ -171,7 +165,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	 * Constructor.
 	 */
 	public EMFProductLineTranslation() {
-		initialize();
+		// Fields which should not change between individual translations are initialized only once
+		translatedClasses = new HashSet<EClass>();
+		translatedReferences = new HashSet<EReference>();
+		translatedAttributes = new HashSet<EAttribute>();
 	}
 
 	/**
@@ -180,6 +177,27 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	private void initialize() {
 		ctx = new Context();
 
+		class2TranslatedEObjects = new BucketSetMap<EClass, EObject>();
+		object2presenceCondition = new HashMap<EObject, PresenceConditionTerm>();
+
+		reference2TranslatedEClass = new HashMap<EReference, EClass>();
+
+		modelAssertions = new ArrayList<BoolExpr>();
+		featureModelAssertions = new ArrayList<BoolExpr>();
+		presenceConditionAssertions = new ArrayList<BoolExpr>();
+		constraintAssertions = new ArrayList<BoolExpr>();
+
+		eDataType2Sort = new HashMap<EDataType, Sort>();
+		eClass2z3Sort = new HashMap<EClass, EnumSort<?>>();
+
+		eLiteral2Expr = new HashMap<Enum<?>, Expr<?>>();
+		eClass2NullElement = new HashMap<EClass, Expr<?>>();
+		eEnum2NullElement = new HashMap<EEnum, Expr<?>>();
+
+		eClass2SelectionFunction = new HashMap<EClass, FuncDecl<?>>();
+		feature2BoolExpr = new HashMap<AbstractFeature, BoolExpr>();
+
+		// Initialize model independent base types
 		intSort = ctx.mkIntSort();
 		stringSort = ctx.mkStringSort();
 		boolSort = ctx.mkBoolSort();
@@ -187,20 +205,17 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		eDataType2Sort.put(EcorePackage.Literals.EINT, intSort);
 		eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
 		eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
-
-		translatedClasses = new HashSet<EClass>();
-		translatedReferences = new HashSet<EReference>();
-		translatedAttributes = new HashSet<EAttribute>();
-
-		class2TranslatedEObjects = new BucketSetMap<EClass, EObject>();
-		object2presenceCondition = new HashMap<EObject, PresenceConditionTerm>();
-
-		reference2TranslatedEClass = new HashMap<EReference, EClass>();
 	}
 
 	/** {@inheritDoc} */
 	@Override
 	public final void translateModel(EObject model) {
+		// Initialize and reset local fields
+		initialize();
+
+		// Reference types need to be collected first, since they are required by optimizations in
+		// collectTranslatedObjects().
+		collectReferenceTypes();
 		collectTranslatedObjects(model, null);
 
 		translateFeatureModel();
@@ -216,6 +231,36 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		translatePresenceConditions();
 	}
 
+	/**
+	 * 
+	 */
+	private void collectReferenceTypes() {
+		for(EReference ref : translatedReferences) {
+			EClass refType = ref.getEReferenceType();
+
+			if(translatedClasses.contains(refType)) {
+				reference2TranslatedEClass.put(ref, refType);
+			} else {
+				// Find a super type of the reference class
+				for(EClass ecls : translatedClasses) {
+					if(ecls.isSuperTypeOf(refType)) {
+						reference2TranslatedEClass.put(ref, ecls);
+					} else if(refType.isSuperTypeOf(ecls)) {
+						// FIXME: Is this a good idea?
+						// Attempt to use nearest found class
+						reference2TranslatedEClass.put(ref, ecls);
+					}
+				}
+
+				// Check if any super type was found
+				if(reference2TranslatedEClass.get(ref) == null) {
+					throw new RuntimeException("ERefernce \"" + ref.getName() + "\" is of type " +
+							ref.getEReferenceType().getName() + " which is not translated.");
+				}
+			}
+		}
+	}
+
 	/**
 	 * @param model
 	 * @param parentCondition
@@ -251,6 +296,21 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		}
 	}
 
+	/**
+	 * @param eo
+	 * @param cls
+	 * @param pc
+	 */
+	private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
+		class2TranslatedEObjects.add(cls, eo);
+
+		if(isIslandOptimizationEnabled) {
+			collectTranslatedReferences(eo, islandOptimizationStepNum);
+		}
+
+		object2presenceCondition.put(eo, pc);
+	}
+
 	/**
 	 * @param model
 	 * @param remainingSteps
@@ -309,8 +369,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	}
 
 	/**
-	 * @param model
-	 * @return
+	 * Retrieves the {@link PresenceCondition} that was assigned to 'modelElement' in the model.
+	 * This function might be overwritten in case an alternative location for presence conditions
+	 * was defined.
 	 */
 	protected PresenceConditionTerm getLocalPresenceCondition(EObject model) {
 		if(model instanceof IOptionalVariationPoint<?>) {
@@ -330,62 +391,27 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		return null;
 	}
 
-	/**
-	 * @param eo
-	 * @param cls
-	 * @param pc
-	 */
-	private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
-		class2TranslatedEObjects.add(cls, eo);
-
-		if(isIslandOptimizationEnabled) {
-			collectTranslatedReferences(eo, islandOptimizationStepNum);
-		}
-
-		object2presenceCondition.put(eo, pc);
-	}
-
 	/** {@inheritDoc} */
 	@Override
 	public void setTranslatedEClasses(Collection<EClass> clss) {
+		translatedClasses.clear();
+
 		translatedClasses.addAll(clss);
 	}
 
 	/** {@inheritDoc} */
 	@Override
 	public void setTranslatedEReferences(Collection<EReference> refs) {
-		translatedReferences.addAll(refs);
-
-		for(EReference ref : refs) {
-			EClass refType = ref.getEReferenceType();
-
-			if(translatedClasses.contains(refType)) {
-				reference2TranslatedEClass.put(ref, refType);
-			} else {
-				// Find a super type of the reference class
-				for(EClass ecls : translatedClasses) {
-					if(ecls.isSuperTypeOf(refType)) {
-						reference2TranslatedEClass.put(ref, ecls);
-					} else if(refType.isSuperTypeOf(ecls)) {
-						// FIXME: Is this a good idea?
-						// Attempt to use nearest found class
-						reference2TranslatedEClass.put(ref, ecls);
-					}
-				}
-
-				// Check if any super type was found
-				if(reference2TranslatedEClass.get(ref) == null) {
-					throw new RuntimeException("ERefernce \"" + ref.getName() + "\" is of type " +
-							ref.getEReferenceType().getName() + " which is not translated.");
-				}
-			}
-		}
+		translatedReferences.clear();
 
+		translatedReferences.addAll(refs);
 	}
 
 	/** {@inheritDoc} */
 	@Override
 	public void setTranslatedEAttributes(Collection<EAttribute> atts) {
+		translatedAttributes.clear();
+
 		translatedAttributes.addAll(atts);
 	}
 
@@ -424,7 +450,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 				// Illegal literals are translated as true.
 				return ctx.mkTrue();
 			}
-			return featureName2BoolExpr.get(literal.getName());
+			return feature2BoolExpr.get(literal);
 		}
 
 		if(pc instanceof DefaultPC) {
@@ -458,7 +484,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		}
 
 		BoolExpr fmExpr = ctx.mkBoolConst("FEATURE_" + featureModel.getName());
-		featureName2BoolExpr.put(featureModel.getName(), fmExpr);
+		feature2BoolExpr.put(featureModel, fmExpr);
 
 		featureModelAssertions.add(fmExpr);
 
@@ -467,13 +493,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			String name = f.getName();
 			String constName = "FEATURE_" + name;
 			final BoolExpr fExpr = ctx.mkBoolConst(constName.replaceAll("@", "AT"));
-			featureName2BoolExpr.put(name, fExpr);
+			feature2BoolExpr.put(f, fExpr);
 
 			// If f is child of another feature, the selection criteria have to be encoded.
 			final EObject fContainer = f.eContainer();
 			if(fContainer instanceof AbstractFeature) {
 				AbstractFeature parentF = (AbstractFeature)fContainer;
-				final BoolExpr parentExpr = featureName2BoolExpr.get(parentF.getName());
+				final BoolExpr parentExpr = feature2BoolExpr.get(parentF);
 
 				if(f.isOptional()) {
 					featureModelAssertions.add(ctx.mkImplies(fExpr, parentExpr));
@@ -488,20 +514,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 		// For alternatives also translate the alternative selection criteria
 		for(AbstractAlternativeFeature af : getChildrenWithType(featureModel,
 				AbstractAlternativeFeature.class)) {
-			BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
+			BoolExpr afExpr = feature2BoolExpr.get(af);
 			EList<AbstractFeature> as = af.getAlternatives();
 
-			featureModelAssertions.add(ctx.mkImplies(afExpr,
-					ctx.mkOr(as.stream().map(alt -> featureName2BoolExpr.get(alt.getName()))
+			featureModelAssertions.add(
+					ctx.mkImplies(afExpr, ctx.mkOr(as.stream().map(alt -> feature2BoolExpr.get(alt))
 							.collect(toList()).toArray(new BoolExpr[0]))));
 
 			for(AbstractFeature a : as) {
-				BoolExpr aExpr = featureName2BoolExpr.get(a.getName());
+				BoolExpr aExpr = feature2BoolExpr.get(a);
 				featureModelAssertions.add(ctx.mkImplies(aExpr, afExpr));
 				featureModelAssertions.add(ctx.mkImplies(aExpr,
 						ctx.mkAnd(as.stream().filter(alt -> alt != a)
-								.map(alt -> ctx.mkNot(featureName2BoolExpr.get(alt.getName())))
-								.collect(toList()).toArray(new BoolExpr[0]))));
+								.map(alt -> ctx.mkNot(feature2BoolExpr.get(alt))).collect(toList())
+								.toArray(new BoolExpr[0]))));
 			}
 		}
 
@@ -511,8 +537,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			AbstractFeature target = c.getTarget();
 			AbstractFeature source = (AbstractFeature)c.eContainer();
 
-			BoolExpr srcExpr = featureName2BoolExpr.get(source.getName());
-			BoolExpr trgExpr = featureName2BoolExpr.get(target.getName());
+			BoolExpr srcExpr = feature2BoolExpr.get(source);
+			BoolExpr trgExpr = feature2BoolExpr.get(target);
 
 			switch(c.getType()) {
 				case REQUIRES:
@@ -528,7 +554,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 	/** Creates and initializes the Z3 solver to be used for analyis. */
 	@Override
-	public Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
+	public Solver createSolver() {
 		Solver solver = ctx.mkSolver();
 
 		solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
@@ -579,8 +605,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 						modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
 								eClass2NullElement.get(refType)));
 					} else {
-						modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
-								ctx.mkEmptySeq(eReference2Sort.get(er))));
+						modelAssertions
+								.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement), ctx.mkEmptySeq(
+										eClass2z3Sort.get(reference2TranslatedEClass.get(er)))));
 					}
 				}
 			}
@@ -601,7 +628,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			List<?> values = (List<?>)value;
 
 			if(values.size() == 0) {
-				return ctx.mkEmptySeq(eReference2Sort.get(er));
+				return ctx.mkEmptySeq(eReferenceToz3Sort(er));
 			}
 
 			SeqExpr[] seqElems = new SeqExpr[values.size()];
@@ -612,7 +639,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 				SeqExpr<?> selectedExpr = ctx.mkUnit(elemExpr);
 				if(refSelFun != null) {
-					SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReference2Sort.get(er));
+					SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReferenceToz3Sort(er));
 					seqElems[i] = (SeqExpr<?>)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
 							selectedExpr, notSelectedExpr);
 				} else {
@@ -621,7 +648,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 			}
 
 			if(seqElems.length == 0) {
-				return ctx.mkEmptySeq(eReference2Sort.get(er));
+				return ctx.mkEmptySeq(eReferenceToz3Sort(er));
 			}
 			if(seqElems.length == 1) {
 				return seqElems[0];
@@ -728,8 +755,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 					FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), rangeSort);
 
 					eAttribute2FunDecl.put(ea, ec, funDecl);
-					// eClass2TranslatedAttributes.add(ec, ea);
-					attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
 				}
 			}
 
@@ -764,10 +789,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 					FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), refSort);
 
-					eReference2Sort.put(er, refSort);
 					eReference2FunDecl.put(er, ec, funDecl);
-					// eclass2TranslatedReferences.add(ec, er);
-					attRefNames2FuncDecl.put(ec, er.getName(), funDecl);
 				}
 			}
 		}
@@ -872,8 +894,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 
 	/** {@inheritDoc} */
 	@Override
-	public FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass cVarType, String string) {
-		return attRefNames2FuncDecl.get(cVarType, string);
+	public FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass cVarType, String name) {
+		for(EReference ref : cVarType.getEAllReferences()) {
+			if(ref.getName().equals(name)) {
+				return eReference2FunDecl.get(ref, cVarType);
+			}
+		}
+
+		for(EAttribute att : cVarType.getEAllAttributes()) {
+			if(att.getName().equals(name)) {
+				return eAttribute2FunDecl.get(att, cVarType);
+			}
+		}
+
+		return null;
 	}
 
 	/** {@inheritDoc} */
@@ -950,4 +984,12 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
 	public void setIslandOptimizationStepNum(int islandOptimizationStepNum) {
 		this.islandOptimizationStepNum = islandOptimizationStepNum;
 	}
+
+	/**
+	 * @param er
+	 * @return
+	 */
+	private EnumSort<?> eReferenceToz3Sort(EReference er) {
+		return eClass2z3Sort.get(reference2TranslatedEClass.get(er));
+	}
 }

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

 package org.fortiss.variability.analysis;
 
 import static com.microsoft.z3.Status.UNSATISFIABLE;
-import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
-import static org.fortiss.variability.VariabilityActivator.getDefault;
 
 import java.io.FileNotFoundException;
 import java.io.PrintWriter;
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
@@ -20,9 +17,7 @@ import org.eclipse.emf.ecore.EReference;
 import org.fortiss.tooling.kernel.model.INamedElement;
 
 import com.microsoft.z3.BoolExpr;
-import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
-import com.microsoft.z3.FuncDecl;
 import com.microsoft.z3.Model;
 import com.microsoft.z3.Solver;
 import com.microsoft.z3.Status;
@@ -37,18 +32,10 @@ public abstract class GenericProductLineAnalysis {
 
 	protected final IProductLineTranslation translation;
 
-	/** List of all translated correctness constraints. */
-	protected List<BoolExpr> rawConstraints = new ArrayList<BoolExpr>();
-
 	protected List<IProductLineConstraint> plConstraints = new ArrayList<IProductLineConstraint>();
 
-	protected Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
-			new HashMap<BoolExpr, IProductLineConstraint>();
-
 	protected final EObject model;
 
-	protected Context ctx;
-
 	/**
 	 * Constructor.
 	 */
@@ -56,7 +43,6 @@ public abstract class GenericProductLineAnalysis {
 		this.model = model;
 
 		this.translation = translation;
-		ctx = translation.getContext();
 	}
 
 	/**
@@ -74,13 +60,14 @@ public abstract class GenericProductLineAnalysis {
 
 		translation.translateModel(model);
 
-		constraintTracker2Constraint = translation.translateConstraints(plConstraints);
+		Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
+				translation.translateConstraints(plConstraints);
 
 		// addRawConstraints();
 
 		// Global.setParameter("parallel.enable", "true");
 
-		Solver solver = translation.createSolver(tracToExpr);
+		Solver solver = translation.createSolver();
 
 		String modelName = ((INamedElement)model).getName();
 		String path = "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "in";
@@ -138,7 +125,7 @@ public abstract class GenericProductLineAnalysis {
 				Expr constInterp = z3Model.getConstInterp(constTrack);
 
 				if(constInterp instanceof BoolExpr) {
-					if(constInterp.equals(ctx.mkTrue())) {
+					if(constInterp.equals(translation.getContext().mkTrue())) {
 						IProductLineConstraint failedConstraint =
 								constraintTracker2Constraint.get(constTrack);
 
@@ -193,111 +180,5 @@ public abstract class GenericProductLineAnalysis {
 
 	}
 
-	/** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
-	protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
-
-	// /** gets the Z3 solver to be used for analysis and adds all constraints. */
-	// protected Solver getSolver() {
-	// Solver solver = translation.createSolver(tracToExpr);
-	//
-	// if(rawConstraints.size() > 0) {
-	// solver.add(rawConstraints.toArray(new BoolExpr[rawConstraints.size()]));
-	//
-	// Set<BoolExpr> constraintTrackerExprs = constraintTracker2Constraint.keySet();
-	// solver.add(translation.getContext().mkOr(
-	// constraintTrackerExprs.toArray(new BoolExpr[constraintTrackerExprs.size()])));
-	// }
-	// return solver;
-	// }
-
-	// /** Needs to be overwritten to add the constraints to be checked. */
-	// protected void addRawConstraints() {
-	// // EMPTY
-	// }
-	//
 	protected abstract void addConstriants();
-
-	protected void translateConstraints() {
-		// for(IProductLineConstraint constraint : plConstraints) {
-		// Expr[] quantifierValiables = constraint.getQuantifierVariables();
-		// EClass[] variableClasses = constraint.getVariablesClasses();
-		// BoolExpr[] containmentExprs = new BoolExpr[0];
-		// BoolExpr body = constraint.getBody();
-		//
-		// boolean isForAll = constraint.isForAll();
-		//
-		// BoolExpr quantifier = createLiftedConstraint(quantifierValiables, variableClasses,
-		// containmentExprs, body, isForAll);
-		//
-		// BoolExpr constraintTracker =
-		// ctx.mkBoolConst("CONSTRAINT_" + constraint.getConstraintName());
-		// constraintTracker2Constraint.put(constraintTracker, constraint);
-		//
-		// rawConstraints.add(ctx.mkEq(constraintTracker, quantifier));
-		// constraintTrackers.add(constraintTracker);
-		// }
-	}
-
-	/** Automatically lifts the given constraint */
-	protected BoolExpr liftConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
-			BoolExpr body, boolean isForAll) {
-		return createLiftedConstraint(quantifierValiables, variableClasses, new BoolExpr[0], body,
-				isForAll);
-	}
-
-	// protected BoolExpr createLiftedQuantifier(String[] quantifierValiableNames,
-	// EClass[] variableClasses, BoolExpr[] containmentExprs, BoolExpr body,
-	// boolean isForAll) {
-	//
-	// int numVar = quantifierValiableNames.length;
-	// Expr[] quantifierValiables = new Expr[numVar];
-	//
-	// for(int i = 0; i < numVar; i++) {
-	// EnumSort sort = translation.geteClass2Datatype().get(variableClasses[i]);
-	// Expr expr = ctx.mkConst(quantifierValiableNames[i], sort);
-	//
-	// quantifierValiables[i] = expr;
-	// }
-	//
-	// return createLiftedConstraint(quantifierValiables, variableClasses, containmentExprs, body,
-	// isForAll);
-	// }
-
-	/** Automatically lifts the given constraint */
-	protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
-			BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
-
-		BoolExpr[] selExprs = new BoolExpr[quantifierValiables.length + containmentExprs.length];
-		for(int i = 0; i < quantifierValiables.length; i++) {
-			EClass cls = variableClasses[i];
-			Expr var = quantifierValiables[i];
-
-			FuncDecl selFun = translation.getSelectionFunction(cls);
-			BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
-			BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, translation.getNullElement(cls)));
-
-			selExprs[i] = ctx.mkAnd(selected, notNull);
-		}
-
-		// Add containment expressions
-		int j = 0;
-		for(int i = quantifierValiables.length; i < quantifierValiables.length +
-				containmentExprs.length; i++) {
-			selExprs[i] = containmentExprs[j++];
-		}
-
-		if(isForAll) {
-			BoolExpr liftedBody = ctx.mkImplies(ctx.mkAnd(selExprs), body);
-			return ctx.mkForall(quantifierValiables, liftedBody, 0, null, null, null, null);
-		}
-
-		// else: Exits
-		BoolExpr liftedBody = ctx.mkAnd(ctx.mkAnd(selExprs), body);
-		return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
-	}
-
-	/** Logs an error in the analysis. */
-	private void logError(String message) {
-		error(getDefault(), "Error in product-line analysis: " + message);
-	}
 }

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

@@ -387,7 +387,7 @@ public class GenericProductLineTranslation implements IProductLineTranslation {
 	// protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
 
 	/** Creates and initializes the Z3 solver to be used for analyis. */
-	public Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
+	public Solver createSolver() {
 		Solver solver = ctx.mkSolver();// ctx.mkTactic("psmt"));
 
 		solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));

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

@@ -62,7 +62,7 @@ public interface IProductLineTranslation {
 	 * @param tracToExpr
 	 * @return
 	 */
-	Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr);
+	Solver createSolver();
 
 	/**
 	 * @param cls