diff --git a/src/api/js/examples/high-level/miracle-sudoku.ts b/src/api/js/examples/high-level/miracle-sudoku.ts new file mode 100644 index 000000000..093d599f3 --- /dev/null +++ b/src/api/js/examples/high-level/miracle-sudoku.ts @@ -0,0 +1,206 @@ +import { init } from '../../build/node'; + +import type { Solver, Arith } from '../../build/node'; + +// solve the "miracle sudoku" +// https://www.youtube.com/watch?v=yKf9aUIxdb4 +// most of the interesting stuff is in `solve` +// the process is: +// - parse the board +// - create a Solver +// - create a Z3.Int variable for each square +// - for known cells, add a constraint which says the variable for that cell equals that value +// - add the usual uniqueness constraints +// - add the special "miracle sudoku" constraints +// - call `await solver.check()` +// - if the result is "sat", the board is solvable +// - call `solver.model()` to get a model, i.e. a concrete assignment of variables which satisfies the model +// - for each variable, call `model.evaluate(v)` to recover its value + +function parseSudoku(str: string) { + // derive a list of { row, col, val } records, one for each specified position + // from a string like + // ....1..3. + // ..9..5..8 + // 8.4..6.25 + // ......6.. + // ..8..4... + // 12..87... + // 3..9..2.. + // .65..8... + // 9........ + + let cells = []; + + let lines = str.trim().split('\n'); + if (lines.length !== 9) { + throw new Error(`expected 9 lines, got ${lines.length}`); + } + for (let row = 0; row < 9; ++row) { + let line = lines[row].trim(); + if (line.length !== 9) { + throw new Error(`expected line of length 9, got length ${line.length}`); + } + for (let col = 0; col < 9; ++col) { + let char = line[col]; + if (char === '.') { + continue; + } + if (char < '1' || char > '9') { + throw new Error(`expected digit or '.', got ${char}`); + } + cells.push({ row, col, value: char.codePointAt(0)! - 48 /* '0' */ }); + } + } + return cells; +} + +(async () => { + let { Context, em } = await init(); + + // if you use 'main' as your context name, you won't need to name it in types like Solver + // if you're creating multiple contexts, give them different names + // then the type system will prevent you from mixing them + let Z3 = Context('main'); + + function addSudokuConstraints(solver: Solver, cells: Arith[][]) { + // the usual constraints: + + // every square is between 1 and 9 + for (let row of cells) { + for (let cell of row) { + solver.add(cell.ge(1)); + solver.add(cell.le(9)); + } + } + + // values in each row are unique + for (let row of cells) { + solver.add(Z3.Distinct(...row)); + } + + // values in each column are unique + for (let col = 0; col < 9; ++col) { + solver.add(Z3.Distinct(...cells.map(row => row[col]))); + } + + // values in each 3x3 subdivision are unique + for (let suprow = 0; suprow < 3; ++suprow) { + for (let supcol = 0; supcol < 3; ++supcol) { + let square = []; + for (let row = 0; row < 3; ++row) { + for (let col = 0; col < 3; ++col) { + square.push(cells[suprow * 3 + row][supcol * 3 + col]); + } + } + solver.add(Z3.Distinct(...square)); + } + } + } + + function applyOffsets(x: number, y: number, offsets: [number, number][]) { + let out = []; + for (let offset of offsets) { + let rx = x + offset[0]; + let ry = y + offset[1]; + if (rx >= 0 && rx < 9 && ry >= 0 && ry < 8) { + out.push({ x: rx, y: ry }); + } + } + return out; + } + + function addMiracleConstraints(s: Solver, cells: Arith[][]) { + // the special "miracle sudoku" constraints + + // any two cells separated by a knight's move or a kings move cannot contain the same digit + let knightOffets: [number, number][] = [ + [1, -2], + [2, -1], + [2, 1], + [1, 2], + [-1, 2], + [-2, 1], + [-2, -1], + [-1, -2], + ]; + let kingOffsets: [number, number][] = [ + [1, 1], + [1, -1], + [-1, 1], + [-1, -1], + ]; // skipping immediately adjacent because those are covered by normal sudoku rules + let allOffets = [...knightOffets, ...kingOffsets]; + for (let row = 0; row < 9; ++row) { + for (let col = 0; col < 9; ++col) { + for (let { x, y } of applyOffsets(row, col, allOffets)) { + s.add(cells[row][col].neq(cells[x][y])); + } + } + } + + // any two orthogonally adjacent cells cannot contain consecutive digits + let orthoOffsets: [number, number][] = [ + [0, 1], + [0, -1], + [1, 0], + [-1, 0], + ]; + for (let row = 0; row < 9; ++row) { + for (let col = 0; col < 9; ++col) { + for (let { x, y } of applyOffsets(row, col, orthoOffsets)) { + s.add(cells[row][col].sub(cells[x][y]).neq(1)); + } + } + } + } + + async function solve(str: string) { + let solver = new Z3.Solver(); + let cells = Array.from({ length: 9 }, (_, col) => Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`))); + for (let { row, col, value } of parseSudoku(str)) { + solver.add(cells[row][col].eq(value)); + } + addSudokuConstraints(solver, cells); + addMiracleConstraints(solver, cells); // remove this line to solve normal sudokus + + let start = Date.now(); + console.log('starting... this may take a minute or two'); + let check = await solver.check(); + console.log(`problem was determined to be ${check} in ${Date.now() - start} ms`); + if (check === 'sat') { + let model = solver.model(); + let str = ''; + for (let row = 0; row < 9; ++row) { + for (let col = 0; col < 9; ++col) { + str += model.eval(cells[row][col]).toString() + (col === 8 ? '' : ' '); + if (col === 2 || col === 5) { + str += ' '; + } + } + str += '\n'; + if (row === 2 || row === 5) { + str += '\n'; + } + } + console.log(str); + } + } + + await solve(` +......... +......... +......... +......... +..1...... +......2.. +......... +......... +......... +`); + + em.PThread.terminateAllThreads(); +})().catch(e => { + console.error('error', e); + process.exit(1); +}); diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index 9555eea31..9ec7d6eca 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -1,7 +1,7 @@ import assert from 'assert'; import asyncToArray from 'iter-tools/methods/async-to-array'; import { init, killThreads } from '../jest'; -import { Arith, Bool, Model, sat, unsat, Z3AssertionError, Z3HighLevel } from './types'; +import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types'; /** * Generate all possible solutions from given assumptions. @@ -31,7 +31,7 @@ async function* allSolutions(...assertions: Bool[]): const solver = new assertions[0].ctx.Solver(); solver.add(...assertions); - while ((await solver.check()) === sat) { + while ((await solver.check()) === 'sat') { const model = solver.model(); const decls = model.decls(); if (decls.length === 0) { @@ -59,13 +59,13 @@ async function prove(conjecture: Bool): Promise { const solver = new conjecture.ctx.Solver(); const { Not } = solver.ctx; solver.add(Not(conjecture)); - expect(await solver.check()).toStrictEqual(unsat); + expect(await solver.check()).toStrictEqual('unsat'); } async function solve(conjecture: Bool): Promise { const solver = new conjecture.ctx.Solver(); solver.add(conjecture); - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); return solver.model(); } @@ -96,7 +96,7 @@ describe('high-level', () => { }); it('proves x = y implies g(x) = g(y)', async () => { - const { Solver, Int, Function, Implies, Not } = new api.Context('main'); + const { Solver, Int, Function, Implies, Not } = api.Context('main'); const solver = new Solver(); const sort = Int.sort(); @@ -106,11 +106,11 @@ describe('high-level', () => { const conjecture = Implies(x.eq(y), g.call(x).eq(g.call(y))); solver.add(Not(conjecture)); - expect(await solver.check()).toStrictEqual(unsat); + expect(await solver.check()).toStrictEqual('unsat'); }); it('disproves x = y implies g(g(x)) = g(y)', async () => { - const { Solver, Int, Function, Implies, Not } = new api.Context('main'); + const { Solver, Int, Function, Implies, Not } = api.Context('main'); const solver = new Solver(); const sort = Int.sort(); @@ -119,14 +119,14 @@ describe('high-level', () => { const g = Function.declare('g', sort, sort); const conjecture = Implies(x.eq(y), g.call(g.call(x)).eq(g.call(y))); solver.add(Not(conjecture)); - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); }); it('checks that Context matches', () => { - const c1 = new api.Context('context'); - const c2 = new api.Context('context'); - const c3 = new api.Context('foo'); - const c4 = new api.Context('bar'); + const c1 = api.Context('context'); + const c2 = api.Context('context'); + const c3 = api.Context('foo'); + const c4 = api.Context('bar'); // Contexts with the same name don't do type checking during compile time. // We need to check for different context dynamically @@ -144,7 +144,7 @@ describe('high-level', () => { describe('booleans', () => { it("proves De Morgan's Law", async () => { - const { Bool, Not, And, Eq, Or } = new api.Context('main'); + const { Bool, Not, And, Eq, Or } = api.Context('main'); const [x, y] = [Bool.const('x'), Bool.const('y')]; const conjecture = Eq(Not(And(x, y)), Or(Not(x), Not(y))); @@ -155,7 +155,7 @@ describe('high-level', () => { describe('ints', () => { it('finds a model', async () => { - const { Solver, Int, isIntVal } = new api.Context('main'); + const { Solver, Int, isIntVal } = api.Context('main'); const solver = new Solver(); const x = Int.const('x'); const y = Int.const('y'); @@ -163,10 +163,10 @@ describe('high-level', () => { solver.add(x.ge(1)); // x >= 1 solver.add(y.lt(x.add(3))); // y < x + 3 - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); const model = solver.model(); - expect(model.length).toStrictEqual(2); + expect(model.length()).toStrictEqual(2); for (const decl of model) { expect(decl.arity()).toStrictEqual(0); @@ -175,8 +175,8 @@ describe('high-level', () => { const yValueExpr = model.get(y); assert(isIntVal(xValueExpr)); assert(isIntVal(yValueExpr)); - const xValue = xValueExpr.value; - const yValue = yValueExpr.value; + const xValue = xValueExpr.value(); + const yValue = yValueExpr.value(); assert(typeof xValue === 'bigint'); assert(typeof yValue === 'bigint'); expect(xValue).toBeGreaterThanOrEqual(1n); @@ -225,7 +225,7 @@ describe('high-level', () => { 541972386 `); - const { Solver, Int, Distinct, isIntVal } = new api.Context('main'); + const { Solver, Int, Distinct, isIntVal } = api.Context('main'); const cells: Arith[][] = []; // 9x9 matrix of integer variables @@ -284,7 +284,7 @@ describe('high-level', () => { } } - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); const model = solver.model(); const result = []; @@ -293,7 +293,7 @@ describe('high-level', () => { for (let j = 0; j < 9; j++) { const cell = model.eval(cells[i][j]); assert(isIntVal(cell)); - const value = cell.value; + const value = cell.value(); assert(typeof value === 'bigint'); expect(value).toBeGreaterThanOrEqual(0n); expect(value).toBeLessThanOrEqual(9n); @@ -308,7 +308,7 @@ describe('high-level', () => { describe('reals', () => { it('can work with numerals', async () => { - const { Real, And } = new api.Context('main'); + const { Real, And } = api.Context('main'); const n1 = Real.val('1/2'); const n2 = Real.val('0.5'); const n3 = Real.val(0.5); @@ -322,7 +322,7 @@ describe('high-level', () => { it('can do non-linear arithmetic', async () => { api.setParam('pp.decimal', true); api.setParam('pp.decimal_precision', 20); - const { Real, Solver, isReal, isRealVal } = new api.Context('main'); + const { Real, Solver, isReal, isRealVal } = api.Context('main'); const x = Real.const('x'); const y = Real.const('y'); const z = Real.const('z'); @@ -331,7 +331,7 @@ describe('high-level', () => { solver.add(x.mul(x).add(y.mul(y)).eq(1)); // x^2 + y^2 == 1 solver.add(x.mul(x).mul(x).add(z.mul(z).mul(z)).lt('1/2')); // x^3 + z^3 < 1/2 - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); const model = solver.model(); expect(isRealVal(model.get(x))).toStrictEqual(true); @@ -344,7 +344,7 @@ describe('high-level', () => { describe('bitvectors', () => { it('can do simple proofs', async () => { - const { BitVec, Concat, Implies, isBitVecVal } = new api.Context('main'); + const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main'); const x = BitVec.const('x', 32); @@ -354,7 +354,7 @@ describe('high-level', () => { assert(isBitVecVal(sSol) && isBitVecVal(uSol)); let v = sSol.asSignedValue(); expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true); - v = uSol.value; + v = uSol.value(); expect(v - 10n <= 0n === v <= 10n).toStrictEqual(true); const y = BitVec.const('y', 32); @@ -363,7 +363,7 @@ describe('high-level', () => { }); it('finds x and y such that: x ^ y - 103 == x * y', async () => { - const { BitVec, isBitVecVal } = new api.Context('main'); + const { BitVec, isBitVecVal } = api.Context('main'); const x = BitVec.const('x', 32); const y = BitVec.const('y', 32); @@ -382,28 +382,28 @@ describe('high-level', () => { describe('Solver', () => { it('can use push and pop', async () => { - const { Solver, Int } = new api.Context('main'); + const { Solver, Int } = api.Context('main'); const solver = new Solver(); const x = Int.const('x'); solver.add(x.gt(0)); - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); solver.push(); solver.add(x.lt(0)); expect(solver.numScopes()).toStrictEqual(1); - expect(await solver.check()).toStrictEqual(unsat); + expect(await solver.check()).toStrictEqual('unsat'); solver.pop(); expect(solver.numScopes()).toStrictEqual(0); - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); }); it('can find multiple solutions', async () => { - const { Int, isIntVal } = new api.Context('main'); + const { Int, isIntVal } = api.Context('main'); const x = Int.const('x'); @@ -413,7 +413,7 @@ describe('high-level', () => { .map(solution => { const expr = solution.eval(x); assert(isIntVal(expr)); - return expr.value; + return expr.value(); }) .sort((a, b) => { assert(a !== null && b !== null && typeof a === 'bigint' && typeof b === 'bigint'); @@ -431,7 +431,7 @@ describe('high-level', () => { describe('AstVector', () => { it('can use basic methods', async () => { - const { Solver, AstVector, Int } = new api.Context('main'); + const { Solver, AstVector, Int } = api.Context('main'); const solver = new Solver(); const vector = new AstVector(); @@ -439,12 +439,12 @@ describe('high-level', () => { vector.push(Int.const(`int__${i}`)); } - const length = vector.length; + const length = vector.length(); for (let i = 0; i < length; i++) { solver.add(vector.get(i).gt(1)); } - expect(await solver.check()).toStrictEqual(sat); + expect(await solver.check()).toStrictEqual('sat'); }); }); }); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 731e47b07..c68e803f9 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -18,6 +18,7 @@ import { Z3_ast_vector, Z3_context, Z3_decl_kind, + Z3_error_code, Z3_func_decl, Z3_func_interp, Z3_lbool, @@ -62,17 +63,14 @@ import { Model, Probe, RatNum, - sat, Solver, Sort, SortToExprMap, Tactic, - unknown, - unsat, Z3Error, Z3HighLevel, } from './types'; -import { allSatisfy, assert, assertExhaustive, autoBind } from './utils'; +import { allSatisfy, assert, assertExhaustive } from './utils'; const FALLBACK_PRECISION = 17; @@ -150,738 +148,112 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return Z3.global_param_get(name); } - function isContext(obj: unknown): obj is Context { - return obj instanceof ContextImpl; - } + function createContext(name: Name, options?: Record): Context { + const cfg = Z3.mk_config(); + if (options != null) { + 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); + Z3.del_config(cfg); - class ContextImpl implements Context { - declare readonly __typename: Context['__typename']; - - readonly ptr: Z3_context; - readonly name: string; - - constructor(name: string, params: Record = {}) { - const cfg = Z3.mk_config(); - Object.entries(params).forEach(([key, value]) => Z3.set_param_value(cfg, key, value.toString())); - const context = Z3.mk_context_rc(cfg); - - this.ptr = context; - this.name = name; - - Z3.set_ast_print_mode(this.ptr, Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - Z3.del_config(cfg); - - // We want to bind functions and operations to `this` inside Context - // So that the user can write things like this and have it work: - // ``` - // const { And, Or } = new Context('main'); - // ``` - // - // Typescript doesn't handle overloading of method fields, only - // methods. We can't use closures to bind this, so we use auto-bind library - // ``` - // class { - // // This works - // test(a: boolean): boolean; - // test(a: number): number; - // test(a: boolean | number): boolean | number { - // return 0; - // } - // - // // This fails to compile - // test2: (a: boolean) => boolean; - // test2: (a: number) => number; - // test2 = (a: boolean | number): boolean | number => { - // return 0; - // } - // } - // ``` - autoBind(this); - - cleanup.register(this, () => Z3.del_context(context)); + function _assertContext(...ctxs: (Context | { ctx: Context })[]) { + ctxs.forEach(other => assert('ctx' in other ? ctx === other.ctx : ctx === other, 'Context mismatch')); } - /////////////// - // Functions // - /////////////// - interrupt(): void { - Z3.interrupt(this.ptr); - } - - isModel(obj: unknown): obj is Model { - const r = obj instanceof ModelImpl; - r && this._assertContext(obj); - return r; - } - - isAst(obj: unknown): obj is Ast { - const r = obj instanceof AstImpl; - r && this._assertContext(obj); - return r; - } - - isSort(obj: unknown): obj is Sort { - const r = obj instanceof SortImpl; - r && this._assertContext(obj); - return r; - } - - isFuncDecl(obj: unknown): obj is FuncDecl { - const r = obj instanceof FuncDeclImpl; - r && this._assertContext(obj); - return r; - } - - isApp(obj: unknown): boolean { - if (!this.isExpr(obj)) { - return false; - } - const kind = Z3.get_ast_kind(this.ptr, obj.ast); - return kind === Z3_ast_kind.Z3_NUMERAL_AST || kind === Z3_ast_kind.Z3_APP_AST; - } - - isConst(obj: unknown): boolean { - return this.isExpr(obj) && this.isApp(obj) && obj.numArgs() === 0; - } - - isExpr(obj: unknown): obj is Expr { - const r = obj instanceof ExprImpl; - r && this._assertContext(obj); - return r; - } - - isVar(obj: unknown): boolean { - return this.isExpr(obj) && Z3.get_ast_kind(this.ptr, obj.ast) === Z3_ast_kind.Z3_VAR_AST; - } - - isAppOf(obj: unknown, kind: Z3_decl_kind): boolean { - return this.isExpr(obj) && this.isApp(obj) && obj.decl().kind() === kind; - } - - isBool(obj: unknown): obj is Bool { - const r = obj instanceof BoolImpl; - r && this._assertContext(obj); - return r; - } - - isTrue(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_TRUE); - } - - isFalse(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_FALSE); - } - - isAnd(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_AND); - } - - isOr(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_OR); - } - - isImplies(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_IMPLIES); - } - - isNot(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_NOT); - } - - isEq(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_EQ); - } - - isDistinct(obj: unknown): boolean { - return this.isAppOf(obj, Z3_decl_kind.Z3_OP_DISTINCT); - } - - isArith(obj: unknown): obj is Arith { - const r = obj instanceof ArithImpl; - r && this._assertContext(obj); - return r; - } - - isArithSort(obj: unknown): obj is ArithSort { - const r = obj instanceof ArithSortImpl; - r && this._assertContext(obj); - return r; - } - - isInt(obj: unknown): boolean { - return this.isArith(obj) && this.isIntSort(obj.sort); - } - - isIntVal(obj: unknown): obj is IntNum { - const r = obj instanceof IntNumImpl; - r && this._assertContext(obj); - return r; - } - - isIntSort(obj: unknown): boolean { - return this.isSort(obj) && obj.kind() === Z3_sort_kind.Z3_INT_SORT; - } - - isReal(obj: unknown): boolean { - return this.isArith(obj) && this.isRealSort(obj.sort); - } - - isRealVal(obj: unknown): obj is RatNum { - const r = obj instanceof RatNumImpl; - r && this._assertContext(obj); - return r; - } - - isRealSort(obj: unknown): boolean { - return this.isSort(obj) && obj.kind() === Z3_sort_kind.Z3_REAL_SORT; - } - - isBitVecSort(obj: unknown): obj is BitVecSort { - const r = obj instanceof BitVecSortImpl; - r && this._assertContext(obj); - return r; - } - - isBitVec(obj: unknown): obj is BitVec { - const r = obj instanceof BitVecImpl; - r && this._assertContext(obj); - return r; - } - - isBitVecVal(obj: unknown): obj is BitVecNum { - const r = obj instanceof BitVecNumImpl; - r && this._assertContext(obj); - return r; - } - - isProbe(obj: unknown): obj is Probe { - const r = obj instanceof ProbeImpl; - r && this._assertContext(obj); - return r; - } - - isTactic(obj: unknown): obj is Tactic { - const r = obj instanceof TacticImpl; - r && this._assertContext(obj); - return r; - } - - isAstVector(obj: unknown): obj is AstVector { - const r = obj instanceof AstVectorImpl; - r && this._assertContext(obj); - return r; - } - - eqIdentity(a: Ast, b: Ast): boolean { - return a.eqIdentity(b); - } - - getVarIndex(obj: Expr): number { - assert(this.isVar(obj), 'Z3 bound variable expected'); - return Z3.get_index_value(this.ptr, obj.ast); - } - - from(primitive: boolean): Bool; - from(primitive: number | CoercibleRational): RatNum; - from(primitive: bigint): IntNum; - from(expr: T): T; - from(expr: CoercibleToExpr): AnyExpr; - from(value: CoercibleToExpr): AnyExpr { - if (typeof value === 'boolean') { - return this.Bool.val(value); - } else if (typeof value === 'number' || isCoercibleRational(value)) { - return this.Real.val(value); - } else if (typeof value === 'bigint') { - return this.Int.val(value); - } else if (this.isExpr(value)) { - return value; - } - assert(false); - } - - async solve(...assertions: Bool[]): Promise { - const solver = new this.Solver(); - solver.add(...assertions); - const result = await solver.check(); - if (result === sat) { - return solver.model(); - } - return result; - } - - ///////////// - // Classes // - ///////////// - readonly Solver = SolverImpl.bind(SolverImpl, this); - readonly Model = ModelImpl.bind(ModelImpl, this); - readonly Tactic = TacticImpl.bind(TacticImpl, this); - readonly AstVector = AstVectorImpl.bind(AstVectorImpl, this) as AstVectorCtor; - readonly AstMap = AstMapImpl.bind(AstMapImpl, this) as AstMapCtor; - - ///////////// - // Objects // - ///////////// - readonly Sort = { - declare: (name: string) => new SortImpl(this, Z3.mk_uninterpreted_sort(this.ptr, this._toSymbol(name))), - }; - readonly Function = { - declare: (name: string, ...signature: FuncDeclSignature) => { - const arity = signature.length - 1; - const rng = signature[arity]; - this._assertContext(rng); - const dom = []; - for (let i = 0; i < arity; i++) { - this._assertContext(signature[i]); - dom.push(signature[i].ptr); - } - return new FuncDeclImpl(this, Z3.mk_func_decl(this.ptr, this._toSymbol(name), dom, rng.ptr)); - }, - fresh: (...signature: FuncDeclSignature) => { - const arity = signature.length - 1; - const rng = signature[arity]; - this._assertContext(rng); - const dom = []; - for (let i = 0; i < arity; i++) { - this._assertContext(signature[i]); - dom.push(signature[i].ptr); - } - return new FuncDeclImpl(this, Z3.mk_fresh_func_decl(this.ptr, 'f', dom, rng.ptr)); - }, - }; - readonly RecFunc = { - declare: (name: string, ...signature: FuncDeclSignature) => { - const arity = signature.length - 1; - const rng = signature[arity]; - this._assertContext(rng); - const dom = []; - for (let i = 0; i < arity; i++) { - this._assertContext(signature[i]); - dom.push(signature[i].ptr); - } - return new FuncDeclImpl(this, Z3.mk_rec_func_decl(this.ptr, this._toSymbol(name), dom, rng.ptr)); - }, - - addDefinition: (f: FuncDecl, args: Expr[], body: Expr) => { - this._assertContext(f, ...args, body); - Z3.add_rec_def( - this.ptr, - f.ptr, - args.map(arg => arg.ast), - body.ast, - ); - }, - }; - readonly Bool = { - sort: () => new BoolSortImpl(this, Z3.mk_bool_sort(this.ptr)), - - const: (name: string) => new BoolImpl(this, Z3.mk_const(this.ptr, this._toSymbol(name), this.Bool.sort().ptr)), - consts: (names: string | string[]) => { - if (typeof names === 'string') { - names = names.split(' '); - } - return names.map(name => this.Bool.const(name)); - }, - vector: (prefix: string, count: number) => { - const result = []; - for (let i = 0; i < count; i++) { - result.push(this.Bool.const(`${prefix}__${i}`)); - } - return result; - }, - fresh: (prefix = 'b') => new BoolImpl(this, Z3.mk_fresh_const(this.ptr, prefix, this.Bool.sort().ptr)), - - val: (value: boolean) => { - if (value) { - return new BoolImpl(this, Z3.mk_true(this.ptr)); - } - return new BoolImpl(this, Z3.mk_false(this.ptr)); - }, - }; - readonly Int = { - sort: () => new ArithSortImpl(this, Z3.mk_int_sort(this.ptr)), - - const: (name: string) => new ArithImpl(this, Z3.mk_const(this.ptr, this._toSymbol(name), this.Int.sort().ptr)), - consts: (names: string | string[]) => { - if (typeof names === 'string') { - names = names.split(' '); - } - return names.map(name => this.Int.const(name)); - }, - vector: (prefix: string, count: number) => { - const result = []; - for (let i = 0; i < count; i++) { - result.push(this.Int.const(`${prefix}__${i}`)); - } - return result; - }, - fresh: (prefix = 'x') => new ArithImpl(this, Z3.mk_fresh_const(this.ptr, prefix, this.Int.sort().ptr)), - - val: (value: number | bigint | string) => { - assert(typeof value === 'bigint' || typeof value === 'string' || Number.isSafeInteger(value)); - return new IntNumImpl(this, Z3.mk_numeral(this.ptr, value.toString(), this.Int.sort().ptr)); - }, - }; - readonly Real = { - sort: () => new ArithSortImpl(this, Z3.mk_real_sort(this.ptr)), - - const: (name: string) => new ArithImpl(this, Z3.mk_const(this.ptr, this._toSymbol(name), this.Real.sort().ptr)), - consts: (names: string | string[]) => { - if (typeof names === 'string') { - names = names.split(' '); - } - return names.map(name => this.Real.const(name)); - }, - vector: (prefix: string, count: number) => { - const result = []; - for (let i = 0; i < count; i++) { - result.push(this.Real.const(`${prefix}__${i}`)); - } - return result; - }, - fresh: (prefix = 'b') => new ArithImpl(this, Z3.mk_fresh_const(this.ptr, prefix, this.Real.sort().ptr)), - - val: (value: number | bigint | string | CoercibleRational) => { - if (isCoercibleRational(value)) { - value = `${value.numerator}/${value.denominator}`; - } - return new RatNumImpl(this, Z3.mk_numeral(this.ptr, value.toString(), this.Real.sort().ptr)); - }, - }; - readonly BitVec = { - sort: (bits: number): BitVecSort => { - assert(Number.isSafeInteger(bits), 'number of bits must be an integer'); - return new BitVecSortImpl(this, Z3.mk_bv_sort(this.ptr, bits)); - }, - - const: (name: string, bits: number | BitVecSort): BitVec => - new BitVecImpl( - this, - Z3.mk_const(this.ptr, this._toSymbol(name), this.isBitVecSort(bits) ? bits.ptr : this.BitVec.sort(bits).ptr), - ), - - consts: (names: string | string[], bits: number | BitVecSort): BitVec[] => { - if (typeof names === 'string') { - names = names.split(' '); - } - return names.map(name => this.BitVec.const(name, bits)); - }, - - val: (value: bigint | number | boolean, bits: number | BitVecSort): BitVecNum => { - if (value === true) { - return this.BitVec.val(1, bits); - } else if (value === false) { - return this.BitVec.val(0, bits); - } - return new BitVecNumImpl( - this, - Z3.mk_numeral(this.ptr, value.toString(), this.isBitVecSort(bits) ? bits.ptr : this.BitVec.sort(bits).ptr), - ); - }, - }; - - //////////////// - // Operations // - //////////////// - If(condition: Probe, onTrue: Tactic, onFalse: Tactic): Tactic; - If( - condition: Bool | boolean, - onTrue: OnTrueRef, - onFalse: OnFalseRef, - ): CoercibleToExprMap; - If( - condition: Bool | Probe | boolean, - onTrue: CoercibleToExpr | Tactic, - onFalse: CoercibleToExpr | Tactic, - ): Expr | Tactic { - if (this.isProbe(condition) && this.isTactic(onTrue) && this.isTactic(onFalse)) { - return this.Cond(condition, onTrue, onFalse); - } - assert( - !this.isProbe(condition) && !this.isTactic(onTrue) && !this.isTactic(onFalse), - 'Mixed expressions and goals', - ); - if (typeof condition === 'boolean') { - condition = this.Bool.val(condition); - } - onTrue = this.from(onTrue); - onFalse = this.from(onFalse); - return this._toExpr(Z3.mk_ite(this.ptr, condition.ptr, onTrue.ast, onFalse.ast)); - } - - Distinct(...exprs: CoercibleToExpr[]): Bool { - assert(exprs.length > 0, "Can't make Distinct ouf of nothing"); - - return new BoolImpl( - this, - Z3.mk_distinct( - this.ptr, - exprs.map(expr => { - expr = this.from(expr); - this._assertContext(expr); - return expr.ast; - }), - ), - ); - } - - Const(name: string, sort: S): SortToExprMap { - this._assertContext(sort); - return this._toExpr(Z3.mk_const(this.ptr, this._toSymbol(name), sort.ptr)) as SortToExprMap; - } - - Consts(names: string | string[], sort: S): SortToExprMap[] { - this._assertContext(sort); - if (typeof names === 'string') { - names = names.split(' '); - } - return names.map(name => this.Const(name, sort)); - } - - FreshConst(sort: S, prefix: string = 'c'): SortToExprMap { - this._assertContext(sort); - return this._toExpr(Z3.mk_fresh_const(sort.ctx.ptr, prefix, sort.ptr)) as SortToExprMap; - } - - Var(idx: number, sort: S): SortToExprMap { - this._assertContext(sort); - return this._toExpr(Z3.mk_bound(sort.ctx.ptr, idx, sort.ptr)) as SortToExprMap; - } - - Implies(a: Bool | boolean, b: Bool | boolean): Bool { - a = this.from(a) as Bool; - b = this.from(b) as Bool; - this._assertContext(a, b); - return new BoolImpl(this, Z3.mk_implies(this.ptr, a.ptr, b.ptr)); - } - - Eq(a: CoercibleToExpr, b: CoercibleToExpr): Bool { - a = this.from(a); - b = this.from(b); - this._assertContext(a, b); - return a.eq(b); - } - - Xor(a: Bool | boolean, b: Bool | boolean): Bool { - a = this.from(a) as Bool; - b = this.from(b) as Bool; - this._assertContext(a, b); - return new BoolImpl(this, Z3.mk_xor(this.ptr, a.ptr, b.ptr)); - } - - Not(a: Probe): Probe; - Not(a: Bool | boolean): Bool; - Not(a: Bool | boolean | Probe): Bool | Probe { - if (typeof a === 'boolean') { - a = this.from(a); - } - this._assertContext(a); - if (this.isProbe(a)) { - return new ProbeImpl(this, Z3.probe_not(this.ptr, a.ptr)); - } - return new BoolImpl(this, Z3.mk_not(this.ptr, a.ptr)); - } - - And(): Bool; - And(vector: AstVector): Bool; - And(...args: (Bool | boolean)[]): Bool; - And(...args: Probe[]): Probe; - And(...args: (AstVector | Probe | Bool | boolean)[]): Bool | Probe { - if (args.length == 1 && args[0] instanceof this.AstVector) { - args = [...args[0].values()]; - assert(allSatisfy(args, this.isBool.bind(this)) ?? true, 'AstVector containing not bools'); - } - - const allProbes = allSatisfy(args, this.isProbe.bind(this)) ?? false; - if (allProbes) { - return this._probeNary(Z3.probe_and, args as [Probe, ...Probe[]]); - } else { - args = args.map(this.from.bind(this)) as Bool[]; - this._assertContext(...(args as Bool[])); - return new BoolImpl( - this, - Z3.mk_and( - this.ptr, - args.map(arg => (arg as Bool).ptr), - ), - ); + // call this after every nontrivial call to the underlying API + function throwIfError() { + if (Z3.get_error_code(contextPtr) !== Z3_error_code.Z3_OK) { + throw new Error(Z3.get_error_msg(ctx.ptr, Z3.get_error_code(ctx.ptr))); } } - Or(): Bool; - Or(vector: AstVector): Bool; - Or(...args: (Bool | boolean)[]): Bool; - Or(...args: Probe[]): Probe; - Or(...args: (AstVector | Probe | Bool | boolean)[]): Bool | Probe { - if (args.length == 1 && args[0] instanceof this.AstVector) { - args = [...args[0].values()]; - assert(allSatisfy(args, this.isBool.bind(this)) ?? true, 'AstVector containing not bools'); - } - - const allProbes = allSatisfy(args, this.isProbe.bind(this)) ?? false; - if (allProbes) { - return this._probeNary(Z3.probe_or, args as [Probe, ...Probe[]]); - } else { - args = args.map(this.from.bind(this)) as Bool[]; - this._assertContext(...(args as Bool[])); - return new BoolImpl( - this, - Z3.mk_or( - this.ptr, - args.map(arg => (arg as Bool).ptr), - ), - ); - } - } - - ToReal(expr: Arith | bigint): Arith { - expr = this.from(expr) as Arith; - this._assertContext(expr); - assert(this.isInt(expr), 'Int expression expected'); - return new ArithImpl(this, Z3.mk_int2real(this.ptr, expr.ast)); - } - - ToInt(expr: Arith | number | CoercibleRational | string): Arith { - if (!this.isExpr(expr)) { - expr = this.Real.val(expr); - } - this._assertContext(expr); - assert(this.isReal(expr), 'Real expression expected'); - return new ArithImpl(this, Z3.mk_real2int(this.ptr, expr.ast)); - } - - IsInt(expr: Arith | number | CoercibleRational | string): Bool { - if (!this.isExpr(expr)) { - expr = this.Real.val(expr); - } - this._assertContext(expr); - assert(this.isReal(expr), 'Real expression expected'); - return new BoolImpl(this, Z3.mk_is_int(this.ptr, expr.ast)); - } - - Sqrt(a: Arith | number | bigint | string | CoercibleRational): Arith { - if (!this.isExpr(a)) { - a = this.Real.val(a); - } - return a.pow('1/2'); - } - - Cbrt(a: Arith | number | bigint | string | CoercibleRational): Arith { - if (!this.isExpr(a)) { - a = this.Real.val(a); - } - return a.pow('1/3'); - } - - BV2Int(a: BitVec, isSigned: boolean): Arith { - this._assertContext(a); - return new ArithImpl(this, Z3.mk_bv2int(this.ptr, a.ast, isSigned)); - } - - Int2BV(a: Arith | bigint | number, bits: number): BitVec { - if (this.isArith(a)) { - assert(this.isInt(a), 'parameter must be an integer'); - } else { - assert(typeof a !== 'number' || Number.isSafeInteger(a), 'parameter must not have decimal places'); - a = this.Int.val(a); - } - return new BitVecImpl(this, Z3.mk_int2bv(this.ptr, bits, a.ast)); - } - - Concat(...bitvecs: BitVec[]): BitVec { - this._assertContext(...bitvecs); - return bitvecs.reduce((prev, curr) => new BitVecImpl(this, Z3.mk_concat(this.ptr, prev.ast, curr.ast))); - } - - Cond(probe: Probe, onTrue: Tactic, onFalse: Tactic): Tactic { - this._assertContext(probe, onTrue, onFalse); - return new this.Tactic(Z3.tactic_cond(this.ptr, probe.ptr, onTrue.ptr, onFalse.ptr)); + function check(val: T) { + throwIfError(); + return val; } ///////////// // Private // ///////////// - _assertContext(...ctxs: (Context | { ctx: Context })[]) { - ctxs.forEach(other => assert('ctx' in other ? this === other.ctx : this === other, 'Context mismatch')); - } - - _toSymbol(s: string | number) { + function _toSymbol(s: string | number) { if (typeof s === 'number') { - return Z3.mk_int_symbol(this.ptr, s); + return check(Z3.mk_int_symbol(contextPtr, s)); } else { - return Z3.mk_string_symbol(this.ptr, s); + return check(Z3.mk_string_symbol(contextPtr, s)); } } - _fromSymbol(sym: Z3_symbol) { - const kind = Z3.get_symbol_kind(this.ptr, sym); + function _fromSymbol(sym: Z3_symbol) { + const kind = check(Z3.get_symbol_kind(contextPtr, sym)); switch (kind) { case Z3_symbol_kind.Z3_INT_SYMBOL: - return Z3.get_symbol_int(this.ptr, sym); + return Z3.get_symbol_int(contextPtr, sym); case Z3_symbol_kind.Z3_STRING_SYMBOL: - return Z3.get_symbol_string(this.ptr, sym); + return Z3.get_symbol_string(contextPtr, sym); default: assertExhaustive(kind); } } - _toAst(ast: Z3_ast): AnyAst { - switch (Z3.get_ast_kind(this.ptr, ast)) { + function _toAst(ast: Z3_ast): AnyAst { + switch (check(Z3.get_ast_kind(contextPtr, ast))) { case Z3_ast_kind.Z3_SORT_AST: - return this._toSort(ast as Z3_sort); + return _toSort(ast as Z3_sort); case Z3_ast_kind.Z3_FUNC_DECL_AST: - return new FuncDeclImpl(this, ast as Z3_func_decl); + return new FuncDeclImpl(ast as Z3_func_decl); default: - return this._toExpr(ast); + return _toExpr(ast); } } - _toSort(ast: Z3_sort): AnySort { - switch (Z3.get_sort_kind(this.ptr, ast)) { + function _toSort(ast: Z3_sort): AnySort { + switch (check(Z3.get_sort_kind(contextPtr, ast))) { case Z3_sort_kind.Z3_BOOL_SORT: - return new BoolSortImpl(this, ast); + return new BoolSortImpl(ast); case Z3_sort_kind.Z3_INT_SORT: case Z3_sort_kind.Z3_REAL_SORT: - return new ArithSortImpl(this, ast); + return new ArithSortImpl(ast); case Z3_sort_kind.Z3_BV_SORT: - return new BitVecSortImpl(this, ast); + return new BitVecSortImpl(ast); default: - return new SortImpl(this, ast); + return new SortImpl(ast); } } - _toExpr(ast: Z3_ast): Bool | IntNum | RatNum | Arith | Expr { - const kind = Z3.get_ast_kind(this.ptr, ast); + function _toExpr(ast: Z3_ast): Bool | IntNum | RatNum | Arith | Expr { + const kind = check(Z3.get_ast_kind(contextPtr, ast)); if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) { assert(false); } - const sortKind = Z3.get_sort_kind(this.ptr, Z3.get_sort(this.ptr, ast)); + const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast))); switch (sortKind) { case Z3_sort_kind.Z3_BOOL_SORT: - return new BoolImpl(this, ast); + return new BoolImpl(ast); case Z3_sort_kind.Z3_INT_SORT: if (kind === Z3_ast_kind.Z3_NUMERAL_AST) { - return new IntNumImpl(this, ast); + return new IntNumImpl(ast); } - return new ArithImpl(this, ast); + return new ArithImpl(ast); case Z3_sort_kind.Z3_REAL_SORT: if (kind === Z3_ast_kind.Z3_NUMERAL_AST) { - return new RatNumImpl(this, ast); + return new RatNumImpl(ast); } - return new ArithImpl(this, ast); + return new ArithImpl(ast); case Z3_sort_kind.Z3_BV_SORT: if (kind === Z3_ast_kind.Z3_NUMERAL_AST) { - return new BitVecNumImpl(this, ast); + return new BitVecNumImpl(ast); } - return new BitVecImpl(this, ast); + return new BitVecImpl(ast); default: - return new ExprImpl(this, ast); + return new ExprImpl(ast); } } - _flattenArgs(args: (T | AstVector)[]): T[] { + function _flattenArgs = AnyAst>(args: (T | AstVector)[]): T[] { const result: T[] = []; for (const arg of args) { - if (this.isAstVector(arg)) { + if (isAstVector(arg)) { result.push(...arg.values()); } else { result.push(arg); @@ -890,984 +262,1693 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return result; } - _toProbe(p: Probe | Z3_probe): Probe { - if (this.isProbe(p)) { + function _toProbe(p: Probe | Z3_probe): Probe { + if (isProbe(p)) { return p; } - return new ProbeImpl(this, p); + return new ProbeImpl(p); } - _probeNary( + function _probeNary( f: (ctx: Z3_context, left: Z3_probe, right: Z3_probe) => Z3_probe, - args: [Probe | Z3_probe, ...(Probe | Z3_probe)[]], + args: [Probe | Z3_probe, ...(Probe | Z3_probe)[]], ) { assert(args.length > 0, 'At least one argument expected'); - let r = this._toProbe(args[0]); + let r = _toProbe(args[0]); for (let i = 1; i < args.length; i++) { - r = new ProbeImpl(this, f(this.ptr, r.ptr, this._toProbe(args[i]).ptr)); + r = new ProbeImpl(check(f(contextPtr, r.ptr, _toProbe(args[i]).ptr))); } return r; } - } - class AstImpl implements Ast { - declare readonly __typename: Ast['__typename']; - - constructor(readonly ctx: ContextImpl, readonly ptr: Ptr) { - const myAst = this.ast; - - Z3.inc_ref(ctx.ptr, myAst); - cleanup.register(this, () => Z3.dec_ref(ctx.ptr, myAst)); + /////////////// + // Functions // + /////////////// + function interrupt(): void { + check(Z3.interrupt(contextPtr)); } - get ast(): Z3_ast { - return this.ptr as any as Z3_ast; + function isModel(obj: unknown): obj is Model { + const r = obj instanceof ModelImpl; + r && _assertContext(obj); + return r; } - get id() { - return Z3.get_ast_id(this.ctx.ptr, this.ast); + function isAst(obj: unknown): obj is Ast { + const r = obj instanceof AstImpl; + r && _assertContext(obj); + return r; } - eqIdentity(other: Ast) { - this.ctx._assertContext(other); - return Z3.is_eq_ast(this.ctx.ptr, this.ast, other.ast); + function isSort(obj: unknown): obj is Sort { + const r = obj instanceof SortImpl; + r && _assertContext(obj); + return r; } - neqIdentity(other: Ast) { - this.ctx._assertContext(other); - return !this.eqIdentity(other); + function isFuncDecl(obj: unknown): obj is FuncDecl { + const r = obj instanceof FuncDeclImpl; + r && _assertContext(obj); + return r; } - sexpr() { - return Z3.ast_to_string(this.ctx.ptr, this.ast); - } - - hash() { - return Z3.get_ast_hash(this.ctx.ptr, this.ast); - } - } - - class SolverImpl implements Solver { - declare readonly __typename: Solver['__typename']; - - readonly ptr: Z3_solver; - - constructor(readonly ctx: ContextImpl, ptr: Z3_solver | string = Z3.mk_solver(ctx.ptr)) { - let myPtr: Z3_solver; - if (typeof ptr === 'string') { - myPtr = Z3.mk_solver_for_logic(ctx.ptr, ctx._toSymbol(ptr)); - } else { - myPtr = ptr; + function isApp(obj: unknown): boolean { + if (!isExpr(obj)) { + return false; } - this.ptr = myPtr; - Z3.solver_inc_ref(ctx.ptr, myPtr); - cleanup.register(this, () => Z3.solver_dec_ref(ctx.ptr, myPtr)); + const kind = check(Z3.get_ast_kind(contextPtr, obj.ast)); + return kind === Z3_ast_kind.Z3_NUMERAL_AST || kind === Z3_ast_kind.Z3_APP_AST; } - push() { - Z3.solver_push(this.ctx.ptr, this.ptr); + function isConst(obj: unknown): boolean { + return isExpr(obj) && isApp(obj) && obj.numArgs() === 0; } - pop(num: number = 1) { - Z3.solver_pop(this.ctx.ptr, this.ptr, num); + + function isExpr(obj: unknown): obj is Expr { + const r = obj instanceof ExprImpl; + r && _assertContext(obj); + return r; } - numScopes() { - return Z3.solver_get_num_scopes(this.ctx.ptr, this.ptr); + + function isVar(obj: unknown): boolean { + return isExpr(obj) && check(Z3.get_ast_kind(contextPtr, obj.ast)) === Z3_ast_kind.Z3_VAR_AST; } - reset() { - Z3.solver_reset(this.ctx.ptr, this.ptr); + + function isAppOf(obj: unknown, kind: Z3_decl_kind): boolean { + return isExpr(obj) && isApp(obj) && obj.decl().kind() === kind; } - add(...exprs: (Bool | AstVector)[]) { - this.ctx._flattenArgs(exprs).forEach(expr => { - this.ctx._assertContext(expr); - Z3.solver_assert(this.ctx.ptr, this.ptr, expr.ast); - }); + + function isBool(obj: unknown): obj is Bool { + const r = obj instanceof BoolImpl; + r && _assertContext(obj); + return r; } - addAndTrack(expr: Bool, constant: Bool | string) { - if (typeof constant === 'string') { - constant = this.ctx.Bool.const(constant); + + function isTrue(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_TRUE); + } + + function isFalse(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_FALSE); + } + + function isAnd(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_AND); + } + + function isOr(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_OR); + } + + function isImplies(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_IMPLIES); + } + + function isNot(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_NOT); + } + + function isEq(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_EQ); + } + + function isDistinct(obj: unknown): boolean { + return isAppOf(obj, Z3_decl_kind.Z3_OP_DISTINCT); + } + + function isArith(obj: unknown): obj is Arith { + const r = obj instanceof ArithImpl; + r && _assertContext(obj); + return r; + } + + function isArithSort(obj: unknown): obj is ArithSort { + const r = obj instanceof ArithSortImpl; + r && _assertContext(obj); + return r; + } + + function isInt(obj: unknown): boolean { + return isArith(obj) && isIntSort(obj.sort); + } + + function isIntVal(obj: unknown): obj is IntNum { + const r = obj instanceof IntNumImpl; + r && _assertContext(obj); + return r; + } + + function isIntSort(obj: unknown): boolean { + return isSort(obj) && obj.kind() === Z3_sort_kind.Z3_INT_SORT; + } + + function isReal(obj: unknown): boolean { + return isArith(obj) && isRealSort(obj.sort); + } + + function isRealVal(obj: unknown): obj is RatNum { + const r = obj instanceof RatNumImpl; + r && _assertContext(obj); + return r; + } + + function isRealSort(obj: unknown): boolean { + return isSort(obj) && obj.kind() === Z3_sort_kind.Z3_REAL_SORT; + } + + function isBitVecSort(obj: unknown): obj is BitVecSort { + const r = obj instanceof BitVecSortImpl; + r && _assertContext(obj); + return r; + } + + function isBitVec(obj: unknown): obj is BitVec { + const r = obj instanceof BitVecImpl; + r && _assertContext(obj); + return r; + } + + function isBitVecVal(obj: unknown): obj is BitVecNum { + const r = obj instanceof BitVecNumImpl; + r && _assertContext(obj); + return r; + } + + function isProbe(obj: unknown): obj is Probe { + const r = obj instanceof ProbeImpl; + r && _assertContext(obj); + return r; + } + + function isTactic(obj: unknown): obj is Tactic { + const r = obj instanceof TacticImpl; + r && _assertContext(obj); + return r; + } + + function isAstVector(obj: unknown): obj is AstVector { + const r = obj instanceof AstVectorImpl; + r && _assertContext(obj); + return r; + } + + function eqIdentity(a: Ast, b: Ast): boolean { + return a.eqIdentity(b); + } + + function getVarIndex(obj: Expr): number { + assert(isVar(obj), 'Z3 bound variable expected'); + return Z3.get_index_value(contextPtr, obj.ast); + } + + function from(primitive: boolean): Bool; + function from(primitive: number | CoercibleRational): RatNum; + function from(primitive: bigint): IntNum; + function from>(expr: T): T; + function from(expr: CoercibleToExpr): AnyExpr; + function from(value: CoercibleToExpr): AnyExpr { + if (typeof value === 'boolean') { + return Bool.val(value); + } else if (typeof value === 'number') { + if (!Number.isFinite(value)) { + throw new Error(`cannot represent infinity/NaN (got ${value})`); + } + if (Math.floor(value) === value) { + return Int.val(value); + } + return Real.val(value); + } else if (isCoercibleRational(value)) { + return Real.val(value); + } else if (typeof value === 'bigint') { + return Int.val(value); + } else if (isExpr(value)) { + return value; } - assert(this.ctx.isConst(constant), 'Provided expression that is not a constant to addAndTrack'); - Z3.solver_assert_and_track(this.ctx.ptr, this.ptr, expr.ast, constant.ast); + assert(false); } - assertions(): AstVector { - return new AstVectorImpl(this.ctx, Z3.solver_get_assertions(this.ctx.ptr, this.ptr)); + async function solve(...assertions: Bool[]): Promise | 'unsat' | 'unknown'> { + const solver = new ctx.Solver(); + solver.add(...assertions); + const result = await solver.check(); + if (result === 'sat') { + return solver.model(); + } + return result; } - async check(...exprs: (Bool | AstVector)[]): Promise { - const assumptions = this.ctx._flattenArgs(exprs).map(expr => { - this.ctx._assertContext(expr); - return expr.ast; - }); - const result = await asyncMutex.runExclusive(() => - Z3.solver_check_assumptions(this.ctx.ptr, this.ptr, assumptions), + ///////////// + // Objects // + ///////////// + const Sort = { + declare: (name: string) => new SortImpl(Z3.mk_uninterpreted_sort(contextPtr, _toSymbol(name))), + }; + const Function = { + declare: (name: string, ...signature: FuncDeclSignature) => { + const arity = signature.length - 1; + const rng = signature[arity]; + _assertContext(rng); + const dom = []; + for (let i = 0; i < arity; i++) { + _assertContext(signature[i]); + dom.push(signature[i].ptr); + } + return new FuncDeclImpl(Z3.mk_func_decl(contextPtr, _toSymbol(name), dom, rng.ptr)); + }, + fresh: (...signature: FuncDeclSignature) => { + const arity = signature.length - 1; + const rng = signature[arity]; + _assertContext(rng); + const dom = []; + for (let i = 0; i < arity; i++) { + _assertContext(signature[i]); + dom.push(signature[i].ptr); + } + return new FuncDeclImpl(Z3.mk_fresh_func_decl(contextPtr, 'f', dom, rng.ptr)); + }, + }; + const RecFunc = { + declare: (name: string, ...signature: FuncDeclSignature) => { + const arity = signature.length - 1; + const rng = signature[arity]; + _assertContext(rng); + const dom = []; + for (let i = 0; i < arity; i++) { + _assertContext(signature[i]); + dom.push(signature[i].ptr); + } + return new FuncDeclImpl(Z3.mk_rec_func_decl(contextPtr, _toSymbol(name), dom, rng.ptr)); + }, + + addDefinition: (f: FuncDecl, args: Expr[], body: Expr) => { + _assertContext(f, ...args, body); + check( + Z3.add_rec_def( + contextPtr, + f.ptr, + args.map(arg => arg.ast), + body.ast, + ), + ); + }, + }; + const Bool = { + sort: () => new BoolSortImpl(Z3.mk_bool_sort(contextPtr)), + + const: (name: string) => new BoolImpl(Z3.mk_const(contextPtr, _toSymbol(name), Bool.sort().ptr)), + consts: (names: string | string[]) => { + if (typeof names === 'string') { + names = names.split(' '); + } + return names.map(name => Bool.const(name)); + }, + vector: (prefix: string, count: number) => { + const result = []; + for (let i = 0; i < count; i++) { + result.push(Bool.const(`${prefix}__${i}`)); + } + return result; + }, + fresh: (prefix = 'b') => new BoolImpl(Z3.mk_fresh_const(contextPtr, prefix, Bool.sort().ptr)), + + val: (value: boolean) => { + if (value) { + return new BoolImpl(Z3.mk_true(contextPtr)); + } + return new BoolImpl(Z3.mk_false(contextPtr)); + }, + }; + const Int = { + sort: () => new ArithSortImpl(Z3.mk_int_sort(contextPtr)), + + const: (name: string) => new ArithImpl(Z3.mk_const(contextPtr, _toSymbol(name), Int.sort().ptr)), + consts: (names: string | string[]) => { + if (typeof names === 'string') { + names = names.split(' '); + } + return names.map(name => Int.const(name)); + }, + vector: (prefix: string, count: number) => { + const result = []; + for (let i = 0; i < count; i++) { + result.push(Int.const(`${prefix}__${i}`)); + } + return result; + }, + fresh: (prefix = 'x') => new ArithImpl(Z3.mk_fresh_const(contextPtr, prefix, Int.sort().ptr)), + + val: (value: number | bigint | string) => { + assert(typeof value === 'bigint' || typeof value === 'string' || Number.isSafeInteger(value)); + return new IntNumImpl(check(Z3.mk_numeral(contextPtr, value.toString(), Int.sort().ptr))); + }, + }; + const Real = { + sort: () => new ArithSortImpl(Z3.mk_real_sort(contextPtr)), + + const: (name: string) => new ArithImpl(check(Z3.mk_const(contextPtr, _toSymbol(name), Real.sort().ptr))), + consts: (names: string | string[]) => { + if (typeof names === 'string') { + names = names.split(' '); + } + return names.map(name => Real.const(name)); + }, + vector: (prefix: string, count: number) => { + const result = []; + for (let i = 0; i < count; i++) { + result.push(Real.const(`${prefix}__${i}`)); + } + return result; + }, + fresh: (prefix = 'b') => new ArithImpl(Z3.mk_fresh_const(contextPtr, prefix, Real.sort().ptr)), + + val: (value: number | bigint | string | CoercibleRational) => { + if (isCoercibleRational(value)) { + value = `${value.numerator}/${value.denominator}`; + } + return new RatNumImpl(Z3.mk_numeral(contextPtr, value.toString(), Real.sort().ptr)); + }, + }; + const BitVec = { + sort(bits: Bits): BitVecSort { + assert(Number.isSafeInteger(bits), 'number of bits must be an integer'); + return new BitVecSortImpl(Z3.mk_bv_sort(contextPtr, bits)); + }, + + const(name: string, bits: Bits | BitVecSort): BitVec { + return new BitVecImpl( + check(Z3.mk_const(contextPtr, _toSymbol(name), isBitVecSort(bits) ? bits.ptr : BitVec.sort(bits).ptr)), + ); + }, + + consts(names: string | string[], bits: Bits | BitVecSort): BitVec[] { + if (typeof names === 'string') { + names = names.split(' '); + } + return names.map(name => BitVec.const(name, bits)); + }, + + val( + value: bigint | number | boolean, + bits: Bits | BitVecSort, + ): BitVecNum { + if (value === true) { + return BitVec.val(1, bits); + } else if (value === false) { + return BitVec.val(0, bits); + } + return new BitVecNumImpl( + check(Z3.mk_numeral(contextPtr, value.toString(), isBitVecSort(bits) ? bits.ptr : BitVec.sort(bits).ptr)), + ); + }, + }; + + //////////////// + // Operations // + //////////////// + function If(condition: Probe, onTrue: Tactic, onFalse: Tactic): Tactic; + function If, OnFalseRef extends CoercibleToExpr>( + condition: Bool | boolean, + onTrue: OnTrueRef, + onFalse: OnFalseRef, + ): CoercibleToExprMap; + function If( + condition: Bool | Probe | boolean, + onTrue: CoercibleToExpr | Tactic, + onFalse: CoercibleToExpr | Tactic, + ): Expr | Tactic { + if (isProbe(condition) && isTactic(onTrue) && isTactic(onFalse)) { + return Cond(condition, onTrue, onFalse); + } + assert(!isProbe(condition) && !isTactic(onTrue) && !isTactic(onFalse), 'Mixed expressions and goals'); + if (typeof condition === 'boolean') { + condition = Bool.val(condition); + } + onTrue = from(onTrue); + onFalse = from(onFalse); + return _toExpr(check(Z3.mk_ite(contextPtr, condition.ptr, onTrue.ast, onFalse.ast))); + } + + function Distinct(...exprs: CoercibleToExpr[]): Bool { + assert(exprs.length > 0, "Can't make Distinct ouf of nothing"); + + return new BoolImpl( + check( + Z3.mk_distinct( + contextPtr, + exprs.map(expr => { + expr = from(expr); + _assertContext(expr); + return expr.ast; + }), + ), + ), ); - switch (result) { - case Z3_lbool.Z3_L_FALSE: - return unsat; - case Z3_lbool.Z3_L_TRUE: - return sat; - case Z3_lbool.Z3_L_UNDEF: - return unknown; - default: - assertExhaustive(result); + } + + function Const>(name: string, sort: S): SortToExprMap { + _assertContext(sort); + return _toExpr(check(Z3.mk_const(contextPtr, _toSymbol(name), sort.ptr))) as SortToExprMap; + } + + function Consts>(names: string | string[], sort: S): SortToExprMap[] { + _assertContext(sort); + if (typeof names === 'string') { + names = names.split(' '); + } + return names.map(name => Const(name, sort)); + } + + function FreshConst>(sort: S, prefix: string = 'c'): SortToExprMap { + _assertContext(sort); + return _toExpr(Z3.mk_fresh_const(sort.ctx.ptr, prefix, sort.ptr)) as SortToExprMap; + } + + function Var>(idx: number, sort: S): SortToExprMap { + _assertContext(sort); + return _toExpr(Z3.mk_bound(sort.ctx.ptr, idx, sort.ptr)) as SortToExprMap; + } + + function Implies(a: Bool | boolean, b: Bool | boolean): Bool { + a = from(a) as Bool; + b = from(b) as Bool; + _assertContext(a, b); + return new BoolImpl(check(Z3.mk_implies(contextPtr, a.ptr, b.ptr))); + } + + function Eq(a: CoercibleToExpr, b: CoercibleToExpr): Bool { + a = from(a); + b = from(b); + _assertContext(a, b); + return a.eq(b); + } + + function Xor(a: Bool | boolean, b: Bool | boolean): Bool { + a = from(a) as Bool; + b = from(b) as Bool; + _assertContext(a, b); + return new BoolImpl(check(Z3.mk_xor(contextPtr, a.ptr, b.ptr))); + } + + function Not(a: Probe): Probe; + function Not(a: Bool | boolean): Bool; + function Not(a: Bool | boolean | Probe): Bool | Probe { + if (typeof a === 'boolean') { + a = from(a); + } + _assertContext(a); + if (isProbe(a)) { + return new ProbeImpl(check(Z3.probe_not(contextPtr, a.ptr))); + } + return new BoolImpl(check(Z3.mk_not(contextPtr, a.ptr))); + } + + function And(): Bool; + function And(vector: AstVector>): Bool; + function And(...args: (Bool | boolean)[]): Bool; + function And(...args: Probe[]): Probe; + function And( + ...args: (AstVector> | Probe | Bool | boolean)[] + ): Bool | Probe { + if (args.length == 1 && args[0] instanceof ctx.AstVector) { + args = [...args[0].values()]; + assert(allSatisfy(args, isBool) ?? true, 'AstVector containing not bools'); + } + + const allProbes = allSatisfy(args, isProbe) ?? false; + if (allProbes) { + return _probeNary(Z3.probe_and, args as [Probe, ...Probe[]]); + } else { + const castArgs = args.map(from) as Bool[]; + _assertContext(...castArgs); + return new BoolImpl( + check( + Z3.mk_and( + contextPtr, + castArgs.map(arg => arg.ptr), + ), + ), + ); } } - model() { - return new this.ctx.Model(Z3.solver_get_model(this.ctx.ptr, this.ptr)); - } - } + function Or(): Bool; + function Or(vector: AstVector>): Bool; + function Or(...args: (Bool | boolean)[]): Bool; + function Or(...args: Probe[]): Probe; + function Or( + ...args: (AstVector> | Probe | Bool | boolean)[] + ): Bool | Probe { + if (args.length == 1 && args[0] instanceof ctx.AstVector) { + args = [...args[0].values()]; + assert(allSatisfy(args, isBool) ?? true, 'AstVector containing not bools'); + } - class ModelImpl implements Model { - declare readonly __typename: Model['__typename']; - - constructor(readonly ctx: ContextImpl, readonly ptr: Z3_model = Z3.mk_model(ctx.ptr)) { - Z3.model_inc_ref(ctx.ptr, ptr); - cleanup.register(this, () => Z3.model_dec_ref(ctx.ptr, ptr)); - } - - get length() { - return Z3.model_get_num_consts(this.ctx.ptr, this.ptr) + Z3.model_get_num_funcs(this.ctx.ptr, this.ptr); - } - - [Symbol.iterator](): Iterator { - return this.values(); - } - - *entries(): IterableIterator<[number, FuncDecl]> { - const length = this.length; - for (let i = 0; i < length; i++) { - yield [i, this.get(i)]; + const allProbes = allSatisfy(args, isProbe) ?? false; + if (allProbes) { + return _probeNary(Z3.probe_or, args as [Probe, ...Probe[]]); + } else { + const castArgs = args.map(from) as Bool[]; + _assertContext(...castArgs); + return new BoolImpl( + check( + Z3.mk_or( + contextPtr, + castArgs.map(arg => arg.ptr), + ), + ), + ); } } - *keys(): IterableIterator { - for (const [key] of this.entries()) { - yield key; + function ToReal(expr: Arith | bigint): Arith { + expr = from(expr) as Arith; + _assertContext(expr); + assert(isInt(expr), 'Int expression expected'); + return new ArithImpl(check(Z3.mk_int2real(contextPtr, expr.ast))); + } + + function ToInt(expr: Arith | number | CoercibleRational | string): Arith { + if (!isExpr(expr)) { + expr = Real.val(expr); + } + _assertContext(expr); + assert(isReal(expr), 'Real expression expected'); + return new ArithImpl(check(Z3.mk_real2int(contextPtr, expr.ast))); + } + + function IsInt(expr: Arith | number | CoercibleRational | string): Bool { + if (!isExpr(expr)) { + expr = Real.val(expr); + } + _assertContext(expr); + assert(isReal(expr), 'Real expression expected'); + return new BoolImpl(check(Z3.mk_is_int(contextPtr, expr.ast))); + } + + function Sqrt(a: Arith | number | bigint | string | CoercibleRational): Arith { + if (!isExpr(a)) { + a = Real.val(a); + } + return a.pow('1/2'); + } + + function Cbrt(a: Arith | number | bigint | string | CoercibleRational): Arith { + if (!isExpr(a)) { + a = Real.val(a); + } + return a.pow('1/3'); + } + + function BV2Int(a: BitVec, isSigned: boolean): Arith { + _assertContext(a); + return new ArithImpl(check(Z3.mk_bv2int(contextPtr, a.ast, isSigned))); + } + + function Int2BV(a: Arith | bigint | number, bits: Bits): BitVec { + if (isArith(a)) { + assert(isInt(a), 'parameter must be an integer'); + } else { + assert(typeof a !== 'number' || Number.isSafeInteger(a), 'parameter must not have decimal places'); + a = Int.val(a); + } + return new BitVecImpl(check(Z3.mk_int2bv(contextPtr, bits, a.ast))); + } + + function Concat(...bitvecs: BitVec[]): BitVec { + _assertContext(...bitvecs); + return bitvecs.reduce((prev, curr) => new BitVecImpl(check(Z3.mk_concat(contextPtr, prev.ast, curr.ast)))); + } + + function Cond(probe: Probe, onTrue: Tactic, onFalse: Tactic): Tactic { + _assertContext(probe, onTrue, onFalse); + return new TacticImpl(check(Z3.tactic_cond(contextPtr, probe.ptr, onTrue.ptr, onFalse.ptr))); + } + + class AstImpl implements Ast { + declare readonly __typename: Ast['__typename']; + readonly ctx: Context; + + constructor(readonly ptr: Ptr) { + this.ctx = ctx; + const myAst = this.ast; + + Z3.inc_ref(contextPtr, myAst); + cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst)); + } + + get ast(): Z3_ast { + return this.ptr; + } + + id() { + return Z3.get_ast_id(contextPtr, this.ast); + } + + eqIdentity(other: Ast) { + _assertContext(other); + return check(Z3.is_eq_ast(contextPtr, this.ast, other.ast)); + } + + neqIdentity(other: Ast) { + _assertContext(other); + return !this.eqIdentity(other); + } + + sexpr() { + return Z3.ast_to_string(contextPtr, this.ast); + } + + hash() { + return Z3.get_ast_hash(contextPtr, this.ast); + } + + toString() { + return this.sexpr(); } } - *values(): IterableIterator { - for (const [, value] of this.entries()) { - yield value; + class SolverImpl implements Solver { + declare readonly __typename: Solver['__typename']; + + readonly ptr: Z3_solver; + readonly ctx: Context; + constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) { + this.ctx = ctx; + let myPtr: Z3_solver; + if (typeof ptr === 'string') { + myPtr = check(Z3.mk_solver_for_logic(contextPtr, _toSymbol(ptr))); + } else { + myPtr = ptr; + } + this.ptr = myPtr; + Z3.solver_inc_ref(contextPtr, myPtr); + cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr)); + } + + 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 | AstVector>)[]) { + _flattenArgs(exprs).forEach(expr => { + _assertContext(expr); + check(Z3.solver_assert(contextPtr, this.ptr, expr.ast)); + }); + } + addAndTrack(expr: Bool, constant: Bool | string) { + if (typeof constant === 'string') { + constant = Bool.const(constant); + } + assert(isConst(constant), 'Provided expression that is not a constant to addAndTrack'); + check(Z3.solver_assert_and_track(contextPtr, this.ptr, expr.ast, constant.ast)); + } + + assertions(): AstVector> { + return new AstVectorImpl(check(Z3.solver_get_assertions(contextPtr, this.ptr))); + } + + async check(...exprs: (Bool | AstVector>)[]): Promise { + const assumptions = _flattenArgs(exprs).map(expr => { + _assertContext(expr); + return expr.ast; + }); + const result = await asyncMutex.runExclusive(() => + check(Z3.solver_check_assumptions(contextPtr, this.ptr, assumptions)), + ); + switch (result) { + case Z3_lbool.Z3_L_FALSE: + return 'unsat'; + case Z3_lbool.Z3_L_TRUE: + return 'sat'; + case Z3_lbool.Z3_L_UNDEF: + return 'unknown'; + default: + assertExhaustive(result); + } + } + + model() { + return new ModelImpl(check(Z3.solver_get_model(contextPtr, this.ptr))); + } + + toString() { + return check(Z3.solver_to_string(contextPtr, this.ptr)); } } - decls() { - return [...this.values()]; - } + class ModelImpl implements Model { + declare readonly __typename: Model['__typename']; + readonly ctx: Context; - sexpr() { - return Z3.model_to_string(this.ctx.ptr, this.ptr); - } - - eval(expr: Bool, modelCompletion?: boolean): Bool; - eval(expr: Arith, modelCompletion?: boolean): Arith; - eval(expr: Expr, modelCompletion: boolean = false) { - this.ctx._assertContext(expr); - const r = Z3.model_eval(this.ctx.ptr, this.ptr, expr.ast, modelCompletion); - if (r === null) { - throw new Z3Error('Failed to evaluatio expression in the model'); + constructor(readonly ptr: Z3_model = Z3.mk_model(contextPtr)) { + this.ctx = ctx; + Z3.model_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr)); + } + + length() { + return Z3.model_get_num_consts(contextPtr, this.ptr) + Z3.model_get_num_funcs(contextPtr, this.ptr); + } + + [Symbol.iterator](): Iterator> { + return this.values(); + } + + *entries(): IterableIterator<[number, FuncDecl]> { + const length = this.length(); + for (let i = 0; i < length; i++) { + yield [i, this.get(i)]; + } + } + + *keys(): IterableIterator { + for (const [key] of this.entries()) { + yield key; + } + } + + *values(): IterableIterator> { + for (const [, value] of this.entries()) { + yield value; + } + } + + decls() { + return [...this.values()]; + } + + sexpr() { + return check(Z3.model_to_string(contextPtr, this.ptr)); + } + + eval(expr: Bool, modelCompletion?: boolean): Bool; + eval(expr: Arith, modelCompletion?: boolean): Arith; + eval(expr: Expr, 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'); + } + return _toExpr(r); + } + + get(i: number): FuncDecl; + get(from: number, to: number): FuncDecl[]; + get(declaration: FuncDecl): FuncInterp | Expr; + get(constant: Expr): Expr; + get(sort: Sort): AstVector>; + get( + i: number | FuncDecl | Expr | Sort, + to?: number, + ): FuncDecl | FuncInterp | Expr | AstVector> | FuncDecl[] { + assert(to === undefined || typeof i === 'number'); + if (typeof i === 'number') { + const length = this.length(); + + if (i >= length) { + throw new RangeError(`expected index ${i} to be less than length ${length}`); + } + + if (to === undefined) { + const numConsts = check(Z3.model_get_num_consts(contextPtr, this.ptr)); + if (i < numConsts) { + return new FuncDeclImpl(check(Z3.model_get_const_decl(contextPtr, this.ptr, i))); + } else { + return new FuncDeclImpl(check(Z3.model_get_func_decl(contextPtr, this.ptr, i - numConsts))); + } + } + + if (to < 0) { + to += length; + } + if (to >= length) { + throw new RangeError(`expected index ${to} to be less than length ${length}`); + } + const result = []; + for (let j = i; j < to; j++) { + result.push(this.get(j)); + } + return result; + } else if (isFuncDecl(i) || (isExpr(i) && isConst(i))) { + const result = this.getInterp(i); + assert(result !== null); + return result; + } else if (isSort(i)) { + return this.getUniverse(i); + } + assert(false, 'Number, declaration or constant expected'); + } + + private getInterp(expr: FuncDecl | Expr): Expr | FuncInterp | null { + assert(isFuncDecl(expr) || isConst(expr), 'Declaration expected'); + if (isConst(expr)) { + assert(isExpr(expr)); + expr = expr.decl(); + } + assert(isFuncDecl(expr)); + if (expr.arity() === 0) { + const result = check(Z3.model_get_const_interp(contextPtr, this.ptr, expr.ptr)); + if (result === null) { + return null; + } + return _toExpr(result); + } else { + const interp = check(Z3.model_get_func_interp(contextPtr, this.ptr, expr.ptr)); + if (interp === null) { + return null; + } + return new FuncInterpImpl(interp); + } + } + + private getUniverse(sort: Sort): AstVector> { + _assertContext(sort); + return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr))); } - return this.ctx._toExpr(r); } - get(i: number): FuncDecl; - get(from: number, to: number): FuncDecl[]; - get(declaration: FuncDecl): FuncInterp | Expr; - get(constant: Expr): Expr; - get(sort: Sort): AstVector; - get( - i: number | FuncDecl | Expr | Sort, - to?: number, - ): FuncDecl | FuncInterp | Expr | AstVector | FuncDecl[] { - assert(to === undefined || typeof i === 'number'); - if (typeof i === 'number') { - const length = this.length; + class FuncInterpImpl implements FuncInterp { + declare readonly __typename: FuncInterp['__typename']; + readonly ctx: Context; - if (i >= length) { - throw new RangeError(); + constructor(readonly ptr: Z3_func_interp) { + this.ctx = ctx; + Z3.func_interp_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr)); + } + } + + class SortImpl extends AstImpl implements Sort { + declare readonly __typename: Sort['__typename']; + + get ast(): Z3_ast { + return Z3.sort_to_ast(contextPtr, this.ptr); + } + + kind() { + return Z3.get_sort_kind(contextPtr, this.ptr); + } + + subsort(other: Sort) { + _assertContext(other); + return false; + } + + cast(expr: Expr): Expr { + _assertContext(expr); + assert(expr.sort.eqIdentity(expr.sort), 'Sort mismatch'); + return expr; + } + + name() { + return _fromSymbol(Z3.get_sort_name(contextPtr, this.ptr)); + } + + eqIdentity(other: Sort) { + _assertContext(other); + return check(Z3.is_eq_sort(contextPtr, this.ptr, other.ptr)); + } + + neqIdentity(other: Sort) { + return !this.eqIdentity(other); + } + } + + class FuncDeclImpl extends AstImpl implements FuncDecl { + declare readonly __typename: FuncDecl['__typename']; + + get ast() { + return Z3.func_decl_to_ast(contextPtr, this.ptr); + } + + name() { + return _fromSymbol(Z3.get_decl_name(contextPtr, this.ptr)); + } + + arity() { + return Z3.get_arity(contextPtr, this.ptr); + } + + domain(i: number) { + assert(i < this.arity(), 'Index out of bounds'); + return _toSort(Z3.get_domain(contextPtr, this.ptr, i)); + } + + range() { + return _toSort(Z3.get_range(contextPtr, this.ptr)); + } + + kind() { + return Z3.get_decl_kind(contextPtr, this.ptr); + } + + params(): (number | string | Z3_symbol | Sort | Expr | FuncDecl)[] { + const n = Z3.get_decl_num_parameters(contextPtr, this.ptr); + const result = []; + for (let i = 0; i < n; i++) { + const kind = check(Z3.get_decl_parameter_kind(contextPtr, this.ptr, i)); + switch (kind) { + case Z3_parameter_kind.Z3_PARAMETER_INT: + result.push(check(Z3.get_decl_int_parameter(contextPtr, this.ptr, i))); + break; + case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: + result.push(check(Z3.get_decl_double_parameter(contextPtr, this.ptr, i))); + break; + case Z3_parameter_kind.Z3_PARAMETER_RATIONAL: + result.push(check(Z3.get_decl_rational_parameter(contextPtr, this.ptr, i))); + break; + case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: + result.push(check(Z3.get_decl_symbol_parameter(contextPtr, this.ptr, i))); + break; + case Z3_parameter_kind.Z3_PARAMETER_SORT: + result.push(new SortImpl(check(Z3.get_decl_sort_parameter(contextPtr, this.ptr, i)))); + break; + case Z3_parameter_kind.Z3_PARAMETER_AST: + result.push(new ExprImpl(check(Z3.get_decl_ast_parameter(contextPtr, this.ptr, i)))); + break; + case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: + result.push(new FuncDeclImpl(check(Z3.get_decl_func_decl_parameter(contextPtr, this.ptr, i)))); + break; + default: + assertExhaustive(kind); + } + } + return result; + } + + call(...args: CoercibleToExpr[]) { + assert(args.length === this.arity(), `Incorrect number of arguments to ${this}`); + return _toExpr( + check(Z3.mk_app( + contextPtr, + this.ptr, + args.map((arg, i) => { + return this.domain(i).cast(arg).ast; + }), + )), + ); + } + } + + class ExprImpl = AnySort> extends AstImpl implements Expr { + declare readonly __typename: Expr['__typename']; + + get sort(): S { + return _toSort(Z3.get_sort(contextPtr, this.ast)) as S; + } + + eq(other: CoercibleToExpr): Bool { + return new BoolImpl(check(Z3.mk_eq(contextPtr, this.ast, from(other).ast))); + } + + neq(other: CoercibleToExpr): Bool { + return new BoolImpl( + check(Z3.mk_distinct( + contextPtr, + [this, other].map(expr => from(expr).ast), + )), + ); + } + + params() { + return this.decl().params(); + } + + decl(): FuncDecl { + assert(isApp(this), 'Z3 application expected'); + return new FuncDeclImpl(check(Z3.get_app_decl(contextPtr, check(Z3.to_app(contextPtr, this.ast))))); + } + + numArgs(): number { + assert(isApp(this), 'Z3 applicaiton expected'); + return check(Z3.get_app_num_args(contextPtr, check(Z3.to_app(contextPtr, this.ast)))); + } + + arg(i: number): ReturnType { + assert(isApp(this), 'Z3 applicaiton expected'); + assert(i < this.numArgs(), `Invalid argument index - expected ${i} to be less than ${this.numArgs()}`); + return _toExpr(check(Z3.get_app_arg(contextPtr, check(Z3.to_app(contextPtr, this.ast)), i))); + } + + children(): ReturnType[] { + const num_args = this.numArgs(); + if (isApp(this)) { + const result = []; + for (let i = 0; i < num_args; i++) { + result.push(this.arg(i)); + } + return result; + } + return []; + } + } + + class BoolSortImpl extends SortImpl implements BoolSort { + declare readonly __typename: BoolSort['__typename']; + + cast(other: Bool | boolean): Bool; + cast(other: CoercibleToExpr): never; + cast(other: CoercibleToExpr | Bool) { + if (typeof other === 'boolean') { + other = Bool.val(other); + } + assert(isExpr(other), 'true, false or Z3 Boolean expression expected.'); + assert(this.eqIdentity(other.sort), 'Value cannot be converted into a Z3 Boolean value'); + return other; + } + + subsort(other: Sort) { + _assertContext(other.ctx); + return other instanceof ArithSortImpl; + } + } + + class BoolImpl extends ExprImpl> implements Bool { + declare readonly __typename: Bool['__typename']; + + not(): Bool { + return Not(this); + } + and(other: Bool | boolean): Bool { + return And(this, other); + } + or(other: Bool | boolean): Bool { + return Or(this, other); + } + xor(other: Bool | boolean): Bool { + return Xor(this, other); + } + } + + class ProbeImpl implements Probe { + declare readonly __typename: Probe['__typename']; + readonly ctx: Context; + + constructor(readonly ptr: Z3_probe) { + this.ctx = ctx; + } + } + + class TacticImpl implements Tactic { + declare readonly __typename: Tactic['__typename']; + + readonly ptr: Z3_tactic; + readonly ctx: Context; + + constructor(tactic: string | Z3_tactic) { + this.ctx = ctx; + let myPtr: Z3_tactic; + if (typeof tactic === 'string') { + myPtr = check(Z3.mk_tactic(contextPtr, tactic)); + } else { + myPtr = tactic; + } + + this.ptr = myPtr; + + Z3.tactic_inc_ref(contextPtr, myPtr); + cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr)); + } + } + + class ArithSortImpl extends SortImpl implements ArithSort { + declare readonly __typename: ArithSort['__typename']; + + cast(other: bigint | number): IntNum | RatNum; + cast(other: CoercibleRational | RatNum): RatNum; + cast(other: IntNum): IntNum; + cast(other: Bool | Arith): Arith; + cast(other: CoercibleToExpr): never; + cast(other: CoercibleToExpr): Arith | RatNum | IntNum { + const sortTypeStr = isIntSort(this) ? 'IntSort' : 'RealSort'; + if (isExpr(other)) { + const otherS = other.sort; + if (isArith(other)) { + if (this.eqIdentity(otherS)) { + return other; + } else if (isIntSort(otherS) && isRealSort(this)) { + return ToReal(other); + } + assert(false, "Can't cast Real to IntSort without loss"); + } else if (isBool(other)) { + if (isIntSort(this)) { + return If(other, 1, 0); + } else { + return ToReal(If(other, 1, 0)); + } + } + assert(false, `Can't cast expression to ${sortTypeStr}`); + } else { + if (typeof other !== 'boolean') { + if (isIntSort(this)) { + assert(!isCoercibleRational(other), "Can't cast fraction to IntSort"); + return Int.val(other); + } + return Real.val(other); + } + assert(false, `Can't cast primitive to ${sortTypeStr}`); + } + } + } + + class ArithImpl extends ExprImpl> implements Arith { + declare readonly __typename: Arith['__typename']; + + add(other: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_add(contextPtr, [this.ast, this.sort.cast(other).ast]))); + } + + mul(other: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_mul(contextPtr, [this.ast, this.sort.cast(other).ast]))); + } + + sub(other: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_sub(contextPtr, [this.ast, this.sort.cast(other).ast]))); + } + + pow(exponent: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_power(contextPtr, this.ast, this.sort.cast(exponent).ast))); + } + + div(other: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_div(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + mod(other: Arith | number | bigint | string | CoercibleRational) { + return new ArithImpl(check(Z3.mk_mod(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + neg() { + return new ArithImpl(check(Z3.mk_unary_minus(contextPtr, this.ast))); + } + + le(other: Arith | number | bigint | string | CoercibleRational) { + return new BoolImpl(check(Z3.mk_le(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + lt(other: Arith | number | bigint | string | CoercibleRational) { + return new BoolImpl(check(Z3.mk_lt(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + gt(other: Arith | number | bigint | string | CoercibleRational) { + return new BoolImpl(check(Z3.mk_gt(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + ge(other: Arith | number | bigint | string | CoercibleRational) { + return new BoolImpl(check(Z3.mk_ge(contextPtr, this.ast, this.sort.cast(other).ast))); + } + } + + class IntNumImpl extends ArithImpl implements IntNum { + declare readonly __typename: IntNum['__typename']; + + value() { + return BigInt(this.asString()); + } + + asString() { + return Z3.get_numeral_string(contextPtr, this.ast); + } + + asBinary() { + return Z3.get_numeral_binary_string(contextPtr, this.ast); + } + } + + class RatNumImpl extends ArithImpl implements RatNum { + declare readonly __typename: RatNum['__typename']; + + value() { + return { numerator: this.numerator().value(), denominator: this.denominator().value() }; + } + + numerator() { + return new IntNumImpl(Z3.get_numerator(contextPtr, this.ast)); + } + + denominator() { + return new IntNumImpl(Z3.get_denominator(contextPtr, this.ast)); + } + + asNumber() { + const { numerator, denominator } = this.value(); + const div = numerator / denominator; + return Number(div) + Number(numerator - div * denominator) / Number(denominator); + } + + asDecimal(prec: number = Number.parseInt(getParam('precision') ?? FALLBACK_PRECISION.toString())) { + return Z3.get_numeral_decimal_string(contextPtr, this.ast, prec); + } + + asString() { + return Z3.get_numeral_string(contextPtr, this.ast); + } + } + + class BitVecSortImpl extends SortImpl implements BitVecSort { + declare readonly __typename: BitVecSort['__typename']; + + size() { + return Z3.get_bv_sort_size(contextPtr, this.ptr) as Bits; + } + + subsort(other: Sort): boolean { + return isBitVecSort(other) && this.size() < other.size(); + } + + cast(other: CoercibleToBitVec): BitVec; + cast(other: CoercibleToExpr): Expr; + cast(other: CoercibleToExpr): Expr { + if (isExpr(other)) { + _assertContext(other); + return other; + } + assert(!isCoercibleRational(other), "Can't convert rational to BitVec"); + return BitVec.val(other, this.size()); + } + } + + class BitVecImpl extends ExprImpl> implements BitVec { + declare readonly __typename: BitVec['__typename']; + + size() { + return this.sort.size(); + } + + add(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvadd(contextPtr, this.ast, this.sort.cast(other).ast))); + } + mul(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvmul(contextPtr, this.ast, this.sort.cast(other).ast))); + } + sub(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvsub(contextPtr, this.ast, this.sort.cast(other).ast))); + } + sdiv(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvsdiv(contextPtr, this.ast, this.sort.cast(other).ast))); + } + udiv(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvudiv(contextPtr, this.ast, this.sort.cast(other).ast))); + } + smod(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvsmod(contextPtr, this.ast, this.sort.cast(other).ast))); + } + urem(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvurem(contextPtr, this.ast, this.sort.cast(other).ast))); + } + srem(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvsrem(contextPtr, this.ast, this.sort.cast(other).ast))); + } + neg(): BitVec { + return new BitVecImpl(check(Z3.mk_bvneg(contextPtr, this.ast))); + } + + or(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvor(contextPtr, this.ast, this.sort.cast(other).ast))); + } + and(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvand(contextPtr, this.ast, this.sort.cast(other).ast))); + } + nand(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvnand(contextPtr, this.ast, this.sort.cast(other).ast))); + } + xor(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvxor(contextPtr, this.ast, this.sort.cast(other).ast))); + } + xnor(other: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvxnor(contextPtr, this.ast, this.sort.cast(other).ast))); + } + shr(count: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvashr(contextPtr, this.ast, this.sort.cast(count).ast))); + } + lshr(count: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvlshr(contextPtr, this.ast, this.sort.cast(count).ast))); + } + shl(count: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_bvshl(contextPtr, this.ast, this.sort.cast(count).ast))); + } + rotateRight(count: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_ext_rotate_right(contextPtr, this.ast, this.sort.cast(count).ast))); + } + rotateLeft(count: CoercibleToBitVec): BitVec { + return new BitVecImpl(check(Z3.mk_ext_rotate_left(contextPtr, this.ast, this.sort.cast(count).ast))); + } + not(): BitVec { + return new BitVecImpl(check(Z3.mk_bvnot(contextPtr, this.ast))); + } + + extract(high: number, low: number): BitVec { + return new BitVecImpl(check(Z3.mk_extract(contextPtr, high, low, this.ast))); + } + signExt(count: number): BitVec { + return new BitVecImpl(check(Z3.mk_sign_ext(contextPtr, count, this.ast))); + } + zeroExt(count: number): BitVec { + return new BitVecImpl(check(Z3.mk_zero_ext(contextPtr, count, this.ast))); + } + repeat(count: number): BitVec { + return new BitVecImpl(check(Z3.mk_repeat(contextPtr, count, this.ast))); + } + + sle(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsle(contextPtr, this.ast, this.sort.cast(other).ast))); + } + ule(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvule(contextPtr, this.ast, this.sort.cast(other).ast))); + } + slt(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvslt(contextPtr, this.ast, this.sort.cast(other).ast))); + } + ult(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvult(contextPtr, this.ast, this.sort.cast(other).ast))); + } + sge(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsge(contextPtr, this.ast, this.sort.cast(other).ast))); + } + uge(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvuge(contextPtr, this.ast, this.sort.cast(other).ast))); + } + sgt(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsgt(contextPtr, this.ast, this.sort.cast(other).ast))); + } + ugt(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvugt(contextPtr, this.ast, this.sort.cast(other).ast))); + } + + redAnd(): BitVec { + return new BitVecImpl(check(Z3.mk_bvredand(contextPtr, this.ast))); + } + redOr(): BitVec { + return new BitVecImpl(check(Z3.mk_bvredor(contextPtr, this.ast))); + } + + addNoOverflow(other: CoercibleToBitVec, isSigned: boolean): Bool { + return new BoolImpl(check(Z3.mk_bvadd_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned))); + } + addNoUnderflow(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvadd_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast))); + } + subNoOverflow(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsub_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast))); + } + subNoUndeflow(other: CoercibleToBitVec, isSigned: boolean): Bool { + return new BoolImpl(check(Z3.mk_bvsub_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned))); + } + sdivNoOverflow(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsdiv_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast))); + } + mulNoOverflow(other: CoercibleToBitVec, isSigned: boolean): Bool { + return new BoolImpl(check(Z3.mk_bvmul_no_overflow(contextPtr, this.ast, this.sort.cast(other).ast, isSigned))); + } + mulNoUndeflow(other: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvmul_no_underflow(contextPtr, this.ast, this.sort.cast(other).ast))); + } + negNoOverflow(): Bool { + return new BoolImpl(check(Z3.mk_bvneg_no_overflow(contextPtr, this.ast))); + } + } + + class BitVecNumImpl extends BitVecImpl implements BitVecNum { + declare readonly __typename: BitVecNum['__typename']; + value() { + return BigInt(this.asString()); + } + + asSignedValue() { + let val = this.value(); + const size = BigInt(this.size()); + if (val >= 2n ** (size - 1n)) { + val = val - 2n ** size; + } + if (val < (-2n) ** (size - 1n)) { + val = val + 2n ** size; + } + return val; + } + asString() { + return Z3.get_numeral_string(contextPtr, this.ast); + } + asBinaryString() { + return Z3.get_numeral_binary_string(contextPtr, this.ast); + } + } + + class AstVectorImpl> { + declare readonly __typename: AstVector['__typename']; + readonly ctx: Context; + + constructor(readonly ptr: Z3_ast_vector = Z3.mk_ast_vector(contextPtr)) { + this.ctx = ctx; + Z3.ast_vector_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr)); + } + + length(): number { + return Z3.ast_vector_size(contextPtr, this.ptr); + } + + [Symbol.iterator](): IterableIterator { + return this.values(); + } + + *entries(): IterableIterator<[number, Item]> { + const length = this.length(); + for (let i = 0; i < length; i++) { + yield [i, this.get(i)]; + } + } + + *keys(): IterableIterator { + for (let [key] of this.entries()) { + yield key; + } + } + + *values(): IterableIterator { + for (let [, value] of this.entries()) { + yield value; + } + } + + get(i: number): Item; + get(from: number, to: number): Item[]; + get(from: number, to?: number): Item | Item[] { + const length = this.length(); + if (from < 0) { + from += length; + } + if (from >= length) { + throw new RangeError(`expected from index ${from} to be less than length ${length}`); } if (to === undefined) { - const numConsts = Z3.model_get_num_consts(this.ctx.ptr, this.ptr); - if (i < numConsts) { - return new FuncDeclImpl(this.ctx, Z3.model_get_const_decl(this.ctx.ptr, this.ptr, i)); - } else { - return new FuncDeclImpl(this.ctx, Z3.model_get_func_decl(this.ctx.ptr, this.ptr, i - numConsts)); - } + return _toAst(check(Z3.ast_vector_get(contextPtr, this.ptr, from))) as Item; } if (to < 0) { to += length; } if (to >= length) { - throw new RangeError(); + throw new RangeError(`expected to index ${to} to be less than length ${length}`); } - const result = []; - for (let j = i; j < to; j++) { - result.push(this.get(j)); - } - return result; - } else if (this.ctx.isFuncDecl(i) || (this.ctx.isExpr(i) && this.ctx.isConst(i))) { - const result = this.getInterp(i); - assert(result !== null); - return result; - } else if (this.ctx.isSort(i)) { - return this.getUniverse(i); - } - assert(false, 'Number, declaration or constant expected'); - } - private getInterp(expr: FuncDecl | Expr): Expr | FuncInterp | null { - assert(this.ctx.isFuncDecl(expr) || this.ctx.isConst(expr), 'Declaration expected'); - if (this.ctx.isConst(expr)) { - assert(this.ctx.isExpr(expr)); - expr = expr.decl(); - } - assert(this.ctx.isFuncDecl(expr)); - if (expr.arity() === 0) { - const result = Z3.model_get_const_interp(this.ctx.ptr, this.ptr, expr.ptr); - if (result === null) { - return null; - } - return this.ctx._toExpr(result); - } else { - const interp = Z3.model_get_func_interp(this.ctx.ptr, this.ptr, expr.ptr); - if (interp === null) { - return null; - } - return new FuncInterpImpl(this.ctx, interp); - } - } - - private getUniverse(sort: Sort): AstVector { - this.ctx._assertContext(sort); - return new AstVectorImpl(this.ctx, Z3.model_get_sort_universe(this.ctx.ptr, this.ptr, sort.ptr)); - } - } - - class FuncInterpImpl implements FuncInterp { - declare readonly __typename: FuncInterp['__typename']; - - constructor(readonly ctx: Context, readonly ptr: Z3_func_interp) { - Z3.func_interp_inc_ref(ctx.ptr, ptr); - cleanup.register(this, () => Z3.func_interp_dec_ref(ctx.ptr, ptr)); - } - } - - class SortImpl extends AstImpl implements Sort { - declare readonly __typename: Sort['__typename']; - - get ast(): Z3_ast { - return Z3.sort_to_ast(this.ctx.ptr, this.ptr); - } - - kind() { - return Z3.get_sort_kind(this.ctx.ptr, this.ptr); - } - - subsort(other: Sort) { - this.ctx._assertContext(other); - return false; - } - - cast(expr: Expr): Expr { - this.ctx._assertContext(expr); - assert(expr.sort.eqIdentity(expr.sort), 'Sort mismatch'); - return expr; - } - - name() { - return this.ctx._fromSymbol(Z3.get_sort_name(this.ctx.ptr, this.ptr)); - } - - eqIdentity(other: Sort) { - this.ctx._assertContext(other); - return Z3.is_eq_sort(this.ctx.ptr, this.ptr, other.ptr); - } - - neqIdentity(other: Sort) { - return !this.eqIdentity(other); - } - } - - class FuncDeclImpl extends AstImpl implements FuncDecl { - declare readonly __typename: FuncDecl['__typename']; - - get ast() { - return Z3.func_decl_to_ast(this.ctx.ptr, this.ptr); - } - - name() { - return this.ctx._fromSymbol(Z3.get_decl_name(this.ctx.ptr, this.ptr)); - } - - arity() { - return Z3.get_arity(this.ctx.ptr, this.ptr); - } - - domain(i: number) { - assert(i < this.arity(), 'Index out of bounds'); - return this.ctx._toSort(Z3.get_domain(this.ctx.ptr, this.ptr, i)); - } - - range() { - return this.ctx._toSort(Z3.get_range(this.ctx.ptr, this.ptr)); - } - - kind() { - return Z3.get_decl_kind(this.ctx.ptr, this.ptr); - } - - params(): (number | string | Z3_symbol | Sort | Expr | FuncDecl)[] { - const n = Z3.get_decl_num_parameters(this.ctx.ptr, this.ptr); - const result = []; - for (let i = 0; i < n; i++) { - const kind = Z3.get_decl_parameter_kind(this.ctx.ptr, this.ptr, i); - switch (kind) { - case Z3_parameter_kind.Z3_PARAMETER_INT: - result.push(Z3.get_decl_int_parameter(this.ctx.ptr, this.ptr, i)); - break; - case Z3_parameter_kind.Z3_PARAMETER_DOUBLE: - result.push(Z3.get_decl_double_parameter(this.ctx.ptr, this.ptr, i)); - break; - case Z3_parameter_kind.Z3_PARAMETER_RATIONAL: - result.push(Z3.get_decl_rational_parameter(this.ctx.ptr, this.ptr, i)); - break; - case Z3_parameter_kind.Z3_PARAMETER_SYMBOL: - result.push(Z3.get_decl_symbol_parameter(this.ctx.ptr, this.ptr, i)); - break; - case Z3_parameter_kind.Z3_PARAMETER_SORT: - result.push(new SortImpl(this.ctx, Z3.get_decl_sort_parameter(this.ctx.ptr, this.ptr, i))); - break; - case Z3_parameter_kind.Z3_PARAMETER_AST: - result.push(new ExprImpl(this.ctx, Z3.get_decl_ast_parameter(this.ctx.ptr, this.ptr, i))); - break; - case Z3_parameter_kind.Z3_PARAMETER_FUNC_DECL: - result.push(new FuncDeclImpl(this.ctx, Z3.get_decl_func_decl_parameter(this.ctx.ptr, this.ptr, i))); - break; - default: - assertExhaustive(kind); - } - } - return result; - } - - call(...args: CoercibleToExpr[]) { - assert(args.length === this.arity(), `Incorrect number of arguments to ${this}`); - return this.ctx._toExpr( - Z3.mk_app( - this.ctx.ptr, - this.ptr, - args.map((arg, i) => { - return this.domain(i).cast(arg).ast; - }), - ), - ); - } - } - - class ExprImpl extends AstImpl implements Expr { - declare readonly __typename: Expr['__typename']; - - get sort(): S { - return this.ctx._toSort(Z3.get_sort(this.ctx.ptr, this.ast)) as S; - } - - eq(other: CoercibleToExpr): Bool { - return new BoolImpl(this.ctx, Z3.mk_eq(this.ctx.ptr, this.ast, this.ctx.from(other).ast)); - } - - neq(other: CoercibleToExpr): Bool { - return new BoolImpl( - this.ctx, - Z3.mk_distinct( - this.ctx.ptr, - [this, other].map(expr => this.ctx.from(expr).ast), - ), - ); - } - - params() { - return this.decl().params(); - } - - decl(): FuncDecl { - assert(this.ctx.isApp(this), 'Z3 application expected'); - return new FuncDeclImpl(this.ctx, Z3.get_app_decl(this.ctx.ptr, Z3.to_app(this.ctx.ptr, this.ast))); - } - - numArgs(): number { - assert(this.ctx.isApp(this), 'Z3 applicaiton expected'); - return Z3.get_app_num_args(this.ctx.ptr, Z3.to_app(this.ctx.ptr, this.ast)); - } - - arg(i: number): ReturnType { - assert(this.ctx.isApp(this), 'Z3 applicaiton expected'); - assert(i < this.numArgs(), 'Invalid argument index'); - return this.ctx._toExpr(Z3.get_app_arg(this.ctx.ptr, Z3.to_app(this.ctx.ptr, this.ast), i)); - } - - children(): ReturnType[] { - const num_args = this.numArgs(); - if (this.ctx.isApp(this)) { - const result = []; - for (let i = 0; i < num_args; i++) { - result.push(this.arg(i)); + const result: Item[] = []; + for (let i = from; i < to; i++) { + result.push(_toAst(check(Z3.ast_vector_get(contextPtr, this.ptr, i))) as Item); } return result; } - return []; - } - } - class BoolSortImpl extends SortImpl implements BoolSort { - declare readonly __typename: BoolSort['__typename']; - - cast(other: Bool | boolean): Bool; - cast(other: CoercibleToExpr): never; - cast(other: CoercibleToExpr | Bool) { - if (typeof other === 'boolean') { - other = this.ctx.Bool.val(other); - } - assert(this.ctx.isExpr(other), 'true, false or Z3 Boolean expression expected.'); - assert(this.eqIdentity(other.sort), 'Value cannot be converted into a Z3 Boolean value'); - return other; - } - - subsort(other: Sort) { - this.ctx._assertContext(other.ctx); - return other instanceof ArithSortImpl; - } - } - - class BoolImpl extends ExprImpl implements Bool { - declare readonly __typename: Bool['__typename']; - - not(): Bool { - return this.ctx.Not(this); - } - and(other: Bool | boolean): Bool { - return this.ctx.And(this, other); - } - or(other: Bool | boolean): Bool { - return this.ctx.Or(this, other); - } - xor(other: Bool | boolean): Bool { - return this.ctx.Xor(this, other); - } - } - - class ProbeImpl implements Probe { - declare readonly __typename: Probe['__typename']; - - constructor(readonly ctx: ContextImpl, readonly ptr: Z3_probe) {} - } - - class TacticImpl implements Tactic { - declare readonly __typename: Tactic['__typename']; - - readonly ptr: Z3_tactic; - - constructor(readonly ctx: ContextImpl, tactic: string | Z3_tactic) { - let myPtr: Z3_tactic; - if (typeof tactic === 'string') { - myPtr = Z3.mk_tactic(ctx.ptr, tactic); - } else { - myPtr = tactic; + set(i: number, v: Item): void { + _assertContext(v); + if (i >= this.length()) { + throw new RangeError(`expected index ${i} to be less than length ${this.length()}`); + } + check(Z3.ast_vector_set(contextPtr, this.ptr, i, v.ast)); } - this.ptr = myPtr; + push(v: Item): void { + _assertContext(v); + check(Z3.ast_vector_push(contextPtr, this.ptr, v.ast)); + } - Z3.tactic_inc_ref(ctx.ptr, myPtr); - cleanup.register(this, () => Z3.tactic_dec_ref(ctx.ptr, myPtr)); - } - } + resize(size: number): void { + check(Z3.ast_vector_resize(contextPtr, this.ptr, size)); + } - class ArithSortImpl extends SortImpl implements ArithSort { - declare readonly __typename: ArithSort['__typename']; - - cast(other: bigint | number): IntNum | RatNum; - cast(other: CoercibleRational | RatNum): RatNum; - cast(other: IntNum): IntNum; - cast(other: Bool | Arith): Arith; - cast(other: CoercibleToExpr): never; - cast(other: CoercibleToExpr): Arith | RatNum | IntNum { - const { If, isExpr, isArith, isBool, isIntSort, isRealSort, ToReal, Int, Real } = this.ctx; - const sortTypeStr = isIntSort(this) ? 'IntSort' : 'RealSort'; - if (isExpr(other)) { - const otherS = other.sort; - if (isArith(other)) { - if (this.eqIdentity(otherS)) { - return other; - } else if (isIntSort(otherS) && isRealSort(this)) { - return this.ctx.ToReal(other); - } - assert(false, "Can't cast Real to IntSort without loss"); - } else if (isBool(other)) { - if (isIntSort(this)) { - return If(other, 1, 0); - } else { - return ToReal(If(other, 1, 0)); + has(v: Item): boolean { + _assertContext(v); + for (const item of this.values()) { + if (item.eqIdentity(v)) { + return true; } } - assert(false, `Can't cast expression to ${sortTypeStr}`); - } else { - if (typeof other !== 'boolean') { - if (isIntSort(this)) { - assert(!isCoercibleRational(other), "Can't cast fraction to IntSort"); - return Int.val(other); - } - return Real.val(other); - } - assert(false, `Can't cast primitive to ${sortTypeStr}`); + return false; } - } - } - class ArithImpl extends ExprImpl implements Arith { - declare readonly __typename: Arith['__typename']; - - add(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_add(this.ctx.ptr, [this.ast, this.sort.cast(other).ast])); - } - - mul(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_mul(this.ctx.ptr, [this.ast, this.sort.cast(other).ast])); - } - - sub(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_sub(this.ctx.ptr, [this.ast, this.sort.cast(other).ast])); - } - - pow(exponent: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_power(this.ctx.ptr, this.ast, this.sort.cast(exponent).ast)); - } - - div(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_div(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - mod(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(this.ctx, Z3.mk_mod(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - neg() { - return new ArithImpl(this.ctx, Z3.mk_unary_minus(this.ctx.ptr, this.ast)); - } - - le(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(this.ctx, Z3.mk_le(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - lt(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(this.ctx, Z3.mk_lt(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - gt(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(this.ctx, Z3.mk_gt(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - ge(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(this.ctx, Z3.mk_ge(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - } - - class IntNumImpl extends ArithImpl implements IntNum { - declare readonly __typename: IntNum['__typename']; - - get value() { - return BigInt(this.asString()); - } - - asString() { - return Z3.get_numeral_string(this.ctx.ptr, this.ast); - } - - asBinary() { - return Z3.get_numeral_binary_string(this.ctx.ptr, this.ast); - } - } - - class RatNumImpl extends ArithImpl implements RatNum { - declare readonly __typename: RatNum['__typename']; - - get value() { - return { numerator: this.numerator().value, denominator: this.denominator().value }; - } - - numerator() { - return new IntNumImpl(this.ctx, Z3.get_numerator(this.ctx.ptr, this.ast)); - } - - denominator() { - return new IntNumImpl(this.ctx, Z3.get_denominator(this.ctx.ptr, this.ast)); - } - - asNumber() { - const { numerator, denominator } = this.value; - const div = numerator / denominator; - return Number(div) + Number(numerator - div * denominator) / Number(denominator); - } - - asDecimal(prec: number = Number.parseInt(getParam('precision') ?? FALLBACK_PRECISION.toString())) { - return Z3.get_numeral_decimal_string(this.ctx.ptr, this.ast, prec); - } - - asString() { - return Z3.get_numeral_string(this.ctx.ptr, this.ast); - } - } - - class BitVecSortImpl extends SortImpl implements BitVecSort { - declare readonly __typename: BitVecSort['__typename']; - - get size() { - return Z3.get_bv_sort_size(this.ctx.ptr, this.ptr); - } - - subsort(other: Sort): boolean { - return this.ctx.isBitVecSort(other) && this.size < other.size; - } - - cast(other: CoercibleToBitVec): BitVec; - cast(other: CoercibleToExpr): Expr; - cast(other: CoercibleToExpr): Expr { - if (this.ctx.isExpr(other)) { - this.ctx._assertContext(other); - return other; - } - assert(!isCoercibleRational(other), "Can't convert rational to BitVec"); - return this.ctx.BitVec.val(other, this.size); - } - } - - class BitVecImpl extends ExprImpl implements BitVec { - declare readonly __typename: BitVec['__typename']; - - get size() { - return this.sort.size; - } - - add(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvadd(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - mul(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvmul(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - sub(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvsub(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - sdiv(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvsdiv(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - udiv(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvudiv(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - smod(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvsmod(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - urem(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvurem(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - srem(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvsrem(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - neg(): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvneg(this.ctx.ptr, this.ast)); - } - - or(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvor(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - and(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvand(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - nand(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvnand(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - xor(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvxor(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - xnor(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvxnor(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - shr(count: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvashr(this.ctx.ptr, this.ast, this.sort.cast(count).ast)); - } - lshr(count: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvlshr(this.ctx.ptr, this.ast, this.sort.cast(count).ast)); - } - shl(count: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvshl(this.ctx.ptr, this.ast, this.sort.cast(count).ast)); - } - rotateRight(count: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_ext_rotate_right(this.ctx.ptr, this.ast, this.sort.cast(count).ast)); - } - rotateLeft(count: CoercibleToBitVec): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_ext_rotate_left(this.ctx.ptr, this.ast, this.sort.cast(count).ast)); - } - not(): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvnot(this.ctx.ptr, this.ast)); - } - - extract(high: number, low: number): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_extract(this.ctx.ptr, high, low, this.ast)); - } - signExt(count: number): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_sign_ext(this.ctx.ptr, count, this.ast)); - } - zeroExt(count: number): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_zero_ext(this.ctx.ptr, count, this.ast)); - } - repeat(count: number): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_repeat(this.ctx.ptr, count, this.ast)); - } - - sle(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvsle(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - ule(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvule(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - slt(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvslt(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - ult(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvult(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - sge(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvsge(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - uge(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvuge(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - sgt(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvsgt(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - ugt(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvugt(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - - redAnd(): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvredand(this.ctx.ptr, this.ast)); - } - redOr(): BitVec { - return new BitVecImpl(this.ctx, Z3.mk_bvredor(this.ctx.ptr, this.ast)); - } - - addNoOverflow(other: CoercibleToBitVec, isSigned: boolean): Bool { - return new BoolImpl( - this.ctx, - Z3.mk_bvadd_no_overflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast, isSigned), - ); - } - addNoUnderflow(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvadd_no_underflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - subNoOverflow(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvsub_no_overflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - subNoUndeflow(other: CoercibleToBitVec, isSigned: boolean): Bool { - return new BoolImpl( - this.ctx, - Z3.mk_bvsub_no_underflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast, isSigned), - ); - } - sdivNoOverflow(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvsdiv_no_overflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - mulNoOverflow(other: CoercibleToBitVec, isSigned: boolean): Bool { - return new BoolImpl( - this.ctx, - Z3.mk_bvmul_no_overflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast, isSigned), - ); - } - mulNoUndeflow(other: CoercibleToBitVec): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvmul_no_underflow(this.ctx.ptr, this.ast, this.sort.cast(other).ast)); - } - negNoOverflow(): Bool { - return new BoolImpl(this.ctx, Z3.mk_bvneg_no_overflow(this.ctx.ptr, this.ast)); - } - } - - class BitVecNumImpl extends BitVecImpl implements BitVecNum { - declare readonly __typename: BitVecNum['__typename']; - get value() { - return BigInt(this.asString()); - } - - asSignedValue() { - let val = this.value; - const size = BigInt(this.size); - if (val >= 2n ** (size - 1n)) { - val = val - 2n ** size; - } - if (val < (-2n) ** (size - 1n)) { - val = val + 2n ** size; - } - return val; - } - asString() { - return Z3.get_numeral_string(this.ctx.ptr, this.ast); - } - asBinaryString() { - return Z3.get_numeral_binary_string(this.ctx.ptr, this.ast); - } - } - - class AstVectorImpl { - declare readonly __typename: AstVector['__typename']; - - constructor(readonly ctx: ContextImpl, readonly ptr: Z3_ast_vector = Z3.mk_ast_vector(ctx.ptr)) { - Z3.ast_vector_inc_ref(ctx.ptr, ptr); - cleanup.register(this, () => Z3.ast_vector_dec_ref(ctx.ptr, ptr)); - } - - get length(): number { - return Z3.ast_vector_size(this.ctx.ptr, this.ptr); - } - - [Symbol.iterator](): IterableIterator { - return this.values(); - } - - *entries(): IterableIterator<[number, Item]> { - const length = this.length; - for (let i = 0; i < length; i++) { - yield [i, this.get(i)]; + sexpr(): string { + return check(Z3.ast_vector_to_string(contextPtr, this.ptr)); } } - *keys(): IterableIterator { - for (let [key] of this.entries()) { - yield key; - } - } + class AstMapImpl, Value extends AnyAst> implements AstMap { + declare readonly __typename: AstMap['__typename']; + readonly ctx: Context; - *values(): IterableIterator { - for (let [, value] of this.entries()) { - yield value; - } - } - - get(i: number): Item; - get(from: number, to: number): Item[]; - get(from: number, to?: number): Item | Item[] { - const length = this.length; - if (from < 0) { - from += length; - } - if (from >= length) { - throw new RangeError(); + constructor(readonly ptr: Z3_ast_map = Z3.mk_ast_map(contextPtr)) { + this.ctx = ctx; + Z3.ast_map_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr)); } - if (to === undefined) { - return this.ctx._toAst(Z3.ast_vector_get(this.ctx.ptr, this.ptr, from)) as Item; + [Symbol.iterator](): Iterator<[Key, Value]> { + return this.entries(); } - if (to < 0) { - to += length; - } - if (to >= length) { - throw new RangeError(); + get size(): number { + return Z3.ast_map_size(contextPtr, this.ptr); } - const result: Item[] = []; - for (let i = from; i < to; i++) { - result.push(this.ctx._toAst(Z3.ast_vector_get(this.ctx.ptr, this.ptr, i)) as Item); - } - return result; - } - - set(i: number, v: Item): void { - this.ctx._assertContext(v); - if (i >= this.length) { - throw new RangeError(); - } - Z3.ast_vector_set(this.ctx.ptr, this.ptr, i, v.ast); - } - - push(v: Item): void { - this.ctx._assertContext(v); - Z3.ast_vector_push(this.ctx.ptr, this.ptr, v.ast); - } - - resize(size: number): void { - Z3.ast_vector_resize(this.ctx.ptr, this.ptr, size); - } - - has(v: Item): boolean { - this.ctx._assertContext(v); - for (const item of this.values()) { - if (item.eqIdentity(v)) { - return true; + *entries(): IterableIterator<[Key, Value]> { + for (const key of this.keys()) { + yield [key, this.get(key)]; } } - return false; - } - sexpr(): string { - return Z3.ast_vector_to_string(this.ctx.ptr, this.ptr); - } - } + keys(): AstVector { + return new AstVectorImpl(Z3.ast_map_keys(contextPtr, this.ptr)); + } - class AstMapImpl implements AstMap { - declare readonly __typename: AstMap['__typename']; + *values(): IterableIterator { + 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; + } - constructor(readonly ctx: ContextImpl, readonly ptr: Z3_ast_map = Z3.mk_ast_map(ctx.ptr)) { - Z3.ast_map_inc_ref(ctx.ptr, ptr); - cleanup.register(this, () => Z3.ast_map_dec_ref(ctx.ptr, ptr)); - } + set(key: Key, value: Value): void { + check(Z3.ast_map_insert(contextPtr, this.ptr, key.ast, value.ast)); + } - [Symbol.iterator](): Iterator<[Key, Value]> { - return this.entries(); - } + delete(key: Key): void { + check(Z3.ast_map_erase(contextPtr, this.ptr, key.ast)); + } - get size(): number { - return Z3.ast_map_size(this.ctx.ptr, this.ptr); - } + clear(): void { + check(Z3.ast_map_reset(contextPtr, this.ptr)); + } - *entries(): IterableIterator<[Key, Value]> { - for (const key of this.keys()) { - yield [key, this.get(key)]; + has(key: Key): boolean { + return check(Z3.ast_map_contains(contextPtr, this.ptr, key.ast)); + } + + sexpr(): string { + return check(Z3.ast_map_to_string(contextPtr, this.ptr)); } } - keys(): AstVector { - return new AstVectorImpl(this.ctx, Z3.ast_map_keys(this.ctx.ptr, this.ptr)); - } + const ctx: Context = { + ptr: contextPtr, + name, - *values(): IterableIterator { - for (const [_, value] of this.entries()) { - yield value; - } - } - get(key: Key): Value { - return this.ctx._toAst(Z3.ast_map_find(this.ctx.ptr, this.ptr, key.ast)) as Value; - } + ///////////// + // Classes // + ///////////// + Solver: SolverImpl, + Model: ModelImpl, + Tactic: TacticImpl, + AstVector: AstVectorImpl as AstVectorCtor, + AstMap: AstMapImpl as AstMapCtor, - set(key: Key, value: Value): void { - Z3.ast_map_insert(this.ctx.ptr, this.ptr, key.ast, value.ast); - } + /////////////// + // Functions // + /////////////// + interrupt, + isModel, + isAst, + isSort, + isFuncDecl, + isApp, + isConst, + isExpr, + isVar, + isAppOf, + isBool, + isTrue, + isFalse, + isAnd, + isOr, + isImplies, + isNot, + isEq, + isDistinct, + isArith, + isArithSort, + isInt, + isIntVal, + isIntSort, + isReal, + isRealVal, + isRealSort, + isBitVecSort, + isBitVec, + isBitVecVal, // TODO fix ordering + isProbe, + isTactic, + isAstVector, + eqIdentity, + getVarIndex, + from, + solve, - delete(key: Key): void { - Z3.ast_map_erase(this.ctx.ptr, this.ptr, key.ast); - } + ///////////// + // Objects // + ///////////// + Sort, + Function, + RecFunc, + Bool, + Int, + Real, + BitVec, - clear(): void { - Z3.ast_map_reset(this.ctx.ptr, this.ptr); - } - - has(key: Key): boolean { - return Z3.ast_map_contains(this.ctx.ptr, this.ptr, key.ast); - } - - sexpr(): string { - return Z3.ast_map_to_string(this.ctx.ptr, this.ptr); - } + //////////////// + // Operations // + //////////////// + If, + Distinct, + Const, + Consts, + FreshConst, + Var, + Implies, + Eq, + Xor, + Not, + And, + Or, + ToReal, + ToInt, + IsInt, + Sqrt, + Cbrt, + BV2Int, + Int2BV, + Concat, + Cond, + }; + cleanup.register(ctx, () => Z3.del_context(contextPtr)); + return ctx; } return { @@ -1881,8 +1962,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { getParam, setParam, resetParams, - isContext, - Context: ContextImpl as ContextCtor, + Context: createContext, }; } diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index a056ef686..eae81ff98 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -16,13 +16,13 @@ import { } from '../low-level'; /** @hidden */ -export type AnySort = +export type AnySort = | Sort | BoolSort | ArithSort | BitVecSort; /** @hidden */ -export type AnyExpr = +export type AnyExpr = | Expr | Bool | Arith @@ -31,10 +31,10 @@ export type AnyExpr = | BitVec | BitVecNum; /** @hidden */ -export type AnyAst = AnyExpr | AnySort | FuncDecl; +export type AnyAst = AnyExpr | AnySort | FuncDecl; /** @hidden */ -export type SortToExprMap, Name extends string = any> = S extends BoolSort +export type SortToExprMap, Name extends string = 'main'> = S extends BoolSort ? Bool : S extends ArithSort ? Arith @@ -45,7 +45,7 @@ export type SortToExprMap, Name extends string = any> = : never; /** @hidden */ -export type CoercibleToExprMap, Name extends string = any> = S extends bigint +export type CoercibleToExprMap, Name extends string = 'main'> = S extends bigint ? IntNum : S extends number | CoercibleRational ? RatNum @@ -76,38 +76,20 @@ export type CoercibleToExprMap, Name extends str export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number }; /** @hidden */ -export type CoercibleToExpr = number | bigint | boolean | CoercibleRational | Expr; +export type CoercibleToExpr = number | bigint | boolean | CoercibleRational | Expr; export class Z3Error extends Error {} export class Z3AssertionError extends Z3Error {} -/** - * Returned by {@link Solver.check} when Z3 could find a solution - * @category Global - */ -export const sat = Symbol('Solver found a solution'); -/** - * Returned by {@link Solver.check} when Z3 couldn't find a solution - * @category Global - */ -export const unsat = Symbol("Solver didn't find a solution"); -/** - * Returned by {@link Solver.check} when Z3 couldn't reason about the assumptions - * @category Global - */ -export const unknown = Symbol("Solver couldn't reason about the assumptions"); /** @category Global */ -export type CheckSatResult = typeof sat | typeof unsat | typeof unknown; +export type CheckSatResult = 'sat' | 'unsat' | 'unknown'; /** @hidden */ export interface ContextCtor { - new (name: Name, options?: Record): Context; + (name: Name, options?: Record): Context; } -export interface Context { - /** @hidden */ - readonly __typename: 'Context'; - +export interface Context { /** @hidden */ readonly ptr: Z3_context; /** @@ -190,7 +172,7 @@ export interface Context { /** @category Functions */ isTactic(obj: unknown): obj is Tactic; /** @category Functions */ - isAstVector(obj: unknown): obj is AstVector, Name>; + isAstVector(obj: unknown): obj is AstVector>; /** * Returns whether two Asts are the same thing * @category Functions */ @@ -232,7 +214,7 @@ export interface Context { * * @see {@link Solver} * @category Functions */ - solve(...assertions: Bool[]): Promise; + solve(...assertions: Bool[]): Promise | 'unsat' | 'unknown'>; ///////////// // Classes // @@ -250,9 +232,9 @@ export interface Context { */ readonly Model: new () => Model; /** @category Classes */ - readonly AstVector: new = AnyAst>() => AstVector; + readonly AstVector: new = AnyAst>() => AstVector; /** @category Classes */ - readonly AstMap: new () => AstMap; + readonly AstMap: new = AnyAst, Value extends Ast = AnyAst>() => AstMap; /** @category Classes */ readonly Tactic: new (name: string) => Tactic; @@ -309,7 +291,7 @@ export interface Context { /** @category Operations */ And(): Bool; /** @category Operations */ - And(vector: AstVector, Name>): Bool; + And(vector: AstVector>): Bool; /** @category Operations */ And(...args: (Bool | boolean)[]): Bool; /** @category Operations */ @@ -317,7 +299,7 @@ export interface Context { /** @category Operations */ Or(): Bool; /** @category Operations */ - Or(vector: AstVector, Name>): Bool; + Or(vector: AstVector>): Bool; /** @category Operations */ Or(...args: (Bool | boolean)[]): Bool; /** @category Operations */ @@ -368,9 +350,11 @@ export interface Context { Int2BV(a: Arith | bigint | number, bits: Bits): BitVec; /** @category Operations */ Concat(...bitvecs: BitVec[]): BitVec; + /** @category Operations */ + Cond(probe: Probe, onTrue: Tactic, onFalse: Tactic): Tactic } -export interface Ast { +export interface Ast { /** @hidden */ readonly __typename: 'Ast' | Sort['__typename'] | FuncDecl['__typename'] | Expr['__typename']; @@ -380,7 +364,7 @@ export interface Ast { /** @virtual */ get ast(): Z3_ast; /** @virtual */ - get id(): number; + id(): number; eqIdentity(other: Ast): boolean; neqIdentity(other: Ast): boolean; @@ -392,7 +376,7 @@ export interface Ast { export interface SolverCtor { new (): Solver; } -export interface Solver { +export interface Solver { /** @hidden */ readonly __typename: 'Solver'; @@ -407,10 +391,10 @@ export interface Solver { pop(num?: number): void; numScopes(): number; reset(): void; - add(...exprs: (Bool | AstVector, Name>)[]): void; + add(...exprs: (Bool | AstVector>)[]): void; addAndTrack(expr: Bool, constant: Bool | string): void; - assertions(): AstVector, Name>; - check(...exprs: (Bool | AstVector, Name>)[]): Promise; + assertions(): AstVector>; + check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; } @@ -418,14 +402,14 @@ export interface Solver { export interface ModelCtor { new (): Model; } -export interface Model extends Iterable> { +export interface Model extends Iterable> { /** @hidden */ readonly __typename: 'Model'; readonly ctx: Context; readonly ptr: Z3_model; - get length(): number; + length(): number; entries(): IterableIterator<[number, FuncDecl]>; keys(): IterableIterator; @@ -436,10 +420,10 @@ export interface Model extends Iterable, modelCompletion?: boolean): Arith; eval(expr: Expr, modelCompletion?: boolean): Expr; get(i: number): FuncDecl; - get(from: number, to: number): FuncDecl[]; + get(from: number, to: number): FuncDecl[]; get(declaration: FuncDecl): FuncInterp | Expr; get(constant: Expr): Expr; - get(sort: Sort): AstVector, Name>; + get(sort: Sort): AstVector>; } /** @@ -461,7 +445,7 @@ export interface Model extends Iterable { declare(name: string): Sort; } -export interface Sort extends Ast { +export interface Sort extends Ast { /** @hidden */ readonly __typename: 'Sort' | BoolSort['__typename'] | ArithSort['__typename'] | BitVecSort['__typename']; @@ -476,7 +460,7 @@ export interface Sort extends Ast { /** * @category Functions */ -export interface FuncInterp { +export interface FuncInterp { /** @hidden */ readonly __typename: 'FuncInterp'; @@ -516,7 +500,7 @@ export interface RecFuncCreation { /** * @category Functions */ -export interface FuncDecl extends Ast { +export interface FuncDecl extends Ast { /** @hidden */ readonly __typename: 'FuncDecl'; @@ -529,7 +513,7 @@ export interface FuncDecl extends Ast[]): AnyExpr; } -export interface Expr = AnySort, Ptr = unknown> +export interface Expr = AnySort, Ptr = unknown> extends Ast { /** @hidden */ readonly __typename: 'Expr' | Bool['__typename'] | Arith['__typename'] | BitVec['__typename']; @@ -546,7 +530,7 @@ export interface Expr = AnySort< } /** @category Booleans */ -export interface BoolSort extends Sort { +export interface BoolSort extends Sort { /** @hidden */ readonly __typename: 'BoolSort'; @@ -554,7 +538,7 @@ export interface BoolSort extends Sort { cast(expr: CoercibleToExpr): never; } /** @category Booleans */ -export interface BoolCreation { +export interface BoolCreation { sort(): BoolSort; const(name: string): Bool; @@ -565,7 +549,7 @@ export interface BoolCreation { val(value: boolean): Bool; } /** @category Booleans */ -export interface Bool extends Expr, Z3_ast> { +export interface Bool extends Expr, Z3_ast> { /** @hidden */ readonly __typename: 'Bool'; @@ -579,7 +563,7 @@ export interface Bool extends Expr extends Sort { +export interface ArithSort extends Sort { /** @hidden */ readonly __typename: 'ArithSort'; @@ -615,7 +599,7 @@ export interface RealCreation { * Represents Integer or Real number expression * @category Arithmetic */ -export interface Arith extends Expr, Z3_ast> { +export interface Arith extends Expr, Z3_ast> { /** @hidden */ readonly __typename: 'Arith' | IntNum['__typename'] | RatNum['__typename']; @@ -683,11 +667,11 @@ export interface Arith extends Expr extends Arith { +export interface IntNum extends Arith { /** @hidden */ readonly __typename: 'IntNum'; - get value(): bigint; + value(): bigint; asString(): string; asBinary(): string; } @@ -707,11 +691,11 @@ export interface IntNum extends Arith { * ``` * @category Arithmetic */ -export interface RatNum extends Arith { +export interface RatNum extends Arith { /** @hidden */ readonly __typename: 'RatNum'; - get value(): { numerator: bigint; denominator: bigint }; + value(): { numerator: bigint; denominator: bigint }; numerator(): IntNum; denominator(): IntNum; asNumber(): number; @@ -725,7 +709,7 @@ export interface RatNum extends Arith { * @typeParam Bits - A number representing amount of bits for this sort * @category Bit Vectors */ -export interface BitVecSort extends Sort { +export interface BitVecSort extends Sort { /** @hidden */ readonly __typename: 'BitVecSort'; @@ -739,14 +723,14 @@ export interface BitVecSort): BitVec; cast(other: CoercibleToExpr): Expr; } /** @hidden */ -export type CoercibleToBitVec = +export type CoercibleToBitVec = | bigint | number | BitVec; @@ -769,7 +753,7 @@ export interface BitVecCreation { * Represents Bit Vector expression * @category Bit Vectors */ -export interface BitVec +export interface BitVec extends Expr, Z3_ast> { /** @hidden */ readonly __typename: 'BitVec' | BitVecNum['__typename']; @@ -790,7 +774,7 @@ export interface BitVec * // 8 * ``` */ - get size(): Bits; + size(): Bits; /** @category Arithmetic */ add(other: CoercibleToBitVec): BitVec; @@ -959,17 +943,17 @@ export interface BitVec * Represents Bit Vector constant value * @category Bit Vectors */ -export interface BitVecNum extends BitVec { +export interface BitVecNum extends BitVec { /** @hidden */ readonly __typename: 'BitVecNum'; - get value(): bigint; + value(): bigint; asSignedValue(): bigint; asString(): string; asBinaryString(): string; } -export interface Probe { +export interface Probe { /** @hidden */ readonly __typename: 'Probe'; @@ -981,7 +965,7 @@ export interface Probe { export interface TacticCtor { new (name: string): Tactic; } -export interface Tactic { +export interface Tactic { /** @hidden */ readonly __typename: 'Tactic'; @@ -991,7 +975,7 @@ export interface Tactic { /** @hidden */ export interface AstVectorCtor { - new = AnyAst>(): AstVector; + new = AnyAst>(): AstVector; } /** * Stores multiple {@link Ast} objects @@ -1009,13 +993,13 @@ export interface AstVectorCtor { * // [2, x] * ``` */ -export interface AstVector = AnyAst, Name extends string = any> extends Iterable { +export interface AstVector = AnyAst> extends Iterable { /** @hidden */ readonly __typename: 'AstVector'; readonly ctx: Context; readonly ptr: Z3_ast_vector; - get length(): number; + length(): number; entries(): IterableIterator<[number, Item]>; keys(): IterableIterator; @@ -1031,7 +1015,7 @@ export interface AstVector = AnyAst, Name extends string /** @hidden */ export interface AstMapCtor { - new (): AstMap; + new = AnyAst, Value extends Ast = AnyAst>(): AstMap; } /** * Stores a mapping between different {@link Ast} objects @@ -1054,7 +1038,7 @@ export interface AstMapCtor { * // 0 * ``` */ -export interface AstMap = AnyAst, Value extends Ast = AnyAst, Name extends string = any> +export interface AstMap = AnyAst, Value extends Ast = AnyAst> extends Iterable<[Key, Value]> { /** @hidden */ readonly __typename: 'AstMap'; @@ -1064,7 +1048,7 @@ export interface AstMap = AnyAst, Value extends Ast = AnyA get size(): number; entries(): IterableIterator<[Key, Value]>; - keys(): AstVector; + keys(): AstVector; values(): IterableIterator; get(key: Key): Value | undefined; set(key: Key, value: Value): void; @@ -1119,11 +1103,6 @@ export interface Z3HighLevel { */ getParam(name: string): string | null; - /** - * Returns whether the given object is a {@link Context} - */ - isContext(obj: unknown): obj is Context; - /** * Use this to create new contexts * @see {@link Context} diff --git a/src/api/js/src/high-level/utils.test.ts b/src/api/js/src/high-level/utils.test.ts index 945f7e9d0..791782783 100644 --- a/src/api/js/src/high-level/utils.test.ts +++ b/src/api/js/src/high-level/utils.test.ts @@ -1,5 +1,5 @@ import { Z3AssertionError } from './types'; -import { allSatisfy, assert, assertExhaustive, autoBind } from './utils'; +import { allSatisfy, assert, assertExhaustive } from './utils'; describe('allSatisfy', () => { it('returns null on empty array', () => { @@ -56,28 +56,6 @@ describe('assertExhaustive', () => { }); }); -describe('autoBind', () => { - class Binded { - readonly name = 'Richard'; - constructor(shouldBind: boolean) { - if (shouldBind === true) { - autoBind(this); - } - } - - test(): string { - return `Hello ${this.name}`; - } - } - - it('binds this', () => { - const { test: withoutBind } = new Binded(false); - const { test: withBind } = new Binded(true); - expect(() => withoutBind()).toThrowError(TypeError); - expect(withBind()).toStrictEqual('Hello Richard'); - }); -}); - describe('assert', () => { it('throws on failure', () => { expect(() => assert(false)).toThrowError(Z3AssertionError); diff --git a/src/api/js/src/high-level/utils.ts b/src/api/js/src/high-level/utils.ts index bd5013710..2f01da170 100644 --- a/src/api/js/src/high-level/utils.ts +++ b/src/api/js/src/high-level/utils.ts @@ -10,32 +10,6 @@ function getAllProperties(obj: Record) { return properties; } -// https://github.com/sindresorhus/auto-bind -// We modify it to use CommonJS instead of ESM -/* -MIT License - -Copyright (c) Sindre Sorhus (https://sindresorhus.com) - -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: - -The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -*/ -export function autoBind>(self: Self): Self { - for (const [obj, key] of getAllProperties(self.constructor.prototype)) { - if (key === 'constructor') { - continue; - } - const descriptor = Reflect.getOwnPropertyDescriptor(obj, key); - if (descriptor && typeof descriptor.value === 'function') { - (self[key] as any) = self[key].bind(self); - } - } - return self; -} - /** * Use to ensure that switches are checked to be exhaustive at compile time *