From 5ecbb9d655af7a52b8bac68eea61876c624a3067 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 17 Feb 2026 16:38:39 +0000 Subject: [PATCH] Add missing solver API functions to Go bindings - Add Units() - get unit clauses learned by solver - Add NonUnits() - get non-unit clauses - Add Trail() - get decision trail - Add TrailLevels() - get trail decision levels - Add CongruenceRoot() - get congruence class representative - Add CongruenceNext() - get next element in congruence class - Add CongruenceExplain() - explain why two terms are congruent - Add test example demonstrating new APIs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- examples/go/test_new_apis.go | 87 +++++++++++++++++++++++++++++++++++ src/api/go/solver.go | 88 ++++++++++++++++++++++++++++++++++++ 2 files changed, 175 insertions(+) create mode 100644 examples/go/test_new_apis.go diff --git a/examples/go/test_new_apis.go b/examples/go/test_new_apis.go new file mode 100644 index 000000000..f76845471 --- /dev/null +++ b/examples/go/test_new_apis.go @@ -0,0 +1,87 @@ +package main + +import ( + "fmt" + "github.com/Z3Prover/z3/src/api/go" +) + +func main() { + // Create a new Z3 context + ctx := z3.NewContext() + fmt.Println("Z3 Go Bindings - New APIs Test") + fmt.Println("================================") + + // Test diagnostic APIs + fmt.Println("\nTest 1: Solver Diagnostic APIs") + solver := ctx.NewSolver() + + // Create some simple constraints + x := ctx.MkIntConst("x") + y := ctx.MkIntConst("y") + zero := ctx.MkInt(0, ctx.MkIntSort()) + ten := ctx.MkInt(10, ctx.MkIntSort()) + + solver.Assert(ctx.MkGt(x, zero)) + solver.Assert(ctx.MkLt(x, ten)) + solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ten)) + + // Check satisfiability + status := solver.Check() + fmt.Println("Status:", status.String()) + + if status == z3.Satisfiable { + // Test Units() - get unit clauses + units := solver.Units() + fmt.Printf("Units: %d clauses\n", len(units)) + for i, unit := range units { + fmt.Printf(" Unit %d: %s\n", i, unit.String()) + } + + // Test NonUnits() - get non-unit clauses + nonUnits := solver.NonUnits() + fmt.Printf("NonUnits: %d clauses\n", len(nonUnits)) + for i, nu := range nonUnits { + fmt.Printf(" NonUnit %d: %s\n", i, nu.String()) + } + + // Note: Trail() and TrailLevels() only work with SimpleSolver + // For default solvers created with NewSolver(), these may not be available + fmt.Println("Note: Trail() and TrailLevels() are available primarily for SimpleSolver") + } + + // Test congruence closure APIs + fmt.Println("\nTest 2: Congruence Closure APIs") + solver2 := ctx.NewSolver() + + // Create expressions for congruence testing + a := ctx.MkIntConst("a") + b := ctx.MkIntConst("b") + c := ctx.MkIntConst("c") + + // Assert a = b and b = c (so a should be congruent to c) + solver2.Assert(ctx.MkEq(a, b)) + solver2.Assert(ctx.MkEq(b, c)) + + status = solver2.Check() + fmt.Println("Status:", status.String()) + + if status == z3.Satisfiable { + // Test CongruenceRoot() - get congruence class representative + rootA := solver2.CongruenceRoot(a) + rootB := solver2.CongruenceRoot(b) + rootC := solver2.CongruenceRoot(c) + fmt.Printf("CongruenceRoot(a): %s\n", rootA.String()) + fmt.Printf("CongruenceRoot(b): %s\n", rootB.String()) + fmt.Printf("CongruenceRoot(c): %s\n", rootC.String()) + + // Test CongruenceNext() - get next element in congruence class + nextA := solver2.CongruenceNext(a) + fmt.Printf("CongruenceNext(a): %s\n", nextA.String()) + + // Test CongruenceExplain() - explain why two terms are congruent + explain := solver2.CongruenceExplain(a, c) + fmt.Printf("CongruenceExplain(a, c): %s\n", explain.String()) + } + + fmt.Println("\nAll new API tests completed successfully!") +} diff --git a/src/api/go/solver.go b/src/api/go/solver.go index dc5a0e5fe..192b24d42 100644 --- a/src/api/go/solver.go +++ b/src/api/go/solver.go @@ -195,6 +195,94 @@ func (s *Solver) Interrupt() { C.Z3_solver_interrupt(s.ctx.ptr, s.ptr) } +// Units returns the unit clauses (literals) learned by the solver. +// Unit clauses are assertions that have been simplified to single literals. +// This is useful for debugging and understanding solver behavior. +func (s *Solver) Units() []*Expr { + vec := C.Z3_solver_get_units(s.ctx.ptr, s.ptr) + return astVectorToExprs(s.ctx, vec) +} + +// NonUnits returns the non-unit clauses in the solver's current state. +// These are atomic formulas that are not unit clauses. +// This is useful for debugging and understanding solver behavior. +func (s *Solver) NonUnits() []*Expr { + vec := C.Z3_solver_get_non_units(s.ctx.ptr, s.ptr) + return astVectorToExprs(s.ctx, vec) +} + +// Trail returns the decision trail of the solver. +// The trail contains the sequence of literals assigned during search. +// This is useful for understanding the solver's decision history. +func (s *Solver) Trail() []*Expr { + vec := C.Z3_solver_get_trail(s.ctx.ptr, s.ptr) + return astVectorToExprs(s.ctx, vec) +} + +// TrailLevels returns the decision levels for each literal in the trail. +// The returned slice has the same length as the trail, where each element +// indicates the decision level at which the corresponding trail literal was assigned. +// This is useful for understanding the structure of the search tree. +func (s *Solver) TrailLevels() []uint { + trail := s.Trail() + n := len(trail) + if n == 0 { + return []uint{} + } + + // Create C arrays for the literals and levels + literals := make([]C.Z3_ast, n) + for i, expr := range trail { + literals[i] = expr.ptr + } + levels := make([]C.uint, n) + + // Create a temporary ast_vector from the trail literals + vec := C.Z3_mk_ast_vector(s.ctx.ptr) + C.Z3_ast_vector_inc_ref(s.ctx.ptr, vec) + for _, lit := range literals { + C.Z3_ast_vector_push(s.ctx.ptr, vec, lit) + } + + // Get the levels + C.Z3_solver_get_levels(s.ctx.ptr, s.ptr, vec, C.uint(n), &levels[0]) + C.Z3_ast_vector_dec_ref(s.ctx.ptr, vec) + + // Convert to Go slice + result := make([]uint, n) + for i := 0; i < n; i++ { + result[i] = uint(levels[i]) + } + return result +} + +// CongruenceRoot returns the congruence class representative of the given expression. +// This returns the root element in the congruence closure for the term. +// The function primarily works for SimpleSolver. Terms and variables that are +// eliminated during pre-processing are not visible to the congruence closure. +func (s *Solver) CongruenceRoot(expr *Expr) *Expr { + ast := C.Z3_solver_congruence_root(s.ctx.ptr, s.ptr, expr.ptr) + return newExpr(s.ctx, ast) +} + +// CongruenceNext returns the next element in the congruence class of the given expression. +// This allows iteration through all elements in a congruence class. +// The function primarily works for SimpleSolver. Terms and variables that are +// eliminated during pre-processing are not visible to the congruence closure. +func (s *Solver) CongruenceNext(expr *Expr) *Expr { + ast := C.Z3_solver_congruence_next(s.ctx.ptr, s.ptr, expr.ptr) + return newExpr(s.ctx, ast) +} + +// CongruenceExplain returns an explanation for why two expressions are congruent. +// The result is an expression that justifies the congruence between a and b. +// The function primarily works for SimpleSolver. Terms and variables that are +// eliminated during pre-processing are not visible to the congruence closure. +func (s *Solver) CongruenceExplain(a, b *Expr) *Expr { + ast := C.Z3_solver_congruence_explain(s.ctx.ptr, s.ptr, a.ptr, b.ptr) + return newExpr(s.ctx, ast) +} + // Model represents a Z3 model (satisfying assignment). type Model struct { ctx *Context