JS/TS: add Optimize class (#6712)

* implement  Optimize class for the high level Typescript API

* javascript and wasm: add _malloc to exported functions

fix the bug https://github.com/Z3Prover/z3/issues/6709

* javascript: add tests for the Optimize class

* javascript: no reason that minimize and optimize must be constants

src/api/js/scripts/build-wasm.ts

@@ -40,7 +40,7 @@ function spawnSync(command: string, opts: SpawnOptions = {}) {
 }
 
 function exportedFuncs(): string[] {
-  const extras = ['_set_throwy_error_handler', '_set_noop_error_handler', ...asyncFuncs.map(f => '_async_' + f)];
+  const extras = ['_malloc', '_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));

src/api/js/src/high-level/high-level.test.ts

@@ -698,4 +698,51 @@ describe('high-level', () => {
       expect(m.eval(f.call(0, 0)).eqIdentity(Int.val(0))).toBeTruthy();
     });
   });
+
+  describe('optimize', () => {
+    it("maximization problem over reals", async () => {
+      const { Real, Optimize } = api.Context('main');
+
+      const opt = new Optimize();
+      const x = Real.const('x');
+      const y = Real.const('y');
+      const z = Real.const('z');
+
+      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)))
+
+      const result = await opt.check()
+      expect(result).toStrictEqual('sat');
+      const model = opt.model();
+      expect(model.eval(x).eqIdentity(Real.val(1))).toBeTruthy();
+      expect(model.eval(y).eqIdentity(Real.val(1))).toBeTruthy();
+      expect(model.eval(z).eqIdentity(Real.val(0))).toBeTruthy();
+    });
+
+    it("minimization problem over integers using addSoft", async () => {
+      const { Int, Optimize } = api.Context('main');
+
+      const opt = new Optimize();
+      const x = Int.const('x');
+      const y = Int.const('y');
+      const z = Int.const('z');
+
+      opt.add(x.ge(0), y.ge(0));
+      opt.add(x.le(1), y.le(1));
+      opt.addSoft(x.eq(1), 2);
+      opt.addSoft(y.eq(1), 1);
+      opt.add(z.eq(x.mul(5).add(y.mul(5))));
+      opt.add(z.le(5));
+      opt.minimize(z);
+
+      const result = await opt.check()
+      expect(result).toStrictEqual('sat');
+      const model = opt.model();
+      expect(model.eval(x).eqIdentity(Int.val(1))).toBeTruthy();
+      expect(model.eval(y).eqIdentity(Int.val(0))).toBeTruthy();
+      expect(model.eval(z).eqIdentity(Int.val(5))).toBeTruthy();
+    });
+  });
+
 });

src/api/js/src/high-level/high-level.ts

@@ -35,6 +35,7 @@ import {
   Z3_app,
   Z3_params,
   Z3_func_entry,
+  Z3_optimize,
 } from '../low-level';
 import {
   AnyAst,
@@ -68,6 +69,7 @@ import {
   FuncInterp,
   IntNum,
   Model,
+  Optimize,
   Pattern,
   Probe,
   Quantifier,
@@ -1327,6 +1329,102 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    class OptimizeImpl implements Optimize<Name> {
+      declare readonly __typename: Optimize['__typename'];
+
+      readonly ptr: Z3_optimize;
+      readonly ctx: Context<Name>;
+
+      constructor(ptr: Z3_optimize = Z3.mk_optimize(contextPtr)) {
+        this.ctx = ctx;
+        let myPtr: Z3_optimize;
+        myPtr = ptr;
+        this.ptr = myPtr;
+        Z3.optimize_inc_ref(contextPtr, myPtr);
+        cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr));
+      }
+
+      set(key: string, value: any): void {
+        Z3.optimize_set_params(contextPtr, this.ptr, _toParams(key, value));
+      }
+
+      push() {
+        Z3.optimize_push(contextPtr, this.ptr);
+      }
+
+      pop() {
+        Z3.optimize_pop(contextPtr, this.ptr);
+      }
+
+      add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]) {
+        _flattenArgs(exprs).forEach(expr => {
+          _assertContext(expr);
+          check(Z3.optimize_assert(contextPtr, this.ptr, expr.ast));
+        });
+      }
+
+      addSoft(expr: Bool<Name>, weight: number | bigint | string | CoercibleRational, id: number | string = "") {
+        if (isCoercibleRational(weight)) {
+          weight = `${weight.numerator}/${weight.denominator}`;
+        }
+        check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id)))
+      }
+
+      addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string) {
+        if (typeof constant === 'string') {
+          constant = Bool.const(constant);
+        }
+        assert(isConst(constant), 'Provided expression that is not a constant to addAndTrack');
+        check(Z3.optimize_assert_and_track(contextPtr, this.ptr, expr.ast, constant.ast));
+      }
+
+      assertions(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr)));
+      }
+
+      maximize(expr: Arith<Name>) {
+        check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast));
+      }
+
+      minimize(expr: Arith<Name>) {
+        check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast));
+      }
+
+      async check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult> {
+        const assumptions = _flattenArgs(exprs).map(expr => {
+          _assertContext(expr);
+          return expr.ast;
+        });
+        const result = await asyncMutex.runExclusive(() =>
+          check(Z3.optimize_check(contextPtr, this.ptr, assumptions)),
+        );
+        switch (result) {
+          case Z3_lbool.Z3_L_FALSE:
+            return 'unsat';
+          case Z3_lbool.Z3_L_TRUE:
+            return 'sat';
+          case Z3_lbool.Z3_L_UNDEF:
+            return 'unknown';
+          default:
+            assertExhaustive(result);
+        }
+      }
+
+      model() {
+        return new ModelImpl(check(Z3.optimize_get_model(contextPtr, this.ptr)));
+      }
+
+      toString() {
+        return check(Z3.optimize_to_string(contextPtr, this.ptr));
+      }
+
+      fromString(s: string) {
+        Z3.optimize_from_string(contextPtr, this.ptr, s);
+        throwIfError();
+      }
+    }
+
+
     class ModelImpl implements Model<Name> {
       declare readonly __typename: Model['__typename'];
       readonly ctx: Context<Name>;
@@ -2671,6 +2769,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       // Classes //
       /////////////
       Solver: SolverImpl,
+      Optimize: OptimizeImpl,
       Model: ModelImpl,
       Tactic: TacticImpl,
       AstVector: AstVectorImpl as AstVectorCtor<Name>,

src/api/js/src/high-level/types.ts

@@ -10,6 +10,7 @@ import {
   Z3_model,
   Z3_probe,
   Z3_solver,
+  Z3_optimize,
   Z3_sort,
   Z3_sort_kind,
   Z3_tactic,
@@ -317,6 +318,9 @@ export interface Context<Name extends string = 'main'> {
    * @category Classes
    */
   readonly Solver: new (logic?: string) => Solver<Name>;
+
+  readonly Optimize: new () => Optimize<Name>;
+
   /**
    * Creates an empty Model
    * @see {@link Solver.model} for common usage of Model
@@ -661,6 +665,39 @@ export interface Solver<Name extends string = 'main'> {
   model(): Model<Name>;
 }
 
+export interface Optimize<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'Optimize';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_optimize;
+
+  set(key: string, value: any): void;
+
+  push(): void;
+
+  pop(num?: number): void;
+
+  add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void;
+
+  addSoft(expr: Bool<Name>, weight: number | bigint | string | CoercibleRational, id?: number | string): void;
+
+  addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string): void;
+
+  assertions(): AstVector<Name, Bool<Name>>;
+
+  fromString(s: string): void;
+
+  maximize(expr: Arith<Name>): void;
+
+  minimize(expr: Arith<Name>): void;
+
+  check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
+
+  model(): Model<Name>;
+}
+
+
 /** @hidden */
 export interface ModelCtor<Name extends string> {
   new (): Model<Name>;