diff --git a/src/api/js/scripts/build-wasm.ts b/src/api/js/scripts/build-wasm.ts index 3caf643df51..0f51c84d3ee 100644 --- a/src/api/js/scripts/build-wasm.ts +++ b/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)); diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index d4207516982..99f95e5b4c6 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/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(); + }); + }); + }); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 80f89b104eb..0869dbd7b46 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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 { + declare readonly __typename: Optimize['__typename']; + + readonly ptr: Z3_optimize; + readonly ctx: Context; + + 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 | AstVector>)[]) { + _flattenArgs(exprs).forEach(expr => { + _assertContext(expr); + check(Z3.optimize_assert(contextPtr, this.ptr, expr.ast)); + }); + } + + addSoft(expr: Bool, 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, constant: Bool | 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> { + return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr))); + } + + maximize(expr: Arith) { + check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast)); + } + + minimize(expr: Arith) { + check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast)); + } + + async check(...exprs: (Bool | AstVector>)[]): Promise { + 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 { declare readonly __typename: Model['__typename']; readonly ctx: Context; @@ -2671,6 +2769,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { // Classes // ///////////// Solver: SolverImpl, + Optimize: OptimizeImpl, Model: ModelImpl, Tactic: TacticImpl, AstVector: AstVectorImpl as AstVectorCtor, diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index c4b56044208..6f3630a6db5 100644 --- a/src/api/js/src/high-level/types.ts +++ b/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 { * @category Classes */ readonly Solver: new (logic?: string) => Solver; + + readonly Optimize: new () => Optimize; + /** * Creates an empty Model * @see {@link Solver.model} for common usage of Model @@ -661,6 +665,39 @@ export interface Solver { model(): Model; } +export interface Optimize { + /** @hidden */ + readonly __typename: 'Optimize'; + + readonly ctx: Context; + readonly ptr: Z3_optimize; + + set(key: string, value: any): void; + + push(): void; + + pop(num?: number): void; + + add(...exprs: (Bool | AstVector>)[]): void; + + addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id?: number | string): void; + + addAndTrack(expr: Bool, constant: Bool | string): void; + + assertions(): AstVector>; + + fromString(s: string): void; + + maximize(expr: Arith): void; + + minimize(expr: Arith): void; + + check(...exprs: (Bool | AstVector>)[]): Promise; + + model(): Model; +} + + /** @hidden */ export interface ModelCtor { new (): Model;