mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-02 16:43:45 +00:00
Code Activity

Typescript typedef and doc fixes take 2 (#8078)

Browse source 
* Fix Typescript typedef to allow `new Context`

* fix init() tsdoc example using nonexistent sat import
This commit is contained in:
Chris Cowan 2025-12-15 12:31:20 -08:00 • committed by Nikolaj Bjorner
parent e2d568f32b
commit d3d770938b
3 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -3309,6 +3309,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
setParam, setParam,
resetParams, resetParams,
Context: createContext, Context: createContext as ContextCtor,
}; };
} }

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

@ -125,6 +125,7 @@ export type CheckSatResult = 'sat' | 'unsat' | 'unknown';
/** @hidden */ /** @hidden */
export interface ContextCtor { export interface ContextCtor {
<Name extends string>(name: Name, options?: Record<string, any>): Context<Name>; <Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
new <Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
} }
export interface Context<Name extends string = 'main'> { export interface Context<Name extends string = 'main'> {

4
src/api/js/src/node.ts
View file

@ -11,7 +11,7 @@ export * from './low-level/types.__GENERATED__';
* The main entry point to the Z3 API * The main entry point to the Z3 API
* *
* ```typescript * ```typescript
* import { init, sat } from 'z3-solver'; * import { init } from 'z3-solver';
* *
* const { Context } = await init(); * const { Context } = await init();
* const { Solver, Int } = new Context('main'); * const { Solver, Int } = new Context('main');
@ -22,7 +22,7 @@ export * from './low-level/types.__GENERATED__';
* const solver = new Solver(); * const solver = new Solver();
* solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10 * solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10
* *
* if (await solver.check() !== sat) { * if (await solver.check() !== 'sat') {
* throw new Error("couldn't find a solution") * throw new Error("couldn't find a solution")
* } * }
* const model = solver.model(); * const model = solver.model();