z3

package
v0.0.0-...-4675d5f Latest Latest
Warning

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

 Go to latest Published: Aug 9, 2022 License: BSD-3-Clause Imports: 8 Imported by: 5

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 

func (l Uninterpreted) Eq(r Uninterpreted) Bool

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

func (Uninterpreted) NE 

func (l Uninterpreted) NE(r Uninterpreted) Bool

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.

Source Files

View all Source files

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
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.