From dc5fa89de35ee0637e3e6894e37015c9a149e694 Mon Sep 17 00:00:00 2001 From: Alexander Kreuzer Date: Tue, 16 Mar 2021 05:24:23 -0700 Subject: [PATCH] Mixing Integers and Rational in the new Java API #5085 (#5098) * Added covariance to arithmetic operations * Added distillSort * Update JavaGenericExample.java Co-authored-by: Alexander Kreuzer Co-authored-by: Nikolaj Bjorner --- examples/java/JavaGenericExample.java | 31 +++++++++++++++++++++++++++ src/api/java/Context.java | 25 ++++++++++----------- src/api/java/Expr.java | 29 +++++++++++++++++++++++++ 3 files changed, 73 insertions(+), 12 deletions(-) diff --git a/examples/java/JavaGenericExample.java b/examples/java/JavaGenericExample.java index 8dd31fed0..1a4ac6628 100644 --- a/examples/java/JavaGenericExample.java +++ b/examples/java/JavaGenericExample.java @@ -829,6 +829,37 @@ class JavaGenericExample } catch (Z3Exception ignored) { } + + // Coercing type change in Z3 + Expr integerDivision = ctx.mkDiv(ctx.mkInt(1), ctx.mkInt(2)); + System.out.printf("%s -> %s%n", integerDivision, integerDivision.simplify()); // (div 1 2) -> 0 + + Expr realDivision = ctx.mkDiv(ctx.mkReal(1), ctx.mkReal(2)); + System.out.printf("%s -> %s%n", realDivision, realDivision.simplify()); // (/ 1.0 2.0) -> 1/2 + + Expr mixedDivision1 = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2)); + Expr tmp = mixedDivision1; + // the return type is a Expr here but since we know it is a + // real view it as such. + Expr mixedDivision2 = mixedDivision1.distillSort(RealSort.class); + System.out.printf("%s -> %s%n", mixedDivision2, mixedDivision2.simplify()); // (/ 1.0 (to_real 2)) -> 1/2 + + // empty distillSort + mixedDivision1.distillSort(ArithSort.class); + + try { + mixedDivision1.distillSort(IntSort.class); + throw new TestFailedException(); // unreachable + } catch (Z3Exception exception) { + System.out.println(exception); // com.microsoft.z3.Z3Exception: Cannot cast expression of sort + // com.microsoft.z3.RealSort to com.microsoft.z3.IntSort. + } + + Expr eq1 = ctx.mkEq(realDivision, integerDivision); + System.out.printf("%s -> %s%n", eq1, eq1.simplify()); // (= (/ 1.0 2.0) (to_real (div 1 2))) -> false + + Expr eq2 = ctx.mkEq(realDivision, mixedDivision2); + System.out.printf("%s -> %s%n", eq2, eq2.simplify()); // (= (/ 1.0 2.0) (/ 1.0 (to_real 2))) -> true } // / Shows how to use Solver(logic) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 0c7f07615..160dfa7db 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -723,7 +723,7 @@ public class Context implements AutoCloseable { /** * Creates the equality {@code x = y} **/ - public BoolExpr mkEq(Expr x, Expr y) + public BoolExpr mkEq(Expr x, Expr y) { checkContextMatch(x); checkContextMatch(y); @@ -735,7 +735,7 @@ public class Context implements AutoCloseable { * Creates a {@code distinct} term. **/ @SafeVarargs - public final BoolExpr mkDistinct(Expr... args) + public final BoolExpr mkDistinct(Expr... args) { checkContextMatch(args); return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length, @@ -758,7 +758,7 @@ public class Context implements AutoCloseable { * @param t2 An expression * @param t3 An expression with the same sort as {@code t2} **/ - public Expr mkITE(Expr t1, Expr t2, Expr t3) + public Expr mkITE(Expr t1, Expr t2, Expr t3) { checkContextMatch(t1); checkContextMatch(t2); @@ -826,7 +826,7 @@ public class Context implements AutoCloseable { * Create an expression representing {@code t[0] + t[1] + ...}. **/ @SafeVarargs - public final ArithExpr mkAdd(Expr... t) + public final ArithExpr mkAdd(Expr... t) { checkContextMatch(t); return (ArithExpr) Expr.create(this, @@ -837,7 +837,7 @@ public class Context implements AutoCloseable { * Create an expression representing {@code t[0] * t[1] * ...}. **/ @SafeVarargs - public final ArithExpr mkMul(Expr... t) + public final ArithExpr mkMul(Expr... t) { checkContextMatch(t); return (ArithExpr) Expr.create(this, @@ -848,7 +848,7 @@ public class Context implements AutoCloseable { * Create an expression representing {@code t[0] - t[1] - ...}. **/ @SafeVarargs - public final ArithExpr mkSub(Expr... t) + public final ArithExpr mkSub(Expr... t) { checkContextMatch(t); return (ArithExpr) Expr.create(this, @@ -868,7 +868,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 / t2}. **/ - public ArithExpr mkDiv(Expr t1, Expr t2) + public ArithExpr mkDiv(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -905,7 +905,8 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 ^ t2}. **/ - public ArithExpr mkPower(Expr t1, Expr t2) + public ArithExpr mkPower(Expr t1, + Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -918,7 +919,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 < t2} **/ - public BoolExpr mkLt(Expr t1, Expr t2) + public BoolExpr mkLt(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -929,7 +930,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 <= t2} **/ - public BoolExpr mkLe(Expr t1, Expr t2) + public BoolExpr mkLe(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -940,7 +941,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 > t2} **/ - public BoolExpr mkGt(Expr t1, Expr t2) + public BoolExpr mkGt(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); @@ -951,7 +952,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t1 >= t2} **/ - public BoolExpr mkGe(Expr t1, Expr t2) + public BoolExpr mkGe(Expr t1, Expr t2) { checkContextMatch(t1); checkContextMatch(t2); diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index f2f64efee..60826665d 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -17,6 +17,9 @@ Notes: package com.microsoft.z3; +import java.lang.reflect.Type; +import java.lang.reflect.ParameterizedType; + import com.microsoft.z3.enumerations.Z3_ast_kind; import com.microsoft.z3.enumerations.Z3_decl_kind; import com.microsoft.z3.enumerations.Z3_lbool; @@ -2090,12 +2093,38 @@ public class Expr extends AST return Native.getIndexValue(getContext().nCtx(), getNativeObject()); } + private Class sort = null; + + /** + * Downcast sort of this expression. {@code + * Expr mixedExpr = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2)); + * Expr realExpr = mixedExpr.distillSort(RealSort.class) + * } + * + * @throws Z3Exception if sort is not compatible with expr. + **/ + public Expr distillSort(Class newSort) { + if (sort != null && !newSort.isAssignableFrom(sort)) { + throw new Z3Exception( + String.format("Cannot distill expression of sort %s to %s.", sort.getName(), newSort.getName())); + } + + return (Expr) ((Expr) this); + } + /** * Constructor for Expr * @throws Z3Exception on error **/ protected Expr(Context ctx, long obj) { super(ctx, obj); + Type superclass = getClass().getGenericSuperclass(); + if (superclass instanceof ParameterizedType) { + Type argType = ((ParameterizedType) superclass).getActualTypeArguments()[0]; + if (argType instanceof Class) { + this.sort = (Class) argType; + } + } } @Override