PLA: Started optimized implementation of product-line analysis

Started optimized implementation with collection of relevant objects.

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

+package org.fortiss.variability.analysis;
+
+import static java.util.stream.Collectors.toList;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.calculateGlobalPresenceCondition;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.getChildrenWithType;
+import static org.fortiss.variability.util.VariabilityUtilsInternal.getContainedSuperClass;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EAttribute;
+import org.eclipse.emf.ecore.EClass;
+import org.eclipse.emf.ecore.EDataType;
+import org.eclipse.emf.ecore.EEnum;
+import org.eclipse.emf.ecore.EEnumLiteral;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EReference;
+import org.eclipse.emf.ecore.EcorePackage;
+import org.fortiss.variability.model.IVariationPoint;
+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;
+import org.fortiss.variability.model.presence.AndPC;
+import org.fortiss.variability.model.presence.DefaultPC;
+import org.fortiss.variability.model.presence.ILiteralReferencable;
+import org.fortiss.variability.model.presence.LiteralPC;
+import org.fortiss.variability.model.presence.NotPC;
+import org.fortiss.variability.model.presence.OrPC;
+import org.fortiss.variability.model.presence.PresenceCondition;
+import org.fortiss.variability.model.presence.PresenceConditionTerm;
+
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.BoolSort;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.EnumSort;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.FuncDecl;
+import com.microsoft.z3.IntSort;
+import com.microsoft.z3.SeqExpr;
+import com.microsoft.z3.SeqSort;
+import com.microsoft.z3.Solver;
+import com.microsoft.z3.Sort;
+import com.microsoft.z3.StringSymbol;
+import com.microsoft.z3.Symbol;
+
+/**
+ * Base class that implements the translation of model product-lines to SMT in order to perform
+ * product-line analysis via constraint lifting.
+ * 
+ * @author bayha
+ */
+public class EMFProductLineTranslation {
+
+	/** Z3 sort for base type integer. */
+	protected IntSort intSort;
+	/** Z3 sort for base type string. */
+	protected SeqSort stringSort;
+	/** Z3 sort for base type boolean. */
+	protected BoolSort boolSort;
+
+	/** Mapping from classes to all their objects */
+	protected BucketSetMap<EClass, EObject> allObjects = new BucketSetMap<EClass, EObject>();
+	/** Mapping from classes to all their subclasses */
+	protected BucketSetMap<EClass, EClass> allSubclasses = new BucketSetMap<EClass, EClass>();
+
+	/** Classes which are not supposed to be translated (usually for optimization). */
+	protected Set<EClass> excludedClasses = new HashSet<EClass>();
+	/** References which are not supposed to be translated (usually for optimization). */
+	protected Set<EReference> excludedReferences = new HashSet<EReference>();
+	/** Mapping from classes to all attributes of the respective type. */
+	protected BucketSetMap<EClass, EAttribute> translatedAttributes =
+			new BucketSetMap<EClass, EAttribute>();
+	/** Mapping from classes to all references of the respective type. */
+	protected BucketSetMap<EClass, EReference> translatedReferences =
+			new BucketSetMap<EClass, EReference>();
+	/** 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. */
+	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> eClass2Datatype = new HashMap<EClass, EnumSort>();
+
+	/** Mapping of class.reference to the respective z3 function. */
+	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).
+	 */
+	protected DualKeyMap<EObject, EClass, Expr> eObject2Expr =
+			new DualKeyMap<EObject, EClass, Expr>();
+
+	protected Map<Expr, EObject> expr2EObject = new HashMap<Expr, EObject>();
+
+	/** 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. */
+	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>();
+	/** Mapping of objects to their presence conditions. */
+	protected Map<EObject, BoolExpr> eObject2Selection = new HashMap<EObject, BoolExpr>();
+
+	/** {@link Context} to capture the translated model. */
+	protected Context ctx = new Context();
+
+	/** List of all translated assertions for the model. */
+	protected List<BoolExpr> modelAssertions = new ArrayList<BoolExpr>();
+	/** List of all assertions for the feature model. */
+	protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
+	/** List of all assertions which encode the presence conditions. */
+	protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
+
+	/* Refacting */
+
+	protected Set<Class<? extends EObject>> translatedClasses;
+	protected Set<EReference> translatedRefernces;
+	protected Set<EObject> translatedObjects;
+	protected BucketSetMap<Class<? extends EObject>, EObject> class2TranslatedEObjects;
+
+	/**
+	 * Constructor.
+	 */
+	protected EMFProductLineTranslation() {
+		initialize();
+	}
+
+	/**
+	 * Initialization of analysis and base types.
+	 */
+	private void initialize() {
+		intSort = ctx.mkIntSort();
+		stringSort = ctx.mkStringSort();
+		boolSort = ctx.mkBoolSort();
+
+		eDataType2Sort.put(EcorePackage.Literals.EINT, intSort);
+		eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
+		eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
+
+		class2TranslatedEObjects = new BucketSetMap<Class<? extends EObject>, EObject>();
+	}
+
+	/** Performs the complete translation of the product-line to Z3. */
+	/* package */ void doTranslate(EObject model) {
+		// Prepare the core translation
+		setTranslatedClassesAndReferences();
+
+		translateFeatureModel(model);
+		collectTranslatedObjects(model);
+
+		// Metamodel translation
+		translateClassesMetamodel();
+		translateAttributesAndReferencesMetamodel();
+
+		// Translate variability
+		translatePresenceConditions();
+
+		// Model translation
+		translateObjects();
+	}
+
+	/**
+	 * TODO
+	 * 
+	 * @param model
+	 */
+	private void collectTranslatedObjects(EObject model) {
+
+		EList<? extends EObject> varModelElements = getVariableModelElements(model);
+		for(EObject eo : varModelElements) {
+			Class<? extends EObject> eoClass = eo.getClass();
+			if(translatedClasses.contains(eoClass)) {
+				collectEObject(eo, eoClass);
+
+				continue;
+			}
+
+			for(Class<? extends EObject> t : translatedClasses) {
+				if(t.isAssignableFrom(eoClass)) {
+					collectEObject(eo, t);
+				}
+			}
+		}
+	}
+
+	/**
+	 * @param eo
+	 */
+	private void collectEObject(EObject eo, Class<? extends EObject> cls) {
+		class2TranslatedEObjects.add(cls, eo);
+
+		for(EReference ref : eo.eClass().getEAllReferences()) {
+			if(translatedRefernces.contains(ref)) {
+				Object refTarget = eo.eGet(ref);
+				if(refTarget instanceof EObject) {
+					EObject refEObj = (EObject)refTarget;
+
+					Class<? extends EObject> refClass = refEObj.getClass();
+					if(translatedClasses.contains(refClass)) {
+						collectEObject(refEObj, refClass);
+
+						continue;
+					}
+
+					Class<? extends EObject> translRefCls =
+							getContainedSuperClass(refClass, translatedClasses);
+					if(translRefCls != null) {
+						collectEObject(eo, translRefCls);
+					} else {
+						throw new RuntimeException("Invalid reference target class found. Class " +
+								refClass.getCanonicalName() + " is not translated.");
+					}
+				}
+
+			}
+		}
+	}
+
+	/**
+	 * @param model
+	 */
+	protected EList<? extends EObject> getVariableModelElements(EObject model) {
+		return getChildrenWithType(model, IVariationPoint.class);
+	}
+
+	/**
+	 * TODO
+	 */
+	protected void setTranslatedClassesAndReferences() {
+		// EMPTY
+	}
+
+	/** Translates the presence conditions to Z3. */
+	protected void translatePresenceConditions() {
+		for(EClass ec : allObjects.keySet()) {
+			EnumSort ecSort = eClass2Datatype.get(ec);
+			FuncDecl selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
+			eClass2SelectionFunction.put(ec, selFun);
+
+			for(EObject eo : allObjects.get(ec)) {
+				BoolExpr eoSelection = eObject2Selection.get(eo);
+
+				// If there is no PC term yet, create one
+				if(eoSelection == null) {
+					final PresenceConditionTerm globalPC = getGlobalPresenceConditionForEObject(eo);
+					eoSelection = translatePresenceCondition(globalPC);
+					if(eoSelection == null) {
+						eoSelection = ctx.mkTrue();
+					}
+					eObject2Selection.put(eo, eoSelection);
+				}
+
+				Expr eoExpr = eObject2Expr.get(eo, ec);
+				presenceConditionAssertions.add(ctx.mkEq(ctx.mkApp(selFun, eoExpr), eoSelection));
+			}
+		}
+	}
+
+	/**
+	 * Calculates the global presence condition for any given {@link EObject}.
+	 * 
+	 * This method might be overwritten if necessary for custom variation point implementations.
+	 */
+	protected PresenceConditionTerm getGlobalPresenceConditionForEObject(EObject eo) {
+		return calculateGlobalPresenceCondition(eo);
+	}
+
+	/** Translates a given {@link PresenceCondition} to Z3. */
+	private BoolExpr translatePresenceCondition(PresenceCondition pc) {
+		if(pc == null) {
+			return null;
+		}
+
+		if(pc instanceof LiteralPC) {
+			ILiteralReferencable literal = ((LiteralPC)pc).getLiteralReference();
+			if(literal == null || literal.getName().length() == 0) {
+				// Illegal literals are translated as true.
+				return ctx.mkTrue();
+			}
+			return featureName2BoolExpr.get(literal.getName());
+		}
+
+		if(pc instanceof DefaultPC) {
+			return translatePresenceCondition(pc.resolveToFeatureLiterals());
+		}
+
+		if(pc instanceof OrPC) {
+			PresenceConditionTerm op1 = ((OrPC)pc).getOperand1();
+			PresenceConditionTerm op2 = ((OrPC)pc).getOperand2();
+			return ctx.mkOr(translatePresenceCondition(op1), translatePresenceCondition(op2));
+		}
+
+		if(pc instanceof AndPC) {
+			PresenceConditionTerm op1 = ((AndPC)pc).getOperand1();
+			PresenceConditionTerm op2 = ((AndPC)pc).getOperand2();
+			return ctx.mkAnd(translatePresenceCondition(op1), translatePresenceCondition(op2));
+		}
+
+		if(pc instanceof NotPC) {
+			return ctx.mkNot(translatePresenceCondition(((NotPC)pc).getOperand()));
+		}
+
+		logError("Unknown PresenceCondition: " + pc);
+		return null;
+	}
+
+	/** Overwrite to exclude classes from the translation for optimization purposes. */
+	protected void excludeClassesAndReferences() {
+		// EMPTY
+	}
+
+	/** Translates the feature model to Z3. */
+	protected void translateFeatureModel(EObject model) {
+		// FIXME: Optimize!
+		EList<AbstractFeatureModel> featureModels =
+				getChildrenWithType(model, AbstractFeatureModel.class);
+
+		if(featureModels.size() == 0) {
+			return;
+		}
+
+		// There can only be one FeatureModel in any project.
+		AbstractFeatureModel fm = featureModels.get(0);
+
+		BoolExpr fmExpr = ctx.mkBoolConst("FEATURE_" + fm.getName());
+		featureName2BoolExpr.put(fm.getName(), fmExpr);
+
+		featureModelAssertions.add(fmExpr);
+
+		// Translate all features (including alternatives)
+		for(AbstractFeature f : getChildrenWithType(fm, AbstractFeature.class)) {
+			String name = f.getName();
+			String constName = "FEATURE_" + name;
+			final BoolExpr fExpr = ctx.mkBoolConst(constName.replaceAll("@", "AT"));
+			featureName2BoolExpr.put(name, 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());
+
+				if(f.isOptional()) {
+					featureModelAssertions.add(ctx.mkImplies(fExpr, parentExpr));
+				} else {
+					if(fContainer instanceof AbstractCompositionalFeature) {
+						featureModelAssertions.add(ctx.mkImplies(parentExpr, fExpr));
+					}
+				}
+			}
+		}
+
+		// For alternatives also translate the alternative selection criteria
+		for(AbstractAlternativeFeature af : getChildrenWithType(fm,
+				AbstractAlternativeFeature.class)) {
+			BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
+			EList<AbstractFeature> as = af.getAlternatives();
+
+			featureModelAssertions.add(ctx.mkImplies(afExpr,
+					ctx.mkOr(as.stream().map(alt -> featureName2BoolExpr.get(alt.getName()))
+							.collect(toList()).toArray(new BoolExpr[0]))));
+
+			for(AbstractFeature a : as) {
+				BoolExpr aExpr = featureName2BoolExpr.get(a.getName());
+				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]))));
+			}
+		}
+
+		// Translate all constraints.
+		for(AbstractCrossFeatureConstraint c : getChildrenWithType(fm,
+				AbstractCrossFeatureConstraint.class)) {
+			AbstractFeature target = c.getTarget();
+			AbstractFeature source = (AbstractFeature)c.eContainer();
+
+			BoolExpr srcExpr = featureName2BoolExpr.get(source.getName());
+			BoolExpr trgExpr = featureName2BoolExpr.get(target.getName());
+
+			switch(c.getType()) {
+				case REQUIRES:
+					featureModelAssertions.add(ctx.mkImplies(srcExpr, trgExpr));
+					break;
+				case EXCLUDES:
+					featureModelAssertions.add(ctx.mkImplies(srcExpr, ctx.mkNot(trgExpr)));
+					break;
+				default: // Suggestions are not translated.
+			}
+		}
+	}
+
+	/** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
+	// protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
+
+	/** Creates and initializes the Z3 solver to be used for analyis. */
+	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(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;
+	}
+
+	/** Translates all objects in the model. */
+	private void translateObjects() {
+		// Translate objects by class.
+		for(EClass ec : allObjects.keySet()) {
+			Set<EObject> Objs = allObjects.get(ec);
+
+			Set<EAttribute> attributes = translatedAttributes.get(ec);
+			if(attributes != null) {
+				for(EAttribute ea : attributes) {
+					FuncDecl attFunc = eAttribute2FunDecl.get(ea, ec);
+
+					for(EObject eo : Objs) {
+						Expr attVal = translateAttributeValue(eo, ea);
+						BoolExpr attValAssertion =
+								ctx.mkEq(ctx.mkApp(attFunc, eObject2Expr.get(eo, ec)), attVal);
+						modelAssertions.add(attValAssertion);
+					}
+				}
+			}
+
+			Set<EReference> references = translatedReferences.get(ec);
+			if(references != null) {
+				for(EReference er : references) {
+					FuncDecl refFunc = eReference2FunDecl.get(er, ec);
+					for(EObject eo : Objs) {
+						Expr eoExpr = eObject2Expr.get(eo, ec);
+						Expr refVal = translateReferenceValue(eo, er);
+						BoolExpr rafValAssertion = ctx.mkEq(ctx.mkApp(refFunc, eoExpr), refVal);
+						modelAssertions.add(rafValAssertion);
+					}
+
+					// Null must always only point to null....
+					EClass refType = er.getEReferenceType();
+					Expr nullElement = eClass2NullElement.get(ec);
+					if(er.getUpperBound() > 0) {
+						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))));
+					}
+				}
+			}
+		}
+	}
+
+	/** Translates the given instance of a relation between individual objects in the model. */
+	private Expr translateReferenceValue(EObject eo, EReference er) {
+		Object value = eo.eGet(er);
+		EClass refType = er.getEReferenceType();
+		Expr refNullValue = eClass2NullElement.get(refType);
+
+		FuncDecl refSelFun = eClass2SelectionFunction.get(er.getEType());
+
+		if(er.getUpperBound() < 0) {
+			// Case for lists
+			List<?> values = (List<?>)value;
+
+			if(values.size() == 0) {
+				return ctx.mkEmptySeq(eReference2Sort.get(er));
+			}
+
+			// Remove objects of untranslated objects.
+			values = values.stream().filter(o -> !excludedClasses.contains(((EObject)o).eClass()))
+					.collect(toList());
+
+			SeqExpr[] seqElems = new SeqExpr[values.size()];
+			for(int i = 0; i < values.size(); i++) {
+				Object o = values.get(i);
+
+				Expr elemExpr = eObject2Expr.get((EObject)o, refType);
+
+				SeqExpr selectedExpr = ctx.mkUnit(elemExpr);
+				if(refSelFun != null) {
+					SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReference2Sort.get(er));
+					seqElems[i] = (SeqExpr)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
+							selectedExpr, notSelectedExpr);
+				} else {
+					seqElems[i] = selectedExpr;
+				}
+			}
+
+			if(seqElems.length == 0) {
+				return ctx.mkEmptySeq(eReference2Sort.get(er));
+			}
+			if(seqElems.length == 1) {
+				return seqElems[0];
+			}
+			return ctx.mkConcat(seqElems);
+		}
+
+		if(value == null) {
+			return refNullValue;
+		}
+
+		Expr singleValExpr = eObject2Expr.get((EObject)value, refType);
+
+		if(refSelFun != null) {
+			// Case with variable target
+			BoolExpr eoSel = (BoolExpr)ctx.mkApp(refSelFun, singleValExpr);
+
+			return ctx.mkITE(eoSel, singleValExpr, refNullValue);
+		}
+
+		// Default case with non variable target.
+		return singleValExpr;
+	}
+
+	/** Creates a function call with the given expression as a parameter. */
+	protected Expr createFunctionCallOnExpr(Expr startExpr, String funName, EClass startExprType) {
+		FuncDecl fun = attRefNames2FuncDecl.get(startExprType, funName);
+		return ctx.mkApp(fun, startExpr);
+	}
+
+	/**
+	 * Creates a containment reference between the given expressions, analogly to the containment in
+	 * EMF.
+	 */
+	protected BoolExpr createContainmentReference(Expr contained, Expr container,
+			EClass containerType, String refName) {
+		SeqExpr contRefExpr = (SeqExpr)createFunctionCallOnExpr(container, refName, containerType);
+		// return ctx.mkAnd(ctx.mkNot(ctx.mkEq(ctx.mkLength(contRefExpr), ctx.mkInt(0))),
+		// ctx.mkContains(contRefExpr, ctx.mkUnit(contained)));
+		return ctx.mkContains(contRefExpr, ctx.mkUnit(contained));
+	}
+
+	/** Translates the given EAttribute value for the given object to Z3. */
+	private Expr translateAttributeValue(EObject eo, EAttribute ea) {
+		Object value = eo.eGet(ea);
+		EDataType attType = ea.getEAttributeType();
+
+		if(ea.getUpperBound() < 0 && value instanceof List<?>) {
+			// Case for lists.
+			List<?> values = (List<?>)value;
+
+			SeqExpr[] seqElem = new SeqExpr[values.size()];
+			for(int i = 0; i < values.size(); i++) {
+				Object o = values.get(i);
+				Expr elemExpr = traslatePrimitiveObject(o, attType);
+
+				seqElem[i] = ctx.mkUnit(elemExpr);
+			}
+
+			return ctx.mkConcat(seqElem);
+		}
+
+		return traslatePrimitiveObject(value, attType);
+	}
+
+	/** Translates the given object for a primitive type (Enums, Integer, String, Boolean) to Z3. */
+	private Expr traslatePrimitiveObject(Object value, EDataType attType) {
+		// Single value
+		if(attType.equals(EcorePackage.Literals.EINT)) {
+			if(value == null) {
+				logError("null int found");
+				return ctx.mkInt(0);
+			}
+			return ctx.mkInt((int)value);
+		}
+		if(attType.equals(EcorePackage.Literals.ESTRING)) {
+			if(value == null) {
+				return ctx.mkString("");
+			}
+			return ctx.mkString((String)value);
+		}
+		if(attType.equals(EcorePackage.Literals.EBOOLEAN)) {
+			if(value == null) {
+				logError("null bool found");
+				return ctx.mkBool(false);
+			}
+			return ctx.mkBool((boolean)value);
+		}
+		if(attType instanceof EEnum) {
+			if(value == null) {
+				return eEnum2NullElement.get(attType);
+			}
+			return eLiteral2Expr.get(value);
+		}
+
+		return null;
+	}
+
+	/** Creates functions for all attributes and references of the meta model in Z3. */
+	private void translateAttributesAndReferencesMetamodel() {
+		for(EClass ec : allObjects.keySet()) {
+			for(EAttribute ea : ec.getEAllAttributes()) {
+				String funId = ec.getName() + "_" + ea.getName();
+
+				EDataType attDataType = ea.getEAttributeType();
+				Sort rangeSort = eDataType2Sort.get(attDataType);
+				if(attDataType instanceof EEnum) {
+					if(rangeSort == null) {
+						rangeSort = translateEnum((EEnum)attDataType);
+						eDataType2Sort.put(attDataType, rangeSort);
+					}
+				}
+
+				if(rangeSort == null) {
+					// Attribute is not translated, as all attribute types except enums are known.
+					continue;
+				}
+
+				FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2Datatype.get(ec), rangeSort);
+
+				eAttribute2FunDecl.put(ea, ec, funDecl);
+				translatedAttributes.add(ec, ea);
+				attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
+			}
+			for(EReference er : ec.getEAllReferences()) {
+				String funId = ec.getName() + "_" + er.getName();
+
+				EClass refType = er.getEReferenceType();
+
+				Sort refSort = eClass2Datatype.get(refType);
+				if(refSort == null) {
+					if(!isReferenceTranslated(er)) {
+						// This is the case in which a custom instance class is specified - those
+						// cannot
+						// be translated.
+						continue;
+					}
+
+					refSort = translateSuperType(refType);
+					if(refSort == null) {
+						// There are no instances of this type...
+						continue;
+					}
+				}
+
+				FuncDecl funDecl;
+
+				if(er.getUpperBound() < 0) {
+					// This is the case of unlimited multiplicity
+					refSort = ctx.mkSeqSort(refSort);
+				}
+
+				funDecl = ctx.mkFuncDecl(funId, eClass2Datatype.get(ec), refSort);
+
+				eReference2Sort.put(er, refSort);
+				eReference2FunDecl.put(er, ec, funDecl);
+				translatedReferences.add(ec, er);
+				attRefNames2FuncDecl.put(ec, er.getName(), funDecl);
+			}
+		}
+	}
+
+	/** Checks whether the given reference is supposed to be translated. */
+	private boolean isReferenceTranslated(EReference ref) {
+		if(excludedReferences.contains(ref)) {
+			return false;
+		}
+
+		EClass refType = ref.getEReferenceType();
+		if(excludedClasses.contains(refType)) {
+			excludedReferences.add(ref);
+			// References to excluded classes not translated.
+			return false;
+		}
+
+		// Only EObjects are translated.
+		boolean isTranslated = EObject.class.isAssignableFrom(refType.getInstanceClass());
+		return isTranslated;
+	}
+
+	/**
+	 * Translates the given superType by adding all objects to it, that belong to
+	 * subtypes.
+	 */
+	private EnumSort translateSuperType(EClass refType) {
+		Set<EClass> subClasses = allSubclasses.get(refType);
+		if(subClasses == null) {
+			// There are no objects of this class in this case, hence it is not relevant.
+			return null;
+		}
+
+		String typeName = refType.getName();
+
+		List<EObject> subClassObjects = new ArrayList<EObject>();
+		for(EClass subCls : subClasses) {
+			if(excludedClasses.contains(subCls)) {
+				// If subclass is excluded, it must not be added here, either.
+				continue;
+			}
+			subClassObjects.addAll(allObjects.get(subCls));
+		}
+
+		Symbol[] allSymbols = new Symbol[subClassObjects.size()];
+		for(int i = 0; i < subClassObjects.size(); i++) {
+			StringSymbol symbol = ctx.mkSymbol(typeName + i);
+
+			allSymbols[i] = symbol;
+		}
+
+		EnumSort sort = ctx.mkEnumSort(ctx.mkSymbol(typeName), allSymbols);
+		eClass2Datatype.put(refType, sort);
+
+		return sort;
+	}
+
+	/** Translates the give enumeration */
+	private Sort translateEnum(EEnum en) {
+		String name = en.getName();
+		EList<EEnumLiteral> enumLiterals = en.getELiterals();
+
+		// Null needs to be encoded as a dedicated literal
+		int numLiterals = enumLiterals.size();
+		String[] literals = new String[numLiterals + 1];
+		for(int i = 0; i < numLiterals; i++) {
+			literals[i] = name + "_" + enumLiterals.get(i).getName();
+		}
+		literals[numLiterals] = name + "_NONE_LITERAL";
+
+		EnumSort enumSort = ctx.mkEnumSort(name, literals);
+
+		// Add regular literals and null literal to the respective mappings.
+		for(int i = 0; i < numLiterals; i++) {
+			eLiteral2Expr.put((Enum<?>)enumLiterals.get(i).getInstance(), enumSort.getConst(i));
+		}
+		eEnum2NullElement.put(en, enumSort.getConst(numLiterals));
+
+		return enumSort;
+	}
+
+	/** Creates the types for all classes and objects in Z3. */
+	private void translateClassesMetamodel() {
+		for(EClass cls : allObjects.keySet()) {
+			List<EObject> objs = new ArrayList<EObject>(allObjects.get(cls));
+
+			// The last index is added for the null element.
+			Symbol[] objSymbols = new Symbol[objs.size() + 1];
+			String clsName = cls.getName();
+			for(int i = 0; i < objs.size(); i++) {
+				String id = clsName + i;
+
+				StringSymbol objSymbol = ctx.mkSymbol(id);
+				objSymbols[i] = objSymbol;
+			}
+			objSymbols[objs.size()] = ctx.mkSymbol(clsName + "NONE");
+
+			// Create EnumSort for class
+			EnumSort enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
+			eClass2Datatype.put(cls, enumSort);
+
+			// Map objects to z3 enum literals
+			Expr[] consts = enumSort.getConsts();
+			for(int i = 0; i < objs.size(); i++) {
+				eObject2Expr.put(objs.get(i), cls, consts[i]);
+				expr2EObject.put(consts[i], objs.get(i));
+			}
+			Expr noneExpr = consts[consts.length - 1];
+			eClass2NullElement.put(cls, noneExpr);
+		}
+	}
+
+	/** Logs an error in the translation. */
+	private void logError(String message) {
+		// FIXME //error(getDefault(), "Error in product-line translation: " + message);
+	}
+
+	/**
+	 * Checks whether any of the elements in the given {@link Collection} is contained in the given
+	 * set of elements.
+	 * 
+	 * @param set
+	 *            The {@link Set} to check for containment.
+	 * @param elements
+	 *            The {@link Collection} of elements to be checked for containment in the set.
+	 * 
+	 * @return 'true' if at least one of the elements on the given {@link Collection} is contained
+	 *         in the given {@link Set}.
+	 */
+	public <E> boolean containsAny(Set<E> set, Collection<E> elements) {
+		for(E e : elements) {
+			if(set.contains(e)) {
+				return true;
+			}
+		}
+		return false;
+	}
+
+	/**
+	 * @param clss
+	 */
+	public void addExcludedClasses(Collection<EClass> clss) {
+		this.excludedClasses.addAll(clss);
+	}
+
+	/** Returns ctx. */
+	public Context getContext() {
+		return ctx;
+	}
+
+	/** Returns eClass2NullElement. */
+	public Map<EClass, Expr> getEClass2NullElement() {
+		return eClass2NullElement;
+	}
+
+	/** Traverses the model to collect all classes and objects to be translated. */
+	private void collectClassesAndObjectsRecrsively(EObject model) {
+		EClass eClass = model.eClass();
+		EList<EClass> superTypes = eClass.getEAllSuperTypes();
+
+		if(excludedClasses.contains(eClass)) {
+			return;
+		}
+
+		if(containsAny(excludedClasses, superTypes)) {
+			excludedClasses.add(eClass);
+			return;
+		}
+
+		for(EClass sprCls : superTypes) {
+			if(!sprCls.equals(EcorePackage.Literals.EOBJECT)) {
+				allObjects.add(sprCls, model);
+				allSubclasses.add(sprCls, eClass);
+			}
+		}
+
+		allObjects.add(eClass, model);
+
+		for(EObject c : model.eContents()) {
+			collectClassesAndObjectsRecrsively(c);
+		}
+	}
+}

org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java

@@ -26,6 +26,7 @@ import java.util.LinkedList;
 import java.util.List;
 import java.util.Map;
 import java.util.Queue;
+import java.util.Set;
 import java.util.function.Predicate;
 
 import org.eclipse.emf.common.util.BasicEList;
@@ -261,4 +262,15 @@ public class VariabilityUtilsInternal {
 
 		return rest;
 	}
+
+	public static Class<? extends EObject> getContainedSuperClass(Class<?> subCls,
+			Set<Class<? extends EObject>> clss) {
+		for(Class<? extends EObject> t : clss) {
+			if(t.isAssignableFrom(subCls)) {
+				return t;
+			}
+		}
+
+		return null;
+	}
 }