Z3 Go API Documentation

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

# 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

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

• Z3 GitHub Repository
• All API Documentation
• Go API README