Go/OCaml API gaps: substitution, AST introspection, Spacer, Goal completion (#9277)

* fix: address issues 1,2,4,5 and add Goal API to Go bindings Issue 2 (Go): Add Substitute, SubstituteVars, SubstituteFuns to Expr Issue 4 (Go): Add GetDecl, NumArgs, Arg to Expr for AST app introspection Goal API (Go): Add IsInconsistent and ToDimacsString to Goal ASTVector (Go): Add public Size, Get, String methods ASTMap (Go): Add ASTMap type with full CRUD API in spacer.go Issue 1 (Go): Add Spacer fixedpoint methods QueryFromLvl, GetGroundSatAnswer, GetRulesAlongTrace, GetRuleNamesAlongTrace, AddInvariant, GetReachable Issue 1 (Go): Add context-level QE functions ModelExtrapolate, QeLite, QeModelProject, QeModelProjectSkolem, QeModelProjectWithWitness Issue 5 (OCaml): Add substitute_funs to z3.ml and z3.mli Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/afa18588-47af-4720-8cea-55fe0544ae55 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * fix: add substitute_funs to Expr module sig in z3.ml The internal sig...end block in z3.ml (the module type declaration for Expr) was missing val substitute_funs, causing OCaml compiler error: The value substitute_funs is required but not provided Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c6662702-46a3-4aa0-b225-d6b73c2a2505 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>
2026-04-15 00:35:11 +00:00 · 2026-04-12 14:00:03 -07:00 · 2026-04-12 14:00:03 -07:00 · 68e528eaf7
commit 68e528eaf7
parent 1566d3cc41
6 changed files with 290 additions and 0 deletions
--- a/src/api/go/fixedpoint.go
+++ b/src/api/go/fixedpoint.go
@ -218,6 +218,59 @@ func (f *Fixedpoint) FromFile(filename string) {
 	C.Z3_fixedpoint_from_file(f.ctx.ptr, f.ptr, cstr)
 }

+// QueryFromLvl poses a query against the asserted rules at the given level.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) QueryFromLvl(query *Expr, lvl uint) Status {
+	result := C.Z3_fixedpoint_query_from_lvl(f.ctx.ptr, f.ptr, query.ptr, C.uint(lvl))
+	switch result {
+	case C.Z3_L_TRUE:
+		return Satisfiable
+	case C.Z3_L_FALSE:
+		return Unsatisfiable
+	default:
+		return Unknown
+	}
+}
+
+// GetGroundSatAnswer retrieves a bottom-up sequence of ground facts.
+// The previous call to Query or QueryFromLvl must have returned Satisfiable.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) GetGroundSatAnswer() *Expr {
+	ptr := C.Z3_fixedpoint_get_ground_sat_answer(f.ctx.ptr, f.ptr)
+	if ptr == nil {
+		return nil
+	}
+	return newExpr(f.ctx, ptr)
+}
+
+// GetRulesAlongTrace returns the list of rules along the counterexample trace.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) GetRulesAlongTrace() *ASTVector {
+	return newASTVector(f.ctx, C.Z3_fixedpoint_get_rules_along_trace(f.ctx.ptr, f.ptr))
+}
+
+// GetRuleNamesAlongTrace returns the list of rule names along the counterexample trace.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) GetRuleNamesAlongTrace() *Symbol {
+	return newSymbol(f.ctx, C.Z3_fixedpoint_get_rule_names_along_trace(f.ctx.ptr, f.ptr))
+}
+
+// AddInvariant adds an assumed invariant for the predicate pred.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) AddInvariant(pred *FuncDecl, property *Expr) {
+	C.Z3_fixedpoint_add_invariant(f.ctx.ptr, f.ptr, pred.ptr, property.ptr)
+}
+
+// GetReachable retrieves the reachable states of a predicate.
+// This is a Spacer-specific function.
+func (f *Fixedpoint) GetReachable(pred *FuncDecl) *Expr {
+	ptr := C.Z3_fixedpoint_get_reachable(f.ctx.ptr, f.ptr, pred.ptr)
+	if ptr == nil {
+		return nil
+	}
+	return newExpr(f.ctx, ptr)
+}
+
 // Statistics represents statistics for Z3 solvers
 type Statistics struct {
 	ctx *Context
--- a/src/api/go/spacer.go
+++ b/src/api/go/spacer.go
@ -0,0 +1,131 @@
+// Copyright (c) Microsoft Corporation 2025
+// Z3 Go API: Spacer quantifier elimination and model projection functions
+
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import "runtime"
+
+// ASTMap represents a mapping from Z3 ASTs to Z3 ASTs.
+type ASTMap struct {
+	ctx *Context
+	ptr C.Z3_ast_map
+}
+
+// newASTMap creates a new ASTMap and manages its reference count.
+func newASTMap(ctx *Context, ptr C.Z3_ast_map) *ASTMap {
+	m := &ASTMap{ctx: ctx, ptr: ptr}
+	C.Z3_ast_map_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(m, func(am *ASTMap) {
+		C.Z3_ast_map_dec_ref(am.ctx.ptr, am.ptr)
+	})
+	return m
+}
+
+// MkASTMap creates a new empty AST map.
+func (c *Context) MkASTMap() *ASTMap {
+	return newASTMap(c, C.Z3_mk_ast_map(c.ptr))
+}
+
+// Contains returns true if the map contains the key k.
+func (m *ASTMap) Contains(k *Expr) bool {
+	return bool(C.Z3_ast_map_contains(m.ctx.ptr, m.ptr, k.ptr))
+}
+
+// Find returns the value associated with key k.
+func (m *ASTMap) Find(k *Expr) *Expr {
+	return newExpr(m.ctx, C.Z3_ast_map_find(m.ctx.ptr, m.ptr, k.ptr))
+}
+
+// Insert associates key k with value v in the map.
+func (m *ASTMap) Insert(k, v *Expr) {
+	C.Z3_ast_map_insert(m.ctx.ptr, m.ptr, k.ptr, v.ptr)
+}
+
+// Erase removes the entry with key k from the map.
+func (m *ASTMap) Erase(k *Expr) {
+	C.Z3_ast_map_erase(m.ctx.ptr, m.ptr, k.ptr)
+}
+
+// Reset removes all entries from the map.
+func (m *ASTMap) Reset() {
+	C.Z3_ast_map_reset(m.ctx.ptr, m.ptr)
+}
+
+// Size returns the number of entries in the map.
+func (m *ASTMap) Size() uint {
+	return uint(C.Z3_ast_map_size(m.ctx.ptr, m.ptr))
+}
+
+// Keys returns all keys in the map as an ASTVector.
+func (m *ASTMap) Keys() *ASTVector {
+	return newASTVector(m.ctx, C.Z3_ast_map_keys(m.ctx.ptr, m.ptr))
+}
+
+// String returns the string representation of the map.
+func (m *ASTMap) String() string {
+	return C.GoString(C.Z3_ast_map_to_string(m.ctx.ptr, m.ptr))
+}
+
+// ModelExtrapolate extrapolates a model of a formula.
+// Given a model m and formula fml, returns an expression that is implied by fml
+// and is consistent with the model. This is a Spacer-specific function.
+func (c *Context) ModelExtrapolate(m *Model, fml *Expr) *Expr {
+	return newExpr(c, C.Z3_model_extrapolate(c.ptr, m.ptr, fml.ptr))
+}
+
+// QeLite performs best-effort quantifier elimination.
+// vars is a vector of variables to eliminate, body is the formula.
+func (c *Context) QeLite(vars *ASTVector, body *Expr) *Expr {
+	return newExpr(c, C.Z3_qe_lite(c.ptr, vars.ptr, body.ptr))
+}
+
+// QeModelProject projects variables given a model.
+// bound is a slice of application expressions representing the variables to project.
+func (c *Context) QeModelProject(m *Model, bound []*Expr, body *Expr) *Expr {
+	n := len(bound)
+	cBound := make([]C.Z3_app, n)
+	for i, b := range bound {
+		cBound[i] = C.Z3_to_app(c.ptr, b.ptr)
+	}
+	var boundPtr *C.Z3_app
+	if n > 0 {
+		boundPtr = &cBound[0]
+	}
+	return newExpr(c, C.Z3_qe_model_project(c.ptr, m.ptr, C.uint(n), boundPtr, body.ptr))
+}
+
+// QeModelProjectSkolem projects variables given a model, storing the skolem witnesses in map_.
+// bound is a slice of application expressions representing the variables to project.
+func (c *Context) QeModelProjectSkolem(m *Model, bound []*Expr, body *Expr, map_ *ASTMap) *Expr {
+	n := len(bound)
+	cBound := make([]C.Z3_app, n)
+	for i, b := range bound {
+		cBound[i] = C.Z3_to_app(c.ptr, b.ptr)
+	}
+	var boundPtr *C.Z3_app
+	if n > 0 {
+		boundPtr = &cBound[0]
+	}
+	return newExpr(c, C.Z3_qe_model_project_skolem(c.ptr, m.ptr, C.uint(n), boundPtr, body.ptr, map_.ptr))
+}
+
+// QeModelProjectWithWitness projects variables given a model and extracts witnesses.
+// The map_ is populated with bindings of projected variables to witness terms.
+// bound is a slice of application expressions representing the variables to project.
+func (c *Context) QeModelProjectWithWitness(m *Model, bound []*Expr, body *Expr, map_ *ASTMap) *Expr {
+	n := len(bound)
+	cBound := make([]C.Z3_app, n)
+	for i, b := range bound {
+		cBound[i] = C.Z3_to_app(c.ptr, b.ptr)
+	}
+	var boundPtr *C.Z3_app
+	if n > 0 {
+		boundPtr = &cBound[0]
+	}
+	return newExpr(c, C.Z3_qe_model_project_with_witness(c.ptr, m.ptr, C.uint(n), boundPtr, body.ptr, map_.ptr))
+}
--- a/src/api/go/tactic.go
+++ b/src/api/go/tactic.go
@ -228,6 +228,17 @@ func (g *Goal) String() string {
 	return C.GoString(C.Z3_goal_to_string(g.ctx.ptr, g.ptr))
 }

+// IsInconsistent returns true if the goal contains the formula false.
+func (g *Goal) IsInconsistent() bool {
+	return bool(C.Z3_goal_inconsistent(g.ctx.ptr, g.ptr))
+}
+
+// ToDimacsString converts the goal to a string in DIMACS format.
+// If includeNames is true, formula names are included as comments.
+func (g *Goal) ToDimacsString(includeNames bool) string {
+	return C.GoString(C.Z3_goal_to_dimacs_string(g.ctx.ptr, g.ptr, C.bool(includeNames)))
+}
+
 // ApplyResult represents the result of applying a tactic to a goal.
 type ApplyResult struct {
 	ctx *Context
--- a/src/api/go/z3.go
+++ b/src/api/go/z3.go
@ -291,6 +291,21 @@ func newASTVector(ctx *Context, ptr C.Z3_ast_vector) *ASTVector {
 	return v
 }

+// Size returns the number of ASTs in the vector.
+func (v *ASTVector) Size() uint {
+	return uint(C.Z3_ast_vector_size(v.ctx.ptr, v.ptr))
+}
+
+// Get returns the i-th AST in the vector.
+func (v *ASTVector) Get(i uint) *Expr {
+	return newExpr(v.ctx, C.Z3_ast_vector_get(v.ctx.ptr, v.ptr, C.uint(i)))
+}
+
+// String returns the string representation of the AST vector.
+func (v *ASTVector) String() string {
+	return C.GoString(C.Z3_ast_vector_to_string(v.ctx.ptr, v.ptr))
+}
+
 // ParamDescrs represents parameter descriptions for Z3 objects.
 type ParamDescrs struct {
 	ctx *Context
@ -640,6 +655,74 @@ func (e *Expr) Simplify() *Expr {
 	return newExpr(e.ctx, C.Z3_simplify(e.ctx.ptr, e.ptr))
 }

+// GetDecl returns the function declaration of an application expression.
+func (e *Expr) GetDecl() *FuncDecl {
+	return newFuncDecl(e.ctx, C.Z3_get_app_decl(e.ctx.ptr, C.Z3_to_app(e.ctx.ptr, e.ptr)))
+}
+
+// NumArgs returns the number of arguments of an application expression.
+func (e *Expr) NumArgs() uint {
+	return uint(C.Z3_get_app_num_args(e.ctx.ptr, C.Z3_to_app(e.ctx.ptr, e.ptr)))
+}
+
+// Arg returns the i-th argument of an application expression.
+func (e *Expr) Arg(i uint) *Expr {
+	return newExpr(e.ctx, C.Z3_get_app_arg(e.ctx.ptr, C.Z3_to_app(e.ctx.ptr, e.ptr), C.uint(i)))
+}
+
+// Substitute replaces every occurrence of from[i] in the expression with to[i].
+// The from and to slices must have the same length.
+func (e *Expr) Substitute(from, to []*Expr) *Expr {
+	n := len(from)
+	cFrom := make([]C.Z3_ast, n)
+	cTo := make([]C.Z3_ast, n)
+	for i := range from {
+		cFrom[i] = from[i].ptr
+		cTo[i] = to[i].ptr
+	}
+	var fromPtr, toPtr *C.Z3_ast
+	if n > 0 {
+		fromPtr = &cFrom[0]
+		toPtr = &cTo[0]
+	}
+	return newExpr(e.ctx, C.Z3_substitute(e.ctx.ptr, e.ptr, C.uint(n), fromPtr, toPtr))
+}
+
+// SubstituteVars replaces free variables in the expression with the expressions in to.
+// Variable with de-Bruijn index i is replaced with to[i].
+func (e *Expr) SubstituteVars(to []*Expr) *Expr {
+	n := len(to)
+	cTo := make([]C.Z3_ast, n)
+	for i, t := range to {
+		cTo[i] = t.ptr
+	}
+	var toPtr *C.Z3_ast
+	if n > 0 {
+		toPtr = &cTo[0]
+	}
+	return newExpr(e.ctx, C.Z3_substitute_vars(e.ctx.ptr, e.ptr, C.uint(n), toPtr))
+}
+
+// SubstituteFuns replaces every occurrence of from[i] applied to arguments
+// with to[i] in the expression.
+// The from and to slices must have the same length.
+func (e *Expr) SubstituteFuns(from []*FuncDecl, to []*Expr) *Expr {
+	n := len(from)
+	cFrom := make([]C.Z3_func_decl, n)
+	cTo := make([]C.Z3_ast, n)
+	for i := range from {
+		cFrom[i] = from[i].ptr
+		cTo[i] = to[i].ptr
+	}
+	var fromPtr *C.Z3_func_decl
+	var toPtr *C.Z3_ast
+	if n > 0 {
+		fromPtr = &cFrom[0]
+		toPtr = &cTo[0]
+	}
+	return newExpr(e.ctx, C.Z3_substitute_funs(e.ctx.ptr, e.ptr, C.uint(n), fromPtr, toPtr))
+}
+
 // MkTypeVariable creates a type variable sort for use in polymorphic functions and datatypes
 func (c *Context) MkTypeVariable(name *Symbol) *Sort {
 	return newSort(c, C.Z3_mk_type_variable(c.ptr, name.ptr))
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@ -475,6 +475,7 @@ sig
  val substitute : expr -> expr list -> expr list -> expr
  val substitute_one : expr -> expr -> expr -> expr
  val substitute_vars : expr -> expr list -> expr
+  val substitute_funs : expr -> FuncDecl.func_decl list -> expr list -> expr
  val translate : expr -> context -> expr
  val to_string : expr -> string
  val is_numeral : expr -> bool
@ -537,6 +538,13 @@ end = struct
  let substitute_vars x to_ =
    Z3native.substitute_vars (gc x) x (List.length to_) to_

+  let substitute_funs x from to_ =
+    let len = List.length from in
+    if List.length to_ <> len then
+      raise (Error "Argument sizes do not match")
+    else
+      Z3native.substitute_funs (gc x) x len from to_
+
  let translate (x:expr) to_ctx =
    if gc x = to_ctx then
      x
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@ -531,6 +531,10 @@ sig
      For every [i] smaller than [num_exprs], the variable with de-Bruijn index [i] is replaced with term [to[i]]. *)
  val substitute_vars : Expr.expr -> Expr.expr list -> expr

+  (** Substitute every application of [from[i]] with [to[i]] in the expression.
+      The [from] and [to] lists must have the same length. *)
+  val substitute_funs : Expr.expr -> FuncDecl.func_decl list -> Expr.expr list -> expr
+
  (** Translates (copies) the term to another context.
      @return A copy of the term which is associated with the other context *)
  val translate : Expr.expr -> context -> expr