mirrors/z3

Fork 0

mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 22:24:20 +00:00

Nikolaj Bjorner 66d0fb5477 git bindings v1.0

2026-02-15 21:24:40 -08:00

2.6 KiB

Raw Blame History

Z3 Go Examples

This directory contains examples demonstrating how to use the Z3 Go bindings.

Examples

basic_example.go

Demonstrates fundamental Z3 operations:

Creating contexts and solvers
Defining integer and boolean variables
Adding constraints
Checking satisfiability
Extracting models

Building and Running

Prerequisites

Build Z3 with Go bindings enabled
Ensure Z3 library is in your library path
Go 1.20 or later

Linux/macOS

# Build Z3 first
cd ../..
mkdir build && cd build
cmake ..
make -j$(nproc)

# Set up environment
cd ../examples/go
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Run examples
go run basic_example.go

Windows

REM Build Z3 first
cd ..\..
mkdir build
cd build
cmake ..
cmake --build . --config Release

REM Set up environment
cd ..\examples\go
set PATH=..\..\build\Release;%PATH%
set CGO_CFLAGS=-I..\..\src\api
set CGO_LDFLAGS=-L..\..\build\Release -lz3

REM Run examples
go run basic_example.go

Expected Output

When you run basic_example.go, you should see output similar to:

Z3 Go Bindings - Basic Example
================================

Example 1: Solving x > 0
Satisfiable!
Model: ...
x = 1

Example 2: Solving x + y = 10 ∧ x - y = 2
Satisfiable!
x = 6
y = 4

Example 3: Boolean satisfiability
Satisfiable!
p = false
q = true

Example 4: Checking unsatisfiability
Status: unsat
The constraints are unsatisfiable (as expected)

All examples completed successfully!

Creating Your Own Examples

Import the Z3 package:

import "github.com/Z3Prover/z3/src/api/go"

Create a context:
```
ctx := z3.NewContext()
```

Create variables and constraints:

x := ctx.MkIntConst("x")
constraint := ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort()))

Solve:

solver := ctx.NewSolver()
solver.Assert(constraint)
if solver.Check() == z3.Satisfiable {
    model := solver.Model()
    // Use model...
}

Troubleshooting

"undefined reference to Z3_*" errors

Make sure:

Z3 is built and the library is in your library path
CGO_LDFLAGS includes the correct library path
On Windows, the DLL is in your PATH

"cannot find package" errors