mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Mixing Integers and Rational in the new Java API #5085 (#5098)

Browse source 
* Added covariance to arithmetic operations

* Added distillSort

* Update JavaGenericExample.java

Co-authored-by: Alexander Kreuzer <alexander.kreuzer@sap.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Alexander Kreuzer 2021-03-16 05:24:23 -07:00 committed by GitHub
parent ee614c2e46
commit dc5fa89de3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 73 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
examples/java/JavaGenericExample.java
View file

@ -829,6 +829,37 @@ class JavaGenericExample
} catch (Z3Exception ignored)
{
}
// Coercing type change in Z3
Expr<IntSort> integerDivision = ctx.mkDiv(ctx.mkInt(1), ctx.mkInt(2));
System.out.printf("%s -> %s%n", integerDivision, integerDivision.simplify()); // (div 1 2) -> 0
Expr<RealSort> 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<ArithSort> mixedDivision1 = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2));
Expr<ArithSort> tmp = mixedDivision1;
// the return type is a Expr<ArithSort> here but since we know it is a
// real view it as such.
Expr<RealSort> 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<BoolSort> 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<BoolSort> 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)

25
src/api/java/Context.java
View file

@ -723,7 +723,7 @@ public class Context implements AutoCloseable {
/**
* Creates the equality {@code x = y}
**/
public <R extends Sort> BoolExpr mkEq(Expr<R> x, Expr<R> 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 <R extends Sort> BoolExpr mkDistinct(Expr<R>... 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 <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<R> t2, Expr<R> t3)
public <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> 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 <R extends ArithSort> ArithExpr<R> mkAdd(Expr<R>... t)
public final <R extends ArithSort> ArithExpr<R> mkAdd(Expr<? extends R>... t)
{
checkContextMatch(t);
return (ArithExpr<R>) Expr.create(this,
@ -837,7 +837,7 @@ public class Context implements AutoCloseable {
* Create an expression representing {@code t[0] * t[1] * ...}.
**/
@SafeVarargs
public final <R extends ArithSort> ArithExpr<R> mkMul(Expr<R>... t)
public final <R extends ArithSort> ArithExpr<R> mkMul(Expr<? extends R>... t)
{
checkContextMatch(t);
return (ArithExpr<R>) Expr.create(this,
@ -848,7 +848,7 @@ public class Context implements AutoCloseable {
* Create an expression representing {@code t[0] - t[1] - ...}.
**/
@SafeVarargs
public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<R>... t)
public final <R extends ArithSort> ArithExpr<R> mkSub(Expr<? extends R>... t)
{
checkContextMatch(t);
return (ArithExpr<R>) Expr.create(this,
@ -868,7 +868,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 / t2}.
**/
public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<R> t1, Expr<R> t2)
public <R extends ArithSort> ArithExpr<R> mkDiv(Expr<? extends R> t1, Expr<? extends R> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
@ -905,7 +905,8 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 ^ t2}.
**/
public <R extends ArithSort> ArithExpr<R> mkPower(Expr<R> t1, Expr<R> t2)
public <R extends ArithSort> ArithExpr<R> mkPower(Expr<? extends R> t1,
Expr<? extends R> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
@ -918,7 +919,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 &lt; t2}
**/
public <R extends ArithSort> BoolExpr mkLt(Expr<R> t1, Expr<R> t2)
public BoolExpr mkLt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
@ -929,7 +930,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 &lt;= t2}
**/
public <R extends ArithSort> BoolExpr mkLe(Expr<R> t1, Expr<R> t2)
public BoolExpr mkLe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
@ -940,7 +941,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 &gt; t2}
**/
public <R extends ArithSort> BoolExpr mkGt(Expr<R> t1, Expr<R> t2)
public BoolExpr mkGt(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);
@ -951,7 +952,7 @@ public class Context implements AutoCloseable {
/**
* Create an expression representing {@code t1 &gt;= t2}
**/
public <R extends ArithSort> BoolExpr mkGe(Expr<R> t1, Expr<R> t2)
public BoolExpr mkGe(Expr<? extends ArithSort> t1, Expr<? extends ArithSort> t2)
{
checkContextMatch(t1);
checkContextMatch(t2);

29
src/api/java/Expr.java
View file

@ -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<R extends Sort> extends AST
return Native.getIndexValue(getContext().nCtx(), getNativeObject());
}
private Class sort = null;
/**
* Downcast sort of this expression. {@code
* Expr<ArithSort> mixedExpr = ctx.mkDiv(ctx.mkReal(1), ctx.mkInt(2));
* Expr<RealSort> realExpr = mixedExpr.distillSort(RealSort.class)
* }
*
* @throws Z3Exception if sort is not compatible with expr.
**/
public <S extends R> Expr<S> distillSort(Class<S> 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<S>) ((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