mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-25 13:36:53 +00:00
Code Activity

Typescript typedef and doc fixes (#8073)

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 09:03:41 -08:00 • committed by GitHub
parent 0076e3bf97
commit 6cfbcd19df
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -125,6 +125,7 @@ export type CheckSatResult = 'sat' | 'unsat' | 'unknown';
/** @hidden */
export interface ContextCtor {
<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'> {

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
*
* ```typescript
* import { init, sat } from 'z3-solver';
* import { init } from 'z3-solver';
*
* const { Context } = await init();
* const { Solver, Int } = new Context('main');
@ -22,7 +22,7 @@ export * from './low-level/types.__GENERATED__';
* const solver = new Solver();
* 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")
* }
* const model = solver.model();