diff --git a/src/api/js/examples/high-level/using_smtlib2.ts b/src/api/js/examples/high-level/using_smtlib2.ts new file mode 100644 index 000000000..e9275b7bf --- /dev/null +++ b/src/api/js/examples/high-level/using_smtlib2.ts @@ -0,0 +1,36 @@ +// @ts-ignore we're not going to bother with types for this +import process from 'process'; +import { init } from '../../build/node'; +import assert from 'assert'; + +(async () => { + let { Context, em } = await init(); + let z3 = Context('main'); + + const x = z3.BitVec.const('x', 256); + const y = z3.BitVec.const('y', 256); + const z = z3.BitVec.const('z', 256); + const xPlusY = x.add(y); + const xPlusZ = x.add(z); + const expr = xPlusY.mul(xPlusZ); + + const to_check = expr.eq(z3.Const('test', expr.sort)); + + const solver = new z3.Solver(); + solver.add(to_check); + const cr = await solver.check(); + console.log(cr); + assert(cr === 'sat'); + + const model = solver.model(); + let modelStr = model.sexpr(); + modelStr = modelStr.replace(/\n/g, ' '); + console.log("Model: ", modelStr); + + const exprs = z3.ast_from_string(modelStr); + console.log(exprs); + +})().catch(e => { + console.error('error', e); + process.exit(1); +}); \ No newline at end of file diff --git a/src/api/js/examples/low-level/example-raw.ts b/src/api/js/examples/low-level/example-raw.ts index 6e34b4aba..2790f9594 100644 --- a/src/api/js/examples/low-level/example-raw.ts +++ b/src/api/js/examples/low-level/example-raw.ts @@ -1,3 +1,4 @@ +// @ts-ignore we're not going to bother with types for this import process from 'process'; import { init, Z3_error_code } from '../../build/node'; diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index f6969a933..a46cae951 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -4461,14 +4461,14 @@ "dev": true }, "shiki": { - "version": "0.10.1", - "resolved": "https://registry.npmjs.org/shiki/-/shiki-0.10.1.tgz", - "integrity": "sha512-VsY7QJVzU51j5o1+DguUd+6vmCmZ5v/6gYu4vyYAhzjuNQU6P/vmSy4uQaOhvje031qQMiW0d2BwgMH52vqMng==", + "version": "0.11.1", + "resolved": "https://registry.npmjs.org/shiki/-/shiki-0.11.1.tgz", + "integrity": "sha512-EugY9VASFuDqOexOgXR18ZV+TbFrQHeCpEYaXamO+SZlsnT/2LxuLBX25GGtIrwaEVFXUAbUQ601SWE2rMwWHA==", "dev": true, "requires": { "jsonc-parser": "^3.0.0", "vscode-oniguruma": "^1.6.1", - "vscode-textmate": "5.2.0" + "vscode-textmate": "^6.0.0" } }, "side-channel": { @@ -4826,16 +4826,15 @@ "dev": true }, "typedoc": { - "version": "0.22.18", - "resolved": "https://registry.npmjs.org/typedoc/-/typedoc-0.22.18.tgz", - "integrity": "sha512-NK9RlLhRUGMvc6Rw5USEYgT4DVAUFk7IF7Q6MYfpJ88KnTZP7EneEa4RcP+tX1auAcz7QT1Iy0bUSZBYYHdoyA==", + "version": "0.23.16", + "resolved": "https://registry.npmjs.org/typedoc/-/typedoc-0.23.16.tgz", + "integrity": "sha512-rumYsCeNRXlyuZVzefD7050n7ptL2uudsCJg50dY0v/stKniqIlRpvx/F/6expC0/Q6Dbab+g/JpZuB7Sw90FA==", "dev": true, "requires": { - "glob": "^8.0.3", "lunr": "^2.3.9", - "marked": "^4.0.16", + "marked": "^4.0.19", "minimatch": "^5.1.0", - "shiki": "^0.10.1" + "shiki": "^0.11.1" }, "dependencies": { "brace-expansion": { @@ -4847,19 +4846,6 @@ "balanced-match": "^1.0.0" } }, - "glob": { - "version": "8.0.3", - "resolved": "https://registry.npmjs.org/glob/-/glob-8.0.3.tgz", - "integrity": "sha512-ull455NHSHI/Y1FqGaaYFaLGkNMMJbavMrEGFXG/PGrg6y7sutWHUHrz6gy6WEBH6akM1M414dWKCNs+IhKdiQ==", - "dev": true, - "requires": { - "fs.realpath": "^1.0.0", - "inflight": "^1.0.4", - "inherits": "2", - "minimatch": "^5.0.1", - "once": "^1.3.0" - } - }, "minimatch": { "version": "5.1.0", "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.0.tgz", @@ -4872,9 +4858,9 @@ } }, "typescript": { - "version": "4.5.4", - "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.5.4.tgz", - "integrity": "sha512-VgYs2A2QIRuGphtzFV7aQJduJ2gyfTljngLzjpfW9FoYZF6xuw1W0vW9ghCKLfcWrCFxK81CSGRAvS1pn4fIUg==", + "version": "4.8.4", + "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.8.4.tgz", + "integrity": "sha512-QCh+85mCy+h0IGff8r5XWzOVSbBO+KfeYrMQh7NJ58QujwcE22u+NUSmUxqF+un70P9GXKxa2HCNiTTMJknyjQ==", "dev": true }, "typical": { @@ -4945,9 +4931,9 @@ "dev": true }, "vscode-textmate": { - "version": "5.2.0", - "resolved": "https://registry.npmjs.org/vscode-textmate/-/vscode-textmate-5.2.0.tgz", - "integrity": "sha512-Uw5ooOQxRASHgu6C7GVvUxisKXfSgW4oFlO+aa+PAkgmH89O3CXxEEzNRNtHSqtXFTl0nAC1uYj0GMSH27uwtQ==", + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/vscode-textmate/-/vscode-textmate-6.0.0.tgz", + "integrity": "sha512-gu73tuZfJgu+mvCSy4UZwd2JXykjK9zAZsfmDeut5dx/1a7FeTk0XwJsSuqQn+cuMCGVbIBfl+s53X4T19DnzQ==", "dev": true }, "walker": { diff --git a/src/api/js/package.json b/src/api/js/package.json index 90a7bfa3d..3e79ba8f4 100644 --- a/src/api/js/package.json +++ b/src/api/js/package.json @@ -1,5 +1,6 @@ { "name": "z3-solver", + "version": "0.1.0", "keywords": [ "Z3", "theorem", @@ -26,8 +27,8 @@ "build:ts:generate": "ts-node --transpileOnly scripts/make-ts-wrapper.ts src/low-level/wrapper.__GENERATED__.ts src/low-level/types.__GENERATED__.ts", "build:wasm": "ts-node --transpileOnly ./scripts/build-wasm.ts", "clean": "rimraf build 'src/**/*.__GENERATED__.*'", - "lint": "prettier -c '{,src/,scripts/,examples}*.{js,ts}'", - "format": "prettier --write '{,src/,scripts/}*.{js,ts}'", + "lint": "prettier -c '{./,src/,scripts/,examples/}**/*.{js,ts}'", + "format": "prettier --write '{./,src/,scripts/}**/*.{js,ts}'", "test": "jest", "docs": "typedoc", "check-engine": "check-engine" @@ -53,8 +54,8 @@ "ts-expect": "^1.3.0", "ts-jest": "^28.0.3", "ts-node": "^10.8.0", - "typedoc": "^0.22.17", - "typescript": "^4.5.4" + "typedoc": "^0.23.16", + "typescript": "^4.8.4" }, "license": "MIT", "dependencies": { diff --git a/src/api/js/scripts/make-ts-wrapper.ts b/src/api/js/scripts/make-ts-wrapper.ts index 58b2ce0ae..568609467 100644 --- a/src/api/js/scripts/make-ts-wrapper.ts +++ b/src/api/js/scripts/make-ts-wrapper.ts @@ -76,6 +76,7 @@ function makeTsWrapper() { } const isInParam = (p: FuncParam) => p.kind !== undefined && ['in', 'in_array'].includes(p.kind); + function wrapFunction(fn: Func) { if (CUSTOM_IMPLEMENTATIONS.includes(fn.name)) { return null; @@ -104,7 +105,7 @@ function makeTsWrapper() { let isAsync = asyncFuncs.includes(fn.name); let trivial = - !['string', 'boolean'].includes(fn.ret) && + !['string', 'boolean', 'unsigned'].includes(fn.ret) && !fn.nullableRet && outParams.length === 0 && !inParams.some(p => p.type === 'string' || p.isArray || p.nullable); @@ -234,6 +235,7 @@ function makeTsWrapper() { function setArg() { args[outParam.idx] = memIdx === 0 ? 'outAddress' : `outAddress + ${memIdx * 4}`; } + let read, type; if (outParam.type === 'string') { read = `Mod.UTF8ToString(getOutUint(${memIdx}))`; @@ -330,11 +332,15 @@ function makeTsWrapper() { if (ret === 0) { return null; } - `.trim(); + `.trim(); + } else if (fn.ret === 'unsigned') { + infix += ` + ret = (new Uint32Array([ret]))[0]; + `.trim(); } // prettier-ignore - let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`; + let invocation = `Mod.ccall('${isAsync ? "async_" : ""}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(", ")}])`; if (isAsync) { invocation = `await Mod.async_call(() => ${invocation})`; diff --git a/src/api/js/scripts/parse-api.ts b/src/api/js/scripts/parse-api.ts index c3292583a..a3aa81acd 100644 --- a/src/api/js/scripts/parse-api.ts +++ b/src/api/js/scripts/parse-api.ts @@ -45,7 +45,7 @@ const types = { __proto__: null, // these are function types I can't be bothered to parse - // NSB: They can be extracted automatically from z3_api.h thanks to the use + // NSB: They can be extracted automatically from z3_api.h thanks to the use // of a macro. Z3_error_handler: 'Z3_error_handler', Z3_push_eh: 'Z3_push_eh', 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 70c11b875..d42075169 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -1,8 +1,8 @@ import assert from 'assert'; import asyncToArray from 'iter-tools/methods/async-to-array'; import { init, killThreads } from '../jest'; -import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types'; -import { expectType } from "ts-expect"; +import { Arith, Bool, Model, Quantifier, Z3AssertionError, Z3HighLevel, AstVector } from './types'; +import { expectType } from 'ts-expect'; /** * Generate all possible solutions from given assumptions. @@ -58,6 +58,7 @@ async function* allSolutions(...assertions: Bool[]): async function prove(conjecture: Bool): Promise { const solver = new conjecture.ctx.Solver(); + solver.set('timeout', 1000); const { Not } = solver.ctx; solver.add(Not(conjecture)); expect(await solver.check()).toStrictEqual('unsat'); @@ -113,11 +114,11 @@ describe('high-level', () => { it('test loading a solver state from a string', async () => { const { Solver, Not, Int } = api.Context('main'); const solver = new Solver(); - solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))") - expect(await solver.check()).toStrictEqual('sat') - const x = Int.const('x') - solver.add(Not(x.eq(1))) - expect(await solver.check()).toStrictEqual('unsat') + solver.fromString('(declare-const x Int) (assert (and (< x 2) (> x 0)))'); + expect(await solver.check()).toStrictEqual('sat'); + const x = Int.const('x'); + solver.add(Not(x.eq(1))); + expect(await solver.check()).toStrictEqual('unsat'); }); it('disproves x = y implies g(g(x)) = g(y)', async () => { @@ -393,14 +394,13 @@ describe('high-level', () => { }); describe('arrays', () => { - it('Example 1', async () => { const Z3 = api.Context('main'); const arr = Z3.Array.const('arr', Z3.Int.sort(), Z3.Int.sort()); const [idx, val] = Z3.Int.consts('idx val'); - const conjecture = (arr.store(idx, val).select(idx).eq(val)); + const conjecture = arr.store(idx, val).select(idx).eq(val); await prove(conjecture); }); @@ -428,7 +428,7 @@ describe('high-level', () => { // and is detected at compile time // @ts-expect-error const arr3 = Array.const('arr3', BitVec.sort(1)); - }) + }); it('can do simple proofs', async () => { const { BitVec, Array, isArray, isArraySort, isConstArray, Eq, Not } = api.Context('main'); @@ -447,13 +447,6 @@ describe('high-level', () => { await prove(Eq(arr2.select(0), FIVE_VAL)); await prove(Not(Eq(arr2.select(0), BitVec.val(6, 256)))); await prove(Eq(arr2.store(idx, val).select(idx), constArr.store(idx, val).select(idx))); - - // TODO: add in Quantifiers and better typing of arrays - // await prove( - // ForAll([idx], idx.add(1).ugt(idx).and(arr.select(idx.add(1)).ugt(arr.select(idx)))).implies( - // arr.select(0).ult(arr.select(1000)) - // ) - // ); }); it('Finds arrays that differ but that sum to the same', async () => { @@ -465,18 +458,16 @@ describe('high-level', () => { const arr1 = Array.const('arr', BitVec.sort(2), BitVec.sort(32)); const arr2 = Array.const('arr2', BitVec.sort(2), BitVec.sort(32)); - const same_sum = arr1.select(0) + const same_sum = arr1 + .select(0) .add(arr1.select(1)) .add(arr1.select(2)) .add(arr1.select(3)) - .eq( - arr2.select(0) - .add(arr2.select(1)) - .add(arr2.select(2)) - .add(arr2.select(3)) - ); + .eq(arr2.select(0).add(arr2.select(1)).add(arr2.select(2)).add(arr2.select(3))); - const different = arr1.select(0).neq(arr2.select(0)) + const different = arr1 + .select(0) + .neq(arr2.select(0)) .or(arr1.select(1).neq(arr2.select(1))) .or(arr1.select(2).neq(arr2.select(2))) .or(arr1.select(3).neq(arr2.select(3))); @@ -485,11 +476,105 @@ describe('high-level', () => { const arr1Vals = [0, 1, 2, 3].map(i => model.eval(arr1.select(i)).value()); const arr2Vals = [0, 1, 2, 3].map(i => model.eval(arr2.select(i)).value()); - expect((arr1Vals.reduce((a, b) => a + b, 0n) % mod) === arr2Vals.reduce((a, b) => a + b, 0n) % mod); + expect(arr1Vals.reduce((a, b) => a + b, 0n) % mod === arr2Vals.reduce((a, b) => a + b, 0n) % mod); for (let i = 0; i < 4; i++) { expect(arr1Vals[i] !== arr2Vals[i]); } }); + + it('Array type inference', async () => { + const z3 = api.Context('main'); + + const Z3_ADDR = z3.BitVec.const('Vault_addr', 160); + const Z3_GLOBAL_STORAGE = z3.Array.const( + 'global_storage', + z3.BitVec.sort(160), + z3.Array.sort(z3.BitVec.sort(160), z3.BitVec.sort(256)), + ); + const Z3_STORAGE = Z3_GLOBAL_STORAGE.select(Z3_ADDR); + + // We are so far unable to properly infer the type of Z3_STORAGE + // expectType< + // SMTArray<'main', [BitVecSort<160>], BitVecSort<256>> + // >(Z3_STORAGE); + }); + }); + + describe('quantifiers', () => { + it('Basic Universal', async () => { + const Z3 = api.Context('main'); + + const [x, y] = Z3.Int.consts('x y'); + + const conjecture = Z3.ForAll([x, y], x.neq(y).implies(x.lt(y).or(x.gt(y)))); + expect(Z3.isBool(conjecture)).toBeTruthy(); + expect(conjecture.var_name(0)).toBe('x'); + expect(conjecture.var_sort(0).eqIdentity(Z3.Int.sort())).toBeTruthy(); + expect(conjecture.var_name(1)).toBe('y'); + expect(conjecture.var_sort(1).eqIdentity(Z3.Int.sort())).toBeTruthy(); + await prove(conjecture); + }); + + it('Basic Existential', async () => { + const Z3 = api.Context('main'); + + const [x, y, z] = Z3.Int.consts('x y z'); + + const quantifier = Z3.Exists([z], Z3.Not(z.lt(x)).and(Z3.Not(z.gt(y)))); + expect(Z3.isBool(quantifier)).toBeTruthy(); + expect(quantifier.var_name(0)).toBe('z'); + expect(quantifier.var_sort(0).eqIdentity(Z3.Int.sort())).toBeTruthy(); + + const conjecture = Z3.Not(x.gt(y)).implies(quantifier); // Can be trivially discovered with z = x or x = y + await prove(conjecture); + }); + + it('Basic Lambda', async () => { + const Z3 = api.Context('main'); + + const [x, y] = Z3.Int.consts('x y z'); + const L = Z3.Lambda([x, y], x.add(y)); + expect(Z3.isArraySort(L.sort)).toBeTruthy(); + expect(Z3.isArray(L)).toBeFalsy(); + expect(L.var_name(0)).toBe('x'); + expect(L.var_sort(0).eqIdentity(Z3.Int.sort())).toBeTruthy(); + expect(L.var_name(1)).toBe('y'); + expect(L.var_sort(1).eqIdentity(Z3.Int.sort())).toBeTruthy(); + + const conjecture = L.select(Z3.Int.val(2), Z3.Int.val(5)).eq(Z3.Int.val(7)); + await prove(conjecture); + }); + + it('Loading Quantifier Preserves Type', async () => { + const Z3 = api.Context('main'); + + const [x, y, z] = Z3.Int.consts('x y z'); + const quantifier = Z3.Exists([z], Z3.Not(z.lt(x)).and(Z3.Not(z.gt(y)))); + expect(Z3.isBool(quantifier)).toBeTruthy(); + + const solver = new Z3.Solver(); + solver.add(quantifier); + + const dumped_str = solver.toString(); + + const solver2 = new Z3.Solver(); + solver2.fromString(dumped_str); + const quantifier2 = solver2.assertions().get(0) as unknown as Quantifier; + expect(Z3.isBool(quantifier2)).toBeTruthy(); + expect(quantifier2.var_name(0)).toBe('z'); + }); + }); + + describe('uninterpreted functions', () => { + it('Type Inference', async () => { + const Z3 = api.Context('main'); + + const f = Z3.Function.declare('f', Z3.Int.sort(), Z3.Bool.sort()); + const input = Z3.Int.val(6); + const output = f.call(input); + expectType(output); + expect(output.sort.eqIdentity(Z3.Bool.sort())).toBeTruthy(); + }); }); describe('Solver', () => { @@ -543,10 +628,11 @@ describe('high-level', () => { describe('AstVector', () => { it('can use basic methods', async () => { - const { Solver, AstVector, Int } = api.Context('main'); + const Z3 = api.Context('main'); + const { Solver, Int } = Z3; const solver = new Solver(); - const vector = new AstVector(); + const vector = new Z3.AstVector(); for (let i = 0; i < 5; i++) { vector.push(Int.const(`int__${i}`)); } @@ -559,4 +645,57 @@ describe('high-level', () => { expect(await solver.check()).toStrictEqual('sat'); }); }); + + describe('Substitution', () => { + it('basic variable substitution', async () => { + const { Int, substitute } = api.Context('main'); + const x = Int.const('x'); + const y = Int.const('y'); + const z = Int.const('z'); + + const expr = x.add(y); + const subst = substitute(expr, [x, z]); + expect(subst.eqIdentity(z.add(y))).toBeTruthy(); + }); + + it('term substitution', async () => { + const { Int, substitute } = api.Context('main'); + const x = Int.const('x'); + const y = Int.const('y'); + const z = Int.const('z'); + + const expr = x.add(y).mul(Int.val(1).sub(x.add(y))); + const subst = substitute(expr, [x.add(y), z]); + expect(subst.eqIdentity(z.mul(Int.val(1).sub(z)))).toBeTruthy(); + }); + }); + + describe('Model', () => { + it('Assigning constants', async () => { + const { Int, Model } = api.Context('main'); + const m = new Model(); + + const [x, y] = Int.consts('x y'); + + m.updateValue(x, Int.val(6)); + m.updateValue(y, Int.val(12)); + + expect(m.eval(x.add(y)).eqIdentity(Int.val(18))).toBeTruthy(); + }); + + it('Creating Func Interpretations', async () => { + const { Int, Function, Model } = api.Context('main'); + const m = new Model(); + + const f = Function.declare('f', Int.sort(), Int.sort(), Int.sort()); + + const f_interp = m.addFuncInterp(f, 0); + f_interp.addEntry([Int.val(1), Int.val(2)], Int.val(3)); + f_interp.addEntry([Int.val(4), Int.val(5)], Int.val(6)); + + expect(m.eval(f.call(1, 2)).eqIdentity(Int.val(3))).toBeTruthy(); + expect(m.eval(f.call(4, 5)).eqIdentity(Int.val(6))).toBeTruthy(); + expect(m.eval(f.call(0, 0)).eqIdentity(Int.val(0))).toBeTruthy(); + }); + }); }); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 59a0b1e36..80f89b104 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -31,13 +31,19 @@ import { Z3_symbol, Z3_symbol_kind, Z3_tactic, + Z3_pattern, + Z3_app, + Z3_params, + Z3_func_entry, } from '../low-level'; import { AnyAst, AnyExpr, AnySort, Arith, - ArithSort, ArrayIndexType, + ArithSort, + ArrayIndexType, + CoercibleToArrayIndexType, Ast, AstMap, AstMapCtor, @@ -48,11 +54,12 @@ import { BitVecSort, Bool, BoolSort, - CheckSatResult, CoercibleFromMap, + CheckSatResult, + CoercibleToMap, CoercibleRational, CoercibleToBitVec, CoercibleToExpr, - CoercibleToExprMap, + CoercibleFromMap, Context, ContextCtor, Expr, @@ -61,7 +68,10 @@ import { FuncInterp, IntNum, Model, + Pattern, Probe, + Quantifier, + BodyT, RatNum, SMTArray, SMTArraySort, @@ -71,6 +81,9 @@ import { Tactic, Z3Error, Z3HighLevel, + CoercibleToArith, + NonEmptySortArray, + FuncEntry, } from './types'; import { allSatisfy, assert, assertExhaustive } from './utils'; @@ -81,18 +94,19 @@ const asyncMutex = new Mutex(); function isCoercibleRational(obj: any): obj is CoercibleRational { // prettier-ignore const r = ( - (obj !== null && - (typeof obj === 'object' || typeof obj === 'function')) && - (obj.numerator !== null && - (typeof obj.numerator === 'number' || typeof obj.numerator === 'bigint')) && - (obj.denominator !== null && - (typeof obj.denominator === 'number' || typeof obj.denominator === 'bigint')) - ); - r && assert( - (typeof obj!.numerator !== 'number' || Number.isSafeInteger(obj!.numerator)) && - (typeof obj!.denominator !== 'number' || Number.isSafeInteger(obj!.denominator)), - 'Fraction numerator and denominator must be integers', - ); + (obj !== null && + (typeof obj === 'object' || typeof obj === 'function')) && + (obj.numerator !== null && + (typeof obj.numerator === 'number' || typeof obj.numerator === 'bigint')) && + (obj.denominator !== null && + (typeof obj.denominator === 'number' || typeof obj.denominator === 'bigint')) + ); + r && + assert( + (typeof obj!.numerator !== 'number' || Number.isSafeInteger(obj!.numerator)) && + (typeof obj!.denominator !== 'number' || Number.isSafeInteger(obj!.denominator)), + 'Fraction numerator and denominator must be integers', + ); return r; } @@ -152,9 +166,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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())) - ); + 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); @@ -171,7 +183,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } - function check(val: T) { + function check(val: T): T { throwIfError(); return val; } @@ -199,6 +211,26 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + function _toParams(key: string, value: any): Z3_params { + const params = Z3.mk_params(contextPtr); + Z3.params_inc_ref(contextPtr, params); + // If value is a boolean + if (typeof value === 'boolean') { + Z3.params_set_bool(contextPtr, params, _toSymbol(key), value); + } else if (typeof value === 'number') { + // If value is a uint + if (Number.isInteger(value)) { + check(Z3.params_set_uint(contextPtr, params, _toSymbol(key), value)); + } else { + // If value is a double + check(Z3.params_set_double(contextPtr, params, _toSymbol(key), value)); + } + } else if (typeof value === 'string') { + check(Z3.params_set_symbol(contextPtr, params, _toSymbol(key), _toSymbol(value))); + } + return params; + } + function _toAst(ast: Z3_ast): AnyAst { switch (check(Z3.get_ast_kind(contextPtr, ast))) { case Z3_ast_kind.Z3_SORT_AST: @@ -229,13 +261,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function _toExpr(ast: Z3_ast): AnyExpr { const kind = check(Z3.get_ast_kind(contextPtr, ast)); if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) { - if (Z3.is_quantifier_forall(contextPtr, ast)) - return new BoolImpl(ast); - if (Z3.is_quantifier_exists(contextPtr, ast)) - return new BoolImpl(ast); - if (Z3.is_lambda(contextPtr, ast)) - return new ExprImpl(ast); - assert(false); + if (Z3.is_lambda(contextPtr, ast)) { + return new LambdaImpl(ast); + } + return new NonLambdaQuantifierImpl(ast); } const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast))); switch (sortKind) { @@ -325,6 +354,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return r; } + function isFuncInterp(obj: unknown): obj is FuncInterp { + const r = obj instanceof FuncInterpImpl; + r && _assertContext(obj); + return r; + } + function isApp(obj: unknown): boolean { if (!isExpr(obj)) { return false; @@ -352,7 +387,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } function isBool(obj: unknown): obj is Bool { - const r = obj instanceof BoolImpl; + const r = obj instanceof ExprImpl && obj.sort.kind() === Z3_sort_kind.Z3_BOOL_SORT; r && _assertContext(obj); return r; } @@ -389,6 +424,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return isAppOf(obj, Z3_decl_kind.Z3_OP_DISTINCT); } + function isQuantifier(obj: unknown): obj is Quantifier { + const r = obj instanceof QuantifierImpl; + r && _assertContext(obj); + return r; + } + function isArith(obj: unknown): obj is Arith { const r = obj instanceof ArithImpl; r && _assertContext(obj); @@ -531,8 +572,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { // expression simplification // /////////////////////////////// - async function simplify(e: Expr) { - const result = await Z3.simplify(contextPtr, e.ast) + async function simplify(e: Expr): Promise> { + const result = await Z3.simplify(contextPtr, e.ast); return _toExpr(check(result)); } @@ -543,7 +584,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { declare: (name: string) => new SortImpl(Z3.mk_uninterpreted_sort(contextPtr, _toSymbol(name))), }; const Function = { - declare: (name: string, ...signature: FuncDeclSignature) => { + declare: [], RangeSort extends Sort>( + name: string, + ...signature: [...DomainSort, RangeSort] + ): FuncDecl => { const arity = signature.length - 1; const rng = signature[arity]; _assertContext(rng); @@ -552,9 +596,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(signature[i]); dom.push(signature[i].ptr); } - return new FuncDeclImpl(Z3.mk_func_decl(contextPtr, _toSymbol(name), dom, rng.ptr)); + return new FuncDeclImpl(Z3.mk_func_decl(contextPtr, _toSymbol(name), dom, rng.ptr)); }, - fresh: (...signature: FuncDeclSignature) => { + fresh: [], RangeSort extends Sort>( + ...signature: [...DomainSort, RangeSort] + ): FuncDecl => { const arity = signature.length - 1; const rng = signature[arity]; _assertContext(rng); @@ -563,7 +609,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(signature[i]); dom.push(signature[i].ptr); } - return new FuncDeclImpl(Z3.mk_fresh_func_decl(contextPtr, 'f', dom, rng.ptr)); + return new FuncDeclImpl(Z3.mk_fresh_func_decl(contextPtr, 'f', dom, rng.ptr)); }, }; const RecFunc = { @@ -701,7 +747,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }, }; const Array = { - sort, ...AnySort[]], RangeSort extends AnySort>( + sort, RangeSort extends AnySort>( ...sig: [...DomainSort, RangeSort] ): SMTArraySort { const arity = sig.length - 1; @@ -711,16 +757,23 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new ArraySortImpl(Z3.mk_array_sort(contextPtr, d.ptr, r.ptr)); } const dom = sig.slice(0, arity); - return new ArraySortImpl(Z3.mk_array_sort_n(contextPtr, dom.map(s => s.ptr), r.ptr)); - }, - const, ...AnySort[]], RangeSort extends AnySort>( - name: string, ...sig: [...DomainSort, RangeSort] - ): SMTArray { - return new ArrayImpl( - check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(...sig).ptr)) + return new ArraySortImpl( + Z3.mk_array_sort_n( + contextPtr, + dom.map(s => s.ptr), + r.ptr, + ), ); }, - consts, ...AnySort[]], RangeSort extends AnySort>( + const, RangeSort extends AnySort>( + name: string, + ...sig: [...DomainSort, RangeSort] + ): SMTArray { + return new ArrayImpl( + check(Z3.mk_const(contextPtr, _toSymbol(name), Array.sort(...sig).ptr)), + ); + }, + consts, RangeSort extends AnySort>( names: string | string[], ...sig: [...DomainSort, RangeSort] ): SMTArray[] { @@ -731,13 +784,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }, K, RangeSort extends AnySort>( domain: DomainSort, - value: SortToExprMap + value: SortToExprMap, ): SMTArray { - return new ArrayImpl<[DomainSort], RangeSort>( - check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr)) - ); - } - } + return new ArrayImpl<[DomainSort], RangeSort>(check(Z3.mk_const_array(contextPtr, domain.ptr, value.ptr))); + }, + }; //////////////// // Operations // @@ -747,7 +798,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { condition: Bool | boolean, onTrue: OnTrueRef, onFalse: OnFalseRef, - ): CoercibleToExprMap; + ): CoercibleFromMap; function If( condition: Bool | Probe | boolean, onTrue: CoercibleToExpr | Tactic, @@ -812,6 +863,13 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new BoolImpl(check(Z3.mk_implies(contextPtr, a.ptr, b.ptr))); } + function Iff(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_iff(contextPtr, a.ptr, b.ptr))); + } + function Eq(a: CoercibleToExpr, b: CoercibleToExpr): Bool { a = from(a); b = from(b); @@ -897,6 +955,84 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + function ForAll>( + quantifiers: ArrayIndexType, + body: Bool, + weight: number = 1, + ): NonLambdaQuantifierImpl { + // Verify all quantifiers are constants + if (!allSatisfy(quantifiers, isConst)) { + throw new Error('Quantifier variables must be constants'); + } + + return new NonLambdaQuantifierImpl( + check( + Z3.mk_quantifier_const_ex( + contextPtr, + true, + weight, + _toSymbol(''), + _toSymbol(''), + quantifiers.map(q => q.ptr as unknown as Z3_app), // The earlier check verifies these are all apps + [], + [], + body.ptr, + ), + ), + ); + } + + function Exists>( + quantifiers: ArrayIndexType, + body: Bool, + weight: number = 1, + ): NonLambdaQuantifierImpl { + // Verify all quantifiers are constants + if (!allSatisfy(quantifiers, isConst)) { + throw new Error('Quantifier variables must be constants'); + } + + return new NonLambdaQuantifierImpl( + check( + Z3.mk_quantifier_const_ex( + contextPtr, + false, + weight, + _toSymbol(''), + _toSymbol(''), + quantifiers.map(q => q.ptr as unknown as Z3_app), // The earlier check verifies these are all apps + [], + [], + body.ptr, + ), + ), + ); + } + + function Lambda, RangeSort extends Sort>( + quantifiers: ArrayIndexType, + expr: SortToExprMap, + ): LambdaImpl { + // TODO(walden): For some reason LambdaImpl leads to type issues + // and Typescript won't build. I'm not sure why since the types seem to all match + // up. For now, we just use any for the domain sort + + // Verify all quantifiers are constants + if (!allSatisfy(quantifiers, isConst)) { + throw new Error('Quantifier variables must be constants'); + } + + return new LambdaImpl( + check( + Z3.mk_lambda_const( + contextPtr, + quantifiers.map(q => q.ptr as unknown as Z3_app), + expr.ptr, + ), + ), + ); + } + function ToReal(expr: Arith | bigint): Arith { expr = from(expr) as Arith; _assertContext(expr); @@ -961,6 +1097,101 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new TacticImpl(check(Z3.tactic_cond(contextPtr, probe.ptr, onTrue.ptr, onFalse.ptr))); } + function LT(a: Arith, b: CoercibleToArith): Bool { + return new BoolImpl(check(Z3.mk_lt(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function GT(a: Arith, b: CoercibleToArith): Bool { + return new BoolImpl(check(Z3.mk_gt(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function LE(a: Arith, b: CoercibleToArith): Bool { + return new BoolImpl(check(Z3.mk_le(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function GE(a: Arith, b: CoercibleToArith): Bool { + return new BoolImpl(check(Z3.mk_ge(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function ULT(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvult(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function UGT(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvugt(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function ULE(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvule(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function UGE(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvuge(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function SLT(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvslt(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function SGT(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsgt(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function SLE(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsle(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function SGE(a: BitVec, b: CoercibleToBitVec): Bool { + return new BoolImpl(check(Z3.mk_bvsge(contextPtr, a.ast, a.sort.cast(b).ast))); + } + + function Extract(hi: number, lo: number, val: BitVec): BitVec { + return new BitVecImpl(check(Z3.mk_extract(contextPtr, hi, lo, val.ast))); + } + + function Select, RangeSort extends Sort>( + array: SMTArray, + ...indices: CoercibleToArrayIndexType + ): SortToExprMap { + const args = indices.map((arg, i) => array.domain_n(i).cast(arg as any)); + if (args.length === 1) { + return _toExpr(check(Z3.mk_select(contextPtr, array.ast, args[0].ast))) as SortToExprMap; + } + const _args = args.map(arg => arg.ast); + return _toExpr(check(Z3.mk_select_n(contextPtr, array.ast, _args))) as SortToExprMap; + } + + function Store, RangeSort extends Sort>( + array: SMTArray, + ...indicesAndValue: [ + ...CoercibleToArrayIndexType, + CoercibleToMap, Name>, + ] + ): SMTArray { + const args = indicesAndValue.map((arg, i) => { + if (i === indicesAndValue.length - 1) { + return array.range().cast(arg as any) as SortToExprMap; + } + return array.domain_n(i).cast(arg as any); + }); + if (args.length <= 1) { + throw new Error('Array store requires both index and value arguments'); + } + if (args.length === 2) { + return _toExpr(check(Z3.mk_store(contextPtr, array.ast, args[0].ast, args[1].ast))) as SMTArray< + Name, + DomainSort, + RangeSort + >; + } + const _idxs = args.slice(0, args.length - 1).map(arg => arg.ast); + return _toExpr(check(Z3.mk_store_n(contextPtr, array.ast, _idxs, args[args.length - 1].ast))) as SMTArray< + Name, + DomainSort, + RangeSort + >; + } + class AstImpl implements Ast { declare readonly __typename: Ast['__typename']; readonly ctx: Context; @@ -1023,6 +1254,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr)); } + set(key: string, value: any): void { + Z3.solver_set_params(contextPtr, this.ptr, _toParams(key, value)); + } + push() { Z3.solver_push(contextPtr, this.ptr); } @@ -1110,20 +1345,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return this.values(); } - * entries(): IterableIterator<[number, FuncDecl]> { + *entries(): IterableIterator<[number, FuncDecl]> { const length = this.length(); for (let i = 0; i < length; i++) { yield [i, this.get(i)]; } } - * keys(): IterableIterator { + *keys(): IterableIterator { for (const [key] of this.entries()) { yield key; } } - * values(): IterableIterator> { + *values(): IterableIterator> { for (const [, value] of this.entries()) { yield value; } @@ -1160,7 +1395,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { get(sort: Sort): AstVector>; get( i: number | FuncDecl | Expr | Sort, - to?: number + to?: number, ): FuncDecl | FuncInterp | Expr | AstVector> | FuncDecl[] { assert(to === undefined || typeof i === 'number'); if (typeof i === 'number') { @@ -1200,6 +1435,41 @@ export function createApi(Z3: Z3Core): Z3HighLevel { assert(false, 'Number, declaration or constant expected'); } + updateValue(decl: FuncDecl | Expr, a: Ast | FuncInterp): void { + _assertContext(decl); + _assertContext(a); + if (isExpr(decl)) { + decl = decl.decl(); + } + if (isFuncDecl(decl) && decl.arity() !== 0 && isFuncInterp(a)) { + const funcInterp = this.addFuncInterp(decl, a.elseValue() as Expr); + for (let i = 0; i < a.numEntries(); i++) { + const e = a.entry(i); + const n = e.numArgs(); + const args = global.Array(n).map((_, i) => e.argValue(i)); + funcInterp.addEntry(args, e.value()); + } + return; + } + if (!isFuncDecl(decl) || decl.arity() !== 0) { + throw new Z3Error('Expecting 0-ary function or constant expression'); + } + if (!isAst(a)) { + throw new Z3Error('Only func declarations can be assigned to func interpretations'); + } + check(Z3.add_const_interp(contextPtr, this.ptr, decl.ptr, a.ast)); + } + + addFuncInterp[] = Sort[], RangeSort extends Sort = Sort>( + decl: FuncDecl, + defaultValue: CoercibleToMap, Name>, + ): FuncInterp { + const fi = check( + Z3.add_func_interp(contextPtr, this.ptr, decl.ptr, decl.range().cast(defaultValue).ptr as Z3_ast), + ); + return new FuncInterpImpl(fi); + } + private getInterp(expr: FuncDecl | Expr): Expr | FuncInterp | null { assert(isFuncDecl(expr) || isConst(expr), 'Declaration expected'); if (isConst(expr)) { @@ -1228,6 +1498,30 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + class FuncEntryImpl implements FuncEntry { + declare readonly __typename: FuncEntry['__typename']; + + readonly ctx: Context; + + constructor(readonly ptr: Z3_func_entry) { + this.ctx = ctx; + Z3.func_entry_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr)); + } + + numArgs() { + return check(Z3.func_entry_get_num_args(contextPtr, this.ptr)); + } + + argValue(i: number): Expr { + return _toExpr(check(Z3.func_entry_get_arg(contextPtr, this.ptr, i))); + } + + value(): Expr { + return _toExpr(check(Z3.func_entry_get_value(contextPtr, this.ptr))); + } + } + class FuncInterpImpl implements FuncInterp { declare readonly __typename: FuncInterp['__typename']; readonly ctx: Context; @@ -1237,6 +1531,33 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.func_interp_inc_ref(contextPtr, ptr); cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr)); } + + elseValue(): Expr { + return _toExpr(check(Z3.func_interp_get_else(contextPtr, this.ptr))); + } + + numEntries(): number { + return check(Z3.func_interp_get_num_entries(contextPtr, this.ptr)); + } + + arity(): number { + return check(Z3.func_interp_get_arity(contextPtr, this.ptr)); + } + + entry(i: number): FuncEntry { + return new FuncEntryImpl(check(Z3.func_interp_get_entry(contextPtr, this.ptr, i))); + } + + addEntry(args: Expr[], value: Expr): void { + const argsVec = new AstVectorImpl(); + for (const arg of args) { + argsVec.push(arg); + } + _assertContext(argsVec); + _assertContext(value); + assert(this.arity() === argsVec.length(), "Number of arguments in entry doesn't match function arity"); + check(Z3.func_interp_add_entry(contextPtr, this.ptr, argsVec.ptr, value.ptr as Z3_ast)); + } } class SortImpl extends AstImpl implements Sort { @@ -1275,10 +1596,13 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } - class FuncDeclImpl extends AstImpl implements FuncDecl { + class FuncDeclImpl[], RangeSort extends Sort> + extends AstImpl + implements FuncDecl + { declare readonly __typename: FuncDecl['__typename']; - get ast() { + get ast(): Z3_ast { return Z3.func_decl_to_ast(contextPtr, this.ptr); } @@ -1290,20 +1614,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return Z3.get_arity(contextPtr, this.ptr); } - domain(i: number) { + domain(i: T): DomainSort[T] { 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)); + range(): RangeSort { + return _toSort(Z3.get_range(contextPtr, this.ptr)) as RangeSort; } kind() { return Z3.get_decl_kind(contextPtr, this.ptr); } - params(): (number | string | Z3_symbol | Sort | Expr | FuncDecl)[] { + params(): (number | string | Sort | Expr | FuncDecl)[] { const n = Z3.get_decl_num_parameters(contextPtr, this.ptr); const result = []; for (let i = 0; i < n; i++) { @@ -1319,7 +1643,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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))); + result.push(_fromSymbol(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)))); @@ -1337,21 +1661,26 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return result; } - call(...args: CoercibleToExpr[]) { + call(...args: CoercibleToArrayIndexType): SortToExprMap { 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; - }), - )), - ); + check( + Z3.mk_app( + contextPtr, + this.ptr, + args.map((arg, i) => { + return this.domain(i).cast(arg as any).ast; + }), + ), + ), + ) as SortToExprMap; } } - class ExprImpl = AnySort> extends AstImpl implements Expr { + class ExprImpl = AnySort> + extends AstImpl + implements Expr + { declare readonly __typename: Expr['__typename']; get sort(): S { @@ -1364,13 +1693,19 @@ export function createApi(Z3: Z3Core): Z3HighLevel { neq(other: CoercibleToExpr): Bool { return new BoolImpl( - check(Z3.mk_distinct( - contextPtr, - [this, other].map(expr => from(expr).ast), - )), + check( + Z3.mk_distinct( + contextPtr, + [this, other].map(expr => from(expr).ast), + ), + ), ); } + name() { + return this.decl().name(); + } + params() { return this.decl().params(); } @@ -1404,6 +1739,16 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + class PatternImpl implements Pattern { + declare readonly __typename: Pattern['__typename']; + readonly ctx: Context; + + constructor(readonly ptr: Z3_pattern) { + this.ctx = ctx; + // TODO: implement rest of Pattern + } + } + class BoolSortImpl extends SortImpl implements BoolSort { declare readonly __typename: BoolSort['__typename']; @@ -1425,7 +1770,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } class BoolImpl extends ExprImpl> implements Bool { - declare readonly __typename: Bool['__typename']; + declare readonly __typename: 'Bool' | 'NonLambdaQuantifier'; not(): Bool { return Not(this); @@ -1446,6 +1791,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { implies(other: Bool | boolean): Bool { return Implies(this, other); } + + iff(other: Bool | boolean): Bool { + return Iff(this, other); + } } class ProbeImpl implements Probe { @@ -1482,12 +1831,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { class ArithSortImpl extends SortImpl implements ArithSort { declare readonly __typename: ArithSort['__typename']; - cast(other: bigint | number): IntNum | RatNum; + cast(other: bigint | number | string): 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 { + cast(other: CoercibleToExpr | string): Arith | RatNum | IntNum { const sortTypeStr = isIntSort(this) ? 'IntSort' : 'RealSort'; if (isExpr(other)) { const otherS = other.sort; @@ -1519,51 +1868,164 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + function Sum(arg0: Arith, ...args: CoercibleToArith[]): Arith; + function Sum( + arg0: BitVec, + ...args: CoercibleToBitVec[] + ): BitVec; + function Sum>(arg0: T, ...args: CoercibleToMap[]): T { + if (arg0 instanceof BitVecImpl) { + // Assert only 2 + if (args.length !== 1) { + throw new Error('BitVec add only supports 2 arguments'); + } + return new BitVecImpl( + check(Z3.mk_bvadd(contextPtr, arg0.ast, arg0.sort.cast(args[0]).ast)), + ) as unknown as T; + } else { + assert(arg0 instanceof ArithImpl); + return new ArithImpl( + check(Z3.mk_add(contextPtr, [arg0.ast].concat(args.map(arg => arg0.sort.cast(arg).ast)))), + ) as unknown as T; + } + } + + function Sub(arg0: Arith, ...args: CoercibleToArith[]): Arith; + function Sub( + arg0: BitVec, + ...args: CoercibleToBitVec[] + ): BitVec; + function Sub>(arg0: T, ...args: CoercibleToMap[]): T { + if (arg0 instanceof BitVecImpl) { + // Assert only 2 + if (args.length !== 1) { + throw new Error('BitVec sub only supports 2 arguments'); + } + return new BitVecImpl( + check(Z3.mk_bvsub(contextPtr, arg0.ast, arg0.sort.cast(args[0]).ast)), + ) as unknown as T; + } else { + assert(arg0 instanceof ArithImpl); + return new ArithImpl( + check(Z3.mk_sub(contextPtr, [arg0.ast].concat(args.map(arg => arg0.sort.cast(arg).ast)))), + ) as unknown as T; + } + } + + function Product(arg0: Arith, ...args: CoercibleToArith[]): Arith; + function Product( + arg0: BitVec, + ...args: CoercibleToBitVec[] + ): BitVec; + function Product>(arg0: T, ...args: CoercibleToMap[]): T { + if (arg0 instanceof BitVecImpl) { + // Assert only 2 + if (args.length !== 1) { + throw new Error('BitVec mul only supports 2 arguments'); + } + return new BitVecImpl( + check(Z3.mk_bvmul(contextPtr, arg0.ast, arg0.sort.cast(args[0]).ast)), + ) as unknown as T; + } else { + assert(arg0 instanceof ArithImpl); + return new ArithImpl( + check(Z3.mk_mul(contextPtr, [arg0.ast].concat(args.map(arg => arg0.sort.cast(arg).ast)))), + ) as unknown as T; + } + } + + function Div(arg0: Arith, arg1: CoercibleToArith): Arith; + function Div( + arg0: BitVec, + arg1: CoercibleToBitVec, + ): BitVec; + function Div>(arg0: T, arg1: CoercibleToMap): T { + if (arg0 instanceof BitVecImpl) { + return new BitVecImpl( + check(Z3.mk_bvsdiv(contextPtr, arg0.ast, arg0.sort.cast(arg1).ast)), + ) as unknown as T; + } else { + assert(arg0 instanceof ArithImpl); + return new ArithImpl(check(Z3.mk_div(contextPtr, arg0.ast, arg0.sort.cast(arg1).ast))) as unknown as T; + } + } + + function BUDiv( + arg0: BitVec, + arg1: CoercibleToBitVec, + ): BitVec { + return new BitVecImpl( + check(Z3.mk_bvudiv(contextPtr, arg0.ast, arg0.sort.cast(arg1).ast)), + ) as unknown as BitVec; + } + + function Neg(a: Arith): Arith; + function Neg(a: BitVec): BitVec; + function Neg>(a: T): T { + if (a instanceof BitVecImpl) { + return new BitVecImpl(check(Z3.mk_bvneg(contextPtr, a.ast))) as unknown as T; + } else { + assert(a instanceof ArithImpl); + return new ArithImpl(check(Z3.mk_unary_minus(contextPtr, a.ast))) as unknown as T; + } + } + + function Mod(a: Arith, b: CoercibleToArith): Arith; + function Mod(a: BitVec, b: CoercibleToBitVec): BitVec; + function Mod>(a: T, b: CoercibleToMap): T { + if (a instanceof BitVecImpl) { + return new BitVecImpl(check(Z3.mk_bvsrem(contextPtr, a.ast, a.sort.cast(b).ast))) as unknown as T; + } else { + assert(a instanceof ArithImpl); + return new ArithImpl(check(Z3.mk_mod(contextPtr, a.ast, a.sort.cast(b).ast))) as unknown as T; + } + } + 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]))); + add(other: CoercibleToArith) { + return Sum(this, other); } - mul(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(check(Z3.mk_mul(contextPtr, [this.ast, this.sort.cast(other).ast]))); + mul(other: CoercibleToArith) { + return Product(this, other); } - sub(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(check(Z3.mk_sub(contextPtr, [this.ast, this.sort.cast(other).ast]))); + sub(other: CoercibleToArith) { + return Sub(this, other); } - pow(exponent: Arith | number | bigint | string | CoercibleRational) { + pow(exponent: CoercibleToArith) { 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))); + div(other: CoercibleToArith) { + return Div(this, other); } - mod(other: Arith | number | bigint | string | CoercibleRational) { - return new ArithImpl(check(Z3.mk_mod(contextPtr, this.ast, this.sort.cast(other).ast))); + mod(other: CoercibleToArith) { + return Mod(this, other); } neg() { - return new ArithImpl(check(Z3.mk_unary_minus(contextPtr, this.ast))); + return Neg(this); } - le(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(check(Z3.mk_le(contextPtr, this.ast, this.sort.cast(other).ast))); + le(other: CoercibleToArith) { + return LE(this, other); } - lt(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(check(Z3.mk_lt(contextPtr, this.ast, this.sort.cast(other).ast))); + lt(other: CoercibleToArith) { + return LT(this, other); } - gt(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(check(Z3.mk_gt(contextPtr, this.ast, this.sort.cast(other).ast))); + gt(other: CoercibleToArith) { + return GT(this, other); } - ge(other: Arith | number | bigint | string | CoercibleRational) { - return new BoolImpl(check(Z3.mk_ge(contextPtr, this.ast, this.sort.cast(other).ast))); + ge(other: CoercibleToArith) { + return GE(this, other); } } @@ -1644,27 +2106,27 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } add(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvadd(contextPtr, this.ast, this.sort.cast(other).ast))); + return Sum(this, other); } mul(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvmul(contextPtr, this.ast, this.sort.cast(other).ast))); + return Product(this, other); } sub(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvsub(contextPtr, this.ast, this.sort.cast(other).ast))); + return Sub(this, other); } sdiv(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvsdiv(contextPtr, this.ast, this.sort.cast(other).ast))); + return Div(this, other); } udiv(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvudiv(contextPtr, this.ast, this.sort.cast(other).ast))); + return BUDiv(this, other); } smod(other: CoercibleToBitVec): BitVec { - return new BitVecImpl(check(Z3.mk_bvsmod(contextPtr, this.ast, this.sort.cast(other).ast))); + return Mod(this, other); } urem(other: CoercibleToBitVec): BitVec { @@ -1676,7 +2138,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } neg(): BitVec { - return new BitVecImpl(check(Z3.mk_bvneg(contextPtr, this.ast))); + return Neg(this); } or(other: CoercibleToBitVec): BitVec { @@ -1723,8 +2185,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { 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))); + extract(high: number, low: number): BitVec { + return Extract(high, low, this); } signExt(count: number): BitVec { @@ -1740,35 +2202,35 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } sle(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvsle(contextPtr, this.ast, this.sort.cast(other).ast))); + return SLE(this, other); } ule(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvule(contextPtr, this.ast, this.sort.cast(other).ast))); + return ULE(this, other); } slt(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvslt(contextPtr, this.ast, this.sort.cast(other).ast))); + return SLT(this, other); } ult(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvult(contextPtr, this.ast, this.sort.cast(other).ast))); + return ULT(this, other); } sge(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvsge(contextPtr, this.ast, this.sort.cast(other).ast))); + return SGE(this, other); } uge(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvuge(contextPtr, this.ast, this.sort.cast(other).ast))); + return UGE(this, other); } sgt(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvsgt(contextPtr, this.ast, this.sort.cast(other).ast))); + return SGT(this, other); } ugt(other: CoercibleToBitVec): Bool { - return new BoolImpl(check(Z3.mk_bvugt(contextPtr, this.ast, this.sort.cast(other).ast))); + return UGT(this, other); } redAnd(): BitVec { @@ -1840,10 +2302,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } - class ArraySortImpl, ...AnySort[]] = [Sort, ...Sort[]], - RangeSort extends AnySort = Sort> + class ArraySortImpl, RangeSort extends Sort> extends SortImpl - implements SMTArraySort { + implements SMTArraySort + { declare readonly __typename: SMTArraySort['__typename']; domain(): DomainSort[0] { @@ -1857,15 +2319,13 @@ export function createApi(Z3: Z3Core): Z3HighLevel { range(): RangeSort { return _toSort(check(Z3.get_array_sort_range(contextPtr, this.ptr))) as RangeSort; } - } - class ArrayImpl< - DomainSort extends [AnySort, ...AnySort[]] = [Sort, ...Sort[]], - RangeSort extends AnySort = Sort - > extends ExprImpl> - implements SMTArray { - declare readonly __typename: SMTArray['__typename']; + class ArrayImpl, RangeSort extends Sort> + extends ExprImpl> + implements SMTArray + { + declare readonly __typename: 'Array' | 'Lambda'; domain(): DomainSort[0] { return this.sort.domain(); @@ -1879,35 +2339,145 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return this.sort.range(); } - select(...indices: ArrayIndexType): SortToExprMap { - const args = indices.map((arg, i) => this.domain_n(i).cast(arg as any)); - if (args.length === 1) { - return _toExpr(check(Z3.mk_select(contextPtr, this.ast, args[0].ast))) as SortToExprMap; - } - const _args = args.map(arg => arg.ast); - return _toExpr(check(Z3.mk_select_n(contextPtr, this.ast, _args))) as SortToExprMap; + select(...indices: CoercibleToArrayIndexType): SortToExprMap { + return Select(this, ...indices) as SortToExprMap; } store( ...indicesAndValue: [ - ...ArrayIndexType, - CoercibleFromMap, Name> + ...CoercibleToArrayIndexType, + CoercibleToMap, Name>, ] ): SMTArray { - const args = indicesAndValue.map((arg, i) => { - if (i === indicesAndValue.length - 1) { - return this.range().cast(arg as CoercibleFromMap, Name>); - } - return this.domain_n(i).cast(arg as any); - }); - if (args.length <= 1) { - throw new Z3Error("Array store requires both index and value arguments"); - } - if (args.length === 2) { - return _toExpr(check(Z3.mk_store(contextPtr, this.ast, args[0].ast, args[1].ast))) as SMTArray; - } - const _idxs = args.slice(0, args.length - 1).map(arg => arg.ast); - return _toExpr(check(Z3.mk_store_n(contextPtr, this.ast, _idxs, args[args.length - 1].ast))) as SMTArray; + return Store(this, ...indicesAndValue); + } + } + + class QuantifierImpl< + QVarSorts extends NonEmptySortArray, + QSort extends BoolSort | SMTArraySort, + > + extends ExprImpl + implements Quantifier + { + declare readonly __typename: Quantifier['__typename']; + + is_forall(): boolean { + return Z3.is_quantifier_forall(contextPtr, this.ast); + } + + is_exists(): boolean { + return Z3.is_quantifier_exists(contextPtr, this.ast); + } + + is_lambda(): boolean { + return Z3.is_lambda(contextPtr, this.ast); + } + + weight(): number { + return Z3.get_quantifier_weight(contextPtr, this.ast); + } + + num_patterns(): number { + return Z3.get_quantifier_num_patterns(contextPtr, this.ast); + } + + pattern(i: number): Pattern { + return new PatternImpl(check(Z3.get_quantifier_pattern_ast(contextPtr, this.ast, i))); + } + + num_no_patterns(): number { + return Z3.get_quantifier_num_no_patterns(contextPtr, this.ast); + } + + no_pattern(i: number): Expr { + return _toExpr(check(Z3.get_quantifier_no_pattern_ast(contextPtr, this.ast, i))); + } + + body(): BodyT { + return _toExpr(check(Z3.get_quantifier_body(contextPtr, this.ast))) as any; + } + + num_vars(): number { + return Z3.get_quantifier_num_bound(contextPtr, this.ast); + } + + var_name(i: number): string | number { + return _fromSymbol(Z3.get_quantifier_bound_name(contextPtr, this.ast, i)); + } + + var_sort(i: T): QVarSorts[T] { + return _toSort(check(Z3.get_quantifier_bound_sort(contextPtr, this.ast, i))); + } + + children(): [BodyT] { + return [this.body()]; + } + } + + class NonLambdaQuantifierImpl> + extends QuantifierImpl> + implements Quantifier>, Bool + { + declare readonly __typename: 'NonLambdaQuantifier'; + + 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); + } + + implies(other: Bool | boolean): Bool { + return Implies(this, other); + } + + iff(other: Bool | boolean): Bool { + return Iff(this, other); + } + } + + // isBool will return false which is unlike the python API (but like the C API) + class LambdaImpl, RangeSort extends Sort> + extends QuantifierImpl> + implements + Quantifier>, + SMTArray + { + declare readonly __typename: 'Lambda'; + + domain(): DomainSort[0] { + return this.sort.domain(); + } + + domain_n(i: T): DomainSort[T] { + return this.sort.domain_n(i); + } + + range(): RangeSort { + return this.sort.range(); + } + + select(...indices: CoercibleToArrayIndexType): SortToExprMap { + return Select(this, ...indices); + } + + store( + ...indicesAndValue: [ + ...CoercibleToArrayIndexType, + CoercibleToMap, Name>, + ] + ): SMTArray { + return Store(this, ...indicesAndValue); } } @@ -1929,20 +2499,20 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return this.values(); } - * entries(): IterableIterator<[number, Item]> { + *entries(): IterableIterator<[number, Item]> { const length = this.length(); for (let i = 0; i < length; i++) { yield [i, this.get(i)]; } } - * keys(): IterableIterator { + *keys(): IterableIterator { for (let [key] of this.entries()) { yield key; } } - * values(): IterableIterator { + *values(): IterableIterator { for (let [, value] of this.entries()) { yield value; } @@ -2027,7 +2597,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return Z3.ast_map_size(contextPtr, this.ptr); } - * entries(): IterableIterator<[Key, Value]> { + *entries(): IterableIterator<[Key, Value]> { for (const key of this.keys()) { yield [key, this.get(key)]; } @@ -2037,7 +2607,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new AstVectorImpl(Z3.ast_map_keys(contextPtr, this.ptr)); } - * values(): IterableIterator { + *values(): IterableIterator { for (const [_, value] of this.entries()) { yield value; } @@ -2068,6 +2638,31 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + function substitute(t: Expr, ...substitutions: [Expr, Expr][]): Expr { + _assertContext(t); + const from: Z3_ast[] = []; + const to: Z3_ast[] = []; + for (const [f, t] of substitutions) { + _assertContext(f); + _assertContext(t); + from.push(f.ast); + to.push(t.ast); + } + return _toExpr(check(Z3.substitute(contextPtr, t.ast, from, to))); + } + + function ast_from_string(s: string): Ast { + const sort_names: Z3_symbol[] = []; + const sorts: Z3_sort[] = []; + const decl_names: Z3_symbol[] = []; + const decls: Z3_func_decl[] = []; + const v = new AstVectorImpl(check(Z3.parse_smtlib2_string(contextPtr, s, sort_names, sorts, decl_names, decls))); + if (v.length() !== 1) { + throw new Error('Expected exactly one AST. Instead got ' + v.length() + ': ' + v.sexpr()); + } + return v.get(0); + } + const ctx: Context = { ptr: contextPtr, name, @@ -2089,6 +2684,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { isAst, isSort, isFuncDecl, + isFuncInterp, isApp, isConst, isExpr, @@ -2103,6 +2699,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { isNot, isEq, isDistinct, + isQuantifier, isArith, isArithSort, isInt, @@ -2147,11 +2744,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel { FreshConst, Var, Implies, + Iff, Eq, Xor, Not, And, Or, + ForAll, + Exists, + Lambda, ToReal, ToInt, IsInt, @@ -2161,6 +2762,36 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Int2BV, Concat, Cond, + LT, + GT, + LE, + GE, + ULT, + UGT, + ULE, + UGE, + SLT, + SGT, + SLE, + SGE, + Sum, + Sub, + Product, + Div, + BUDiv, + Neg, + Mod, + Select, + Store, + Extract, + + substitute, + simplify, + + ///////////// + // Loading // + ///////////// + ast_from_string, }; cleanup.register(ctx, () => Z3.del_context(contextPtr)); return ctx; diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index a6cb01e79..c4b560442 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -5,13 +5,13 @@ import { Z3_context, Z3_decl_kind, Z3_func_decl, + Z3_func_entry, Z3_func_interp, Z3_model, Z3_probe, Z3_solver, Z3_sort, Z3_sort_kind, - Z3_symbol, Z3_tactic, } from '../low-level'; @@ -21,7 +21,7 @@ export type AnySort = | BoolSort | ArithSort | BitVecSort - | SMTArraySort, ...AnySort[]], AnySort>; + | SMTArraySort; /** @hidden */ export type AnyExpr = | Expr @@ -31,53 +31,64 @@ export type AnyExpr = | RatNum | BitVec | BitVecNum - | SMTArray, ...AnySort[]], AnySort>; + | SMTArray; /** @hidden */ export type AnyAst = AnyExpr | AnySort | FuncDecl; /** @hidden */ -export type SortToExprMap, Name extends string = 'main'> = - S extends BoolSort - ? Bool - : S extends ArithSort - ? Arith - : S extends BitVecSort - ? BitVec - : S extends SMTArraySort - ? SMTArray - : S extends Sort - ? Expr - : never; +export type SortToExprMap, Name extends string = 'main'> = S extends BoolSort + ? Bool + : S extends ArithSort + ? Arith + : S extends BitVecSort + ? BitVec + : S extends SMTArraySort + ? SMTArray + : S extends Sort + ? Expr + : never; /** @hidden */ -export type CoercibleToExprMap, Name extends string = 'main'> = - S extends bigint - ? ArithSort - : S extends number | CoercibleRational - ? RatNum - : S extends boolean - ? Bool - : S extends Expr - ? S - : never; +export type CoercibleFromMap, Name extends string = 'main'> = S extends bigint + ? Arith + : S extends number | CoercibleRational + ? RatNum + : S extends boolean + ? Bool + : S extends Expr + ? S + : never; /** @hidden */ -export type CoercibleFromMap, Name extends string = 'main'> = - S extends Bool - ? (boolean | Bool) - : S extends IntNum - ? (bigint | number | IntNum) - : S extends RatNum - ? (bigint | number | CoercibleRational | RatNum) - : S extends Arith - ? (bigint | number | CoercibleRational | Arith) - : S extends BitVec - ? (number | BitVec) - : S extends SMTArray - ? SMTArray - : S extends Expr - ? Expr - : never; +export type CoercibleToBitVec = + | bigint + | number + | BitVec; + +export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number }; + +/** @hidden */ +export type CoercibleToExpr = number | bigint | boolean | CoercibleRational | Expr; + +/** @hidden */ +export type CoercibleToArith = number | string | bigint | CoercibleRational | Arith; + +/** @hidden */ +export type CoercibleToMap, Name extends string = 'main'> = T extends Bool + ? boolean | Bool + : T extends IntNum + ? bigint | number | IntNum + : T extends RatNum + ? bigint | number | CoercibleRational | RatNum + : T extends Arith + ? CoercibleToArith + : T extends BitVec + ? CoercibleToBitVec + : T extends SMTArray + ? SMTArray + : T extends Expr + ? Expr + : never; /** * Used to create a Real constant @@ -97,16 +108,10 @@ export type CoercibleFromMap, Name extends string = 'mai * @see {@link Context.from} * @category Global */ -export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number }; -/** @hidden */ -export type CoercibleToExpr = number | bigint | boolean | CoercibleRational | Expr; +export class Z3Error extends Error {} -export class Z3Error extends Error { -} - -export class Z3AssertionError extends Z3Error { -} +export class Z3AssertionError extends Z3Error {} /** @category Global */ export type CheckSatResult = 'sat' | 'unsat' | 'unknown'; @@ -149,6 +154,9 @@ export interface Context { /** @category Functions */ isFuncDecl(obj: unknown): obj is FuncDecl; + /** @category Functions */ + isFuncInterp(obj: unknown): obj is FuncInterp; + /** @category Functions */ isApp(obj: unknown): boolean; @@ -191,6 +199,9 @@ export interface Context { /** @category Functions */ isDistinct(obj: unknown): boolean; + /** @category Functions */ + isQuantifier(obj: unknown): obj is Quantifier; + /** @category Functions */ isArith(obj: unknown): obj is Arith; @@ -225,10 +236,10 @@ export interface Context { isBitVecVal(obj: unknown): obj is BitVecNum; /** @category Functions */ - isArraySort(obj: unknown): obj is SMTArraySort, ...AnySort[]], AnySort>; + isArraySort(obj: unknown): obj is SMTArraySort; /** @category Functions */ - isArray(obj: unknown): obj is SMTArray, ...AnySort[]], AnySort>; + isArray(obj: unknown): obj is SMTArray; /** @category Functions */ isConstArray(obj: unknown): boolean; @@ -315,7 +326,11 @@ export interface Context { /** @category Classes */ readonly AstVector: new = AnyAst>() => AstVector; /** @category Classes */ - readonly AstMap: new = AnyAst, Value extends Ast = AnyAst>() => AstMap; + readonly AstMap: new = AnyAst, Value extends Ast = AnyAst>() => AstMap< + Name, + Key, + Value + >; /** @category Classes */ readonly Tactic: new (name: string) => Tactic; @@ -363,7 +378,7 @@ export interface Context { condition: Bool | boolean, onTrue: OnTrueRef, onFalse: OnFalseRef, - ): CoercibleToExprMap; + ): CoercibleFromMap; /** @category Operations */ Distinct(...args: CoercibleToExpr[]): Bool; @@ -371,6 +386,9 @@ export interface Context { /** @category Operations */ Implies(a: Bool | boolean, b: Bool | boolean): Bool; + /** @category Operations */ + Iff(a: Bool | boolean, b: Bool | boolean): Bool; + /** @category Operations */ Eq(a: CoercibleToExpr, b: CoercibleToExpr): Bool; @@ -407,6 +425,28 @@ export interface Context { /** @category Operations */ Or(...args: Probe[]): Probe; + // Quantifiers + + /** @category Operations */ + ForAll>( + quantifiers: ArrayIndexType, + body: Bool, + weight?: number, + ): Quantifier> & Bool; + + /** @category Operations */ + Exists>( + quantifiers: ArrayIndexType, + body: Bool, + weight?: number, + ): Quantifier> & Bool; + + /** @category Operations */ + Lambda, RangeSort extends Sort>( + quantifiers: ArrayIndexType, + expr: SortToExprMap, + ): Quantifier> & SMTArray; + // Arithmetic /** @category Operations */ ToReal(expr: Arith | bigint): Arith; @@ -437,7 +477,7 @@ export interface Context { * // a**(1/2) * ``` * @category Operations */ - Sqrt(a: Arith | number | bigint | string | CoercibleRational): Arith; + Sqrt(a: CoercibleToArith): Arith; /** * Returns a Z3 expression representing cubic root of a @@ -449,7 +489,7 @@ export interface Context { * // a**(1/3) * ``` * @category Operations */ - Cbrt(a: Arith | number | bigint | string | CoercibleRational): Arith; + Cbrt(a: CoercibleToArith): Arith; // Bit Vectors /** @category Operations */ @@ -462,7 +502,102 @@ export interface Context { Concat(...bitvecs: BitVec[]): BitVec; /** @category Operations */ - Cond(probe: Probe, onTrue: Tactic, onFalse: Tactic): Tactic + Cond(probe: Probe, onTrue: Tactic, onFalse: Tactic): Tactic; + + // Arith + + /** @category Operations */ + LT(a: Arith, b: CoercibleToArith): Bool; + + /** @category Operations */ + GT(a: Arith, b: CoercibleToArith): Bool; + + /** @category Operations */ + LE(a: Arith, b: CoercibleToArith): Bool; + + /** @category Operations */ + GE(a: Arith, b: CoercibleToArith): Bool; + + // Bit Vectors + + /** @category Operations */ + ULT(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + UGT(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + ULE(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + UGE(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + SLT(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + SGT(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + SGE(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + SLE(a: BitVec, b: CoercibleToBitVec): Bool; + + /** @category Operations */ + Sum(arg0: Arith, ...args: CoercibleToArith[]): Arith; + + Sum(arg0: BitVec, ...args: CoercibleToBitVec[]): BitVec; + + Sub(arg0: Arith, ...args: CoercibleToArith[]): Arith; + + Sub(arg0: BitVec, ...args: CoercibleToBitVec[]): BitVec; + + Product(arg0: Arith, ...args: CoercibleToArith[]): Arith; + + Product(arg0: BitVec, ...args: CoercibleToBitVec[]): BitVec; + + Div(arg0: Arith, arg1: CoercibleToArith): Arith; + + Div(arg0: BitVec, arg1: CoercibleToBitVec): BitVec; + + BUDiv(arg0: BitVec, arg1: CoercibleToBitVec): BitVec; + + Neg(a: Arith): Arith; + + Neg(a: BitVec): BitVec; + + Mod(a: Arith, b: CoercibleToArith): Arith; + + Mod(a: BitVec, b: CoercibleToBitVec): BitVec; + + // Arrays + + /** @category Operations */ + Select, RangeSort extends Sort = Sort>( + array: SMTArray, + ...indices: CoercibleToArrayIndexType + ): SortToExprMap; + + /** @category Operations */ + Store, RangeSort extends Sort = Sort>( + array: SMTArray, + ...indicesAndValue: [ + ...CoercibleToArrayIndexType, + CoercibleToMap, Name>, + ] + ): SMTArray; + + /** @category Operations */ + Extract(hi: number, lo: number, val: BitVec): BitVec; + + /** @category Operations */ + ast_from_string(s: string): Ast; + + /** @category Operations */ + substitute(t: Expr, ...substitutions: [Expr, Expr][]): Expr; + + simplify(expr: Expr): Promise>; } export interface Ast { @@ -490,7 +625,7 @@ export interface Ast { /** @hidden */ export interface SolverCtor { - new(): Solver; + new (): Solver; } export interface Solver { @@ -500,10 +635,11 @@ export interface Solver { readonly ctx: Context; readonly ptr: Z3_solver; - /* TODO(ritave): Decide on how to discern between integer and float parameters set(key: string, value: any): void; - set(params: Record): void; - */ + + /* TODO(ritave): Decide on how to discern between integer and float parameters + set(params: Record): void; + */ push(): void; pop(num?: number): void; @@ -527,7 +663,7 @@ export interface Solver { /** @hidden */ export interface ModelCtor { - new(): Model; + new (): Model; } export interface Model extends Iterable> { @@ -566,6 +702,13 @@ export interface Model extends Iterable): Expr; get(sort: Sort): AstVector>; + + updateValue(decl: FuncDecl | Expr, a: Ast | FuncInterp): void; + + addFuncInterp[] = Sort[], RangeSort extends Sort = Sort>( + decl: FuncDecl, + defaultValue: CoercibleToMap, Name>, + ): FuncInterp; } /** @@ -608,6 +751,23 @@ export interface Sort extends Ast { name(): string | number; } +/** + * @category Functions + */ +export interface FuncEntry { + /** @hidden */ + readonly __typename: 'FuncEntry'; + + readonly ctx: Context; + readonly ptr: Z3_func_entry; + + numArgs(): number; + + argValue(i: number): Expr; + + value(): Expr; +} + /** * @category Functions */ @@ -617,6 +777,16 @@ export interface FuncInterp { readonly ctx: Context; readonly ptr: Z3_func_interp; + + elseValue(): Expr; + + numEntries(): number; + + arity(): number; + + entry(i: number): FuncEntry; + + addEntry(args: Expr[], value: Expr): void; } /** @hidden */ @@ -639,9 +809,14 @@ export interface FuncDeclCreation { * @param name Name of the function * @param signature The domains, and last parameter - the range of the function */ - declare(name: string, ...signature: FuncDeclSignature): FuncDecl; + declare[], RangeSort extends Sort>( + name: string, + ...signature: [...DomainSort, RangeSort] + ): FuncDecl; - fresh(...signature: FuncDeclSignature): FuncDecl; + fresh[], RangeSort extends Sort>( + ...signature: [...DomainSort, RangeSort] + ): FuncDecl; } /** @@ -656,7 +831,11 @@ export interface RecFuncCreation { /** * @category Functions */ -export interface FuncDecl extends Ast { +export interface FuncDecl< + Name extends string = 'main', + DomainSort extends Sort[] = Sort[], + RangeSort extends Sort = Sort, +> extends Ast { /** @hidden */ readonly __typename: 'FuncDecl'; @@ -664,21 +843,26 @@ export interface FuncDecl extends Ast; + domain(i: T): DomainSort[T]; - range(): Sort; + range(): RangeSort; kind(): Z3_decl_kind; - params(): (number | string | Z3_symbol | Sort | Expr | FuncDecl)[]; + params(): (number | string | Sort | Expr | FuncDecl)[]; - call(...args: CoercibleToExpr[]): AnyExpr; + call(...args: CoercibleToArrayIndexType): SortToExprMap; } export interface Expr = AnySort, Ptr = unknown> extends Ast { /** @hidden */ - readonly __typename: 'Expr' | Bool['__typename'] | Arith['__typename'] | BitVec['__typename'] | SMTArray['__typename']; + readonly __typename: + | 'Expr' + | Bool['__typename'] + | Arith['__typename'] + | BitVec['__typename'] + | SMTArray['__typename']; get sort(): S; @@ -688,6 +872,8 @@ export interface Expr = AnySo params(): ReturnType['params']>; + name(): ReturnType['name']>; + decl(): FuncDecl; numArgs(): number; @@ -725,7 +911,7 @@ export interface BoolCreation { /** @category Booleans */ export interface Bool extends Expr, Z3_ast> { /** @hidden */ - readonly __typename: 'Bool'; + readonly __typename: 'Bool' | 'NonLambdaQuantifier'; not(): Bool; @@ -738,6 +924,13 @@ export interface Bool extends Expr | boolean): Bool; } +// TODO: properly implement pattern +/** @category Quantifiers */ +export interface Pattern { + /** @hidden */ + readonly __typename: 'Pattern'; +} + /** * A Sort that represents Integers or Real numbers * @category Arithmetic @@ -798,17 +991,17 @@ export interface Arith extends Expr | number | bigint | string): Arith; + add(other: CoercibleToArith): Arith; /** * Multiplies two numbers together */ - mul(other: Arith | number | bigint | string): Arith; + mul(other: CoercibleToArith): Arith; /** * Subtract second number from the first one */ - sub(other: Arith | number | bigint | string): Arith; + sub(other: CoercibleToArith): Arith; /** * Applies power to the number @@ -820,12 +1013,12 @@ export interface Arith extends Expr | number | bigint | string): Arith; + pow(exponent: CoercibleToArith): Arith; /** * Divides the number by the second one */ - div(other: Arith | number | bigint | string): Arith; + div(other: CoercibleToArith): Arith; /** * Returns a number modulo second one @@ -837,7 +1030,7 @@ export interface Arith extends Expr | number | bigint | string): Arith; + mod(other: CoercibleToArith): Arith; /** * Returns a negation of the number @@ -847,22 +1040,22 @@ export interface Arith extends Expr | number | bigint | string): Bool; + le(other: CoercibleToArith): Bool; /** * Returns whether the number is less than the second one (`<`) */ - lt(other: Arith | number | bigint | string): Bool; + lt(other: CoercibleToArith): Bool; /** * Returns whether the number is greater than the second one (`>`) */ - gt(other: Arith | number | bigint | string): Bool; + gt(other: CoercibleToArith): Bool; /** * Returns whether the number is greater or equal than the second one (`>=`) */ - ge(other: Arith | number | bigint | string): Bool; + ge(other: CoercibleToArith): Bool; } /** @@ -939,12 +1132,6 @@ export interface BitVecSort): Expr; } -/** @hidden */ -export type CoercibleToBitVec = - | bigint - | number - | BitVec; - /** @category Bit Vectors */ export interface BitVecCreation { sort(bits: Bits): BitVecSort; @@ -1213,10 +1400,11 @@ export interface BitVecNum, ...AnySort[]] = [Sort, ...Sort[]], +export interface SMTArraySort< + Name extends string = 'main', + DomainSort extends NonEmptySortArray = [Sort, ...Sort[]], RangeSort extends AnySort = AnySort, - > extends Sort { +> extends Sort { /** @hidden */ readonly __typename: 'ArraySort'; @@ -1236,36 +1424,47 @@ export interface SMTArraySort { - sort, ...AnySort[]], RangeSort extends AnySort>( + sort, RangeSort extends Sort>( ...sig: [...DomainSort, RangeSort] ): SMTArraySort; - const, ...AnySort[]], RangeSort extends AnySort>( - name: string, ...sig: [...DomainSort, RangeSort] + const, RangeSort extends Sort>( + name: string, + ...sig: [...DomainSort, RangeSort] ): SMTArray; - consts, ...AnySort[]], RangeSort extends AnySort>( + consts, RangeSort extends Sort>( names: string | string[], ...sig: [...DomainSort, RangeSort] ): SMTArray[]; K, RangeSort extends AnySort>( domain: DomainSort, - value: SortToExprMap + value: SortToExprMap, ): SMTArray; } -export type ArrayIndexType, ...AnySort[]] = [Sort, ...Sort[]]> = [...{ - [Index in keyof DomainSort]: DomainSort[Index] extends AnySort ? - CoercibleFromMap, Name> : - DomainSort[Index]; -}] +export type NonEmptySortArray = [Sort, ...Array>]; + +export type ArrayIndexType[]> = [ + ...{ + [Key in keyof DomainSort]: DomainSort[Key] extends AnySort + ? SortToExprMap + : DomainSort[Key]; + }, +]; + +export type CoercibleToArrayIndexType[]> = [ + ...{ + [Key in keyof DomainSort]: DomainSort[Key] extends AnySort + ? CoercibleToMap, Name> + : DomainSort[Key]; + }, +]; /** * Represents Array expression @@ -1274,13 +1473,13 @@ export type ArrayIndexType, ...AnySort[]] = [Sort, ...Sort[]], - RangeSort extends AnySort = AnySort> - extends Expr, Z3_ast> { - +export interface SMTArray< + Name extends string = 'main', + DomainSort extends NonEmptySortArray = [Sort, ...Sort[]], + RangeSort extends Sort = Sort, +> extends Expr, Z3_ast> { /** @hidden */ - readonly __typename: 'Array'; + readonly __typename: 'Array' | 'Lambda'; domain(): DomainSort[0]; @@ -1288,7 +1487,7 @@ export interface SMTArray): SortToExprMap; + select(...indices: CoercibleToArrayIndexType): SortToExprMap; /** * value should be coercible to RangeSort @@ -1297,11 +1496,60 @@ export interface SMTArray, - CoercibleFromMap, Name> + ...CoercibleToArrayIndexType, + CoercibleToMap, Name>, ] ): SMTArray; +} +/** + * Defines the expression type of the body of a quantifier expression + * + * @category Quantifiers + */ +export type BodyT< + Name extends string = 'main', + QVarSorts extends NonEmptySortArray = [Sort, ...Sort[]], + QSort extends BoolSort | SMTArraySort = BoolSort | SMTArraySort, +> = QSort extends BoolSort + ? Bool + : QSort extends SMTArray + ? SortToExprMap + : never; + +/** @category Quantifiers */ +export interface Quantifier< + Name extends string = 'main', + QVarSorts extends NonEmptySortArray = [Sort, ...Sort[]], + QSort extends BoolSort | SMTArraySort = BoolSort | SMTArraySort, +> extends Expr { + readonly __typename: 'NonLambdaQuantifier' | 'Lambda'; + + is_forall(): boolean; + + is_exists(): boolean; + + is_lambda(): boolean; + + weight(): number; + + num_patterns(): number; + + pattern(i: number): Pattern; + + num_no_patterns(): number; + + no_pattern(i: number): Expr; + + body(): BodyT; + + num_vars(): number; + + var_name(i: number): string | number; + + var_sort(i: T): QVarSorts[T]; + + children(): [BodyT]; } export interface Probe { @@ -1314,7 +1562,7 @@ export interface Probe { /** @hidden */ export interface TacticCtor { - new(name: string): Tactic; + new (name: string): Tactic; } export interface Tactic { @@ -1327,7 +1575,7 @@ export interface Tactic { /** @hidden */ export interface AstVectorCtor { - new = AnyAst>(): AstVector; + new = AnyAst>(): AstVector; } /** @@ -1378,7 +1626,7 @@ export interface AstVector /** @hidden */ export interface AstMapCtor { - new = AnyAst, Value extends Ast = AnyAst>(): AstMap; + new = AnyAst, Value extends Ast = AnyAst>(): AstMap; } /** @@ -1402,8 +1650,11 @@ export interface AstMapCtor { * // 0 * ``` */ -export interface AstMap = AnyAst, Value extends Ast = AnyAst> - extends Iterable<[Key, Value]> { +export interface AstMap< + Name extends string = 'main', + Key extends Ast = AnyAst, + Value extends Ast = AnyAst, +> extends Iterable<[Key, Value]> { /** @hidden */ readonly __typename: 'AstMap';