z3

package
v0.0.0-...-f39ad0c Latest Latest
Warning

This package is not in the latest version of its module.

Go to latest
Published: Jun 23, 2023 License: BSD-3-Clause, GPL-2.0 Imports: 8 Imported by: 7

Documentation

Overview

Package z3 checks the satisfiability of logical formulas.

This package provides bindings for the Z3 SMT solver (https://github.com/Z3Prover/z3). Z3 checks satisfiability of logical formulas over a wide range of terms, including booleans, integers, reals, bit-vectors, and uninterpreted functions. For a good introduction to the concepts of SMT and Z3, see the Z3 guide (http://rise4fun.com/z3/tutorialcontent/guide).

This package does not yet support all of the features or types supported by Z3, though it supports a reasonably large subset.

The main entry point to the z3 package is type Context. All values are created and all solving is done relative to some Context, and values from different Contexts cannot be mixed.

Symbolic values implement the Value interface. Every value has a type, called a "sort" and represented by type Sort. Sorts fall into general categories called "kinds", such as Bool and Int. Each kind corresponds to a different concrete type that implements the Value interface, since the kind determines the set of operations that make sense on a value. A Bool expression is also called a "formula".

These concrete value types help with type checking expressions, but type checking is ultimately done dynamically by Z3. Attempting to create a badly typed value will panic.

Symbolic values are represented as expressions of numerals, constants, and uninterpreted functions. A numeral is a literal, fixed value like "2". A constant is a term like "x", whose value is fixed but unspecified. An uninterpreted function is a function whose mapping from arguments to results is fixed but unspecified (this is in contrast to an "interpreted function" like + whose interpretation is specified to be addition). Functions are pure (side-effect-free) like mathematical functions, but unlike mathematical functions they are always total. A constant can be thought of as a function with zero arguments.

It's possible to go back and forth between a symbolic value and the expression representing that value using Value.AsAST and AST.AsValue.

Type Solver checks the satisfiability of a set of formulas. If the Solver determines that a set of formulas is satisfiable, it can construct a Model giving a specific assignment of constants and uninterpreted functions that satisfies the set of formulas.

Index

Constants

View Source
const (
	ASTKindApp        = ASTKind(C.Z3_APP_AST)        // Constant and applications
	ASTKindNumeral    = ASTKind(C.Z3_NUMERAL_AST)    // Numeral constants (excluding real algebraic numbers)
	ASTKindVar        = ASTKind(C.Z3_VAR_AST)        // Bound variables
	ASTKindQuantifier = ASTKind(C.Z3_QUANTIFIER_AST) // Quantifiers
	ASTKindSort       = ASTKind(C.Z3_SORT_AST)       // Sorts
	ASTKindFuncDecl   = ASTKind(C.Z3_FUNC_DECL_AST)  // Function declarations
	ASTKindUnknown    = ASTKind(C.Z3_UNKNOWN_AST)
)
View Source
const (
	KindUninterpreted = Kind(C.Z3_UNINTERPRETED_SORT)
	KindBool          = Kind(C.Z3_BOOL_SORT)
	KindInt           = Kind(C.Z3_INT_SORT)
	KindReal          = Kind(C.Z3_REAL_SORT)
	KindBV            = Kind(C.Z3_BV_SORT)
	KindArray         = Kind(C.Z3_ARRAY_SORT)
	KindDatatype      = Kind(C.Z3_DATATYPE_SORT)
	KindRelation      = Kind(C.Z3_RELATION_SORT)
	KindFiniteDomain  = Kind(C.Z3_FINITE_DOMAIN_SORT)
	KindFloatingPoint = Kind(C.Z3_FLOATING_POINT_SORT)
	KindRoundingMode  = Kind(C.Z3_ROUNDING_MODE_SORT)
	KindUnknown       = Kind(C.Z3_UNKNOWN_SORT)
)

Variables

This section is empty.

Functions

This section is empty.

Types

type AST

type AST struct {
	// contains filtered or unexported fields
}

An AST is the abstract syntax tree of an expression, sort, etc.

func (AST) AsFuncDecl

func (ast AST) AsFuncDecl() FuncDecl

AsFuncDecl returns this AST as a FuncDecl.

It panics if ast is not a function declaration expression. That is, ast must have Kind ASTKindFuncDecl.

func (AST) AsSort

func (ast AST) AsSort() Sort

AsSort returns this AST as a sort.

It panics if ast is not a sort expression. That is, ast must have Kind ASTKindSort.

func (AST) AsValue

func (ast AST) AsValue() Value

AsValue returns this AST as a symbolic value.

It panics if ast is not a value expression. That is, ast must have Kind ASTKindApp, ASTKindNumeral, ASTKindVar, or ASTKindQuantifier.

func (AST) Context

func (ast AST) Context() *Context

Context returns the Context that created ast.

func (AST) Equal

func (ast AST) Equal(o AST) bool

Equal returns true if ast and o are identical ASTs.

func (AST) Hash

func (ast AST) Hash() uint64

Hash returns a hash of ast. Structurally identical ASTs will have the same hash code.

func (AST) ID

func (ast AST) ID() uint64

ID returns the unique identifier for ast. Within a Context, two ASTs have the same ID if and only if they are Equal.

func (AST) Kind

func (ast AST) Kind() ASTKind

Kind returns ast's kind.

func (AST) String

func (ast AST) String() string

String returns ast as an S-expression.

func (AST) Translate

func (ast AST) Translate(target *Context) AST

Translate copies ast into the target Context.

type ASTKind

type ASTKind int

ASTKind is a general category of ASTs, such as numerals, applications, or sorts.

func (ASTKind) String

func (k ASTKind) String() string

String returns k as a string like "ASTKindApp".

type Array

type Array value

Array is a symbolic value representing an extensional array.

Unlike typical arrays in programming, an extensional array has an arbitrary index (domain) sort, in addition to an arbitrary value (range) sort. It can also be viewed like a hash table, except that all possible keys are always present.

Arrays are "updated" by storing a new value to a particular index. This creates a new array that's identical to the old array except that that index.

Array implements Value.

func (Array) Default

func (x Array) Default() Value

Default returns the default value of an array, for arrays that can be represented as finite maps plus a default value.

This is useful for extracting array values interpreted by models.

func (Array) Eq

func (l Array) Eq(r Array) Bool

Eq returns a Value that is true if l and r are equal.

func (Array) NE

func (l Array) NE(r Array) Bool

NE returns a Value that is true if l and r are not equal.

func (Array) Select

func (x Array) Select(i Value) Value

Select returns the value of array x at index i.

i's sort must match x's domain. The result has the sort of x's range.

func (Array) Store

func (x Array) Store(i Value, v Value) Array

Store returns an array y that's identical to x except that y.Select(i) == v.

i's sort must match x's domain and v's sort must match x's range. The result has the same sort as x.

type BV

type BV value

BV is a symbolic value representing a bit-vector.

Bit vectors correspond to machine words. They have finite domains of size 2^n and implement modular arithmetic in both unsigned and two's complement signed forms.

BV implements Value.

func (BV) Add

func (l BV) Add(r BV) BV

Add returns the two's complement sum of l and r.

l and r must have the same size.

func (BV) AllBits

func (l BV) AllBits() BV

AllBits returns a 1-bit bit-vector that is the bit-wise "and" of all bits.

func (BV) And

func (l BV) And(r BV) BV

And returns the bit-wise and of l and r.

l and r must have the same size.

func (BV) AnyBits

func (l BV) AnyBits() BV

AnyBits returns a 1-bit bit-vector that is the bit-wise "or" of all bits.

func (BV) AsBigSigned

func (lit BV) AsBigSigned() (val *big.Int, isLiteral bool)

AsBigSigned returns the value of lit as a math/big.Int, interpreting lit as a signed two's complement number. If lit is not a literal, it returns nil, false.

func (BV) AsBigUnsigned

func (lit BV) AsBigUnsigned() (val *big.Int, isLiteral bool)

AsBigUnsigned is like AsBigSigned, but interprets lit as unsigned.

func (BV) AsInt64

func (lit BV) AsInt64() (val int64, isLiteral, ok bool)

AsInt64 returns the value of lit as an int64, interpreting lit as a two's complement signed number. If lit is not a literal, it returns 0, false, false. If lit is a literal, but its value cannot be represented as an int64, it returns 0, true, false.

func (BV) AsUint64

func (lit BV) AsUint64() (val uint64, isLiteral, ok bool)

AsUint64 is like AsInt64, but interprets lit as unsigned and fails if lit cannot be represented as a uint64.

func (BV) Concat

func (l BV) Concat(r BV) BV

Concat returns concatenation of l and r.

The result is a bit-vector whose length is the sum of the lengths of l and r.

func (BV) Eq

func (l BV) Eq(r BV) Bool

Eq returns a Value that is true if l and r are equal.

func (BV) Extract

func (l BV) Extract(high int, low int) BV

Extract returns bits [high, low] (inclusive) of l, where bit 0 is the least significant bit.

func (BV) IEEEToFloat

func (l BV) IEEEToFloat(s Sort) Float

IEEEToFloat converts l into a floating-point number, interpreting l in IEEE 754-2008 format.

The size of l must equal ebits+sbits of s.

func (BV) Lsh

func (l BV) Lsh(i BV) BV

Lsh returns l shifted left by i bits.

This is equivalent to l * 2^i.

l and i must have the same size. The result has the same sort.

func (BV) Mul

func (l BV) Mul(r BV) BV

Mul returns the two's complement product of l and r.

l and r must have the same size.

func (BV) NE

func (l BV) NE(r BV) Bool

NE returns a Value that is true if l and r are not equal.

func (BV) Nand

func (l BV) Nand(r BV) BV

Nand returns the bit-wise nand of l and r.

l and r must have the same size.

func (BV) Neg

func (l BV) Neg() BV

Neg returns the two's complement negation of l.

func (BV) Nor

func (l BV) Nor(r BV) BV

Nor returns the bit-wise nor of l and r.

l and r must have the same size.

func (BV) Not

func (l BV) Not() BV

Not returns the bit-wise negation of l.

func (BV) Or

func (l BV) Or(r BV) BV

Or returns the bit-wise or of l and r.

l and r must have the same size.

func (BV) Repeat

func (l BV) Repeat(i int) BV

Repeat returns l repeated up to length i.

func (BV) RotateLeft

func (l BV) RotateLeft(i BV) BV

RotateLeft returns l rotated left by i bits.

l and i must have the same size.

func (BV) RotateRight

func (l BV) RotateRight(i BV) BV

RotateRight returns l rotated right by i bits.

l and i must have the same size.

func (BV) SDiv

func (l BV) SDiv(r BV) BV

SDiv returns l / r rounded toward 0, treating l and r as two's complement signed numbers.

If r is 0, the result is unconstrained.

l and r must have the same size.

func (BV) SGE

func (l BV) SGE(r BV) Bool

SGE returns the l >= r, where l and r are signed.

l and r must have the same size.

func (BV) SGT

func (l BV) SGT(r BV) Bool

SGT returns the l > r, where l and r are signed.

l and r must have the same size.

func (BV) SLE

func (l BV) SLE(r BV) Bool

SLE returns the l <= r, where l and r are signed.

l and r must have the same size.

func (BV) SLT

func (l BV) SLT(r BV) Bool

SLT returns the l < r, where l and r are signed.

l and r must have the same size.

func (BV) SMod

func (l BV) SMod(r BV) BV

SMod returns the two's complement signed modulus of l divided by r.

The sign of the result follows the sign of r.

l and r must have the same size.

func (BV) SRem

func (l BV) SRem(r BV) BV

SRem returns the two's complement signed remainder of l divided by r.

The sign of the result follows the sign of l.

l and r must have the same size.

func (BV) SRsh

func (l BV) SRsh(i BV) BV

SRsh returns l arithmetically shifted right by i bits.

This is like URsh, but the sign of the result is the sign of l.

l and i must have the same size. The result has the same sort.

func (BV) SToFloat

func (l BV) SToFloat(s Sort) Float

SToFloat converts signed bit-vector l into a floating-point number.

If necessary, the result will be rounded according to the current rounding mode.

func (BV) SToInt

func (l BV) SToInt() Int

SToInt converts signed bit-vector l to an integer.

func (BV) SignExtend

func (l BV) SignExtend(i int) BV

SignExtend returns l sign-extended to a bit-vector of length m+i, where m is the length of l.

func (BV) Sub

func (l BV) Sub(r BV) BV

Sub returns the two's complement subtraction l minus r.

l and r must have the same size.

func (BV) UDiv

func (l BV) UDiv(r BV) BV

UDiv returns the floor of l / r, treating l and r as unsigned.

If r is 0, the result is unconstrained.

l and r must have the same size.

func (BV) UGE

func (l BV) UGE(r BV) Bool

UGE returns the l >= r, where l and r are unsigned.

l and r must have the same size.

func (BV) UGT

func (l BV) UGT(r BV) Bool

UGT returns the l > r, where l and r are unsigned.

l and r must have the same size.

func (BV) ULE

func (l BV) ULE(r BV) Bool

ULE returns the l <= r, where l and r are unsigned.

l and r must have the same size.

func (BV) ULT

func (l BV) ULT(r BV) Bool

ULT returns the l < r, where l and r are unsigned.

l and r must have the same size.

func (BV) URem

func (l BV) URem(r BV) BV

URem returns the unsigned remainder of l divided by r.

l and r must have the same size.

func (BV) URsh

func (l BV) URsh(i BV) BV

URsh returns l logically shifted right by i bits.

This is equivalent to l / 2^i, where l and i are unsigned.

l and i must have the same size. The result has the same sort.

func (BV) UToFloat

func (l BV) UToFloat(s Sort) Float

UToFloat converts unsigned bit-vector l into a floating-point number.

If necessary, the result will be rounded according to the current rounding mode.

func (BV) UToInt

func (l BV) UToInt() Int

UToInt converts unsigned bit-vector l to an integer.

func (BV) Xnor

func (l BV) Xnor(r BV) BV

Xnor returns the bit-wise xnor of l and r.

l and r must have the same size.

func (BV) Xor

func (l BV) Xor(r BV) BV

Xor returns the bit-wise xor of l and r.

l and r must have the same size.

func (BV) ZeroExtend

func (l BV) ZeroExtend(i int) BV

ZeroExtend returns l zero-extended to a bit-vector of length m+i, where m is the length of l.

type Bool

type Bool value

Bool is a symbolic value representing "true" or "false".

Bool implements Value.

func (Bool) And

func (l Bool) And(r ...Bool) Bool

And returns a Value that is true if l and all arguments are true.

func (Bool) AsBool

func (l Bool) AsBool() (val bool, isLiteral bool)

AsBool returns the value of l as a Go bool. If l is not a literal, AsBool returns false, false.

func (Bool) Eq

func (l Bool) Eq(r Bool) Bool

Eq returns a Value that is true if l and r are equal.

func (Bool) IfThenElse

func (cond Bool) IfThenElse(cons Value, alt Value) Value

IfThenElse returns a Value equal to cons if cond is true, otherwise alt.

cons and alt must have the same sort. The result will have the same sort as cons and alt.

func (Bool) Iff

func (l Bool) Iff(r Bool) Bool

Iff returns a Value that is true if l and r are equal (l if-and-only-if r).

func (Bool) Implies

func (l Bool) Implies(r Bool) Bool

Implies returns a Value that is true if l implies r.

func (Bool) NE

func (l Bool) NE(r Bool) Bool

NE returns a Value that is true if l and r are not equal.

func (Bool) Not

func (l Bool) Not() Bool

Not returns the boolean negation of l.

func (Bool) Or

func (l Bool) Or(r ...Bool) Bool

Or returns a Value that is true if l or any argument is true.

func (Bool) Xor

func (l Bool) Xor(r Bool) Bool

Xor returns a Value that is true if l xor r.

type Config

type Config struct {
	// contains filtered or unexported fields
}

Config stores a set of configuration parameters. Configs are used to configure many different objects in Z3.

func NewContextConfig

func NewContextConfig() *Config

NewContextConfig returns *Config for configuring a new Context.

The following are commonly useful parameters:

	timeout           uint    Timeout in milliseconds used for solvers (default: ∞)
	auto_config       bool    Use heuristics to automatically select solver and configure it (default: true)
	proof             bool    Enable proof generation (default: false)
	model             bool    Enable model generation for solvers by default (default: true)
     unsat_core        bool    Enable unsat core generation for solvers by default (default: false)

Most of these can be changed after a Context is created using Context.Config().

func NewSimplifyConfig

func NewSimplifyConfig(ctx *Context) *Config

NewSimplifyConfig returns *Config for configuring the simplifier.

func (*Config) SetBool

func (p *Config) SetBool(name string, value bool) *Config

func (*Config) SetFloat

func (p *Config) SetFloat(name string, value float64) *Config

func (*Config) SetString

func (p *Config) SetString(name, value string) *Config

func (*Config) SetUint

func (p *Config) SetUint(name string, value uint) *Config

type Context

type Context struct {
	// contains filtered or unexported fields
}

Context is an environment for creating symbolic values and checking satisfiability.

Nearly all interaction with Z3 is done relative to a Context. Values are bound to the Context that created them and cannot be combined with Values from other Contexts.

Context is thread-safe. However, most operations block other operations (one notable exception is Interrupt). Hence, to do things in parallel, it's best to create multiple Contexts.

func NewContext

func NewContext(config *Config) *Context

NewContext returns a new Z3 context with the given configuration.

The config argument must have been created with NewContextConfig. If config is nil, the default configuration is used.

func (*Context) ArraySort

func (ctx *Context) ArraySort(domain, range_ Sort) Sort

ArraySort returns a sort for arrays that are indexed by domain and have values from range.

func (*Context) BVConst

func (ctx *Context) BVConst(name string, bits int) BV

BVConst returns a bit-vector constant named "name" with the given width in bits.

func (*Context) BVSort

func (ctx *Context) BVSort(bits int) Sort

BVSort returns a bit-vector sort of the given width in bits.

func (*Context) BoolConst

func (ctx *Context) BoolConst(name string) Bool

BoolConst returns a boolean constant named "name".

func (*Context) BoolSort

func (ctx *Context) BoolSort() Sort

BoolSort returns the boolean sort.

func (*Context) Config

func (ctx *Context) Config() *Config

Config returns a *Config object for dynamically changing ctx's configuration.

func (*Context) Const

func (ctx *Context) Const(name string, sort Sort) Value

Const returns a constant named "name" of the given sort. This constant will be same as all other constants created with this name.

func (*Context) ConstArray

func (ctx *Context) ConstArray(domain Sort, value Value) Array

ConstArray returns an Array value where every index maps to value.

func (*Context) Distinct

func (ctx *Context) Distinct(vals ...Value) Bool

Distinct returns a Value that is true if no two vals are equal.

All Values must have the same sort.

func (*Context) Extra

func (ctx *Context) Extra(key interface{}) interface{}

Extra returns the "extra" data associated with key, or nil if there is no data associated with key.

func (*Context) FiniteDomainSort

func (ctx *Context) FiniteDomainSort(name string, n uint64) Sort

FiniteDomainSort returns a sort for finite domain values with domain size n.

Two finite-domain sorts are the same if and only if they have the same name.

func (*Context) FloatFromBits

func (ctx *Context) FloatFromBits(sign, exp, sig BV) Float

FloatFromBits constructs a floating-point value from a sign bit, exponent bits, and significand bits.

See the description of type Float for how these bits are interpreted.

sign must be a 1-bit bit-vector.

func (*Context) FloatInf

func (ctx *Context) FloatInf(s Sort, neg bool) Float

FloatInf returns a floating-point infinity of sort s.

func (*Context) FloatNaN

func (ctx *Context) FloatNaN(s Sort) Float

FloatNaN returns a floating-point NaN of sort s.

func (*Context) FloatSort

func (ctx *Context) FloatSort(ebits, sbits int) Sort

FloatSort returns a floating-point sort with ebits exponent bits and sbits significand bits.

Note that sbits counts the "hidden" most-significant bit of the significand. Hence, a double-precision floating point number has sbits of 53, even though only 52 bits are actually represented.

Common exponent and significand bit counts are:

                 ebits sbits
Half precision       5    11
Single precision     8    24  (float32)
Double precision    11    53  (float64)
Quad precision      15   113

func (*Context) FloatZero

func (ctx *Context) FloatZero(s Sort, neg bool) Float

FloatZero returns a (signed) floating-point zero of sort s.

func (*Context) FreshConst

func (ctx *Context) FreshConst(prefix string, sort Sort) Value

FreshConst returns a constant that is distinct from all other constants. The name will begin with "prefix".

func (*Context) FreshFuncDecl

func (ctx *Context) FreshFuncDecl(prefix string, domain []Sort, range_ Sort) FuncDecl

FreshFuncDecl creates a fresh uninterpreted function distinct from all other functions.

func (*Context) FromBigInt

func (ctx *Context) FromBigInt(val *big.Int, sort Sort) Value

FromBigInt returns a literal whose value is val. sort must have kind int, real, finite-domain, bit-vector, or float.

func (*Context) FromBigRat

func (ctx *Context) FromBigRat(val *big.Rat) Real

FromBigRat returns a real literal whose value is val.

func (*Context) FromBool

func (ctx *Context) FromBool(val bool) Bool

FromBool returns a boolean value with value val.

func (*Context) FromFloat32

func (ctx *Context) FromFloat32(val float32, sort Sort) Float

FromFloat32 constructs a floating-point literal from val. sort must be a floating-point sort.

func (*Context) FromFloat64

func (ctx *Context) FromFloat64(val float64, sort Sort) Float

FromFloat64 constructs a floating-point literal from val. sort must be a floating-point sort.

func (*Context) FromInt

func (ctx *Context) FromInt(val int64, sort Sort) Value

FromInt returns a literal whose value is val. sort must have kind int, real, finite-domain, bit-vector, or float.

func (*Context) FuncDecl

func (ctx *Context) FuncDecl(name string, domain []Sort, range_ Sort) FuncDecl

FuncDecl creates an uninterpreted function named "name".

In contrast with an interpreted function like "+", an uninterpreted function is only assigned an interpretation in a particular model, and different models may assign different interpretations.

func (*Context) IntConst

func (ctx *Context) IntConst(name string) Int

IntConst returns a int constant named "name".

func (*Context) IntSort

func (ctx *Context) IntSort() Sort

IntSort returns the integer sort.

func (*Context) Interrupt

func (ctx *Context) Interrupt()

Interrupt stops the current solver, simplifier, or tactic being executed by ctx.

func (*Context) RealConst

func (ctx *Context) RealConst(name string) Real

RealConst returns a int constant named "name".

func (*Context) RealSort

func (ctx *Context) RealSort() Sort

RealSort returns the real sort.

func (*Context) RoundingMode

func (ctx *Context) RoundingMode() RoundingMode

RoundingMode returns ctx's current rounding mode for floating-point operations.

func (*Context) SetExtra

func (ctx *Context) SetExtra(key, value interface{})

SetExtra associates key with value in ctx's "extra" data. This can be used by other packages to associate other data with ctx, such as caches. key must support comparison.

func (*Context) SetRoundingMode

func (ctx *Context) SetRoundingMode(rm RoundingMode) RoundingMode

SetRoundingMode sets ctx's current rounding mode for floating-point operations and returns ctx's old rounding mode.

func (*Context) Simplify

func (ctx *Context) Simplify(x Value, config *Config) Value

Simplify simplifies expression x.

The config argument must have been created with NewSimplifyConfig. If config is nil, the default configuration is used.

The resulting expression will have the same sort and value as x, but with a simpler AST.

func (*Context) UninterpretedSort

func (ctx *Context) UninterpretedSort(name string) Sort

UninterpretedSort returns a sort for uninterpreted values.

Two uninterpreted sorts are the same if and only if they have the same name.

type ErrSatUnknown

type ErrSatUnknown struct {
	// Reason gives a brief description of why Z3 could not
	// determine satisfiability.
	Reason string
}

ErrSatUnknown is produced when Z3 cannot determine satisfiability.

func (*ErrSatUnknown) Error

func (e *ErrSatUnknown) Error() string

Error returns the reason Z3 could not determine satisfiability.

type FiniteDomain

type FiniteDomain value

FiniteDomain is a symbolic value from a finite domain of size n, where n depends on the value's sort.

Finite domain values are uninterpreted (see Uninterpreted), but represented as numerals. Hence, to construct a specific finite-domain value, use methods like Context.FromInt with a value in [0, n).

FiniteDomain implements Value.

func (FiniteDomain) Eq

func (l FiniteDomain) Eq(r FiniteDomain) Bool

Eq returns a Value that is true if l and r are equal.

func (FiniteDomain) NE

func (l FiniteDomain) NE(r FiniteDomain) Bool

NE returns a Value that is true if l and r are not equal.

type Float

type Float value

Float is a symbolic value representing a floating-point number with IEEE 764-2008 semantics (extended to any possible exponent and significand length).

A floating-point number falls into one of five categories: normal numbers, subnormal numbers, zero, infinite, or NaN. All of these except for NaN can be either positive or negative.

Floating-point numbers are represented as three fields: a single bit sign, an exponent ebits wide, and a significand sbits-1 wide. If the exponent field is neither all 0s or all 1s, then the value is a "normal" number, which is interpreted as

(-1)^sign * 2^(exp - bias) * (1 + sig / 2^sbits)

where bias = 2^(ebits - 1) - 1, and exp and sig are interpreted as unsigned binary values. In particular, the significand is extended with a "hidden" most-significant 1 bit and the exponent is "biased".

Float implements Value.

func (Float) Abs

func (l Float) Abs() Float

Abs returns the absolute value of l.

func (Float) Add

func (l Float) Add(r Float) Float

Add returns l+r.

Add uses the current rounding mode.

func (Float) AsBigFloat

func (lit Float) AsBigFloat() (val *big.Float, isLiteral bool)

AsBigFloat returns the value of lit as a math/big.Float. If lit is not a literal, it returns nil, false. If lit is NaN, it returns nil, true (because big.Float cannot represent NaN).

func (Float) Div

func (l Float) Div(r Float) Float

Div returns l/r.

Div uses the current rounding mode.

func (Float) Eq

func (l Float) Eq(r Float) Bool

Eq returns a Value that is true if l and r are equal.

func (Float) GE

func (l Float) GE(r Float) Bool

GE returns l >= r.

func (Float) GT

func (l Float) GT(r Float) Bool

GT returns l > r.

func (Float) IEEEEq

func (l Float) IEEEEq(r Float) Bool

IEEEEq returns l == r according to IEEE 754 equality.

This differs from Eq, which is true if l and r are identical. In contrast, under IEEE equality, ±0 == ±0, while NaN != NaN and ±inf != ±inf.

func (Float) IsInfinite

func (l Float) IsInfinite() Bool

IsInfinite returns true if l is ±∞.

func (Float) IsNaN

func (l Float) IsNaN() Bool

IsNaN returns true if l is NaN.

func (Float) IsNegative

func (l Float) IsNegative() Bool

IsNegative returns true if l is negative.

func (Float) IsNormal

func (l Float) IsNormal() Bool

IsNormal returns true if l is a normal floating-point number.

func (Float) IsPositive

func (l Float) IsPositive() Bool

IsPositive returns true if l is positive.

func (Float) IsSubnormal

func (l Float) IsSubnormal() Bool

IsSubnormal returns true if l is a subnormal floating-point number.

func (Float) IsZero

func (l Float) IsZero() Bool

IsZero returns true if l is ±0.

func (Float) LE

func (l Float) LE(r Float) Bool

LE returns l <= r.

func (Float) LT

func (l Float) LT(r Float) Bool

LT returns l < r.

func (Float) Max

func (l Float) Max(r Float) Float

Max returns the maximum of l and r.

func (Float) Min

func (l Float) Min(r Float) Float

Min returns the minimum of l and r.

func (Float) Mul

func (l Float) Mul(r Float) Float

Mul returns l*r.

Mul uses the current rounding mode.

func (Float) MulAdd

func (l Float) MulAdd(r Float, a Float) Float

MulAdd returns l*r+a (fused multiply and add).

MulAdd uses the current rounding mode on the result of the whole operation.

func (Float) NE

func (l Float) NE(r Float) Bool

NE returns a Value that is true if l and r are not equal.

func (Float) Neg

func (l Float) Neg() Float

Neg returns -l.

func (Float) Rem

func (l Float) Rem(r Float) Float

Rem returns the remainder of l/r.

func (Float) Round

func (l Float) Round(rm RoundingMode) Float

Round rounds l to an integral floating-point value according to rounding mode rm.

func (Float) Sqrt

func (l Float) Sqrt() Float

Sqrt returns the square root of l.

Sqrt uses the current rounding mode.

func (Float) Sub

func (l Float) Sub(r Float) Float

Sub returns l-r.

Sub uses the current rounding mode.

func (Float) ToFloat

func (l Float) ToFloat(s Sort) Float

ToFloat converts l into a floating-point number of a different floating-point sort.

If necessary, the result will be rounded according to the current rounding mode.

func (Float) ToIEEEBV

func (l Float) ToIEEEBV() BV

ToIEEEBV converts l to a bit-vector in IEEE 754-2008 format.

Note that NaN has many possible representations. This conversion always uses the same representation.

func (Float) ToReal

func (l Float) ToReal() Real

ToReal converts l into a real number.

If l is ±inf, or NaN, the result is unspecified.

func (Float) ToSBV

func (l Float) ToSBV(bits int) BV

ToSBV converts l.Round() into a signed bit-vector of size 'bits'.

l is first rounded to an integer using the current rounding mode. If the result is not in the range [-2^(bits-1), 2^(bits-1)-1], the result is unspecified.

func (Float) ToUBV

func (l Float) ToUBV(bits int) BV

ToUBV converts l.Round() into an unsigned bit-vector of size 'bits'.

l is first rounded to an integer using the current rounding mode. If the result is not in the range [0, 2^bits-1], the result is unspecified.

type FuncDecl

type FuncDecl struct {
	// contains filtered or unexported fields
}

FuncDecl is a function declaration.

A FuncDecl can represent either a interpreted function like "+" or an uninterpreted function created by Context.FuncDecl.

A FuncDecl can be applied to a set of arguments to create a Value representing the result of the function.

func (FuncDecl) Apply

func (f FuncDecl) Apply(args ...Value) Value

Apply creates a Value representing the result of applying f to args.

The sorts of args must be the domain of f. The sort of the resulting value will be f's range.

func (FuncDecl) AsAST

func (f FuncDecl) AsAST() AST

AsAST returns the AST representation of f.

func (FuncDecl) Context

func (f FuncDecl) Context() *Context

Context returns the Context that created f.

func (FuncDecl) Map

func (f FuncDecl) Map(args ...Array) Array

Map applies f to each value in each of the args array.

Given that f has sort range_1, ..., range_n -> range, args[i] must have array sort [domain -> range_i]. The result will have array sort [domain -> range].

func (FuncDecl) String

func (f FuncDecl) String() string

String returns a string representation of f.

type Int

type Int value

Int is a symbolic value representing an integer with infinite precision.

Int implements Value.

func (Int) Add

func (l Int) Add(r ...Int) Int

Add returns the sum l + r[0] + r[1] + ...

func (Int) AsBigInt

func (lit Int) AsBigInt() (val *big.Int, isConst bool)

AsBigInt returns the value of lit as a math/big.Int. If lit is not a literal, it returns nil, false.

func (Int) AsInt64

func (lit Int) AsInt64() (val int64, isLiteral, ok bool)

AsInt64 returns the value of lit as an int64. If lit is not a literal, it returns 0, false, false. If lit is a literal, but its value cannot be represented as an int64, it returns 0, true, false.

func (Int) AsUint64

func (lit Int) AsUint64() (val uint64, isLiteral, ok bool)

AsUint64 is like AsInt64, but returns a uint64 and fails if lit cannot be represented as a uint64.

func (Int) Div

func (l Int) Div(r Int) Int

Div returns the floor of l / r.

If r is 0, the result is unconstrained.

Note that this differs from Go division: Go rounds toward zero (truncated division), whereas this rounds toward -inf.

func (Int) Eq

func (l Int) Eq(r Int) Bool

Eq returns a Value that is true if l and r are equal.

func (Int) Exp

func (l Int) Exp(r Int) Int

Exp returns lᶠ.

func (Int) GE

func (l Int) GE(r Int) Bool

GE returns l >= r.

func (Int) GT

func (l Int) GT(r Int) Bool

GT returns l > r.

func (Int) LE

func (l Int) LE(r Int) Bool

LE returns l <= r.

func (Int) LT

func (l Int) LT(r Int) Bool

LT returns l < r.

func (Int) Mod

func (l Int) Mod(r Int) Int

Mod returns modulus of l / r.

The sign of the result follows the sign of r.

func (Int) Mul

func (l Int) Mul(r ...Int) Int

Mul returns the product l * r[0] * r[1] * ...

func (Int) NE

func (l Int) NE(r Int) Bool

NE returns a Value that is true if l and r are not equal.

func (Int) Neg

func (l Int) Neg() Int

Neg returns -l.

func (Int) Rem

func (l Int) Rem(r Int) Int

Rem returns remainder of l / r.

The sign of the result follows the sign of l.

Note that this differs subtly from Go's remainder operator because this is based floored division rather than truncated division.

func (Int) Sub

func (l Int) Sub(r ...Int) Int

Sub returns l - r[0] - r[1] - ...

func (Int) ToBV

func (l Int) ToBV(bits int) BV

ToBV converts l to a bit-vector of width bits.

func (Int) ToReal

func (l Int) ToReal() Real

ToReal converts l to sort Real.

type Kind

type Kind int

Kind is a general category of sorts, such as int or array.

func (Kind) String

func (k Kind) String() string

String returns k as a string like "KindBool".

type Model

type Model struct {
	// contains filtered or unexported fields
}

A Model is a binding of constants that satisfies a set of formulas.

func (*Model) Eval

func (m *Model) Eval(val Value, completion bool) Value

Eval evaluates val using the concrete interpretations of constants and functions in model m.

If completion is true, it will assign interpretations for any constants or functions that currently don't have an interpretation in m. Otherwise, the resulting value may not be concrete.

Eval returns nil if val cannot be evaluated. This can happen if val contains a quantifier or is type-incorrect, or if m is a partial model (that is, the option MODEL_PARTIAL was set to true).

func (*Model) SortUniverse

func (m *Model) SortUniverse(s Sort) []Uninterpreted

SortUniverse returns the interpretation of s in m. s must be in the set returned by m.Sorts.

The interpretation of s is a finite set of distinct values of sort s.

func (*Model) Sorts

func (m *Model) Sorts() []Sort

Sorts returns the uninterpreted sorts that m assigns an interpretation to.

Each of these interpretations is a finite set of distinct values known as the "universe" of the sort. These values can be retrieved with SortUniverse.

func (*Model) String

func (m *Model) String() string

String returns a string representation of m.

type Real

type Real value

Real is a symbolic value representing a real number.

Real implements Value.

func (Real) Add

func (l Real) Add(r ...Real) Real

Add returns the sum l + r[0] + r[1] + ...

func (Real) Approx

func (lit Real) Approx(precision int) (lower, upper Real, isLiteralIrrational bool)

Approx approximates lit as two rational literals, where the difference between lower and upper is less than 1/10**precision. If lit is not an irrational literal, it returns false for isLiteralIrrational.

func (Real) AsBigRat

func (lit Real) AsBigRat() (val *big.Rat, isLiteralRational bool)

AsBigRat returns the value of lit as a math/big.Rat. If lit is not a literal or is not rational, it returns nil, false.

func (Real) AsRat

func (lit Real) AsRat() (numer, denom Int, isLiteralRational bool)

AsRat returns the value of lit as a numerator and denominator Int literals. If lit is not a literal or is not rational, it returns false for isLiteralRational. To round an arbitrary real to be rational, see method Real.Approx.

func (Real) Div

func (l Real) Div(r Real) Real

Div returns l / r.

If r is 0, the result is unconstrained.

func (Real) Eq

func (l Real) Eq(r Real) Bool

Eq returns a Value that is true if l and r are equal.

func (Real) Exp

func (l Real) Exp(r Real) Real

Exp returns lᶠ.

func (Real) GE

func (l Real) GE(r Real) Bool

GE returns l >= r.

func (Real) GT

func (l Real) GT(r Real) Bool

GT returns l > r.

func (Real) IsInt

func (l Real) IsInt() Bool

IsInt returns a Value that is true if l has no fractional part.

func (Real) LE

func (l Real) LE(r Real) Bool

LE returns l <= r.

func (Real) LT

func (l Real) LT(r Real) Bool

LT returns l < r.

func (Real) Mul

func (l Real) Mul(r ...Real) Real

Mul returns the product l * r[0] * r[1] * ...

func (Real) NE

func (l Real) NE(r Real) Bool

NE returns a Value that is true if l and r are not equal.

func (Real) Neg

func (l Real) Neg() Real

Neg returns -l.

func (Real) Sub

func (l Real) Sub(r ...Real) Real

Sub returns l - r[0] - r[1] - ...

func (Real) ToFloat

func (l Real) ToFloat(s Sort) Float

ToFloat converts l into a floating-point number.

If necessary, the result will be rounded according to the current rounding mode.

func (Real) ToFloatExp

func (l Real) ToFloatExp(exp Int, s Sort) Float

ToFloatExp converts l into a floating-point number l*2^exp.

If necessary, the result will be rounded according to the current rounding mode.

func (Real) ToInt

func (l Real) ToInt() Int

ToInt returns the floor of l as sort Int.

Note that this is not truncation. For example, ToInt(-1.3) is -2.

type RoundingMode

type RoundingMode int

RoundingMode represents a floating-point rounding mode.

The zero value of RoundingMode is RoundToNearestEven, which is the rounding mode in Go and the typical default rounding mode in floating-point math.

const (
	// RoundToNearestEven rounds floating-point results to the
	// nearest representable value. If the result is exactly
	// midway between two representable values, the even
	// representable value is chosen.
	RoundToNearestEven RoundingMode = iota

	// RoundToNearestAway rounds floating-point results to the
	// nearest representable value. If the result is exactly
	// midway between two representable values, the value with the
	// largest magnitude (away from 0) is chosen.
	RoundToNearestAway

	// RoundToPositive rounds floating-point results toward
	// positive infinity.
	RoundToPositive

	// RoundToPositive rounds floating-point results toward
	// negative infinity.
	RoundToNegative

	// RoundToZero rounds floating-point results toward zero.
	RoundToZero
)

type Solver

type Solver struct {
	// contains filtered or unexported fields
}

A Solver is a collection of predicates that can be checked for satisfiability.

These predicates form a stack that can be manipulated with Push/Pop.

func NewSolver

func NewSolver(ctx *Context) *Solver

NewSolver returns a new, empty solver.

func (*Solver) Assert

func (s *Solver) Assert(val Bool)

Assert adds val to the set of predicates that must be satisfied.

func (*Solver) Check

func (s *Solver) Check() (sat bool, err error)

Check determines whether the predicates in Solver s are satisfiable or unsatisfiable. If Z3 is unable to determine satisfiability, it returns an *ErrSatUnknown error.

func (*Solver) Model

func (s *Solver) Model() *Model

Model returns the model for the last Check. Model panics if Check has not been called or the last Check did not return true.

func (*Solver) Pop

func (s *Solver) Pop()

Pop removes assertions that were added since the matching Push.

func (*Solver) Push

func (s *Solver) Push()

Push saves the current state of the Solver so it can be restored with Pop.

func (*Solver) Reset

func (s *Solver) Reset()

Reset removes all assertions from the Solver and resets its stack.

func (*Solver) String

func (s *Solver) String() string

String returns a string representation of s.

type Sort

type Sort struct {
	// contains filtered or unexported fields
}

Sort represents the type of a symbolic value. A Sort can be a basic type such as "int" or "bool" or a parameterized type such as "bit-vector of 30 bits" or "array from int to bool".

func (Sort) AsAST

func (s Sort) AsAST() AST

AsAST returns the AST representation of s.

func (Sort) BVSize

func (s Sort) BVSize() int

BVSize returns the bit size of a bit-vector sort.

func (Sort) Context

func (s Sort) Context() *Context

Context returns the Context that created sort.

func (Sort) DomainAndRange

func (s Sort) DomainAndRange() (domain, range_ Sort)

DomainAndRange returns the domain and range of an array sort.

func (Sort) FloatSize

func (s Sort) FloatSize() (ebits, sbits int)

FloatSize returns the number of exponent and significand bits in s.

func (Sort) Kind

func (s Sort) Kind() Kind

Kind returns s's kind.

func (Sort) String

func (s Sort) String() string

String returns a string representation of s.

type Uninterpreted

type Uninterpreted value

Uninterpreted is a symbolic value with no interpretation. Uninterpreted values have identity—that is, they can be compared for equality—but have no inherent meaning otherwise.

Uninterpreted and FiniteDomain are similar, except that Uninterpreted values come from an unbounded universe.

Uninterpreted implements Value.

func (Uninterpreted) Eq

Eq returns a Value that is true if l and r are equal.

func (Uninterpreted) NE

NE returns a Value that is true if l and r are not equal.

type Value

type Value interface {
	// AsAST returns the abstract syntax tree underlying this
	// Value.
	AsAST() AST

	// Sort returns this value's sort.
	Sort() Sort

	// Context returns the Context that created this Value.
	Context() *Context

	// String returns an S-expression representation of this value.
	String() string
	// contains filtered or unexported methods
}

An Value is a symbolic value (a Z3 expression).

This package exports a concrete type for each different kind of value, such as Bool, BV, and Int. These concrete types provide methods for deriving other values.

Having separate types for each kind separates which methods can be applied to which kind of value and provides some level of static type safety. However, by no means does this fully capture Z3's type system, so dynamic type checking can still fail.

Directories

Path Synopsis
Package z3log exposes Z3's interaction log.
Package z3log exposes Z3's interaction log.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL