mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-27 22:33:35 +00:00
Code Activity

Revert "Typescript typedef and doc fixes (#8073)" (#8077)

Browse source 
This reverts commit 6cfbcd19df.
This commit is contained in:
Nikolaj Bjorner 2025-12-15 17:38:04 +00:00
parent 13204421e7
commit e2d568f32b
2 changed files with 2 additions and 3 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,7 +125,6 @@ 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 } from 'z3-solver'; * import { init, sat } 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();