mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
[WIP] More TS Binding Features (#6412)
* feat: basic quantfier support * feat: added isQuantifier * feat: expanded functions * wip: (lambda broken) * temp fix to LambdaImpl typing issue * feat: function type inference * formatting with prettier * fix: imported from invalid module * fix isBool bug and dumping to smtlib * substitution and model.updateValue * api to add custom func interps to model * fix: building * properly handling uint32 -> number conversion in z3 TS wrapper * added simplify * remame Add->Sum and Mul->Product * formatting
This commit is contained in:
Walden Yan
GitHub
parent
5e30323b1a
commit
ede9e5ffc2
9 changed files with 1383 additions and 332 deletions
36
src/api/js/examples/high-level/using_smtlib2.ts
Normal file
36
src/api/js/examples/high-level/using_smtlib2.ts
Normal file
|
|
@ -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);
|
||||
});
|
||||
|
|
@ -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';
|
||||
|
||||
|
|
|
|||
44
src/api/js/package-lock.json
generated
44
src/api/js/package-lock.json
generated
|
|
@ -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": {
|
||||
|
|
|
|||
|
|
@ -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": {
|
||||
|
|
|
|||
|
|
@ -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})`;
|
||||
|
|
|
|||
|
|
@ -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',
|
||||
|
|
|
|||
|
|
@ -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<Name extends string>(...assertions: Bool<Name>[]):
|
|||
|
||||
async function prove(conjecture: Bool): Promise<void> {
|
||||
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<Bool>(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<Arith>();
|
||||
const vector = new Z3.AstVector<Arith>();
|
||||
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();
|
||||
});
|
||||
});
|
||||
});
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
|
|
@ -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<Name extends string = 'main'> =
|
|||
| BoolSort<Name>
|
||||
| ArithSort<Name>
|
||||
| BitVecSort<number, Name>
|
||||
| SMTArraySort<Name, [AnySort<Name>, ...AnySort<Name>[]], AnySort<Name>>;
|
||||
| SMTArraySort<Name>;
|
||||
/** @hidden */
|
||||
export type AnyExpr<Name extends string = 'main'> =
|
||||
| Expr<Name>
|
||||
|
|
@ -31,53 +31,64 @@ export type AnyExpr<Name extends string = 'main'> =
|
|||
| RatNum<Name>
|
||||
| BitVec<number, Name>
|
||||
| BitVecNum<number, Name>
|
||||
| SMTArray<Name, [AnySort<Name>, ...AnySort<Name>[]], AnySort<Name>>;
|
||||
| SMTArray<Name>;
|
||||
/** @hidden */
|
||||
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
|
||||
|
||||
/** @hidden */
|
||||
export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'> =
|
||||
S extends BoolSort
|
||||
? Bool<Name>
|
||||
: S extends ArithSort<Name>
|
||||
? Arith<Name>
|
||||
: S extends BitVecSort<infer Size, Name>
|
||||
? BitVec<Size, Name>
|
||||
: S extends SMTArraySort<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: S extends Sort<Name>
|
||||
? Expr<Name, S, Z3_ast>
|
||||
: never;
|
||||
export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'> = S extends BoolSort
|
||||
? Bool<Name>
|
||||
: S extends ArithSort<Name>
|
||||
? Arith<Name>
|
||||
: S extends BitVecSort<infer Size, Name>
|
||||
? BitVec<Size, Name>
|
||||
: S extends SMTArraySort<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: S extends Sort<Name>
|
||||
? Expr<Name, S, Z3_ast>
|
||||
: never;
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToExprMap<S extends CoercibleToExpr<Name>, Name extends string = 'main'> =
|
||||
S extends bigint
|
||||
? ArithSort<Name>
|
||||
: S extends number | CoercibleRational
|
||||
? RatNum<Name>
|
||||
: S extends boolean
|
||||
? Bool<Name>
|
||||
: S extends Expr<Name>
|
||||
? S
|
||||
: never;
|
||||
export type CoercibleFromMap<S extends CoercibleToExpr<Name>, Name extends string = 'main'> = S extends bigint
|
||||
? Arith<Name>
|
||||
: S extends number | CoercibleRational
|
||||
? RatNum<Name>
|
||||
: S extends boolean
|
||||
? Bool<Name>
|
||||
: S extends Expr<Name>
|
||||
? S
|
||||
: never;
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleFromMap<S extends AnyExpr<Name>, Name extends string = 'main'> =
|
||||
S extends Bool<Name>
|
||||
? (boolean | Bool<Name>)
|
||||
: S extends IntNum<Name>
|
||||
? (bigint | number | IntNum<Name>)
|
||||
: S extends RatNum<Name>
|
||||
? (bigint | number | CoercibleRational | RatNum<Name>)
|
||||
: S extends Arith<Name>
|
||||
? (bigint | number | CoercibleRational | Arith<Name>)
|
||||
: S extends BitVec<infer Size, Name>
|
||||
? (number | BitVec<Size, Name>)
|
||||
: S extends SMTArray<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: S extends Expr<Name>
|
||||
? Expr<Name>
|
||||
: never;
|
||||
export type CoercibleToBitVec<Bits extends number = number, Name extends string = 'main'> =
|
||||
| bigint
|
||||
| number
|
||||
| BitVec<Bits, Name>;
|
||||
|
||||
export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToExpr<Name extends string = 'main'> = number | bigint | boolean | CoercibleRational | Expr<Name>;
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToArith<Name extends string = 'main'> = number | string | bigint | CoercibleRational | Arith<Name>;
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToMap<T extends AnyExpr<Name>, Name extends string = 'main'> = T extends Bool<Name>
|
||||
? boolean | Bool<Name>
|
||||
: T extends IntNum<Name>
|
||||
? bigint | number | IntNum<Name>
|
||||
: T extends RatNum<Name>
|
||||
? bigint | number | CoercibleRational | RatNum<Name>
|
||||
: T extends Arith<Name>
|
||||
? CoercibleToArith<Name>
|
||||
: T extends BitVec<infer Size, Name>
|
||||
? CoercibleToBitVec<Size, Name>
|
||||
: T extends SMTArray<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: T extends Expr<Name>
|
||||
? Expr<Name>
|
||||
: never;
|
||||
|
||||
/**
|
||||
* Used to create a Real constant
|
||||
|
|
@ -97,16 +108,10 @@ export type CoercibleFromMap<S extends AnyExpr<Name>, Name extends string = 'mai
|
|||
* @see {@link Context.from}
|
||||
* @category Global
|
||||
*/
|
||||
export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToExpr<Name extends string = 'main'> = number | bigint | boolean | CoercibleRational | Expr<Name>;
|
||||
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<Name extends string = 'main'> {
|
|||
/** @category Functions */
|
||||
isFuncDecl(obj: unknown): obj is FuncDecl<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isFuncInterp(obj: unknown): obj is FuncInterp<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isApp(obj: unknown): boolean;
|
||||
|
||||
|
|
@ -191,6 +199,9 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Functions */
|
||||
isDistinct(obj: unknown): boolean;
|
||||
|
||||
/** @category Functions */
|
||||
isQuantifier(obj: unknown): obj is Quantifier<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isArith(obj: unknown): obj is Arith<Name>;
|
||||
|
||||
|
|
@ -225,10 +236,10 @@ export interface Context<Name extends string = 'main'> {
|
|||
isBitVecVal(obj: unknown): obj is BitVecNum<number, Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isArraySort(obj: unknown): obj is SMTArraySort<Name, [AnySort<Name>, ...AnySort<Name>[]], AnySort<Name>>;
|
||||
isArraySort(obj: unknown): obj is SMTArraySort<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isArray(obj: unknown): obj is SMTArray<Name, [AnySort<Name>, ...AnySort<Name>[]], AnySort<Name>>;
|
||||
isArray(obj: unknown): obj is SMTArray<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isConstArray(obj: unknown): boolean;
|
||||
|
|
@ -315,7 +326,11 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Classes */
|
||||
readonly AstVector: new <Item extends Ast<Name> = AnyAst<Name>>() => AstVector<Name, Item>;
|
||||
/** @category Classes */
|
||||
readonly AstMap: new <Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>() => AstMap<Name, Key, Value>;
|
||||
readonly AstMap: new <Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>() => AstMap<
|
||||
Name,
|
||||
Key,
|
||||
Value
|
||||
>;
|
||||
/** @category Classes */
|
||||
readonly Tactic: new (name: string) => Tactic<Name>;
|
||||
|
||||
|
|
@ -363,7 +378,7 @@ export interface Context<Name extends string = 'main'> {
|
|||
condition: Bool<Name> | boolean,
|
||||
onTrue: OnTrueRef,
|
||||
onFalse: OnFalseRef,
|
||||
): CoercibleToExprMap<OnTrueRef | OnFalseRef, Name>;
|
||||
): CoercibleFromMap<OnTrueRef | OnFalseRef, Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Distinct(...args: CoercibleToExpr<Name>[]): Bool<Name>;
|
||||
|
|
@ -371,6 +386,9 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Operations */
|
||||
Implies(a: Bool<Name> | boolean, b: Bool<Name> | boolean): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Iff(a: Bool<Name> | boolean, b: Bool<Name> | boolean): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Eq(a: CoercibleToExpr<Name>, b: CoercibleToExpr<Name>): Bool<Name>;
|
||||
|
||||
|
|
@ -407,6 +425,28 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Operations */
|
||||
Or(...args: Probe<Name>[]): Probe<Name>;
|
||||
|
||||
// Quantifiers
|
||||
|
||||
/** @category Operations */
|
||||
ForAll<QVarSorts extends NonEmptySortArray<Name>>(
|
||||
quantifiers: ArrayIndexType<Name, QVarSorts>,
|
||||
body: Bool<Name>,
|
||||
weight?: number,
|
||||
): Quantifier<Name, QVarSorts, BoolSort<Name>> & Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Exists<QVarSorts extends NonEmptySortArray<Name>>(
|
||||
quantifiers: ArrayIndexType<Name, QVarSorts>,
|
||||
body: Bool<Name>,
|
||||
weight?: number,
|
||||
): Quantifier<Name, QVarSorts, BoolSort<Name>> & Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Lambda<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>(
|
||||
quantifiers: ArrayIndexType<Name, DomainSort>,
|
||||
expr: SortToExprMap<RangeSort, Name>,
|
||||
): Quantifier<Name, DomainSort, SMTArraySort<Name, DomainSort, RangeSort>> & SMTArray<Name, DomainSort, RangeSort>;
|
||||
|
||||
// Arithmetic
|
||||
/** @category Operations */
|
||||
ToReal(expr: Arith<Name> | bigint): Arith<Name>;
|
||||
|
|
@ -437,7 +477,7 @@ export interface Context<Name extends string = 'main'> {
|
|||
* // a**(1/2)
|
||||
* ```
|
||||
* @category Operations */
|
||||
Sqrt(a: Arith<Name> | number | bigint | string | CoercibleRational): Arith<Name>;
|
||||
Sqrt(a: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Returns a Z3 expression representing cubic root of a
|
||||
|
|
@ -449,7 +489,7 @@ export interface Context<Name extends string = 'main'> {
|
|||
* // a**(1/3)
|
||||
* ```
|
||||
* @category Operations */
|
||||
Cbrt(a: Arith<Name> | number | bigint | string | CoercibleRational): Arith<Name>;
|
||||
Cbrt(a: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
// Bit Vectors
|
||||
/** @category Operations */
|
||||
|
|
@ -462,7 +502,102 @@ export interface Context<Name extends string = 'main'> {
|
|||
Concat(...bitvecs: BitVec<number, Name>[]): BitVec<number, Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Cond(probe: Probe<Name>, onTrue: Tactic<Name>, onFalse: Tactic<Name>): Tactic<Name>
|
||||
Cond(probe: Probe<Name>, onTrue: Tactic<Name>, onFalse: Tactic<Name>): Tactic<Name>;
|
||||
|
||||
// Arith
|
||||
|
||||
/** @category Operations */
|
||||
LT(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
GT(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
LE(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
GE(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
// Bit Vectors
|
||||
|
||||
/** @category Operations */
|
||||
ULT<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
UGT<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
ULE<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
UGE<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
SLT<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
SGT<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
SGE<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
SLE<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Sum(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
|
||||
|
||||
Sum<Bits extends number>(arg0: BitVec<Bits, Name>, ...args: CoercibleToBitVec<Bits, Name>[]): BitVec<Bits, Name>;
|
||||
|
||||
Sub(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
|
||||
|
||||
Sub<Bits extends number>(arg0: BitVec<Bits, Name>, ...args: CoercibleToBitVec<Bits, Name>[]): BitVec<Bits, Name>;
|
||||
|
||||
Product(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
|
||||
|
||||
Product<Bits extends number>(arg0: BitVec<Bits, Name>, ...args: CoercibleToBitVec<Bits, Name>[]): BitVec<Bits, Name>;
|
||||
|
||||
Div(arg0: Arith<Name>, arg1: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
Div<Bits extends number>(arg0: BitVec<Bits, Name>, arg1: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
|
||||
|
||||
BUDiv<Bits extends number>(arg0: BitVec<Bits, Name>, arg1: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
|
||||
|
||||
Neg(a: Arith<Name>): Arith<Name>;
|
||||
|
||||
Neg<Bits extends number>(a: BitVec<Bits, Name>): BitVec<Bits, Name>;
|
||||
|
||||
Mod(a: Arith<Name>, b: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
Mod<Bits extends number>(a: BitVec<Bits, Name>, b: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
|
||||
|
||||
// Arrays
|
||||
|
||||
/** @category Operations */
|
||||
Select<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name> = Sort<Name>>(
|
||||
array: SMTArray<Name, DomainSort, RangeSort>,
|
||||
...indices: CoercibleToArrayIndexType<Name, DomainSort>
|
||||
): SortToExprMap<RangeSort, Name>;
|
||||
|
||||
/** @category Operations */
|
||||
Store<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name> = Sort<Name>>(
|
||||
array: SMTArray<Name, DomainSort, RangeSort>,
|
||||
...indicesAndValue: [
|
||||
...CoercibleToArrayIndexType<Name, DomainSort>,
|
||||
CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
|
||||
]
|
||||
): SMTArray<Name, DomainSort, RangeSort>;
|
||||
|
||||
/** @category Operations */
|
||||
Extract<Bits extends number>(hi: number, lo: number, val: BitVec<Bits, Name>): BitVec<number, Name>;
|
||||
|
||||
/** @category Operations */
|
||||
ast_from_string(s: string): Ast<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
substitute(t: Expr<Name>, ...substitutions: [Expr<Name>, Expr<Name>][]): Expr<Name>;
|
||||
|
||||
simplify(expr: Expr<Name>): Promise<Expr<Name>>;
|
||||
}
|
||||
|
||||
export interface Ast<Name extends string = 'main', Ptr = unknown> {
|
||||
|
|
@ -490,7 +625,7 @@ export interface Ast<Name extends string = 'main', Ptr = unknown> {
|
|||
|
||||
/** @hidden */
|
||||
export interface SolverCtor<Name extends string> {
|
||||
new(): Solver<Name>;
|
||||
new (): Solver<Name>;
|
||||
}
|
||||
|
||||
export interface Solver<Name extends string = 'main'> {
|
||||
|
|
@ -500,10 +635,11 @@ export interface Solver<Name extends string = 'main'> {
|
|||
readonly ctx: Context<Name>;
|
||||
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<string, any>): void;
|
||||
*/
|
||||
|
||||
/* TODO(ritave): Decide on how to discern between integer and float parameters
|
||||
set(params: Record<string, any>): void;
|
||||
*/
|
||||
push(): void;
|
||||
|
||||
pop(num?: number): void;
|
||||
|
|
@ -527,7 +663,7 @@ export interface Solver<Name extends string = 'main'> {
|
|||
|
||||
/** @hidden */
|
||||
export interface ModelCtor<Name extends string> {
|
||||
new(): Model<Name>;
|
||||
new (): Model<Name>;
|
||||
}
|
||||
|
||||
export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<Name>> {
|
||||
|
|
@ -566,6 +702,13 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
|
|||
get(constant: Expr<Name>): Expr<Name>;
|
||||
|
||||
get(sort: Sort<Name>): AstVector<Name, AnyExpr<Name>>;
|
||||
|
||||
updateValue(decl: FuncDecl<Name> | Expr<Name>, a: Ast<Name> | FuncInterp<Name>): void;
|
||||
|
||||
addFuncInterp<DomainSort extends Sort<Name>[] = Sort<Name>[], RangeSort extends Sort<Name> = Sort<Name>>(
|
||||
decl: FuncDecl<Name, DomainSort, RangeSort>,
|
||||
defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
|
||||
): FuncInterp<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -608,6 +751,23 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
|
|||
name(): string | number;
|
||||
}
|
||||
|
||||
/**
|
||||
* @category Functions
|
||||
*/
|
||||
export interface FuncEntry<Name extends string = 'main'> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FuncEntry';
|
||||
|
||||
readonly ctx: Context<Name>;
|
||||
readonly ptr: Z3_func_entry;
|
||||
|
||||
numArgs(): number;
|
||||
|
||||
argValue(i: number): Expr<Name>;
|
||||
|
||||
value(): Expr<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
* @category Functions
|
||||
*/
|
||||
|
|
@ -617,6 +777,16 @@ export interface FuncInterp<Name extends string = 'main'> {
|
|||
|
||||
readonly ctx: Context<Name>;
|
||||
readonly ptr: Z3_func_interp;
|
||||
|
||||
elseValue(): Expr<Name>;
|
||||
|
||||
numEntries(): number;
|
||||
|
||||
arity(): number;
|
||||
|
||||
entry(i: number): FuncEntry<Name>;
|
||||
|
||||
addEntry(args: Expr<Name>[], value: Expr<Name>): void;
|
||||
}
|
||||
|
||||
/** @hidden */
|
||||
|
|
@ -639,9 +809,14 @@ export interface FuncDeclCreation<Name extends string> {
|
|||
* @param name Name of the function
|
||||
* @param signature The domains, and last parameter - the range of the function
|
||||
*/
|
||||
declare(name: string, ...signature: FuncDeclSignature<Name>): FuncDecl<Name>;
|
||||
declare<DomainSort extends Sort<Name>[], RangeSort extends Sort<Name>>(
|
||||
name: string,
|
||||
...signature: [...DomainSort, RangeSort]
|
||||
): FuncDecl<Name, DomainSort, RangeSort>;
|
||||
|
||||
fresh(...signature: FuncDeclSignature<Name>): FuncDecl<Name>;
|
||||
fresh<DomainSort extends Sort<Name>[], RangeSort extends Sort<Name>>(
|
||||
...signature: [...DomainSort, RangeSort]
|
||||
): FuncDecl<Name, DomainSort, RangeSort>;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -656,7 +831,11 @@ export interface RecFuncCreation<Name extends string> {
|
|||
/**
|
||||
* @category Functions
|
||||
*/
|
||||
export interface FuncDecl<Name extends string = 'main'> extends Ast<Name, Z3_func_decl> {
|
||||
export interface FuncDecl<
|
||||
Name extends string = 'main',
|
||||
DomainSort extends Sort<Name>[] = Sort<Name>[],
|
||||
RangeSort extends Sort<Name> = Sort<Name>,
|
||||
> extends Ast<Name, Z3_func_decl> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FuncDecl';
|
||||
|
||||
|
|
@ -664,21 +843,26 @@ export interface FuncDecl<Name extends string = 'main'> extends Ast<Name, Z3_fun
|
|||
|
||||
arity(): number;
|
||||
|
||||
domain(i: number): Sort<Name>;
|
||||
domain<T extends number>(i: T): DomainSort[T];
|
||||
|
||||
range(): Sort<Name>;
|
||||
range(): RangeSort;
|
||||
|
||||
kind(): Z3_decl_kind;
|
||||
|
||||
params(): (number | string | Z3_symbol | Sort<Name> | Expr<Name> | FuncDecl<Name>)[];
|
||||
params(): (number | string | Sort<Name> | Expr<Name> | FuncDecl<Name>)[];
|
||||
|
||||
call(...args: CoercibleToExpr<Name>[]): AnyExpr<Name>;
|
||||
call(...args: CoercibleToArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name>;
|
||||
}
|
||||
|
||||
export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySort<Name>, Ptr = unknown>
|
||||
extends Ast<Name, Ptr> {
|
||||
/** @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<Name extends string = 'main', S extends Sort<Name> = AnySo
|
|||
|
||||
params(): ReturnType<FuncDecl<Name>['params']>;
|
||||
|
||||
name(): ReturnType<FuncDecl<Name>['name']>;
|
||||
|
||||
decl(): FuncDecl<Name>;
|
||||
|
||||
numArgs(): number;
|
||||
|
|
@ -725,7 +911,7 @@ export interface BoolCreation<Name extends string = 'main'> {
|
|||
/** @category Booleans */
|
||||
export interface Bool<Name extends string = 'main'> extends Expr<Name, BoolSort<Name>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'Bool';
|
||||
readonly __typename: 'Bool' | 'NonLambdaQuantifier';
|
||||
|
||||
not(): Bool<Name>;
|
||||
|
||||
|
|
@ -738,6 +924,13 @@ export interface Bool<Name extends string = 'main'> extends Expr<Name, BoolSort<
|
|||
implies(other: Bool<Name> | boolean): Bool<Name>;
|
||||
}
|
||||
|
||||
// TODO: properly implement pattern
|
||||
/** @category Quantifiers */
|
||||
export interface Pattern<Name extends string = 'main'> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'Pattern';
|
||||
}
|
||||
|
||||
/**
|
||||
* A Sort that represents Integers or Real numbers
|
||||
* @category Arithmetic
|
||||
|
|
@ -798,17 +991,17 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
|
|||
/**
|
||||
* Adds two numbers together
|
||||
*/
|
||||
add(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
add(other: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Multiplies two numbers together
|
||||
*/
|
||||
mul(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
mul(other: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Subtract second number from the first one
|
||||
*/
|
||||
sub(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
sub(other: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Applies power to the number
|
||||
|
|
@ -820,12 +1013,12 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
|
|||
* // x=-2
|
||||
* ```
|
||||
*/
|
||||
pow(exponent: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
pow(exponent: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Divides the number by the second one
|
||||
*/
|
||||
div(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
div(other: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Returns a number modulo second one
|
||||
|
|
@ -837,7 +1030,7 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
|
|||
* // x=8
|
||||
* ```
|
||||
*/
|
||||
mod(other: Arith<Name> | number | bigint | string): Arith<Name>;
|
||||
mod(other: CoercibleToArith<Name>): Arith<Name>;
|
||||
|
||||
/**
|
||||
* Returns a negation of the number
|
||||
|
|
@ -847,22 +1040,22 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
|
|||
/**
|
||||
* Return whether the number is less or equal than the second one (`<=`)
|
||||
*/
|
||||
le(other: Arith<Name> | number | bigint | string): Bool<Name>;
|
||||
le(other: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/**
|
||||
* Returns whether the number is less than the second one (`<`)
|
||||
*/
|
||||
lt(other: Arith<Name> | number | bigint | string): Bool<Name>;
|
||||
lt(other: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/**
|
||||
* Returns whether the number is greater than the second one (`>`)
|
||||
*/
|
||||
gt(other: Arith<Name> | number | bigint | string): Bool<Name>;
|
||||
gt(other: CoercibleToArith<Name>): Bool<Name>;
|
||||
|
||||
/**
|
||||
* Returns whether the number is greater or equal than the second one (`>=`)
|
||||
*/
|
||||
ge(other: Arith<Name> | number | bigint | string): Bool<Name>;
|
||||
ge(other: CoercibleToArith<Name>): Bool<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -939,12 +1132,6 @@ export interface BitVecSort<Bits extends number = number, Name extends string =
|
|||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
}
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToBitVec<Bits extends number = number, Name extends string = 'main'> =
|
||||
| bigint
|
||||
| number
|
||||
| BitVec<Bits, Name>;
|
||||
|
||||
/** @category Bit Vectors */
|
||||
export interface BitVecCreation<Name extends string> {
|
||||
sort<Bits extends number = number>(bits: Bits): BitVecSort<Bits, Name>;
|
||||
|
|
@ -1213,10 +1400,11 @@ export interface BitVecNum<Bits extends number = number, Name extends string = '
|
|||
* @typeParam RangeSort The sort of the array range
|
||||
* @category Arrays
|
||||
*/
|
||||
export interface SMTArraySort<Name extends string = 'main',
|
||||
DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
|
||||
export interface SMTArraySort<
|
||||
Name extends string = 'main',
|
||||
DomainSort extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
|
||||
RangeSort extends AnySort<Name> = AnySort<Name>,
|
||||
> extends Sort<Name> {
|
||||
> extends Sort<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'ArraySort';
|
||||
|
||||
|
|
@ -1236,36 +1424,47 @@ export interface SMTArraySort<Name extends string = 'main',
|
|||
* The sort of the range
|
||||
*/
|
||||
range(): RangeSort;
|
||||
|
||||
}
|
||||
|
||||
/** @category Arrays */
|
||||
export interface SMTArrayCreation<Name extends string> {
|
||||
sort<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
|
||||
sort<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>(
|
||||
...sig: [...DomainSort, RangeSort]
|
||||
): SMTArraySort<Name, DomainSort, RangeSort>;
|
||||
|
||||
const<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
|
||||
name: string, ...sig: [...DomainSort, RangeSort]
|
||||
const<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>(
|
||||
name: string,
|
||||
...sig: [...DomainSort, RangeSort]
|
||||
): SMTArray<Name, DomainSort, RangeSort>;
|
||||
|
||||
consts<DomainSort extends [AnySort<Name>, ...AnySort<Name>[]], RangeSort extends AnySort<Name>>(
|
||||
consts<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>(
|
||||
names: string | string[],
|
||||
...sig: [...DomainSort, RangeSort]
|
||||
): SMTArray<Name, DomainSort, RangeSort>[];
|
||||
|
||||
K<DomainSort extends AnySort<Name>, RangeSort extends AnySort<Name>>(
|
||||
domain: DomainSort,
|
||||
value: SortToExprMap<RangeSort, Name>
|
||||
value: SortToExprMap<RangeSort, Name>,
|
||||
): SMTArray<Name, [DomainSort], RangeSort>;
|
||||
}
|
||||
|
||||
export type ArrayIndexType<Name extends string = 'main',
|
||||
DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]]> = [...{
|
||||
[Index in keyof DomainSort]: DomainSort[Index] extends AnySort<Name> ?
|
||||
CoercibleFromMap<SortToExprMap<DomainSort[Index], Name>, Name> :
|
||||
DomainSort[Index];
|
||||
}]
|
||||
export type NonEmptySortArray<Name extends string = 'main'> = [Sort<Name>, ...Array<Sort<Name>>];
|
||||
|
||||
export type ArrayIndexType<Name extends string, DomainSort extends Sort<Name>[]> = [
|
||||
...{
|
||||
[Key in keyof DomainSort]: DomainSort[Key] extends AnySort<Name>
|
||||
? SortToExprMap<DomainSort[Key], Name>
|
||||
: DomainSort[Key];
|
||||
},
|
||||
];
|
||||
|
||||
export type CoercibleToArrayIndexType<Name extends string, DomainSort extends Sort<Name>[]> = [
|
||||
...{
|
||||
[Key in keyof DomainSort]: DomainSort[Key] extends AnySort<Name>
|
||||
? CoercibleToMap<SortToExprMap<DomainSort[Key], Name>, Name>
|
||||
: DomainSort[Key];
|
||||
},
|
||||
];
|
||||
|
||||
/**
|
||||
* Represents Array expression
|
||||
|
|
@ -1274,13 +1473,13 @@ export type ArrayIndexType<Name extends string = 'main',
|
|||
* @typeParam RangeSort The sort of the array range
|
||||
* @category Arrays
|
||||
*/
|
||||
export interface SMTArray<Name extends string = 'main',
|
||||
DomainSort extends [AnySort<Name>, ...AnySort<Name>[]] = [Sort<Name>, ...Sort<Name>[]],
|
||||
RangeSort extends AnySort<Name> = AnySort<Name>>
|
||||
extends Expr<Name, SMTArraySort<Name, DomainSort, RangeSort>, Z3_ast> {
|
||||
|
||||
export interface SMTArray<
|
||||
Name extends string = 'main',
|
||||
DomainSort extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
|
||||
RangeSort extends Sort<Name> = Sort<Name>,
|
||||
> extends Expr<Name, SMTArraySort<Name, DomainSort, RangeSort>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'Array';
|
||||
readonly __typename: 'Array' | 'Lambda';
|
||||
|
||||
domain(): DomainSort[0];
|
||||
|
||||
|
|
@ -1288,7 +1487,7 @@ export interface SMTArray<Name extends string = 'main',
|
|||
|
||||
range(): RangeSort;
|
||||
|
||||
select(...indices: ArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name>;
|
||||
select(...indices: CoercibleToArrayIndexType<Name, DomainSort>): SortToExprMap<RangeSort, Name>;
|
||||
|
||||
/**
|
||||
* value should be coercible to RangeSort
|
||||
|
|
@ -1297,11 +1496,60 @@ export interface SMTArray<Name extends string = 'main',
|
|||
*/
|
||||
store(
|
||||
...indicesAndValue: [
|
||||
...ArrayIndexType<Name, DomainSort>,
|
||||
CoercibleFromMap<SortToExprMap<RangeSort, Name>, Name>
|
||||
...CoercibleToArrayIndexType<Name, DomainSort>,
|
||||
CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
|
||||
]
|
||||
): SMTArray<Name, DomainSort, RangeSort>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Defines the expression type of the body of a quantifier expression
|
||||
*
|
||||
* @category Quantifiers
|
||||
*/
|
||||
export type BodyT<
|
||||
Name extends string = 'main',
|
||||
QVarSorts extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
|
||||
QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts> = BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
|
||||
> = QSort extends BoolSort<Name>
|
||||
? Bool<Name>
|
||||
: QSort extends SMTArray<Name, QVarSorts, infer RangeSort>
|
||||
? SortToExprMap<RangeSort, Name>
|
||||
: never;
|
||||
|
||||
/** @category Quantifiers */
|
||||
export interface Quantifier<
|
||||
Name extends string = 'main',
|
||||
QVarSorts extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
|
||||
QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts> = BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
|
||||
> extends Expr<Name, QSort> {
|
||||
readonly __typename: 'NonLambdaQuantifier' | 'Lambda';
|
||||
|
||||
is_forall(): boolean;
|
||||
|
||||
is_exists(): boolean;
|
||||
|
||||
is_lambda(): boolean;
|
||||
|
||||
weight(): number;
|
||||
|
||||
num_patterns(): number;
|
||||
|
||||
pattern(i: number): Pattern<Name>;
|
||||
|
||||
num_no_patterns(): number;
|
||||
|
||||
no_pattern(i: number): Expr<Name>;
|
||||
|
||||
body(): BodyT<Name, QVarSorts, QSort>;
|
||||
|
||||
num_vars(): number;
|
||||
|
||||
var_name(i: number): string | number;
|
||||
|
||||
var_sort<T extends number>(i: T): QVarSorts[T];
|
||||
|
||||
children(): [BodyT<Name, QVarSorts, QSort>];
|
||||
}
|
||||
|
||||
export interface Probe<Name extends string = 'main'> {
|
||||
|
|
@ -1314,7 +1562,7 @@ export interface Probe<Name extends string = 'main'> {
|
|||
|
||||
/** @hidden */
|
||||
export interface TacticCtor<Name extends string> {
|
||||
new(name: string): Tactic<Name>;
|
||||
new (name: string): Tactic<Name>;
|
||||
}
|
||||
|
||||
export interface Tactic<Name extends string = 'main'> {
|
||||
|
|
@ -1327,7 +1575,7 @@ export interface Tactic<Name extends string = 'main'> {
|
|||
|
||||
/** @hidden */
|
||||
export interface AstVectorCtor<Name extends string> {
|
||||
new<Item extends Ast<Name> = AnyAst<Name>>(): AstVector<Name, Item>;
|
||||
new <Item extends Ast<Name> = AnyAst<Name>>(): AstVector<Name, Item>;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -1378,7 +1626,7 @@ export interface AstVector<Name extends string = 'main', Item extends Ast<Name>
|
|||
|
||||
/** @hidden */
|
||||
export interface AstMapCtor<Name extends string> {
|
||||
new<Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>(): AstMap<Name, Key, Value>;
|
||||
new <Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>(): AstMap<Name, Key, Value>;
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -1402,8 +1650,11 @@ export interface AstMapCtor<Name extends string> {
|
|||
* // 0
|
||||
* ```
|
||||
*/
|
||||
export interface AstMap<Name extends string = 'main', Key extends Ast<Name> = AnyAst<Name>, Value extends Ast<Name> = AnyAst<Name>>
|
||||
extends Iterable<[Key, Value]> {
|
||||
export interface AstMap<
|
||||
Name extends string = 'main',
|
||||
Key extends Ast<Name> = AnyAst<Name>,
|
||||
Value extends Ast<Name> = AnyAst<Name>,
|
||||
> extends Iterable<[Key, Value]> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'AstMap';
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue