z3.go

Go to the documentation of this file.

// Package z3 provides Go bindings for the Z3 theorem prover.
//
// Z3 is a high-performance SMT (Satisfiability Modulo Theories) solver
// developed at Microsoft Research. These bindings wrap the Z3 C API using
// CGO and provide idiomatic Go interfaces with automatic memory management.
//
// # Basic Usage
//
// Create a context and solver:
//
//      ctx := z3.NewContext()
//      solver := ctx.NewSolver()
//
// Create variables and constraints:
//
//      x := ctx.MkIntConst("x")
//      y := ctx.MkIntConst("y")
//      solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ctx.MkInt(10, ctx.MkIntSort())))
//      solver.Assert(ctx.MkGt(x, y))
//
// Check satisfiability and get model:
//
//      if solver.Check() == z3.Satisfiable {
//          model := solver.Model()
//          xVal, _ := model.Eval(x, true)
//          fmt.Println("x =", xVal.String())
//      }
//
// # Memory Management
//
// All Z3 objects are automatically managed using Go finalizers. Reference
// counting is handled transparently - you don't need to manually free objects.
//
// # Supported Features
//
//   - Boolean logic, integer and real arithmetic
//   - Bit-vectors and floating-point arithmetic
//   - Arrays, sequences, and strings
//   - Regular expressions
//   - Algebraic datatypes
//   - Quantifiers and lambda expressions
//   - Tactics and goal-based solving
//   - Optimization (MaxSMT)
//   - Fixedpoint solver (Datalog/CHC)
//
// For more examples, see the examples/go directory in the Z3 repository.
package z3
 
/*
#cgo CFLAGS: -I${SRCDIR}/..
#cgo LDFLAGS: -lz3
#include "z3.h"
#include <stdlib.h>
*/
import "C"
import (
        "runtime"
        "unsafe"
)
 
// Config represents a Z3 configuration object.
type Config struct {
        ptr C.Z3_config
}
 
// NewConfig creates a new Z3 configuration.
func NewConfig() *Config {
        cfg := &Config{ptr: C.Z3_mk_config()}
        runtime.SetFinalizer(cfg, func(c *Config) {
                C.Z3_del_config(c.ptr)
        })
        return cfg
}
 
// SetParamValue sets a configuration parameter.
func (c *Config) SetParamValue(paramID, paramValue string) {
        cParamID := C.CString(paramID)
        cParamValue := C.CString(paramValue)
        defer C.free(unsafe.Pointer(cParamID))
        defer C.free(unsafe.Pointer(cParamValue))
        C.Z3_set_param_value(c.ptr, cParamID, cParamValue)
}
 
// Context represents a Z3 logical context.
type Context struct {
        ptr C.Z3_context
}
 
// NewContext creates a new Z3 context with default configuration.
func NewContext() *Context {
        ctx := &Context{ptr: C.Z3_mk_context_rc(C.Z3_mk_config())}
        C.Z3_enable_concurrent_dec_ref(ctx.ptr)
        runtime.SetFinalizer(ctx, func(c *Context) {
                C.Z3_del_context(c.ptr)
        })
        return ctx
}
 
// NewContextWithConfig creates a new Z3 context with the given configuration.
func NewContextWithConfig(cfg *Config) *Context {
        ctx := &Context{ptr: C.Z3_mk_context_rc(cfg.ptr)}
        C.Z3_enable_concurrent_dec_ref(ctx.ptr)
        runtime.SetFinalizer(ctx, func(c *Context) {
                C.Z3_del_context(c.ptr)
        })
        return ctx
}
 
// SetParam sets a global or context parameter.
func (c *Context) SetParam(key, value string) {
        cKey := C.CString(key)
        cValue := C.CString(value)
        defer C.free(unsafe.Pointer(cKey))
        defer C.free(unsafe.Pointer(cValue))
        C.Z3_update_param_value(c.ptr, cKey, cValue)
}
 
// Symbol represents a Z3 symbol.
type Symbol struct {
        ctx *Context
        ptr C.Z3_symbol
}
 
// newSymbol creates a new Symbol.
func newSymbol(ctx *Context, ptr C.Z3_symbol) *Symbol {
        return &Symbol{ctx: ctx, ptr: ptr}
}
 
// MkIntSymbol creates an integer symbol.
func (c *Context) MkIntSymbol(i int) *Symbol {
        return &Symbol{
                ctx: c,
                ptr: C.Z3_mk_int_symbol(c.ptr, C.int(i)),
        }
}
 
// MkStringSymbol creates a string symbol.
func (c *Context) MkStringSymbol(s string) *Symbol {
        cStr := C.CString(s)
        defer C.free(unsafe.Pointer(cStr))
        return &Symbol{
                ctx: c,
                ptr: C.Z3_mk_string_symbol(c.ptr, cStr),
        }
}
 
// String returns the string representation of the symbol.
func (s *Symbol) String() string {
        kind := C.Z3_get_symbol_kind(s.ctx.ptr, s.ptr)
        if kind == C.Z3_INT_SYMBOL {
                return string(rune(C.Z3_get_symbol_int(s.ctx.ptr, s.ptr)))
        }
        return C.GoString(C.Z3_get_symbol_string(s.ctx.ptr, s.ptr))
}
 
// AST represents a Z3 abstract syntax tree node.
type AST struct {
        ctx *Context
        ptr C.Z3_ast
}
 
// incRef increments the reference count of the AST.
func (a *AST) incRef() {
        C.Z3_inc_ref(a.ctx.ptr, a.ptr)
}
 
// decRef decrements the reference count of the AST.
func (a *AST) decRef() {
        C.Z3_dec_ref(a.ctx.ptr, a.ptr)
}
 
// String returns the string representation of the AST.
func (a *AST) String() string {
        return C.GoString(C.Z3_ast_to_string(a.ctx.ptr, a.ptr))
}
 
// Hash returns the hash code of the AST.
func (a *AST) Hash() uint32 {
        return uint32(C.Z3_get_ast_hash(a.ctx.ptr, a.ptr))
}
 
// Equal checks if two ASTs are equal.
func (a *AST) Equal(other *AST) bool {
        if a.ctx != other.ctx {
                return false
        }
        return bool(C.Z3_is_eq_ast(a.ctx.ptr, a.ptr, other.ptr))
}
 
// Sort represents a Z3 sort (type).
type Sort struct {
        ctx *Context
        ptr C.Z3_sort
}
 
// newSort creates a new Sort and manages its reference count.
func newSort(ctx *Context, ptr C.Z3_sort) *Sort {
        sort := &Sort{ctx: ctx, ptr: ptr}
        C.Z3_inc_ref(ctx.ptr, C.Z3_sort_to_ast(ctx.ptr, ptr))
        runtime.SetFinalizer(sort, func(s *Sort) {
                C.Z3_dec_ref(s.ctx.ptr, C.Z3_sort_to_ast(s.ctx.ptr, s.ptr))
        })
        return sort
}
 
// String returns the string representation of the sort.
func (s *Sort) String() string {
        return C.GoString(C.Z3_sort_to_string(s.ctx.ptr, s.ptr))
}
 
// Equal checks if two sorts are equal.
func (s *Sort) Equal(other *Sort) bool {
        if s.ctx != other.ctx {
                return false
        }
        return bool(C.Z3_is_eq_sort(s.ctx.ptr, s.ptr, other.ptr))
}
 
// MkBoolSort creates the Boolean sort.
func (c *Context) MkBoolSort() *Sort {
        return newSort(c, C.Z3_mk_bool_sort(c.ptr))
}
 
// MkBvSort creates a bit-vector sort of the given size.
func (c *Context) MkBvSort(sz uint) *Sort {
        return newSort(c, C.Z3_mk_bv_sort(c.ptr, C.uint(sz)))
}
 
// Expr represents a Z3 expression.
type Expr struct {
        ctx *Context
        ptr C.Z3_ast
}
 
// newExpr creates a new Expr and manages its reference count.
func newExpr(ctx *Context, ptr C.Z3_ast) *Expr {
        expr := &Expr{ctx: ctx, ptr: ptr}
        C.Z3_inc_ref(ctx.ptr, ptr)
        runtime.SetFinalizer(expr, func(e *Expr) {
                C.Z3_dec_ref(e.ctx.ptr, e.ptr)
        })
        return expr
}
 
// intsToCs converts a []int slice to []C.int, returning the slice and
// a pointer to its first element (nil if empty).
func intsToCs(ints []int) ([]C.int, *C.int) {
        if len(ints) == 0 {
                return nil, nil
        }
        cInts := make([]C.int, len(ints))
        for i, v := range ints {
                cInts[i] = C.int(v)
        }
        return cInts, &cInts[0]
}
 
// exprsToASTs converts a []*Expr slice to []C.Z3_ast, returning the slice and
// a pointer to its first element (nil if empty).
func exprsToASTs(exprs []*Expr) ([]C.Z3_ast, *C.Z3_ast) {
        if len(exprs) == 0 {
                return nil, nil
        }
        cExprs := make([]C.Z3_ast, len(exprs))
        for i, e := range exprs {
                cExprs[i] = e.ptr
        }
        return cExprs, &cExprs[0]
}
 
// sortsToCSorts converts a []*Sort slice to []C.Z3_sort, returning the slice and
// a pointer to its first element (nil if empty).
func sortsToCSorts(sorts []*Sort) ([]C.Z3_sort, *C.Z3_sort) {
        if len(sorts) == 0 {
                return nil, nil
        }
        cSorts := make([]C.Z3_sort, len(sorts))
        for i, s := range sorts {
                cSorts[i] = s.ptr
        }
        return cSorts, &cSorts[0]
}
 
// String returns the string representation of the expression.
func (e *Expr) String() string {
        return C.GoString(C.Z3_ast_to_string(e.ctx.ptr, e.ptr))
}
 
// Equal checks if two expressions are equal.
func (e *Expr) Equal(other *Expr) bool {
        if e.ctx != other.ctx {
                return false
        }
        return bool(C.Z3_is_eq_ast(e.ctx.ptr, e.ptr, other.ptr))
}
 
// GetSort returns the sort of the expression.
func (e *Expr) GetSort() *Sort {
        return newSort(e.ctx, C.Z3_get_sort(e.ctx.ptr, e.ptr))
}
 
// Pattern represents a Z3 pattern for quantifier instantiation.
type Pattern struct {
        ctx *Context
        ptr C.Z3_pattern
}
 
// newPattern creates a new Pattern and manages its reference count.
func newPattern(ctx *Context, ptr C.Z3_pattern) *Pattern {
        p := &Pattern{ctx: ctx, ptr: ptr}
        // Patterns are ASTs in the C API
        C.Z3_inc_ref(ctx.ptr, (C.Z3_ast)(unsafe.Pointer(ptr)))
        runtime.SetFinalizer(p, func(pat *Pattern) {
                C.Z3_dec_ref(pat.ctx.ptr, (C.Z3_ast)(unsafe.Pointer(pat.ptr)))
        })
        return p
}
 
// ASTVector represents a vector of Z3 ASTs.
type ASTVector struct {
        ctx *Context
        ptr C.Z3_ast_vector
}
 
// newASTVector creates a new ASTVector and manages its reference count.
func newASTVector(ctx *Context, ptr C.Z3_ast_vector) *ASTVector {
        v := &ASTVector{ctx: ctx, ptr: ptr}
        C.Z3_ast_vector_inc_ref(ctx.ptr, ptr)
        runtime.SetFinalizer(v, func(vec *ASTVector) {
                C.Z3_ast_vector_dec_ref(vec.ctx.ptr, vec.ptr)
        })
        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
        ptr C.Z3_param_descrs
}
 
// newParamDescrs creates a new ParamDescrs and manages its reference count.
func newParamDescrs(ctx *Context, ptr C.Z3_param_descrs) *ParamDescrs {
        pd := &ParamDescrs{ctx: ctx, ptr: ptr}
        C.Z3_param_descrs_inc_ref(ctx.ptr, ptr)
        runtime.SetFinalizer(pd, func(descrs *ParamDescrs) {
                C.Z3_param_descrs_dec_ref(descrs.ctx.ptr, descrs.ptr)
        })
        return pd
}
 
// MkTrue creates the Boolean constant true.
func (c *Context) MkTrue() *Expr {
        return newExpr(c, C.Z3_mk_true(c.ptr))
}
 
// MkFalse creates the Boolean constant false.
func (c *Context) MkFalse() *Expr {
        return newExpr(c, C.Z3_mk_false(c.ptr))
}
 
// MkBool creates a Boolean constant.
func (c *Context) MkBool(value bool) *Expr {
        if value {
                return c.MkTrue()
        }
        return c.MkFalse()
}
 
// MkNumeral creates a numeral from a string.
func (c *Context) MkNumeral(numeral string, sort *Sort) *Expr {
        cStr := C.CString(numeral)
        defer C.free(unsafe.Pointer(cStr))
        return newExpr(c, C.Z3_mk_numeral(c.ptr, cStr, sort.ptr))
}
 
// MkConst creates a constant (variable) with the given name and sort.
func (c *Context) MkConst(name *Symbol, sort *Sort) *Expr {
        return newExpr(c, C.Z3_mk_const(c.ptr, name.ptr, sort.ptr))
}
 
// MkBoolConst creates a Boolean constant (variable) with the given name.
func (c *Context) MkBoolConst(name string) *Expr {
        sym := c.MkStringSymbol(name)
        return c.MkConst(sym, c.MkBoolSort())
}
 
// Boolean operations
 
// MkAnd creates a conjunction.
func (c *Context) MkAnd(exprs ...*Expr) *Expr {
        if len(exprs) == 0 {
                return c.MkTrue()
        }
        if len(exprs) == 1 {
                return exprs[0]
        }
        _, cExprsPtr := exprsToASTs(exprs)
        return newExpr(c, C.Z3_mk_and(c.ptr, C.uint(len(exprs)), cExprsPtr))
}
 
// MkOr creates a disjunction.
func (c *Context) MkOr(exprs ...*Expr) *Expr {
        if len(exprs) == 0 {
                return c.MkFalse()
        }
        if len(exprs) == 1 {
                return exprs[0]
        }
        _, cExprsPtr := exprsToASTs(exprs)
        return newExpr(c, C.Z3_mk_or(c.ptr, C.uint(len(exprs)), cExprsPtr))
}
 
// MkNot creates a negation.
func (c *Context) MkNot(expr *Expr) *Expr {
        return newExpr(c, C.Z3_mk_not(c.ptr, expr.ptr))
}
 
// MkImplies creates an implication.
func (c *Context) MkImplies(lhs, rhs *Expr) *Expr {
        return newExpr(c, C.Z3_mk_implies(c.ptr, lhs.ptr, rhs.ptr))
}
 
// MkIff creates a bi-implication (if and only if).
func (c *Context) MkIff(lhs, rhs *Expr) *Expr {
        return newExpr(c, C.Z3_mk_iff(c.ptr, lhs.ptr, rhs.ptr))
}
 
// MkXor creates exclusive or.
func (c *Context) MkXor(lhs, rhs *Expr) *Expr {
        return newExpr(c, C.Z3_mk_xor(c.ptr, lhs.ptr, rhs.ptr))
}
 
// Comparison operations
 
// MkEq creates an equality.
func (c *Context) MkEq(lhs, rhs *Expr) *Expr {
        return newExpr(c, C.Z3_mk_eq(c.ptr, lhs.ptr, rhs.ptr))
}
 
// MkDistinct creates a distinct constraint.
func (c *Context) MkDistinct(exprs ...*Expr) *Expr {
        if len(exprs) <= 1 {
                return c.MkTrue()
        }
        _, cExprsPtr := exprsToASTs(exprs)
        return newExpr(c, C.Z3_mk_distinct(c.ptr, C.uint(len(exprs)), cExprsPtr))
}
 
// Pseudo-Boolean / cardinality constraints
 
// MkAtMost encodes p1 + p2 + ... + pn <= k.
func (c *Context) MkAtMost(args []*Expr, k uint) *Expr {
        _, cArgsPtr := exprsToASTs(args)
        return newExpr(c, C.Z3_mk_atmost(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
}
 
// MkAtLeast encodes p1 + p2 + ... + pn >= k.
func (c *Context) MkAtLeast(args []*Expr, k uint) *Expr {
        _, cArgsPtr := exprsToASTs(args)
        return newExpr(c, C.Z3_mk_atleast(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
}
 
// MkPBLe encodes k1*p1 + k2*p2 + ... + kn*pn <= k.
func (c *Context) MkPBLe(args []*Expr, coeffs []int, k int) *Expr {
        if len(args) != len(coeffs) {
                panic("MkPBLe: args and coeffs must have the same length")
        }
        _, cArgsPtr := exprsToASTs(args)
        _, cCoeffsPtr := intsToCs(coeffs)
        return newExpr(c, C.Z3_mk_pble(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
 
// MkPBGe encodes k1*p1 + k2*p2 + ... + kn*pn >= k.
func (c *Context) MkPBGe(args []*Expr, coeffs []int, k int) *Expr {
        if len(args) != len(coeffs) {
                panic("MkPBGe: args and coeffs must have the same length")
        }
        _, cArgsPtr := exprsToASTs(args)
        _, cCoeffsPtr := intsToCs(coeffs)
        return newExpr(c, C.Z3_mk_pbge(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
 
// MkPBEq encodes k1*p1 + k2*p2 + ... + kn*pn = k.
func (c *Context) MkPBEq(args []*Expr, coeffs []int, k int) *Expr {
        if len(args) != len(coeffs) {
                panic("MkPBEq: args and coeffs must have the same length")
        }
        _, cArgsPtr := exprsToASTs(args)
        _, cCoeffsPtr := intsToCs(coeffs)
        return newExpr(c, C.Z3_mk_pbeq(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
}
 
// FuncDecl represents a function declaration.
type FuncDecl struct {
        ctx *Context
        ptr C.Z3_func_decl
}
 
// newFuncDecl creates a new FuncDecl and manages its reference count.
func newFuncDecl(ctx *Context, ptr C.Z3_func_decl) *FuncDecl {
        fd := &FuncDecl{ctx: ctx, ptr: ptr}
        C.Z3_inc_ref(ctx.ptr, C.Z3_func_decl_to_ast(ctx.ptr, ptr))
        runtime.SetFinalizer(fd, func(f *FuncDecl) {
                C.Z3_dec_ref(f.ctx.ptr, C.Z3_func_decl_to_ast(f.ctx.ptr, f.ptr))
        })
        return fd
}
 
// String returns the string representation of the function declaration.
func (f *FuncDecl) String() string {
        return C.GoString(C.Z3_func_decl_to_string(f.ctx.ptr, f.ptr))
}
 
// GetName returns the name of the function declaration.
func (f *FuncDecl) GetName() *Symbol {
        return &Symbol{
                ctx: f.ctx,
                ptr: C.Z3_get_decl_name(f.ctx.ptr, f.ptr),
        }
}
 
// GetArity returns the arity (number of parameters) of the function.
func (f *FuncDecl) GetArity() int {
        return int(C.Z3_get_arity(f.ctx.ptr, f.ptr))
}
 
// GetDomain returns the sort of the i-th parameter.
func (f *FuncDecl) GetDomain(i int) *Sort {
        return newSort(f.ctx, C.Z3_get_domain(f.ctx.ptr, f.ptr, C.uint(i)))
}
 
// GetRange returns the sort of the return value.
func (f *FuncDecl) GetRange() *Sort {
        return newSort(f.ctx, C.Z3_get_range(f.ctx.ptr, f.ptr))
}
 
// MkFuncDecl creates a function declaration.
func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl {
        _, domainPtr := sortsToCSorts(domain)
        return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
}
 
// MkRecFuncDecl creates a recursive function declaration.
// After creating, use AddRecDef to provide the function body.
func (c *Context) MkRecFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl {
        _, domainPtr := sortsToCSorts(domain)
        return newFuncDecl(c, C.Z3_mk_rec_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
}
 
// AddRecDef adds the definition (body) for a recursive function created with MkRecFuncDecl.
func (c *Context) AddRecDef(f *FuncDecl, args []*Expr, body *Expr) {
        _, argsPtr := exprsToASTs(args)
        C.Z3_add_rec_def(c.ptr, f.ptr, C.uint(len(args)), argsPtr, body.ptr)
}
 
// MkApp creates a function application.
func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr {
        _, argsPtr := exprsToASTs(args)
        return newExpr(c, C.Z3_mk_app(c.ptr, decl.ptr, C.uint(len(args)), argsPtr))
}
 
// Quantifier operations
 
// MkForall creates a universal quantifier.
func (c *Context) MkForall(bound []*Expr, body *Expr) *Expr {
        cBound := make([]C.Z3_app, len(bound))
        for i, b := range bound {
                // Z3_app is a subtype of Z3_ast; constants are apps
                cBound[i] = (C.Z3_app)(unsafe.Pointer(b.ptr))
        }
        var boundPtr *C.Z3_app
        if len(bound) > 0 {
                boundPtr = &cBound[0]
        }
        return newExpr(c, C.Z3_mk_forall_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr))
}
 
// MkExists creates an existential quantifier.
func (c *Context) MkExists(bound []*Expr, body *Expr) *Expr {
        cBound := make([]C.Z3_app, len(bound))
        for i, b := range bound {
                // Z3_app is a subtype of Z3_ast; constants are apps
                cBound[i] = (C.Z3_app)(unsafe.Pointer(b.ptr))
        }
        var boundPtr *C.Z3_app
        if len(bound) > 0 {
                boundPtr = &cBound[0]
        }
        return newExpr(c, C.Z3_mk_exists_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr))
}
 
// Simplify simplifies an expression.
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 {
        _, toPtr := exprsToASTs(to)
        return newExpr(e.ctx, C.Z3_substitute_vars(e.ctx.ptr, e.ptr, C.uint(len(to)), 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))
}
 
// Quantifier represents a quantified formula (forall or exists)
type Quantifier struct {
        ctx *Context
        ptr C.Z3_ast
}
 
// newQuantifier creates a new Quantifier with proper memory management
func newQuantifier(ctx *Context, ptr C.Z3_ast) *Quantifier {
        q := &Quantifier{ctx: ctx, ptr: ptr}
        C.Z3_inc_ref(ctx.ptr, ptr)
        runtime.SetFinalizer(q, func(qf *Quantifier) {
                C.Z3_dec_ref(qf.ctx.ptr, qf.ptr)
        })
        return q
}
 
// AsExpr converts a Quantifier to an Expr
func (q *Quantifier) AsExpr() *Expr {
        return newExpr(q.ctx, q.ptr)
}
 
// IsUniversal returns true if this is a universal quantifier (forall)
func (q *Quantifier) IsUniversal() bool {
        return bool(C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr))
}
 
// IsExistential returns true if this is an existential quantifier (exists)
func (q *Quantifier) IsExistential() bool {
        return bool(C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr))
}
 
// GetWeight returns the weight of the quantifier
func (q *Quantifier) GetWeight() int {
        return int(C.Z3_get_quantifier_weight(q.ctx.ptr, q.ptr))
}
 
// GetNumPatterns returns the number of patterns
func (q *Quantifier) GetNumPatterns() int {
        return int(C.Z3_get_quantifier_num_patterns(q.ctx.ptr, q.ptr))
}
 
// GetPattern returns the pattern at the given index
func (q *Quantifier) GetPattern(idx int) *Pattern {
        ptr := C.Z3_get_quantifier_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx))
        return newPattern(q.ctx, ptr)
}
 
// GetNumNoPatterns returns the number of no-patterns
func (q *Quantifier) GetNumNoPatterns() int {
        return int(C.Z3_get_quantifier_num_no_patterns(q.ctx.ptr, q.ptr))
}
 
// GetNoPattern returns the no-pattern at the given index
func (q *Quantifier) GetNoPattern(idx int) *Pattern {
        ptr := C.Z3_get_quantifier_no_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx))
        return newPattern(q.ctx, (C.Z3_pattern)(unsafe.Pointer(ptr)))
}
 
// GetNumBound returns the number of bound variables
func (q *Quantifier) GetNumBound() int {
        return int(C.Z3_get_quantifier_num_bound(q.ctx.ptr, q.ptr))
}
 
// GetBoundName returns the name of the bound variable at the given index
func (q *Quantifier) GetBoundName(idx int) *Symbol {
        ptr := C.Z3_get_quantifier_bound_name(q.ctx.ptr, q.ptr, C.uint(idx))
        return newSymbol(q.ctx, ptr)
}
 
// GetBoundSort returns the sort of the bound variable at the given index
func (q *Quantifier) GetBoundSort(idx int) *Sort {
        ptr := C.Z3_get_quantifier_bound_sort(q.ctx.ptr, q.ptr, C.uint(idx))
        return newSort(q.ctx, ptr)
}
 
// GetBody returns the body of the quantifier
func (q *Quantifier) GetBody() *Expr {
        ptr := C.Z3_get_quantifier_body(q.ctx.ptr, q.ptr)
        return newExpr(q.ctx, ptr)
}
 
// String returns the string representation of the quantifier
func (q *Quantifier) String() string {
        return q.AsExpr().String()
}
 
// MkQuantifier creates a quantifier with patterns
func (c *Context) MkQuantifier(isForall bool, weight int, sorts []*Sort, names []*Symbol, body *Expr, patterns []*Pattern) *Quantifier {
        forallInt := C.bool(isForall)
 
        numBound := len(sorts)
        if numBound != len(names) {
                panic("Number of sorts must match number of names")
        }
 
        var cSorts []C.Z3_sort
        var cNames []C.Z3_symbol
        if numBound > 0 {
                cSorts = make([]C.Z3_sort, numBound)
                cNames = make([]C.Z3_symbol, numBound)
                for i := 0; i < numBound; i++ {
                        cSorts[i] = sorts[i].ptr
                        cNames[i] = names[i].ptr
                }
        }
 
        var cPatterns []C.Z3_pattern
        var patternsPtr *C.Z3_pattern
        numPatterns := len(patterns)
        if numPatterns > 0 {
                cPatterns = make([]C.Z3_pattern, numPatterns)
                for i := 0; i < numPatterns; i++ {
                        cPatterns[i] = patterns[i].ptr
                }
                patternsPtr = &cPatterns[0]
        }
 
        var sortsPtr *C.Z3_sort
        var namesPtr *C.Z3_symbol
        if numBound > 0 {
                sortsPtr = &cSorts[0]
                namesPtr = &cNames[0]
        }
 
        ptr := C.Z3_mk_quantifier(c.ptr, forallInt, C.uint(weight), C.uint(numPatterns), patternsPtr,
                C.uint(numBound), sortsPtr, namesPtr, body.ptr)
        return newQuantifier(c, ptr)
}
 
// MkQuantifierConst creates a quantifier using constant bound variables
func (c *Context) MkQuantifierConst(isForall bool, weight int, bound []*Expr, body *Expr, patterns []*Pattern) *Quantifier {
        forallInt := C.bool(isForall)
 
        numBound := len(bound)
        var cBound []C.Z3_app
        var boundPtr *C.Z3_app
        if numBound > 0 {
                cBound = make([]C.Z3_app, numBound)
                for i := 0; i < numBound; i++ {
                        cBound[i] = (C.Z3_app)(unsafe.Pointer(bound[i].ptr))
                }
                boundPtr = &cBound[0]
        }
 
        var cPatterns []C.Z3_pattern
        var patternsPtr *C.Z3_pattern
        numPatterns := len(patterns)
        if numPatterns > 0 {
                cPatterns = make([]C.Z3_pattern, numPatterns)
                for i := 0; i < numPatterns; i++ {
                        cPatterns[i] = patterns[i].ptr
                }
                patternsPtr = &cPatterns[0]
        }
 
        ptr := C.Z3_mk_quantifier_const(c.ptr, forallInt, C.uint(weight), C.uint(numBound), boundPtr,
                C.uint(numPatterns), patternsPtr, body.ptr)
        return newQuantifier(c, ptr)
}
 
// Lambda represents a lambda expression
type Lambda struct {
        ctx *Context
        ptr C.Z3_ast
}
 
// newLambda creates a new Lambda with proper memory management
func newLambda(ctx *Context, ptr C.Z3_ast) *Lambda {
        l := &Lambda{ctx: ctx, ptr: ptr}
        C.Z3_inc_ref(ctx.ptr, ptr)
        runtime.SetFinalizer(l, func(lam *Lambda) {
                C.Z3_dec_ref(lam.ctx.ptr, lam.ptr)
        })
        return l
}
 
// AsExpr converts a Lambda to an Expr
func (l *Lambda) AsExpr() *Expr {
        return newExpr(l.ctx, l.ptr)
}
 
// GetNumBound returns the number of bound variables
func (l *Lambda) GetNumBound() int {
        return int(C.Z3_get_quantifier_num_bound(l.ctx.ptr, l.ptr))
}
 
// GetBoundName returns the name of the bound variable at the given index
func (l *Lambda) GetBoundName(idx int) *Symbol {
        ptr := C.Z3_get_quantifier_bound_name(l.ctx.ptr, l.ptr, C.uint(idx))
        return newSymbol(l.ctx, ptr)
}
 
// GetBoundSort returns the sort of the bound variable at the given index
func (l *Lambda) GetBoundSort(idx int) *Sort {
        ptr := C.Z3_get_quantifier_bound_sort(l.ctx.ptr, l.ptr, C.uint(idx))
        return newSort(l.ctx, ptr)
}
 
// GetBody returns the body of the lambda expression
func (l *Lambda) GetBody() *Expr {
        ptr := C.Z3_get_quantifier_body(l.ctx.ptr, l.ptr)
        return newExpr(l.ctx, ptr)
}
 
// String returns the string representation of the lambda
func (l *Lambda) String() string {
        return l.AsExpr().String()
}
 
// MkLambda creates a lambda expression with sorts and names
func (c *Context) MkLambda(sorts []*Sort, names []*Symbol, body *Expr) *Lambda {
        numBound := len(sorts)
        if numBound != len(names) {
                panic("Number of sorts must match number of names")
        }
 
        var cSorts []C.Z3_sort
        var cNames []C.Z3_symbol
        var sortsPtr *C.Z3_sort
        var namesPtr *C.Z3_symbol
 
        if numBound > 0 {
                cSorts = make([]C.Z3_sort, numBound)
                cNames = make([]C.Z3_symbol, numBound)
                for i := 0; i < numBound; i++ {
                        cSorts[i] = sorts[i].ptr
                        cNames[i] = names[i].ptr
                }
                sortsPtr = &cSorts[0]
                namesPtr = &cNames[0]
        }
 
        ptr := C.Z3_mk_lambda(c.ptr, C.uint(numBound), sortsPtr, namesPtr, body.ptr)
        return newLambda(c, ptr)
}
 
// MkLambdaConst creates a lambda expression using constant bound variables
func (c *Context) MkLambdaConst(bound []*Expr, body *Expr) *Lambda {
        numBound := len(bound)
        var cBound []C.Z3_app
        var boundPtr *C.Z3_app
 
        if numBound > 0 {
                cBound = make([]C.Z3_app, numBound)
                for i := 0; i < numBound; i++ {
                        cBound[i] = (C.Z3_app)(unsafe.Pointer(bound[i].ptr))
                }
                boundPtr = &cBound[0]
        }
 
        ptr := C.Z3_mk_lambda_const(c.ptr, C.uint(numBound), boundPtr, body.ptr)
        return newLambda(c, ptr)
}
 
// SetGlobalParam sets a global Z3 parameter.
func SetGlobalParam(id, value string) {
        cID := C.CString(id)
        cValue := C.CString(value)
        defer C.free(unsafe.Pointer(cID))
        defer C.free(unsafe.Pointer(cValue))
        C.Z3_global_param_set(cID, cValue)
}
 
// GetGlobalParam retrieves the value of a global Z3 parameter.
// Returns the value and true if the parameter exists, or empty string and false otherwise.
func GetGlobalParam(id string) (string, bool) {
        cID := C.CString(id)
        defer C.free(unsafe.Pointer(cID))
        var cValue C.Z3_string
        ok := C.Z3_global_param_get(cID, &cValue)
        if ok == C.bool(false) {
                return "", false
        }
        return C.GoString(cValue), true
}
 
// ResetAllGlobalParams resets all global Z3 parameters to their default values.
func ResetAllGlobalParams() {
        C.Z3_global_param_reset_all()
}
 
// astVectorToExprs converts a Z3_ast_vector to a slice of Expr.
// This function properly manages the reference count of the vector by
// incrementing it on entry and decrementing it on exit.
// The individual AST elements are already reference counted by newExpr.
func astVectorToExprs(ctx *Context, vec C.Z3_ast_vector) []*Expr {
        // Increment reference count for the vector since we're using it
        C.Z3_ast_vector_inc_ref(ctx.ptr, vec)
        defer C.Z3_ast_vector_dec_ref(ctx.ptr, vec)
 
        size := uint(C.Z3_ast_vector_size(ctx.ptr, vec))
        result := make([]*Expr, size)
        for i := uint(0); i < size; i++ {
                result[i] = newExpr(ctx, C.Z3_ast_vector_get(ctx.ptr, vec, C.uint(i)))
        }
        return result
}