Implementing the Z3 transformation of IExpressions.

refs 3224

org.fortiss.af3.specification/trunk/src/org/fortiss/af3/specification/utils/.ratings

-
 AnalysisConstraintsUtils.java 338283908b336201c69abdc0890efcfa1d513cad YELLOW
 SpecificationsFactory.java 0d703af2138e6183d7de1eecf5b3f49b15b32362 YELLOW
 TLSpecificationUtils.java 74c1a4c58f40ee41b84ce2f60094c57a53511214 GREEN
+Z3SpecificationUtils.java 150b3321a20991ef50382e0d5c61315eeea212a3 RED

org.fortiss.af3.specification/trunk/src/org/fortiss/af3/specification/utils/Z3SpecificationUtils.java

+/*-------------------------------------------------------------------------+
+| Copyright 2017 fortiss GmbH                                              |
+|                                                                          |
+| Licensed under the Apache License, Version 2.0 (the "License");          |
+| you may not use this file except in compliance with the License.         |
+| You may obtain a copy of the License at                                  |
+|                                                                          |
+|    http://www.apache.org/licenses/LICENSE-2.0                            |
+|                                                                          |
+| Unless required by applicable law or agreed to in writing, software      |
+| distributed under the License is distributed on an "AS IS" BASIS,        |
+| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
+| See the License for the specific language governing permissions and      |
+| limitations under the License.                                           |
++--------------------------------------------------------------------------*/
+package org.fortiss.af3.specification.utils;
+
+import static org.fortiss.af3.expression.model.terms.EOperator.ADD_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.AND_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.DIVIDE_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.EQUAL_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.GREATER_EQUAL_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.GREATER_THAN_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.LOWER_EQUAL_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.LOWER_THAN_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.MULTIPLY_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.NEGATE_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.NOT_EQUAL_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.NOT_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.OR_VALUE;
+import static org.fortiss.af3.expression.model.terms.EOperator.SUBTRACT_VALUE;
+
+import org.eclipse.emf.common.util.EList;
+import org.fortiss.af3.component.model.InputPort;
+import org.fortiss.af3.component.model.behavior.common.DataStateVariable;
+import org.fortiss.af3.expression.model.terms.EOperator;
+import org.fortiss.af3.expression.model.terms.FunctionCall;
+import org.fortiss.af3.expression.model.terms.IExpressionTerm;
+import org.fortiss.af3.expression.model.terms.PredefinedFunction;
+import org.fortiss.af3.expression.model.types.TBool;
+import org.fortiss.af3.expression.model.types.TDouble;
+import org.fortiss.af3.expression.model.types.TInt;
+import org.fortiss.af3.project.model.typesystem.ITerm;
+import org.fortiss.af3.project.model.typesystem.IType;
+
+import com.microsoft.z3.ArithExpr;
+import com.microsoft.z3.BoolExpr;
+import com.microsoft.z3.Context;
+import com.microsoft.z3.Expr;
+import com.microsoft.z3.IntNum;
+
+/**
+ * 
+ * @author vivek
+ */
+public class Z3SpecificationUtils {
+
+	/**
+	 * @param dataVars
+	 * @param ctx
+	 * @return
+	 */
+	public static Expr dataVarToZ3(EList<DataStateVariable> dataVars, Context ctx) {
+		IType type;
+		BoolExpr expr = ctx.mkTrue();
+		for(DataStateVariable dv : dataVars) {
+			type = dv.getVariableType();
+			String name = dv.toString();
+			expr = mkZ3Expr(name, type, expr, ctx);
+		}
+		return expr;
+	}
+
+	/**
+	 * @param inputVars
+	 * @param ctx
+	 * @return
+	 */
+	public static Expr portsToZ3(EList<InputPort> inputVars, Context ctx) {
+		IType type;
+		BoolExpr expr = ctx.mkTrue();
+		for(InputPort ip : inputVars) {
+			type = ip.getVariableType();
+			String name = ip.toString();
+			expr = mkZ3Expr(name, type, expr, ctx);
+		}
+		return expr;
+	}
+
+	// TODO: Complete the cases here.
+	/**
+	 * @return Converts an {@link IExpression} into a Z3 {@link Expr}. Here we are assuming that the
+	 *         af3 expression is well typed.
+	 */
+	public static Expr toZ3(IExpressionTerm af3expr, Context ctx) {
+		if(af3expr instanceof FunctionCall) {
+			EOperator op =
+					((PredefinedFunction)((FunctionCall)af3expr).getFunction()).getOperator();
+			EList<ITerm> args = ((FunctionCall)af3expr).getArguments();
+			Expr[] argExpr = new Expr[args.size()];
+			Expr exprAux;
+			for(int i = 0; i < args.size(); ++i) {
+				exprAux = toZ3((IExpressionTerm)args.get(i), ctx);
+				if(exprAux == null)
+					return null;
+				argExpr[i] = exprAux;
+			}
+			switch(op.getValue()) {
+				case ADD_VALUE:
+					return ctx.mkAdd((ArithExpr[])argExpr);
+				case SUBTRACT_VALUE:
+					return ctx.mkSub((ArithExpr[])argExpr);
+				case MULTIPLY_VALUE:
+					return ctx.mkMul((ArithExpr[])argExpr);
+				case DIVIDE_VALUE:
+					return ctx.mkDiv((ArithExpr)argExpr[0], (ArithExpr)argExpr[1]);
+				case LOWER_THAN_VALUE:
+					return ctx.mkLt((ArithExpr)argExpr[0], (ArithExpr)argExpr[1]);
+				case GREATER_THAN_VALUE:
+					return ctx.mkGt((ArithExpr)argExpr[0], (ArithExpr)argExpr[1]);
+				case LOWER_EQUAL_VALUE:
+					return ctx.mkLe((ArithExpr)argExpr[0], (ArithExpr)argExpr[1]);
+				case GREATER_EQUAL_VALUE:
+					return ctx.mkGe((ArithExpr)argExpr[0], (ArithExpr)argExpr[1]);
+				case EQUAL_VALUE:
+					return ctx.mkEq(argExpr[0], argExpr[1]);
+				case NOT_EQUAL_VALUE:
+					return ctx.mkNot(ctx.mkEq(argExpr[0], argExpr[1]));
+				case NOT_VALUE:
+					return ctx.mkNot((BoolExpr)argExpr[0]);
+				case NEGATE_VALUE:
+					return ctx.mkUnaryMinus((ArithExpr)argExpr[0]);
+				case OR_VALUE:
+					return ctx.mkOr((BoolExpr[])argExpr);
+				case AND_VALUE:
+					return ctx.mkAnd((BoolExpr[])argExpr);
+			}
+		}
+		return null;
+	}
+
+	/**
+	 * @param name
+	 * @param type
+	 * @param expr
+	 * @param ctx
+	 * @return
+	 */
+	private static BoolExpr mkZ3Expr(String name, IType type, BoolExpr expr, Context ctx) {
+		if(type instanceof TInt) {
+			IntNum z3var = ctx.mkInt(name);
+			BoolExpr expHigh =
+					ctx.mkLe(z3var, ctx.mkReal(Integer.toString(((TInt)type).getUpperBound())));
+			BoolExpr expLow =
+					ctx.mkLe(z3var, ctx.mkReal(Integer.toString(((TInt)type).getLowerBound())));
+			expr = ctx.mkAnd(expr, ctx.mkAnd(expHigh, expLow));
+		}
+		// Not sure what to do here yet.
+		if(type instanceof TDouble) {
+			ctx.mkReal(name);
+		}
+		if(type instanceof TBool) {
+			ctx.mkBoolConst(name);
+		}
+		return expr;
+	}
+}