From 319db5dbb1380ecc78e96efc2639a96e826b83aa Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 11 Jan 2026 10:01:04 -0800 Subject: [PATCH] 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 | 20 +++++ src/api/dotnet/Expr.cs | 22 +++++ src/api/js/src/high-level/high-level.ts | 90 +++++++++++++++++++++ src/api/js/src/high-level/types.ts | 102 ++++++++++++++++++++++++ src/api/python/z3/z3.py | 24 ++++++ 5 files changed, 258 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 1a3b7ce8d..6dd71655a 100644 --- a/src/api/c++/z3++.h +++ b/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 _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 const& deps, expr_vector const& clause)> on_clause_eh_t; class on_clause { diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 7dabc49cd..c385a7ed4 100644 --- a/src/api/dotnet/Expr.cs +++ b/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))); } + /// + /// Substitute functions in with the expressions in . + /// + /// + /// The expressions in can have free variables. The free variable in to[i] at de-Bruijn index 0 + /// refers to the first argument of from[i], the free variable at index 1 corresponds to the second argument, and so on. + /// The arrays and must have the same size. + /// + 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(from); + Context.CheckContextMatch(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))); + } + /// /// Translates (copies) the term to the Context . /// diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index f990966b4..609cd350c 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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 { + 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 { + 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 { + 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 { + declare readonly __typename: Statistics['__typename']; + readonly ctx: Context; + 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[] { + const result: StatisticsEntry[] = []; + 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> { + return this.entries()[Symbol.iterator](); + } + + release() { + Z3.stats_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } + } + class FuncEntryImpl implements FuncEntry { declare readonly __typename: FuncEntry['__typename']; diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index df412edff..f089482a4 100644 --- a/src/api/js/src/high-level/types.ts +++ b/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 { model(): Model; + /** + * 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; + /** * Return a string describing why the last call to {@link check} returned `'unknown'`. * @@ -1150,6 +1172,8 @@ export interface Optimize { model(): Model; + statistics(): Statistics; + /** * 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 { */ fromFile(file: string): AstVector>; + /** + * Retrieve statistics for the fixedpoint solver. + * Returns performance metrics and diagnostic information. + * @returns A Statistics object containing solver metrics + */ + statistics(): Statistics; + /** * 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 extends Iterable { + /** @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 { + new (): Statistics; +} + +/** + * Statistics for solver operations + * + * Provides access to performance metrics, memory usage, decision counts, + * and other diagnostic information from solver operations. + */ +export interface Statistics extends Iterable> { + /** @hidden */ + readonly __typename: 'Statistics'; + + readonly ctx: Context; + 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[]; + + /** + * 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 * diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 33c72871c..3994f8131 100644 --- a/src/api/python/z3/z3.py +++ b/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