From 7a5022362678a314b43b931d3fcc97ef513dbb6c Mon Sep 17 00:00:00 2001
From: Andreas Bayha <bayha@fortiss.org>
Date: Wed, 2 Aug 2023 12:08:41 +0200
Subject: [PATCH] Variability: Clean-up optimized EMF translation
Removed unused and commented out code. Added comments.
Issue-ref: 4146
Issue-URL: https://git.fortiss.org/af3/af3/-/issues/4146
Signed-off-by: Andreas Bayha <bayha@fortiss.org>
---
.../analysis/EMFProductLineTranslation.java | 360 ++++++------------
1 file changed, 123 insertions(+), 237 deletions(-)
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
index eceb5c61e..485a58918 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
@@ -56,81 +56,68 @@ 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.
+ * Base class that implements the translation of EMF based model product-lines to SMT in order to
+ * perform product-line analysis via constraint lifting.
*
* @author bayha
*/
public class EMFProductLineTranslation implements IProductLineTranslation {
- /** 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> eClass2TranslatedAttributes =
- // new BucketSetMap<EClass, EAttribute>();
- // /** Mapping from classes to all references of the respective type. */
- // protected BucketSetMap<EClass, EReference> eclass2TranslatedReferences =
- // new BucketSetMap<EClass, EReference>();
-
/** Mapping of attributes to their translated Z3 function. */
- protected DualKeyMap<EAttribute, EClass, FuncDecl> eAttribute2FunDecl =
- new DualKeyMap<EAttribute, EClass, FuncDecl>();
+ 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>();
+ protected DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl =
+ new DualKeyMap<EReference, EClass, FuncDecl<?>>();
- /** Mapping of references to the respective translated Z3 type. */
+ /** 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>();
+ protected Map<EClass, EnumSort<?>> eClass2z3Sort = 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 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).
+ * 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??.
*/
- protected DualKeyMap<EObject, EClass, Expr> eObject2z3Expr =
- new DualKeyMap<EObject, EClass, Expr>();
-
- protected Map<Expr, EObject> expr2EObject = new HashMap<Expr, EObject>();
+ 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>();
+ 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>();
-
+ 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>();
+ protected Map<EEnum, Expr<?>> eEnum2NullElement = new HashMap<EEnum, Expr<?>>();
- /** Mapping of feature names to corresponding Z3 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>();
- /** Mapping of objects to their presence conditions. */
- protected Map<EObject, BoolExpr> eObject2Selection = new HashMap<EObject, BoolExpr>();
+ protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction =
+ new HashMap<EClass, FuncDecl<?>>();
+
+ /* Refactoring */
/** {@link Context} to capture the translated model. */
- protected Context ctx = new Context();
+ protected Context ctx;
+
+ /** 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;
/** List of all translated assertions for the model. */
protected List<BoolExpr> modelAssertions = new ArrayList<BoolExpr>();
@@ -138,26 +125,46 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
/** List of all assertions which encode the presence conditions. */
protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
-
+ /** List of all assertions which encode the constraints. */
protected List<BoolExpr> constraintAssertions = new ArrayList<BoolExpr>();
- /* Refactoring */
-
+ /** The set to specify all {@link EClass} to be translated by this translation. */
protected Set<EClass> translatedClasses;
+ /** The set to specify all {@link EReference} to be translated by this translation. */
protected Set<EReference> translatedReferences;
+ /** The set to specify all {@link EAttribute} to be translated by this translation. */
protected Set<EAttribute> translatedAttributes;
- protected Set<EObject> translatedObjects;
-
- protected AbstractFeatureModel featureModel;
+ /** 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;
+ /** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */
protected Map<EObject, PresenceConditionTerm> object2presenceCondition;
+ /**
+ * The mapping from Z3 {@link Expr} back to the respective {@link EObject} to be used for
+ * interpreting solver results.
+ */
+ protected Map<Expr<?>, EObject> expr2EObject = new HashMap<Expr<?>, EObject>();
+
+ /**
+ * The mapping of translated {@link EReference}s to the type that will be used for translation.
+ * This type might be different from the references original type in case only a subtype is
+ * specified for translation.
+ */
protected Map<EReference, EClass> reference2TranslatedEClass;
+ /** Flag that specifies whether the optimization to only translate optional parts is enabled. */
private boolean isIslandOptimizationEnabled = false;
+ /**
+ * The number of non-variable elements that are connected to a variable element to be translated
+ * in case the "island optimization" is enabled.
+ */
private int islandOptimizationStepNum = 0;
/**
@@ -171,6 +178,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
* Initialization of analysis and base types.
*/
private void initialize() {
+ ctx = new Context();
+
intSort = ctx.mkIntSort();
stringSort = ctx.mkStringSort();
boolSort = ctx.mkBoolSort();
@@ -189,8 +198,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
reference2TranslatedEClass = new HashMap<EReference, EClass>();
}
- /** Performs the complete translation of the product-line to Z3. */
- public void translateModel(EObject model) {
+ /** {@inheritDoc} */
+ @Override
+ public final void translateModel(EObject model) {
collectTranslatedObjects(model, null);
translateFeatureModel();
@@ -206,6 +216,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
translatePresenceConditions();
}
+ /**
+ * @param model
+ * @param parentCondition
+ */
private void collectTranslatedObjects(EObject model, PresenceConditionTerm parentCondition) {
if(model instanceof AbstractFeatureModel) {
featureModel = (AbstractFeatureModel)model;
@@ -237,6 +251,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
+ /**
+ * @param model
+ * @param remainingSteps
+ */
private void collectTranslatedReferences(EObject model, int remainingSteps) {
if(remainingSteps <= 0) {
return;
@@ -314,6 +332,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/**
* @param eo
+ * @param cls
+ * @param pc
*/
private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
class2TranslatedEObjects.add(cls, eo);
@@ -325,10 +345,14 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
object2presenceCondition.put(eo, pc);
}
+ /** {@inheritDoc} */
+ @Override
public void setTranslatedEClasses(Collection<EClass> clss) {
translatedClasses.addAll(clss);
}
+ /** {@inheritDoc} */
+ @Override
public void setTranslatedEReferences(Collection<EReference> refs) {
translatedReferences.addAll(refs);
@@ -359,6 +383,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
+ /** {@inheritDoc} */
+ @Override
public void setTranslatedEAttributes(Collection<EAttribute> atts) {
translatedAttributes.addAll(atts);
}
@@ -366,8 +392,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/** Translates all presence conditions to Z3. */
protected void translatePresenceConditions() {
for(EClass ec : translatedClasses) {
- EnumSort ecSort = eClass2z3Sort.get(ec);
- FuncDecl selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
+ EnumSort<?> ecSort = eClass2z3Sort.get(ec);
+ FuncDecl<?> selFun = ctx.mkFuncDecl("SELECTED_" + ec.getName(), ecSort, boolSort);
eClass2SelectionFunction.put(ec, selFun);
for(EObject eo : class2TranslatedEObjects.get(ec)) {
@@ -380,9 +406,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
eoSelection = ctx.mkTrue();
}
- eObject2Selection.put(eo, eoSelection);
-
- Expr eoExpr = eObject2z3Expr.get(eo, ec);
+ Expr<?> eoExpr = eObject2z3Expr.get(eo, ec);
presenceConditionAssertions.add(ctx.mkEq(ctx.mkApp(selFun, eoExpr), eoSelection));
}
}
@@ -502,12 +526,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
- /** 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. */
+ @Override
public Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
- Solver solver = ctx.mkSolver();// ctx.mkTactic("psmt"));
+ Solver solver = ctx.mkSolver();
solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
solver.add(presenceConditionAssertions
@@ -528,10 +550,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
EList<EAttribute> attributes = ec.getEAllAttributes();
for(EAttribute ea : attributes) {
if(translatedAttributes.contains(ea)) {
- FuncDecl attFunc = eAttribute2FunDecl.get(ea, ec);
+ FuncDecl<?> attFunc = eAttribute2FunDecl.get(ea, ec);
for(EObject eo : objs) {
- Expr attVal = translateAttributeValue(eo, ea);
+ Expr<?> attVal = translateAttributeValue(eo, ea);
BoolExpr attValAssertion =
ctx.mkEq(ctx.mkApp(attFunc, eObject2z3Expr.get(eo, ec)), attVal);
modelAssertions.add(attValAssertion);
@@ -542,17 +564,17 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
EList<EReference> references = ec.getEAllReferences();
for(EReference er : references) {
if(translatedReferences.contains(er)) {
- FuncDecl refFunc = eReference2FunDecl.get(er, ec);
+ FuncDecl<?> refFunc = eReference2FunDecl.get(er, ec);
for(EObject eo : objs) {
- Expr eoExpr = eObject2z3Expr.get(eo, ec);
- Expr refVal = translateReferenceValue(eo, er);
+ Expr<?> eoExpr = eObject2z3Expr.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 = reference2TranslatedEClass.get(er);
- Expr nullElement = eClass2NullElement.get(ec);
+ Expr<?> nullElement = eClass2NullElement.get(ec);
if(er.getUpperBound() > 0) {
modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
eClass2NullElement.get(refType)));
@@ -566,12 +588,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
/** Translates the given instance of a relation between individual objects in the model. */
- private Expr translateReferenceValue(EObject eo, EReference er) {
+ @SuppressWarnings({"unchecked", "rawtypes"})
+ private Expr<?> translateReferenceValue(EObject eo, EReference er) {
Object value = eo.eGet(er);
EClass refType = reference2TranslatedEClass.get(er);
- Expr refNullValue = eClass2NullElement.get(refType);
+ Expr<?> refNullValue = eClass2NullElement.get(refType);
- FuncDecl refSelFun = eClass2SelectionFunction.get(refType);
+ FuncDecl<?> refSelFun = eClass2SelectionFunction.get(refType);
if(er.getUpperBound() < 0) {
// Case for lists
@@ -581,21 +604,16 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
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 = eObject2z3Expr.get((EObject)o, refType);
+ Expr<?> elemExpr = eObject2z3Expr.get((EObject)o, refType);
- SeqExpr selectedExpr = ctx.mkUnit(elemExpr);
+ 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),
+ seqElems[i] = (SeqExpr<?>)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
selectedExpr, notSelectedExpr);
} else {
seqElems[i] = selectedExpr;
@@ -628,28 +646,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
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) {
+ @SuppressWarnings({"rawtypes", "unchecked"})
+ private Expr<?> translateAttributeValue(EObject eo, EAttribute ea) {
Object value = eo.eGet(ea);
EDataType attType = ea.getEAttributeType();
@@ -660,7 +659,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
SeqExpr[] seqElem = new SeqExpr[values.size()];
for(int i = 0; i < values.size(); i++) {
Object o = values.get(i);
- Expr elemExpr = translatePrimitiveObject(o, attType);
+ Expr<?> elemExpr = translatePrimitiveObject(o, attType);
seqElem[i] = ctx.mkUnit(elemExpr);
}
@@ -672,7 +671,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
/** Translates the given object for a primitive type (Enums, Integer, String, Boolean) to Z3. */
- private Expr translatePrimitiveObject(Object value, EDataType attType) {
+ private Expr<?> translatePrimitiveObject(Object value, EDataType attType) {
// Single value
if(attType.equals(EcorePackage.Literals.EINT)) {
if(value == null) {
@@ -726,7 +725,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
continue;
}
- FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), rangeSort);
+ FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), rangeSort);
eAttribute2FunDecl.put(ea, ec, funDecl);
// eClass2TranslatedAttributes.add(ec, ea);
@@ -763,7 +762,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
refSort = ctx.mkSeqSort(refSort);
}
- FuncDecl funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), refSort);
+ FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), refSort);
eReference2Sort.put(er, refSort);
eReference2FunDecl.put(er, ec, funDecl);
@@ -774,59 +773,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
- // /** 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();
@@ -840,7 +786,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
literals[numLiterals] = name + "_NONE_LITERAL";
- EnumSort enumSort = ctx.mkEnumSort(name, literals);
+ EnumSort<?> enumSort = ctx.mkEnumSort(name, literals);
// Add regular literals and null literal to the respective mappings.
for(int i = 0; i < numLiterals; i++) {
@@ -868,16 +814,16 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
objSymbols[objs.size()] = ctx.mkSymbol(clsName + "NONE");
// Create EnumSort for class
- EnumSort enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
+ EnumSort<?> enumSort = ctx.mkEnumSort(ctx.mkSymbol(clsName), objSymbols);
eClass2z3Sort.put(cls, enumSort);
// Map objects to z3 enum literals
- Expr[] consts = enumSort.getConsts();
+ Expr<?>[] consts = enumSort.getConsts();
for(int i = 0; i < objs.size(); i++) {
eObject2z3Expr.put(objs.get(i), cls, consts[i]);
expr2EObject.put(consts[i], objs.get(i));
}
- Expr noneExpr = consts[consts.length - 1];
+ Expr<?> noneExpr = consts[consts.length - 1];
eClass2NullElement.put(cls, noneExpr);
}
}
@@ -887,80 +833,19 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
// 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. */
+ /** {@inheritDoc} */
+ @Override
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);
- // }
- // }
-
/** {@inheritDoc} */
@Override
public EObject getEObjectForExpression(Expr<?> expr) {
return expr2EObject.get(expr);
}
- /** {@inheritDoc} */
+ /** {@inheritDoc} FIXME: required?? */
@Override
public FuncDecl<?> getSelectionFunction(EClass cls) {
return eClass2SelectionFunction.get(cls);
@@ -981,13 +866,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/** {@inheritDoc} */
@Override
- public EnumSort getDatatype(EClass ec) {
+ public EnumSort<?> getDatatype(EClass ec) {
return eClass2z3Sort.get(ec);
}
/** {@inheritDoc} */
@Override
- public FuncDecl getAttributeReferenceFunctionDeclaration(EClass cVarType, String string) {
+ public FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass cVarType, String string) {
return attRefNames2FuncDecl.get(cVarType, string);
}
@@ -999,7 +884,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
new HashMap<BoolExpr, IProductLineConstraint>();
for(IProductLineConstraint constraint : constraints) {
- Expr[] quantifierValiables = constraint.getQuantifierVariables();
+ Expr<?>[] quantifierValiables = constraint.getQuantifierVariables();
EClass[] variableClasses = constraint.getVariablesClasses();
BoolExpr[] containmentExprs = new BoolExpr[0];
BoolExpr body = constraint.getBody();
@@ -1023,15 +908,16 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
/** Automatically lifts the given constraint */
- protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
- BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
+ 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];
+ Expr<?> var = quantifierValiables[i];
- FuncDecl selFun = getSelectionFunction(cls);
+ FuncDecl<?> selFun = getSelectionFunction(cls);
BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, getNullElement(cls)));
@@ -1055,12 +941,12 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
}
- /** Sets isIslandOptimizationEnabled. */
+ /** Sets isIslandOptimizationEnabled. TODO */
public void setIslandOptimizationEnabled(boolean isIslandOptimizationEnabled) {
this.isIslandOptimizationEnabled = isIslandOptimizationEnabled;
}
- /** Sets islandOptimizationStepNum. */
+ /** Sets islandOptimizationStepNum. TODO */
public void setIslandOptimizationStepNum(int islandOptimizationStepNum) {
this.islandOptimizationStepNum = islandOptimizationStepNum;
}
--
GitLab