From f4606b1f2d69ad2f5d438c6c28755dde78b8cf14 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 17:23:26 +0000 Subject: [PATCH 1/4] Initial plan From ac10af417a2bdaa3fea148c11a2ca4bd1e33fb06 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 17:28:12 +0000 Subject: [PATCH 2/4] Add missing API methods to Go and OCaml bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/go/solver.go | 19 +++++++++++++++++++ src/api/ml/z3.ml | 32 ++++++++++++++++++++++++++++++++ src/api/ml/z3.mli | 40 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 91 insertions(+) diff --git a/src/api/go/solver.go b/src/api/go/solver.go index eab330e5f..bbda4f42e 100644 --- a/src/api/go/solver.go +++ b/src/api/go/solver.go @@ -280,6 +280,14 @@ func (s *Solver) CongruenceExplain(a, b *Expr) *Expr { return newExpr(s.ctx, ast) } +// SetInitialValue provides an initial value hint for a variable to the solver. +// This can help guide the solver to find solutions more efficiently. +// The variable must be a constant or function application, and the value must be +// compatible with the variable's sort. +func (s *Solver) SetInitialValue(variable, value *Expr) { + C.Z3_solver_set_initial_value(s.ctx.ptr, s.ptr, variable.ptr, value.ptr) +} + // Model represents a Z3 model (satisfying assignment). type Model struct { ctx *Context @@ -382,3 +390,14 @@ func (fi *FuncInterp) GetElse() *Expr { func (fi *FuncInterp) GetArity() uint { return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr)) } + +// SortUniverse returns the universe of values for an uninterpreted sort in the model. +// The universe is represented as a list of distinct expressions. +// Returns nil if the sort is not an uninterpreted sort in this model. +func (m *Model) SortUniverse(sort *Sort) []*Expr { + vec := C.Z3_model_get_sort_universe(m.ctx.ptr, m.ptr, sort.ptr) + if vec == nil { + return nil + } + return astVectorToExprs(m.ctx, vec) +} diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 8cb587ef9..65cfad207 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1940,6 +1940,38 @@ struct let interrupt (ctx:context) (s:solver) = Z3native.solver_interrupt ctx s + + let get_units x = + let av = Z3native.solver_get_units (gc x) x in + AST.ASTVector.to_expr_list av + + let get_non_units x = + let av = Z3native.solver_get_non_units (gc x) x in + AST.ASTVector.to_expr_list av + + let get_trail x = + let av = Z3native.solver_get_trail (gc x) x in + AST.ASTVector.to_expr_list av + + let get_levels x literals = + let n = List.length literals in + let levels = Array.make n 0 in + let av = Z3native.mk_ast_vector (gc x) in + List.iter (fun e -> Z3native.ast_vector_push (gc x) av e) literals; + Z3native.solver_get_levels (gc x) x av n levels; + levels + + let congruence_root x a = Z3native.solver_congruence_root (gc x) x a + + let congruence_next x a = Z3native.solver_congruence_next (gc x) x a + + let congruence_explain x a b = Z3native.solver_congruence_explain (gc x) x a b + + let from_file x = Z3native.solver_from_file (gc x) x + + let from_string x = Z3native.solver_from_string (gc x) x + + let set_initial_value x var value = Z3native.solver_set_initial_value (gc x) x var value end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index b473ff37e..4efbb074f 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3389,6 +3389,46 @@ sig it is more convenient to cancel a specific solver. Solvers that are not selected for interrupts are left alone.*) val interrupt: context -> solver -> unit + + (** Retrieve the set of units from the solver. + Units are clauses of size 1 learned by the solver during solving. *) + val get_units : solver -> Expr.expr list + + (** Retrieve the set of non-units from the solver. + Non-units are clauses of size greater than 1 learned by the solver. *) + val get_non_units : solver -> Expr.expr list + + (** Retrieve the trail (sequence of assignments) from the solver. + The trail shows the sequence of literal assignments made by the solver. *) + val get_trail : solver -> Expr.expr list + + (** Retrieve the decision levels of trail literals. + Given a list of literals from the trail, returns an array of their decision levels. + @param literals List of literals from the trail + @return Array of decision levels corresponding to the input literals *) + val get_levels : solver -> Expr.expr list -> int array + + (** Retrieve the congruence closure root of an expression. + Returns the representative of the equivalence class containing the expression. *) + val congruence_root : solver -> Expr.expr -> Expr.expr + + (** Retrieve the next element in the congruence closure equivalence class. + Congruence classes form a circular list; this returns the next element. *) + val congruence_next : solver -> Expr.expr -> Expr.expr + + (** Retrieve an explanation for why two expressions are congruent. + Returns an expression that justifies the congruence between a and b. *) + val congruence_explain : solver -> Expr.expr -> Expr.expr -> Expr.expr + + (** Parse SMT-LIB2 formulas from a file and assert them into the solver. *) + val from_file : solver -> string -> unit + + (** Parse SMT-LIB2 formulas from a string and assert them into the solver. *) + val from_string : solver -> string -> unit + + (** Provide an initial value hint for a variable to the solver. + This can help guide the solver to find solutions more efficiently. *) + val set_initial_value : solver -> Expr.expr -> Expr.expr -> unit end (** Fixedpoint solving *) From c74acb59a9038d5175b98b3bdbc1d73e5f8aab10 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Wed, 18 Feb 2026 17:45:38 +0000 Subject: [PATCH 3/4] Add test for new Go API methods Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- examples/go/test_new_api_additions.go | 74 +++++++++++++++++++++++++++ 1 file changed, 74 insertions(+) create mode 100644 examples/go/test_new_api_additions.go diff --git a/examples/go/test_new_api_additions.go b/examples/go/test_new_api_additions.go new file mode 100644 index 000000000..9a3549c13 --- /dev/null +++ b/examples/go/test_new_api_additions.go @@ -0,0 +1,74 @@ +package main + +import ( + "fmt" + "os" + "path/filepath" + + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + // Test SetInitialValue + fmt.Println("\nTesting Solver.SetInitialValue()...") + ctx2 := z3.NewContext() + solver2 := ctx2.NewSolver() + + x := ctx2.MkIntConst("x") + y := ctx2.MkIntConst("y") + + // Set initial values to guide the solver + solver2.SetInitialValue(x, ctx2.MkInt(5, ctx2.MkIntSort())) + solver2.SetInitialValue(y, ctx2.MkInt(10, ctx2.MkIntSort())) + + // Add constraints + solver2.Assert(ctx2.MkGt(x, ctx2.MkInt(0, ctx2.MkIntSort()))) + solver2.Assert(ctx2.MkGt(y, ctx2.MkInt(0, ctx2.MkIntSort()))) + + if solver2.Check() == z3.Satisfiable { + fmt.Println(" ✓ SetInitialValue works (solver found solution)") + } else { + fmt.Println(" ✗ SetInitialValue failed") + os.Exit(1) + } + + // Test FromString + fmt.Println("\nTesting Solver.FromString()...") + ctx3 := z3.NewContext() + solver3 := ctx3.NewSolver() + + smtString := "(declare-const z Int)(assert (> z 42))" + solver3.FromString(smtString) + + if solver3.Check() == z3.Satisfiable { + fmt.Println(" ✓ FromString works correctly") + } else { + fmt.Println(" ✗ FromString failed") + os.Exit(1) + } + + // Test FromFile + fmt.Println("\nTesting Solver.FromFile()...") + ctx4 := z3.NewContext() + solver4 := ctx4.NewSolver() + + // Create a temporary SMT file + tmpDir := os.TempDir() + smtFile := filepath.Join(tmpDir, "test.smt2") + err := os.WriteFile(smtFile, []byte("(declare-const w Int)\n(assert (< w 100))\n"), 0644) + if err != nil { + fmt.Printf(" ✗ Failed to create test file: %v\n", err) + os.Exit(1) + } + defer os.Remove(smtFile) + + solver4.FromFile(smtFile) + if solver4.Check() == z3.Satisfiable { + fmt.Println(" ✓ FromFile works correctly") + } else { + fmt.Println(" ✗ FromFile failed") + os.Exit(1) + } + + fmt.Println("\nAll tests passed! ✓") +} From 6c02a3b6bb8007e1130998673d4523f388c6e7b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Feb 2026 13:25:52 -0800 Subject: [PATCH 4/4] Delete examples/go/test_new_api_additions.go --- examples/go/test_new_api_additions.go | 74 --------------------------- 1 file changed, 74 deletions(-) delete mode 100644 examples/go/test_new_api_additions.go diff --git a/examples/go/test_new_api_additions.go b/examples/go/test_new_api_additions.go deleted file mode 100644 index 9a3549c13..000000000 --- a/examples/go/test_new_api_additions.go +++ /dev/null @@ -1,74 +0,0 @@ -package main - -import ( - "fmt" - "os" - "path/filepath" - - "github.com/Z3Prover/z3/src/api/go" -) - -func main() { - // Test SetInitialValue - fmt.Println("\nTesting Solver.SetInitialValue()...") - ctx2 := z3.NewContext() - solver2 := ctx2.NewSolver() - - x := ctx2.MkIntConst("x") - y := ctx2.MkIntConst("y") - - // Set initial values to guide the solver - solver2.SetInitialValue(x, ctx2.MkInt(5, ctx2.MkIntSort())) - solver2.SetInitialValue(y, ctx2.MkInt(10, ctx2.MkIntSort())) - - // Add constraints - solver2.Assert(ctx2.MkGt(x, ctx2.MkInt(0, ctx2.MkIntSort()))) - solver2.Assert(ctx2.MkGt(y, ctx2.MkInt(0, ctx2.MkIntSort()))) - - if solver2.Check() == z3.Satisfiable { - fmt.Println(" ✓ SetInitialValue works (solver found solution)") - } else { - fmt.Println(" ✗ SetInitialValue failed") - os.Exit(1) - } - - // Test FromString - fmt.Println("\nTesting Solver.FromString()...") - ctx3 := z3.NewContext() - solver3 := ctx3.NewSolver() - - smtString := "(declare-const z Int)(assert (> z 42))" - solver3.FromString(smtString) - - if solver3.Check() == z3.Satisfiable { - fmt.Println(" ✓ FromString works correctly") - } else { - fmt.Println(" ✗ FromString failed") - os.Exit(1) - } - - // Test FromFile - fmt.Println("\nTesting Solver.FromFile()...") - ctx4 := z3.NewContext() - solver4 := ctx4.NewSolver() - - // Create a temporary SMT file - tmpDir := os.TempDir() - smtFile := filepath.Join(tmpDir, "test.smt2") - err := os.WriteFile(smtFile, []byte("(declare-const w Int)\n(assert (< w 100))\n"), 0644) - if err != nil { - fmt.Printf(" ✗ Failed to create test file: %v\n", err) - os.Exit(1) - } - defer os.Remove(smtFile) - - solver4.FromFile(smtFile) - if solver4.Check() == z3.Satisfiable { - fmt.Println(" ✓ FromFile works correctly") - } else { - fmt.Println(" ✗ FromFile failed") - os.Exit(1) - } - - fmt.Println("\nAll tests passed! ✓") -}