mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Add WebAssembly/TypeScript bindings (#5762)
* Add TypeScript bindings * mark Z3_eval_smtlib2_string as async
This commit is contained in:
Kevin Gibbons
GitHub
parent
9ac57fc510
commit
2b934b601d
61
.github/workflows/wasm-release.yml
vendored
Normal file
61
.github/workflows/wasm-release.yml
vendored
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
name: WebAssembly Publish
|
||||
|
||||
on:
|
||||
workflow_dispatch:
|
||||
|
||||
defaults:
|
||||
run:
|
||||
working-directory: src/api/js
|
||||
|
||||
env:
|
||||
EM_VERSION: 3.1.0
|
||||
|
||||
jobs:
|
||||
publish:
|
||||
name: Publish
|
||||
runs-on: ubuntu-latest
|
||||
steps:
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v2
|
||||
|
||||
- name: Setup node
|
||||
uses: actions/setup-node@v2
|
||||
with:
|
||||
node-version: 'lts/*'
|
||||
registry-url: 'https://registry.npmjs.org'
|
||||
|
||||
- name: Prepare for publish
|
||||
run: |
|
||||
npm version $(node -e 'console.log(fs.readFileSync("../../../scripts/release.yml", "utf8").match(/ReleaseVersion:\s*\x27(\S+)\x27/)[1])')
|
||||
mv PUBLISHED_README.md README.md
|
||||
cp ../../../LICENSE.txt .
|
||||
|
||||
- name: Setup emscripten
|
||||
uses: mymindstorm/setup-emsdk@v11
|
||||
with:
|
||||
no-install: true
|
||||
version: ${{env.EM_VERSION}}
|
||||
actions-cache-folder: 'emsdk-cache'
|
||||
|
||||
- name: Install dependencies
|
||||
run: npm ci
|
||||
|
||||
- name: Build TypeScript
|
||||
run: npm run build-ts
|
||||
|
||||
- name: Build wasm
|
||||
run: |
|
||||
emsdk install ${EM_VERSION}
|
||||
emsdk activate ${EM_VERSION}
|
||||
source $(dirname $(which emsdk))/emsdk_env.sh
|
||||
which node
|
||||
which clang++
|
||||
npm run build-wasm
|
||||
|
||||
- name: Test
|
||||
run: npm test
|
||||
|
||||
- name: Publish
|
||||
run: npm publish
|
||||
env:
|
||||
NODE_AUTH_TOKEN: ${{ secrets.NPM_TOKEN }}
|
||||
66
.github/workflows/wasm.yml
vendored
66
.github/workflows/wasm.yml
vendored
|
|
@ -1,43 +1,51 @@
|
|||
name: WASM Build
|
||||
name: WebAssembly Build
|
||||
|
||||
on:
|
||||
push:
|
||||
branches: [ master ]
|
||||
pull_request:
|
||||
|
||||
defaults:
|
||||
run:
|
||||
working-directory: src/api/js
|
||||
|
||||
env:
|
||||
BUILD_TYPE: Release
|
||||
EM_VERSION: 3.1.0
|
||||
|
||||
jobs:
|
||||
build:
|
||||
check:
|
||||
name: Check
|
||||
runs-on: ubuntu-latest
|
||||
|
||||
steps:
|
||||
- name: Checkout code
|
||||
uses: actions/checkout@v2
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v2
|
||||
|
||||
- name: Import emscripten
|
||||
uses: mymindstorm/setup-emsdk@v9
|
||||
- name: Setup node
|
||||
uses: actions/setup-node@v2
|
||||
with:
|
||||
node-version: 'lts/*'
|
||||
|
||||
- name: Configure CMake and build
|
||||
run: |
|
||||
mkdir build
|
||||
cd build
|
||||
- name: Setup emscripten
|
||||
uses: mymindstorm/setup-emsdk@v11
|
||||
with:
|
||||
no-install: true
|
||||
version: ${{env.EM_VERSION}}
|
||||
actions-cache-folder: 'emsdk-cache'
|
||||
|
||||
emcmake cmake \
|
||||
-DCMAKE_BUILD_TYPE=MinSizeRel \
|
||||
-DZ3_BUILD_LIBZ3_SHARED=OFF \
|
||||
-DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
|
||||
-DZ3_BUILD_TEST_EXECUTABLES=OFF \
|
||||
-DZ3_BUILD_EXECUTABLE=OFF \
|
||||
-DZ3_SINGLE_THREADED=ON \
|
||||
-DCMAKE_CXX_FLAGS="-s DISABLE_EXCEPTION_CATCHING=0" \
|
||||
..;
|
||||
make
|
||||
tar -cvf z3-build-wasm.tar *.a
|
||||
- name: Install dependencies
|
||||
run: npm ci
|
||||
|
||||
- name: Archive production artifacts
|
||||
uses: actions/upload-artifact@v2
|
||||
with:
|
||||
name: z3-build-wasm
|
||||
path: build/z3-build-wasm.tar
|
||||
retention-days: 5
|
||||
- name: Build TypeScript
|
||||
run: npm run build-ts
|
||||
|
||||
- name: Build wasm
|
||||
run: |
|
||||
emsdk install ${EM_VERSION}
|
||||
emsdk activate ${EM_VERSION}
|
||||
source $(dirname $(which emsdk))/emsdk_env.sh
|
||||
which node
|
||||
which clang++
|
||||
npm run build-wasm
|
||||
|
||||
- name: Test
|
||||
run: npm test
|
||||
|
|
|
|||
7
.gitignore
vendored
7
.gitignore
vendored
|
|
@ -75,6 +75,13 @@ src/api/ml/z3enums.ml
|
|||
src/api/ml/z3native.mli
|
||||
src/api/ml/z3enums.mli
|
||||
src/api/ml/z3.mllib
|
||||
src/api/js/node_modules/
|
||||
src/api/js/*.js
|
||||
src/api/js/build/
|
||||
src/api/js/**/*.d.ts
|
||||
!src/api/js/scripts/*.js
|
||||
!src/api/js/src/*.js
|
||||
|
||||
out/**
|
||||
*.bak
|
||||
doc/api
|
||||
|
|
|
|||
|
|
@ -195,9 +195,9 @@ See [``examples/python``](examples/python) for examples.
|
|||
|
||||
The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in [src/api/julia](src/api/julia).
|
||||
|
||||
### ``Web Assembly``
|
||||
### ``Web Assembly`` / ``TypeScript`` / ``JavaScript``
|
||||
|
||||
[WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel.
|
||||
A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](src/api/js).
|
||||
|
||||
## System Overview
|
||||
|
||||
|
|
|
|||
124
src/api/js/PUBLISHED_README.md
Normal file
124
src/api/js/PUBLISHED_README.md
Normal file
|
|
@ -0,0 +1,124 @@
|
|||
# Z3 TypeScript Bindings
|
||||
|
||||
This project provides low-level TypeScript bindings for the [Z3 theorem prover](https://github.com/Z3Prover/z3). It is available on npm as [z3-solver](https://www.npmjs.com/package/z3-solver).
|
||||
|
||||
Z3 itself is distributed as a wasm artifact as part of this package. You can find the documentation for the Z3 API [here](https://z3prover.github.io/api/html/z3__api_8h.html), though note the differences below.
|
||||
|
||||
|
||||
## Using
|
||||
|
||||
This requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications.
|
||||
|
||||
Other than the differences below, the bindings can be used exactly as you'd use the C library. Because this is a wrapper around a C library, most of the values you'll use are just numbers representing pointers. For this reason you are strongly encouraged to make use of the TypeScript types to differentiate among the different kinds of value.
|
||||
|
||||
The module exports an `init` function, is an async function which initializes the library and returns `{ em, Z3 }` - `em` contains the underlying emscripten module, which you can use to e.g. kill stray threads, and `Z3` contains the actual bindings. The other module exports are the enums defined in the Z3 API.
|
||||
|
||||
[`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c).
|
||||
|
||||
|
||||
## Differences from the C API
|
||||
|
||||
### Integers
|
||||
|
||||
JavaScript numbers are IEEE double-precisions floats. These can be used wherever the C API expects an `int`, `unsigned int`, `float`, or `double`.
|
||||
|
||||
`int64_t` and `uint64_t` cannot be precisely represented by JS numbers, so in the TS bindings they are represented by [BigInts](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Data_structures#bigint_type).
|
||||
|
||||
### Out parameters
|
||||
|
||||
In C, to return multiple values a function will take an address to write to, conventionally referred to as an "out parameter". Sometimes the function returns a boolean to indicate success; other times it may return nothing or some other value.
|
||||
|
||||
In JS the convention when returning multiple values is to return records containing the values of interest.
|
||||
|
||||
The wrapper translates between the two conventions. For example, the C declaration
|
||||
|
||||
```c
|
||||
void Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
|
||||
```
|
||||
|
||||
is represented in the TS bindings as
|
||||
|
||||
```ts
|
||||
function rcf_get_numerator_denominator(c: Z3_context, a: Z3_rcf_num): { n: Z3_rcf_num; d: Z3_rcf_num } {
|
||||
// ...
|
||||
}
|
||||
```
|
||||
|
||||
When there is only a single out parameter, and the return value is not otherwise of interest, the parameter is not wrapped. For example, the C declaration
|
||||
|
||||
```c
|
||||
Z3_bool Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
|
||||
```
|
||||
|
||||
is represented in the TS bindings as
|
||||
|
||||
```ts
|
||||
function model_eval(c: Z3_context, m: Z3_model, t: Z3_ast, model_completion: boolean): Z3_ast | null {
|
||||
// ...
|
||||
}
|
||||
```
|
||||
|
||||
Note that the boolean return type of the C function is translated into a nullable return type for the TS binding.
|
||||
|
||||
When the return value is of interest it is included in the returned record under the key `rv`.
|
||||
|
||||
|
||||
### Arrays
|
||||
|
||||
The when the C API takes an array as an argument it will also require a parameter which specifies the length of the array (since arrays do not carry their own lengths in C). In the TS bindings this is automatically inferred.
|
||||
|
||||
For example, the C declaration
|
||||
```js
|
||||
unsigned Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
|
||||
```
|
||||
|
||||
is represented in the TS bindings as
|
||||
|
||||
```ts
|
||||
function rcf_mk_roots(c: Z3_context, a: Z3_rcf_num[]): { rv: number; roots: Z3_rcf_num[] } {
|
||||
// ...
|
||||
}
|
||||
```
|
||||
|
||||
When there are multiple arrays which the C API expects to be of the same length, the TS bindings will enforce that this is the case.
|
||||
|
||||
|
||||
### Null pointers
|
||||
|
||||
Some of the C APIs accept or return null pointers (represented by types whose name end in `_opt`). These are represented in the TS bindings as `| null`. For example, the C declaration
|
||||
|
||||
```js
|
||||
Z3_ast_opt Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
|
||||
```
|
||||
|
||||
is represented in the TS bindings as
|
||||
|
||||
```ts
|
||||
function model_get_const_interp(c: Z3_context, m: Z3_model, a: Z3_func_decl): Z3_ast | null {
|
||||
// ...
|
||||
}
|
||||
```
|
||||
|
||||
|
||||
### Async functions
|
||||
|
||||
Certain long-running APIs are not appropriate to call on the main thread. In the TS bindings those APIs are marked as `async` and are automatically called on a different thread. This includes the following APIs:
|
||||
|
||||
- `Z3_simplify`
|
||||
- `Z3_simplify_ex`
|
||||
- `Z3_solver_check`
|
||||
- `Z3_solver_check_assumptions`
|
||||
- `Z3_solver_cube`
|
||||
- `Z3_solver_get_consequences`
|
||||
- `Z3_tactic_apply`
|
||||
- `Z3_tactic_apply_ex`
|
||||
- `Z3_optimize_check`
|
||||
- `Z3_algebraic_roots`
|
||||
- `Z3_algebraic_eval`
|
||||
- `Z3_fixedpoint_query`
|
||||
- `Z3_fixedpoint_query_relations`
|
||||
- `Z3_fixedpoint_query_from_lvl`
|
||||
- `Z3_polynomial_subresultants`
|
||||
|
||||
Note that these are not thread-safe, and so only one call can be running at a time. Trying to call a second async API before the first completes will throw.
|
||||
|
||||
17
src/api/js/README.md
Normal file
17
src/api/js/README.md
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
# TypeScript Bindings
|
||||
|
||||
This directory contains JavaScript code to automatically derive TypeScript bindings for the C API, which are published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver).
|
||||
|
||||
The readme for the bindings themselves is located in [`PUBLISHED_README.md`](./PUBLISHED_README.md).
|
||||
|
||||
|
||||
## Building
|
||||
|
||||
You'll need to have emscripten set up, along with all of its dependencies. The easiest way to do that is with [emsdk](https://github.com/emscripten-core/emsdk).
|
||||
|
||||
Then run `npm i` to install dependencies, `npm run build-ts` to build the TypeScript wrapper, and `npm run build-wasm` to build the wasm artifact.
|
||||
|
||||
|
||||
## Tests
|
||||
|
||||
Current tests are very minimal: [`test-ts-api.ts`](./test-ts-api.ts) contains a couple real cases translated very mechanically from [this file](https://github.com/Z3Prover/z3/blob/90fd3d82fce20d45ed2eececdf65545bab769503/examples/c/test_capi.c).
|
||||
23
src/api/js/build-wasm.sh
Executable file
23
src/api/js/build-wasm.sh
Executable file
|
|
@ -0,0 +1,23 @@
|
|||
#!/bin/bash
|
||||
|
||||
set -euxo pipefail
|
||||
|
||||
|
||||
export ROOT=$PWD
|
||||
|
||||
cd ../../..
|
||||
export CXXFLAGS="-pthread -s USE_PTHREADS=1 -s DISABLE_EXCEPTION_CATCHING=0"
|
||||
export LDFLAGS="-s WASM_BIGINT -s -pthread -s USE_PTHREADS=1"
|
||||
if [ ! -f "build/Makefile" ]; then
|
||||
emconfigure python scripts/mk_make.py --staticlib --single-threaded
|
||||
fi
|
||||
|
||||
cd build
|
||||
emmake make -j$(nproc) libz3.a
|
||||
|
||||
cd $ROOT
|
||||
|
||||
export EM_CACHE=$HOME/.emscripten/
|
||||
export FNS=$(node scripts/list-exports.js)
|
||||
export METHODS='["ccall","FS","allocate","UTF8ToString","intArrayFromString","ALLOC_NORMAL"]'
|
||||
emcc build/async-fns.cc ../../../build/libz3.a --std=c++20 --pre-js src/async-wrapper.js -g2 -pthread -fexceptions -s WASM_BIGINT -s USE_PTHREADS=1 -s PTHREAD_POOL_SIZE=0 -s PTHREAD_POOL_SIZE_STRICT=0 -s MODULARIZE=1 -s 'EXPORT_NAME="initZ3"' -s EXPORTED_RUNTIME_METHODS=$METHODS -s EXPORTED_FUNCTIONS=$FNS -s DISABLE_EXCEPTION_CATCHING=0 -s SAFE_HEAP=0 -s DEMANGLE_SUPPORT=1 -s TOTAL_MEMORY=1GB -I z3/src/api/ -o build/z3-built.js
|
||||
57
src/api/js/example-raw.ts
Normal file
57
src/api/js/example-raw.ts
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
import { init } from './build/wrapper';
|
||||
|
||||
// demonstrates use of the raw API
|
||||
|
||||
(async () => {
|
||||
let { em, Z3 } = await init();
|
||||
|
||||
Z3.global_param_set('verbose', '10');
|
||||
console.log('verbosity:', Z3.global_param_get('verbose'));
|
||||
|
||||
let config = Z3.mk_config();
|
||||
let ctx = Z3.mk_context_rc(config);
|
||||
Z3.del_config(config);
|
||||
|
||||
let unicodeStr = [...'hello™'].map(x => x.codePointAt(0)!);
|
||||
let strAst = Z3.mk_u32string(ctx, unicodeStr);
|
||||
Z3.inc_ref(ctx, strAst);
|
||||
|
||||
console.log(Z3.is_string(ctx, strAst));
|
||||
console.log(Z3.get_string(ctx, strAst));
|
||||
console.log(Z3.get_string_contents(ctx, strAst, unicodeStr.length));
|
||||
|
||||
let bv = Z3.mk_bv_numeral(ctx, [true, true, false]);
|
||||
let bs = Z3.mk_ubv_to_str(ctx, bv);
|
||||
console.log(Z3.ast_to_string(ctx, bs));
|
||||
|
||||
let intSort = Z3.mk_int_sort(ctx);
|
||||
let big = Z3.mk_int64(ctx, 42n, intSort);
|
||||
console.log(Z3.get_numeral_string(ctx, big));
|
||||
console.log(Z3.get_numeral_int64(ctx, big));
|
||||
|
||||
console.log(Z3.get_version());
|
||||
|
||||
let head_tail = [Z3.mk_string_symbol(ctx, 'car'), Z3.mk_string_symbol(ctx, 'cdr')];
|
||||
|
||||
let nil_con = Z3.mk_constructor(ctx, Z3.mk_string_symbol(ctx, 'nil'), Z3.mk_string_symbol(ctx, 'is_nil'), [], [], []);
|
||||
let cons_con = Z3.mk_constructor(
|
||||
ctx,
|
||||
Z3.mk_string_symbol(ctx, 'cons'),
|
||||
Z3.mk_string_symbol(ctx, 'is_cons'),
|
||||
head_tail,
|
||||
[null, null],
|
||||
[0, 0],
|
||||
);
|
||||
|
||||
let cell = Z3.mk_datatype(ctx, Z3.mk_string_symbol(ctx, 'cell'), [nil_con, cons_con]);
|
||||
console.log(Z3.query_constructor(ctx, nil_con, 0));
|
||||
console.log(Z3.query_constructor(ctx, cons_con, 2));
|
||||
|
||||
Z3.dec_ref(ctx, strAst);
|
||||
Z3.del_context(ctx);
|
||||
|
||||
em.PThread.terminateAllThreads();
|
||||
})().catch(e => {
|
||||
console.error('error', e);
|
||||
process.exit(1);
|
||||
});
|
||||
30
src/api/js/package-lock.json
generated
Normal file
30
src/api/js/package-lock.json
generated
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
{
|
||||
"requires": true,
|
||||
"lockfileVersion": 1,
|
||||
"dependencies": {
|
||||
"@types/node": {
|
||||
"version": "17.0.8",
|
||||
"resolved": "https://registry.npmjs.org/@types/node/-/node-17.0.8.tgz",
|
||||
"integrity": "sha512-YofkM6fGv4gDJq78g4j0mMuGMkZVxZDgtU0JRdx6FgiJDG+0fY0GKVolOV8WqVmEhLCXkQRjwDdKyPxJp/uucg==",
|
||||
"dev": true
|
||||
},
|
||||
"prettier": {
|
||||
"version": "2.5.1",
|
||||
"resolved": "https://registry.npmjs.org/prettier/-/prettier-2.5.1.tgz",
|
||||
"integrity": "sha512-vBZcPRUR5MZJwoyi3ZoyQlc1rXeEck8KgeC9AwwOn+exuxLxq5toTRDTSaVrXHxelDMHy9zlicw8u66yxoSUFg==",
|
||||
"dev": true
|
||||
},
|
||||
"sprintf-js": {
|
||||
"version": "1.1.2",
|
||||
"resolved": "https://registry.npmjs.org/sprintf-js/-/sprintf-js-1.1.2.tgz",
|
||||
"integrity": "sha512-VE0SOVEHCk7Qc8ulkWw3ntAzXuqf7S2lvwQaDLRnUeIEaKNQJzV6BwmLKhOqT61aGhfUMrXeaBk+oDGCzvhcug==",
|
||||
"dev": true
|
||||
},
|
||||
"typescript": {
|
||||
"version": "4.5.4",
|
||||
"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.5.4.tgz",
|
||||
"integrity": "sha512-VgYs2A2QIRuGphtzFV7aQJduJ2gyfTljngLzjpfW9FoYZF6xuw1W0vW9ghCKLfcWrCFxK81CSGRAvS1pn4fIUg==",
|
||||
"dev": true
|
||||
}
|
||||
}
|
||||
}
|
||||
27
src/api/js/package.json
Normal file
27
src/api/js/package.json
Normal file
|
|
@ -0,0 +1,27 @@
|
|||
{
|
||||
"name": "z3-solver",
|
||||
"keywords": ["Z3", "theorem", "prover", "solver", "satisfiability", "smt", "satisfiability modulo theories"],
|
||||
"homepage": "https://github.com/Z3Prover/z3/tree/master/src/api/js",
|
||||
"repository": "github:Z3Prover/z3",
|
||||
"engines": {
|
||||
"node": ">=16"
|
||||
},
|
||||
"main": "build/wrapper.js",
|
||||
"types": "build/wrapper.d.ts",
|
||||
"files": [
|
||||
"build/*.{js,d.ts,wasm}"
|
||||
],
|
||||
"scripts": {
|
||||
"build-ts": "mkdir -p build && node scripts/make-ts-wrapper.js > build/wrapper.ts && tsc",
|
||||
"build-wasm": "mkdir -p build && node scripts/make-cc-wrapper.js > build/async-fns.cc && ./build-wasm.sh",
|
||||
"format": "prettier --write --single-quote --arrow-parens avoid --print-width 120 --trailing-comma all '{,src/,scripts/}*.{js,ts}'",
|
||||
"test": "node test-ts-api.js"
|
||||
},
|
||||
"devDependencies": {
|
||||
"@types/node": "^17.0.8",
|
||||
"prettier": "^2.5.1",
|
||||
"sprintf-js": "^1.1.2",
|
||||
"typescript": "^4.5.4"
|
||||
},
|
||||
"license": "MIT"
|
||||
}
|
||||
22
src/api/js/scripts/async-fns.js
Normal file
22
src/api/js/scripts/async-fns.js
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
'use strict';
|
||||
|
||||
// things which you probably want to do off-thread
|
||||
// from https://github.com/Z3Prover/z3/issues/5746#issuecomment-1006289146
|
||||
module.exports = [
|
||||
'Z3_eval_smtlib2_string',
|
||||
'Z3_simplify',
|
||||
'Z3_simplify_ex',
|
||||
'Z3_solver_check',
|
||||
'Z3_solver_check_assumptions',
|
||||
'Z3_solver_cube',
|
||||
'Z3_solver_get_consequences',
|
||||
'Z3_tactic_apply',
|
||||
'Z3_tactic_apply_ex',
|
||||
'Z3_optimize_check',
|
||||
'Z3_algebraic_roots',
|
||||
'Z3_algebraic_eval',
|
||||
'Z3_fixedpoint_query',
|
||||
'Z3_fixedpoint_query_relations',
|
||||
'Z3_fixedpoint_query_from_lvl',
|
||||
'Z3_polynomial_subresultants',
|
||||
];
|
||||
11
src/api/js/scripts/list-exports.js
Normal file
11
src/api/js/scripts/list-exports.js
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
'use strict';
|
||||
|
||||
// this is called by build.sh to generate the names of the bindings to export
|
||||
|
||||
let { functions } = require('./parse-api.js');
|
||||
let asyncFns = require('./async-fns.js');
|
||||
|
||||
let extras = asyncFns.map(f => '_async_' + f);
|
||||
let fns = functions.filter(f => !asyncFns.includes(f.name));
|
||||
|
||||
console.log(JSON.stringify([...extras, ...functions.map(f => '_' + f.name)]));
|
||||
82
src/api/js/scripts/make-cc-wrapper.js
Normal file
82
src/api/js/scripts/make-cc-wrapper.js
Normal file
|
|
@ -0,0 +1,82 @@
|
|||
'use strict';
|
||||
|
||||
// generates c wrappers with off-thread versions of specified functions
|
||||
|
||||
let path = require('path');
|
||||
|
||||
let { functions } = require('./parse-api.js');
|
||||
let asyncFns = require('./async-fns.js');
|
||||
|
||||
let wrappers = [];
|
||||
|
||||
for (let fnName of asyncFns) {
|
||||
let fn = functions.find(f => f.name === fnName);
|
||||
if (fn == null) {
|
||||
throw new Error(`could not find definition for ${fnName}`);
|
||||
}
|
||||
let wrapper;
|
||||
if (fn.cRet === 'Z3_string') {
|
||||
wrapper = `wrapper_str`;
|
||||
} else if (['int', 'unsigned', 'void'].includes(fn.cRet) || fn.cRet.startsWith('Z3_')) {
|
||||
wrapper = `wrapper`;
|
||||
} else {
|
||||
throw new Error(`async function with unknown return type ${fn.cRet}`);
|
||||
}
|
||||
|
||||
wrappers.push(
|
||||
`
|
||||
extern "C" void async_${fn.name}(${fn.params
|
||||
.map(p => `${p.isConst ? 'const ' : ''}${p.cType}${p.isPtr ? '*' : ''} ${p.name}${p.isArray ? '[]' : ''}`)
|
||||
.join(', ')}) {
|
||||
${wrapper}<decltype(&${fn.name}), &${fn.name}>(${fn.params.map(p => `${p.name}`).join(', ')});
|
||||
}
|
||||
`.trim(),
|
||||
);
|
||||
}
|
||||
|
||||
console.log(`// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
|
||||
// DO NOT EDIT IT BY HAND
|
||||
|
||||
#include <thread>
|
||||
|
||||
#include <emscripten.h>
|
||||
|
||||
#include "../../z3.h"
|
||||
|
||||
template<typename Fn, Fn fn, typename... Args>
|
||||
void wrapper(Args&&... args) {
|
||||
std::thread t([...args = std::forward<Args>(args)] {
|
||||
try {
|
||||
auto result = fn(args...);
|
||||
MAIN_THREAD_ASYNC_EM_ASM({
|
||||
resolve_async($0);
|
||||
}, result);
|
||||
} catch (...) {
|
||||
MAIN_THREAD_ASYNC_EM_ASM({
|
||||
reject_async('failed with unknown exception');
|
||||
});
|
||||
throw;
|
||||
}
|
||||
});
|
||||
t.detach();
|
||||
}
|
||||
|
||||
template<typename Fn, Fn fn, typename... Args>
|
||||
void wrapper_str(Args&&... args) {
|
||||
std::thread t([...args = std::forward<Args>(args)] {
|
||||
try {
|
||||
auto result = fn(args...);
|
||||
MAIN_THREAD_ASYNC_EM_ASM({
|
||||
resolve_async(UTF8ToString($0));
|
||||
}, result);
|
||||
} catch (...) {
|
||||
MAIN_THREAD_ASYNC_EM_ASM({
|
||||
reject_async('failed with unknown exception');
|
||||
});
|
||||
throw;
|
||||
}
|
||||
});
|
||||
t.detach();
|
||||
}
|
||||
|
||||
${wrappers.join('\n\n')}`);
|
||||
422
src/api/js/scripts/make-ts-wrapper.js
Normal file
422
src/api/js/scripts/make-ts-wrapper.js
Normal file
|
|
@ -0,0 +1,422 @@
|
|||
'use strict';
|
||||
|
||||
let path = require('path');
|
||||
let prettier = require('prettier');
|
||||
|
||||
let { primitiveTypes, types, enums, functions } = require('./parse-api.js');
|
||||
let asyncFns = require('./async-fns.js');
|
||||
|
||||
let subtypes = {
|
||||
__proto__: null,
|
||||
Z3_sort: 'Z3_ast',
|
||||
Z3_func_decl: 'Z3_ast',
|
||||
};
|
||||
|
||||
let makePointerType = t =>
|
||||
`export type ${t} = ` + (t in subtypes ? `Subpointer<'${t}', '${subtypes[t]}'>;` : `Pointer<'${t}'>;`);
|
||||
|
||||
// this supports a up to 6 out intergers/pointers
|
||||
// or up to 3 out int64s
|
||||
const BYTES_TO_ALLOCATE_FOR_OUT_PARAMS = 24;
|
||||
|
||||
function toEmType(type) {
|
||||
if (type in primitiveTypes) {
|
||||
type = primitiveTypes[type];
|
||||
}
|
||||
if (['boolean', 'number', 'string', 'bigint', 'void'].includes(type)) {
|
||||
return type;
|
||||
}
|
||||
if (type.startsWith('Z3_')) {
|
||||
return 'number';
|
||||
}
|
||||
throw new Error(`unknown parameter type ${type}`);
|
||||
}
|
||||
|
||||
function isZ3PointerType(type) {
|
||||
return type.startsWith('Z3_');
|
||||
}
|
||||
|
||||
function toEm(p) {
|
||||
if (typeof p === 'string') {
|
||||
// we've already set this, e.g. by replacing it with an expression
|
||||
return p;
|
||||
}
|
||||
let { type } = p;
|
||||
if (p.kind === 'out') {
|
||||
throw new Error(`unknown out parameter type ${JSON.stringify(p)}`);
|
||||
}
|
||||
if (p.isArray) {
|
||||
if (isZ3PointerType(type) || type === 'unsigned' || type === 'int') {
|
||||
// this works for nullables also because null coerces to 0
|
||||
return `intArrayToByteArr(${p.name} as unknown as number[])`;
|
||||
} else if (type === 'boolean') {
|
||||
return `boolArrayToByteArr(${p.name})`;
|
||||
} else {
|
||||
throw new Error(`only know how to deal with arrays of int/bool (got ${type})`);
|
||||
}
|
||||
}
|
||||
if (type in primitiveTypes) {
|
||||
type = primitiveTypes[type];
|
||||
}
|
||||
|
||||
if (['boolean', 'number', 'bigint', 'string'].includes(type)) {
|
||||
return p.name;
|
||||
}
|
||||
if (type.startsWith('Z3_')) {
|
||||
return p.name;
|
||||
}
|
||||
throw new Error(`unknown parameter type ${JSON.stringify(p)}`);
|
||||
}
|
||||
|
||||
let isInParam = p => ['in', 'in_array'].includes(p.kind);
|
||||
function wrapFunction(fn) {
|
||||
let inParams = fn.params.filter(isInParam);
|
||||
let outParams = fn.params.map((p, idx) => ({ ...p, idx })).filter(p => !isInParam(p));
|
||||
|
||||
// we'll figure out how to deal with these cases later
|
||||
let unknownInParam = inParams.find(
|
||||
p =>
|
||||
p.isPtr ||
|
||||
p.type === 'Z3_char_ptr' ||
|
||||
(p.isArray && !(isZ3PointerType(p.type) || p.type === 'unsigned' || p.type === 'int' || p.type === 'boolean')),
|
||||
);
|
||||
if (unknownInParam) {
|
||||
console.error(`skipping ${fn.name} - unknown in parameter ${JSON.stringify(unknownInParam)}`);
|
||||
return null;
|
||||
}
|
||||
|
||||
if (fn.ret === 'Z3_char_ptr') {
|
||||
console.error(`skipping ${fn.name} - returns a string or char pointer`);
|
||||
return null;
|
||||
}
|
||||
// console.error(fn.name);
|
||||
|
||||
let isAsync = asyncFns.includes(fn.name);
|
||||
let trivial =
|
||||
!['string', 'boolean'].includes(fn.ret) &&
|
||||
!fn.nullableRet &&
|
||||
outParams.length === 0 &&
|
||||
!inParams.some(p => p.type === 'string' || p.isArray || p.nullable);
|
||||
|
||||
let name = fn.name.startsWith('Z3_') ? fn.name.substring(3) : fn.name;
|
||||
|
||||
let params = inParams.map(p => {
|
||||
let type = p.type;
|
||||
if (p.isArray && p.nullable) {
|
||||
type = `(${type} | null)[]`;
|
||||
} else if (p.isArray) {
|
||||
type = `${type}[]`;
|
||||
} else if (p.nullable) {
|
||||
type = `${type} | null`;
|
||||
}
|
||||
return `${p.name}: ${type}`;
|
||||
});
|
||||
|
||||
if (trivial && isAsync) {
|
||||
// i.e. and async
|
||||
return `${name}: function (${params.join(', ')}): Promise<${fn.ret}> {
|
||||
return Mod.async_call(Mod._async_${fn.name}, ${fn.params.map(toEm).join(', ')});
|
||||
}`;
|
||||
}
|
||||
|
||||
if (trivial) {
|
||||
return `${name}: Mod._${fn.name} as ((${params.join(', ')}) => ${fn.ret})`;
|
||||
}
|
||||
|
||||
// otherwise fall back to ccall
|
||||
|
||||
let ctypes = fn.params.map(p =>
|
||||
p.kind === 'in_array' ? 'array' : p.kind === 'out_array' ? 'number' : p.isPtr ? 'number' : toEmType(p.type),
|
||||
);
|
||||
|
||||
let prefix = '';
|
||||
let infix = '';
|
||||
let rv = 'ret';
|
||||
let suffix = '';
|
||||
|
||||
let args = fn.params;
|
||||
|
||||
let arrayLengthParams = new Map();
|
||||
for (let p of inParams) {
|
||||
if (p.nullable && !p.isArray) {
|
||||
// this would be easy to implement - just map null to 0 - but nothing actually uses nullable non-array input parameters, so we can't ensure we've done it right
|
||||
console.error(`skipping ${fn.name} - nullable input parameter`);
|
||||
return null;
|
||||
}
|
||||
if (!p.isArray) {
|
||||
continue;
|
||||
}
|
||||
let { sizeIndex } = p;
|
||||
if (arrayLengthParams.has(sizeIndex)) {
|
||||
let otherParam = arrayLengthParams.get(sizeIndex);
|
||||
prefix += `
|
||||
if (${otherParam}.length !== ${p.name}.length) {
|
||||
throw new TypeError(\`${otherParam} and ${p.name} must be the same length (got \${${otherParam}.length} and \{${p.name}.length})\`);
|
||||
}
|
||||
`.trim();
|
||||
continue;
|
||||
}
|
||||
arrayLengthParams.set(sizeIndex, p.name);
|
||||
|
||||
let sizeParam = fn.params[sizeIndex];
|
||||
if (!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)) {
|
||||
throw new Error(
|
||||
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
|
||||
);
|
||||
}
|
||||
args[sizeIndex] = `${p.name}.length`;
|
||||
params[sizeIndex] = null;
|
||||
}
|
||||
|
||||
let returnType = fn.ret;
|
||||
let cReturnType = toEmType(fn.ret);
|
||||
if (outParams.length > 0) {
|
||||
let mapped = [];
|
||||
let memIdx = 0; // offset from `outAddress` where the data should get written, in units of 4 bytes
|
||||
|
||||
for (let outParam of outParams) {
|
||||
if (outParam.isArray) {
|
||||
if (isZ3PointerType(outParam.type) || outParam.type === 'unsigned') {
|
||||
let { sizeIndex } = outParam;
|
||||
|
||||
let count;
|
||||
if (arrayLengthParams.has(sizeIndex)) {
|
||||
// i.e. this is also the length of an input array
|
||||
count = args[sizeIndex];
|
||||
} else {
|
||||
let sizeParam = fn.params[sizeIndex];
|
||||
if (!(sizeParam.kind === 'in' && sizeParam.type === 'unsigned' && !sizeParam.isPtr && !sizeParam.isArray)) {
|
||||
throw new Error(
|
||||
`size index is not unsigned int (for fn ${fn.name} parameter ${sizeIndex} got ${sizeParam.type})`,
|
||||
);
|
||||
}
|
||||
count = sizeParam.name;
|
||||
}
|
||||
let outArrayAddress = `outArray_${outParam.name}`;
|
||||
prefix += `
|
||||
let ${outArrayAddress} = Mod._malloc(4 * ${count});
|
||||
try {
|
||||
`.trim();
|
||||
suffix =
|
||||
`
|
||||
} finally {
|
||||
Mod._free(${outArrayAddress});
|
||||
}
|
||||
`.trim() + suffix;
|
||||
args[outParam.idx] = outArrayAddress;
|
||||
mapped.push({
|
||||
name: outParam.name,
|
||||
read:
|
||||
`readUintArray(${outArrayAddress}, ${count})` +
|
||||
(outParam.type === 'unsigned' ? '' : `as unknown as ${outParam.type}[]`),
|
||||
type: `${outParam.type}[]`,
|
||||
});
|
||||
} else {
|
||||
console.error(`skipping ${fn.name} - out array of ${outParam.type}`);
|
||||
return null;
|
||||
}
|
||||
} else if (outParam.isPtr) {
|
||||
function setArg() {
|
||||
args[outParam.idx] = memIdx === 0 ? 'outAddress' : `outAddress + ${memIdx * 4}`;
|
||||
}
|
||||
let read, type;
|
||||
if (outParam.type === 'string') {
|
||||
read = `Mod.UTF8ToString(getOutUint(${memIdx}))`;
|
||||
setArg();
|
||||
++memIdx;
|
||||
} else if (isZ3PointerType(outParam.type)) {
|
||||
read = `getOutUint(${memIdx}) as unknown as ${outParam.type}`;
|
||||
setArg();
|
||||
++memIdx;
|
||||
} else if (outParam.type === 'unsigned') {
|
||||
read = `getOutUint(${memIdx})`;
|
||||
setArg();
|
||||
++memIdx;
|
||||
} else if (outParam.type === 'int') {
|
||||
read = `getOutInt(${memIdx})`;
|
||||
setArg();
|
||||
++memIdx;
|
||||
} else if (outParam.type === 'uint64_t') {
|
||||
if (memIdx % 2 === 1) {
|
||||
++memIdx;
|
||||
}
|
||||
read = `getOutUint64(${memIdx / 2})`;
|
||||
setArg();
|
||||
memIdx += 2;
|
||||
} else if (outParam.type === 'int64_t') {
|
||||
if (memIdx % 2 === 1) {
|
||||
++memIdx;
|
||||
}
|
||||
read = `getOutInt64(${memIdx / 2})`;
|
||||
setArg();
|
||||
memIdx += 2;
|
||||
} else {
|
||||
console.error(`skipping ${fn.name} - unknown out parameter type ${outParam.type}`);
|
||||
return null;
|
||||
}
|
||||
if (memIdx > Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / 4)) {
|
||||
// prettier-ignore
|
||||
console.error(`skipping ${fn.name} - out parameter sizes sum to ${memIdx * 4}, which is > ${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS}`);
|
||||
return null;
|
||||
}
|
||||
mapped.push({
|
||||
name: outParam.name,
|
||||
read,
|
||||
type: outParam.type,
|
||||
});
|
||||
} else {
|
||||
console.error(`skipping ${fn.name} - out param is neither pointer nor array`);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
let ignoreReturn = fn.ret === 'boolean' || fn.ret === 'void';
|
||||
if (outParams.length === 1) {
|
||||
let outParam = mapped[0];
|
||||
if (ignoreReturn) {
|
||||
returnType = outParam.type;
|
||||
rv = outParam.read;
|
||||
} else {
|
||||
returnType = `{ rv: ${fn.ret}, ${outParam.name} : ${outParam.type} }`;
|
||||
rv = `{ rv: ret, ${outParam.name} : ${outParam.read} }`;
|
||||
}
|
||||
} else {
|
||||
if (ignoreReturn) {
|
||||
returnType = `{ ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
|
||||
rv = `{ ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
|
||||
} else {
|
||||
returnType = `{ rv: ${fn.ret}, ${mapped.map(p => `${p.name} : ${p.type}`).join(', ')} }`;
|
||||
rv = `{ rv: ret, ${mapped.map(p => `${p.name}: ${p.read}`).join(', ')} }`;
|
||||
}
|
||||
}
|
||||
|
||||
if (fn.ret === 'boolean') {
|
||||
// assume the boolean indicates success
|
||||
infix += `
|
||||
if (!ret) {
|
||||
return null;
|
||||
}
|
||||
`.trim();
|
||||
cReturnType = 'boolean';
|
||||
returnType += ' | null';
|
||||
} else if (fn.ret === 'void') {
|
||||
cReturnType = 'void';
|
||||
} else if (isZ3PointerType(fn.ret) || fn.ret === 'unsigned') {
|
||||
cReturnType = 'number';
|
||||
} else {
|
||||
console.error(`skipping ${fn.name} - out parameter for function which returns non-boolean`);
|
||||
return null;
|
||||
}
|
||||
}
|
||||
|
||||
if (fn.nullableRet) {
|
||||
returnType += ' | null';
|
||||
infix += `
|
||||
if (ret === 0) {
|
||||
return null;
|
||||
}
|
||||
`.trim();
|
||||
}
|
||||
|
||||
if (isAsync) {
|
||||
}
|
||||
|
||||
// prettier-ignore
|
||||
let invocation = `Mod.ccall('${isAsync ? 'async_' : ''}${fn.name}', '${cReturnType}', ${JSON.stringify(ctypes)}, [${args.map(toEm).join(', ')}])`;
|
||||
|
||||
if (isAsync) {
|
||||
invocation = `await Mod.async_call(() => ${invocation})`;
|
||||
returnType = `Promise<${returnType}>`;
|
||||
}
|
||||
|
||||
let out = `${name}: ${isAsync ? 'async' : ''} function(${params.filter(p => p != null).join(', ')}): ${returnType} {
|
||||
${prefix}`;
|
||||
if (infix === '' && suffix === '' && rv === 'ret') {
|
||||
out += `return ${invocation};`;
|
||||
} else {
|
||||
out += `
|
||||
let ret = ${invocation};
|
||||
${infix}return ${rv};${suffix}
|
||||
`.trim();
|
||||
}
|
||||
out += '}';
|
||||
return out;
|
||||
}
|
||||
|
||||
function wrapEnum(name, values) {
|
||||
let enumEntries = Object.entries(values);
|
||||
return `export enum ${name} {
|
||||
${enumEntries.map(([k, v], i) => k + (v === (enumEntries[i - 1]?.[1] ?? -1) + 1 ? '' : ` = ${v}`) + ',').join('\n')}
|
||||
};`;
|
||||
}
|
||||
|
||||
function getValidOutArrayIndexes(size) {
|
||||
return Array.from({ length: Math.floor(BYTES_TO_ALLOCATE_FOR_OUT_PARAMS / size) }, (_, i) => i).join(' | ');
|
||||
}
|
||||
|
||||
let out = `
|
||||
// THIS FILE IS AUTOMATICALLY GENERATED BY ${path.basename(__filename)}
|
||||
// DO NOT EDIT IT BY HAND
|
||||
|
||||
// @ts-ignore no-implicit-any
|
||||
import initModule = require('./z3-built.js');
|
||||
interface Pointer<T extends string> extends Number {
|
||||
readonly __typeName: T;
|
||||
}
|
||||
interface Subpointer<T extends string, S extends string> extends Pointer<S> {
|
||||
readonly __typeName2: T;
|
||||
}
|
||||
|
||||
${Object.entries(primitiveTypes)
|
||||
.filter(e => e[0] !== 'void')
|
||||
.map(e => `type ${e[0]} = ${e[1]};`)
|
||||
.join('\n')}
|
||||
|
||||
${Object.keys(types)
|
||||
.filter(k => k.startsWith('Z3'))
|
||||
.map(makePointerType)
|
||||
.join('\n')}
|
||||
|
||||
${Object.entries(enums)
|
||||
.map(e => wrapEnum(e[0], e[1]))
|
||||
.join('\n\n')}
|
||||
|
||||
export async function init() {
|
||||
let Mod = await initModule();
|
||||
|
||||
// this works for both signed and unsigned, because JS will wrap for you when constructing the Uint32Array
|
||||
function intArrayToByteArr(ints: number[]) {
|
||||
return new Uint8Array((new Uint32Array(ints)).buffer);
|
||||
}
|
||||
|
||||
function boolArrayToByteArr(bools: boolean[]) {
|
||||
return bools.map(b => b ? 1 : 0);
|
||||
}
|
||||
|
||||
function readUintArray(address: number, count: number) {
|
||||
return Array.from(new Uint32Array(Mod.HEAPU32.buffer, address, count));
|
||||
}
|
||||
|
||||
let outAddress = Mod._malloc(${BYTES_TO_ALLOCATE_FOR_OUT_PARAMS});
|
||||
let outUintArray = (new Uint32Array(Mod.HEAPU32.buffer, outAddress, 4));
|
||||
let getOutUint = (i: ${getValidOutArrayIndexes(4)}) => outUintArray[i];
|
||||
let outIntArray = (new Int32Array(Mod.HEAPU32.buffer, outAddress, 4));
|
||||
let getOutInt = (i: ${getValidOutArrayIndexes(4)}) => outIntArray[i];
|
||||
let outUint64Array = (new BigUint64Array(Mod.HEAPU32.buffer, outAddress, 2));
|
||||
let getOutUint64 = (i: ${getValidOutArrayIndexes(8)}) => outUint64Array[i];
|
||||
let outInt64Array = (new BigInt64Array(Mod.HEAPU32.buffer, outAddress, 2));
|
||||
let getOutInt64 = (i: ${getValidOutArrayIndexes(8)}) => outInt64Array[i];
|
||||
|
||||
return {
|
||||
em: Mod,
|
||||
Z3: {
|
||||
${functions
|
||||
.map(wrapFunction)
|
||||
.filter(f => f != null)
|
||||
.join(',\n')}
|
||||
}
|
||||
};
|
||||
}
|
||||
`;
|
||||
|
||||
console.log(prettier.format(out, { singleQuote: true, parser: 'typescript' }));
|
||||
354
src/api/js/scripts/parse-api.js
Normal file
354
src/api/js/scripts/parse-api.js
Normal file
|
|
@ -0,0 +1,354 @@
|
|||
'use strict';
|
||||
|
||||
let fs = require('fs');
|
||||
let path = require('path');
|
||||
|
||||
let files = [
|
||||
'z3_api.h',
|
||||
'z3_algebraic.h',
|
||||
'z3_ast_containers.h',
|
||||
'z3_fixedpoint.h',
|
||||
'z3_fpa.h',
|
||||
'z3_optimization.h',
|
||||
'z3_polynomial.h',
|
||||
'z3_rcf.h',
|
||||
'z3_spacer.h',
|
||||
];
|
||||
|
||||
let aliases = {
|
||||
__proto__: null,
|
||||
Z3_bool: 'boolean',
|
||||
Z3_string: 'string',
|
||||
bool: 'boolean',
|
||||
signed: 'int',
|
||||
};
|
||||
|
||||
let primitiveTypes = {
|
||||
__proto__: null,
|
||||
Z3_char_ptr: 'string',
|
||||
unsigned: 'number',
|
||||
int: 'number',
|
||||
uint64_t: 'bigint',
|
||||
int64_t: 'bigint',
|
||||
double: 'number',
|
||||
float: 'number',
|
||||
};
|
||||
|
||||
let optTypes = {
|
||||
__proto__: null,
|
||||
|
||||
Z3_sort_opt: 'Z3_sort',
|
||||
Z3_ast_opt: 'Z3_ast',
|
||||
Z3_func_interp_opt: 'Z3_func_interp',
|
||||
};
|
||||
|
||||
// parse type declarations
|
||||
let types = {
|
||||
__proto__: null,
|
||||
|
||||
// these are function types I can't be bothered to parse
|
||||
Z3_error_handler: 'Z3_error_handler',
|
||||
Z3_push_eh: 'Z3_push_eh',
|
||||
Z3_pop_eh: 'Z3_pop_eh',
|
||||
Z3_fresh_eh: 'Z3_fresh_eh',
|
||||
Z3_fixed_eh: 'Z3_fixed_eh',
|
||||
Z3_eq_eh: 'Z3_eq_eh',
|
||||
Z3_final_eh: 'Z3_final_eh',
|
||||
Z3_created_eh: 'Z3_created_eh',
|
||||
};
|
||||
|
||||
let defApis = Object.create(null);
|
||||
let functions = [];
|
||||
let enums = Object.create(null);
|
||||
for (let file of files) {
|
||||
let contents = fs.readFileSync(path.join(__dirname, '..', '..', file), 'utf8');
|
||||
|
||||
// we _could_ use an actual C++ parser, which accounted for macros and everything
|
||||
// but that's super painful
|
||||
// and the files are regular enough that we can get away without it
|
||||
|
||||
// we could also do this by modifying the `update_api.py` script
|
||||
// which we should probably do eventually
|
||||
// but this is easier while this remains not upstreamed
|
||||
|
||||
// we need to parse the `def_API` stuff so we know which things are out parameters
|
||||
// unfortunately we also need to parse the actual declarations so we know the parameter names also
|
||||
let pytypes = Object.create(null);
|
||||
|
||||
let typeMatches = contents.matchAll(
|
||||
/def_Type\(\s*'(?<name>[A-Za-z0-9_]+)',\s*'(?<cname>[A-Za-z0-9_]+)',\s*'(?<pname>[A-Za-z0-9_]+)'\)/g,
|
||||
);
|
||||
for (let { groups } of typeMatches) {
|
||||
pytypes[groups.name] = groups.cname;
|
||||
}
|
||||
|
||||
// we filter first to ensure our regex isn't too strict
|
||||
let apiLines = contents.split('\n').filter(l => /def_API|extra_API/.test(l));
|
||||
for (let line of apiLines) {
|
||||
let match = line.match(
|
||||
/^\s*(?<def>def_API|extra_API) *\(\s*'(?<name>[A-Za-z0-9_]+)'\s*,\s*(?<ret>[A-Za-z0-9_]+)\s*,\s*\((?<params>((_in|_out|_in_array|_out_array|_inout_array)\([^)]+\)\s*,?\s*)*)\)\s*\)\s*$/,
|
||||
);
|
||||
if (match == null) {
|
||||
throw new Error(`failed to match def_API call ${JSON.stringify(line)}`);
|
||||
}
|
||||
let { name, ret, def } = match.groups;
|
||||
let params = match.groups.params.trim();
|
||||
let text = params;
|
||||
let parsedParams = [];
|
||||
while (true) {
|
||||
text = eatWs(text);
|
||||
({ text, match } = eat(text, /^_(?<kind>in|out|in_array|out_array|inout_array)\(/));
|
||||
if (match == null) {
|
||||
break;
|
||||
}
|
||||
let kind = match.groups.kind;
|
||||
if (kind === 'inout_array') kind = 'in_array'; // https://github.com/Z3Prover/z3/discussions/5761
|
||||
if (kind === 'in' || kind === 'out') {
|
||||
({ text, match } = expect(text, /^[A-Za-z0-9_]+/));
|
||||
parsedParams.push({ kind, type: match[0] });
|
||||
} else {
|
||||
({ text, match } = expect(text, /^(\d+),/));
|
||||
let sizeIndex = Number(match[1]);
|
||||
text = eatWs(text);
|
||||
({ text, match } = expect(text, /^[A-Za-z0-9_]+/));
|
||||
parsedParams.push({ kind, sizeIndex, type: match[0] });
|
||||
}
|
||||
({ text, match } = expect(text, /^\)/));
|
||||
text = eatWs(text);
|
||||
({ text, match } = eat(text, /^,/));
|
||||
}
|
||||
if (text !== '') {
|
||||
throw new Error(`extra text in parameter list ${JSON.stringify(text)}`);
|
||||
}
|
||||
if (name in defApis) {
|
||||
throw new Error(`multiple defApi calls for ${name}`);
|
||||
}
|
||||
defApis[name] = { params: parsedParams, ret, extra: def === 'extra_API' };
|
||||
}
|
||||
|
||||
for (let match of contents.matchAll(/DEFINE_TYPE\((?<type>[A-Za-z0-9_]+)\)/g)) {
|
||||
types[match.groups.type] = match.groups.type;
|
||||
}
|
||||
|
||||
// parse enum declarations
|
||||
for (let idx = 0; idx < contents.length; ) {
|
||||
let nextIdx = contents.indexOf('typedef enum', idx);
|
||||
if (nextIdx === -1) {
|
||||
break;
|
||||
}
|
||||
let lineStart = contents.lastIndexOf('\n', nextIdx);
|
||||
let lineEnd = contents.indexOf(';', nextIdx);
|
||||
if (lineStart === -1 || lineEnd === -1) {
|
||||
throw new Error(`could not parse enum at index ${nextIdx}`);
|
||||
}
|
||||
idx = lineEnd;
|
||||
let slice = contents.substring(lineStart, lineEnd);
|
||||
let { match, text } = eat(slice, /^\s*typedef enum\s*\{/);
|
||||
if (match === null) {
|
||||
throw new Error(`could not parse enum ${JSON.stringify(slice)}`);
|
||||
}
|
||||
let vals = Object.create(null);
|
||||
let next = 0;
|
||||
while (true) {
|
||||
let blank = true;
|
||||
while (blank) {
|
||||
({ match, text } = eat(text, /^\s*(\/\/[^\n]*\n)?/));
|
||||
blank = match[0].length > 0;
|
||||
}
|
||||
({ match, text } = eat(text, /^[A-Za-z0-9_]+/));
|
||||
if (match === null) {
|
||||
throw new Error(`could not parse enum value in ${slice}`);
|
||||
}
|
||||
let name = match[0];
|
||||
text = eatWs(text);
|
||||
|
||||
({ match, text } = eat(text, /^= *(?<val>[^\n,\s]+)/));
|
||||
if (match !== null) {
|
||||
let parsedVal = Number(match.groups.val);
|
||||
if (Object.is(parsedVal, NaN)) {
|
||||
throw new Error('unknown value ' + match.groups.val);
|
||||
}
|
||||
vals[name] = parsedVal;
|
||||
next = parsedVal;
|
||||
} else {
|
||||
vals[name] = next;
|
||||
}
|
||||
text = eatWs(text);
|
||||
({ match, text } = eat(text, /^,?\s*}/));
|
||||
if (match !== null) {
|
||||
break;
|
||||
}
|
||||
|
||||
({ match, text } = expect(text, /^,/));
|
||||
|
||||
++next;
|
||||
}
|
||||
text = eatWs(text);
|
||||
({ match, text } = expect(text, /^[A-Za-z0-9_]+/));
|
||||
if (match[0] in enums) {
|
||||
throw new Error(`duplicate enum definition ${match[0]}`);
|
||||
}
|
||||
enums[match[0]] = vals;
|
||||
text = eatWs(text);
|
||||
if (text !== '') {
|
||||
throw new Error('expected end of definition, got ' + text);
|
||||
}
|
||||
}
|
||||
|
||||
// parse function declarations
|
||||
for (let idx = 0; idx < contents.length; ) {
|
||||
let nextIdx = contents.indexOf(' Z3_API ', idx);
|
||||
if (nextIdx === -1) {
|
||||
break;
|
||||
}
|
||||
let lineStart = contents.lastIndexOf('\n', nextIdx);
|
||||
let lineEnd = contents.indexOf(';', nextIdx);
|
||||
if (lineStart === -1 || lineEnd === -1) {
|
||||
throw new Error(`could not parse definition at index ${nextIdx}`);
|
||||
}
|
||||
idx = lineEnd;
|
||||
|
||||
let slice = contents.substring(lineStart, lineEnd);
|
||||
let match = slice.match(/^\s*(?<ret>[A-Za-z0-9_]+) +Z3_API +(?<name>[A-Za-z0-9_]+)\s*\((?<params>[^)]*)\)/);
|
||||
if (match == null) {
|
||||
throw new Error(`failed to match c definition: ${JSON.stringify(slice)}`);
|
||||
}
|
||||
let { ret, name, params } = match.groups;
|
||||
let parsedParams = [];
|
||||
|
||||
if (params.trim() !== 'void') {
|
||||
for (let param of params.split(',')) {
|
||||
let paramType, paramName, isConst, isPtr, isArray;
|
||||
|
||||
let { match, text } = eat(param, /^\s*/);
|
||||
({ match, text } = eat(text, /^[A-Za-z0-9_]+/));
|
||||
if (match === null) {
|
||||
throw new Error(`failed to parse param type in ${JSON.stringify(slice)} for param ${JSON.stringify(param)}`);
|
||||
}
|
||||
paramType = match[0];
|
||||
|
||||
text = eatWs(text);
|
||||
|
||||
({ match, text } = eat(text, /^const(?![A-Za-z0-9_])/));
|
||||
isConst = match !== null;
|
||||
|
||||
({ match, text } = eat(text, /^\s*\*/));
|
||||
isPtr = match !== null;
|
||||
|
||||
text = eatWs(text);
|
||||
|
||||
if (text === '') {
|
||||
paramName = 'UNNAMED';
|
||||
isArray = false;
|
||||
} else {
|
||||
({ match, text } = eat(text, /^[A-Za-z0-9_]+/));
|
||||
if (match === null) {
|
||||
throw new Error(
|
||||
`failed to parse param name in ${JSON.stringify(slice)} for param ${JSON.stringify(param)}`,
|
||||
);
|
||||
}
|
||||
paramName = match[0];
|
||||
text = eatWs(text);
|
||||
|
||||
({ match, text } = eat(text, /^\[\]/));
|
||||
isArray = match !== null;
|
||||
|
||||
text = eatWs(text);
|
||||
|
||||
if (text !== '') {
|
||||
throw new Error(`excess text in param in ${JSON.stringify(slice)} for param ${JSON.stringify(param)}`);
|
||||
}
|
||||
}
|
||||
|
||||
if (paramType === 'Z3_string_ptr' && !isPtr) {
|
||||
paramType = 'Z3_string';
|
||||
isPtr = true;
|
||||
}
|
||||
|
||||
let nullable = false;
|
||||
if (paramType in optTypes) {
|
||||
nullable = true;
|
||||
paramType = optTypes[paramType];
|
||||
}
|
||||
|
||||
let cType = paramType;
|
||||
paramType = aliases[paramType] ?? paramType;
|
||||
|
||||
parsedParams.push({ type: paramType, cType, name: paramName, isConst, isPtr, isArray, nullable });
|
||||
}
|
||||
}
|
||||
|
||||
let nullableRet = false;
|
||||
if (ret in optTypes) {
|
||||
nullableRet = true;
|
||||
ret = optTypes[ret];
|
||||
}
|
||||
|
||||
let cRet = ret;
|
||||
ret = aliases[ret] ?? ret;
|
||||
|
||||
if (name in defApis) {
|
||||
functions.push({ ret, cRet, name, params: parsedParams, nullableRet });
|
||||
}
|
||||
// only a few things are missing `def_API`; we'll skip those
|
||||
}
|
||||
}
|
||||
|
||||
function isKnownType(t) {
|
||||
return t in enums || t in types || t in primitiveTypes || ['string', 'boolean', 'void'].includes(t);
|
||||
}
|
||||
|
||||
for (let fn of functions) {
|
||||
if (!isKnownType(fn.ret)) {
|
||||
throw new Error(`unknown type ${fn.ret}`);
|
||||
}
|
||||
let defParams = defApis[fn.name].params;
|
||||
if (fn.params.length !== defParams.length) {
|
||||
throw new Error(`parameter length mismatch for ${fn.name}`);
|
||||
}
|
||||
let idx = 0;
|
||||
for (let param of fn.params) {
|
||||
if (!isKnownType(param.type)) {
|
||||
throw new Error(`unknown type ${param.type}`);
|
||||
}
|
||||
param.kind = defParams[idx].kind;
|
||||
if (param.kind === 'in_array' || param.kind === 'out_array') {
|
||||
if (defParams[idx].sizeIndex == null) {
|
||||
throw new Error(`function ${fn.name} parameter ${idx} is marked as ${param.kind} but has no index`);
|
||||
}
|
||||
param.sizeIndex = defParams[idx].sizeIndex;
|
||||
if (!param.isArray && param.isPtr) {
|
||||
// not clear why some things are written as `int * x` and others `int x[]`
|
||||
// but we can jsut cast
|
||||
param.isArray = true;
|
||||
param.isPtr = false;
|
||||
}
|
||||
if (!param.isArray) {
|
||||
throw new Error(`function ${fn.name} parameter ${idx} is marked as ${param.kind} but not typed as array`);
|
||||
}
|
||||
}
|
||||
++idx;
|
||||
}
|
||||
}
|
||||
|
||||
function eat(str, regex) {
|
||||
const match = str.match(regex);
|
||||
if (match == null) {
|
||||
return { match, text: str };
|
||||
}
|
||||
return { match, text: str.substring(match[0].length) };
|
||||
}
|
||||
|
||||
function eatWs(text) {
|
||||
return eat(text, /^\s*/).text;
|
||||
}
|
||||
|
||||
function expect(str, regex) {
|
||||
let { text, match } = eat(str, regex);
|
||||
if (match === null) {
|
||||
throw new Error(`expected ${regex}, got ${JSON.stringify(text)}`);
|
||||
}
|
||||
return { text, match };
|
||||
}
|
||||
|
||||
module.exports = { primitiveTypes, types, enums, functions };
|
||||
38
src/api/js/src/async-wrapper.js
Normal file
38
src/api/js/src/async-wrapper.js
Normal file
|
|
@ -0,0 +1,38 @@
|
|||
// this wrapper works with async-fns to provide promise-based off-thread versions of some functions
|
||||
|
||||
let capability = null;
|
||||
function resolve_async(val) {
|
||||
// setTimeout is a workaround for https://github.com/emscripten-core/emscripten/issues/15900
|
||||
if (capability == null) {
|
||||
return;
|
||||
}
|
||||
let cap = capability;
|
||||
capability = null;
|
||||
|
||||
setTimeout(() => {
|
||||
cap.resolve(val);
|
||||
}, 0);
|
||||
}
|
||||
|
||||
function reject_async(val) {
|
||||
if (capability == null) {
|
||||
return;
|
||||
}
|
||||
let cap = capability;
|
||||
capability = null;
|
||||
|
||||
setTimeout(() => {
|
||||
cap.reject(val);
|
||||
}, 0);
|
||||
}
|
||||
|
||||
Module.async_call = function (f, ...args) {
|
||||
if (capability !== null) {
|
||||
throw new Error(`you can't execute multiple async functions at the same time; let the previous one finish first`);
|
||||
}
|
||||
let promise = new Promise((resolve, reject) => {
|
||||
capability = { resolve, reject };
|
||||
});
|
||||
f(...args);
|
||||
return promise;
|
||||
};
|
||||
392
src/api/js/test-ts-api.ts
Normal file
392
src/api/js/test-ts-api.ts
Normal file
|
|
@ -0,0 +1,392 @@
|
|||
// Some of the examples from test_capi.c.
|
||||
// Note that none of the type annotations on variable declarations are necessary:
|
||||
// TypeScript can infer all of them.
|
||||
// They're just here so readers can see what types things are.
|
||||
|
||||
import type {
|
||||
Z3_config,
|
||||
Z3_context,
|
||||
Z3_solver,
|
||||
Z3_sort,
|
||||
Z3_ast,
|
||||
Z3_app,
|
||||
Z3_model,
|
||||
Z3_symbol,
|
||||
Z3_ast_vector,
|
||||
Z3_func_decl,
|
||||
Z3_func_interp,
|
||||
Z3_func_entry,
|
||||
} from './build/wrapper';
|
||||
import { init, Z3_lbool, Z3_ast_kind, Z3_sort_kind, Z3_symbol_kind } from './build/wrapper';
|
||||
|
||||
// @ts-ignore we're not going to bother with types for this
|
||||
import { sprintf } from 'sprintf-js';
|
||||
|
||||
let printf = (str: string, ...args: unknown[]) => console.log(sprintf(str.replace(/\n$/, ''), ...args));
|
||||
|
||||
(async () => {
|
||||
let { em, Z3 } = await init();
|
||||
|
||||
function mk_context(): Z3_context {
|
||||
let cfg: Z3_config = Z3.mk_config();
|
||||
Z3.set_param_value(cfg, 'model', 'true');
|
||||
let ctx: Z3_context = Z3.mk_context(cfg);
|
||||
Z3.del_config(cfg);
|
||||
return ctx;
|
||||
}
|
||||
|
||||
function mk_proof_context(): Z3_context {
|
||||
let cfg: Z3_config = Z3.mk_config();
|
||||
let ctx: Z3_context;
|
||||
Z3.set_param_value(cfg, 'proof', 'true');
|
||||
ctx = Z3.mk_context(cfg);
|
||||
Z3.del_config(cfg);
|
||||
return ctx;
|
||||
}
|
||||
|
||||
function mk_solver(ctx: Z3_context): Z3_solver {
|
||||
let s: Z3_solver = Z3.mk_solver(ctx);
|
||||
Z3.solver_inc_ref(ctx, s);
|
||||
return s;
|
||||
}
|
||||
|
||||
function del_solver(ctx: Z3_context, s: Z3_solver) {
|
||||
Z3.solver_dec_ref(ctx, s);
|
||||
}
|
||||
|
||||
function mk_var(ctx: Z3_context, name: string, ty: Z3_sort): Z3_ast {
|
||||
let s: Z3_symbol = Z3.mk_string_symbol(ctx, name);
|
||||
return Z3.mk_const(ctx, s, ty);
|
||||
}
|
||||
|
||||
function mk_bool_var(ctx: Z3_context, name: string): Z3_ast {
|
||||
let ty: Z3_sort = Z3.mk_bool_sort(ctx);
|
||||
return mk_var(ctx, name, ty);
|
||||
}
|
||||
|
||||
function exitf(m: string) {
|
||||
console.error(`BUG: ${m}`);
|
||||
process.exit(1);
|
||||
}
|
||||
|
||||
function display_symbol(c: Z3_context, s: Z3_symbol) {
|
||||
switch (Z3.get_symbol_kind(c, s)) {
|
||||
case Z3_symbol_kind.Z3_INT_SYMBOL:
|
||||
process.stdout.write(sprintf('#%d', Z3.get_symbol_int(c, s)));
|
||||
break;
|
||||
case Z3_symbol_kind.Z3_STRING_SYMBOL:
|
||||
process.stdout.write(sprintf('%s', Z3.get_symbol_string(c, s)));
|
||||
break;
|
||||
default:
|
||||
throw new Error('unreachable');
|
||||
}
|
||||
}
|
||||
|
||||
function display_sort(c: Z3_context, ty: Z3_sort) {
|
||||
switch (Z3.get_sort_kind(c, ty)) {
|
||||
case Z3_sort_kind.Z3_UNINTERPRETED_SORT:
|
||||
display_symbol(c, Z3.get_sort_name(c, ty));
|
||||
break;
|
||||
case Z3_sort_kind.Z3_BOOL_SORT:
|
||||
process.stdout.write('bool');
|
||||
break;
|
||||
case Z3_sort_kind.Z3_INT_SORT:
|
||||
process.stdout.write('int');
|
||||
break;
|
||||
case Z3_sort_kind.Z3_REAL_SORT:
|
||||
process.stdout.write('real');
|
||||
break;
|
||||
case Z3_sort_kind.Z3_BV_SORT:
|
||||
process.stdout.write(sprintf('bv%d', Z3.get_bv_sort_size(c, ty)));
|
||||
break;
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT:
|
||||
process.stdout.write('[');
|
||||
display_sort(c, Z3.get_array_sort_domain(c, ty));
|
||||
process.stdout.write('->');
|
||||
display_sort(c, Z3.get_array_sort_range(c, ty));
|
||||
process.stdout.write(']');
|
||||
break;
|
||||
case Z3_sort_kind.Z3_DATATYPE_SORT:
|
||||
if (Z3.get_datatype_sort_num_constructors(c, ty) !== 1) {
|
||||
process.stdout.write(sprintf('%s', Z3.sort_to_string(c, ty)));
|
||||
break;
|
||||
}
|
||||
{
|
||||
let num_fields: number = Z3.get_tuple_sort_num_fields(c, ty);
|
||||
let i: number;
|
||||
process.stdout.write('(');
|
||||
for (i = 0; i < num_fields; i++) {
|
||||
let field: Z3_func_decl = Z3.get_tuple_sort_field_decl(c, ty, i);
|
||||
if (i > 0) {
|
||||
process.stdout.write(', ');
|
||||
}
|
||||
display_sort(c, Z3.get_range(c, field));
|
||||
}
|
||||
process.stdout.write(')');
|
||||
break;
|
||||
}
|
||||
default:
|
||||
process.stdout.write('unknown[');
|
||||
display_symbol(c, Z3.get_sort_name(c, ty));
|
||||
process.stdout.write(']');
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
function display_ast(c: Z3_context, v: Z3_ast) {
|
||||
switch (Z3.get_ast_kind(c, v)) {
|
||||
case Z3_ast_kind.Z3_NUMERAL_AST: {
|
||||
let t: Z3_sort;
|
||||
process.stdout.write(sprintf('%s', Z3.get_numeral_string(c, v)));
|
||||
t = Z3.get_sort(c, v);
|
||||
process.stdout.write(':');
|
||||
display_sort(c, t);
|
||||
break;
|
||||
}
|
||||
case Z3_ast_kind.Z3_APP_AST: {
|
||||
let i: number;
|
||||
let app: Z3_app = Z3.to_app(c, v);
|
||||
let num_fields: number = Z3.get_app_num_args(c, app);
|
||||
let d: Z3_func_decl = Z3.get_app_decl(c, app);
|
||||
process.stdout.write(sprintf('%s', Z3.func_decl_to_string(c, d)));
|
||||
if (num_fields > 0) {
|
||||
process.stdout.write('[');
|
||||
for (i = 0; i < num_fields; i++) {
|
||||
if (i > 0) {
|
||||
process.stdout.write(', ');
|
||||
}
|
||||
display_ast(c, Z3.get_app_arg(c, app, i));
|
||||
}
|
||||
process.stdout.write(']');
|
||||
}
|
||||
break;
|
||||
}
|
||||
case Z3_ast_kind.Z3_QUANTIFIER_AST: {
|
||||
process.stdout.write('quantifier');
|
||||
}
|
||||
default:
|
||||
process.stdout.write('#unknown');
|
||||
}
|
||||
}
|
||||
|
||||
function display_function_interpretations(c: Z3_context, m: Z3_model) {
|
||||
let num_functions: number;
|
||||
let i: number;
|
||||
|
||||
process.stdout.write('function interpretations:\n');
|
||||
|
||||
num_functions = Z3.model_get_num_funcs(c, m);
|
||||
for (i = 0; i < num_functions; i++) {
|
||||
let fdecl: Z3_func_decl;
|
||||
let name: Z3_symbol;
|
||||
let func_else: Z3_ast;
|
||||
let num_entries = 0;
|
||||
let j: number;
|
||||
let finterp: Z3_func_interp | null;
|
||||
|
||||
fdecl = Z3.model_get_func_decl(c, m, i);
|
||||
finterp = Z3.model_get_func_interp(c, m, fdecl);
|
||||
if (finterp) Z3.func_interp_inc_ref(c, finterp);
|
||||
name = Z3.get_decl_name(c, fdecl);
|
||||
display_symbol(c, name);
|
||||
process.stdout.write(' = {');
|
||||
if (finterp) num_entries = Z3.func_interp_get_num_entries(c, finterp);
|
||||
for (j = 0; j < num_entries; j++) {
|
||||
let num_args: number;
|
||||
let k: number;
|
||||
let fentry: Z3_func_entry = Z3.func_interp_get_entry(c, finterp!, j);
|
||||
Z3.func_entry_inc_ref(c, fentry);
|
||||
if (j > 0) {
|
||||
process.stdout.write(', ');
|
||||
}
|
||||
num_args = Z3.func_entry_get_num_args(c, fentry);
|
||||
process.stdout.write('(');
|
||||
for (k = 0; k < num_args; k++) {
|
||||
if (k > 0) {
|
||||
process.stdout.write(', ');
|
||||
}
|
||||
display_ast(c, Z3.func_entry_get_arg(c, fentry, k));
|
||||
}
|
||||
process.stdout.write('|->');
|
||||
display_ast(c, Z3.func_entry_get_value(c, fentry));
|
||||
process.stdout.write(')');
|
||||
Z3.func_entry_dec_ref(c, fentry);
|
||||
}
|
||||
if (num_entries > 0) {
|
||||
process.stdout.write(', ');
|
||||
}
|
||||
if (finterp) {
|
||||
process.stdout.write('(else|->');
|
||||
func_else = Z3.func_interp_get_else(c, finterp);
|
||||
display_ast(c, func_else);
|
||||
Z3.func_interp_dec_ref(c, finterp);
|
||||
}
|
||||
process.stdout.write(')}\n');
|
||||
}
|
||||
}
|
||||
function display_model(c: Z3_context, m: Z3_model | null) {
|
||||
let num_constants: number;
|
||||
let i: number;
|
||||
|
||||
if (!m) return;
|
||||
|
||||
num_constants = Z3.model_get_num_consts(c, m);
|
||||
for (i = 0; i < num_constants; i++) {
|
||||
let name: Z3_symbol;
|
||||
let cnst: Z3_func_decl = Z3.model_get_const_decl(c, m, i);
|
||||
let a: Z3_ast;
|
||||
let v: Z3_ast;
|
||||
let ok: boolean;
|
||||
name = Z3.get_decl_name(c, cnst);
|
||||
display_symbol(c, name);
|
||||
process.stdout.write(' = ');
|
||||
a = Z3.mk_app(c, cnst, []);
|
||||
v = a;
|
||||
let result = Z3.model_eval(c, m, a, true);
|
||||
ok = result != null;
|
||||
if (result != null) {
|
||||
v = result;
|
||||
}
|
||||
display_ast(c, v);
|
||||
process.stdout.write('\n');
|
||||
}
|
||||
display_function_interpretations(c, m);
|
||||
}
|
||||
|
||||
async function check(ctx: Z3_context, s: Z3_solver, expected_result: Z3_lbool) {
|
||||
let m: Z3_model | null = null;
|
||||
let result: Z3_lbool = await Z3.solver_check(ctx, s);
|
||||
switch (result) {
|
||||
case Z3_lbool.Z3_L_FALSE:
|
||||
printf('unsat\n');
|
||||
break;
|
||||
case Z3_lbool.Z3_L_UNDEF:
|
||||
printf('unknown\n');
|
||||
m = Z3.solver_get_model(ctx, s);
|
||||
if (m) Z3.model_inc_ref(ctx, m);
|
||||
printf('potential model:\n%s\n', Z3.model_to_string(ctx, m));
|
||||
break;
|
||||
case Z3_lbool.Z3_L_TRUE:
|
||||
m = Z3.solver_get_model(ctx, s);
|
||||
if (m) Z3.model_inc_ref(ctx, m);
|
||||
printf('sat\n%s\n', Z3.model_to_string(ctx, m));
|
||||
break;
|
||||
}
|
||||
if (result !== expected_result) {
|
||||
exitf('unexpected result');
|
||||
}
|
||||
if (m) Z3.model_dec_ref(ctx, m);
|
||||
}
|
||||
|
||||
// https://github.com/Z3Prover/z3/blob/174889ad5ea8b1e1127aeec8a4121a5687ac9a2b/examples/c/test_capi.c#L1440
|
||||
async function bitvector_example2() {
|
||||
let ctx: Z3_context = mk_context();
|
||||
let s: Z3_solver = mk_solver(ctx);
|
||||
|
||||
/* construct x ^ y - 103 == x * y */
|
||||
let bv_sort: Z3_sort = Z3.mk_bv_sort(ctx, 32);
|
||||
let x: Z3_ast = mk_var(ctx, 'x', bv_sort);
|
||||
let y: Z3_ast = mk_var(ctx, 'y', bv_sort);
|
||||
let x_xor_y: Z3_ast = Z3.mk_bvxor(ctx, x, y);
|
||||
let c103: Z3_ast = Z3.mk_numeral(ctx, '103', bv_sort);
|
||||
let lhs: Z3_ast = Z3.mk_bvsub(ctx, x_xor_y, c103);
|
||||
let rhs: Z3_ast = Z3.mk_bvmul(ctx, x, y);
|
||||
let ctr: Z3_ast = Z3.mk_eq(ctx, lhs, rhs);
|
||||
|
||||
printf('\nbitvector_example2\n');
|
||||
// LOG_MSG("bitvector_example2");
|
||||
printf('find values of x and y, such that x ^ y - 103 == x * y\n');
|
||||
|
||||
// /* add the constraint <tt>x ^ y - 103 == x * y<\tt> to the logical context */
|
||||
Z3.solver_assert(ctx, s, ctr);
|
||||
|
||||
// /* find a model (i.e., values for x an y that satisfy the constraint */
|
||||
await check(ctx, s, Z3_lbool.Z3_L_TRUE);
|
||||
|
||||
del_solver(ctx, s);
|
||||
Z3.del_context(ctx);
|
||||
}
|
||||
|
||||
// https://github.com/Z3Prover/z3/blob/174889ad5ea8b1e1127aeec8a4121a5687ac9a2b/examples/c/test_capi.c#L2230
|
||||
async function unsat_core_and_proof_example() {
|
||||
let ctx: Z3_context = mk_proof_context();
|
||||
let s: Z3_solver = mk_solver(ctx);
|
||||
let pa: Z3_ast = mk_bool_var(ctx, 'PredA');
|
||||
let pb: Z3_ast = mk_bool_var(ctx, 'PredB');
|
||||
let pc: Z3_ast = mk_bool_var(ctx, 'PredC');
|
||||
let pd: Z3_ast = mk_bool_var(ctx, 'PredD');
|
||||
let p1: Z3_ast = mk_bool_var(ctx, 'P1');
|
||||
let p2: Z3_ast = mk_bool_var(ctx, 'P2');
|
||||
let p3: Z3_ast = mk_bool_var(ctx, 'P3');
|
||||
let p4: Z3_ast = mk_bool_var(ctx, 'P4');
|
||||
let assumptions: Z3_ast[] = [Z3.mk_not(ctx, p1), Z3.mk_not(ctx, p2), Z3.mk_not(ctx, p3), Z3.mk_not(ctx, p4)];
|
||||
let args1: Z3_ast[] = [pa, pb, pc];
|
||||
let f1 = Z3.mk_and(ctx, args1);
|
||||
let args2: Z3_ast[] = [pa, Z3.mk_not(ctx, pb), pc];
|
||||
let f2 = Z3.mk_and(ctx, args2);
|
||||
let args3: Z3_ast[] = [Z3.mk_not(ctx, pa), Z3.mk_not(ctx, pc)];
|
||||
let f3 = Z3.mk_or(ctx, args3);
|
||||
let f4 = pd;
|
||||
let g1: Z3_ast[] = [f1, p1];
|
||||
let g2: Z3_ast[] = [f2, p2];
|
||||
let g3: Z3_ast[] = [f3, p3];
|
||||
let g4: Z3_ast[] = [f4, p4];
|
||||
let result: Z3_lbool;
|
||||
let proof: Z3_ast;
|
||||
let m: Z3_model | null = null;
|
||||
let i: number;
|
||||
let core: Z3_ast_vector;
|
||||
|
||||
printf('\nunsat_core_and_proof_example\n');
|
||||
// LOG_MSG("unsat_core_and_proof_example");
|
||||
|
||||
Z3.solver_assert(ctx, s, Z3.mk_or(ctx, g1));
|
||||
Z3.solver_assert(ctx, s, Z3.mk_or(ctx, g2));
|
||||
Z3.solver_assert(ctx, s, Z3.mk_or(ctx, g3));
|
||||
Z3.solver_assert(ctx, s, Z3.mk_or(ctx, g4));
|
||||
|
||||
result = await Z3.solver_check_assumptions(ctx, s, assumptions);
|
||||
|
||||
switch (result) {
|
||||
case Z3_lbool.Z3_L_FALSE:
|
||||
core = Z3.solver_get_unsat_core(ctx, s);
|
||||
proof = Z3.solver_get_proof(ctx, s);
|
||||
printf('unsat\n');
|
||||
printf('proof: %s\n', Z3.ast_to_string(ctx, proof));
|
||||
|
||||
printf('\ncore:\n');
|
||||
for (i = 0; i < Z3.ast_vector_size(ctx, core); ++i) {
|
||||
printf('%s\n', Z3.ast_to_string(ctx, Z3.ast_vector_get(ctx, core, i)));
|
||||
}
|
||||
printf('\n');
|
||||
break;
|
||||
case Z3_lbool.Z3_L_UNDEF:
|
||||
printf('unknown\n');
|
||||
printf('potential model:\n');
|
||||
m = Z3.solver_get_model(ctx, s);
|
||||
if (m) Z3.model_inc_ref(ctx, m);
|
||||
display_model(ctx, m);
|
||||
throw new Error('result was undef, should have been unsat');
|
||||
case Z3_lbool.Z3_L_TRUE:
|
||||
printf('sat\n');
|
||||
m = Z3.solver_get_model(ctx, s);
|
||||
if (m) Z3.model_inc_ref(ctx, m);
|
||||
display_model(ctx, m);
|
||||
throw new Error('result was sat, should have been unsat');
|
||||
}
|
||||
|
||||
/* delete logical context */
|
||||
if (m) Z3.model_dec_ref(ctx, m);
|
||||
del_solver(ctx, s);
|
||||
Z3.del_context(ctx);
|
||||
}
|
||||
|
||||
await bitvector_example2();
|
||||
await unsat_core_and_proof_example();
|
||||
|
||||
// shut down
|
||||
em.PThread.terminateAllThreads();
|
||||
})().catch(e => {
|
||||
console.error('error', e);
|
||||
process.exit(1);
|
||||
});
|
||||
14
src/api/js/tsconfig.json
Normal file
14
src/api/js/tsconfig.json
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
{
|
||||
"compilerOptions": {
|
||||
"target": "es2021",
|
||||
"module": "commonjs",
|
||||
"esModuleInterop": true,
|
||||
"declaration": true,
|
||||
"forceConsistentCasingInFileNames": true,
|
||||
"strict": true,
|
||||
"skipLibCheck": true
|
||||
},
|
||||
"exclude": [
|
||||
"src"
|
||||
]
|
||||
}
|
||||
Loading…
Reference in a new issue