Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings (#8146)

* Initial plan

* Add Simplifier, Params, and ParamDescrs APIs to TypeScript bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add Tactic.usingParams and comprehensive documentation for new APIs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Format code with prettier

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add implementation summary documentation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix test by using valid parameter for solve-eqs simplifier

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete IMPLEMENTATION_SUMMARY.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

@@ -1323,9 +1323,20 @@ describe('high-level', () => {
     it('can get tactic parameter descriptions', () => {
       const { Tactic } = api.Context('main');
       const tactic = new Tactic('simplify');
-      const paramDescrs = tactic.getParamDescrs();
+      const paramDescrs = tactic.paramDescrs();
       expect(paramDescrs).toBeDefined();
     });
+
+    it('can configure tactic with parameters', () => {
+      const { Tactic, Params } = api.Context('main');
+      const tactic = new Tactic('simplify');
+      const params = new Params();
+      params.set('max_steps', 100);
+
+      const configuredTactic = tactic.usingParams(params);
+      expect(configuredTactic).toBeDefined();
+      expect(configuredTactic).not.toBe(tactic);
+    });
   });
 
   describe('ApplyResult API', () => {
@@ -1674,8 +1685,8 @@ describe('high-level', () => {
 
       const empty = Seq.empty(Int.sort());
       const len_empty = empty.length();
-      // TOOD: simplify len_empty const len_empty_simplified = 
-//      expect(len_empty_simplified.toString()).toContain('0');
+      // TOOD: simplify len_empty const len_empty_simplified =
+      //      expect(len_empty_simplified.toString()).toContain('0');
     });
 
     it('can concatenate strings', async () => {
@@ -1793,7 +1804,7 @@ describe('high-level', () => {
       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');
 
@@ -1832,4 +1843,145 @@ describe('high-level', () => {
       expect(result).toBe('sat');
     });
   });
+
+  describe('Params API', () => {
+    it('can create params', () => {
+      const { Params } = api.Context('main');
+      const params = new Params();
+      expect(params).toBeDefined();
+    });
+
+    it('can set boolean parameter', () => {
+      const { Params } = api.Context('main');
+      const params = new Params();
+      params.set('elim_and', true);
+      const str = params.toString();
+      expect(str).toContain('elim_and');
+      expect(str).toContain('true');
+    });
+
+    it('can set integer parameter', () => {
+      const { Params } = api.Context('main');
+      const params = new Params();
+      params.set('max_steps', 100);
+      const str = params.toString();
+      expect(str).toContain('max_steps');
+      expect(str).toContain('100');
+    });
+
+    it('can set double parameter', () => {
+      const { Params } = api.Context('main');
+      const params = new Params();
+      params.set('timeout', 1.5);
+      const str = params.toString();
+      expect(str).toContain('timeout');
+    });
+
+    it('can set string parameter', () => {
+      const { Params } = api.Context('main');
+      const params = new Params();
+      params.set('logic', 'QF_LIA');
+      const str = params.toString();
+      expect(str).toContain('logic');
+      expect(str).toContain('QF_LIA');
+    });
+
+    it('can validate params against param descrs', () => {
+      const { Params, Tactic } = api.Context('main');
+      const tactic = new Tactic('simplify');
+      const params = new Params();
+      params.set('elim_and', true);
+
+      const paramDescrs = tactic.paramDescrs();
+      // This should not throw - validation should succeed
+      expect(() => params.validate(paramDescrs)).not.toThrow();
+    });
+  });
+
+  describe('ParamDescrs API', () => {
+    it('can get param descriptions from tactic', () => {
+      const { Tactic } = api.Context('main');
+      const tactic = new Tactic('simplify');
+      const paramDescrs = tactic.paramDescrs();
+      expect(paramDescrs).toBeDefined();
+    });
+
+    it('param descrs toString returns non-empty string', () => {
+      const { Tactic } = api.Context('main');
+      const tactic = new Tactic('simplify');
+      const paramDescrs = tactic.paramDescrs();
+      const str = paramDescrs.toString();
+      expect(typeof str).toBe('string');
+      expect(str.length).toBeGreaterThan(0);
+    });
+  });
+
+  describe('Simplifier API', () => {
+    it('can create a simplifier', () => {
+      const { Simplifier } = api.Context('main');
+      const simplifier = new Simplifier('solve-eqs');
+      expect(simplifier).toBeDefined();
+    });
+
+    it('can get simplifier help', () => {
+      const { Simplifier } = api.Context('main');
+      const simplifier = new Simplifier('solve-eqs');
+      const help = simplifier.help();
+      expect(typeof help).toBe('string');
+      expect(help.length).toBeGreaterThan(0);
+    });
+
+    it('can get simplifier parameter descriptions', () => {
+      const { Simplifier } = api.Context('main');
+      const simplifier = new Simplifier('solve-eqs');
+      const paramDescrs = simplifier.paramDescrs();
+      expect(paramDescrs).toBeDefined();
+      expect(typeof paramDescrs.toString).toBe('function');
+    });
+
+    it('can use simplifier with parameters', () => {
+      const { Simplifier, Params } = api.Context('main');
+      const simplifier = new Simplifier('solve-eqs');
+      const params = new Params();
+      params.set('ite_solver', false);
+
+      const configuredSimplifier = simplifier.usingParams(params);
+      expect(configuredSimplifier).toBeDefined();
+      expect(configuredSimplifier).not.toBe(simplifier);
+    });
+
+    it('can compose simplifiers with andThen', () => {
+      const { Simplifier } = api.Context('main');
+      const s1 = new Simplifier('solve-eqs');
+      const s2 = new Simplifier('simplify');
+
+      const composed = s1.andThen(s2);
+      expect(composed).toBeDefined();
+      expect(composed).not.toBe(s1);
+      expect(composed).not.toBe(s2);
+    });
+
+    it('can add simplifier to solver', async () => {
+      const { Simplifier, Solver, Int } = api.Context('main');
+      const simplifier = new Simplifier('solve-eqs');
+      const solver = new Solver();
+
+      // Add simplifier to solver
+      solver.addSimplifier(simplifier);
+
+      // Add a constraint and solve
+      const x = Int.const('x');
+      const y = Int.const('y');
+      solver.add(x.eq(y.add(1)), y.eq(5));
+
+      const result = await solver.check();
+      expect(result).toBe('sat');
+
+      if (result === 'sat') {
+        const model = solver.model();
+        const xVal = model.eval(x);
+        expect(xVal.toString()).toBe('6');
+      }
+    });
+  });
 });

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

@@ -43,6 +43,7 @@ import {
   Z3_apply_result,
   Z3_goal_prec,
   Z3_param_descrs,
+  Z3_simplifier,
 } from '../low-level';
 import {
   AnyAst,
@@ -84,6 +85,8 @@ import {
   IntNum,
   Model,
   Optimize,
+  Params,
+  ParamDescrs,
   Pattern,
   Probe,
   Quantifier,
@@ -91,6 +94,7 @@ import {
   RatNum,
   Seq,
   SeqSort,
+  Simplifier,
   SMTArray,
   SMTArraySort,
   Solver,
@@ -1826,6 +1830,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         check(Z3.solver_assert_and_track(contextPtr, this.ptr, expr.ast, constant.ast));
       }
 
+      addSimplifier(simplifier: Simplifier<Name>): void {
+        _assertContext(simplifier);
+        check(Z3.solver_add_simplifier(contextPtr, this.ptr, simplifier.ptr));
+      }
+
       assertions(): AstVector<Name, Bool<Name>> {
         return new AstVectorImpl(check(Z3.solver_get_assertions(contextPtr, this.ptr)));
       }
@@ -2875,8 +2884,136 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return Z3.tactic_get_help(contextPtr, this.ptr);
       }
 
-      getParamDescrs(): Z3_param_descrs {
-        return check(Z3.tactic_get_param_descrs(contextPtr, this.ptr));
+      paramDescrs(): ParamDescrs<Name> {
+        const descrs = check(Z3.tactic_get_param_descrs(contextPtr, this.ptr));
+        return new ParamDescrsImpl(descrs);
+      }
+
+      usingParams(params: Params<Name>): Tactic<Name> {
+        _assertContext(params);
+        const newTactic = check(Z3.tactic_using_params(contextPtr, this.ptr, params.ptr));
+        return new TacticImpl(newTactic);
+      }
+    }
+
+    class ParamsImpl implements Params<Name> {
+      declare readonly __typename: Params['__typename'];
+
+      readonly ptr: Z3_params;
+      readonly ctx: Context<Name>;
+
+      constructor(params?: Z3_params) {
+        this.ctx = ctx;
+        if (params) {
+          this.ptr = params;
+        } else {
+          this.ptr = Z3.mk_params(contextPtr);
+        }
+        Z3.params_inc_ref(contextPtr, this.ptr);
+        cleanup.register(this, () => Z3.params_dec_ref(contextPtr, this.ptr), this);
+      }
+
+      set(name: string, value: boolean | number | string): void {
+        const sym = _toSymbol(name);
+        if (typeof value === 'boolean') {
+          Z3.params_set_bool(contextPtr, this.ptr, sym, value);
+        } else if (typeof value === 'number') {
+          if (Number.isInteger(value)) {
+            check(Z3.params_set_uint(contextPtr, this.ptr, sym, value));
+          } else {
+            check(Z3.params_set_double(contextPtr, this.ptr, sym, value));
+          }
+        } else if (typeof value === 'string') {
+          check(Z3.params_set_symbol(contextPtr, this.ptr, sym, _toSymbol(value)));
+        }
+      }
+
+      validate(descrs: ParamDescrs<Name>): void {
+        _assertContext(descrs);
+        Z3.params_validate(contextPtr, this.ptr, descrs.ptr);
+      }
+
+      toString(): string {
+        return Z3.params_to_string(contextPtr, this.ptr);
+      }
+    }
+
+    class ParamDescrsImpl implements ParamDescrs<Name> {
+      declare readonly __typename: ParamDescrs['__typename'];
+
+      readonly ptr: Z3_param_descrs;
+      readonly ctx: Context<Name>;
+
+      constructor(paramDescrs: Z3_param_descrs) {
+        this.ctx = ctx;
+        this.ptr = paramDescrs;
+        Z3.param_descrs_inc_ref(contextPtr, this.ptr);
+        cleanup.register(this, () => Z3.param_descrs_dec_ref(contextPtr, this.ptr), this);
+      }
+
+      size(): number {
+        return Z3.param_descrs_size(contextPtr, this.ptr);
+      }
+
+      getName(i: number): string {
+        const sym = Z3.param_descrs_get_name(contextPtr, this.ptr, i);
+        const name = _fromSymbol(sym);
+        return typeof name === 'string' ? name : `${name}`;
+      }
+
+      getKind(name: string): number {
+        return Z3.param_descrs_get_kind(contextPtr, this.ptr, _toSymbol(name));
+      }
+
+      getDocumentation(name: string): string {
+        return Z3.param_descrs_get_documentation(contextPtr, this.ptr, _toSymbol(name));
+      }
+
+      toString(): string {
+        return Z3.param_descrs_to_string(contextPtr, this.ptr);
+      }
+    }
+
+    class SimplifierImpl implements Simplifier<Name> {
+      declare readonly __typename: Simplifier['__typename'];
+
+      readonly ptr: Z3_simplifier;
+      readonly ctx: Context<Name>;
+
+      constructor(simplifier: string | Z3_simplifier) {
+        this.ctx = ctx;
+        let myPtr: Z3_simplifier;
+        if (typeof simplifier === 'string') {
+          myPtr = check(Z3.mk_simplifier(contextPtr, simplifier));
+        } else {
+          myPtr = simplifier;
+        }
+
+        this.ptr = myPtr;
+
+        Z3.simplifier_inc_ref(contextPtr, myPtr);
+        cleanup.register(this, () => Z3.simplifier_dec_ref(contextPtr, myPtr), this);
+      }
+
+      help(): string {
+        return Z3.simplifier_get_help(contextPtr, this.ptr);
+      }
+
+      paramDescrs(): ParamDescrs<Name> {
+        const descrs = check(Z3.simplifier_get_param_descrs(contextPtr, this.ptr));
+        return new ParamDescrsImpl(descrs);
+      }
+
+      usingParams(params: Params<Name>): Simplifier<Name> {
+        _assertContext(params);
+        const newSimplifier = check(Z3.simplifier_using_params(contextPtr, this.ptr, params.ptr));
+        return new SimplifierImpl(newSimplifier);
+      }
+
+      andThen(other: Simplifier<Name>): Simplifier<Name> {
+        _assertContext(other);
+        const newSimplifier = check(Z3.simplifier_and_then(contextPtr, this.ptr, other.ptr));
+        return new SimplifierImpl(newSimplifier);
       }
     }
 
@@ -4238,6 +4375,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Model: ModelImpl,
       Tactic: TacticImpl,
       Goal: GoalImpl,
+      Params: ParamsImpl,
+      Simplifier: SimplifierImpl,
       AstVector: AstVectorImpl as AstVectorCtor<Name>,
       AstMap: AstMapImpl as AstMapCtor<Name>,
 

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

@@ -21,6 +21,8 @@ import {
   Z3_apply_result,
   Z3_goal_prec,
   Z3_param_descrs,
+  Z3_params,
+  Z3_simplifier,
 } from '../low-level';
 
 /** @hidden */
@@ -406,6 +408,10 @@ export interface Context<Name extends string = 'main'> {
   readonly Tactic: new (name: string) => Tactic<Name>;
   /** @category Classes */
   readonly Goal: new (models?: boolean, unsat_cores?: boolean, proofs?: boolean) => Goal<Name>;
+  /** @category Classes */
+  readonly Params: new () => Params<Name>;
+  /** @category Classes */
+  readonly Simplifier: new (name: string) => Simplifier<Name>;
 
   /////////////
   // Objects //
@@ -874,6 +880,13 @@ export interface Solver<Name extends string = 'main'> {
 
   addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string): void;
 
+  /**
+   * Attach a simplifier to the solver for incremental pre-processing.
+   * The solver will use the simplifier for incremental pre-processing of assertions.
+   * @param simplifier - The simplifier to attach
+   */
+  addSimplifier(simplifier: Simplifier<Name>): void;
+
   assertions(): AstVector<Name, Bool<Name>>;
 
   fromString(s: string): void;
@@ -2956,9 +2969,130 @@ export interface Tactic<Name extends string = 'main'> {
 
   /**
    * Get parameter descriptions for the tactic.
-   * Returns a Z3 parameter descriptors object.
+   * Returns a ParamDescrs object for introspecting available parameters.
    */
-  getParamDescrs(): Z3_param_descrs;
+  paramDescrs(): ParamDescrs<Name>;
+
+  /**
+   * Return a tactic that uses the given configuration parameters.
+   * @param params - Parameters to configure the tactic
+   */
+  usingParams(params: Params<Name>): Tactic<Name>;
+}
+
+/**
+ * Params is a set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
+ * @category Tactics
+ */
+export interface Params<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'Params';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_params;
+
+  /**
+   * Set a parameter with the given name and value.
+   * @param name - Parameter name
+   * @param value - Parameter value (boolean, number, or string)
+   */
+  set(name: string, value: boolean | number | string): void;
+
+  /**
+   * Validate the parameter set against a parameter description set.
+   * @param descrs - Parameter descriptions to validate against
+   */
+  validate(descrs: ParamDescrs<Name>): void;
+
+  /**
+   * Convert the parameter set to a string representation.
+   */
+  toString(): string;
+}
+
+/** @hidden */
+export interface ParamsCtor<Name extends string> {
+  new (): Params<Name>;
+}
+
+/**
+ * ParamDescrs is a set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
+ * @category Tactics
+ */
+export interface ParamDescrs<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'ParamDescrs';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_param_descrs;
+
+  /**
+   * Return the number of parameters in the description set.
+   */
+  size(): number;
+
+  /**
+   * Return the name of the parameter at the given index.
+   * @param i - Index of the parameter
+   */
+  getName(i: number): string;
+
+  /**
+   * Return the kind (type) of the parameter with the given name.
+   * @param name - Parameter name
+   */
+  getKind(name: string): number;
+
+  /**
+   * Return the documentation string for the parameter with the given name.
+   * @param name - Parameter name
+   */
+  getDocumentation(name: string): string;
+
+  /**
+   * Convert the parameter description set to a string representation.
+   */
+  toString(): string;
+}
+
+/**
+ * Simplifiers act as pre-processing utilities for solvers.
+ * Build a custom simplifier and add it to a solver for incremental preprocessing.
+ * @category Tactics
+ */
+export interface Simplifier<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'Simplifier';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_simplifier;
+
+  /**
+   * Return a string containing a description of parameters accepted by this simplifier.
+   */
+  help(): string;
+
+  /**
+   * Return the parameter description set for this simplifier.
+   */
+  paramDescrs(): ParamDescrs<Name>;
+
+  /**
+   * Return a simplifier that uses the given configuration parameters.
+   * @param params - Parameters to configure the simplifier
+   */
+  usingParams(params: Params<Name>): Simplifier<Name>;
+
+  /**
+   * Return a simplifier that applies this simplifier and then another simplifier.
+   * @param other - The simplifier to apply after this one
+   */
+  andThen(other: Simplifier<Name>): Simplifier<Name>;
+}
+
+/** @hidden */
+export interface SimplifierCtor<Name extends string> {
+  new (name: string): Simplifier<Name>;
 }
 
 /** @hidden */