mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-26 18:15:37 +00:00
Code Activity

Improve TypeScript Optimize documentation for handle index clarity

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-24 17:28:45 +00:00
parent 9802b32a3e
commit ce04a24348
2 changed files with 25 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

@ -2142,7 +2142,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
proof(): Expr<Name> | null {
const result = Z3.solver_get_proof(contextPtr, this.ptr);
throwIfError();
if (result === null) {
if (!result) {
return null;
}
return _toExpr(result);

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

@ -1478,14 +1478,36 @@ export interface Optimize<Name extends string = 'main'> {
/**
* Add a maximization objective.
* @param expr - The expression to maximize
* @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
* @returns A zero-based numeric handle index for this objective, used to retrieve bounds
* via {@link getLower}/{@link getUpper} after calling {@link check}
*
* @example
* ```typescript
* const opt = new Optimize();
* const x = Int.const('x');
* opt.add(x.ge(0), x.le(10));
* const h = opt.maximize(x);
* await opt.check();
* console.log('Max x:', opt.getUpper(h).toString()); // '10'
* ```
*/
maximize(expr: Arith<Name> | BitVec<number, Name>): number;
/**
* Add a minimization objective.
* @param expr - The expression to minimize
* @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
* @returns A zero-based numeric handle index for this objective, used to retrieve bounds
* via {@link getLower}/{@link getUpper} after calling {@link check}
*
* @example
* ```typescript
* const opt = new Optimize();
* const x = Int.const('x');
* opt.add(x.ge(0), x.le(10));
* const h = opt.minimize(x);
* await opt.check();
* console.log('Min x:', opt.getLower(h).toString()); // '0'
* ```
*/
minimize(expr: Arith<Name> | BitVec<number, Name>): number;