From d840d3255832b48af4c5723f691d3a5811fff2e4 Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Mon, 3 Jul 2023 09:28:30 +0200
Subject: [PATCH] PLA: Started optimized implementation of product-line
analysis
Started optimized implementation with collection of relevant objects.
Issue-ref: 4240
Issue-URL: https://git.fortiss.org/af3/af3/-/issues/4240
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../analysis/EMFProductLineTranslation.java | 892 ++++++++++++++++++
.../util/VariabilityUtilsInternal.java | 12 +
2 files changed, 904 insertions(+)
create mode 100644 org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
new file mode 100644
index 000000000..a52e72050
--- /dev/null
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
@@ -0,0 +1,892 @@
+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);
+ }
+ }
+}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java b/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java
index 60efb90f7..3db6af80e 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/util/VariabilityUtilsInternal.java
+++ b/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;
+ }
}
--
GitLab