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 485a5891823adc4c74fcc7978e193d2600ce3191..86aa2e7d2f7299279787a3d2c583c6c4e7c7c685 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/EMFProductLineTranslation.java
@@ -63,50 +63,28 @@ import com.microsoft.z3.Symbol;
*/
public class EMFProductLineTranslation implements IProductLineTranslation {
- /** Mapping of attributes to their translated Z3 function. */
+ /*
+ * FIXME: These should be
+ * easier now, since we do not translate objects for all inheritance levels. Multiple
+ * properties??.
+ */
+
+ /**
+ * Mapping of attributes to their translated Z3 function.
+ */
protected DualKeyMap<EAttribute, EClass, FuncDecl<?>> eAttribute2FunDecl =
new DualKeyMap<EAttribute, EClass, FuncDecl<?>>();
/** Mapping of references to their translated Z3 function. */
protected DualKeyMap<EReference, EClass, FuncDecl<?>> eReference2FunDecl =
new DualKeyMap<EReference, EClass, FuncDecl<?>>();
- /** Mapping of references to the respective translated Z3 type. FIXME: Still required? */
- protected Map<EReference, Sort> eReference2Sort = new HashMap<EReference, Sort>();
-
- /** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
- protected Map<EDataType, Sort> eDataType2Sort = new HashMap<EDataType, Sort>();
- /** Mapping for classes to their respective Z3 type. */
- protected Map<EClass, EnumSort<?>> eClass2z3Sort = new HashMap<EClass, EnumSort<?>>();
-
- /** Mapping of class.reference to the respective z3 function. FIXME: REMOVE */
- protected DualKeyMap<EClass, String, FuncDecl<?>> attRefNames2FuncDecl =
- new DualKeyMap<EClass, String, FuncDecl<?>>();
-
/**
* Mapping of objects with types to their translated Z3 expressions. (EClass is necessary as an
- * object is translated for all classes in the inheritance hierarchy). FIXME: This should be
- * easier now, since we do not translate objects for all inheritance levels. Multiple
- * properties??.
+ * object is translated for all classes in the inheritance hierarchy).
*/
protected DualKeyMap<EObject, EClass, Expr<?>> eObject2z3Expr =
new DualKeyMap<EObject, EClass, Expr<?>>();
- /** Mapping of enumeration literals to the translated Z3 expression. */
- protected Map<Enum<?>, Expr<?>> eLiteral2Expr = new HashMap<Enum<?>, Expr<?>>();
- /** Mapping of classes to their respective z3 expression for 'null' */
- protected Map<EClass, Expr<?>> eClass2NullElement = new HashMap<EClass, Expr<?>>();
- /** Mapping of enumerations to their respective z3 expression for 'null' */
- protected Map<EEnum, Expr<?>> eEnum2NullElement = new HashMap<EEnum, Expr<?>>();
-
- /**
- * Mapping of feature names to corresponding Z3 Expr. FIXME: Is this still necessary? Feature
- * Ref should be okay.
- */
- protected Map<String, BoolExpr> featureName2BoolExpr = new HashMap<String, BoolExpr>();
- /** Mapping of classes to the selection function (lambda) for this type. */
- protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction =
- new HashMap<EClass, FuncDecl<?>>();
-
/* Refactoring */
/** {@link Context} to capture the translated model. */
@@ -120,13 +98,28 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
protected BoolSort boolSort;
/** List of all translated assertions for the model. */
- protected List<BoolExpr> modelAssertions = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> modelAssertions;
/** List of all assertions for the feature model. */
- protected List<BoolExpr> featureModelAssertions = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> featureModelAssertions;
/** List of all assertions which encode the presence conditions. */
- protected List<BoolExpr> presenceConditionAssertions = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> presenceConditionAssertions;
/** List of all assertions which encode the constraints. */
- protected List<BoolExpr> constraintAssertions = new ArrayList<BoolExpr>();
+ protected List<BoolExpr> constraintAssertions;
+
+ /** Mapping of EDataTypes (e.g. EInt) to their translated Z3 type. */
+ protected Map<EDataType, Sort> eDataType2Sort;
+ /** Mapping for classes to their respective Z3 type. */
+ protected Map<EClass, EnumSort<?>> eClass2z3Sort;
+
+ /** Mapping of enumeration literals to the translated Z3 expression. */
+ protected Map<Enum<?>, Expr<?>> eLiteral2Expr;
+ /** Mapping of classes to their respective z3 expression for 'null' */
+ protected Map<EClass, Expr<?>> eClass2NullElement;
+ /** Mapping of enumerations to their respective z3 expression for 'null' */
+ protected Map<EEnum, Expr<?>> eEnum2NullElement;
+
+ /** Mapping of classes to the selection function for this type. */
+ protected Map<EClass, FuncDecl<?>> eClass2SelectionFunction;
/** The set to specify all {@link EClass} to be translated by this translation. */
protected Set<EClass> translatedClasses;
@@ -135,12 +128,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/** The set to specify all {@link EAttribute} to be translated by this translation. */
protected Set<EAttribute> translatedAttributes;
- /** The set of all {@link EObject} that are collected by this translation to be translated. */
- protected Set<EObject> translatedObjects;
/** The mapping of translated {@link EClass} to the objects that have been collected. */
protected BucketSetMap<EClass, EObject> class2TranslatedEObjects;
+
/** The {@link AbstractFeatureModel} collected by this translation */
protected AbstractFeatureModel featureModel;
+ /** Mapping of features to corresponding Z3 {@link BoolExpr}. */
+ protected Map<AbstractFeature, BoolExpr> feature2BoolExpr;
/** The mapping of translated {@link EObject}s to global {@link PresenceCondition}s. */
protected Map<EObject, PresenceConditionTerm> object2presenceCondition;
@@ -171,7 +165,10 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
* Constructor.
*/
public EMFProductLineTranslation() {
- initialize();
+ // Fields which should not change between individual translations are initialized only once
+ translatedClasses = new HashSet<EClass>();
+ translatedReferences = new HashSet<EReference>();
+ translatedAttributes = new HashSet<EAttribute>();
}
/**
@@ -180,6 +177,27 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
private void initialize() {
ctx = new Context();
+ class2TranslatedEObjects = new BucketSetMap<EClass, EObject>();
+ object2presenceCondition = new HashMap<EObject, PresenceConditionTerm>();
+
+ reference2TranslatedEClass = new HashMap<EReference, EClass>();
+
+ modelAssertions = new ArrayList<BoolExpr>();
+ featureModelAssertions = new ArrayList<BoolExpr>();
+ presenceConditionAssertions = new ArrayList<BoolExpr>();
+ constraintAssertions = new ArrayList<BoolExpr>();
+
+ eDataType2Sort = new HashMap<EDataType, Sort>();
+ eClass2z3Sort = new HashMap<EClass, EnumSort<?>>();
+
+ eLiteral2Expr = new HashMap<Enum<?>, Expr<?>>();
+ eClass2NullElement = new HashMap<EClass, Expr<?>>();
+ eEnum2NullElement = new HashMap<EEnum, Expr<?>>();
+
+ eClass2SelectionFunction = new HashMap<EClass, FuncDecl<?>>();
+ feature2BoolExpr = new HashMap<AbstractFeature, BoolExpr>();
+
+ // Initialize model independent base types
intSort = ctx.mkIntSort();
stringSort = ctx.mkStringSort();
boolSort = ctx.mkBoolSort();
@@ -187,20 +205,17 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
eDataType2Sort.put(EcorePackage.Literals.EINT, intSort);
eDataType2Sort.put(EcorePackage.Literals.ESTRING, stringSort);
eDataType2Sort.put(EcorePackage.Literals.EBOOLEAN, boolSort);
-
- translatedClasses = new HashSet<EClass>();
- translatedReferences = new HashSet<EReference>();
- translatedAttributes = new HashSet<EAttribute>();
-
- class2TranslatedEObjects = new BucketSetMap<EClass, EObject>();
- object2presenceCondition = new HashMap<EObject, PresenceConditionTerm>();
-
- reference2TranslatedEClass = new HashMap<EReference, EClass>();
}
/** {@inheritDoc} */
@Override
public final void translateModel(EObject model) {
+ // Initialize and reset local fields
+ initialize();
+
+ // Reference types need to be collected first, since they are required by optimizations in
+ // collectTranslatedObjects().
+ collectReferenceTypes();
collectTranslatedObjects(model, null);
translateFeatureModel();
@@ -216,6 +231,36 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
translatePresenceConditions();
}
+ /**
+ *
+ */
+ private void collectReferenceTypes() {
+ for(EReference ref : translatedReferences) {
+ EClass refType = ref.getEReferenceType();
+
+ if(translatedClasses.contains(refType)) {
+ reference2TranslatedEClass.put(ref, refType);
+ } else {
+ // Find a super type of the reference class
+ for(EClass ecls : translatedClasses) {
+ if(ecls.isSuperTypeOf(refType)) {
+ reference2TranslatedEClass.put(ref, ecls);
+ } else if(refType.isSuperTypeOf(ecls)) {
+ // FIXME: Is this a good idea?
+ // Attempt to use nearest found class
+ reference2TranslatedEClass.put(ref, ecls);
+ }
+ }
+
+ // Check if any super type was found
+ if(reference2TranslatedEClass.get(ref) == null) {
+ throw new RuntimeException("ERefernce \"" + ref.getName() + "\" is of type " +
+ ref.getEReferenceType().getName() + " which is not translated.");
+ }
+ }
+ }
+ }
+
/**
* @param model
* @param parentCondition
@@ -251,6 +296,21 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
}
+ /**
+ * @param eo
+ * @param cls
+ * @param pc
+ */
+ private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
+ class2TranslatedEObjects.add(cls, eo);
+
+ if(isIslandOptimizationEnabled) {
+ collectTranslatedReferences(eo, islandOptimizationStepNum);
+ }
+
+ object2presenceCondition.put(eo, pc);
+ }
+
/**
* @param model
* @param remainingSteps
@@ -309,8 +369,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
/**
- * @param model
- * @return
+ * Retrieves the {@link PresenceCondition} that was assigned to 'modelElement' in the model.
+ * This function might be overwritten in case an alternative location for presence conditions
+ * was defined.
*/
protected PresenceConditionTerm getLocalPresenceCondition(EObject model) {
if(model instanceof IOptionalVariationPoint<?>) {
@@ -330,62 +391,27 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
return null;
}
- /**
- * @param eo
- * @param cls
- * @param pc
- */
- private void collectEObject(EObject eo, EClass cls, PresenceConditionTerm pc) {
- class2TranslatedEObjects.add(cls, eo);
-
- if(isIslandOptimizationEnabled) {
- collectTranslatedReferences(eo, islandOptimizationStepNum);
- }
-
- object2presenceCondition.put(eo, pc);
- }
-
/** {@inheritDoc} */
@Override
public void setTranslatedEClasses(Collection<EClass> clss) {
+ translatedClasses.clear();
+
translatedClasses.addAll(clss);
}
/** {@inheritDoc} */
@Override
public void setTranslatedEReferences(Collection<EReference> refs) {
- translatedReferences.addAll(refs);
-
- for(EReference ref : refs) {
- EClass refType = ref.getEReferenceType();
-
- if(translatedClasses.contains(refType)) {
- reference2TranslatedEClass.put(ref, refType);
- } else {
- // Find a super type of the reference class
- for(EClass ecls : translatedClasses) {
- if(ecls.isSuperTypeOf(refType)) {
- reference2TranslatedEClass.put(ref, ecls);
- } else if(refType.isSuperTypeOf(ecls)) {
- // FIXME: Is this a good idea?
- // Attempt to use nearest found class
- reference2TranslatedEClass.put(ref, ecls);
- }
- }
-
- // Check if any super type was found
- if(reference2TranslatedEClass.get(ref) == null) {
- throw new RuntimeException("ERefernce \"" + ref.getName() + "\" is of type " +
- ref.getEReferenceType().getName() + " which is not translated.");
- }
- }
- }
+ translatedReferences.clear();
+ translatedReferences.addAll(refs);
}
/** {@inheritDoc} */
@Override
public void setTranslatedEAttributes(Collection<EAttribute> atts) {
+ translatedAttributes.clear();
+
translatedAttributes.addAll(atts);
}
@@ -424,7 +450,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
// Illegal literals are translated as true.
return ctx.mkTrue();
}
- return featureName2BoolExpr.get(literal.getName());
+ return feature2BoolExpr.get(literal);
}
if(pc instanceof DefaultPC) {
@@ -458,7 +484,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
BoolExpr fmExpr = ctx.mkBoolConst("FEATURE_" + featureModel.getName());
- featureName2BoolExpr.put(featureModel.getName(), fmExpr);
+ feature2BoolExpr.put(featureModel, fmExpr);
featureModelAssertions.add(fmExpr);
@@ -467,13 +493,13 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
String name = f.getName();
String constName = "FEATURE_" + name;
final BoolExpr fExpr = ctx.mkBoolConst(constName.replaceAll("@", "AT"));
- featureName2BoolExpr.put(name, fExpr);
+ feature2BoolExpr.put(f, fExpr);
// If f is child of another feature, the selection criteria have to be encoded.
final EObject fContainer = f.eContainer();
if(fContainer instanceof AbstractFeature) {
AbstractFeature parentF = (AbstractFeature)fContainer;
- final BoolExpr parentExpr = featureName2BoolExpr.get(parentF.getName());
+ final BoolExpr parentExpr = feature2BoolExpr.get(parentF);
if(f.isOptional()) {
featureModelAssertions.add(ctx.mkImplies(fExpr, parentExpr));
@@ -488,20 +514,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
// For alternatives also translate the alternative selection criteria
for(AbstractAlternativeFeature af : getChildrenWithType(featureModel,
AbstractAlternativeFeature.class)) {
- BoolExpr afExpr = featureName2BoolExpr.get(af.getName());
+ BoolExpr afExpr = feature2BoolExpr.get(af);
EList<AbstractFeature> as = af.getAlternatives();
- featureModelAssertions.add(ctx.mkImplies(afExpr,
- ctx.mkOr(as.stream().map(alt -> featureName2BoolExpr.get(alt.getName()))
+ featureModelAssertions.add(
+ ctx.mkImplies(afExpr, ctx.mkOr(as.stream().map(alt -> feature2BoolExpr.get(alt))
.collect(toList()).toArray(new BoolExpr[0]))));
for(AbstractFeature a : as) {
- BoolExpr aExpr = featureName2BoolExpr.get(a.getName());
+ BoolExpr aExpr = feature2BoolExpr.get(a);
featureModelAssertions.add(ctx.mkImplies(aExpr, afExpr));
featureModelAssertions.add(ctx.mkImplies(aExpr,
ctx.mkAnd(as.stream().filter(alt -> alt != a)
- .map(alt -> ctx.mkNot(featureName2BoolExpr.get(alt.getName())))
- .collect(toList()).toArray(new BoolExpr[0]))));
+ .map(alt -> ctx.mkNot(feature2BoolExpr.get(alt))).collect(toList())
+ .toArray(new BoolExpr[0]))));
}
}
@@ -511,8 +537,8 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
AbstractFeature target = c.getTarget();
AbstractFeature source = (AbstractFeature)c.eContainer();
- BoolExpr srcExpr = featureName2BoolExpr.get(source.getName());
- BoolExpr trgExpr = featureName2BoolExpr.get(target.getName());
+ BoolExpr srcExpr = feature2BoolExpr.get(source);
+ BoolExpr trgExpr = feature2BoolExpr.get(target);
switch(c.getType()) {
case REQUIRES:
@@ -528,7 +554,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/** Creates and initializes the Z3 solver to be used for analyis. */
@Override
- public Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
+ public Solver createSolver() {
Solver solver = ctx.mkSolver();
solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
@@ -579,8 +605,9 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
eClass2NullElement.get(refType)));
} else {
- modelAssertions.add(ctx.mkEq(ctx.mkApp(refFunc, nullElement),
- ctx.mkEmptySeq(eReference2Sort.get(er))));
+ modelAssertions
+ .add(ctx.mkEq(ctx.mkApp(refFunc, nullElement), ctx.mkEmptySeq(
+ eClass2z3Sort.get(reference2TranslatedEClass.get(er)))));
}
}
}
@@ -601,7 +628,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
List<?> values = (List<?>)value;
if(values.size() == 0) {
- return ctx.mkEmptySeq(eReference2Sort.get(er));
+ return ctx.mkEmptySeq(eReferenceToz3Sort(er));
}
SeqExpr[] seqElems = new SeqExpr[values.size()];
@@ -612,7 +639,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
SeqExpr<?> selectedExpr = ctx.mkUnit(elemExpr);
if(refSelFun != null) {
- SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReference2Sort.get(er));
+ SeqExpr notSelectedExpr = ctx.mkEmptySeq(eReferenceToz3Sort(er));
seqElems[i] = (SeqExpr<?>)ctx.mkITE((BoolExpr)ctx.mkApp(refSelFun, elemExpr),
selectedExpr, notSelectedExpr);
} else {
@@ -621,7 +648,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
}
if(seqElems.length == 0) {
- return ctx.mkEmptySeq(eReference2Sort.get(er));
+ return ctx.mkEmptySeq(eReferenceToz3Sort(er));
}
if(seqElems.length == 1) {
return seqElems[0];
@@ -728,8 +755,6 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), rangeSort);
eAttribute2FunDecl.put(ea, ec, funDecl);
- // eClass2TranslatedAttributes.add(ec, ea);
- attRefNames2FuncDecl.put(ec, ea.getName(), funDecl);
}
}
@@ -764,10 +789,7 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
FuncDecl<?> funDecl = ctx.mkFuncDecl(funId, eClass2z3Sort.get(ec), refSort);
- eReference2Sort.put(er, refSort);
eReference2FunDecl.put(er, ec, funDecl);
- // eclass2TranslatedReferences.add(ec, er);
- attRefNames2FuncDecl.put(ec, er.getName(), funDecl);
}
}
}
@@ -872,8 +894,20 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
/** {@inheritDoc} */
@Override
- public FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass cVarType, String string) {
- return attRefNames2FuncDecl.get(cVarType, string);
+ public FuncDecl<?> getAttributeReferenceFunctionDeclaration(EClass cVarType, String name) {
+ for(EReference ref : cVarType.getEAllReferences()) {
+ if(ref.getName().equals(name)) {
+ return eReference2FunDecl.get(ref, cVarType);
+ }
+ }
+
+ for(EAttribute att : cVarType.getEAllAttributes()) {
+ if(att.getName().equals(name)) {
+ return eAttribute2FunDecl.get(att, cVarType);
+ }
+ }
+
+ return null;
}
/** {@inheritDoc} */
@@ -950,4 +984,12 @@ public class EMFProductLineTranslation implements IProductLineTranslation {
public void setIslandOptimizationStepNum(int islandOptimizationStepNum) {
this.islandOptimizationStepNum = islandOptimizationStepNum;
}
+
+ /**
+ * @param er
+ * @return
+ */
+ private EnumSort<?> eReferenceToz3Sort(EReference er) {
+ return eClass2z3Sort.get(reference2TranslatedEClass.get(er));
+ }
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java
index 7dd4a9b1cb4ffa59521056f87525d1effd48719a..2727a9ad6301eb6b7948f192b6ff0747497944d6 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineAnalysis.java
@@ -1,13 +1,10 @@
package org.fortiss.variability.analysis;
import static com.microsoft.z3.Status.UNSATISFIABLE;
-import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
-import static org.fortiss.variability.VariabilityActivator.getDefault;
import java.io.FileNotFoundException;
import java.io.PrintWriter;
import java.util.ArrayList;
-import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
@@ -20,9 +17,7 @@ import org.eclipse.emf.ecore.EReference;
import org.fortiss.tooling.kernel.model.INamedElement;
import com.microsoft.z3.BoolExpr;
-import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
-import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.Model;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Status;
@@ -37,18 +32,10 @@ public abstract class GenericProductLineAnalysis {
protected final IProductLineTranslation translation;
- /** List of all translated correctness constraints. */
- protected List<BoolExpr> rawConstraints = new ArrayList<BoolExpr>();
-
protected List<IProductLineConstraint> plConstraints = new ArrayList<IProductLineConstraint>();
- protected Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
- new HashMap<BoolExpr, IProductLineConstraint>();
-
protected final EObject model;
- protected Context ctx;
-
/**
* Constructor.
*/
@@ -56,7 +43,6 @@ public abstract class GenericProductLineAnalysis {
this.model = model;
this.translation = translation;
- ctx = translation.getContext();
}
/**
@@ -74,13 +60,14 @@ public abstract class GenericProductLineAnalysis {
translation.translateModel(model);
- constraintTracker2Constraint = translation.translateConstraints(plConstraints);
+ Map<BoolExpr, IProductLineConstraint> constraintTracker2Constraint =
+ translation.translateConstraints(plConstraints);
// addRawConstraints();
// Global.setParameter("parallel.enable", "true");
- Solver solver = translation.createSolver(tracToExpr);
+ Solver solver = translation.createSolver();
String modelName = ((INamedElement)model).getName();
String path = "C:\\Users\\bayha\\tmp\\z3" + modelName + (start % 159739431) + "in";
@@ -138,7 +125,7 @@ public abstract class GenericProductLineAnalysis {
Expr constInterp = z3Model.getConstInterp(constTrack);
if(constInterp instanceof BoolExpr) {
- if(constInterp.equals(ctx.mkTrue())) {
+ if(constInterp.equals(translation.getContext().mkTrue())) {
IProductLineConstraint failedConstraint =
constraintTracker2Constraint.get(constTrack);
@@ -193,111 +180,5 @@ public abstract class GenericProductLineAnalysis {
}
- /** Mapping from tracking variables to z3 expression (used for counterexample extraction). */
- protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
-
- // /** gets the Z3 solver to be used for analysis and adds all constraints. */
- // protected Solver getSolver() {
- // Solver solver = translation.createSolver(tracToExpr);
- //
- // if(rawConstraints.size() > 0) {
- // solver.add(rawConstraints.toArray(new BoolExpr[rawConstraints.size()]));
- //
- // Set<BoolExpr> constraintTrackerExprs = constraintTracker2Constraint.keySet();
- // solver.add(translation.getContext().mkOr(
- // constraintTrackerExprs.toArray(new BoolExpr[constraintTrackerExprs.size()])));
- // }
- // return solver;
- // }
-
- // /** Needs to be overwritten to add the constraints to be checked. */
- // protected void addRawConstraints() {
- // // EMPTY
- // }
- //
protected abstract void addConstriants();
-
- protected void translateConstraints() {
- // for(IProductLineConstraint constraint : plConstraints) {
- // Expr[] quantifierValiables = constraint.getQuantifierVariables();
- // EClass[] variableClasses = constraint.getVariablesClasses();
- // BoolExpr[] containmentExprs = new BoolExpr[0];
- // BoolExpr body = constraint.getBody();
- //
- // boolean isForAll = constraint.isForAll();
- //
- // BoolExpr quantifier = createLiftedConstraint(quantifierValiables, variableClasses,
- // containmentExprs, body, isForAll);
- //
- // BoolExpr constraintTracker =
- // ctx.mkBoolConst("CONSTRAINT_" + constraint.getConstraintName());
- // constraintTracker2Constraint.put(constraintTracker, constraint);
- //
- // rawConstraints.add(ctx.mkEq(constraintTracker, quantifier));
- // constraintTrackers.add(constraintTracker);
- // }
- }
-
- /** Automatically lifts the given constraint */
- protected BoolExpr liftConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
- BoolExpr body, boolean isForAll) {
- return createLiftedConstraint(quantifierValiables, variableClasses, new BoolExpr[0], body,
- isForAll);
- }
-
- // protected BoolExpr createLiftedQuantifier(String[] quantifierValiableNames,
- // EClass[] variableClasses, BoolExpr[] containmentExprs, BoolExpr body,
- // boolean isForAll) {
- //
- // int numVar = quantifierValiableNames.length;
- // Expr[] quantifierValiables = new Expr[numVar];
- //
- // for(int i = 0; i < numVar; i++) {
- // EnumSort sort = translation.geteClass2Datatype().get(variableClasses[i]);
- // Expr expr = ctx.mkConst(quantifierValiableNames[i], sort);
- //
- // quantifierValiables[i] = expr;
- // }
- //
- // return createLiftedConstraint(quantifierValiables, variableClasses, containmentExprs, body,
- // isForAll);
- // }
-
- /** Automatically lifts the given constraint */
- protected BoolExpr createLiftedConstraint(Expr[] quantifierValiables, EClass[] variableClasses,
- BoolExpr[] containmentExprs, BoolExpr body, boolean isForAll) {
-
- BoolExpr[] selExprs = new BoolExpr[quantifierValiables.length + containmentExprs.length];
- for(int i = 0; i < quantifierValiables.length; i++) {
- EClass cls = variableClasses[i];
- Expr var = quantifierValiables[i];
-
- FuncDecl selFun = translation.getSelectionFunction(cls);
- BoolExpr selected = (BoolExpr)ctx.mkApp(selFun, var);
- BoolExpr notNull = ctx.mkNot(ctx.mkEq(var, translation.getNullElement(cls)));
-
- selExprs[i] = ctx.mkAnd(selected, notNull);
- }
-
- // Add containment expressions
- int j = 0;
- for(int i = quantifierValiables.length; i < quantifierValiables.length +
- containmentExprs.length; i++) {
- selExprs[i] = containmentExprs[j++];
- }
-
- if(isForAll) {
- BoolExpr liftedBody = ctx.mkImplies(ctx.mkAnd(selExprs), body);
- return ctx.mkForall(quantifierValiables, liftedBody, 0, null, null, null, null);
- }
-
- // else: Exits
- BoolExpr liftedBody = ctx.mkAnd(ctx.mkAnd(selExprs), body);
- return ctx.mkExists(quantifierValiables, liftedBody, 0, null, null, null, null);
- }
-
- /** Logs an error in the analysis. */
- private void logError(String message) {
- error(getDefault(), "Error in product-line analysis: " + message);
- }
}
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
index 2c7c64f7d47206ee92a35b3b9fdeb94255bf6c20..8cf8565a2c477974d459e833479cdeb2c12c1366 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/GenericProductLineTranslation.java
@@ -387,7 +387,7 @@ public class GenericProductLineTranslation implements IProductLineTranslation {
// protected Map<BoolExpr, BoolExpr> tracToExpr = new HashMap<BoolExpr, BoolExpr>();
/** Creates and initializes the Z3 solver to be used for analyis. */
- public Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr) {
+ public Solver createSolver() {
Solver solver = ctx.mkSolver();// ctx.mkTactic("psmt"));
solver.add(featureModelAssertions.toArray(new BoolExpr[featureModelAssertions.size()]));
diff --git a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
index acafedb851f8343dd6a87169fcc8facbc5522b02..410a2dba4858ab8453035d6ec631999ed36f4a2e 100644
--- a/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
+++ b/org.fortiss.variability/src/org/fortiss/variability/analysis/IProductLineTranslation.java
@@ -62,7 +62,7 @@ public interface IProductLineTranslation {
* @param tracToExpr
* @return
*/
- Solver createSolver(Map<BoolExpr, BoolExpr> tracToExpr);
+ Solver createSolver();
/**
* @param cls