README
¶
Go Bindings to the Z3 Theorem Prover
go-z3 provides bindings to Z3, a theorem prover out of Microsoft Research. Z3 is a state-of-the-art SMT Solver.
This library provides bindings via cgo directly to Z3.
Library Status: Most major sections of the API are covered, but the Z3 API is massive. Adding missing APIs should be trivial unless the entire category/type is not implemented yet. Please issue a pull request for any missing APIs and I'll add it!
Installation
Installation is a little trickier than a standard Go library, but not
by much. You can't simply go get this library, unfortunately. This is
because Z3 must first be built. We
don't ship a pre-built version of Z3.
To build Z3, we've made it very easy. You will need the following packages available on your host operating system:
- Python
- Make
- gcc/Clang
Then just type:
$ make
This will download Z3, compile it, and run the tests for go-z3, verifying that your build is functional. By default, go-z3 will download and build the "master" ref of Z3, but this is customizable.
Compiling/installing the go-z3 library should work on Linux, Mac OS X, and Windows. On Windows, msys is the only supported build toolchain (same as Go itself).
Due to this linking, it is strongly recommended that you vendor this repository and bake our build system into your process.
Customizing the Z3 Compilation
You can customize the Z3 compilation by setting a couple environmental
variables prior to calling make:
Z3_REFis the git ref that will be checked out for Z3. This defaults to to a recently tagged version. It is recommended that you explicitly set this to a ref that works for you to avoid any changes in this library later.
Usage
go-z3 exposes the Z3 API in a style that mostly idiomatic Go. The API should be comfortable to use by any Go programmer without having intimate knowledge of how Z3 works.
For usage examples and documentation, please see the go-z3 GoDoc, which we keep up to date and full of examples.
For a quick taste of what using go-z3 looks like, though, we provide a basic example below:
package main
import (
"fmt"
"github.com/mitchellh/go-z3"
)
func main() {
// Create the context
config := z3.NewConfig()
ctx := z3.NewContext(config)
config.Close()
defer ctx.Close()
// Logic:
// x + y + z > 4
// x + y < 2
// z > 0
// x != y != z
// x, y, z != 0
// x + y = -3
// Create the solver
s := ctx.NewSolver()
defer s.Close()
// Vars
x := ctx.Const(ctx.Symbol("x"), ctx.IntSort())
y := ctx.Const(ctx.Symbol("y"), ctx.IntSort())
z := ctx.Const(ctx.Symbol("z"), ctx.IntSort())
zero := ctx.Int(0, ctx.IntSort()) // To save repeats
// x + y + z > 4
s.Assert(x.Add(y, z).Gt(ctx.Int(4, ctx.IntSort())))
// x + y < 2
s.Assert(x.Add(y).Lt(ctx.Int(2, ctx.IntSort())))
// z > 0
s.Assert(z.Gt(zero))
// x != y != z
s.Assert(x.Distinct(y, z))
// x, y, z != 0
s.Assert(x.Eq(zero).Not())
s.Assert(y.Eq(zero).Not())
s.Assert(z.Eq(zero).Not())
// x + y = -3
s.Assert(x.Add(y).Eq(ctx.Int(-3, ctx.IntSort())))
if v := s.Check(); v != True {
fmt.Println("Unsolveable")
return
}
// Get the resulting model:
m := s.Model()
assignments := m.Assignments()
m.Close()
fmt.Printf("x = %s\n", assignments["x"])
fmt.Printf("y = %s\n", assignments["y"])
fmt.Printf("z = %s\n", assignments["z"])
// Output:
// x = (- 2)
// y = (- 1)
// z = 8
}
Issues and Contributing
If you find an issue with this library, please report an issue. If you'd like, we welcome any contributions. Fork this library and submit a pull request.
Documentation
¶
Overview ¶
Package z3 provides Go bindings to the Z3 SMT Solver.
The bindings are a balance between idiomatic Go and being an obvious translation from the Z3 API so you can look up Z3 APIs and find the intuitive mapping in Go.
The most foreign thing to Go programmers will be error handling. Rather than return the `error` type from almost every function, the z3 package mimics Z3's API by requiring you to set an error handler callback. This error handler will be invoked whenenver an error occurs. See ErrorHandler and Context.SetErrorHandler for more information.
Index ¶
- Constants
- type AST
- func (a *AST) Add(args ...*AST) *AST
- func (a *AST) And(args ...*AST) *AST
- func (a *AST) BigInt() *big.Int
- func (a *AST) DeclName() *Symbol
- func (a *AST) Distinct(args ...*AST) *AST
- func (a *AST) Div(arg *AST) *AST
- func (a *AST) Eq(a2 *AST) *AST
- func (a *AST) Ge(a2 *AST) *AST
- func (a *AST) Gt(a2 *AST) *AST
- func (a *AST) Iff(a2 *AST) *AST
- func (a *AST) Implies(a2 *AST) *AST
- func (a *AST) Int() int
- func (a *AST) IntString() string
- func (a *AST) Ite(a2, a3 *AST) *AST
- func (a *AST) Le(a2 *AST) *AST
- func (a *AST) Lt(a2 *AST) *AST
- func (a *AST) Mul(args ...*AST) *AST
- func (a *AST) Not() *AST
- func (a *AST) Or(args ...*AST) *AST
- func (a *AST) String() string
- func (a *AST) Sub(args ...*AST) *AST
- func (a *AST) Xor(a2 *AST) *AST
- type Config
- type Context
- func (c *Context) BigInt(v *big.Int, typ *Sort) *AST
- func (c *Context) BoolSort() *Sort
- func (c *Context) Close() error
- func (c *Context) Const(s *Symbol, typ *Sort) *AST
- func (c *Context) Error(code ErrorCode) string
- func (c *Context) False() *AST
- func (c *Context) Int(v int, typ *Sort) *AST
- func (c *Context) IntSort() *Sort
- func (c *Context) NewSolver() *Solver
- func (c *Context) SetErrorHandler(f ErrorHandler)
- func (c *Context) Symbol(name string) *Symbol
- func (c *Context) SymbolInt(name int) *Symbol
- func (c *Context) True() *AST
- func (c *Context) Z3Value() C.Z3_context
- type ErrorCode
- type ErrorHandler
- type LBool
- type Model
- type Solver
- type Sort
- type Symbol
Constants ¶
const ( False LBool = C.Z3_L_FALSE Undef = C.Z3_L_UNDEF True = C.Z3_L_TRUE )
const ( ErrorCodeOk ErrorCode = C.Z3_OK ErrorCodeSortError = C.Z3_SORT_ERROR ErrorCodeIOB = C.Z3_IOB ErrorCodeInvalidArg = C.Z3_INVALID_ARG ErrorCodeParserError = C.Z3_PARSER_ERROR ErrorCodeNoParser = C.Z3_NO_PARSER ErrorCodeInvalidPattern = C.Z3_INVALID_PATTERN ErrorCodeMemoutFail = C.Z3_MEMOUT_FAIL ErrorCodeFileAccessError = C.Z3_FILE_ACCESS_ERROR ErrorCodeInternalFatal = C.Z3_INTERNAL_FATAL ErrorCodeInvalidUsage = C.Z3_INVALID_USAGE ErrorCodeDecRefError = C.Z3_DEC_REF_ERROR ErrorCodeException = C.Z3_EXCEPTION )
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type AST ¶
type AST struct {
// contains filtered or unexported fields
}
AST represents an AST value in Z3.
AST memory management is automatically managed by the Context it is contained within. When the Context is freed, so are the AST nodes.
func (*AST) Add ¶
Add creates an AST node representing adding.
All AST values must be part of the same context.
func (*AST) And ¶
And creates an AST node representing a and a2 and ... aN.
a and a2 must be part of the same Context and be boolean types.
func (*AST) DeclName ¶
DeclName returns the name of a declaration. The AST value must be a func declaration for this to work.
func (*AST) Distinct ¶
Distinct creates an AST node representing adding.
All AST values must be part of the same context.
func (*AST) Iff ¶
Iff creates an AST node representing a iff a2.
a and a2 must be part of the same Context and be boolean types.
func (*AST) Implies ¶
Implies creates an AST node representing a implies a2.
a and a2 must be part of the same Context and be boolean types.
func (*AST) Int ¶
Int gets the integer value of this AST. The value must be able to fit into a machine integer.
func (*AST) Ite ¶
Ite creates an AST node representing if a then a2 else a3.
a and a2 must be part of the same Context and be boolean types.
func (*AST) Mul ¶
Mul creates an AST node representing multiplication.
All AST values must be part of the same context.
func (*AST) Or ¶
Or creates an AST node representing a or a2 or ... aN.
a and a2 must be part of the same Context and be boolean types.
type Config ¶
type Config struct {
// contains filtered or unexported fields
}
Config is used to set configuration for Z3. This should be created with NewConfig and closed with Close when you're done using it.
Config structures are used to set parameters for Z3 behavior. See the Z3 docs for information on available parameters. They can be set with SetParamValue.
As for 2016-03-02, the parameters available are documented as:
proof (Boolean) Enable proof generation debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting trace (Boolean) Tracing support for VCC trace_file_name (String) Trace out file for VCC traces timeout (unsigned) default timeout (in milliseconds) used for solvers well_sorted_check type checker auto_config use heuristics to automatically select solver and configure it model model generation for solvers, this parameter can be overwritten when creating a solver model_validate validate models produced by solvers unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
func (*Config) SetParamValue ¶
SetParamValue sets the parameters for a Config. See the Config docs.
type Context ¶
type Context struct {
// contains filtered or unexported fields
}
Context is what handles most of the interactions with Z3.
func NewContext ¶
func (*Context) Const ¶
Const declares a variable. It is called "Const" since internally this is equivalent to create a function that always returns a constant value. From an initial user perspective this may be confusing but go-z3 is following identical naming convention.
func (*Context) Error ¶
Error returns the error message for the given error code. This code can be retrieved via the error handler callback.
This MUST be called during the handler. This must not be called later since the error state on the context may have cleared.
Maps: Z3_get_error_msg_ex
func (*Context) SetErrorHandler ¶
func (c *Context) SetErrorHandler(f ErrorHandler)
SetErrorHandler registers the error handler. This handler is invoked whenever an error occurs within Z3.
func (*Context) Symbol ¶
Create a symbol named by a string within the context.
The memory associated with this symbol is freed when the context is freed.
func (*Context) SymbolInt ¶
Create a symbol named by an int within the context.
The memory associated with this symbol is freed when the context is freed.
func (*Context) Z3Value ¶
func (c *Context) Z3Value() C.Z3_context
Z3Value returns the internal structure for this Context.
type ErrorHandler ¶
ErrorHandler is the callback that is invoked when an error occurs in Z3 and is registered by SetErrorHandler.
type LBool ¶
type LBool int8
LBool is the lifted boolean type representing false, true, and undefined.
type Model ¶
type Model struct {
// contains filtered or unexported fields
}
Model represents a model from a solver.
Memory management for this is manual and based on reference counting. When a model is initialized (via Solver.Model for example), it always has a reference count of 1. You must call Close when you're done.
func (*Model) Assignments ¶
Assignments returns a map of all the assignments for all the constants within the model. The key of the map will be the String value of the symbol.
This doesn't map to any specific Z3 API. This is a higher-level function provided by go-z3 to make the Z3 API easier to consume in Go.
func (*Model) Close ¶
Close decreases the reference count for this model. If nothing else has manually increased the reference count, this will free the memory associated with it.
func (*Model) ConstDecl ¶
ConstDecl returns the const declaration for the given index. idx must be less than NumConsts.
Maps: Z3_model_get_const_decl
func (*Model) DecRef ¶
func (m *Model) DecRef()
DecRef decreases the reference count of this model. This is advanced, you probably don't need to use this.
Close will decrease it automatically from the initial 1, so this should only be called with exact matching calls to IncRef.
func (*Model) Eval ¶
Eval evaluates the given AST within the model. This can be used to get the assignment of an AST. This will return nil if evaluation failed.
For example:
x := ctx.Const(ctx.Symbol("x"), ctx.IntSort())
// ... further solving
m.Eval(x) => x's value
Maps: Z3_model_eval
func (*Model) IncRef ¶
func (m *Model) IncRef()
IncRef increases the reference count of this model. This is advanced, you probably don't need to use this.
type Solver ¶
type Solver struct {
// contains filtered or unexported fields
}
Solver is a single solver tied to a specific Context within Z3.
It is created via the NewSolver methods on Context. When a solver is no longer needed, the Close method must be called. This will remove the solver from the context and no more APIs on Solver may be called thereafter.
Freeing the context (Context.Close) will NOT automatically close associated solvers. They must be managed separately.
type Sort ¶
type Sort struct {
// contains filtered or unexported fields
}
Sort represents a sort in Z3.
Source Files