Commit 09ea3031 authored by Tiziano Munaro's avatar Tiziano Munaro
Browse files

Adapt DSML translation to use real values where necessary

Issue-Ref: 4052
Issue-Url: https://af3-developer.fortiss.org/issues/4052

Signed-off-by: Tiziano Munaro's avatarTiziano Munaro <munaro@fortiss.org>
parent 835d1c90
AF3z3Activator.java 3b41854f824afc76c3f804e627ca24dc438df758 GREEN
Z3Type.java 73e319ae206d2fd456ec9430c01b5ff7fc7282d0 GREEN
Z3javaAPIWrapper.java d21fa89f50dd9afe49eaad0901384bdf99df548f GREEN
Z3javaAPIWrapper.java 563486b7205451cdb994e8aed70667f04b37239b YELLOW
......@@ -234,6 +234,14 @@ public class Z3javaAPIWrapper {
/** Returns an {@link ArithExpr}: <i>expr1 / expr2</i>. */
public static ArithExpr createDivision(Context context, ArithExpr expr1, ArithExpr expr2)
throws Z3Exception {
// By default, the context.mkDiv function casts real values to integer ones in a situation
// of mixed types. Here we enforce the behavior known from all major programming languages,
// where a division with a real term is executed as a floating point division.
if(expr1 instanceof RealExpr && expr2 instanceof IntExpr) {
expr2 = context.mkInt2Real((IntExpr)expr2);
} else if(expr1 instanceof IntExpr && expr2 instanceof RealExpr) {
expr1 = context.mkInt2Real((IntExpr)expr1);
}
return context.mkDiv(expr1, expr2);
}
......
BasicDeploScheduleConstraint.java 76029b866e82f7fcbb78292e366a41d39ad86cdc GREEN
BasicDeploymentConstraint.java bd66d1e997b091ddd28423529de5a5c23af1bee9 GREEN
BasicScheduleConstraint.java 8b054b5ad961295b97936e26240eb33a10a1ee9a GREEN
ConstraintDefinitionUtils.java 8a709a9cd10edd36d1ac3ed0ded0c938aa010f12 GREEN
ConstraintDefinitionUtils.java 5bac39f6a9c1299bc1dcc2a655496d4def646efc YELLOW
ConstraintTransformationAdapter.java 8806164d71491c7d1af665990dd154f2275cad8c GREEN
DSMLTransformationService.java 2c19395bffa10cdaf2e7f38fdb592254289e659c GREEN
DSMLtoSMTTransformator.java 32431ae9bcbca84d1c7cb9726f77af67019da250 GREEN
DefaultExpressionTransformator.java 9f572be21d1d96bc3d7604695678e57035a1b82e GREEN
DSMLTransformationService.java 7869a480c0fccb5f75677b392a5d1dd1a3328b5c YELLOW
DSMLtoSMTTransformator.java 0e750ee0a344b1913774d1a83a8568ff09f49436 YELLOW
DefaultExpressionTransformator.java 34733e33b3a55eef0fdda724b74fe181beaa7f2d YELLOW
DeploScheduleRun.java 2b07bd6b40cf4ce2eabc12198f6db3b9655bed25 GREEN
DeploymentRun.java 4b2d0a6d64bb5a6efabc2ee9bf933cc523843ac8 GREEN
EnergyConstraintDefinition.java cc18ecec975ce706ebcb83e282c9a17fe4608596 GREEN
ExpressionTransformator.java 81dfc30221e519aa8175693353ace8992687327f GREEN
IDSMLTransformationService.java 4c5bd9a06d74e31823bd8ef586687cbb344291e0 GREEN
IDSMLTransformationService.java 0bbcefa52d1127250697ca3d92a1b810db1b8871 YELLOW
NonQuantifiedExpressionTransformator.java 9ee437aeaf518d94b81e34a275cd01b87cfca1bf GREEN
QuantifiedExpressionTransformator.java 01e7162b24d16adb23f646cf02340879e8a18205 GREEN
SMTTransformationUtils.java 376da0f5dafb350b49004c7d75fb8858b53d3b7d GREEN
SMTTransformationUtils.java 14f70ea23c0589b5105dae9f7034a99eb3f72606 YELLOW
ScheduleRun.java 43d869a9adfbebe34c34f1ebb0bc8e0600f45b9d GREEN
SolverRun.java ff3c69cf4fed2007f7f6bbeaefb4a2343d3c2e8d YELLOW
TimingConstraintDefinition.java 92281277d99bb52b72c1cb898bba944b3b9a24f7 GREEN
......@@ -172,7 +172,7 @@ public class ConstraintDefinitionUtils {
// Create a arithmetic property literal representing an arithmetic decision variable. Its
// name is used to create a "floating" function in Z3 and the extraction of the assigned
// values from the resulting model.
return createArithmeticPropertyLiteral(set, null, START_TIME_IDENTIFIER);
return createArithmeticPropertyLiteral(set, ra -> new BigDecimal(0), START_TIME_IDENTIFIER);
}
/** For the given set of {@link ResourceAllocation}, creates a corresponding duration set. */
......@@ -181,7 +181,7 @@ public class ConstraintDefinitionUtils {
// Create a arithmetic property literal representing an arithmetic decision variable. Its
// name is used to create a "floating" function in Z3 and the extraction of the assigned
// values from the resulting model.
return createArithmeticPropertyLiteral(set, null, DURATION_IDENTIFIER);
return createArithmeticPropertyLiteral(set, ra -> new BigDecimal(0), DURATION_IDENTIFIER);
}
/**
......
......@@ -162,9 +162,9 @@ public class DSMLTransformationService implements IDSMLTransformationService {
* name.
*/
private ArithExpr getZ3FunctionForModelElement(Context context, IModelElement modelElement,
String name, EnumSort sort) {
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
for(Expr element : sort.getConsts()) {
String name, EnumSort inputSort, Sort outputSort) {
FuncDecl function = createFunction(context, name, inputSort, outputSort);
for(Expr element : inputSort.getConsts()) {
if(element.equals(existingInstances.get(modelElement))) {
return (ArithExpr)function.apply(element);
}
......@@ -176,9 +176,9 @@ public class DSMLTransformationService implements IDSMLTransformationService {
@Override
public ArithExpr getZ3Function(
ArithmeticPropertyLiteral<? extends IModelElement, Number> arithExpr,
IModelElement model) {
IModelElement model, Sort outputSort) {
String name = getFunctionName(arithExpr);
return getZ3FunctionForModelElement(context, model, name, getSort(model));
return getZ3FunctionForModelElement(context, model, name, getSort(model), outputSort);
}
/** {@inheritDoc} */
......
......@@ -27,6 +27,8 @@ import static org.fortiss.af3.exploration.smt.modeltransformation.ConstraintDefi
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.DURATION_IDENTIFIER;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.START_TIME_IDENTIFIER;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.getFunctionName;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.toDecimal;
import static org.fortiss.af3.exploration.util.DSMLUtils.isReal;
import static org.fortiss.af3.exploration.util.ExplorationUtils.isDebugVerboseEnabled;
import static org.fortiss.af3.schedule.utils.AF3ScheduleModelElementFactory.createResourceSchedule;
import static org.fortiss.tooling.common.util.LambdaUtils.filter;
......@@ -36,8 +38,6 @@ 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.math.BigDecimal;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
......@@ -84,7 +84,6 @@ import com.microsoft.z3.Context;
import com.microsoft.z3.EnumSort;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Model;
import com.microsoft.z3.RatNum;
import com.microsoft.z3.Z3Exception;
......@@ -289,19 +288,19 @@ public class DSMLtoSMTTransformator {
// searches for the starting time and duration values in the model
Expr startExpr = startFun.apply(m.getValue());
IntNum startNum = (IntNum)model.eval(startExpr, true);
RatNum startNum = (RatNum)model.eval(startExpr, true);
Expr durationExpr = durationFun.apply(m.getValue());
IntNum durationNum = (IntNum)model.eval(durationExpr, true);
RatNum durationNum = (RatNum)model.eval(durationExpr, true);
// Create output resource allocations (input set is not writable)
ResourceAllocation outResAlloc = copy(inResAlloc);
// Adds information extracted from the solution to the new resource allocation
PeriodicTimeTrigger periodicTimeTrigger = (PeriodicTimeTrigger)outResAlloc.getTrigger();
periodicTimeTrigger.setStartTime(new BigDecimal(startNum.getBigInteger()));
periodicTimeTrigger.setStartTime(toDecimal(startNum));
PeriodicTimeTrigger inputTrigger = (PeriodicTimeTrigger)inResAlloc.getTrigger();
periodicTimeTrigger.setPeriod(inputTrigger.getPeriod());
outResAlloc.setDuration(new BigDecimal(durationNum.getBigInteger()));
outResAlloc.setDuration(toDecimal(durationNum));
resAllList.add(outResAlloc);
}
......@@ -445,17 +444,13 @@ public class DSMLtoSMTTransformator {
List<? extends IModelElement> modelElements = aPLit.getSetReference().getEntries();
for(IModelElement modelElement : modelElements) {
Number value = aPLit.getValue(modelElement);
Expr valueExpr = null;
if(value instanceof Integer || value instanceof BigInteger ||
value instanceof Byte || value instanceof Short || value instanceof Long) {
valueExpr = createInteger(context, value.intValue());
} else if(value instanceof BigDecimal || value instanceof Double ||
value instanceof Float) {
valueExpr = createReal(context, value.toString());
}
boolean isReal = isReal(value);
Expr valueExpr = isReal ? createReal(context, value.toString())
: createInteger(context, value.intValue());
if(valueExpr != null) {
ArithExpr z3Function = transformationService.getZ3Function(aPLit, modelElement);
ArithExpr z3Function = transformationService.getZ3Function(aPLit, modelElement,
valueExpr.getSort());
final BoolExpr createEqual = createEqual(context, z3Function, valueExpr);
Collection<BoolExpr> filter2 =
......
......@@ -32,6 +32,7 @@ import static com.microsoft.z3.Z3javaAPIWrapper.createSmaller;
import static com.microsoft.z3.Z3javaAPIWrapper.createSmallerEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createSubtraction;
import static org.fortiss.af3.exploration.smt.modeltransformation.SMTTransformationUtils.getFunctionName;
import static org.fortiss.af3.exploration.util.DSMLUtils.isReal;
import java.util.Map;
......@@ -83,6 +84,7 @@ import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.EnumSort;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.Sort;
import com.microsoft.z3.Z3Exception;
/**
......@@ -143,16 +145,26 @@ public class DefaultExpressionTransformator extends ExpressionTransformator {
}
/** Returns an {@link ArithExpr} for the given {@link ArithmeticPropertyLiteral}. */
private ArithExpr getZ3Function(
ArithmeticPropertyLiteral<? extends IModelElement, ? extends Number> arithExpr,
private <S extends IModelElement> ArithExpr getZ3Function(
ArithmeticPropertyLiteral<S, ? extends Number> arithExpr,
Map<Set<IModelElement>, IModelElement> modelElements)
throws UnsupportedDataTypeException, Z3Exception {
String name = getFunctionName(arithExpr);
Set<? extends IModelElement> setReference = arithExpr.getSetReference();
Set<? extends IModelElement> superSetReference = setReference.getSuperSetReference();
EnumSort sort = transformationService.getExistingSorts().get(superSetReference);
Set<S> setReference = arithExpr.getSetReference();
Set<S> superSetReference = setReference.getSuperSetReference();
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
//@CodeFormatterOff
@SuppressWarnings("unchecked")
boolean isReal = modelElements.values().stream()
.filter(me -> setReference.getEntryType().isAssignableFrom(me.getClass()))
.map(me -> arithExpr.getValue((S)me))
.anyMatch(value -> isReal(value));
//@CodeFormatterOn
EnumSort inputSort = transformationService.getExistingSorts().get(superSetReference);
Sort outputSort = isReal ? context.getRealSort() : context.getIntSort();
FuncDecl function = createFunction(context, name, inputSort, outputSort);
return (ArithExpr)function.apply(getLiteralExpr(modelElements, arithExpr));
}
......
......@@ -58,7 +58,7 @@ public interface IDSMLTransformationService {
* the given {@link IModelElement}.
*/
ArithExpr getZ3Function(ArithmeticPropertyLiteral<? extends IModelElement, Number> arithExpr,
IModelElement model);
IModelElement model, Sort outputSort);
/** Returns the existing {@link Sort}s instances for the respective {@link IModelElement}s. */
Map<Set<? extends IModelElement>, EnumSort> getExistingSorts();
......
......@@ -17,6 +17,7 @@ package org.fortiss.af3.exploration.smt.modeltransformation;
import static java.lang.Character.isDigit;
import java.math.BigDecimal;
import java.text.Normalizer;
import org.fortiss.af3.exploration.dseml.model.expression.IPropertyLiteral;
......@@ -24,6 +25,7 @@ import org.fortiss.tooling.base.model.element.IModelElement;
import org.fortiss.tooling.kernel.model.INamedElement;
import com.microsoft.z3.Context;
import com.microsoft.z3.RatNum;
import com.microsoft.z3.Symbol;
import com.microsoft.z3.Z3javaAPIWrapper;
......@@ -103,4 +105,13 @@ public class SMTTransformationUtils {
modelNameASCII = modelNameASCII.replace(";", "");
return modelNameASCII;
}
/**
* Converts a {@link RatNum} to a {@link BigDecimal} by dividing its numerator and denominator.
*/
public static BigDecimal toDecimal(RatNum rationalNumber) {
double numerator = rationalNumber.getBigIntNumerator().doubleValue();
double denominator = rationalNumber.getBigIntDenominator().doubleValue();
return new BigDecimal(numerator / denominator);
}
}
ExpressionStaticImpl.java 58ee22ff265d2939bfde2c89feec67620e10fdc5 GREEN
IPropertyLiteralStaticImpl.java 60668b095effeff7421ac03ad0b18285db23afd4 GREEN
IPropertyLiteralStaticImpl.java 15971f6ae1e0dfd74b78c97655e8971e968eb804 YELLOW
SetStaticImpl.java 56445fcfdbbfb9ad341cea430b4168ed7002bfb3 GREEN
SuperSetStaticImpl.java 6de608c5a2bb0847a3119ae5218a1cf9a86c250c GREEN
......@@ -45,7 +45,7 @@ public class IPropertyLiteralStaticImpl {
* {@link IModelElement} to query.
* @return The "property" of the element.
*/
public static <T extends IModelElement, R, L extends IPropertyLiteral<T, R>> R
public static <T extends IModelElement, R> R
getValue(IPropertyLiteral<T, ?> modelElementPropertyLiteralImpl, T element) {
EAttribute getterFeature = ExpressionPackage.eINSTANCE.getIPropertyLiteral_GetterMethod();
@SuppressWarnings("unchecked") Function<T, R> getter =
......
DSEProjectModelElementFactory.java fcedc4eb7da9f08bd5682c23d5e29c0f81f9f0db GREEN
DSESolutionConversionUtils.java a6ccbba92864c653d1518a92455e87c17f7cc72b GREEN
DSMLModelElementFactory.java 8081a2d7e2a1ee311b830305854bb60bb7572d91 GREEN
DSMLUtils.java c07eeef09787cea9db98533d346e3e384a232593 GREEN
DSMLUtils.java 1113377031374cef7e29afcef458c4aeecad2b21 YELLOW
ExplorationCLIUtils.java 84ca98376ec32613396f1c26910a83179f4b3db1 GREEN
ExplorationReflectionUtils.java 62731e1cef32fe93f2c2017f93f5ba1f054d5197 GREEN
ExplorationUtils.java 00da54dcf0441295d0453683a159c05bf2a8e884 GREEN
......
......@@ -15,6 +15,9 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.util;
import java.math.BigDecimal;
import java.math.BigInteger;
/**
* Utility methods for the constraint DSL.
*
......@@ -36,4 +39,16 @@ public class DSMLUtils {
}
return s.substring(0, 1).toLowerCase();
}
/** Checks whether a {@link Number} represents a real number or not. */
public static boolean isReal(Number value) {
if(value instanceof Integer || value instanceof BigInteger || value instanceof Byte ||
value instanceof Short || value instanceof Long) {
return false;
} else if(value instanceof BigDecimal || value instanceof Double ||
value instanceof Float) {
return true;
}
throw new UnsupportedOperationException("The type of the `Number` value is not supported.");
}
}
Markdown is supported
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