Commit 3541f920 authored by Simon Barner's avatar Simon Barner
Browse files

Minor cleanup (preserves previous ratings)

parent cd9baaa6
DSLtoSMT.java 2da85c44fe4fbcce7ba8ec7d1945871703334d38 RED
ScheduleRun.java 060e5b0edd7d9e4a02f438a429a423697480a394 RED
DSLtoSMT.java 5477dc915254a4af1250c5fb1676f44dc4018622 RED
ScheduleRun.java c994a02420e21663d0c4756874862df9ceae2863 RED
SolverRun.java 5b89317c195314b2c144740144ca4038559a9581 RED
......@@ -71,7 +71,7 @@ import org.fortiss.af3.exploration.dsl_v2.model.expression.IExpression;
import org.fortiss.af3.exploration.dsl_v2.model.expression.IUnaryOperator;
import org.fortiss.af3.exploration.dsl_v2.model.expression.ModelElementLiteral;
import org.fortiss.af3.exploration.smt.model.StartTimeDummy;
import org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNONQuantifiedSMT;
import org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToNonQuantifiedSMT;
import org.fortiss.af3.exploration.smt.modeltransformation.rework.ConstraintToQuantifiedSMT;
import org.fortiss.tooling.base.model.element.IAnnotatedSpecification;
import org.fortiss.tooling.base.model.element.IModelElement;
......@@ -88,7 +88,7 @@ import com.microsoft.z3.Z3Type;
/**
* Class which which transforms an {@link IExpression} into a z3 {@link Expr} via the z3 API.
* Still needed for schedule synthesis. will be reaplced by {@link ConstraintToNONQuantifiedSMT} and
* Still needed for schedule synthesis. will be reaplced by {@link ConstraintToNonQuantifiedSMT} and
* {@link ConstraintToQuantifiedSMT}.
*
* @deprecated Will be replaced after release 2.12 (see #2920)
......
BasicDeploymentConstraint.java 31b6ee4370a371c959dab902034394cc87d9ae55 GREEN
ConstraintToNONQuantifiedSMT.java 0bb4ef00bed982f0356ea8de75b4dd2586bb3159 GREEN
ConstraintToQuantifiedSMT.java 9ce6e6f75f71c8fc9477a4a339bd9acd67ea8f4d GREEN
DSMLTransformationService.java 57217d40598d8028d0f0db2b940229a463e03c46 GREEN
DSMLtoSMTTransformator.java 5ed555b000db8eeb8768d06a57c3aa68226ea45f GREEN
DeploymentRun2.java 8c4b10a06b3e76c2ee6364d27ee2cd37f3feb370 GREEN
IDSMLTransformationService.java 381cd084ac01f6289893e026b8317ad0d8b1c4e1 GREEN
SMTTransformationUtils.java e0002fedbebe5fc5386d63b114ccb4e29afba26b GREEN
SolvedSMTResult.java 6c835cd7223eeb13cfeeccad3d8ea4bebb60f6fb GREEN
SolverRun2.java 7af4762df4b1bd9d797fbc0516f49b3d420fbab0 GREEN
BasicDeploymentConstraint.java de7431e56468acb1be4532aa735b8e0b50a39536 GREEN
ConstraintToNonQuantifiedSMT.java 47628c67b414a17a58363563235d8e9c88a3bdf6 GREEN
ConstraintToQuantifiedSMT.java 2fc3146a82f9a9bf397cfe1dc78d9227f6ec52b8 GREEN
DSMLTransformationService.java 92de6291ab2d5e4cd6cecd8c6ab6dcd5ea614197 GREEN
DSMLtoSMTTransformator.java 5569410a91098556bd1ab6ceed3589b9b526eb66 GREEN
DeploymentRun2.java 260c87d56bdc37db0fca7a03f1fd476cb8f86b15 GREEN
IDSMLTransformationService.java b575743a18db1a64f9a0bbc9624d9ec6b3626c97 GREEN
SMTTransformationUtils.java 3b1915d18a06dc6eb35d2b670f2fd70ccbe51de9 GREEN
SolvedSMTResult.java ee5178b476b7ed67b4dae792a0ef500273730220 GREEN
SolverRun2.java e79383d1fe27f4ae14b7fc6ce838b57a44121c7a GREEN
......@@ -79,10 +79,12 @@ public class BasicDeploymentConstraint {
for(IConnection ch : signalSuperSet.getEntries()) {
EObject source = ch.getSource().getOwner();
EObject target = ch.getTarget().getOwner();
if(!components.contains(source))
if(!components.contains(source)) {
components.add((Task)source);
if(!components.contains(target))
}
if(!components.contains(target)) {
components.add((Task)target);
}
}
ForAll routingConstraints =
......@@ -105,18 +107,22 @@ public class BasicDeploymentConstraint {
/**
* Creates a basic routing constraints.
*
* Informal description:
* "If a signal is allocated to a virtual link then
* the source of the signal (task) has to be allocated to the source of the virtual link
* (processing unit)
* and the sink of the signal (task) has to be allocated to the sink of the virtual link
* (processing unit)"
*
* Formalized in SMT:
* (assert (forall ((s SignalImpl))
* (forall ((v VirtualLinkImpl))
* (=> (= (allocate s) v)
* <p>
* <b>Informal description:</b><br>
* "If a signal is allocated to a virtual link then the source of the signal (task) has to be
* allocated to the source of the virtual link (processing unit) and the sink of the signal
* (task) has to be allocated to the sink of the virtual link (processing unit)"
* </p>
* <p>
* <b>Formalized in SMT:</b><br>
* <code>
* (assert (forall ((s SignalImpl))<br>
* (forall ((v VirtualLinkImpl))<br>
* (=> (= (allocate s) v)<br>
* (and (= (allocate (start s)) (start v)) (= (allocate (end s)) (end v)))))))
* </code>
* </p>
* *
*
* @throws Exception
* if constraint creation fails
......@@ -158,11 +164,12 @@ public class BasicDeploymentConstraint {
// (= (allocate (start s)) (start v))
ModelElementLiteral ch = createModelElementLiteral(channels);
Start startCH = FunctionFactory.eINSTANCE.createStart();
FunctionFactory ff = FunctionFactory.eINSTANCE;
Start startCH = ff.createStart();
startCH.setArgs(ch);
startCH.setSetReference((Set<IModelElement>)(Set<?>)dseSuperSets.get(Task.class));
ModelElementLiteral ro = createModelElementLiteral(virtualLinks);
Start startRoute = FunctionFactory.eINSTANCE.createStart();
Start startRoute = ff.createStart();
startRoute.setArgs(ro);
startRoute.setSetReference((Set<IModelElement>)(Set<?>)dseSuperSets
.get(ExecutionUnit.class));
......@@ -170,11 +177,11 @@ public class BasicDeploymentConstraint {
// (= (allocate (end s)) (end v))
ModelElementLiteral ch2 = createModelElementLiteral(channels);
End endCH = FunctionFactory.eINSTANCE.createEnd();
End endCH = ff.createEnd();
endCH.setArgs(ch2);
endCH.setSetReference((Set<IModelElement>)(Set<?>)dseSuperSets.get(Task.class));
ModelElementLiteral ro2 = createModelElementLiteral(virtualLinks);
End endRoute = FunctionFactory.eINSTANCE.createEnd();
End endRoute = ff.createEnd();
endRoute.setArgs(ro2);
endRoute.setSetReference((Set<IModelElement>)(Set<?>)dseSuperSets.get(ExecutionUnit.class));
Allocation allocationEndChEndRoute = createAllocation(endCH, endRoute);
......@@ -319,9 +326,13 @@ public class BasicDeploymentConstraint {
}
/**
* Creates a {@link End} function with startArg class as input parameter and returnType
* class as return type.
* end(endArg)==returnType
* <p>
* Creates a {@link End} function with {@code startArg} class as input parameter and
* {@code returnType} class as return type.
* </p>
* <p>
* {@code end(endArg)==returnType}
* </p>
*/
private static Equal end(Set<IModelElement> endArg, Set<IModelElement> returnType) {
End endCH = FunctionFactory.eINSTANCE.createEnd();
......@@ -334,9 +345,13 @@ public class BasicDeploymentConstraint {
}
/**
* Creates a {@link Start} function with startArg class as input parameter and returnType
* class as return type.
* start(startArg) == returnType
* <p>
* Creates a {@link Start} function with {@code startArg} class as input parameter and
* {@code returnType} class as return type.
* </p>
* <p>
* {@code start(startArg) == returnType}
* </p>
*/
private static Equal start(Set<IModelElement> startArg, Set<IModelElement> returnType) {
Start startCH = FunctionFactory.eINSTANCE.createStart();
......
......@@ -28,6 +28,7 @@ import static com.microsoft.z3.Z3javaAPIWrapper.createInteger;
import static com.microsoft.z3.Z3javaAPIWrapper.createMultiplication;
import static com.microsoft.z3.Z3javaAPIWrapper.createNot;
import static com.microsoft.z3.Z3javaAPIWrapper.createOr;
import static com.microsoft.z3.Z3javaAPIWrapper.createReal;
import static com.microsoft.z3.Z3javaAPIWrapper.createSmaller;
import static com.microsoft.z3.Z3javaAPIWrapper.createSmallerEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createSubtraction;
......@@ -83,27 +84,26 @@ import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Z3Exception;
import com.microsoft.z3.Z3javaAPIWrapper;
/**
* Transforms an {@link IExpression} into a z3 {@link Expr} via the z3 API.
* Transforms an {@link IExpression} into a z3 {@link Expr} via the Z3 API.
* This transformations unfolds any given {@link IBinderExpression} e.g. a quantifier.
*
* @author eder
*/
public class ConstraintToNONQuantifiedSMT {
public class ConstraintToNonQuantifiedSMT {
/** The Z3 context. */
private Context context;
/** Transformation Service instance. */
private final IDSMLTransformationService TRANSFORM_INST;
private final IDSMLTransformationService transformationService;
/** Constructor. */
public ConstraintToNONQuantifiedSMT(Context context,
public ConstraintToNonQuantifiedSMT(Context context,
IDSMLTransformationService transformationService) {
this.context = context;
this.TRANSFORM_INST = transformationService;
this.transformationService = transformationService;
}
/** Transforms the given {@link IBooleanExpression} into a z3 {@link BoolExpr}. */
......@@ -254,8 +254,8 @@ public class ConstraintToNONQuantifiedSMT {
if(((ModelElementPropertyLiteral)expression).getSetReference().getEntries()
.contains(e)) {
ArithExpr z3Function =
TRANSFORM_INST
.getZ3Function((ModelElementPropertyLiteral)expression, e);
transformationService.getZ3Function(
(ModelElementPropertyLiteral)expression, e);
return z3Function;
}
}
......@@ -263,7 +263,7 @@ public class ConstraintToNONQuantifiedSMT {
" cannot be resolved.");
} else if(expression instanceof ArithmeticLiteral) {
final String string = ((ArithmeticLiteral)expression).getValue().toString();
return Z3javaAPIWrapper.createReal(context, string);
return createReal(context, string);
}
throw new UnsupportedOperationException("There is no arithmetic expression '" +
expression.getClass().getSimpleName() + "' implemented.");
......@@ -271,7 +271,7 @@ public class ConstraintToNONQuantifiedSMT {
/** Returns the {@link ArithExpr} concerning the annotation of the model element. */
public Expr getZ3EnumInstance(IModelElement element) throws Z3Exception {
return TRANSFORM_INST.getModelElementInstance(element);
return transformationService.getModelElementInstance(element);
}
/**
......@@ -303,8 +303,8 @@ public class ConstraintToNONQuantifiedSMT {
ModelElementLiteral rightDest, IModelElement sourceModel,
IModelElement destinationModel) throws Z3Exception,
UnsupportedDataTypeException {
Expr source = TRANSFORM_INST.getModelElementInstance(sourceModel);
Expr destination = TRANSFORM_INST.getModelElementInstance(destinationModel);
Expr source = transformationService.getModelElementInstance(sourceModel);
Expr destination = transformationService.getModelElementInstance(destinationModel);
if(leftSource instanceof IFunction) {
source = createFunctionExpression((IFunction)leftSource, sourceModel);
......@@ -313,7 +313,7 @@ public class ConstraintToNONQuantifiedSMT {
destination = createFunctionExpression((IFunction)rightDest, destinationModel);
}
FuncDecl alloc = TRANSFORM_INST.getAllocFunctionForLeftSideType(sourceModel);
FuncDecl alloc = transformationService.getAllocFunctionForLeftSideType(sourceModel);
Expr apply = alloc.apply(source);
return createEqual(context, apply, destination);
}
......@@ -322,45 +322,47 @@ public class ConstraintToNONQuantifiedSMT {
private Expr createFunctionExpression(IFunction function, IModelElement... modelElements)
throws UnsupportedDataTypeException {
if(function instanceof Start) {
final FuncDecl z3FunctionDecl = TRANSFORM_INST.getZ3FunctionDecl((Start)function);
final FuncDecl z3FunctionDecl =
transformationService.getZ3FunctionDecl((Start)function);
for(IModelElement m : modelElements) {
Set<IModelElement> startSet = ((Start)function).getArgs().getSetReference();
if(startSet.getEntries().contains(m)) {
Expr source = TRANSFORM_INST.getModelElementInstance(m);
Expr source = transformationService.getModelElementInstance(m);
return z3FunctionDecl.apply(source);
}
}
} else if(function instanceof End) {
final FuncDecl z3FunctionDecl = TRANSFORM_INST.getZ3FunctionDecl((End)function);
final FuncDecl z3FunctionDecl = transformationService.getZ3FunctionDecl((End)function);
for(IModelElement m : modelElements) {
Set<IModelElement> endSet = ((End)function).getArgs().getSetReference();
if(endSet.getEntries().contains(m)) {
Expr source = TRANSFORM_INST.getModelElementInstance(m);
Expr source = transformationService.getModelElementInstance(m);
return z3FunctionDecl.apply(source);
}
}
} else if(function instanceof Uses) {
final FuncDecl z3FunctionDecl = TRANSFORM_INST.getZ3FunctionDecl((Uses)function);
final FuncDecl z3FunctionDecl = transformationService.getZ3FunctionDecl((Uses)function);
Expr source0 = null;
Expr source1 = null;
for(IModelElement m : modelElements) {
Set<IModelElement> usesSet0 = ((Uses)function).getArg0().getSetReference();
if(usesSet0.getEntries().contains(m)) {
source0 = TRANSFORM_INST.getModelElementInstance(m);
source0 = transformationService.getModelElementInstance(m);
} else {
Set<IModelElement> usesSet1 = ((Uses)function).getArg1().getSetReference();
if(usesSet1.getEntries().contains(m)) {
source1 = TRANSFORM_INST.getModelElementInstance(m);
source1 = transformationService.getModelElementInstance(m);
}
}
}
return z3FunctionDecl.apply(source0, source1);
} else if(function instanceof Weight) {
final FuncDecl z3FunctionDecl = TRANSFORM_INST.getZ3FunctionDecl((Weight)function);
final FuncDecl z3FunctionDecl =
transformationService.getZ3FunctionDecl((Weight)function);
for(IModelElement m : modelElements) {
Set<IModelElement> weightSet = ((Weight)function).getArg0().getSetReference();
if(weightSet.getEntries().contains(m)) {
Expr source = TRANSFORM_INST.getModelElementInstance(m);
Expr source = transformationService.getModelElementInstance(m);
return z3FunctionDecl.apply(source);
}
}
......
......@@ -25,6 +25,7 @@ import static com.microsoft.z3.Z3javaAPIWrapper.createGreater;
import static com.microsoft.z3.Z3javaAPIWrapper.createGreaterEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createIfThenElse;
import static com.microsoft.z3.Z3javaAPIWrapper.createImplication;
import static com.microsoft.z3.Z3javaAPIWrapper.createInteger;
import static com.microsoft.z3.Z3javaAPIWrapper.createMultiplication;
import static com.microsoft.z3.Z3javaAPIWrapper.createNot;
import static com.microsoft.z3.Z3javaAPIWrapper.createOr;
......@@ -86,7 +87,6 @@ import com.microsoft.z3.IntNum;
import com.microsoft.z3.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Z3Exception;
import com.microsoft.z3.Z3javaAPIWrapper;
/**
* Transformation of the DSL to SMT by using SMT (enum) data types and quantifiers.
......@@ -100,12 +100,13 @@ public class ConstraintToQuantifiedSMT {
private Context context;
/** Transformation Service instance. */
private final IDSMLTransformationService TRANSFORM_INST;
private final IDSMLTransformationService transformationService;
/** Constructor. */
public ConstraintToQuantifiedSMT(Context context, IDSMLTransformationService transformationService) {
public ConstraintToQuantifiedSMT(Context context,
IDSMLTransformationService transformationService) {
this.context = context;
this.TRANSFORM_INST = transformationService;
this.transformationService = transformationService;
}
/** Transforms the given {@link IBooleanExpression} into a z3 {@link BoolExpr}. */
......@@ -156,8 +157,8 @@ public class ConstraintToQuantifiedSMT {
private ArithExpr getZ3Function(Context context, ModelElementPropertyLiteral arithExpr) {
String name = getFunctionName(arithExpr);
Set<IModelElement> setReference = arithExpr.getSetReference();
Sort sort = TRANSFORM_INST.getExistingSorts().get(setReference);
Expr element = TRANSFORM_INST.getExistingSymbols().get(sort);
Sort sort = transformationService.getExistingSorts().get(setReference);
Expr element = transformationService.getExistingSymbols().get(sort);
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
return (ArithExpr)function.apply(element);
}
......@@ -170,7 +171,7 @@ public class ConstraintToQuantifiedSMT {
IModelElement model) {
String name = getFunctionName(arithExpr);
Set<IModelElement> setReference = arithExpr.getSetReference();
EnumSort sort = TRANSFORM_INST.getExistingSorts().get(setReference);
EnumSort sort = transformationService.getExistingSorts().get(setReference);
String uniqueModelName = createUniqueModelName(model);
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
for(Expr element : sort.getConsts()) {
......@@ -222,18 +223,18 @@ public class ConstraintToQuantifiedSMT {
ModelElementLiteral rightModel = expression.getRight();
Expr leftElement, rightElement;
EnumSort leftSort = TRANSFORM_INST.getSort(leftModel.getSetReference());
EnumSort rightSort = TRANSFORM_INST.getSort(rightModel.getSetReference());
EnumSort leftSort = transformationService.getSort(leftModel.getSetReference());
EnumSort rightSort = transformationService.getSort(rightModel.getSetReference());
if(leftModel instanceof IFunction) {
leftElement = toSMTFunction((IFunction)leftModel);
} else {
leftElement = TRANSFORM_INST.getExistingSymbols().get(leftSort);
leftElement = transformationService.getExistingSymbols().get(leftSort);
}
if(rightModel instanceof IFunction) {
rightElement = toSMTFunction((IFunction)rightModel);
} else {
rightElement = TRANSFORM_INST.getExistingSymbols().get(rightSort);
rightElement = transformationService.getExistingSymbols().get(rightSort);
}
if(expression instanceof Allocation) {
return createAllocationExpression(leftElement, leftSort, rightElement, rightSort);
......@@ -244,18 +245,18 @@ public class ConstraintToQuantifiedSMT {
/** Returns the respective z3 symbol for this literal. */
private Expr toModelLiteral(ModelElementLiteral expression) {
Set<?> setReference = expression.getSetReference();
EnumSort sort = TRANSFORM_INST.getSort(setReference);
return TRANSFORM_INST.getExistingSymbols().get(sort);
EnumSort sort = transformationService.getSort(setReference);
return transformationService.getExistingSymbols().get(sort);
}
/** Returns the given function as an {@link Expr} (applied {@link FuncDecl}). */
private Expr toSMTFunction(IFunction function) throws UnsupportedDataTypeException {
if(function instanceof Start) {
return TRANSFORM_INST.getZ3Function((Start)function);
return transformationService.getZ3Function((Start)function);
} else if(function instanceof End) {
return TRANSFORM_INST.getZ3Function((End)function);
return transformationService.getZ3Function((End)function);
} else if(function instanceof Weight) {
return TRANSFORM_INST.getZ3Function((Weight)function);
return transformationService.getZ3Function((Weight)function);
}
throw new UnsupportedDataTypeException("The type " + function.getClass().getSimpleName() +
" is not implemented yet.");
......@@ -299,7 +300,7 @@ public class ConstraintToQuantifiedSMT {
*/
private BoolExpr createAllocationExpression(Expr leftElement, EnumSort leftSort,
Expr rightElement, EnumSort rightSort) {
FuncDecl allocate = TRANSFORM_INST.getAllocateFunction(leftSort, rightSort);
FuncDecl allocate = transformationService.getAllocateFunction(leftSort, rightSort);
Expr apply = allocate.apply(leftElement);
return createEqual(context, apply, rightElement);
}
......@@ -307,9 +308,9 @@ public class ConstraintToQuantifiedSMT {
/** Transforms {@link ForAll} and {@link Exists} into a SMT {@link Quantifier}. */
private Expr toSMTQuantor(IBinderExpression expression) throws UnsupportedDataTypeException,
Z3Exception {
EnumSort sort = TRANSFORM_INST.getSort(expression.getSet());
EnumSort sort = transformationService.getSort(expression.getSet());
Expr body = toSMT(expression.getExpression());
Expr expr = TRANSFORM_INST.getExistingSymbols().get(sort);
Expr expr = transformationService.getExistingSymbols().get(sort);
final Expr[] boundSorts = new Expr[] {expr};
if(expression instanceof ForAll) {
......@@ -326,8 +327,8 @@ public class ConstraintToQuantifiedSMT {
* all statements as a SMT {@link ArithExpr}.
*/
private Expr toSMTsum(Sum sum) throws UnsupportedDataTypeException, Z3Exception {
EnumSort sort = TRANSFORM_INST.getSort(sum.getSet());
final IntNum ZERO = Z3javaAPIWrapper.createInteger(context, 0);
EnumSort sort = transformationService.getSort(sum.getSet());
final IntNum ZERO = createInteger(context, 0);
ArrayList<ArithExpr> sumTerms = new ArrayList<>();
for(Expr element : sort.getConsts()) {
IBooleanExpression expression = sum.getExpression();
......@@ -356,15 +357,15 @@ public class ConstraintToQuantifiedSMT {
leftElement = element;
leftSort = sort;
} else {
leftSort = TRANSFORM_INST.getSort(leftModel.getSetReference());
leftElement = TRANSFORM_INST.getExistingSymbols().get(leftSort);
leftSort = transformationService.getSort(leftModel.getSetReference());
leftElement = transformationService.getExistingSymbols().get(leftSort);
}
if(rightModel.getSetReference().equals(sum.getSet())) {
rightElement = element;
rightSort = sort;
} else {
rightSort = TRANSFORM_INST.getSort(rightModel.getSetReference());
rightElement = TRANSFORM_INST.getExistingSymbols().get(rightSort);
rightSort = transformationService.getSort(rightModel.getSetReference());
rightElement = transformationService.getExistingSymbols().get(rightSort);
}
if(expression instanceof Allocation) {
locExpr =
......
......@@ -17,6 +17,7 @@ package org.fortiss.af3.exploration.smt.modeltransformation.rework;
import static com.microsoft.z3.Z3javaAPIWrapper.createEnumSort;
import static com.microsoft.z3.Z3javaAPIWrapper.createFunction;
import static com.microsoft.z3.Z3javaAPIWrapper.createSymbol;
import static org.fortiss.af3.exploration.smt.modeltransformation.rework.SMTTransformationUtils.createSymbol;
import static org.fortiss.af3.exploration.smt.modeltransformation.rework.SMTTransformationUtils.createUniqueModelName;
import static org.fortiss.af3.exploration.smt.modeltransformation.rework.SMTTransformationUtils.getFunctionName;
......@@ -54,10 +55,9 @@ import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Symbol;
import com.microsoft.z3.Z3javaAPIWrapper;
/**
* Transformation service used for translating any {@link IExpression} into SMT
* Transformation service used for translating any {@link IExpression} into SMT.
*
* @author eder
*/
......@@ -99,8 +99,7 @@ public class DSMLTransformationService implements IDSMLTransformationService {
return;
}
// Set cannot not be null.
Symbol type =
Z3javaAPIWrapper.createSymbol(context, entries.get(0).getClass().getSimpleName());
Symbol type = createSymbol(context, entries.get(0).getClass().getSimpleName());
for(IModelElement m : entries) {
Symbol symbol = createSymbol(context, m);
symbols.add(symbol);
......@@ -293,7 +292,6 @@ public class DSMLTransformationService implements IDSMLTransformationService {
existingSorts.entrySet();
for(Entry<Set<? extends IModelElement>, EnumSort> e : entrySet) {
for(Expr element : e.getValue().getConsts()) {
// if(element.toString().equals(expr.toString())) {
if(expr.toString().equals(element.toString()) ||
expr.toString().equals("|" + element.toString() + "|")) {
Predicate<? super IModelElement> namePred =
......
......@@ -27,6 +27,7 @@ import static org.fortiss.tooling.common.util.LambdaUtils.filter;
import static org.fortiss.tooling.common.util.LambdaUtils.getFirst;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.warning;
import java.util.ArrayList;
import java.util.Collection;
......@@ -86,7 +87,6 @@ import org.fortiss.tooling.base.model.element.IModelElementSpecification;
import org.fortiss.tooling.common.util.LambdaUtils;
import org.fortiss.tooling.kernel.extension.data.ITopLevelElement;
import org.fortiss.tooling.kernel.service.IPersistencyService;
import org.fortiss.tooling.kernel.utils.LoggingUtils;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
......@@ -102,8 +102,6 @@ import com.microsoft.z3.Z3Exception;
*
* @author eder
*/
// TODO(AD): Maybe a more specific class name would be useful since "LanguageTransformation" is very
// general.
public class DSMLtoSMTTransformator {
/** The objectives and constraints to be transformed into SMT. */
private ExplorationSpecification explorationSpec;
......@@ -115,7 +113,7 @@ public class DSMLtoSMTTransformator {
private ConstraintToQuantifiedSMT basicQuantifiedTransformation;
/** Basic non quantfied transformation. */
private ConstraintToNONQuantifiedSMT genericNonQuantifiedTransformation;
private ConstraintToNonQuantifiedSMT genericNonQuantifiedTransformation;
/** Transformation Service instance to be used. */
private IDSMLTransformationService transformationService;
......@@ -168,7 +166,7 @@ public class DSMLtoSMTTransformator {
basicQuantifiedTransformation =
new ConstraintToQuantifiedSMT(context, transformationService);
genericNonQuantifiedTransformation =
new ConstraintToNONQuantifiedSMT(context, transformationService);
new ConstraintToNonQuantifiedSMT(context, transformationService);
for(ExplorationTarget<?> dslExpression : explorationSpec.getTargets()) {
try {
......@@ -252,7 +250,7 @@ public class DSMLtoSMTTransformator {
}
/**
* Pre processing. Currently only used for Bus elimination objective. Basically this methods
* Pre-processing. Currently only used for Bus elimination objective. Basically this methods
* removes all routes from all used sets that use the bus, which should be eliminated.
*/
@SuppressWarnings({"unchecked", "rawtypes"})
......@@ -499,7 +497,7 @@ public class DSMLtoSMTTransformator {