mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Make multi-index arrays not so bad (#4857)

Browse source
This commit is contained in:
Addison Crump 2020-12-05 17:45:46 -06:00 • committed by GitHub
parent 4d55f83654
commit b0cecf7747
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -229,7 +229,7 @@ public class Context implements AutoCloseable {
/**
* Create a new array sort.
**/
public <R extends Sort> ArraySort<?, R> mkArraySort(Sort[] domains, R range)
public <R extends Sort> ArraySort<Sort, R> mkArraySort(Sort[] domains, R range)
{
checkContextMatch(domains);
checkContextMatch(range);
@ -1725,7 +1725,7 @@ public class Context implements AutoCloseable {
* @see #mkArraySort
* @see #mkStore
**/
public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<?, R>> a, Expr<?>[] args)
public <R extends Sort> Expr<R> mkSelect(Expr<ArraySort<Sort, R>> a, Expr<?>[] args)
{
checkContextMatch(a);
checkContextMatch(args);
@ -1775,7 +1775,7 @@ public class Context implements AutoCloseable {
* @see #mkSelect
**/
public <R extends Sort> ArrayExpr<?, R> mkStore(Expr<ArraySort<?, R>> a, Expr<?>[] args, Expr<R> v)
public <R extends Sort> ArrayExpr<Sort, R> mkStore(Expr<ArraySort<Sort, R>> a, Expr<?>[] args, Expr<R> v)
{
checkContextMatch(a);
checkContextMatch(args);