Java type generics #4832

addisoncrump · 2020-11-28T21:27:41Z

Using type generics like this makes it more feasible to implement operations in Java with fewer casts and much easier to use with the var keyword. There are a few breaking changes that I'd like to review with a contributor and a few questions about typing (as I am not familiar with some of the features of z3, e.g. enum types vs finite domains, Optimize, Fixedpoint, etc). Gonna go through and add comments on the PR for each of these.

ghost · 2020-11-28T21:27:56Z

All CLA requirements met.

examples/java/JavaExample.java

addisoncrump · 2020-11-28T22:05:21Z

src/api/java/Context.java

    }


    /**
     * Create a new array sort.
     **/
-    public ArraySort mkArraySort(Sort[] domains, Sort range)
+    public <R extends Sort> ArraySort<?, R> mkArraySort(Sort[] domains, R range)


No real way to extract the domain sort here. Java type generics aren't quite as powerful as C++ templates and there's no tuple typing.

addisoncrump · 2020-11-28T22:14:30Z

src/api/java/Context.java

                Native.mkBound(nCtx(), index, ty.getNativeObject()));
    }

    /**
     * Create a quantifier pattern.
     **/
-    public Pattern mkPattern(Expr... terms)
+    public Pattern mkPattern(Expr<?>... terms)


Is there anything we can say consistently about the types of the terms in a pattern? Not sure how this is restricted in z3.

addisoncrump · 2020-11-28T22:31:43Z

src/api/java/Optimize.java

@@ -75,7 +76,7 @@ public void Add(BoolExpr ... constraints)
    /**
     * Handle to objectives returned by objective functions.
     **/
-    public static class Handle {
+    public static class Handle<R extends Sort> {


Can this be more narrowly defined to R extends ArithSort?

addisoncrump · 2020-11-28T22:31:49Z

src/api/java/Optimize.java

@@ -110,7 +111,7 @@ public Expr getUpper()
         * and otherwise is represented by the expression {@code value + eps * EPSILON},
         * where {@code EPSILON} is an arbitrarily small real number.
         */
-        public Expr[] getUpperAsVector()
+        public Expr<?>[] getUpperAsVector()


Can this be typed to R instead of ??

addisoncrump · 2020-11-28T22:35:29Z

src/api/java/Optimize.java

@@ -150,19 +150,19 @@ public String toString()
     * Return an objective which associates with the group of constraints.
     *
     **/
-    public Handle AssertSoft(BoolExpr constraint, int weight, String group)
+    public Handle<?> AssertSoft(BoolExpr constraint, int weight, String group)


Requires explicit casting by user because there's no input to base the result type with; I think this is a reasonable requirement on the user. Won't break existing code.

addisoncrump

Because Expr<FPSort> and Expr<RealSort> have the same parameters after type erasure, it's not possible to have them permissively typed. There might be a workaround with a rename (e.g. mkFPtoFP_FP, mkFPtoFP_Real), but this is kind of gross and in most cases it's likely acceptable for it to just be cast by the user.

addisoncrump

Like the previous issue between Expr<FPSort> and Expr<RealSort>, these two conflict after type erasure. Same notes as above.

…own capture types for datatype consistency

…own to be sort, not capture, and Constructor.of should make a capture

addisoncrump · 2020-11-29T00:19:43Z

I think this is just about ready. Only breaking changes are where things are explicitly typed by a cast where they should not be. Things are made more permissive for different types of Expr and there's forced consistency between various operations, e.g. mkAdd will no longer accept Exprs of two different subtypes without cast (though this would only be breaking if someone was already using var keywords).

I'll add an example of why this makes life so much better for all of us later this evening, gotta get food.

addisoncrump · 2020-11-29T04:24:12Z

You can diff JavaExample.java and Java13Example.java to see how auto-typing + functional with streams makes things a lot easier to use.

addisoncrump · 2020-11-29T06:06:20Z

examples/java/Java13Example.java

@@ -1649,18 +1472,17 @@ public void treeExample(Context ctx) throws TestFailedException
    // / forest ::= nil | cons(tree, forest)
    // / tree ::= nil | cons(forest, forest)
    // / </remarks>
-    public void forestExample(Context ctx) throws TestFailedException
+    @SuppressWarnings({"unchecked", "unused", "UnusedAssignment"})
+    public <Tree, Forest> void forestExample(Context ctx) throws TestFailedException


I especially encourage you to look at this to get a better understanding of why these changes are such a quality of life improvement.

addisoncrump · 2020-11-29T06:38:15Z

Looks like the pipelines are failing because it's attempting to compile Java13Example with Java 8.

The code that modifies z3 proper is all Java 8 compatible, but the example code is theoretically 11+ (though I've only tested it with 13). The script or the build environment could be modified, but I think that's a little beyond my decision.

NikolajBjorner · 2020-11-30T00:56:18Z

These updates look great.
There was a decision to have sorts of expressions reflected in sub-types. This is both manifested in Java and .Net.
It forces writing application code that is statically type correct, but then ends up requiring a bunch of coercions.
It is my understanding that this update retains the subtyping, but avoids some of the end-user hassle.

It would also break other client code that would have to be ported to handle this new discipline.
Given that it is a breaking change, I will wait a little week before merging in case someone using the Java bindings have substantial issues.

The Java13 example could be excluded from the build or the pipelines would somehow have to be configured to use the newer, non-default, version of Java. I am not sure how exactly to configure the pipelines with a non-default version of Java so I suggest to omit the Java13 example in the first round.

addisoncrump · 2020-11-30T01:10:01Z

As far as I know, there are technically no breaking changes to already compiled code, as these casts are removed during type erasure, I did not modify the underlying un-generic types, and generically typed return values are strictly subtypes of what was originally returned. As for the code which will be compiled after this change, the only breaking changes are to when sorts are explicitly declared as wider than what they are, e.g. Sort s = ctx.getIntSort(), which are then used to type the return values of a mkConst or similar. Technically I think I can work around these too and make it have zero breaking changes (!), so let me see what I can do.

I'll just /* */ out Java13Example.java.

NikolajBjorner · 2020-11-30T01:27:38Z

Technically I think I can work around these too and make it have zero breaking changes (!), so let me see what I can do.

I don't think it is worth it. Clients should either use "var" or the more specific types. I don't see a reason to support something that is a step back.

addisoncrump · 2020-11-30T02:18:17Z

It boils down to whether you prefer completeness or correctness:

Sort s = ctx.getIntSort();
IntExpr e = (IntExpr) ctx.mkConst("a", s);

This fails to compile, even though it's sound. On the other hand, this also becomes permissible:

Sort s = ctx.getIntSort();
BitVecExpr e = (BitVecExpr) ctx.mkConst("a", s);

Which would compile with the change, but it would be incorrect. Note that, were s specifically typed to IntSort, this would not compile.

Which case would be more apt? With the change, you sacrifice some correctness, but it's compatible with older versions as unchecked type generic casting.

addisoncrump · 2020-11-30T02:38:29Z

Actually, after testing this, that change makes more problems than it solves. Disregard.

…var and Expr[]::new construction

addisoncrump · 2020-11-30T02:48:40Z

Rather than outright deleting Java13Example, I replaced it with JavaGenericExample which is Java 8 compatible (used some scripting to undo var, then removed some API features introduced in Java 11). Let's see what happens in CI and hopefully that's that.

NikolajBjorner · 2020-11-30T03:32:43Z

It boils down to whether you prefer completeness or correctness:

I don't see any need to change your pull request: the changes required in JavaExample.java are benign and I consider them warranted. I think other clients will be well served with making similar changes.

…dn't even show up in my IDE, weird

addisoncrump · 2020-11-30T14:39:23Z

Okay, that's everything. Let me know if you find anything that doesn't make perfect sense.

NikolajBjorner · 2020-11-30T18:05:02Z

Super!

Introduced in Z3Prover/z3#4832

…ub.tudo-aqua-z3-turnkey-4.8.10 - Bump z3-turnkey from 4.8.9 to 4.8.10 - Adapt types as needed to accommodate Z3Prover/z3#4832 (upcasting some types, and supplying some needed type params).

Generify, needs some testing and review

19d83e3

Remove unnecessary change

da9c2ed

addisoncrump commented Nov 28, 2020

View reviewed changes

examples/java/JavaExample.java Show resolved Hide resolved

addisoncrump commented Nov 28, 2020

View reviewed changes

addisoncrump added 2 commits November 28, 2020 16:07

Whoops, ? capture that type

7c30c50

Misread the docs, whoops

c1096ad

addisoncrump commented Nov 28, 2020

View reviewed changes

addisoncrump added 2 commits November 28, 2020 16:22

More permissible arithmetic operations

9173296

Implement believed Optimize generics

9ad727d

addisoncrump commented Nov 28, 2020

View reviewed changes

Missed a few generics

b6b42c9

addisoncrump commented Nov 28, 2020

View reviewed changes

addisoncrump added 8 commits November 28, 2020 16:41

More permissible expr for arrays in parameters

8904764

More permissible expr for bitvecs in parameters

92f5f2d

More permissible expr for bools in parameters

9d4aa7c

More permissible expr for fps in parameters

dd80510

More permissible expr for fprms in parameters

e154a47

More permissible expr for ints in parameters

37da41d

More permissible expr for reals in parameters

f7f43a8

Undo breaking name conflict due to type erasure; see notes

e3d7a9b

addisoncrump commented Nov 28, 2020

View reviewed changes

addisoncrump added 4 commits November 28, 2020 17:13

Whoops, fix typing of ReExpr

372de12

Sort corrections for Re, Seq

7894e69

More permissible expr for regular expressions in parameters

5f58655

Fix name conflict between sequences and regular expressions; see notes

67e4ef8

addisoncrump commented Nov 28, 2020

View reviewed changes

addisoncrump added 2 commits November 28, 2020 17:34

Minor typo, big implications!

714e8f7

Make Constructor consistent, associate captured types with other unkn…

e47e996

…own capture types for datatype consistency

addisoncrump added 2 commits November 28, 2020 18:11

More expressive; outputs of multiple datatype definitions are only kn…

d975295

…own to be sort, not capture, and Constructor.of should make a capture

Be less dumb and just type it a little differently

cf0289e

addisoncrump marked this pull request as ready for review November 29, 2020 00:17

Update examples, make sure to type Expr and FuncDecl sort returns

c5a1737

General fixups

ca8a595

addisoncrump commented Nov 29, 2020

View reviewed changes

addisoncrump force-pushed the type-generics branch from c828898 to ca8a595 Compare November 30, 2020 02:42

Downgrade java version, make it only for the generic support, remove …

4e14a1c

…var and Expr[]::new construction

Turns out Java 8 hadn't figured out how to do stream generics yet. Di…

82a0d4f

…dn't even show up in my IDE, weird

NikolajBjorner merged commit 3bca1fb into Z3Prover:master Nov 30, 2020

addisoncrump deleted the type-generics branch November 30, 2020 19:21

akreuzer mentioned this pull request Mar 8, 2021

Mixing Integers and Rational in the new Java API #5085

Closed

shonfeder pushed a commit to apalache-mc/apalache that referenced this pull request Jul 5, 2021

Adapt SMT interface and Z3SolverContext to generic Expr types

8bc6957

Introduced in Z3Prover/z3#4832

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Java type generics #4832

Java type generics #4832

addisoncrump commented Nov 28, 2020 •

edited

Loading

ghost commented Nov 28, 2020 •

edited by ghost

Loading

addisoncrump Nov 28, 2020 •

edited

Loading

addisoncrump Nov 28, 2020

addisoncrump Nov 28, 2020

addisoncrump Nov 28, 2020

addisoncrump Nov 28, 2020

addisoncrump left a comment •

edited

Loading

addisoncrump left a comment

addisoncrump commented Nov 29, 2020

addisoncrump commented Nov 29, 2020

addisoncrump Nov 29, 2020

addisoncrump commented Nov 29, 2020

NikolajBjorner commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020 •

edited

Loading

addisoncrump commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020

Java type generics #4832

Java type generics #4832

Conversation

addisoncrump commented Nov 28, 2020 • edited Loading

ghost commented Nov 28, 2020 • edited by ghost Loading

addisoncrump Nov 28, 2020 • edited Loading

Choose a reason for hiding this comment

addisoncrump Nov 28, 2020

Choose a reason for hiding this comment

addisoncrump Nov 28, 2020

Choose a reason for hiding this comment

addisoncrump Nov 28, 2020

Choose a reason for hiding this comment

addisoncrump Nov 28, 2020

Choose a reason for hiding this comment

addisoncrump left a comment • edited Loading

Choose a reason for hiding this comment

addisoncrump left a comment

Choose a reason for hiding this comment

addisoncrump commented Nov 29, 2020

addisoncrump commented Nov 29, 2020

addisoncrump Nov 29, 2020

Choose a reason for hiding this comment

addisoncrump commented Nov 29, 2020

NikolajBjorner commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020 • edited Loading

addisoncrump commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020

addisoncrump commented Nov 30, 2020

NikolajBjorner commented Nov 30, 2020

addisoncrump commented Nov 28, 2020 •

edited

Loading

ghost commented Nov 28, 2020 •

edited by ghost

Loading

addisoncrump Nov 28, 2020 •

edited

Loading

addisoncrump left a comment •

edited

Loading

NikolajBjorner commented Nov 30, 2020 •

edited

Loading