Add benchmark export to C# and TypeScript APIs (#8228)

* Initial plan

* Add benchmark export functionality to C# and TypeScript APIs

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

* Fix TypeScript build error: remove redundant array length parameter

The Z3 TypeScript wrapper auto-generates array length parameters from the array itself, so passing assumptions.length explicitly causes a parameter count mismatch. Removed the redundant parameter.

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/dotnet/Context.cs

@@ -3491,6 +3491,32 @@ namespace Microsoft.Z3
                 AST.ArrayLength(decls), Symbol.ArrayToNative(declNames), AST.ArrayToNative(decls)));
             return assertions.ToBoolExprArray();
         }
+
+        /// <summary>
+        /// Convert a benchmark into SMT-LIB2 formatted string.
+        /// </summary>
+        /// <param name="name">Name of the benchmark. May be null.</param>
+        /// <param name="logic">The benchmark logic. May be null.</param>
+        /// <param name="status">Status string, such as "sat", "unsat", or "unknown".</param>
+        /// <param name="attributes">Other attributes, such as source, difficulty or category. May be null.</param>
+        /// <param name="assumptions">Auxiliary assumptions.</param>
+        /// <param name="formula">Formula to be checked for consistency in conjunction with assumptions.</param>
+        /// <returns>A string representation of the benchmark in SMT-LIB2 format.</returns>
+        public string BenchmarkToSmtlibString(string name, string logic, string status, string attributes, BoolExpr[] assumptions, BoolExpr formula)
+        {
+            Debug.Assert(assumptions != null);
+            Debug.Assert(formula != null);
+
+            return Native.Z3_benchmark_to_smtlib_string(
+                nCtx,
+                name,
+                logic,
+                status,
+                attributes,
+                (uint)(assumptions?.Length ?? 0),
+                AST.ArrayToNative(assumptions),
+                formula.NativeObject);
+        }
         #endregion
 
         #region Goals

src/api/dotnet/Solver.cs

@@ -590,6 +590,34 @@ namespace Microsoft.Z3
             return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Convert the solver assertions to SMT-LIB2 format as a benchmark.
+        /// </summary>
+        /// <param name="status">Status string, such as "sat", "unsat", or "unknown". Default is "unknown".</param>
+        /// <returns>A string representation of the solver's assertions in SMT-LIB2 format.</returns>
+        public string ToSmt2(string status = "unknown")
+        {
+            BoolExpr[] assertions = Assertions;
+            BoolExpr formula;
+            BoolExpr[] assumptions;
+            
+            if (assertions.Length > 0)
+            {
+                // Use last assertion as formula and rest as assumptions
+                assumptions = new BoolExpr[assertions.Length - 1];
+                Array.Copy(assertions, assumptions, assertions.Length - 1);
+                formula = assertions[assertions.Length - 1];
+            }
+            else
+            {
+                // No assertions, use true
+                assumptions = new BoolExpr[0];
+                formula = Context.MkTrue();
+            }
+
+            return Context.BenchmarkToSmtlibString("", "", status, "", assumptions, formula);
+        }
+
         #region Internal
         internal Solver(Context ctx, IntPtr obj)
             : base(ctx, obj)

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

@@ -1899,6 +1899,36 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return check(Z3.solver_to_string(contextPtr, this.ptr));
       }
 
+      toSmtlib2(status: string = 'unknown'): string {
+        const assertionsVec = this.assertions();
+        const numAssertions = assertionsVec.length();
+        let formula: Z3_ast;
+        let assumptions: Z3_ast[];
+
+        if (numAssertions > 0) {
+          // Use last assertion as formula and rest as assumptions
+          assumptions = [];
+          for (let i = 0; i < numAssertions - 1; i++) {
+            assumptions.push(assertionsVec.get(i).ast);
+          }
+          formula = assertionsVec.get(numAssertions - 1).ast;
+        } else {
+          // No assertions, use true
+          assumptions = [];
+          formula = ctx.Bool.val(true).ast;
+        }
+
+        return check(Z3.benchmark_to_smtlib_string(
+          contextPtr,
+          '',
+          '',
+          status,
+          '',
+          assumptions,
+          formula
+        ));
+      }
+
       fromString(s: string) {
         Z3.solver_from_string(contextPtr, this.ptr, s);
         throwIfError();

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

@@ -1172,6 +1172,28 @@ export interface Solver<Name extends string = 'main'> {
    */
   fromFile(filename: string): void;
 
+  /**
+   * Convert the solver's assertions to SMT-LIB2 format as a benchmark.
+   * 
+   * This exports the current set of assertions in the solver as an SMT-LIB2 string,
+   * which can be used for bug reporting, sharing problems, or benchmarking.
+   *
+   * @param status - Status string such as "sat", "unsat", or "unknown" (default: "unknown")
+   * @returns A string representation of the solver's assertions in SMT-LIB2 format
+   *
+   * @example
+   * ```typescript
+   * const solver = new Solver();
+   * const x = Int.const('x');
+   * const y = Int.const('y');
+   * solver.add(x.gt(0));
+   * solver.add(y.eq(x.add(1)));
+   * const smtlib2 = solver.toSmtlib2('unknown');
+   * console.log(smtlib2); // Prints SMT-LIB2 formatted problem
+   * ```
+   */
+  toSmtlib2(status?: string): string;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,