mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 01:01:19 +00:00
Code Activity

Update emscripten (#7473)

Browse source 
* fixes for newer emscripten thread handling behavior

* fix return type for async wrapper functions

* update prettier

* update typescript and fix errors

* update emscripten version in CI

* update js readme about tests
This commit is contained in:
Kevin Gibbons 2024-12-06 18:11:14 -08:00 • committed by GitHub
parent 4fbf54afd0
commit e5f8327483
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
17 changed files with 275 additions and 108 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/api/js/src/high-level/high-level.test.ts
View file

@ -374,7 +374,6 @@ describe('high-level', () => {
});
});
describe('bitvectors', () => {
it('can do simple proofs', async () => {
const { BitVec, Concat, Implies, isBitVecVal } = api.Context('main');
@ -413,7 +412,6 @@ describe('high-level', () => {
});
});
describe('arrays', () => {
it('Example 1', async () => {
const Z3 = api.Context('main');
@ -848,7 +846,7 @@ describe('high-level', () => {
});
describe('optimize', () => {
it("maximization problem over reals", async () => {
it('maximization problem over reals', async () => {
const { Real, Optimize } = api.Context('main');
const opt = new Optimize();
@ -858,9 +856,9 @@ describe('high-level', () => {
opt.add(x.ge(0), y.ge(0), z.ge(0));
opt.add(x.le(1), y.le(1), z.le(1));
opt.maximize(x.mul(7).add(y.mul(9)).sub(z.mul(3)))
opt.maximize(x.mul(7).add(y.mul(9)).sub(z.mul(3)));
const result = await opt.check()
const result = await opt.check();
expect(result).toStrictEqual('sat');
const model = opt.model();
expect(model.eval(x).eqIdentity(Real.val(1))).toBeTruthy();
@ -868,7 +866,7 @@ describe('high-level', () => {
expect(model.eval(z).eqIdentity(Real.val(0))).toBeTruthy();
});
it("minimization problem over integers using addSoft", async () => {
it('minimization problem over integers using addSoft', async () => {
const { Int, Optimize } = api.Context('main');
const opt = new Optimize();
@ -884,7 +882,7 @@ describe('high-level', () => {
opt.add(z.le(5));
opt.minimize(z);
const result = await opt.check()
const result = await opt.check();
expect(result).toStrictEqual('sat');
const model = opt.model();
expect(model.eval(x).eqIdentity(Int.val(1))).toBeTruthy();
@ -892,5 +890,4 @@ describe('high-level', () => {
expect(model.eval(z).eqIdentity(Int.val(5))).toBeTruthy();
});
});
});

2
src/api/js/src/high-level/high-level.ts
View file

@ -741,7 +741,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
},
val<Bits extends number>(
value: bigint | number | boolean,
value: bigint | number | boolean | string,
bits: Bits | BitVecSort<Bits, Name>,
): BitVecNum<Bits, Name> {
if (value === true) {

6
src/api/js/src/high-level/types.ts
View file

@ -37,6 +37,7 @@ export type AnyExpr<Name extends string = 'main'> =
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
/** @hidden */
// prettier-ignore
export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'> = S extends BoolSort
? Bool<Name>
: S extends ArithSort<Name>
@ -50,6 +51,7 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'>
: never;
/** @hidden */
// prettier-ignore
export type CoercibleFromMap<S extends CoercibleToExpr<Name>, Name extends string = 'main'> = S extends bigint
? Arith<Name>
: S extends number | CoercibleRational
@ -69,12 +71,13 @@ export type CoercibleToBitVec<Bits extends number = number, Name extends string
export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
/** @hidden */
export type CoercibleToExpr<Name extends string = 'main'> = number | bigint | boolean | CoercibleRational | Expr<Name>;
export type CoercibleToExpr<Name extends string = 'main'> = number | string | bigint | boolean | CoercibleRational | Expr<Name>;
/** @hidden */
export type CoercibleToArith<Name extends string = 'main'> = number | string | bigint | CoercibleRational | Arith<Name>;
/** @hidden */
// prettier-ignore
export type CoercibleToMap<T extends AnyExpr<Name>, Name extends string = 'main'> = T extends Bool<Name>
? boolean | Bool<Name>
: T extends IntNum<Name>
@ -1656,6 +1659,7 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
*
* @category Quantifiers
*/
// prettier-ignore
export type BodyT<
Name extends string = 'main',
QVarSorts extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],

2
src/api/js/src/low-level/async-wrapper.js
View file

@ -1,6 +1,8 @@
// this wrapper works with async-fns to provide promise-based off-thread versions of some functions
// It's prepended directly by emscripten to the resulting z3-built.js
let threadTimeouts = [];
let capability = null;
function resolve_async(val) {
// setTimeout is a workaround for https://github.com/emscripten-core/emscripten/issues/15900

4
src/api/js/src/low-level/index.ts
View file

@ -1,4 +1,4 @@
export * from './types.__GENERATED__';
export * from './wrapper.__GENERATED__';
export type Z3Core = Awaited<ReturnType<typeof import('./wrapper.__GENERATED__')['init']>>['Z3'];
export type Z3LowLevel = Awaited<ReturnType<typeof import('./wrapper.__GENERATED__')['init']>>;
export type Z3Core = Awaited<ReturnType<(typeof import('./wrapper.__GENERATED__'))['init']>>['Z3'];
export type Z3LowLevel = Awaited<ReturnType<(typeof import('./wrapper.__GENERATED__'))['init']>>;