Z3 Go API Documentation - Z3

Overview

The Z3 Go bindings provide idiomatic Go access to the Z3 SMT solver. These bindings use CGO to wrap the Z3 C API and provide automatic memory management through Go finalizers.

Package: github.com/Z3Prover/z3/src/api/go

Quick Start

package main

import (
    "fmt"
    "github.com/Z3Prover/z3/src/api/go"
)

func main() {
    // Create a context
    ctx := z3.NewContext()

    // Create integer variable
    x := ctx.MkIntConst("x")

    // Create solver
    solver := ctx.NewSolver()

    // Add constraint: x > 0
    zero := ctx.MkInt(0, ctx.MkIntSort())
    solver.Assert(ctx.MkGt(x, zero))

    // Check satisfiability
    if solver.Check() == z3.Satisfiable {
        fmt.Println("sat")
        model := solver.Model()
        if val, ok := model.Eval(x, true); ok {
            fmt.Println("x =", val.String())
        }
    }
}

Installation

Prerequisites:

Go 1.20 or later
Z3 built as a shared library
CGO enabled (default)

Build Z3 with Go bindings:

# Using CMake
mkdir build && cd build
cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ..
make

# Using Python build script
python scripts/mk_make.py --go
cd build && make

Set environment variables:

export CGO_CFLAGS="-I${Z3_ROOT}/src/api"
export CGO_LDFLAGS="-L${Z3_ROOT}/build -lz3"
export LD_LIBRARY_PATH="${Z3_ROOT}/build:$LD_LIBRARY_PATH"

API Modules

z3.go

Package z3 provides Go bindings for the Z3 theorem prover. It wraps the Z3 C API using CGO.

solver.go

Solver and Model API for SMT solving

tactic.go

Tactics, Goals, Probes, and Parameters for goal-based solving

bitvec.go

Bit-vector operations and constraints

fp.go

IEEE 754 floating-point operations

seq.go

Sequences, strings, and regular expressions

datatype.go

Algebraic datatypes, tuples, and enumerations

optimize.go

Optimization with maximize/minimize objectives

Features

Core SMT: Boolean logic, arithmetic, arrays, quantifiers
Bit-vectors: Fixed-size bit-vector arithmetic and operations
Floating-point: IEEE 754 floating-point arithmetic
Strings & Sequences: String constraints and sequence operations
Regular Expressions: Pattern matching and regex constraints
Datatypes: Algebraic datatypes, tuples, enumerations
Tactics: Goal-based solving with tactic combinators
Optimization: MaxSMT with maximize/minimize objectives
Memory Management: Automatic via Go finalizers

Resources

← Back to main API documentation