From 08addfa6544107f2af10ed9c922f44398376297d Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 17:03:50 +0000 Subject: [PATCH 1/4] Initial plan From 9802b32a3e1eb697abbeff0f55affef364dd18c2 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 17:22:17 +0000 Subject: [PATCH 2/4] 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 | 10 +++ src/api/go/optimize.go | 12 ++++ src/api/go/simplifier.go | 54 +++++++++++++++++ src/api/go/solver.go | 41 +++++++++++++ src/api/java/Solver.java | 23 +++++++ src/api/js/src/high-level/high-level.ts | 56 +++++++++++++++-- src/api/js/src/high-level/types.ts | 81 ++++++++++++++++++++++++- src/api/ml/z3.ml | 2 + src/api/ml/z3.mli | 7 +++ 9 files changed, 280 insertions(+), 6 deletions(-) create mode 100644 src/api/go/simplifier.go diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 4b57257d8..8c33d0795 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -650,6 +650,16 @@ namespace Microsoft.Z3 return Context.BenchmarkToSmtlibString("", "", status, "", assumptions, formula); } + /// + /// Convert the solver's Boolean formula to DIMACS CNF format. + /// + /// If true, include variable names in the DIMACS output. Default is true. + /// A string containing the DIMACS CNF representation. + 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) diff --git a/src/api/go/optimize.go b/src/api/go/optimize.go index 4aead73cd..ead936ed7 100644 --- a/src/api/go/optimize.go +++ b/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 +} diff --git a/src/api/go/simplifier.go b/src/api/go/simplifier.go new file mode 100644 index 000000000..a8ec39360 --- /dev/null +++ b/src/api/go/simplifier.go @@ -0,0 +1,54 @@ +package z3 + +/* +#include "z3.h" +#include +*/ +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)) +} diff --git a/src/api/go/solver.go b/src/api/go/solver.go index 5e98476e2..7fd8f4586 100644 --- a/src/api/go/solver.go +++ b/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 diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 528169959..0f3023b50 100644 --- a/src/api/java/Solver.java +++ b/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. * diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 9aaa6a1a4..9958af691 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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): Solver { + const ptr = check(Z3.solver_translate(contextPtr, this.ptr, target.ptr)); + return new (target.Solver as unknown as new (ptr: Z3_solver) => Solver)(ptr); + } + + proof(): Expr | 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 | BitVec) { - check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast)); + maximize(expr: Arith | BitVec): number { + return check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast)); } - minimize(expr: Arith | BitVec) { - check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast)); + minimize(expr: Arith | BitVec): number { + return check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast)); + } + + getLower(index: number): Expr { + return _toExpr(check(Z3.optimize_get_lower(contextPtr, this.ptr, index))); + } + + getUpper(index: number): Expr { + return _toExpr(check(Z3.optimize_get_upper(contextPtr, this.ptr, index))); + } + + unsatCore(): AstVector> { + return new AstVectorImpl(check(Z3.optimize_get_unsat_core(contextPtr, this.ptr))); + } + + objectives(): AstVector> { + 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): Optimize { + const ptr = check(Z3.optimize_translate(contextPtr, this.ptr, target.ptr)); + return new (target.Optimize as unknown as new (ptr: Z3_optimize) => Optimize)(ptr); } async check(...exprs: (Bool | AstVector>)[]): Promise { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index e6d29f340..69a0f10eb 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1394,6 +1394,28 @@ export interface Solver { */ 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): Solver; + + /** + * 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 | 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 { fromString(s: string): void; - maximize(expr: Arith): 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): 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 | BitVec): 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 | BitVec): 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; + + /** + * 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; + + /** + * Retrieve the unsat core after a check that returned 'unsat'. + * @returns An AstVector containing the subset of assumptions that caused UNSAT + */ + unsatCore(): AstVector>; + + /** + * Retrieve the set of objective expressions. + * @returns An AstVector containing the objectives + */ + objectives(): AstVector>; + + /** + * 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): Optimize; check(...exprs: (Bool | AstVector>)[]): Promise; diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 40e0a1451..96e4ab1b6 100644 --- a/src/api/ml/z3.ml +++ b/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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5c13941aa..f9c0de47c 100644 --- a/src/api/ml/z3.mli +++ b/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 From ce04a243488e02f7eb50bc98b72e01f219b5291f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 24 Feb 2026 17:28:45 +0000 Subject: [PATCH 3/4] Improve TypeScript Optimize documentation for handle index clarity Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/js/src/high-level/high-level.ts | 2 +- src/api/js/src/high-level/types.ts | 26 +++++++++++++++++++++++-- 2 files changed, 25 insertions(+), 3 deletions(-) diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 9958af691..367696a12 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -2142,7 +2142,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { proof(): Expr | null { const result = Z3.solver_get_proof(contextPtr, this.ptr); throwIfError(); - if (result === null) { + if (!result) { return null; } return _toExpr(result); diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 69a0f10eb..e070c4b58 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -1478,14 +1478,36 @@ export interface Optimize { /** * 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} + * @returns A zero-based numeric handle index for this objective, used to retrieve bounds + * via {@link getLower}/{@link getUpper} after calling {@link check} + * + * @example + * ```typescript + * const opt = new Optimize(); + * const x = Int.const('x'); + * opt.add(x.ge(0), x.le(10)); + * const h = opt.maximize(x); + * await opt.check(); + * console.log('Max x:', opt.getUpper(h).toString()); // '10' + * ``` */ maximize(expr: Arith | BitVec): 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} + * @returns A zero-based numeric handle index for this objective, used to retrieve bounds + * via {@link getLower}/{@link getUpper} after calling {@link check} + * + * @example + * ```typescript + * const opt = new Optimize(); + * const x = Int.const('x'); + * opt.add(x.ge(0), x.le(10)); + * const h = opt.minimize(x); + * await opt.check(); + * console.log('Min x:', opt.getLower(h).toString()); // '0' + * ``` */ minimize(expr: Arith | BitVec): number; From cfb3a0175646a8abcabad23a20641c285018e654 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Feb 2026 09:58:12 -0800 Subject: [PATCH 4/4] Update Solver.cs --- src/api/dotnet/Solver.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 8c33d0795..b06f9ed16 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -657,7 +657,7 @@ namespace Microsoft.Z3 /// A string containing the DIMACS CNF representation. public string ToDimacs(bool includeNames = true) { - return Native.Z3_solver_to_dimacs_string(Context.nCtx, NativeObject, includeNames); + return Native.Z3_solver_to_dimacs_string(Context.nCtx, NativeObject, includeNames ? (byte)1 : (byte)0); } #region Internal