Go bindings for the Z3 Theorem Prover
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
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())
}
}
}
Prerequisites:
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"
Core types (Context, Config, Symbol, Sort, Expr, FuncDecl, Quantifier, Lambda) and basic operations
Types: AST, ASTVector, Config, Context, Expr, FuncDecl, Lambda, ParamDescrs, Pattern, Quantifier, Sort, Symbol
Key Functions: AsExpr(), AsExpr(), Equal(), Equal(), Equal(), GetArity(), GetBody(), GetBody(), GetBoundName(), GetBoundName(), GetBoundSort(), GetBoundSort(), GetDomain(), GetName(), GetNoPattern() (+51 more)
Solver and Model API for SMT solving
Types: FuncInterp, Model, Solver
Key Functions: Assert(), AssertAndTrack(), Assertions(), Check(), CheckAssumptions(), CongruenceExplain(), CongruenceNext(), CongruenceRoot(), Eval(), FromFile(), FromString(), GetArity(), GetConstDecl(), GetConstInterp(), GetElse() (+28 more)
Tactics, Goals, Probes, and Parameters for goal-based solving
Types: ApplyResult, Goal, Params, Probe, Tactic
Key Functions: And(), AndThen(), Apply(), Apply(), Assert(), Eq(), Formula(), Ge(), GetHelp(), Gt(), IsDecidedSat(), IsDecidedUnsat(), Le(), Lt(), MkGoal() (+24 more)
Arithmetic operations (integers, reals) and comparisons
Key Functions: MkAdd(), MkDiv(), MkGe(), MkGt(), MkInt(), MkInt64(), MkIntConst(), MkIntSort(), MkLe(), MkLt(), MkMod(), MkMul(), MkReal(), MkRealConst(), MkRealSort() (+2 more)
Array operations (select, store, constant arrays)
Key Functions: MkArraySort(), MkConstArray(), MkSelect(), MkStore()
Bit-vector operations and constraints
Key Functions: MkBV(), MkBVAShr(), MkBVAdd(), MkBVAnd(), MkBVConst(), MkBVFromInt64(), MkBVLShr(), MkBVMul(), MkBVNeg(), MkBVNot(), MkBVOr(), MkBVSDiv(), MkBVSGE(), MkBVSGT(), MkBVSLE() (+15 more)
IEEE 754 floating-point operations
Key Functions: MkFPAbs(), MkFPAdd(), MkFPDiv(), MkFPEq(), MkFPGE(), MkFPGT(), MkFPInf(), MkFPIsInf(), MkFPIsNaN(), MkFPIsZero(), MkFPLE(), MkFPLT(), MkFPMul(), MkFPNaN(), MkFPNeg() (+10 more)
Sequences, strings, and regular expressions
Key Functions: MkEmptySeq(), MkInRe(), MkIntToStr(), MkReAllchar(), MkReComplement(), MkReConcat(), MkReDiff(), MkReEmpty(), MkReFull(), MkReIntersect(), MkReLoop(), MkReOption(), MkRePlus(), MkRePower(), MkReRange() (+20 more)
Algebraic datatypes, tuples, and enumerations
Types: Constructor, ConstructorList
Key Functions: GetDatatypeSortConstructor(), GetDatatypeSortConstructorAccessor(), GetDatatypeSortNumConstructors(), GetDatatypeSortRecognizer(), MkConstructor(), MkConstructorList(), MkDatatypeSort(), MkDatatypeSorts(), MkEnumSort(), MkListSort(), MkTupleSort()
Optimization with maximize/minimize objectives
Types: Optimize
Key Functions: Assert(), AssertAndTrack(), AssertSoft(), Assertions(), Check(), FromFile(), FromString(), GetHelp(), GetLower(), GetLowerAsVector(), GetUpper(), GetUpperAsVector(), Maximize(), Minimize(), Model() (+8 more)
Fixedpoint solver for Datalog and constrained Horn clauses (CHC)
Types: Fixedpoint, Statistics
Key Functions: AddCover(), AddFact(), AddRule(), Assert(), FromFile(), FromString(), GetAnswer(), GetAssertions(), GetCoverDelta(), GetDoubleValue(), GetHelp(), GetKey(), GetNumLevels(), GetParamDescrs(), GetReasonUnknown() (+15 more)
Interaction logging for debugging and analysis
Key Functions: AppendLog(), CloseLog(), IsLogOpen(), OpenLog()