Add missing API methods: dimacs, translate, proof, addSimplifier, getLower/getUpper, etc.

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

src/api/dotnet/Solver.cs

@@ -650,6 +650,16 @@ namespace Microsoft.Z3
             return Context.BenchmarkToSmtlibString("", "", status, "", assumptions, formula);
         }
 
+        /// <summary>
+        /// Convert the solver's Boolean formula to DIMACS CNF format.
+        /// </summary>
+        /// <param name="includeNames">If true, include variable names in the DIMACS output. Default is true.</param>
+        /// <returns>A string containing the DIMACS CNF representation.</returns>
+        public string ToDimacs(bool includeNames = true)
+        {
+            return Native.Z3_solver_to_dimacs_string(Context.nCtx, NativeObject, includeNames);
+        }
+
         #region Internal
         internal Solver(Context ctx, IntPtr obj)
             : base(ctx, obj)

src/api/go/optimize.go

@@ -193,3 +193,15 @@ func (o *Optimize) FromString(s string) {
 	defer C.free(unsafe.Pointer(cStr))
 	C.Z3_optimize_from_string(o.ctx.ptr, o.ptr, cStr)
 }
+
+// Translate creates a copy of the optimize context in the target context.
+// This is useful when working with multiple Z3 contexts.
+func (o *Optimize) Translate(target *Context) *Optimize {
+	ptr := C.Z3_optimize_translate(o.ctx.ptr, o.ptr, target.ptr)
+	newOpt := &Optimize{ctx: target, ptr: ptr}
+	C.Z3_optimize_inc_ref(target.ptr, ptr)
+	runtime.SetFinalizer(newOpt, func(opt *Optimize) {
+		C.Z3_optimize_dec_ref(opt.ctx.ptr, opt.ptr)
+	})
+	return newOpt
+}

src/api/go/simplifier.go

@@ -0,0 +1,54 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Simplifier represents a Z3 simplifier for pre-processing solver assertions.
+type Simplifier struct {
+	ctx *Context
+	ptr C.Z3_simplifier
+}
+
+// newSimplifier creates a new Simplifier and manages its reference count.
+func newSimplifier(ctx *Context, ptr C.Z3_simplifier) *Simplifier {
+	s := &Simplifier{ctx: ctx, ptr: ptr}
+	C.Z3_simplifier_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(s, func(simp *Simplifier) {
+		C.Z3_simplifier_dec_ref(simp.ctx.ptr, simp.ptr)
+	})
+	return s
+}
+
+// MkSimplifier creates a simplifier with the given name.
+func (c *Context) MkSimplifier(name string) *Simplifier {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return newSimplifier(c, C.Z3_mk_simplifier(c.ptr, cName))
+}
+
+// AndThen creates a simplifier that applies s followed by s2.
+func (s *Simplifier) AndThen(s2 *Simplifier) *Simplifier {
+	return newSimplifier(s.ctx, C.Z3_simplifier_and_then(s.ctx.ptr, s.ptr, s2.ptr))
+}
+
+// UsingParams creates a simplifier that uses the given parameters.
+func (s *Simplifier) UsingParams(params *Params) *Simplifier {
+	return newSimplifier(s.ctx, C.Z3_simplifier_using_params(s.ctx.ptr, s.ptr, params.ptr))
+}
+
+// GetHelp returns help information for the simplifier.
+func (s *Simplifier) GetHelp() string {
+	return C.GoString(C.Z3_simplifier_get_help(s.ctx.ptr, s.ptr))
+}
+
+// GetParamDescrs returns parameter descriptions for the simplifier.
+func (s *Simplifier) GetParamDescrs() *ParamDescrs {
+	return newParamDescrs(s.ctx, C.Z3_simplifier_get_param_descrs(s.ctx.ptr, s.ptr))
+}

src/api/go/solver.go

@@ -357,6 +357,47 @@ func (dst *Solver) ImportModelConverter(src *Solver) {
 	C.Z3_solver_import_model_converter(dst.ctx.ptr, src.ptr, dst.ptr)
 }
 
+// Translate creates a copy of the solver in the target context.
+// This is useful when working with multiple Z3 contexts.
+func (s *Solver) Translate(target *Context) *Solver {
+	ptr := C.Z3_solver_translate(s.ctx.ptr, s.ptr, target.ptr)
+	newSolver := &Solver{ctx: target, ptr: ptr}
+	C.Z3_solver_inc_ref(target.ptr, ptr)
+	runtime.SetFinalizer(newSolver, func(solver *Solver) {
+		C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
+	})
+	return newSolver
+}
+
+// GetProof returns the proof of unsatisfiability from the last check.
+// Returns nil if no proof is available (e.g. the result was not UNSAT,
+// or proof production is disabled).
+func (s *Solver) GetProof() *Expr {
+	result := C.Z3_solver_get_proof(s.ctx.ptr, s.ptr)
+	if result == nil {
+		return nil
+	}
+	return newExpr(s.ctx, result)
+}
+
+// AddSimplifier creates a new solver with the given simplifier attached for
+// pre-processing assertions before solving.
+func (s *Solver) AddSimplifier(simplifier *Simplifier) *Solver {
+	ptr := C.Z3_solver_add_simplifier(s.ctx.ptr, s.ptr, simplifier.ptr)
+	newSolver := &Solver{ctx: s.ctx, ptr: ptr}
+	C.Z3_solver_inc_ref(s.ctx.ptr, ptr)
+	runtime.SetFinalizer(newSolver, func(solver *Solver) {
+		C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
+	})
+	return newSolver
+}
+
+// Dimacs converts the solver's Boolean formula to DIMACS CNF format.
+// If includeNames is true, variable names are included in the output.
+func (s *Solver) Dimacs(includeNames bool) string {
+	return C.GoString(C.Z3_solver_to_dimacs_string(s.ctx.ptr, s.ptr, C.bool(includeNames)))
+}
+
 // Model represents a Z3 model (satisfying assignment).
 type Model struct {
 	ctx *Context

src/api/java/Solver.java

@@ -566,6 +566,29 @@ public class Solver extends Z3Object {
         return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
     }
 
+    /**
+     * Create a new solver with pre-processing simplification attached.
+     *
+     * @param simplifier The simplifier to attach for pre-processing
+     * @return A new solver with the simplifier applied
+     **/
+    public Solver addSimplifier(Simplifier simplifier)
+    {
+        return new Solver(getContext(), Native.solverAddSimplifier(
+                getContext().nCtx(), getNativeObject(), simplifier.getNativeObject()));
+    }
+
+    /**
+     * Convert the solver's Boolean formula to DIMACS CNF format.
+     *
+     * @param includeNames If true, include variable names in the DIMACS output
+     * @return A string containing the DIMACS CNF representation
+     **/
+    public String toDimacs(boolean includeNames)
+    {
+        return Native.solverToDimacsString(getContext().nCtx(), getNativeObject(), includeNames);
+    }
+
     /**
      * Solver statistics.
      * 

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

@@ -2130,6 +2130,24 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         ));
       }
 
+      dimacs(includeNames: boolean = true): string {
+        return check(Z3.solver_to_dimacs_string(contextPtr, this.ptr, includeNames));
+      }
+
+      translate(target: Context<Name>): Solver<Name> {
+        const ptr = check(Z3.solver_translate(contextPtr, this.ptr, target.ptr));
+        return new (target.Solver as unknown as new (ptr: Z3_solver) => Solver<Name>)(ptr);
+      }
+
+      proof(): Expr<Name> | null {
+        const result = Z3.solver_get_proof(contextPtr, this.ptr);
+        throwIfError();
+        if (result === null) {
+          return null;
+        }
+        return _toExpr(result);
+      }
+
       fromString(s: string) {
         Z3.solver_from_string(contextPtr, this.ptr, s);
         throwIfError();
@@ -2306,12 +2324,42 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr)));
       }
 
-      maximize(expr: Arith<Name> | BitVec<number, Name>) {
-        check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast));
+      maximize(expr: Arith<Name> | BitVec<number, Name>): number {
+        return check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast));
       }
 
-      minimize(expr: Arith<Name> | BitVec<number, Name>) {
-        check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast));
+      minimize(expr: Arith<Name> | BitVec<number, Name>): number {
+        return check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast));
+      }
+
+      getLower(index: number): Expr<Name> {
+        return _toExpr(check(Z3.optimize_get_lower(contextPtr, this.ptr, index)));
+      }
+
+      getUpper(index: number): Expr<Name> {
+        return _toExpr(check(Z3.optimize_get_upper(contextPtr, this.ptr, index)));
+      }
+
+      unsatCore(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.optimize_get_unsat_core(contextPtr, this.ptr)));
+      }
+
+      objectives(): AstVector<Name, Expr<Name>> {
+        return new AstVectorImpl(check(Z3.optimize_get_objectives(contextPtr, this.ptr)));
+      }
+
+      reasonUnknown(): string {
+        return check(Z3.optimize_get_reason_unknown(contextPtr, this.ptr));
+      }
+
+      fromFile(filename: string): void {
+        Z3.optimize_from_file(contextPtr, this.ptr, filename);
+        throwIfError();
+      }
+
+      translate(target: Context<Name>): Optimize<Name> {
+        const ptr = check(Z3.optimize_translate(contextPtr, this.ptr, target.ptr));
+        return new (target.Optimize as unknown as new (ptr: Z3_optimize) => Optimize<Name>)(ptr);
       }
 
       async check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult> {

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

@@ -1394,6 +1394,28 @@ export interface Solver<Name extends string = 'main'> {
    */
   toSmtlib2(status?: string): string;
 
+  /**
+   * Convert the solver's Boolean formula to DIMACS CNF format.
+   *
+   * @param includeNames - If true, include variable names in the output (default: true)
+   * @returns A string containing the DIMACS CNF representation
+   */
+  dimacs(includeNames?: boolean): string;
+
+  /**
+   * Translate the solver to a different context.
+   * @param target - The target context
+   * @returns A new Solver instance in the target context
+   */
+  translate(target: Context<Name>): Solver<Name>;
+
+  /**
+   * Retrieve a proof of unsatisfiability after a check that returned 'unsat'.
+   * Requires proof production to be enabled.
+   * @returns An expression representing the proof, or null if unavailable
+   */
+  proof(): Expr<Name> | null;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,
@@ -1446,9 +1468,64 @@ export interface Optimize<Name extends string = 'main'> {
 
   fromString(s: string): void;
 
-  maximize(expr: Arith<Name>): void;
+  /**
+   * Load SMT-LIB2 format assertions from a file into the optimizer.
+   *
+   * @param filename - Path to the file containing SMT-LIB2 format assertions
+   */
+  fromFile(filename: string): void;
 
-  minimize(expr: Arith<Name>): void;
+  /**
+   * Add a maximization objective.
+   * @param expr - The expression to maximize
+   * @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
+   */
+  maximize(expr: Arith<Name> | BitVec<number, Name>): number;
+
+  /**
+   * Add a minimization objective.
+   * @param expr - The expression to minimize
+   * @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
+   */
+  minimize(expr: Arith<Name> | BitVec<number, Name>): number;
+
+  /**
+   * Retrieve the lower bound for the objective at the given handle index.
+   * Call this after {@link check} returns 'sat'.
+   * @param index - The handle index returned by {@link maximize} or {@link minimize}
+   */
+  getLower(index: number): Expr<Name>;
+
+  /**
+   * Retrieve the upper bound for the objective at the given handle index.
+   * Call this after {@link check} returns 'sat'.
+   * @param index - The handle index returned by {@link maximize} or {@link minimize}
+   */
+  getUpper(index: number): Expr<Name>;
+
+  /**
+   * Retrieve the unsat core after a check that returned 'unsat'.
+   * @returns An AstVector containing the subset of assumptions that caused UNSAT
+   */
+  unsatCore(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Retrieve the set of objective expressions.
+   * @returns An AstVector containing the objectives
+   */
+  objectives(): AstVector<Name, Expr<Name>>;
+
+  /**
+   * Return a string describing why the last call to {@link check} returned 'unknown'.
+   */
+  reasonUnknown(): string;
+
+  /**
+   * Translate the optimize context to a different context.
+   * @param target - The target context
+   * @returns A new Optimize instance in the target context
+   */
+  translate(target: Context<Name>): Optimize<Name>;
 
   check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
 

src/api/ml/z3.ml

@@ -1955,6 +1955,7 @@ struct
   let add_simplifier = Z3native.solver_add_simplifier
   let translate x = Z3native.solver_translate (gc x) x
   let to_string x = Z3native.solver_to_string (gc x) x
+  let to_dimacs x include_names = Z3native.solver_to_dimacs_string (gc x) x include_names
 
   let interrupt (ctx:context) (s:solver) =
     Z3native.solver_interrupt ctx s
@@ -2145,6 +2146,7 @@ struct
   let from_string (x:optimize) (s:string) = Z3native.optimize_from_string (gc x) x s
   let get_assertions (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_assertions (gc x) x)
   let get_objectives (x:optimize) = AST.ASTVector.to_expr_list (Z3native.optimize_get_objectives (gc x) x)
+  let translate (x:optimize) (to_ctx:context) = Z3native.optimize_translate (gc x) x to_ctx
 end
 
 

src/api/ml/z3.mli

@@ -3428,6 +3428,10 @@ sig
   (** A string representation of the solver. *)
   val to_string : solver -> string
 
+  (** Convert the solver's Boolean formula to DIMACS CNF format.
+      @param include_names If true, include variable names in the output. *)
+  val to_dimacs : solver -> bool -> string
+
   (** Solver local interrupt.
 
       Normally you should use Z3_interrupt to cancel solvers because only
@@ -3665,6 +3669,9 @@ sig
       corresponding minimization objective. In this way the resulting
       objective function is always returned as a minimization objective. *)
   val get_objectives : optimize -> Expr.expr list
+
+  (** Translate the optimize context to a different context. *)
+  val translate : optimize -> context -> optimize
 end