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: AddRecDef(), Arg(), AsExpr(), AsExpr(), Equal(), Equal(), Equal(), Get(), GetArity(), GetBody(), GetBody(), GetBoundName(), GetBoundName(), GetBoundSort(), GetBoundSort() (+70 more)
Solver and Model API for SMT solving
Types: FuncEntry, FuncInterp, Model, Solver
Key Functions: AddEntry(), AddSimplifier(), Assert(), AssertAndTrack(), Assertions(), Check(), CheckAssumptions(), CongruenceExplain(), CongruenceNext(), CongruenceRoot(), Cube(), Dimacs(), Eval(), FromFile(), FromString() (+44 more)
Tactics, Goals, Probes, and Parameters for goal-based solving
Types: ApplyResult, Goal, Params, Probe, Tactic
Key Functions: And(), AndThen(), Apply(), Apply(), ApplyEx(), Assert(), ConvertModel(), Depth(), Eq(), Formula(), Ge(), GetHelp(), GetParamDescrs(), GetProbeDescr(), GetTacticDescr() (+41 more)
Arithmetic operations (integers, reals) and comparisons
Key Functions: MkAbs(), MkAdd(), MkDiv(), MkDivides(), MkGe(), MkGt(), MkInt(), MkInt2Real(), MkInt64(), MkIntConst(), MkIntSort(), MkIsInt(), MkLe(), MkLt(), MkMod() (+8 more)
Array operations (select, store, constant arrays)
Key Functions: MkArrayDefault(), MkArrayExt(), MkArraySort(), MkAsArray(), MkConstArray(), MkMap(), MkSelect(), MkSelectN(), MkStore(), MkStoreN()
Bit-vector operations and constraints
Key Functions: MkBV(), MkBVAShr(), MkBVAdd(), MkBVAddNoOverflow(), MkBVAddNoUnderflow(), MkBVAnd(), MkBVConst(), MkBVExtRotateLeft(), MkBVExtRotateRight(), MkBVFromInt64(), MkBVLShr(), MkBVMul(), MkBVMulNoOverflow(), MkBVMulNoUnderflow(), MkBVNeg() (+30 more)
IEEE 754 floating-point operations
Key Functions: MkFPAbs(), MkFPAdd(), MkFPDiv(), MkFPEq(), MkFPFMA(), MkFPFP(), MkFPGE(), MkFPGT(), MkFPInf(), MkFPIsInf(), MkFPIsNaN(), MkFPIsNegative(), MkFPIsNormal(), MkFPIsPositive(), MkFPIsSubnormal() (+39 more)
Sequences, strings, and regular expressions
Key Functions: MkEmptySeq(), MkInRe(), MkIntToStr(), MkReAllchar(), MkReComplement(), MkReConcat(), MkReDiff(), MkReEmpty(), MkReFull(), MkReIntersect(), MkReLoop(), MkReOption(), MkRePlus(), MkRePower(), MkReRange() (+31 more)
Algebraic datatypes, tuples, and enumerations
Types: Constructor, ConstructorList
Key Functions: GetDatatypeSortConstructor(), GetDatatypeSortConstructorAccessor(), GetDatatypeSortNumConstructors(), GetDatatypeSortRecognizer(), MkConstructor(), MkConstructorList(), MkDatatypeSort(), MkDatatypeSorts(), MkEnumSort(), MkListSort(), MkPolymorphicDatatypeSort(), 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() (+9 more)
Fixedpoint solver for Datalog and constrained Horn clauses (CHC)
Types: Fixedpoint, Statistics
Key Functions: AddCover(), AddFact(), AddInvariant(), AddRule(), Assert(), FromFile(), FromString(), GetAnswer(), GetAssertions(), GetCoverDelta(), GetDoubleValue(), GetGroundSatAnswer(), GetHelp(), GetKey(), GetNumLevels() (+21 more)
Interaction logging for debugging and analysis
Key Functions: AppendLog(), CloseLog(), IsLogOpen(), OpenLog()