Add missing API methods across language bindings (#8150)

* Initial plan

* Add API coherence improvements for C#, Python, C++, and TypeScript

- C#: Add SubstituteFuns method to Expr class
- Python: Add update method to ExprRef class
- C++: Add update method to expr class
- TypeScript: Add complete Statistics API with Statistics interface, StatisticsEntry interface, StatisticsImpl class, and statistics() methods for Solver, Optimize, and Fixedpoint

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

* Add Z3_stats import and Statistics types to TypeScript bindings

- Add Z3_stats to imports in types.ts and high-level.ts
- Add Statistics and StatisticsEntry to type imports in high-level.ts
- Fixes missing type references identified in code review

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

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/c++/z3++.h

@@ -1237,6 +1237,16 @@ namespace z3 {
           return vec;
         }
 
+        /**
+           \brief Update the arguments of this application.
+           Return a new expression with the same function declaration and updated arguments.
+           The number of new arguments must match the current number of arguments.
+
+           \pre is_app()
+           \pre args.size() == num_args()
+        */
+        expr update(expr_vector const& args) const;
+
         /**
            \brief Return the 'body' of this quantifier.
 
@@ -4369,6 +4379,16 @@ namespace z3 {
         return expr(ctx(), r);
     }
 
+    inline expr expr::update(expr_vector const& args) const {
+        array<Z3_ast> _args(args.size());
+        for (unsigned i = 0; i < args.size(); ++i) {
+            _args[i] = args[i];
+        }
+        Z3_ast r = Z3_update_term(ctx(), m_ast, args.size(), _args.ptr());
+        check_error();
+        return expr(ctx(), r);
+    }
+
     typedef std::function<void(expr const& proof, std::vector<unsigned> const& deps, expr_vector const& clause)> on_clause_eh_t;
 
     class on_clause {

src/api/dotnet/Expr.cs

@@ -159,6 +159,28 @@ namespace Microsoft.Z3
             return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
         }
 
+        /// <summary>
+        /// Substitute functions in <paramref name="from"/> with the expressions in <paramref name="to"/>.
+        /// </summary>
+        /// <remarks>
+        /// The expressions in <paramref name="to"/> can have free variables. The free variable in <c>to[i]</c> at de-Bruijn index 0 
+        /// refers to the first argument of <c>from[i]</c>, the free variable at index 1 corresponds to the second argument, and so on.
+        /// The arrays <paramref name="from"/> and <paramref name="to"/> must have the same size.
+        /// </remarks>
+        public Expr SubstituteFuns(FuncDecl[] from, Expr[] to)
+        {
+            Debug.Assert(from != null);
+            Debug.Assert(to != null);
+            Debug.Assert(from.All(f => f != null));
+            Debug.Assert(to.All(t => t != null));
+
+            Context.CheckContextMatch<FuncDecl>(from);
+            Context.CheckContextMatch<Expr>(to);
+            if (from.Length != to.Length)
+                throw new Z3Exception("Arrays 'from' and 'to' must have the same length");
+            return Expr.Create(Context, Native.Z3_substitute_funs(Context.nCtx, NativeObject, (uint)from.Length, FuncDecl.ArrayToNative(from), Expr.ArrayToNative(to)));
+        }
+
         /// <summary>
         /// Translates (copies) the term to the Context <paramref name="ctx"/>.
         /// </summary>

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

@@ -30,6 +30,7 @@ import {
   Z3_solver,
   Z3_sort,
   Z3_sort_kind,
+  Z3_stats,
   Z3_symbol,
   Z3_symbol_kind,
   Z3_tactic,
@@ -100,6 +101,8 @@ import {
   Solver,
   Sort,
   SortToExprMap,
+  Statistics,
+  StatisticsEntry,
   Tactic,
   Goal,
   ApplyResult,
@@ -1867,6 +1870,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new ModelImpl(check(Z3.solver_get_model(contextPtr, this.ptr)));
       }
 
+      statistics(): Statistics<Name> {
+        return new StatisticsImpl(check(Z3.solver_get_statistics(contextPtr, this.ptr)));
+      }
+
       reasonUnknown(): string {
         return check(Z3.solver_get_reason_unknown(contextPtr, this.ptr));
       }
@@ -2008,6 +2015,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new ModelImpl(check(Z3.optimize_get_model(contextPtr, this.ptr)));
       }
 
+      statistics(): Statistics<Name> {
+        return new StatisticsImpl(check(Z3.optimize_get_statistics(contextPtr, this.ptr)));
+      }
+
       toString() {
         return check(Z3.optimize_to_string(contextPtr, this.ptr));
       }
@@ -2167,6 +2178,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(av);
       }
 
+      statistics(): Statistics<Name> {
+        return new StatisticsImpl(check(Z3.fixedpoint_get_statistics(contextPtr, this.ptr)));
+      }
+
       release() {
         Z3.fixedpoint_dec_ref(contextPtr, this.ptr);
         this._ptr = null;
@@ -2378,6 +2393,81 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    class StatisticsImpl implements Statistics<Name> {
+      declare readonly __typename: Statistics['__typename'];
+      readonly ctx: Context<Name>;
+      private _ptr: Z3_stats | null;
+      get ptr(): Z3_stats {
+        _assertPtr(this._ptr);
+        return this._ptr;
+      }
+
+      constructor(ptr: Z3_stats) {
+        this.ctx = ctx;
+        this._ptr = ptr;
+        Z3.stats_inc_ref(contextPtr, ptr);
+        cleanup.register(this, () => Z3.stats_dec_ref(contextPtr, ptr), this);
+      }
+
+      size(): number {
+        return Z3.stats_size(contextPtr, this.ptr);
+      }
+
+      keys(): string[] {
+        const result: string[] = [];
+        const sz = this.size();
+        for (let i = 0; i < sz; i++) {
+          result.push(Z3.stats_get_key(contextPtr, this.ptr, i));
+        }
+        return result;
+      }
+
+      get(key: string): number {
+        const sz = this.size();
+        for (let i = 0; i < sz; i++) {
+          if (Z3.stats_get_key(contextPtr, this.ptr, i) === key) {
+            if (Z3.stats_is_uint(contextPtr, this.ptr, i)) {
+              return Z3.stats_get_uint_value(contextPtr, this.ptr, i);
+            } else {
+              return Z3.stats_get_double_value(contextPtr, this.ptr, i);
+            }
+          }
+        }
+        throw new Error(`Statistics key not found: ${key}`);
+      }
+
+      entries(): StatisticsEntry<Name>[] {
+        const result: StatisticsEntry<Name>[] = [];
+        const sz = this.size();
+        for (let i = 0; i < sz; i++) {
+          const key = Z3.stats_get_key(contextPtr, this.ptr, i);
+          const isUint = Z3.stats_is_uint(contextPtr, this.ptr, i);
+          const isDouble = Z3.stats_is_double(contextPtr, this.ptr, i);
+          const value = isUint 
+            ? Z3.stats_get_uint_value(contextPtr, this.ptr, i)
+            : Z3.stats_get_double_value(contextPtr, this.ptr, i);
+          result.push({
+            __typename: 'StatisticsEntry' as const,
+            key,
+            value,
+            isUint,
+            isDouble,
+          });
+        }
+        return result;
+      }
+
+      [Symbol.iterator](): Iterator<StatisticsEntry<Name>> {
+        return this.entries()[Symbol.iterator]();
+      }
+
+      release() {
+        Z3.stats_dec_ref(contextPtr, this.ptr);
+        this._ptr = null;
+        cleanup.unregister(this);
+      }
+    }
+
     class FuncEntryImpl implements FuncEntry<Name> {
       declare readonly __typename: FuncEntry['__typename'];
 

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

@@ -16,6 +16,7 @@ import {
   Z3_optimize,
   Z3_sort,
   Z3_sort_kind,
+  Z3_stats,
   Z3_tactic,
   Z3_goal,
   Z3_apply_result,
@@ -958,6 +959,27 @@ export interface Solver<Name extends string = 'main'> {
 
   model(): Model<Name>;
 
+  /**
+   * Retrieve statistics for the solver.
+   * Returns performance metrics, memory usage, decision counts, and other diagnostic information.
+   *
+   * @returns A Statistics object containing solver metrics
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * solver.add(x.gt(0));
+   * await solver.check();
+   * const stats = solver.statistics();
+   * console.log('Statistics size:', stats.size());
+   * for (const entry of stats) {
+   *   console.log(`${entry.key}: ${entry.value}`);
+   * }
+   * ```
+   */
+  statistics(): Statistics<Name>;
+
   /**
    * Return a string describing why the last call to {@link check} returned `'unknown'`.
    *
@@ -1150,6 +1172,8 @@ export interface Optimize<Name extends string = 'main'> {
 
   model(): Model<Name>;
 
+  statistics(): Statistics<Name>;
+
   /**
    * Manually decrease the reference count of the optimize
    * This is automatically done when the optimize is garbage collected,
@@ -1297,6 +1321,13 @@ export interface Fixedpoint<Name extends string = 'main'> {
    */
   fromFile(file: string): AstVector<Name, Bool<Name>>;
 
+  /**
+   * Retrieve statistics for the fixedpoint solver.
+   * Returns performance metrics and diagnostic information.
+   * @returns A Statistics object containing solver metrics
+   */
+  statistics(): Statistics<Name>;
+
   /**
    * Manually decrease the reference count of the fixedpoint
    * This is automatically done when the fixedpoint is garbage collected,
@@ -1442,6 +1473,77 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
   release(): void;
 }
 
+/**
+ * Statistics entry representing a single key-value pair from solver statistics
+ */
+export interface StatisticsEntry<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'StatisticsEntry';
+  
+  /** The key/name of this statistic */
+  readonly key: string;
+  
+  /** The numeric value of this statistic */
+  readonly value: number;
+  
+  /** True if this statistic is stored as an unsigned integer */
+  readonly isUint: boolean;
+  
+  /** True if this statistic is stored as a double */
+  readonly isDouble: boolean;
+}
+
+export interface StatisticsCtor<Name extends string> {
+  new (): Statistics<Name>;
+}
+
+/**
+ * Statistics for solver operations
+ * 
+ * Provides access to performance metrics, memory usage, decision counts, 
+ * and other diagnostic information from solver operations.
+ */
+export interface Statistics<Name extends string = 'main'> extends Iterable<StatisticsEntry<Name>> {
+  /** @hidden */
+  readonly __typename: 'Statistics';
+
+  readonly ctx: Context<Name>;
+  readonly ptr: Z3_stats;
+
+  /**
+   * Return the number of statistical data points
+   * @returns The number of statistics entries
+   */
+  size(): number;
+
+  /**
+   * Return the keys of all statistical data
+   * @returns Array of statistic keys
+   */
+  keys(): string[];
+
+  /**
+   * Return a specific statistic value by key
+   * @param key - The key of the statistic to retrieve
+   * @returns The numeric value of the statistic
+   * @throws Error if the key doesn't exist
+   */
+  get(key: string): number;
+
+  /**
+   * Return all statistics as an array of entries
+   * @returns Array of all statistics entries
+   */
+  entries(): StatisticsEntry<Name>[];
+
+  /**
+   * Manually decrease the reference count of the statistics object
+   * This is automatically done when the statistics is garbage collected,
+   * but calling this eagerly can help release memory sooner.
+   */
+  release(): void;
+}
+
 /**
  * Part of {@link Context}. Used to declare uninterpreted sorts
  *

src/api/python/z3/z3.py

@@ -1154,6 +1154,30 @@ class ExprRef(AstRef):
         else:
             return []
 
+    def update(self, *args):
+        """Update the arguments of the expression.
+        
+        Return a new expression with the same function declaration and updated arguments.
+        The number of new arguments must match the current number of arguments.
+        
+        >>> f = Function('f', IntSort(), IntSort(), IntSort())
+        >>> a = Int('a')
+        >>> b = Int('b')
+        >>> c = Int('c')
+        >>> t = f(a, b)
+        >>> t.update(c, c)
+        f(c, c)
+        """
+        if z3_debug():
+            _z3_assert(is_app(self), "Z3 application expected")
+            _z3_assert(len(args) == self.num_args(), "Number of arguments does not match")
+            _z3_assert(all([is_expr(arg) for arg in args]), "Z3 expressions expected")
+        num = len(args)
+        _args = (Ast * num)()
+        for i in range(num):
+            _args[i] = args[i].as_ast()
+        return _to_expr_ref(Z3_update_term(self.ctx_ref(), self.as_ast(), num, _args), self.ctx)
+
     def from_string(self, s):
         pass