mirror of
https://github.com/Z3Prover/z3
synced 2026-02-22 16:27:37 +00:00
git bindings v1.0
This commit is contained in:
Nikolaj Bjorner
parent
adacc27644
commit
a03500a194
33 changed files with 5289 additions and 7 deletions
331
src/api/go/README.md
Normal file
331
src/api/go/README.md
Normal file
|
|
@ -0,0 +1,331 @@
|
|||
# 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
|
||||
|
||||
```bash
|
||||
mkdir build && cd build
|
||||
cmake -DBUILD_GO_BINDINGS=ON ..
|
||||
make
|
||||
```
|
||||
|
||||
### With Python Build System
|
||||
|
||||
```bash
|
||||
python scripts/mk_make.py --go
|
||||
cd build
|
||||
make
|
||||
```
|
||||
|
||||
## Usage
|
||||
|
||||
### Basic Example
|
||||
|
||||
```go
|
||||
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
|
||||
|
||||
```bash
|
||||
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
|
||||
|
||||
- [Z3 GitHub Repository](https://github.com/Z3Prover/z3)
|
||||
- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html)
|
||||
- [Z3 Guide](https://microsoft.github.io/z3guide/)
|
||||
Loading…
Add table
Add a link
Reference in a new issue