diff --git a/src/api/js/examples/high-level/miracle-sudoku.ts b/src/api/js/examples/high-level/miracle-sudoku.ts index 763581ae7..c42c04a95 100644 --- a/src/api/js/examples/high-level/miracle-sudoku.ts +++ b/src/api/js/examples/high-level/miracle-sudoku.ts @@ -157,7 +157,9 @@ function parseSudoku(str: string) { async function solve(str: string) { let solver = new Z3.Solver(); - let cells = Array.from({ length: 9 }, (_, col) => Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`))); + let cells = Array.from({ length: 9 }, (_, col) => + Array.from({ length: 9 }, (_, row) => Z3.Int.const(`c_${row}_${col}`)), + ); for (let { row, col, value } of parseSudoku(str)) { solver.add(cells[row][col].eq(value)); } diff --git a/src/api/js/examples/high-level/using_smtlib2.ts b/src/api/js/examples/high-level/using_smtlib2.ts index e9275b7bf..7faf7063d 100644 --- a/src/api/js/examples/high-level/using_smtlib2.ts +++ b/src/api/js/examples/high-level/using_smtlib2.ts @@ -25,12 +25,11 @@ import assert from 'assert'; const model = solver.model(); let modelStr = model.sexpr(); modelStr = modelStr.replace(/\n/g, ' '); - console.log("Model: ", modelStr); + console.log('Model: ', modelStr); const exprs = z3.ast_from_string(modelStr); console.log(exprs); - })().catch(e => { console.error('error', e); process.exit(1); -}); \ No newline at end of file +}); diff --git a/src/api/js/examples/low-level/example-raw.ts b/src/api/js/examples/low-level/example-raw.ts index 68e7997e6..4cdb075ab 100644 --- a/src/api/js/examples/low-level/example-raw.ts +++ b/src/api/js/examples/low-level/example-raw.ts @@ -59,7 +59,9 @@ import { init, Z3_error_code } from '../../build/node.js'; console.log('confirming error messages work:', Z3.get_error_msg(ctx, Z3.get_error_code(ctx))); Z3.global_param_set('verbose', '0'); - let result = await Z3.eval_smtlib2_string(ctx, ` + let result = await Z3.eval_smtlib2_string( + ctx, + ` (declare-const p Bool) (declare-const q Bool) (declare-const r Bool) @@ -68,7 +70,8 @@ import { init, Z3_error_code } from '../../build/node.js'; (assert ((_ pbeq 5 2 1 3 3 2) p q r s t)) (check-sat) (get-model) - `); + `, + ); console.log('checking string evaluation', result); Z3.dec_ref(ctx, strAst); diff --git a/src/api/js/package-lock.json b/src/api/js/package-lock.json index 432e00568..3e3911ec6 100644 --- a/src/api/js/package-lock.json +++ b/src/api/js/package-lock.json @@ -14,13 +14,12 @@ "devDependencies": { "@types/jest": "^27.5.1", "@types/node": "^17.0.8", - "@types/prettier": "^2.6.1", "@types/sprintf-js": "^1.1.2", "check-engine": "^1.10.1", "iter-tools": "^7.3.1", "jest": "^28.1.0", "npm-run-all": "^4.1.5", - "prettier": "^2.5.1", + "prettier": "^3.4.2", "rimraf": "^3.0.2", "sprintf-js": "^1.1.2", "ts-expect": "^1.3.0", @@ -5880,15 +5879,16 @@ } }, "node_modules/prettier": { - "version": "2.7.1", - "resolved": "https://registry.npmjs.org/prettier/-/prettier-2.7.1.tgz", - "integrity": "sha512-ujppO+MkdPqoVINuDFDRLClm7D78qbDt0/NR+wp5FqEZOoTNAjPHWj17QRhu7geIHJfcNhRk1XVQmF8Bp3ye+g==", + "version": "3.4.2", + "resolved": "https://registry.npmjs.org/prettier/-/prettier-3.4.2.tgz", + "integrity": "sha512-e9MewbtFo+Fevyuxn/4rrcDAaq0IYxPGLvObpQjiZBMAzB9IGmzlnG9RZy3FFas+eBMu2vA0CszMeduow5dIuQ==", "dev": true, + "license": "MIT", "bin": { - "prettier": "bin-prettier.js" + "prettier": "bin/prettier.cjs" }, "engines": { - "node": ">=10.13.0" + "node": ">=14" }, "funding": { "url": "https://github.com/prettier/prettier?sponsor=1" diff --git a/src/api/js/package.json b/src/api/js/package.json index bc6e006d4..e272ad456 100644 --- a/src/api/js/package.json +++ b/src/api/js/package.json @@ -42,13 +42,12 @@ "devDependencies": { "@types/jest": "^27.5.1", "@types/node": "^17.0.8", - "@types/prettier": "^2.6.1", "@types/sprintf-js": "^1.1.2", "check-engine": "^1.10.1", "iter-tools": "^7.3.1", "jest": "^28.1.0", "npm-run-all": "^4.1.5", - "prettier": "^2.5.1", + "prettier": "^3.4.2", "rimraf": "^3.0.2", "sprintf-js": "^1.1.2", "ts-expect": "^1.3.0", diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts index a5b57ee3f..970ed06f0 100644 --- a/src/api/js/scripts/build-wasm.ts +++ b/src/api/js/scripts/build-wasm.ts @@ -40,7 +40,13 @@ function spawnSync(command: string, opts: SpawnOptions = {}) { } function exportedFuncs(): string[] { - const extras = ['_malloc', '_free', '_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFuncs.map(f => '_async_' + f)]; + const extras = [ + '_malloc', + '_free', + '_set_throwy_error_handler', + '_set_noop_error_handler', + ...asyncFuncs.map(f => '_async_' + f), + ]; // TODO(ritave): This variable is unused in original script, find out if it's important const fns: any[] = (functions as any[]).filter(f => !asyncFuncs.includes(f.name)); diff --git a/src/api/js/scripts/make-ts-wrapper.ts b/src/api/js/scripts/make-ts-wrapper.ts index 6eb81c806..277684d2b 100644 --- a/src/api/js/scripts/make-ts-wrapper.ts +++ b/src/api/js/scripts/make-ts-wrapper.ts @@ -10,7 +10,7 @@ assert(process.argv.length === 4, `Usage: ${process.argv[0]} ${process.argv[1]} const wrapperFilePath = process.argv[2]; const typesFilePath = process.argv[3]; -function makeTsWrapper() { +async function makeTsWrapper() { const subtypes = { __proto__: null, Z3_sort: 'Z3_ast', @@ -464,13 +464,18 @@ export async function init(initModule: any) { `; return { - wrapperDocument: prettier.format(wrapperDocument, { singleQuote: true, parser: 'typescript' }), - typesDocument: prettier.format(typesDocument, { singleQuote: true, parser: 'typescript' }), + wrapperDocument: await prettier.format(wrapperDocument, { singleQuote: true, parser: 'typescript' }), + typesDocument: await prettier.format(typesDocument, { singleQuote: true, parser: 'typescript' }), }; } -const { wrapperDocument, typesDocument } = makeTsWrapper(); -fs.mkdirSync(path.dirname(wrapperFilePath), { recursive: true }); -fs.writeFileSync(wrapperFilePath, wrapperDocument); -fs.mkdirSync(path.dirname(typesFilePath), { recursive: true }); -fs.writeFileSync(typesFilePath, typesDocument); +(async () => { + const { wrapperDocument, typesDocument } = await makeTsWrapper(); + fs.mkdirSync(path.dirname(wrapperFilePath), { recursive: true }); + fs.writeFileSync(wrapperFilePath, wrapperDocument); + fs.mkdirSync(path.dirname(typesFilePath), { recursive: true }); + fs.writeFileSync(typesFilePath, typesDocument); +})().catch(e => { + console.error(e); + process.exit(1); +}); diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index b3ed6e82f..fb8805d99 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -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(); }); }); - }); diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 02b95951e..a9bad4125 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -37,6 +37,7 @@ export type AnyExpr = export type AnyAst = AnyExpr | AnySort | FuncDecl; /** @hidden */ +// prettier-ignore export type SortToExprMap, Name extends string = 'main'> = S extends BoolSort ? Bool : S extends ArithSort @@ -50,6 +51,7 @@ export type SortToExprMap, Name extends string = 'main'> : never; /** @hidden */ +// prettier-ignore export type CoercibleFromMap, Name extends string = 'main'> = S extends bigint ? Arith : S extends number | CoercibleRational @@ -75,6 +77,7 @@ export type CoercibleToExpr = number | bigint | bo export type CoercibleToArith = number | string | bigint | CoercibleRational | Arith; /** @hidden */ +// prettier-ignore export type CoercibleToMap, Name extends string = 'main'> = T extends Bool ? boolean | Bool : T extends IntNum @@ -1656,6 +1659,7 @@ export interface SMTSet = [Sort, ...Sort[]], diff --git a/src/api/js/src/low-level/index.ts b/src/api/js/src/low-level/index.ts index 4a842bab6..1791eae27 100644 --- a/src/api/js/src/low-level/index.ts +++ b/src/api/js/src/low-level/index.ts @@ -1,4 +1,4 @@ export * from './types.__GENERATED__'; export * from './wrapper.__GENERATED__'; -export type Z3Core = Awaited>['Z3']; -export type Z3LowLevel = Awaited>; +export type Z3Core = Awaited>['Z3']; +export type Z3LowLevel = Awaited>;