Skip to content

Commit

Permalink
Java type generics (#4832)
Browse files Browse the repository at this point in the history
* Generify, needs some testing and review

* Remove unnecessary change

* Whoops, ? capture that type

* Misread the docs, whoops

* More permissible arithmetic operations

* Implement believed Optimize generics

* Missed a few generics

* More permissible expr for arrays in parameters

* More permissible expr for bitvecs in parameters

* More permissible expr for bools in parameters

* More permissible expr for fps in parameters

* More permissible expr for fprms in parameters

* More permissible expr for ints in parameters

* More permissible expr for reals in parameters

* Undo breaking name conflict due to type erasure; see notes

* Whoops, fix typing of ReExpr

* Sort corrections for Re, Seq

* More permissible expr for regular expressions in parameters

* Fix name conflict between sequences and regular expressions; see notes

* Minor typo, big implications!

* Make Constructor consistent, associate captured types with other unknown capture types for datatype consistency

* More expressive; outputs of multiple datatype definitions are only known to be sort, not capture, and Constructor.of should make a capture

* Be less dumb and just type it a little differently

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

* General fixups

* Downgrade java version, make it only for the generic support, remove var and Expr[]::new construction

* Turns out Java 8 hadn't figured out how to do stream generics yet. Didn't even show up in my IDE, weird
  • Loading branch information
addisoncrump authored Nov 30, 2020
1 parent bb24b3f commit 3bca1fb
Show file tree
Hide file tree
Showing 45 changed files with 2,724 additions and 588 deletions.
6 changes: 3 additions & 3 deletions examples/java/JavaExample.java
Original file line number Diff line number Diff line change
Expand Up @@ -599,7 +599,7 @@ void quantifierExample1(Context ctx)
System.out.println("QuantifierExample");
Log.append("QuantifierExample");

Sort[] types = new Sort[3];
IntSort[] types = new IntSort[3];
IntExpr[] xs = new IntExpr[3];
Symbol[] names = new Symbol[3];
IntExpr[] vars = new IntExpr[3];
Expand Down Expand Up @@ -1398,7 +1398,7 @@ public void bitvectorExample1(Context ctx) throws TestFailedException
System.out.println("BitvectorExample1");
Log.append("BitvectorExample1");

Sort bv_type = ctx.mkBitVecSort(32);
BitVecSort bv_type = ctx.mkBitVecSort(32);
BitVecExpr x = (BitVecExpr) ctx.mkConst("x", bv_type);
BitVecNum zero = (BitVecNum) ctx.mkNumeral("0", bv_type);
BitVecNum ten = ctx.mkBV(10, 32);
Expand All @@ -1420,7 +1420,7 @@ public void bitvectorExample2(Context ctx) throws TestFailedException
Log.append("BitvectorExample2");

/* construct x ^ y - 103 == x * y */
Sort bv_type = ctx.mkBitVecSort(32);
BitVecSort bv_type = ctx.mkBitVecSort(32);
BitVecExpr x = ctx.mkBVConst("x", 32);
BitVecExpr y = ctx.mkBVConst("y", 32);
BitVecExpr x_xor_y = ctx.mkBVXOR(x, y);
Expand Down
Loading

0 comments on commit 3bca1fb

Please sign in to comment.