Skip to content

README.md

Latest commit

 

History

History
331 lines (253 loc) · 10.7 KB

README.md

File metadata and controls

331 lines (253 loc) · 10.7 KB

Z3 Go Bindings

This directory contains Go language bindings for the Z3 theorem prover.

Overview

The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support:

  • Core Z3 Types: Context, Config, Symbol, AST, Sort, Expr, FuncDecl
  • Solver Operations: Creating solvers, asserting constraints, checking satisfiability
  • Model Manipulation: Extracting and evaluating models
  • Boolean Logic: And, Or, Not, Implies, Iff, Xor
  • Arithmetic: Add, Sub, Mul, Div, Mod, comparison operators
  • Bit-vectors: Full bit-vector arithmetic, bitwise operations, shifts, comparisons
  • Floating Point: IEEE 754 floating-point arithmetic with rounding modes
  • Arrays: Select, Store, constant arrays
  • Sequences/Strings: String operations, concatenation, contains, indexing
  • Regular Expressions: Pattern matching, Kleene star/plus, regex operations
  • Quantifiers: Forall, Exists
  • Functions: Function declarations and applications
  • Tactics & Goals: Goal-based solving and tactic combinators
  • Probes: Goal property checking
  • Datatypes: Algebraic datatypes, tuples, enumerations, lists
  • Parameters: Solver and tactic configuration
  • Optimize: Optimization problems with maximize/minimize objectives

Building

Prerequisites

  • Go 1.20 or later
  • Z3 library built and installed
  • CGO enabled

With CMake

mkdir build && cd build
cmake -DBUILD_GO_BINDINGS=ON ..
make

With Python Build System

python scripts/mk_make.py --go
cd build
make

Usage

Basic Example

package main

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

func main() {
    // Create a context
    ctx := z3.NewContext()
    
    // Create variables
    x := ctx.MkIntConst("x")
    y := ctx.MkIntConst("y")
    
    // Create constraints: x + y == 10 && x > y
    ten := ctx.MkInt(10, ctx.MkIntSort())
    eq := ctx.MkEq(ctx.MkAdd(x, y), ten)
    gt := ctx.MkGt(x, y)
    
    // Create solver and check
    solver := ctx.NewSolver()
    solver.Assert(eq)
    solver.Assert(gt)
    
    if solver.Check() == z3.Satisfiable {
        model := solver.Model()
        if xVal, ok := model.Eval(x, true); ok {
            fmt.Println("x =", xVal.String())
        }
        if yVal, ok := model.Eval(y, true); ok {
            fmt.Println("y =", yVal.String())
        }
    }
}

Running Examples

cd examples/go

# Set library path (Linux/Mac)
export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
export CGO_CFLAGS="-I../../src/api"
export CGO_LDFLAGS="-L../../build -lz3"

# Set library path (Windows)
set PATH=..\..\build;%PATH%
set CGO_CFLAGS=-I../../src/api
set CGO_LDFLAGS=-L../../build -lz3

# Run example
go run basic_example.go

API Reference

Context

  • NewContext() - Create a new Z3 context
  • NewContextWithConfig(cfg *Config) - Create context with configuration
  • SetParam(key, value string) - Set context parameters

Creating Expressions

  • MkBoolConst(name string) - Create Boolean variable
  • MkIntConst(name string) - Create integer variable
  • MkRealConst(name string) - Create real variable
  • MkInt(value int, sort *Sort) - Create integer constant
  • MkReal(num, den int) - Create rational constant

Boolean Operations

  • MkAnd(exprs ...*Expr) - Conjunction
  • MkOr(exprs ...*Expr) - Disjunction
  • MkNot(expr *Expr) - Negation
  • MkImplies(lhs, rhs *Expr) - Implication
  • MkIff(lhs, rhs *Expr) - If-and-only-if
  • MkXor(lhs, rhs *Expr) - Exclusive or

Arithmetic Operations

  • MkAdd(exprs ...*Expr) - Addition
  • MkSub(exprs ...*Expr) - Subtraction
  • MkMul(exprs ...*Expr) - Multiplication
  • MkDiv(lhs, rhs *Expr) - Division
  • MkMod(lhs, rhs *Expr) - Modulo
  • MkRem(lhs, rhs *Expr) - Remainder

Comparison Operations

  • MkEq(lhs, rhs *Expr) - Equality
  • MkDistinct(exprs ...*Expr) - Distinct
  • MkLt(lhs, rhs *Expr) - Less than
  • MkLe(lhs, rhs *Expr) - Less than or equal
  • MkGt(lhs, rhs *Expr) - Greater than
  • MkGe(lhs, rhs *Expr) - Greater than or equal

Solver Operations

  • NewSolver() - Create a new solver
  • Assert(constraint *Expr) - Add constraint
  • Check() - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown)
  • Model() - Get model (if satisfiable)
  • Push() - Create backtracking point
  • Pop(n uint) - Remove backtracking points
  • Reset() - Remove all assertions

Model Operations

  • Eval(expr *Expr, modelCompletion bool) - Evaluate expression in model
  • NumConsts() - Number of constants in model
  • NumFuncs() - Number of functions in model
  • String() - Get string representation

Bit-vector Operations

  • MkBvSort(sz uint) - Create bit-vector sort
  • MkBVConst(name string, size uint) - Create bit-vector variable
  • MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr) - Arithmetic operations
  • MkBVAnd/Or/Xor/Not(...) - Bitwise operations
  • MkBVShl/LShr/AShr(lhs, rhs *Expr) - Shift operations
  • MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...) - Comparisons
  • MkConcat(lhs, rhs *Expr) - Bit-vector concatenation
  • MkExtract(high, low uint, expr *Expr) - Extract bits
  • MkSignExt/ZeroExt(i uint, expr *Expr) - Extend bit-vectors

Floating-Point Operations

  • MkFPSort(ebits, sbits uint) - Create floating-point sort
  • MkFPSort16/32/64/128() - Standard IEEE 754 sorts
  • MkFPInf/NaN/Zero(sort *Sort, ...) - Special values
  • MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr) - Arithmetic with rounding
  • MkFPNeg/Abs/Sqrt(...) - Unary operations
  • MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr) - Comparisons
  • MkFPIsNaN/IsInf/IsZero(expr *Expr) - Predicates

Sequence/String Operations

  • MkStringSort() - Create string sort
  • MkSeqSort(elemSort *Sort) - Create sequence sort
  • MkString(value string) - Create string constant
  • MkSeqConcat(exprs ...*Expr) - Concatenation
  • MkSeqLength(seq *Expr) - Length
  • MkSeqPrefix/Suffix/Contains(...) - Predicates
  • MkSeqAt(seq, index *Expr) - Element access
  • MkSeqExtract(seq, offset, length *Expr) - Substring
  • MkStrToInt/IntToStr(...) - Conversions

Regular Expression Operations

  • MkReSort(seqSort *Sort) - Create regex sort
  • MkToRe(seq *Expr) - Convert string to regex
  • MkInRe(seq, re *Expr) - String matches regex predicate
  • MkReStar(re *Expr) - Kleene star (zero or more)
  • MkRePlus(re *Expr) - Kleene plus (one or more)
  • MkReOption(re *Expr) - Optional (zero or one)
  • MkRePower(re *Expr, n uint) - Exactly n repetitions
  • MkReLoop(re *Expr, lo, hi uint) - Bounded repetition
  • MkReConcat(regexes ...*Expr) - Concatenation
  • MkReUnion(regexes ...*Expr) - Alternation (OR)
  • MkReIntersect(regexes ...*Expr) - Intersection
  • MkReComplement(re *Expr) - Complement
  • MkReDiff(a, b *Expr) - Difference
  • MkReEmpty/Full/Allchar(sort *Sort) - Special regexes
  • MkReRange(lo, hi *Expr) - Character range
  • MkSeqReplaceRe/ReAll(seq, re, replacement *Expr) - Regex replace

Datatype Operations

  • MkConstructor(name, recognizer string, ...) - Create constructor
  • MkDatatypeSort(name string, constructors []*Constructor) - Create datatype
  • MkDatatypeSorts(names []string, ...) - Mutually recursive datatypes
  • MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort) - Tuples
  • MkEnumSort(name string, enumNames []string) - Enumerations
  • MkListSort(name string, elemSort *Sort) - Lists

Tactic Operations

  • MkTactic(name string) - Create tactic by name
  • MkGoal(models, unsatCores, proofs bool) - Create goal
  • Apply(g *Goal) - Apply tactic to goal
  • AndThen(t2 *Tactic) - Sequential composition
  • OrElse(t2 *Tactic) - Try first, fallback to second
  • Repeat(max uint) - Repeat tactic
  • TacticWhen/Cond(...) - Conditional tactics

Probe Operations

  • MkProbe(name string) - Create probe by name
  • Apply(g *Goal) - Evaluate probe on goal
  • Lt/Gt/Le/Ge/Eq(p2 *Probe) - Probe comparisons
  • And/Or/Not(...) - Probe combinators

Parameter Operations

  • MkParams() - Create parameter set
  • SetBool/Uint/Double/Symbol(key string, value ...) - Set parameters

Optimize Operations

  • NewOptimize() - Create optimization context
  • Assert(constraint *Expr) - Add constraint
  • AssertSoft(constraint *Expr, weight, group string) - Add soft constraint
  • Maximize(expr *Expr) - Add maximization objective
  • Minimize(expr *Expr) - Add minimization objective
  • Check(assumptions ...*Expr) - Check and optimize
  • Model() - Get optimal model
  • GetLower/Upper(index uint) - Get objective bounds
  • Push/Pop() - Backtracking
  • Assertions/Objectives() - Get assertions and objectives
  • UnsatCore() - Get unsat core

Fixedpoint Operations (Datalog/CHC)

  • NewFixedpoint() - Create fixedpoint solver
  • RegisterRelation(funcDecl *FuncDecl) - Register predicate
  • AddRule(rule *Expr, name *Symbol) - Add Horn clause
  • AddFact(pred *FuncDecl, args []int) - Add table fact
  • Query(query *Expr) - Query constraints
  • QueryRelations(relations []*FuncDecl) - Query relations
  • GetAnswer() - Get satisfying instance or proof
  • Push/Pop() - Backtracking

Quantifier Operations

  • MkQuantifier(isForall bool, weight int, sorts, names, body, patterns) - Create quantifier
  • MkQuantifierConst(isForall bool, weight int, bound, body, patterns) - Create with bound vars
  • IsUniversal/IsExistential() - Check quantifier type
  • GetNumBound() - Number of bound variables
  • GetBoundName/Sort(idx int) - Get bound variable info
  • GetBody() - Get quantifier body
  • GetNumPatterns() - Number of patterns
  • GetPattern(idx int) - Get pattern

Lambda Operations

  • MkLambda(sorts, names, body) - Create lambda expression
  • MkLambdaConst(bound, body) - Create lambda with bound variables
  • GetNumBound() - Number of bound variables
  • GetBoundName/Sort(idx int) - Get bound variable info
  • GetBody() - Get lambda body

Type Variables

  • MkTypeVariable(name *Symbol) - Create polymorphic type variable sort

Logging

  • OpenLog(filename string) - Open interaction log
  • CloseLog() - Close log
  • AppendLog(s string) - Append to log
  • IsLogOpen() - Check if log is open

Memory Management

The Go bindings use runtime.SetFinalizer to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately.

Thread Safety

Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context.

License

Z3 is licensed under the MIT License. See LICENSE.txt in the repository root.

Contributing

Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository.

References