mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

update prettier

Browse source
This commit is contained in:
Kevin Gibbons 2024-12-06 12:30:09 -08:00
parent 2d903aae87
commit d93a8fd3f0
10 changed files with 49 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/js/examples/high-level/miracle-sudoku.ts
View file

@ -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));
}

5
src/api/js/examples/high-level/using_smtlib2.ts
View file

@ -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);
});
});

7
src/api/js/examples/low-level/example-raw.ts
View file

@ -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);

14
src/api/js/package-lock.json generated
View file

@ -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"

3
src/api/js/package.json
View file

@ -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",

8
src/api/js/scripts/build-wasm.ts
View file

@ -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));

21
src/api/js/scripts/make-ts-wrapper.ts
View file

@ -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);
});

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();
});
});
});

4
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
@ -75,6 +77,7 @@ export type CoercibleToExpr<Name extends string = 'main'> = number | bigint | bo
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>[]],

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']>>;