From 7c69858b147d72de04804a80ae74503d5845a097 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 10 Jan 2026 14:38:34 -0800 Subject: [PATCH] Add Goal, ApplyResult, and Tactic APIs to TypeScript bindings (#8141) * Initial plan * Add Goal, ApplyResult, and enhanced Tactic/Probe APIs to TypeScript bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix async tactic.apply and add comprehensive tests for new APIs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Address code review feedback: fix proxy handler, factory method, and type improvements Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add API examples documentation and format code with Prettier Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix merge conflict in test file - complete truncated tactic test Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add test case for tactic.apply method missing bracket, * Change tactic from 'simplify' to 'smt' * Delete src/api/js/TACTICS_API_EXAMPLES.md --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/api/js/src/high-level/high-level.test.ts | 316 ++++++++++++++++++ src/api/js/src/high-level/high-level.ts | 332 ++++++++++++++++++- src/api/js/src/high-level/types.ts | 224 +++++++++++++ 3 files changed, 865 insertions(+), 7 deletions(-) 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 dba731156..0c4a1788b 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -1196,6 +1196,309 @@ describe('high-level', () => { }); }); + describe('Goal API', () => { + it('can create a goal', () => { + const { Goal } = api.Context('main'); + const goal = new Goal(); + expect(goal).toBeDefined(); + expect(goal.size()).toBe(0); + }); + + it('can add constraints to goal', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0), x.lt(10)); + expect(goal.size()).toBe(2); + }); + + it('can get constraints from goal', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0)); + const constraint = goal.get(0); + expect(constraint.sexpr()).toContain('x'); + expect(constraint.sexpr()).toContain('>'); + }); + + it('can check goal properties', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + + expect(goal.inconsistent()).toBe(false); + expect(goal.depth()).toBe(0); + expect(goal.numExprs()).toBe(0); + + goal.add(x.gt(0)); + expect(goal.size()).toBe(1); + expect(goal.numExprs()).toBeGreaterThanOrEqual(1); + }); + + it('can reset goal', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0), x.lt(10)); + expect(goal.size()).toBe(2); + goal.reset(); + expect(goal.size()).toBe(0); + }); + + it('can convert goal to expression', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + + // Empty goal should be True + expect(goal.asExpr().sexpr()).toBe('true'); + + // Single constraint + goal.add(x.gt(0)); + expect(goal.asExpr().sexpr()).toContain('x'); + + // Multiple constraints should be conjunction + goal.add(x.lt(10)); + const expr = goal.asExpr(); + expect(expr.sexpr()).toContain('and'); + }); + + it('can get goal string representation', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0)); + const str = goal.toString(); + expect(str).toContain('x'); + expect(str).toContain('>'); + }); + }); + + describe('Tactic API', () => { + it('can create a tactic', () => { + const { Tactic } = api.Context('main'); + const tactic = new Tactic('simplify'); + expect(tactic).toBeDefined(); + }); + + it('can apply tactic to goal', async () => { + const { Int, Goal, Tactic } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.add(1).gt(2)); + + const tactic = new Tactic('simplify'); + const result = await tactic.apply(goal); + + expect(result).toBeDefined(); + expect(result.length()).toBeGreaterThan(0); + }); + + it('can apply tactic to boolean expression', async () => { + const { Int, Tactic } = api.Context('main'); + const x = Int.const('x'); + const tactic = new Tactic('simplify'); + const result = await tactic.apply(x.add(1).gt(2)); + + expect(result).toBeDefined(); + expect(result.length()).toBeGreaterThan(0); + }); + + it('can create solver from tactic', () => { + const { Tactic } = api.Context('main'); + const tactic = new Tactic('simplify'); + const solver = tactic.solver(); + expect(solver).toBeDefined(); + }); + + it('can get tactic help', () => { + const { Tactic } = api.Context('main'); + const tactic = new Tactic('simplify'); + const help = tactic.help(); + expect(typeof help).toBe('string'); + expect(help.length).toBeGreaterThan(0); + }); + + it('can get tactic parameter descriptions', () => { + const { Tactic } = api.Context('main'); + const tactic = new Tactic('simplify'); + const paramDescrs = tactic.getParamDescrs(); + expect(paramDescrs).toBeDefined(); + }); + }); + + describe('ApplyResult API', () => { + it('can get subgoals from apply result', async () => { + const { Int, Goal, Tactic } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0), x.lt(10)); + + const tactic = new Tactic('simplify'); + const result = await tactic.apply(goal); + + expect(result.length()).toBeGreaterThan(0); + const subgoal = result.getSubgoal(0); + expect(subgoal).toBeDefined(); + expect(subgoal.size()).toBeGreaterThanOrEqual(0); + }); + + it('supports indexer access', async () => { + const { Int, Goal, Tactic } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0)); + + const tactic = new Tactic('simplify'); + const result = await tactic.apply(goal); + + // Indexer access should work + const subgoal = result[0]; + expect(subgoal).toBeDefined(); + expect(typeof subgoal.size).toBe('function'); + expect(subgoal.size()).toBeGreaterThanOrEqual(0); + }); + + it('can get string representation', async () => { + const { Int, Goal, Tactic } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0)); + + const tactic = new Tactic('simplify'); + const result = await tactic.apply(goal); + const str = result.toString(); + + expect(typeof str).toBe('string'); + expect(str.length).toBeGreaterThan(0); + }); + }); + + describe('Tactic Combinators', () => { + it('can compose tactics with AndThen', () => { + const { Tactic, AndThen } = api.Context('main'); + const t1 = new Tactic('simplify'); + const t2 = new Tactic('solve-eqs'); + const combined = AndThen(t1, t2); + expect(combined).toBeDefined(); + }); + + it('can create fallback tactics with OrElse', () => { + const { Tactic, OrElse } = api.Context('main'); + const t1 = new Tactic('simplify'); + const t2 = new Tactic('solve-eqs'); + const combined = OrElse(t1, t2); + expect(combined).toBeDefined(); + }); + + it('can repeat a tactic', () => { + const { Tactic, Repeat } = api.Context('main'); + const t = new Tactic('simplify'); + const repeated = Repeat(t, 5); + expect(repeated).toBeDefined(); + }); + + it('can apply tactic with timeout', () => { + const { Tactic, TryFor } = api.Context('main'); + const t = new Tactic('simplify'); + const withTimeout = TryFor(t, 1000); + expect(withTimeout).toBeDefined(); + }); + + it('can create Skip tactic', () => { + const { Skip } = api.Context('main'); + const skip = Skip(); + expect(skip).toBeDefined(); + }); + + it('can create Fail tactic', () => { + const { Fail } = api.Context('main'); + const fail = Fail(); + expect(fail).toBeDefined(); + }); + + it('can compose tactics in parallel with ParOr', () => { + const { Tactic, ParOr } = api.Context('main'); + const t1 = new Tactic('simplify'); + const t2 = new Tactic('solve-eqs'); + const combined = ParOr(t1, t2); + expect(combined).toBeDefined(); + }); + + it('can use With to set tactic parameters', () => { + const { Tactic, With } = api.Context('main'); + const t = new Tactic('simplify'); + const withParams = With(t, { max_steps: 100 }); + expect(withParams).toBeDefined(); + }); + + it('can use tactic combinators with strings', () => { + const { AndThen, OrElse } = api.Context('main'); + const t1 = AndThen('simplify', 'solve-eqs'); + expect(t1).toBeDefined(); + + const t2 = OrElse('simplify', 'solve-eqs'); + expect(t2).toBeDefined(); + }); + }); + + describe('Probe API', () => { + it('can apply probe to goal', () => { + const { Int, Goal } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.gt(0), x.lt(10)); + + // Create a simple probe - we'd need to add probe creation functions + // For now, just test that the method signature is correct + expect(goal).toBeDefined(); + }); + }); + + describe('Goal and Tactic Integration', () => { + it('can solve using tactics', async () => { + const { Int, Goal, Tactic } = api.Context('main'); + const x = Int.const('x'); + const y = Int.const('y'); + + const goal = new Goal(); + goal.add(x.gt(0), y.gt(x), y.lt(10)); + + const tactic = new Tactic('simplify'); + const result = await tactic.apply(goal); + + expect(result.length()).toBeGreaterThan(0); + const subgoal = result.getSubgoal(0); + expect(subgoal.size()).toBeGreaterThan(0); + }); + + it('can use tactic solver for satisfiability', async () => { + const { Int, Tactic } = api.Context('main'); + const x = Int.const('x'); + + const tactic = new Tactic('smt'); + const solver = tactic.solver(); + solver.add(x.gt(0), x.lt(10)); + + const result = await solver.check(); + expect(result).toBe('sat'); + }); + + it('can chain multiple tactics', async () => { + const { Int, Goal, AndThen } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.add(1).eq(3)); + + const tactic = AndThen('simplify', 'solve-eqs'); + const result = await tactic.apply(goal); + + expect(result).toBeDefined(); + expect(result.length()).toBeGreaterThan(0); + }); + }); + describe('floating-point', () => { it('can create FP sorts', () => { const { Float } = api.Context('main'); @@ -1478,6 +1781,19 @@ describe('high-level', () => { expect(result).toBe('sat'); }); + it('can chain multiple tactics', async () => { + const { Int, Goal, AndThen } = api.Context('main'); + const x = Int.const('x'); + const goal = new Goal(); + goal.add(x.add(1).eq(3)); + + const tactic = AndThen('simplify', 'solve-eqs'); + const result = await tactic.apply(goal); + + expect(result).toBeDefined(); + expect(result.length()).toBeGreaterThan(0); + }); + it('supports string type checking', () => { const { String: Str, Seq, Int, isSeqSort, isSeq, isStringSort, isString } = api.Context('main'); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 2eab4f28f..e12f8a341 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -39,6 +39,10 @@ import { Z3_func_entry, Z3_optimize, Z3_fixedpoint, + Z3_goal, + Z3_apply_result, + Z3_goal_prec, + Z3_param_descrs, } from '../low-level'; import { AnyAst, @@ -93,6 +97,8 @@ import { Sort, SortToExprMap, Tactic, + Goal, + ApplyResult, Z3Error, Z3HighLevel, CoercibleToArith, @@ -605,6 +611,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return r; } + function isGoal(obj: unknown): obj is Goal { + const r = obj instanceof GoalImpl; + r && _assertContext(obj); + return r; + } + function isAstVector(obj: unknown): obj is AstVector { const r = obj instanceof AstVectorImpl; r && _assertContext(obj); @@ -1417,6 +1429,127 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return new TacticImpl(check(Z3.tactic_cond(contextPtr, probe.ptr, onTrue.ptr, onFalse.ptr))); } + function _toTactic(t: Tactic | string): Tactic { + return typeof t === 'string' ? new TacticImpl(t) : t; + } + + function AndThen( + t1: Tactic | string, + t2: Tactic | string, + ...ts: (Tactic | string)[] + ): Tactic { + let result = _toTactic(t1); + let current = _toTactic(t2); + _assertContext(result, current); + result = new TacticImpl(check(Z3.tactic_and_then(contextPtr, result.ptr, current.ptr))); + + for (const t of ts) { + current = _toTactic(t); + _assertContext(result, current); + result = new TacticImpl(check(Z3.tactic_and_then(contextPtr, result.ptr, current.ptr))); + } + + return result; + } + + function OrElse( + t1: Tactic | string, + t2: Tactic | string, + ...ts: (Tactic | string)[] + ): Tactic { + let result = _toTactic(t1); + let current = _toTactic(t2); + _assertContext(result, current); + result = new TacticImpl(check(Z3.tactic_or_else(contextPtr, result.ptr, current.ptr))); + + for (const t of ts) { + current = _toTactic(t); + _assertContext(result, current); + result = new TacticImpl(check(Z3.tactic_or_else(contextPtr, result.ptr, current.ptr))); + } + + return result; + } + + const UINT_MAX = 4294967295; + + function Repeat(t: Tactic | string, max?: number): Tactic { + const tactic = _toTactic(t); + _assertContext(tactic); + const maxVal = max !== undefined ? max : UINT_MAX; + return new TacticImpl(check(Z3.tactic_repeat(contextPtr, tactic.ptr, maxVal))); + } + + function TryFor(t: Tactic | string, ms: number): Tactic { + const tactic = _toTactic(t); + _assertContext(tactic); + return new TacticImpl(check(Z3.tactic_try_for(contextPtr, tactic.ptr, ms))); + } + + function When(p: Probe, t: Tactic | string): Tactic { + const tactic = _toTactic(t); + _assertContext(p, tactic); + return new TacticImpl(check(Z3.tactic_when(contextPtr, p.ptr, tactic.ptr))); + } + + function Skip(): Tactic { + return new TacticImpl(check(Z3.tactic_skip(contextPtr))); + } + + function Fail(): Tactic { + return new TacticImpl(check(Z3.tactic_fail(contextPtr))); + } + + function FailIf(p: Probe): Tactic { + _assertContext(p); + return new TacticImpl(check(Z3.tactic_fail_if(contextPtr, p.ptr))); + } + + function ParOr(...tactics: (Tactic | string)[]): Tactic { + assert(tactics.length > 0, 'ParOr requires at least one tactic'); + const tacticImpls = tactics.map(t => _toTactic(t)); + _assertContext(...tacticImpls); + const tacticPtrs = tacticImpls.map(t => t.ptr); + return new TacticImpl(check(Z3.tactic_par_or(contextPtr, tacticPtrs))); + } + + function ParAndThen(t1: Tactic | string, t2: Tactic | string): Tactic { + const tactic1 = _toTactic(t1); + const tactic2 = _toTactic(t2); + _assertContext(tactic1, tactic2); + return new TacticImpl(check(Z3.tactic_par_and_then(contextPtr, tactic1.ptr, tactic2.ptr))); + } + + function With(t: Tactic | string, params: Record): Tactic { + const tactic = _toTactic(t); + _assertContext(tactic); + // Convert params to Z3_params + const z3params = check(Z3.mk_params(contextPtr)); + Z3.params_inc_ref(contextPtr, z3params); + try { + for (const [key, value] of Object.entries(params)) { + const sym = _toSymbol(key); + if (typeof value === 'boolean') { + Z3.params_set_bool(contextPtr, z3params, sym, value); + } else if (typeof value === 'number') { + if (Number.isInteger(value)) { + Z3.params_set_uint(contextPtr, z3params, sym, value); + } else { + Z3.params_set_double(contextPtr, z3params, sym, value); + } + } else if (typeof value === 'string') { + Z3.params_set_symbol(contextPtr, z3params, sym, _toSymbol(value)); + } else { + throw new Error(`Unsupported parameter type for ${key}`); + } + } + const result = new TacticImpl(check(Z3.tactic_using_params(contextPtr, tactic.ptr, z3params))); + return result; + } finally { + Z3.params_dec_ref(contextPtr, z3params); + } + } + function LT(a: Arith, b: CoercibleToArith): Bool { return new BoolImpl(check(Z3.mk_lt(contextPtr, a.ast, a.sort.cast(b).ast))); } @@ -1940,9 +2073,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { async query(query: Bool): Promise { _assertContext(query); - const result = await asyncMutex.runExclusive(() => - check(Z3.fixedpoint_query(contextPtr, this.ptr, query.ast)), - ); + const result = await asyncMutex.runExclusive(() => check(Z3.fixedpoint_query(contextPtr, this.ptr, query.ast))); switch (result) { case Z3_lbool.Z3_L_FALSE: return 'unsat'; @@ -2548,8 +2679,154 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_probe) { this.ctx = ctx; } + + apply(goal: Goal): number { + _assertContext(goal); + return Z3.probe_apply(contextPtr, this.ptr, goal.ptr); + } } + class GoalImpl implements Goal { + declare readonly __typename: Goal['__typename']; + readonly ctx: Context; + readonly ptr: Z3_goal; + + constructor(models: boolean = true, unsat_cores: boolean = false, proofs: boolean = false) { + this.ctx = ctx; + const myPtr = check(Z3.mk_goal(contextPtr, models, unsat_cores, proofs)); + this.ptr = myPtr; + Z3.goal_inc_ref(contextPtr, myPtr); + cleanup.register(this, () => Z3.goal_dec_ref(contextPtr, myPtr), this); + } + + // Factory method for creating from existing Z3_goal pointer + static fromPtr(goalPtr: Z3_goal): GoalImpl { + const goal = Object.create(GoalImpl.prototype) as GoalImpl; + (goal as any).ctx = ctx; + (goal as any).ptr = goalPtr; + Z3.goal_inc_ref(contextPtr, goalPtr); + cleanup.register(goal, () => Z3.goal_dec_ref(contextPtr, goalPtr), goal); + return goal; + } + + add(...constraints: (Bool | boolean)[]): void { + for (const constraint of constraints) { + const boolConstraint = isBool(constraint) ? constraint : Bool.val(constraint); + _assertContext(boolConstraint); + Z3.goal_assert(contextPtr, this.ptr, boolConstraint.ast); + } + } + + size(): number { + return Z3.goal_size(contextPtr, this.ptr); + } + + get(i: number): Bool { + assert(i >= 0 && i < this.size(), 'Index out of bounds'); + const ast = check(Z3.goal_formula(contextPtr, this.ptr, i)); + return new BoolImpl(ast); + } + + depth(): number { + return Z3.goal_depth(contextPtr, this.ptr); + } + + inconsistent(): boolean { + return Z3.goal_inconsistent(contextPtr, this.ptr); + } + + precision(): Z3_goal_prec { + return Z3.goal_precision(contextPtr, this.ptr); + } + + reset(): void { + Z3.goal_reset(contextPtr, this.ptr); + } + + numExprs(): number { + return Z3.goal_num_exprs(contextPtr, this.ptr); + } + + isDecidedSat(): boolean { + return Z3.goal_is_decided_sat(contextPtr, this.ptr); + } + + isDecidedUnsat(): boolean { + return Z3.goal_is_decided_unsat(contextPtr, this.ptr); + } + + convertModel(model: Model): Model { + _assertContext(model); + const convertedModel = check(Z3.goal_convert_model(contextPtr, this.ptr, model.ptr)); + return new ModelImpl(convertedModel); + } + + asExpr(): Bool { + const sz = this.size(); + if (sz === 0) { + return Bool.val(true); + } else if (sz === 1) { + return this.get(0); + } else { + const constraints: Bool[] = []; + for (let i = 0; i < sz; i++) { + constraints.push(this.get(i)); + } + return And(...constraints); + } + } + + toString(): string { + return Z3.goal_to_string(contextPtr, this.ptr); + } + + dimacs(includeNames: boolean = true): string { + return Z3.goal_to_dimacs_string(contextPtr, this.ptr, includeNames); + } + } + + class ApplyResultImpl implements ApplyResult { + declare readonly __typename: ApplyResult['__typename']; + readonly ctx: Context; + readonly ptr: Z3_apply_result; + + constructor(ptr: Z3_apply_result) { + this.ctx = ctx; + this.ptr = ptr; + Z3.apply_result_inc_ref(contextPtr, ptr); + cleanup.register(this, () => Z3.apply_result_dec_ref(contextPtr, ptr), this); + } + + length(): number { + return Z3.apply_result_get_num_subgoals(contextPtr, this.ptr); + } + + getSubgoal(i: number): Goal { + assert(i >= 0 && i < this.length(), 'Index out of bounds'); + const goalPtr = check(Z3.apply_result_get_subgoal(contextPtr, this.ptr, i)); + return GoalImpl.fromPtr(goalPtr); + } + + toString(): string { + return Z3.apply_result_to_string(contextPtr, this.ptr); + } + + [index: number]: Goal; + } + + // Add indexer support to ApplyResultImpl + const applyResultHandler = { + get(target: ApplyResultImpl, prop: string | symbol): any { + if (typeof prop === 'string') { + const index = parseInt(prop, 10); + if (!isNaN(index) && index >= 0 && index < target.length()) { + return target.getSubgoal(index); + } + } + return (target as any)[prop]; + }, + }; + class TacticImpl implements Tactic { declare readonly __typename: Tactic['__typename']; @@ -2570,6 +2847,37 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.tactic_inc_ref(contextPtr, myPtr); cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr), this); } + + async apply(goal: Goal | Bool): Promise> { + let goalToUse: Goal; + + if (isBool(goal)) { + // Convert Bool expression to Goal + goalToUse = new GoalImpl(); + goalToUse.add(goal); + } else { + goalToUse = goal; + } + + _assertContext(goalToUse); + const result = await Z3.tactic_apply(contextPtr, this.ptr, goalToUse.ptr); + const applyResult = new ApplyResultImpl(check(result)); + // Wrap with Proxy to enable indexer access + return new Proxy(applyResult, applyResultHandler) as ApplyResult; + } + + solver(): Solver { + const solverPtr = check(Z3.mk_solver_from_tactic(contextPtr, this.ptr)); + return new SolverImpl(solverPtr); + } + + help(): string { + return Z3.tactic_get_help(contextPtr, this.ptr); + } + + getParamDescrs(): Z3_param_descrs { + return check(Z3.tactic_get_param_descrs(contextPtr, this.ptr)); + } } class ArithSortImpl extends SortImpl implements ArithSort { @@ -3892,10 +4200,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return _toExpr(check(Z3.substitute_vars(contextPtr, t.ast, toAsts))); } - function substituteFuns( - t: Expr, - ...substitutions: [FuncDecl, Expr][] - ): Expr { + function substituteFuns(t: Expr, ...substitutions: [FuncDecl, Expr][]): Expr { _assertContext(t); const from: Z3_func_decl[] = []; const to: Z3_ast[] = []; @@ -3932,6 +4237,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Fixedpoint: FixedpointImpl, Model: ModelImpl, Tactic: TacticImpl, + Goal: GoalImpl, AstVector: AstVectorImpl as AstVectorCtor, AstMap: AstMapImpl as AstMapCtor, @@ -3984,6 +4290,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { isConstArray, isProbe, isTactic, + isGoal, isAstVector, eqIdentity, getVarIndex, @@ -4041,6 +4348,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Int2BV, Concat, Cond, + AndThen, + OrElse, + Repeat, + TryFor, + When, + Skip, + Fail, + FailIf, + ParOr, + ParAndThen, + With, LT, GT, LE, diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index fa14ebfd6..4074a1db4 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -17,6 +17,10 @@ import { Z3_sort, Z3_sort_kind, Z3_tactic, + Z3_goal, + Z3_apply_result, + Z3_goal_prec, + Z3_param_descrs, } from '../low-level'; /** @hidden */ @@ -309,6 +313,9 @@ export interface Context { /** @category Functions */ isTactic(obj: unknown): obj is Tactic; + /** @category Functions */ + isGoal(obj: unknown): obj is Goal; + /** @category Functions */ isAstVector(obj: unknown): obj is AstVector>; @@ -397,6 +404,8 @@ export interface Context { >; /** @category Classes */ readonly Tactic: new (name: string) => Tactic; + /** @category Classes */ + readonly Goal: new (models?: boolean, unsat_cores?: boolean, proofs?: boolean) => Goal; ///////////// // Objects // @@ -516,6 +525,74 @@ export interface Context { /** @category Operations */ AtLeast(args: [Bool, ...Bool[]], k: number): Bool; + // Tactic Combinators + + /** + * Compose two tactics sequentially. Applies t1 to a goal, then t2 to each subgoal. + * @category Tactics + */ + AndThen(t1: Tactic | string, t2: Tactic | string, ...ts: (Tactic | string)[]): Tactic; + + /** + * Create a tactic that applies t1, and if it fails, applies t2. + * @category Tactics + */ + OrElse(t1: Tactic | string, t2: Tactic | string, ...ts: (Tactic | string)[]): Tactic; + + /** + * Repeat a tactic up to max times (default: unbounded). + * @category Tactics + */ + Repeat(t: Tactic | string, max?: number): Tactic; + + /** + * Apply tactic with a timeout in milliseconds. + * @category Tactics + */ + TryFor(t: Tactic | string, ms: number): Tactic; + + /** + * Apply tactic only if probe condition is true. + * @category Tactics + */ + When(p: Probe, t: Tactic | string): Tactic; + + /** + * Create a tactic that always succeeds and does nothing (skip). + * @category Tactics + */ + Skip(): Tactic; + + /** + * Create a tactic that always fails. + * @category Tactics + */ + Fail(): Tactic; + + /** + * Create a tactic that fails if probe condition is true. + * @category Tactics + */ + FailIf(p: Probe): Tactic; + + /** + * Apply tactics in parallel and return first successful result. + * @category Tactics + */ + ParOr(...tactics: (Tactic | string)[]): Tactic; + + /** + * Compose two tactics in parallel (t1 and then t2 in parallel). + * @category Tactics + */ + ParAndThen(t1: Tactic | string, t2: Tactic | string): Tactic; + + /** + * Apply tactic with given parameters. + * @category Tactics + */ + With(t: Tactic | string, params: Record): Tactic; + // Quantifiers /** @category Operations */ @@ -2716,12 +2793,137 @@ export interface Quantifier< children(): [BodyT]; } +/** @hidden */ +export interface GoalCtor { + new (models?: boolean, unsat_cores?: boolean, proofs?: boolean): Goal; +} + +/** + * Goal is a collection of constraints we want to find a solution or show to be unsatisfiable. + * Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals. + * @category Tactics + */ +export interface Goal { + /** @hidden */ + readonly __typename: 'Goal'; + + readonly ctx: Context; + readonly ptr: Z3_goal; + + /** + * Add constraints to the goal. + */ + add(...constraints: (Bool | boolean)[]): void; + + /** + * Return the number of constraints in the goal. + */ + size(): number; + + /** + * Return a constraint from the goal at the given index. + */ + get(i: number): Bool; + + /** + * Return the depth of the goal (number of tactics applied). + */ + depth(): number; + + /** + * Return true if the goal contains the False constraint. + */ + inconsistent(): boolean; + + /** + * Return the precision of the goal (precise, under-approximation, over-approximation). + */ + precision(): Z3_goal_prec; + + /** + * Reset the goal to empty. + */ + reset(): void; + + /** + * Return the number of expressions in the goal. + */ + numExprs(): number; + + /** + * Return true if the goal is decided to be satisfiable. + */ + isDecidedSat(): boolean; + + /** + * Return true if the goal is decided to be unsatisfiable. + */ + isDecidedUnsat(): boolean; + + /** + * Convert a model for the goal to a model for the original goal. + */ + convertModel(model: Model): Model; + + /** + * Convert the goal to a single Boolean expression (conjunction of all constraints). + */ + asExpr(): Bool; + + /** + * Return a string representation of the goal. + */ + toString(): string; + + /** + * Return a DIMACS string representation of the goal. + */ + dimacs(includeNames?: boolean): string; +} + +/** + * ApplyResult contains the subgoals produced by applying a tactic to a goal. + * @category Tactics + */ +export interface ApplyResult { + /** @hidden */ + readonly __typename: 'ApplyResult'; + + readonly ctx: Context; + readonly ptr: Z3_apply_result; + + /** + * Return the number of subgoals in the result. + */ + length(): number; + + /** + * Return a subgoal at the given index. + */ + getSubgoal(i: number): Goal; + + /** + * Return a string representation of the apply result. + */ + toString(): string; + + /** + * Get subgoal at index (alias for getSubgoal). + */ + [index: number]: Goal; +} + export interface Probe { /** @hidden */ readonly __typename: 'Probe'; readonly ctx: Context; readonly ptr: Z3_probe; + + /** + * Apply the probe to a goal and return the result as a number. + */ + apply(goal: Goal): number; } /** @hidden */ @@ -2735,6 +2937,28 @@ export interface Tactic { readonly ctx: Context; readonly ptr: Z3_tactic; + + /** + * Apply the tactic to a goal and return the resulting subgoals. + */ + apply(goal: Goal | Bool): Promise>; + + /** + * Create a solver from this tactic. + * The solver will always solve each check() from scratch using this tactic. + */ + solver(): Solver; + + /** + * Get help string describing the tactic. + */ + help(): string; + + /** + * Get parameter descriptions for the tactic. + * Returns a Z3 parameter descriptors object. + */ + getParamDescrs(): Z3_param_descrs; } /** @hidden */