Skip to content
Snippets Groups Projects
Commit 7a502236 authored by Andreas Bayha's avatar Andreas Bayha
Browse files

Variability: Clean-up optimized EMF translation 

Removed unused and commented out code. Added comments.

Issue-ref: 4146
Issue-URL: af3#4146



Signed-off-by: default avatarAndreas Bayha <bayha@fortiss.org>
parent 6653199a
No related branches found
No related tags found
1 merge request!1784240
Pipeline #38668 passed
Stage: test
Pipeline: maven-releng

#38669

    Hide whitespace changes
    Inline Side-by-side
    org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
    + 123
    − 237
    View file @ 7a502236
    ......@@ -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;
    }
    ......
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment