New methods:
- Expr.getNumeralDouble(): retrieve any numeral as a double
- IntNum.getUint(): extract numeral as unsigned 32-bit value
- IntNum.getUint64(): extract numeral as unsigned 64-bit value
- RatNum.getSmall(): numerator/denominator as int64 pair
- RatNum.getRationalInt64(): numerator/denominator (returns null on overflow)
Each is a thin wrapper around the existing Native binding.
Added examples to JavaExample.java covering all new methods.
* add Expr.isGround() to Java API
Expose Z3_is_ground as a public method on Expr. Returns true when the
expression contains no free variables.
* add Expr.isLambda() to Java API
Expose Z3_is_lambda as a public method on Expr. Returns true when the
expression is a lambda quantifier.
* add AST.getDepth() to Java API
Expose Z3_get_depth as a public method on AST. Returns the maximum
number of nodes on any path from root to leaf.
* add ArraySort.getArity() to Java API
Expose Z3_get_array_arity as a public method on ArraySort. Returns
the number of dimensions of a multi-dimensional array sort.
* add DatatypeSort.isRecursive() to Java API
Expose Z3_is_recursive_datatype_sort as a public method on
DatatypeSort. Returns true when the datatype refers to itself.
* add FPExpr.isNumeral() to Java API
Expose Z3_fpa_is_numeral as a public method on FPExpr. Returns true
when the expression is a concrete floating-point value.
* add isGroundExample test to JavaExample
Test Expr.isGround() on constants, variables, and compound
expressions.
* add astDepthExample test to JavaExample
Test AST.getDepth() on leaf nodes and nested expressions to verify
the depth computation.
* add arrayArityExample test to JavaExample
Test ArraySort.getArity() on single-domain and multi-domain array
sorts.
* add recursiveDatatypeExample test to JavaExample
Test DatatypeSort.isRecursive() on a recursive list datatype and a
non-recursive pair datatype.
* add fpNumeralExample test to JavaExample
Test FPExpr.isNumeral() on a floating point constant and a symbolic
variable.
* add isLambdaExample test to JavaExample
Test Expr.isLambda() on a lambda expression and a plain variable.
* 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
