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 <nbjorner@microsoft.com>

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');
 

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<Name> {
+      const r = obj instanceof GoalImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
     function isAstVector(obj: unknown): obj is AstVector<Name> {
       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<Name> | string): Tactic<Name> {
+      return typeof t === 'string' ? new TacticImpl(t) : t;
+    }
+
+    function AndThen(
+      t1: Tactic<Name> | string,
+      t2: Tactic<Name> | string,
+      ...ts: (Tactic<Name> | string)[]
+    ): Tactic<Name> {
+      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<Name> | string,
+      t2: Tactic<Name> | string,
+      ...ts: (Tactic<Name> | string)[]
+    ): Tactic<Name> {
+      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<Name> | string, max?: number): Tactic<Name> {
+      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<Name> | string, ms: number): Tactic<Name> {
+      const tactic = _toTactic(t);
+      _assertContext(tactic);
+      return new TacticImpl(check(Z3.tactic_try_for(contextPtr, tactic.ptr, ms)));
+    }
+
+    function When(p: Probe<Name>, t: Tactic<Name> | string): Tactic<Name> {
+      const tactic = _toTactic(t);
+      _assertContext(p, tactic);
+      return new TacticImpl(check(Z3.tactic_when(contextPtr, p.ptr, tactic.ptr)));
+    }
+
+    function Skip(): Tactic<Name> {
+      return new TacticImpl(check(Z3.tactic_skip(contextPtr)));
+    }
+
+    function Fail(): Tactic<Name> {
+      return new TacticImpl(check(Z3.tactic_fail(contextPtr)));
+    }
+
+    function FailIf(p: Probe<Name>): Tactic<Name> {
+      _assertContext(p);
+      return new TacticImpl(check(Z3.tactic_fail_if(contextPtr, p.ptr)));
+    }
+
+    function ParOr(...tactics: (Tactic<Name> | string)[]): Tactic<Name> {
+      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<Name> | string, t2: Tactic<Name> | string): Tactic<Name> {
+      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<Name> | string, params: Record<string, any>): Tactic<Name> {
+      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<Name>, b: CoercibleToArith<Name>): Bool<Name> {
       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<Name>): Promise<CheckSatResult> {
         _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<Name>): number {
+        _assertContext(goal);
+        return Z3.probe_apply(contextPtr, this.ptr, goal.ptr);
+      }
     }
 
+    class GoalImpl implements Goal<Name> {
+      declare readonly __typename: Goal['__typename'];
+      readonly ctx: Context<Name>;
+      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<Name> | 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<Name> {
+        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<Name>): Model<Name> {
+        _assertContext(model);
+        const convertedModel = check(Z3.goal_convert_model(contextPtr, this.ptr, model.ptr));
+        return new ModelImpl(convertedModel);
+      }
+
+      asExpr(): Bool<Name> {
+        const sz = this.size();
+        if (sz === 0) {
+          return Bool.val(true);
+        } else if (sz === 1) {
+          return this.get(0);
+        } else {
+          const constraints: Bool<Name>[] = [];
+          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<Name> {
+      declare readonly __typename: ApplyResult['__typename'];
+      readonly ctx: Context<Name>;
+      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<Name> {
+        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<Name>;
+    }
+
+    // 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<Name> {
       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<Name> | Bool<Name>): Promise<ApplyResult<Name>> {
+        let goalToUse: Goal<Name>;
+
+        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<Name>;
+      }
+
+      solver(): Solver<Name> {
+        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<Name> {
@@ -3892,10 +4200,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return _toExpr(check(Z3.substitute_vars(contextPtr, t.ast, toAsts)));
     }
 
-    function substituteFuns(
-      t: Expr<Name>,
-      ...substitutions: [FuncDecl<Name>, Expr<Name>][]
-    ): Expr<Name> {
+    function substituteFuns(t: Expr<Name>, ...substitutions: [FuncDecl<Name>, Expr<Name>][]): Expr<Name> {
       _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<Name>,
       AstMap: AstMapImpl as AstMapCtor<Name>,
 
@@ -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,

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<Name extends string = 'main'> {
   /** @category Functions */
   isTactic(obj: unknown): obj is Tactic<Name>;
 
+  /** @category Functions */
+  isGoal(obj: unknown): obj is Goal<Name>;
+
   /** @category Functions */
   isAstVector(obj: unknown): obj is AstVector<Name, AnyAst<Name>>;
 
@@ -397,6 +404,8 @@ export interface Context<Name extends string = 'main'> {
   >;
   /** @category Classes */
   readonly Tactic: new (name: string) => Tactic<Name>;
+  /** @category Classes */
+  readonly Goal: new (models?: boolean, unsat_cores?: boolean, proofs?: boolean) => Goal<Name>;
 
   /////////////
   // Objects //
@@ -516,6 +525,74 @@ export interface Context<Name extends string = 'main'> {
   /** @category Operations */
   AtLeast(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name>;
 
+  // Tactic Combinators
+
+  /**
+   * Compose two tactics sequentially. Applies t1 to a goal, then t2 to each subgoal.
+   * @category Tactics
+   */
+  AndThen(t1: Tactic<Name> | string, t2: Tactic<Name> | string, ...ts: (Tactic<Name> | string)[]): Tactic<Name>;
+
+  /**
+   * Create a tactic that applies t1, and if it fails, applies t2.
+   * @category Tactics
+   */
+  OrElse(t1: Tactic<Name> | string, t2: Tactic<Name> | string, ...ts: (Tactic<Name> | string)[]): Tactic<Name>;
+
+  /**
+   * Repeat a tactic up to max times (default: unbounded).
+   * @category Tactics
+   */
+  Repeat(t: Tactic<Name> | string, max?: number): Tactic<Name>;
+
+  /**
+   * Apply tactic with a timeout in milliseconds.
+   * @category Tactics
+   */
+  TryFor(t: Tactic<Name> | string, ms: number): Tactic<Name>;
+
+  /**
+   * Apply tactic only if probe condition is true.
+   * @category Tactics
+   */
+  When(p: Probe<Name>, t: Tactic<Name> | string): Tactic<Name>;
+
+  /**
+   * Create a tactic that always succeeds and does nothing (skip).
+   * @category Tactics
+   */
+  Skip(): Tactic<Name>;
+
+  /**
+   * Create a tactic that always fails.
+   * @category Tactics
+   */
+  Fail(): Tactic<Name>;
+
+  /**
+   * Create a tactic that fails if probe condition is true.
+   * @category Tactics
+   */
+  FailIf(p: Probe<Name>): Tactic<Name>;
+
+  /**
+   * Apply tactics in parallel and return first successful result.
+   * @category Tactics
+   */
+  ParOr(...tactics: (Tactic<Name> | string)[]): Tactic<Name>;
+
+  /**
+   * Compose two tactics in parallel (t1 and then t2 in parallel).
+   * @category Tactics
+   */
+  ParAndThen(t1: Tactic<Name> | string, t2: Tactic<Name> | string): Tactic<Name>;
+
+  /**
+   * Apply tactic with given parameters.
+   * @category Tactics
+   */
+  With(t: Tactic<Name> | string, params: Record<string, any>): Tactic<Name>;
+
   // Quantifiers
 
   /** @category Operations */
@@ -2716,12 +2793,137 @@ export interface Quantifier<
   children(): [BodyT<Name, QVarSorts, QSort>];
 }
 
+/** @hidden */
+export interface GoalCtor<Name extends string> {
+  new (models?: boolean, unsat_cores?: boolean, proofs?: boolean): Goal<Name>;
+}
+
+/**
+ * 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<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'Goal';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_goal;
+
+  /**
+   * Add constraints to the goal.
+   */
+  add(...constraints: (Bool<Name> | 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<Name>;
+
+  /**
+   * 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<Name>): Model<Name>;
+
+  /**
+   * Convert the goal to a single Boolean expression (conjunction of all constraints).
+   */
+  asExpr(): Bool<Name>;
+
+  /**
+   * 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<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'ApplyResult';
+
+  readonly ctx: Context<Name>;
+  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<Name>;
+
+  /**
+   * Return a string representation of the apply result.
+   */
+  toString(): string;
+
+  /**
+   * Get subgoal at index (alias for getSubgoal).
+   */
+  [index: number]: Goal<Name>;
+}
+
 export interface Probe<Name extends string = 'main'> {
   /** @hidden */
   readonly __typename: 'Probe';
 
   readonly ctx: Context<Name>;
   readonly ptr: Z3_probe;
+
+  /**
+   * Apply the probe to a goal and return the result as a number.
+   */
+  apply(goal: Goal<Name>): number;
 }
 
 /** @hidden */
@@ -2735,6 +2937,28 @@ export interface Tactic<Name extends string = 'main'> {
 
   readonly ctx: Context<Name>;
   readonly ptr: Z3_tactic;
+
+  /**
+   * Apply the tactic to a goal and return the resulting subgoals.
+   */
+  apply(goal: Goal<Name> | Bool<Name>): Promise<ApplyResult<Name>>;
+
+  /**
+   * Create a solver from this tactic.
+   * The solver will always solve each check() from scratch using this tactic.
+   */
+  solver(): Solver<Name>;
+
+  /**
+   * 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 */