Commit bfca7359 authored by Johannes Eder's avatar Johannes Eder
Browse files

Transformation of DSL into SMT by using SMT custom data types and quantifiers.

refs 2914
parent 814e85cf
......@@ -17,14 +17,395 @@ $Id: codetemplates.xml 1 2011-01-01 00:00:01Z hoelzl $
+--------------------------------------------------------------------------*/
package org.fortiss.af3.exploration.smt.modeltransformation;
import static com.microsoft.z3.Z3javaAPIWrapper.createAddition;
import static com.microsoft.z3.Z3javaAPIWrapper.createAnd;
import static com.microsoft.z3.Z3javaAPIWrapper.createBoolean;
import static com.microsoft.z3.Z3javaAPIWrapper.createDivision;
import static com.microsoft.z3.Z3javaAPIWrapper.createEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createFunction;
import static com.microsoft.z3.Z3javaAPIWrapper.createGreater;
import static com.microsoft.z3.Z3javaAPIWrapper.createGreaterEqual;
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;
import static com.microsoft.z3.Z3javaAPIWrapper.createSmaller;
import static com.microsoft.z3.Z3javaAPIWrapper.createSmallerEqual;
import static com.microsoft.z3.Z3javaAPIWrapper.createSubtraction;
import java.util.ArrayList;
import java.util.HashMap;
import javax.activation.UnsupportedDataTypeException;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.ArithmeticLiteral;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.Div;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.IArithmeticExpression;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.Minus;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.ModelElementPropertyLiteral;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.Mul;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.Plus;
import org.fortiss.af3.exploration.dsl_v2.model.arithmetic.Sum;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.And;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.BooleanLiteral;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.Exists;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.ForAll;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.IBooleanExpression;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.Implies;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.Not;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.Or;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.allocation.Allocation;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.allocation.ILocationExpression;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.Equal;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.Greater;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.GreaterEqual;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.IComparisonExpression;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.Less;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.LessEqual;
import org.fortiss.af3.exploration.dsl_v2.model.booleanp.comparison.NotEqual;
import org.fortiss.af3.exploration.dsl_v2.model.expression.IBinaryOperator;
import org.fortiss.af3.exploration.dsl_v2.model.expression.IBinderExpression;
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.dsl_v2.model.expression.Set;
import org.fortiss.tooling.base.model.element.IAnnotatedSpecification;
import org.fortiss.tooling.base.model.element.IModelElement;
import org.fortiss.tooling.kernel.model.INamedElement;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
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.Quantifier;
import com.microsoft.z3.Sort;
import com.microsoft.z3.StringSymbol;
import com.microsoft.z3.Symbol;
import com.microsoft.z3.Z3Exception;
import com.microsoft.z3.Z3javaAPIWrapper;
/**
* Transformation of the DSL to SMT by suing SMT data types and quantifiers
* Transformation of the DSL to SMT by using SMT (enum) data types and quantifiers
*
* @author eder
* @author $Author: hoelzl $
* @author $Author: eder $
* @version $Rev: 18709 $
* @ConQAT.Rating RED Hash:
*/
public class DSLToSMT2 {
/** DSL SET to SMT Sort mapping */
private HashMap<Set, Sort> existingSorts = new HashMap<>();
/** Sort to referring symbol mapping. */
private HashMap<Sort, Expr> existingSymbols = new HashMap<>();
/** Transforms the given {@link IBooleanExpression} into a z3 {@link BoolExpr}. */
public Expr toSMT(Context context, IExpression expression) throws UnsupportedDataTypeException,
Z3Exception {
if(expression instanceof ForAll || expression instanceof Exists) {
return toSMTQuantor(context, (IBinderExpression)expression);
} else if(expression instanceof Sum) {
return toSMTsum(context, (Sum)expression);
} else if(expression instanceof IBooleanExpression) {
return toSMTBoolean(context, (IBooleanExpression)expression);
} else if(expression instanceof IArithmeticExpression) {
return toSMTArithmetic(context, (IArithmeticExpression)expression);
}
throw new UnsupportedDataTypeException("Unkown expression " + expression);
}
/** Transforms an {@link IArithmeticExpression} into an SMT {@link ArithExpr}. */
private Expr toSMTArithmetic(Context context, IArithmeticExpression expression)
throws UnsupportedDataTypeException, Z3Exception {
if(expression instanceof IBinaryOperator<?>) {
Expr left = toSMT(context, ((IBinaryOperator<?>)expression).getLeft());
Expr right = toSMT(context, ((IBinaryOperator<?>)expression).getRight());
if(expression instanceof Plus) {
return createAddition(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof Minus) {
return createSubtraction(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof Div) {
return createDivision(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof Mul) {
return createMultiplication(context, (ArithExpr)left, (ArithExpr)right);
}
} else if(expression instanceof ModelElementPropertyLiteral) {
return getZ3Function(context, (ModelElementPropertyLiteral)expression);
} else if(expression instanceof ArithmeticLiteral) {
// TODO(JE): value is 'casted' into integer. should be turned into a real expression
// in z3. Refs 2666
return createInteger(context, ((ArithmeticLiteral)expression).getValue().intValue());
}
throw new UnsupportedOperationException("There is no arithmetic expression '" +
expression.getClass().getSimpleName() + "' implemented.");
}
/** Returns the {@link ArithExpr} concerning the annotation of the model element. */
private ArithExpr getZ3Function(Context context, ModelElementPropertyLiteral arithExpr) {
String name = getFunctionName(arithExpr);
Set setReference = arithExpr.getSetReference();
Sort sort = existingSorts.get(setReference);
Expr element = existingSymbols.get(sort);
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
return (ArithExpr)function.apply(element);
}
/** Transforms a {@link IBooleanExpression} into a SMT {@link BoolExpr}. */
private Expr toSMTBoolean(Context context, IBooleanExpression expression)
throws UnsupportedDataTypeException, Z3Exception {
if(expression instanceof IBinaryOperator<?>) {
if(expression instanceof ILocationExpression) {
return createLocationExpression(context, (ILocationExpression)expression);
}
Expr left = toSMT(context, ((IBinaryOperator<?>)expression).getLeft());
Expr right = toSMT(context, ((IBinaryOperator<?>)expression).getRight());
if(expression instanceof IComparisonExpression) {
return createComparisonExpression(context, (IComparisonExpression<?>)expression,
left, right);
} else if(expression instanceof And) {
return createAnd(context, (BoolExpr)left, (BoolExpr)right);
} else if(expression instanceof Or) {
return createOr(context, (BoolExpr)left, (BoolExpr)right);
} else if(expression instanceof Implies) {
return createImplication(context, (BoolExpr)left, (BoolExpr)right);
}
} else if(expression instanceof IUnaryOperator<?>) {
Expr right = toSMT(context, ((IUnaryOperator<?>)expression).getRight());
if(expression instanceof Not) {
return createNot(context, (BoolExpr)right);
}
} else if(expression instanceof BooleanLiteral) {
return createBoolean(context, ((BooleanLiteral)expression).isValue());
}
throw new UnsupportedOperationException("There is no boolean expression '" +
expression.getClass().getSimpleName() + "' implemented.");
}
/** Transforms a {@link ILocationExpression} into a SMT {@link BoolExpr}. */
private BoolExpr createLocationExpression(Context context, ILocationExpression expression) {
ModelElementLiteral leftModel = expression.getLeft();
ModelElementLiteral rightModel = expression.getRight();
Sort leftSort = existingSorts.get(leftModel.getSetReference());
Expr leftElement = existingSymbols.get(leftSort);
Sort rightSort = existingSorts.get(rightModel.getSetReference());
Expr rightElement = existingSymbols.get(rightSort);
if(expression instanceof Allocation) {
return createAllocationExpression(context, leftElement, leftSort, rightElement,
rightSort);
}
return createDislocationExpression(context, leftElement, leftSort, rightElement, rightSort);
}
/** Transforms a {@link IComparisonExpression} into a SMT {@link BoolExpr}. */
private BoolExpr createComparisonExpression(Context context,
IComparisonExpression<?> expression, Expr left, Expr right) {
if(expression instanceof Greater) {
return createGreater(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof GreaterEqual) {
return createGreaterEqual(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof Equal) {
return createEqual(context, left, right);
} else if(expression instanceof NotEqual) {
BoolExpr equal = createEqual(context, left, right);
return createNot(context, equal);
} else if(expression instanceof LessEqual) {
return createSmallerEqual(context, (ArithExpr)left, (ArithExpr)right);
} else if(expression instanceof Less) {
return createSmaller(context, (ArithExpr)left, (ArithExpr)right);
}
throw new UnsupportedOperationException("There is no comparison expression '" +
expression.getClass().getSimpleName() + "' implemented.");
}
/**
* Creates a dislocation expression of leftElement (out of a set of leftSort elements) which may
* not be allocated to rightElement (out of a set of rightSort elements).
*/
private BoolExpr createDislocationExpression(Context context, Expr leftElement, Sort leftSort,
Expr rightElement, Sort rightSort) {
FuncDecl allocate = createFunction(context, "allocate", leftSort, rightSort);
Expr apply = allocate.apply(leftElement);
BoolExpr equal = createEqual(context, apply, rightElement);
BoolExpr notEqual = createNot(context, equal);
return notEqual;
}
/**
* Creates a allocation expression of leftElement (out of a set of leftSort elements) which
* shall be allocated to rightElement (out of a set of rightSort elements).
*/
private BoolExpr createAllocationExpression(Context context, Expr leftElement, Sort leftSort,
Expr rightElement, Sort rightSort) {
// TODO: check if function stays the same if it is created a few times with same sorts
FuncDecl allocate = createFunction(context, "allocate", leftSort, rightSort);
Expr apply = allocate.apply(leftElement);
BoolExpr equal = createEqual(context, apply, rightElement);
return equal;
}
/** Transforms {@link ForAll} and {@link Exists} into a SMT {@link Quantifier}. */
private Expr toSMTQuantor(Context context, IBinderExpression expression)
throws UnsupportedDataTypeException, Z3Exception {
EnumSort sort = createEnumSort(context, expression);
createSymbol(context, expression, sort);
Expr body = toSMT(context, expression.getExpression());
Expr expr = existingSymbols.get(sort);
final Expr[] boundSorts = new Expr[] {expr};
if(expression instanceof ForAll) {
Quantifier mkForall = context.mkForall(boundSorts, body, 1, null, null, null, null);
return mkForall;
} else if(expression instanceof Exists) {
Quantifier mkExists = context.mkExists(boundSorts, body, 1, null, null, null, null);
return mkExists;
}
throw new UnsupportedOperationException("There is no quantor expression '" +
expression.getClass().getSimpleName() + "' implemented.");
}
/**
* Creates a generic element {@link Expr} (to be used in quantifiers) of the given
* {@link EnumSort}.
*/
private StringSymbol createSymbol(Context context, IBinderExpression expression, EnumSort sort) {
String setName = expression.getSet().getName();
if(setName != null && setName.length() > 0) {
setName = setName.substring(0, 1).toLowerCase();
} else {
setName = "x";
}
Expr elementOfSort = context.mkConst(setName, sort);
StringSymbol symbol = context.mkSymbol(setName);
existingSorts.put(expression.getSet(), sort);
existingSymbols.put(sort, elementOfSort);
return symbol;
}
/**
* Transforms the {@link Set} of the given {@link IBinderExpression} into a SMT {@link EnumSort}
* .
*/
private EnumSort createEnumSort(Context context, IBinderExpression expression) {
EList<IModelElement> entries = expression.getSet().getEntries();
ArrayList<Symbol> symbols = new ArrayList<>();
if(entries.isEmpty())
throw new UnsupportedOperationException(expression + " contains an empty set.");
// a set must not be empty otherwise a BinderExpression does not make sense
Symbol type =
Z3javaAPIWrapper.createSymbol(context, entries.get(0).getClass().getSimpleName());
int i = 0;
for(IModelElement m : entries) {
Symbol symbol = createSymbol(context, m, i++);
symbols.add(symbol);
}
final Symbol[] array = symbols.toArray(new Symbol[0]);
EnumSort sort = Z3javaAPIWrapper.createEnumSort(context, type, array);
return sort;
}
/**
* In case of {@link Sum}, unfold expression into if-then-else statements and return the sum of
* all statements as a SMT {@link ArithExpr}.
*/
private Expr toSMTsum(Context context, Sum sum) throws UnsupportedDataTypeException,
Z3Exception {
EnumSort sort = createEnumSort(context, sum);
createSymbol(context, sum, sort);
final IntNum ZERO = Z3javaAPIWrapper.createInteger(context, 0);
ArrayList<ArithExpr> sumTerms = new ArrayList<>();
for(Expr element : sort.getConsts()) {
IBooleanExpression expression = sum.getExpression();
ArithExpr arithExpr = null;
if(sum.getTerms() instanceof ModelElementPropertyLiteral) {
ModelElementPropertyLiteral terms = (ModelElementPropertyLiteral)sum.getTerms();
// Expr arithExpr = toSMT(context, sum.getTerms());
String name = getFunctionName(terms);
Set setReference = terms.getSetReference();
if(!setReference.equals(sum.getSet())) {
throw new UnsupportedOperationException("Cannot refer to a set outside a SUM");
}
FuncDecl function = createFunction(context, name, sort, context.getIntSort());
arithExpr = (ArithExpr)function.apply(element);
} else {
throw new UnsupportedDataTypeException("The type " +
sum.getTerms().getClass().getSimpleName() +
" is not supported in SUM expressions");
}
if(expression instanceof ILocationExpression) {
ModelElementLiteral leftModel = ((ILocationExpression)expression).getLeft();
ModelElementLiteral rightModel = ((ILocationExpression)expression).getRight();
Expr leftElement, rightElement;
Sort leftSort, rightSort;
Expr locExpr;
if(leftModel.getSetReference().equals(sum.getSet())) {
leftElement = element;
leftSort = sort;
} else {
leftSort = existingSorts.get(leftModel.getSetReference());
leftElement = existingSymbols.get(leftSort);
}
if(rightModel.getSetReference().equals(sum.getSet())) {
rightElement = element;
rightSort = sort;
} else {
rightSort = existingSorts.get(rightModel.getSetReference());
rightElement = existingSymbols.get(rightSort);
}
if(expression instanceof Allocation) {
locExpr =
createAllocationExpression(context, leftElement, leftSort,
rightElement, rightSort);
} else {
locExpr =
createDislocationExpression(context, leftElement, leftSort,
rightElement, rightSort);
}
Expr term =
Z3javaAPIWrapper.createIfThenElse(context, (BoolExpr)locExpr, arithExpr,
ZERO);
sumTerms.add((ArithExpr)term);
} else {
throw new UnsupportedDataTypeException("The type " +
expression.getClass().getSimpleName() +
" is not supported in SUM expressions");
}
}
ArithExpr addition = createAddition(context, sumTerms.toArray(new ArithExpr[0]));
return addition;
}
/**
* Returns the name of the function for the given {@link IAnnotatedSpecification} in the
* {@link ModelElementPropertyLiteral}.
*/
private String getFunctionName(ModelElementPropertyLiteral terms) {
return "f_" + terms.getSpecificationType().getSimpleName() + "_value";
}
/** Creates a {@link Symbol} for the given {@link IModelElement} and iterator. */
private Symbol createSymbol(Context context, IModelElement modelElement, int iterator) {
return Z3javaAPIWrapper.createSymbol(context, ((INamedElement)modelElement).getName() +
iterator);
}
}
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