JS/TS API Array support (#6393)

* feat: basic array support

Still need deeper type support for Arrays

* fixed broken format rules

* spaces inside curly

* feat: range sort type inference

* feat: better type inference in model eval

* doc: fixed some incorrect documentation

* feat: domain type inference

* feat: addressed suggestions

* feat: addressed suggestions

* chore: moved ts-expect from deps to dev-deps

* test: added z3guide examples

* fix: removed ts-expect from dependencies again

* docs: fixed some documentation

src/api/js/package.json

@@ -35,7 +35,8 @@
   "contributors": [
     "Kevin Gibbons <bakkot@gmail.com>",
     "Nikolaj Bjorner",
-    "Olaf Tomalka <olaf@tomalka.me>"
+    "Olaf Tomalka <olaf@tomalka.me>",
+    "Walden Yan <waldenyan20@gmail.com>"
   ],
   "devDependencies": {
     "@types/jest": "^27.5.1",
@@ -49,6 +50,7 @@
     "prettier": "^2.5.1",
     "rimraf": "^3.0.2",
     "sprintf-js": "^1.1.2",
+    "ts-expect": "^1.3.0",
     "ts-jest": "^28.0.3",
     "ts-node": "^10.8.0",
     "typedoc": "^0.22.17",

src/api/js/src/high-level/high-level.test.ts

@@ -2,6 +2,7 @@ import assert from 'assert';
 import asyncToArray from 'iter-tools/methods/async-to-array';
 import { init, killThreads } from '../jest';
 import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types';
+import { expectType } from "ts-expect";
 
 /**
  * Generate all possible solutions from given assumptions.
@@ -113,7 +114,7 @@ describe('high-level', () => {
     const { Solver, Not, Int } = api.Context('main');
     const solver = new Solver();
     solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))")
-    expect(await solver.check()).toStrictEqual('sat')    
+    expect(await solver.check()).toStrictEqual('sat')
     const x = Int.const('x')
     solver.add(Not(x.eq(1)))
     expect(await solver.check()).toStrictEqual('unsat')
@@ -211,6 +212,7 @@ describe('high-level', () => {
         }
         return cells;
       }
+
       const INSTANCE = toSudoku(`
         ....94.3.
         ...51...7
@@ -390,6 +392,106 @@ describe('high-level', () => {
     });
   });
 
+  describe('arrays', () => {
+
+    it('Example 1', async () => {
+      const Z3 = api.Context('main');
+
+      const arr = Z3.Array.const('arr', Z3.Int.sort(), Z3.Int.sort());
+      const [idx, val] = Z3.Int.consts('idx val');
+
+      const conjecture = (arr.store(idx, val).select(idx).eq(val));
+      await prove(conjecture);
+    });
+
+    it('domain and range type inference', async () => {
+      const { BitVec, Array, isArray, isArraySort } = api.Context('main');
+
+      const arr = Array.const('arr', BitVec.sort(160), BitVec.sort(256));
+
+      const domain = arr.domain();
+      expect(domain.size()).toStrictEqual(160);
+      expect(arr.domain_n(0).size()).toStrictEqual(160);
+      const range = arr.range();
+      expect(range.size()).toStrictEqual(256);
+
+      assert(isArray(arr) && isArraySort(arr.sort));
+
+      const arr2 = Array.const('arr2', BitVec.sort(1), BitVec.sort(2), BitVec.sort(3));
+      const dom2 = arr2.domain_n(1);
+
+      // We can call size() on dom2 and see that it is two bits
+      // purely from type inference
+      expectType<2>(dom2.size());
+
+      // Won't let us create an array constant with only one of domain/range
+      // and is detected at compile time
+      // @ts-expect-error
+      const arr3 = Array.const('arr3', BitVec.sort(1));
+    })
+
+    it('can do simple proofs', async () => {
+      const { BitVec, Array, isArray, isArraySort, isConstArray, Eq, Not } = api.Context('main');
+
+      const idx = BitVec.const('idx', 160);
+      const val = BitVec.const('val', 256);
+
+      const FIVE_VAL = BitVec.val(5, 256);
+
+      const arr = Array.const('arr', BitVec.sort(160), BitVec.sort(256));
+
+      const constArr = Array.K(BitVec.sort(160), FIVE_VAL);
+      assert(isArray(arr) && isArraySort(arr.sort) && isConstArray(constArr));
+
+      const arr2 = arr.store(0, 5);
+      await prove(Eq(arr2.select(0), FIVE_VAL));
+      await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256))));
+      await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx)));
+
+      // TODO: add in Quantifiers and better typing of arrays
+      // await prove(
+      //   ForAll([idx], idx.add(1).ugt(idx).and(arr.select(idx.add(1)).ugt(arr.select(idx)))).implies(
+      //     arr.select(0).ult(arr.select(1000))
+      //   )
+      // );
+    });
+
+    it('Finds arrays that differ but that sum to the same', async () => {
+      const Z3 = api.Context('main');
+      const { Array, BitVec } = Z3;
+
+      const mod = 1n << 32n;
+
+      const arr1 = Array.const('arr', BitVec.sort(2), BitVec.sort(32));
+      const arr2 = Array.const('arr2', BitVec.sort(2), BitVec.sort(32));
+
+      const same_sum = arr1.select(0)
+        .add(arr1.select(1))
+        .add(arr1.select(2))
+        .add(arr1.select(3))
+        .eq(
+          arr2.select(0)
+            .add(arr2.select(1))
+            .add(arr2.select(2))
+            .add(arr2.select(3))
+        );
+
+      const different = arr1.select(0).neq(arr2.select(0))
+        .or(arr1.select(1).neq(arr2.select(1)))
+        .or(arr1.select(2).neq(arr2.select(2)))
+        .or(arr1.select(3).neq(arr2.select(3)));
+
+      const model = await solve(same_sum.and(different));
+
+      const arr1Vals = [0, 1, 2, 3].map(i => model.eval(arr1.select(i)).value());
+      const arr2Vals = [0, 1, 2, 3].map(i => model.eval(arr2.select(i)).value());
+      expect((arr1Vals.reduce((a, b) => a + b, 0n) % mod) === arr2Vals.reduce((a, b) => a + b, 0n) % mod);
+      for (let i = 0; i < 4; i++) {
+        expect(arr1Vals[i] !== arr2Vals[i]);
+      }
+    });
+  });
+
   describe('Solver', () => {
     it('can use push and pop', async () => {
       const { Solver, Int } = api.Context('main');

src/api/js/src/high-level/high-level.ts

@@ -37,7 +37,7 @@ import {
   AnyExpr,
   AnySort,
   Arith,
-  ArithSort,
+  ArithSort, ArrayIndexType,
   Ast,
   AstMap,
   AstMapCtor,
@@ -48,7 +48,7 @@ import {
   BitVecSort,
   Bool,
   BoolSort,
-  CheckSatResult,
+  CheckSatResult, CoercibleFromMap,
   CoercibleRational,
   CoercibleToBitVec,
   CoercibleToExpr,
@@ -63,6 +63,8 @@ import {
   Model,
   Probe,
   RatNum,
+  SMTArray,
+  SMTArraySort,
   Solver,
   Sort,
   SortToExprMap,
@@ -86,12 +88,11 @@ function isCoercibleRational(obj: any): obj is CoercibleRational {
     (obj.denominator !== null &&
       (typeof obj.denominator === 'number' || typeof obj.denominator === 'bigint'))
   );
-  r &&
+  r && assert(
-    assert(
+    (typeof obj!.numerator !== 'number' || Number.isSafeInteger(obj!.numerator)) &&
-      (typeof obj.numerator !== 'number' || Number.isSafeInteger(obj.numerator)) &&
+    (typeof obj!.denominator !== 'number' || Number.isSafeInteger(obj!.denominator)),
-        (typeof obj.denominator !== 'number' || Number.isSafeInteger(obj.denominator)),
+    'Fraction numerator and denominator must be integers',
-      'Fraction numerator and denominator must be integers',
+  );
-    );
   return r;
 }
 
@@ -151,7 +152,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
   function createContext<Name extends string>(name: Name, options?: Record<string, any>): Context<Name> {
     const cfg = Z3.mk_config();
     if (options != null) {
-      Object.entries(options).forEach(([key, value]) => check(Z3.set_param_value(cfg, key, value.toString())));
+      Object.entries(options).forEach(
+        ([key, value]) => check(Z3.set_param_value(cfg, key, value.toString()))
+      );
     }
     const contextPtr = Z3.mk_context_rc(cfg);
     Z3.set_ast_print_mode(contextPtr, Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
@@ -216,20 +219,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
           return new ArithSortImpl(ast);
         case Z3_sort_kind.Z3_BV_SORT:
           return new BitVecSortImpl(ast);
+        case Z3_sort_kind.Z3_ARRAY_SORT:
+          return new ArraySortImpl(ast);
         default:
           return new SortImpl(ast);
       }
     }
 
-    function _toExpr(ast: Z3_ast): Bool<Name> | IntNum<Name> | RatNum<Name> | Arith<Name> | Expr<Name> {
+    function _toExpr(ast: Z3_ast): AnyExpr<Name> {
       const kind = check(Z3.get_ast_kind(contextPtr, ast));
       if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
         if (Z3.is_quantifier_forall(contextPtr, ast))
-           return new BoolImpl(ast);
+          return new BoolImpl(ast);
         if (Z3.is_quantifier_exists(contextPtr, ast))
-           return new BoolImpl(ast);
+          return new BoolImpl(ast);
         if (Z3.is_lambda(contextPtr, ast))
-           return new ExprImpl(ast);
+          return new ExprImpl(ast);
         assert(false);
       }
       const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));
@@ -251,6 +256,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
             return new BitVecNumImpl(ast);
           }
           return new BitVecImpl(ast);
+        case Z3_sort_kind.Z3_ARRAY_SORT:
+          return new ArrayImpl(ast);
         default:
           return new ExprImpl(ast);
       }
@@ -440,6 +447,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return r;
     }
 
+    function isArraySort(obj: unknown): obj is SMTArraySort<Name> {
+      const r = obj instanceof ArraySortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isArray(obj: unknown): obj is SMTArray<Name> {
+      const r = obj instanceof ArrayImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isConstArray(obj: unknown): boolean {
+      return isAppOf(obj, Z3_decl_kind.Z3_OP_CONST_ARRAY);
+    }
+
     function isProbe(obj: unknown): obj is Probe<Name> {
       const r = obj instanceof ProbeImpl;
       r && _assertContext(obj);
@@ -508,9 +531,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     // expression simplification //
     ///////////////////////////////
 
-    async function simplify(e : Expr<Name>) {
+    async function simplify(e: Expr<Name>) {
-       const result = await Z3.simplify(contextPtr, e.ast)       
+      const result = await Z3.simplify(contextPtr, e.ast)
-       return _toExpr(check(result));
+      return _toExpr(check(result));
     }
 
     /////////////
@@ -677,6 +700,44 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         );
       },
     };
+    const Array = {
+      sort<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        ...sig: [...DomainSort, RangeSort]
+      ): SMTArraySort<Name, DomainSort, RangeSort> {
+        const arity = sig.length - 1;
+        const r = sig[arity];
+        const d = sig[0];
+        if (arity === 1) {
+          return new ArraySortImpl(Z3.mk_array_sort(contextPtr, d.ptr, r.ptr));
+        }
+        const dom = sig.slice(0, arity);
+        return new ArraySortImpl(Z3.mk_array_sort_n(contextPtr, dom.map(s => s.ptr), r.ptr));
+      },
+      const<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        name: string, ...sig: [...DomainSort, RangeSort]
+      ): SMTArray<Name, DomainSort, RangeSort> {
+        return new ArrayImpl<DomainSort, RangeSort>(
+          check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(...sig).ptr))
+        );
+      },
+      consts<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
+        names: string | string[],
+        ...sig: [...DomainSort, RangeSort]
+      ): SMTArray<Name, DomainSort, RangeSort>[] {
+        if (typeof names === 'string') {
+          names = names.split(' ');
+        }
+        return names.map(name => Array.const(name, ...sig));
+      },
+      K<DomainSort extends AnySort<Name>, RangeSort extends AnySort<Name>>(
+        domain: DomainSort,
+        value: SortToExprMap<RangeSort, Name>
+      ): SMTArray<Name, [DomainSort], RangeSort> {
+        return new ArrayImpl<[DomainSort], RangeSort>(
+          check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr))
+        );
+      }
+    }
 
     ////////////////
     // Operations //
@@ -948,6 +1009,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
       readonly ptr: Z3_solver;
       readonly ctx: Context<Name>;
+
       constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) {
         this.ctx = ctx;
         let myPtr: Z3_solver;
@@ -964,21 +1026,26 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       push() {
         Z3.solver_push(contextPtr, this.ptr);
       }
+
       pop(num: number = 1) {
         Z3.solver_pop(contextPtr, this.ptr, num);
       }
+
       numScopes() {
         return Z3.solver_get_num_scopes(contextPtr, this.ptr);
       }
+
       reset() {
         Z3.solver_reset(contextPtr, this.ptr);
       }
+
       add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]) {
         _flattenArgs(exprs).forEach(expr => {
           _assertContext(expr);
           check(Z3.solver_assert(contextPtr, this.ptr, expr.ast));
         });
       }
+
       addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string) {
         if (typeof constant === 'string') {
           constant = Bool.const(constant);
@@ -1019,7 +1086,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return check(Z3.solver_to_string(contextPtr, this.ptr));
       }
 
-      fromString(s : string) {
+      fromString(s: string) {
         Z3.solver_from_string(contextPtr, this.ptr, s);
         throwIfError();
       }
@@ -1043,20 +1110,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return this.values();
       }
 
-      *entries(): IterableIterator<[number, FuncDecl<Name>]> {
+      * entries(): IterableIterator<[number, FuncDecl<Name>]> {
         const length = this.length();
         for (let i = 0; i < length; i++) {
           yield [i, this.get(i)];
         }
       }
 
-      *keys(): IterableIterator<number> {
+      * keys(): IterableIterator<number> {
         for (const [key] of this.entries()) {
           yield key;
         }
       }
 
-      *values(): IterableIterator<FuncDecl<Name>> {
+      * values(): IterableIterator<FuncDecl<Name>> {
         for (const [, value] of this.entries()) {
           yield value;
         }
@@ -1076,11 +1143,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
       eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>;
       eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>;
+      eval<Bits extends number = number>(expr: BitVec<Bits, Name>, modelCompletion?: boolean): BitVecNum<Bits, Name>;
       eval(expr: Expr<Name>, modelCompletion: boolean = false) {
         _assertContext(expr);
         const r = check(Z3.model_eval(contextPtr, this.ptr, expr.ast, modelCompletion));
         if (r === null) {
-          throw new Z3Error('Failed to evaluatio expression in the model');
+          throw new Z3Error('Failed to evaluate expression in the model');
         }
         return _toExpr(r);
       }
@@ -1092,7 +1160,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       get(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
       get(
         i: number | FuncDecl<Name> | Expr<Name> | Sort<Name>,
-        to?: number,
+        to?: number
       ): FuncDecl<Name> | FuncInterp<Name> | Expr<Name> | AstVector<Name, AnyAst<Name>> | FuncDecl<Name>[] {
         assert(to === undefined || typeof i === 'number');
         if (typeof i === 'number') {
@@ -1362,15 +1430,22 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       not(): Bool<Name> {
         return Not(this);
       }
+
       and(other: Bool<Name> | boolean): Bool<Name> {
         return And(this, other);
       }
+
       or(other: Bool<Name> | boolean): Bool<Name> {
         return Or(this, other);
       }
+
       xor(other: Bool<Name> | boolean): Bool<Name> {
         return Xor(this, other);
       }
+
+      implies(other: Bool<Name> | boolean): Bool<Name> {
+        return Implies(this, other);
+      }
     }
 
     class ProbeImpl implements Probe<Name> {
@@ -1571,27 +1646,35 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       add(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvadd(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       mul(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvmul(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sub(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsub(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sdiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsdiv(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       udiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvudiv(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       smod(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsmod(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       urem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvurem(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       srem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvsrem(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       neg(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvneg(contextPtr, this.ast)));
       }
@@ -1599,33 +1682,43 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       or(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       and(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvand(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       nand(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvnand(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       xor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvxor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       xnor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvxnor(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       shr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvashr(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       lshr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvlshr(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       shl(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvshl(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       rotateRight(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_ext_rotate_right(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       rotateLeft(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_ext_rotate_left(contextPtr, this.ast, this.sort.cast(count).ast)));
       }
+
       not(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvnot(contextPtr, this.ast)));
       }
@@ -1633,12 +1726,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       extract(high: number, low: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_extract(contextPtr, high, low, this.ast)));
       }
+
       signExt(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_sign_ext(contextPtr, count, this.ast)));
       }
+
       zeroExt(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_zero_ext(contextPtr, count, this.ast)));
       }
+
       repeat(count: number): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_repeat(contextPtr, count, this.ast)));
       }
@@ -1646,24 +1742,31 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       sle(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsle(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ule(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvule(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       slt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvslt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ult(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvult(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sge(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsge(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       uge(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvuge(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       sgt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsgt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       ugt(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvugt(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
@@ -1671,6 +1774,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       redAnd(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvredand(contextPtr, this.ast)));
       }
+
       redOr(): BitVec<Bits, Name> {
         return new BitVecImpl<Bits>(check(Z3.mk_bvredor(contextPtr, this.ast)));
       }
@@ -1678,24 +1782,31 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       addNoOverflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvadd_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       addNoUnderflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvadd_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       subNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsub_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       subNoUndeflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsub_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       sdivNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvsdiv_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       mulNoOverflow(other: CoercibleToBitVec<Bits, Name>, isSigned: boolean): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvmul_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned)));
       }
+
       mulNoUndeflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvmul_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast)));
       }
+
       negNoOverflow(): Bool<Name> {
         return new BoolImpl(check(Z3.mk_bvneg_no_overflow(contextPtr, this.ast)));
       }
@@ -1703,6 +1814,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
 
     class BitVecNumImpl<Bits extends number> extends BitVecImpl<Bits> implements BitVecNum<Bits, Name> {
       declare readonly __typename: BitVecNum['__typename'];
+
       value() {
         return BigInt(this.asString());
       }
@@ -1718,14 +1830,87 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         }
         return val;
       }
+
       asString() {
         return Z3.get_numeral_string(contextPtr, this.ast);
       }
+
       asBinaryString() {
         return Z3.get_numeral_binary_string(contextPtr, this.ast);
       }
     }
 
+    class ArraySortImpl<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
+      RangeSort extends AnySort<Name> = Sort<Name>>
+      extends SortImpl
+      implements SMTArraySort<Name, DomainSort, RangeSort> {
+      declare readonly __typename: SMTArraySort['__typename'];
+
+      domain(): DomainSort[0] {
+        return _toSort(check(Z3.get_array_sort_domain(contextPtr, this.ptr)));
+      }
+
+      domain_n<T extends number>(i: T): DomainSort[T] {
+        return _toSort(check(Z3.get_array_sort_domain_n(contextPtr, this.ptr, i)));
+      }
+
+      range(): RangeSort {
+        return _toSort(check(Z3.get_array_sort_range(contextPtr, this.ptr))) as RangeSort;
+      }
+
+    }
+
+    class ArrayImpl<
+      DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
+      RangeSort extends AnySort<Name> = Sort<Name>
+    > extends ExprImpl<Z3_ast, ArraySortImpl<DomainSort, RangeSort>>
+      implements SMTArray<Name, DomainSort, RangeSort> {
+      declare readonly __typename: SMTArray['__typename'];
+
+      domain(): DomainSort[0] {
+        return this.sort.domain();
+      }
+
+      domain_n<T extends number>(i: T): DomainSort[T] {
+        return this.sort.domain_n(i);
+      }
+
+      range(): RangeSort {
+        return this.sort.range();
+      }
+
+      select(...indices: ArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name> {
+        const args = indices.map((arg, i) => this.domain_n(i).cast(arg as any));
+        if (args.length === 1) {
+          return _toExpr(check(Z3.mk_select(contextPtr, this.ast, args[0].ast))) as SortToExprMap<RangeSort, Name>;
+        }
+        const _args = args.map(arg => arg.ast);
+        return _toExpr(check(Z3.mk_select_n(contextPtr, this.ast, _args))) as SortToExprMap<RangeSort, Name>;
+      }
+
+      store(
+        ...indicesAndValue: [
+          ...ArrayIndexType<Name, DomainSort>,
+          CoercibleFromMap<SortToExprMap<RangeSort, Name>, Name>
+        ]
+      ): SMTArray<Name, DomainSort, RangeSort> {
+        const args = indicesAndValue.map((arg, i) => {
+          if (i === indicesAndValue.length - 1) {
+            return this.range().cast(arg as CoercibleFromMap<SortToExprMap<RangeSort, Name>, Name>);
+          }
+          return this.domain_n(i).cast(arg as any);
+        });
+        if (args.length <= 1) {
+          throw new Z3Error("Array store requires both index and value arguments");
+        }
+        if (args.length === 2) {
+          return _toExpr(check(Z3.mk_store(contextPtr, this.ast, args[0].ast, args[1].ast))) as SMTArray<Name, DomainSort, RangeSort>;
+        }
+        const _idxs = args.slice(0, args.length - 1).map(arg => arg.ast);
+        return _toExpr(check(Z3.mk_store_n(contextPtr, this.ast, _idxs, args[args.length - 1].ast))) as SMTArray<Name, DomainSort, RangeSort>;
+      }
+    }
+
     class AstVectorImpl<Item extends AnyAst<Name>> {
       declare readonly __typename: AstVector['__typename'];
       readonly ctx: Context<Name>;
@@ -1744,20 +1929,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return this.values();
       }
 
-      *entries(): IterableIterator<[number, Item]> {
+      * entries(): IterableIterator<[number, Item]> {
         const length = this.length();
         for (let i = 0; i < length; i++) {
           yield [i, this.get(i)];
         }
       }
 
-      *keys(): IterableIterator<number> {
+      * keys(): IterableIterator<number> {
         for (let [key] of this.entries()) {
           yield key;
         }
       }
 
-      *values(): IterableIterator<Item> {
+      * values(): IterableIterator<Item> {
         for (let [, value] of this.entries()) {
           yield value;
         }
@@ -1842,7 +2027,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return Z3.ast_map_size(contextPtr, this.ptr);
       }
 
-      *entries(): IterableIterator<[Key, Value]> {
+      * entries(): IterableIterator<[Key, Value]> {
         for (const key of this.keys()) {
           yield [key, this.get(key)];
         }
@@ -1852,11 +2037,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(Z3.ast_map_keys(contextPtr, this.ptr));
       }
 
-      *values(): IterableIterator<Value> {
+      * values(): IterableIterator<Value> {
         for (const [_, value] of this.entries()) {
           yield value;
         }
       }
+
       get(key: Key): Value {
         return _toAst(check(Z3.ast_map_find(contextPtr, this.ptr, key.ast))) as Value;
       }
@@ -1928,6 +2114,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       isBitVecSort,
       isBitVec,
       isBitVecVal, // TODO fix ordering
+      isArraySort,
+      isArray,
+      isConstArray,
       isProbe,
       isTactic,
       isAstVector,
@@ -1946,6 +2135,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Int,
       Real,
       BitVec,
+      Array,
 
       ////////////////
       // Operations //