st

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: 3 Imported by: 0

Documentation

Overview

Package st provides symbolic equivalents of basic Go types.

Every value from this package can be either concrete or symbolic. Operations on concrete values always produce concrete values and are implemented as the underlying Go operations, so they're efficient. If one of the operands is symbolic, the result is generally symbolic.

Every type provided by this package has two fields: C and S. If the value is concrete, C is its concrete value. Otherwise, S is its symbolic value. This makes it convenient to write concrete literals. E.g., st.Int{C: 2} is a concrete "2".

Every type also has an "Any" constructor that returns an unconstrained symbolic value of that type. This value can be thought of as taking on every possible value of that type.

Every Go operation on a type has a corresponding method. Where possible, these follow the names from math/big. 

x + y	x.Add(y)
x - y	x.Sub(y)
x * y	x.Mul(y)
x / y	x.Div(y)	(does not panic on symbolic divide by 0)
x % y	x.Rem(y)

x & y	x.And(y)
x | y	x.Or(y)
x ^ y	x.Xor(y)
x << y	x.Lsh(y)
x >> y	x.Rsh(y)
x &^ y	x.AndNot(y)

x && y	x.And(y)	(Bool only; *not* short-circuiting)
x || y	x.Or(y)		(Bool only; *not* short-circuiting)

x == y	x.Eq(y)
x != y	x.NE(y)
x <  y	x.LT(y)
x <= y	x.LE(y)
x >  y	x.GT(y)
x >= y	x.GE(y)

-x	x.Neg()
^x	x.Not()
!x	x.Not() 	(Bool only)

For any pair of types T and U that support conversion in Go, T has a method ToU() that returns a U value.

TODO: Float, complex, and string types.

Index

Constants

This section is empty.

Variables

View Source 
var RealApproxDigits = 100

RealApproxDigits is the number of decimal digits an irrational real will be approximated to when evaluating it as a *big.Rat.

Functions

This section is empty.

Types

type Bool 

type Bool struct {
	C bool
	S z3.Bool
}

Bool implements symbolic bool values.

func AnyBool 

func AnyBool(ctx *z3.Context, name string) Bool

AnyBool returns an unconstrained symbolic Bool.

func (Bool) And 

func (x Bool) And(y Bool) Bool

func (Bool) Eq 

func (x Bool) Eq(y Bool) Bool

func (Bool) Eval 

func (x Bool) Eval(m *z3.Model) bool

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Bool) IsConcrete 

func (x Bool) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Bool) NE 

func (x Bool) NE(y Bool) Bool

func (Bool) Not 

func (x Bool) Not() Bool

func (Bool) Or 

func (x Bool) Or(y Bool) Bool

func (Bool) String 

func (x Bool) String() string

String returns x as a string.

type Int 

type Int struct {
	C int
	S z3.BV
}

Int implements symbolic int values.

func AnyInt 

func AnyInt(ctx *z3.Context, name string) Int

AnyInt returns an unconstrained symbolic Int.

func (Int) Add 

func (x Int) Add(y Int) Int

func (Int) And 

func (x Int) And(y Int) Int

func (Int) AndNot 

func (x Int) AndNot(y Int) Int

func (Int) Eq 

func (x Int) Eq(y Int) Bool

func (Int) Eval 

func (x Int) Eval(m *z3.Model) int

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Int) GE 

func (x Int) GE(y Int) Bool

func (Int) GT 

func (x Int) GT(y Int) Bool

func (Int) IsConcrete 

func (x Int) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Int) LE 

func (x Int) LE(y Int) Bool

func (Int) LT 

func (x Int) LT(y Int) Bool

func (Int) Lsh 

func (x Int) Lsh(y Uint64) Int

func (Int) Mul 

func (x Int) Mul(y Int) Int

func (Int) NE 

func (x Int) NE(y Int) Bool

func (Int) Neg 

func (x Int) Neg() Int

func (Int) Not 

func (x Int) Not() Int

func (Int) Or 

func (x Int) Or(y Int) Int

func (Int) Quo 

func (x Int) Quo(y Int) Int

func (Int) Rem 

func (x Int) Rem(y Int) Int

func (Int) Rsh 

func (x Int) Rsh(y Uint64) Int

func (Int) String 

func (x Int) String() string

String returns x as a string.

func (Int) Sub 

func (x Int) Sub(y Int) Int

func (Int) ToInt 

func (x Int) ToInt() Int

func (Int) ToInt16 

func (x Int) ToInt16() Int16

func (Int) ToInt32 

func (x Int) ToInt32() Int32

func (Int) ToInt64 

func (x Int) ToInt64() Int64

func (Int) ToInt8 

func (x Int) ToInt8() Int8

func (Int) ToUint 

func (x Int) ToUint() Uint

func (Int) ToUint16 

func (x Int) ToUint16() Uint16

func (Int) ToUint32 

func (x Int) ToUint32() Uint32

func (Int) ToUint64 

func (x Int) ToUint64() Uint64

func (Int) ToUint8 

func (x Int) ToUint8() Uint8

func (Int) ToUintptr 

func (x Int) ToUintptr() Uintptr

func (Int) Xor 

func (x Int) Xor(y Int) Int

type Int16 

type Int16 struct {
	C int16
	S z3.BV
}

Int16 implements symbolic int16 values.

func AnyInt16 

func AnyInt16(ctx *z3.Context, name string) Int16

AnyInt16 returns an unconstrained symbolic Int16.

func (Int16) Add 

func (x Int16) Add(y Int16) Int16

func (Int16) And 

func (x Int16) And(y Int16) Int16

func (Int16) AndNot 

func (x Int16) AndNot(y Int16) Int16

func (Int16) Eq 

func (x Int16) Eq(y Int16) Bool

func (Int16) Eval 

func (x Int16) Eval(m *z3.Model) int16

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Int16) GE 

func (x Int16) GE(y Int16) Bool

func (Int16) GT 

func (x Int16) GT(y Int16) Bool

func (Int16) IsConcrete 

func (x Int16) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Int16) LE 

func (x Int16) LE(y Int16) Bool

func (Int16) LT 

func (x Int16) LT(y Int16) Bool

func (Int16) Lsh 

func (x Int16) Lsh(y Uint64) Int16

func (Int16) Mul 

func (x Int16) Mul(y Int16) Int16

func (Int16) NE 

func (x Int16) NE(y Int16) Bool

func (Int16) Neg 

func (x Int16) Neg() Int16

func (Int16) Not 

func (x Int16) Not() Int16

func (Int16) Or 

func (x Int16) Or(y Int16) Int16

func (Int16) Quo 

func (x Int16) Quo(y Int16) Int16

func (Int16) Rem 

func (x Int16) Rem(y Int16) Int16

func (Int16) Rsh 

func (x Int16) Rsh(y Uint64) Int16

func (Int16) String 

func (x Int16) String() string

String returns x as a string.

func (Int16) Sub 

func (x Int16) Sub(y Int16) Int16

func (Int16) ToInt 

func (x Int16) ToInt() Int

func (Int16) ToInt16 

func (x Int16) ToInt16() Int16

func (Int16) ToInt32 

func (x Int16) ToInt32() Int32

func (Int16) ToInt64 

func (x Int16) ToInt64() Int64

func (Int16) ToInt8 

func (x Int16) ToInt8() Int8

func (Int16) ToUint 

func (x Int16) ToUint() Uint

func (Int16) ToUint16 

func (x Int16) ToUint16() Uint16

func (Int16) ToUint32 

func (x Int16) ToUint32() Uint32

func (Int16) ToUint64 

func (x Int16) ToUint64() Uint64

func (Int16) ToUint8 

func (x Int16) ToUint8() Uint8

func (Int16) ToUintptr 

func (x Int16) ToUintptr() Uintptr

func (Int16) Xor 

func (x Int16) Xor(y Int16) Int16

type Int32 

type Int32 struct {
	C int32
	S z3.BV
}

Int32 implements symbolic int32 values.

func AnyInt32 

func AnyInt32(ctx *z3.Context, name string) Int32

AnyInt32 returns an unconstrained symbolic Int32.

func (Int32) Add 

func (x Int32) Add(y Int32) Int32

func (Int32) And 

func (x Int32) And(y Int32) Int32

func (Int32) AndNot 

func (x Int32) AndNot(y Int32) Int32

func (Int32) Eq 

func (x Int32) Eq(y Int32) Bool

func (Int32) Eval 

func (x Int32) Eval(m *z3.Model) int32

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Int32) GE 

func (x Int32) GE(y Int32) Bool

func (Int32) GT 

func (x Int32) GT(y Int32) Bool

func (Int32) IsConcrete 

func (x Int32) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Int32) LE 

func (x Int32) LE(y Int32) Bool

func (Int32) LT 

func (x Int32) LT(y Int32) Bool

func (Int32) Lsh 

func (x Int32) Lsh(y Uint64) Int32

func (Int32) Mul 

func (x Int32) Mul(y Int32) Int32

func (Int32) NE 

func (x Int32) NE(y Int32) Bool

func (Int32) Neg 

func (x Int32) Neg() Int32

func (Int32) Not 

func (x Int32) Not() Int32

func (Int32) Or 

func (x Int32) Or(y Int32) Int32

func (Int32) Quo 

func (x Int32) Quo(y Int32) Int32

func (Int32) Rem 

func (x Int32) Rem(y Int32) Int32

func (Int32) Rsh 

func (x Int32) Rsh(y Uint64) Int32

func (Int32) String 

func (x Int32) String() string

String returns x as a string.

func (Int32) Sub 

func (x Int32) Sub(y Int32) Int32

func (Int32) ToInt 

func (x Int32) ToInt() Int

func (Int32) ToInt16 

func (x Int32) ToInt16() Int16

func (Int32) ToInt32 

func (x Int32) ToInt32() Int32

func (Int32) ToInt64 

func (x Int32) ToInt64() Int64

func (Int32) ToInt8 

func (x Int32) ToInt8() Int8

func (Int32) ToUint 

func (x Int32) ToUint() Uint

func (Int32) ToUint16 

func (x Int32) ToUint16() Uint16

func (Int32) ToUint32 

func (x Int32) ToUint32() Uint32

func (Int32) ToUint64 

func (x Int32) ToUint64() Uint64

func (Int32) ToUint8 

func (x Int32) ToUint8() Uint8

func (Int32) ToUintptr 

func (x Int32) ToUintptr() Uintptr

func (Int32) Xor 

func (x Int32) Xor(y Int32) Int32

type Int64 

type Int64 struct {
	C int64
	S z3.BV
}

Int64 implements symbolic int64 values.

func AnyInt64 

func AnyInt64(ctx *z3.Context, name string) Int64

AnyInt64 returns an unconstrained symbolic Int64.

func (Int64) Add 

func (x Int64) Add(y Int64) Int64

func (Int64) And 

func (x Int64) And(y Int64) Int64

func (Int64) AndNot 

func (x Int64) AndNot(y Int64) Int64

func (Int64) Eq 

func (x Int64) Eq(y Int64) Bool

func (Int64) Eval 

func (x Int64) Eval(m *z3.Model) int64

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Int64) GE 

func (x Int64) GE(y Int64) Bool

func (Int64) GT 

func (x Int64) GT(y Int64) Bool

func (Int64) IsConcrete 

func (x Int64) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Int64) LE 

func (x Int64) LE(y Int64) Bool

func (Int64) LT 

func (x Int64) LT(y Int64) Bool

func (Int64) Lsh 

func (x Int64) Lsh(y Uint64) Int64

func (Int64) Mul 

func (x Int64) Mul(y Int64) Int64

func (Int64) NE 

func (x Int64) NE(y Int64) Bool

func (Int64) Neg 

func (x Int64) Neg() Int64

func (Int64) Not 

func (x Int64) Not() Int64

func (Int64) Or 

func (x Int64) Or(y Int64) Int64

func (Int64) Quo 

func (x Int64) Quo(y Int64) Int64

func (Int64) Rem 

func (x Int64) Rem(y Int64) Int64

func (Int64) Rsh 

func (x Int64) Rsh(y Uint64) Int64

func (Int64) String 

func (x Int64) String() string

String returns x as a string.

func (Int64) Sub 

func (x Int64) Sub(y Int64) Int64

func (Int64) ToInt 

func (x Int64) ToInt() Int

func (Int64) ToInt16 

func (x Int64) ToInt16() Int16

func (Int64) ToInt32 

func (x Int64) ToInt32() Int32

func (Int64) ToInt64 

func (x Int64) ToInt64() Int64

func (Int64) ToInt8 

func (x Int64) ToInt8() Int8

func (Int64) ToUint 

func (x Int64) ToUint() Uint

func (Int64) ToUint16 

func (x Int64) ToUint16() Uint16

func (Int64) ToUint32 

func (x Int64) ToUint32() Uint32

func (Int64) ToUint64 

func (x Int64) ToUint64() Uint64

func (Int64) ToUint8 

func (x Int64) ToUint8() Uint8

func (Int64) ToUintptr 

func (x Int64) ToUintptr() Uintptr

func (Int64) Xor 

func (x Int64) Xor(y Int64) Int64

type Int8 

type Int8 struct {
	C int8
	S z3.BV
}

Int8 implements symbolic int8 values.

func AnyInt8 

func AnyInt8(ctx *z3.Context, name string) Int8

AnyInt8 returns an unconstrained symbolic Int8.

func (Int8) Add 

func (x Int8) Add(y Int8) Int8

func (Int8) And 

func (x Int8) And(y Int8) Int8

func (Int8) AndNot 

func (x Int8) AndNot(y Int8) Int8

func (Int8) Eq 

func (x Int8) Eq(y Int8) Bool

func (Int8) Eval 

func (x Int8) Eval(m *z3.Model) int8

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Int8) GE 

func (x Int8) GE(y Int8) Bool

func (Int8) GT 

func (x Int8) GT(y Int8) Bool

func (Int8) IsConcrete 

func (x Int8) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Int8) LE 

func (x Int8) LE(y Int8) Bool

func (Int8) LT 

func (x Int8) LT(y Int8) Bool

func (Int8) Lsh 

func (x Int8) Lsh(y Uint64) Int8

func (Int8) Mul 

func (x Int8) Mul(y Int8) Int8

func (Int8) NE 

func (x Int8) NE(y Int8) Bool

func (Int8) Neg 

func (x Int8) Neg() Int8

func (Int8) Not 

func (x Int8) Not() Int8

func (Int8) Or 

func (x Int8) Or(y Int8) Int8

func (Int8) Quo 

func (x Int8) Quo(y Int8) Int8

func (Int8) Rem 

func (x Int8) Rem(y Int8) Int8

func (Int8) Rsh 

func (x Int8) Rsh(y Uint64) Int8

func (Int8) String 

func (x Int8) String() string

String returns x as a string.

func (Int8) Sub 

func (x Int8) Sub(y Int8) Int8

func (Int8) ToInt 

func (x Int8) ToInt() Int

func (Int8) ToInt16 

func (x Int8) ToInt16() Int16

func (Int8) ToInt32 

func (x Int8) ToInt32() Int32

func (Int8) ToInt64 

func (x Int8) ToInt64() Int64

func (Int8) ToInt8 

func (x Int8) ToInt8() Int8

func (Int8) ToUint 

func (x Int8) ToUint() Uint

func (Int8) ToUint16 

func (x Int8) ToUint16() Uint16

func (Int8) ToUint32 

func (x Int8) ToUint32() Uint32

func (Int8) ToUint64 

func (x Int8) ToUint64() Uint64

func (Int8) ToUint8 

func (x Int8) ToUint8() Uint8

func (Int8) ToUintptr 

func (x Int8) ToUintptr() Uintptr

func (Int8) Xor 

func (x Int8) Xor(y Int8) Int8

type Integer 

type Integer struct {
	C *big.Int
	S z3.Int
}

Integer implements symbolic *big.Int values.

func AnyInteger 

func AnyInteger(ctx *z3.Context, name string) Integer

AnyInteger returns an unconstrained symbolic Integer.

func (Integer) Add 

func (x Integer) Add(y Integer) Integer

func (Integer) Eq 

func (x Integer) Eq(y Integer) Bool

func (Integer) Eval 

func (x Integer) Eval(m *z3.Model) *big.Int

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Integer) GE 

func (x Integer) GE(y Integer) Bool

func (Integer) GT 

func (x Integer) GT(y Integer) Bool

func (Integer) IsConcrete 

func (x Integer) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Integer) LE 

func (x Integer) LE(y Integer) Bool

func (Integer) LT 

func (x Integer) LT(y Integer) Bool

func (Integer) Mul 

func (x Integer) Mul(y Integer) Integer

func (Integer) NE 

func (x Integer) NE(y Integer) Bool

func (Integer) Neg 

func (x Integer) Neg() Integer

func (Integer) Quo 

func (x Integer) Quo(y Integer) Integer

func (Integer) Rem 

func (x Integer) Rem(y Integer) Integer

func (Integer) String 

func (x Integer) String() string

String returns x as a string.

func (Integer) Sub 

func (x Integer) Sub(y Integer) Integer

type Real 

type Real struct {
	C *big.Rat
	S z3.Real
}

Real implements symbolic *big.Rat values.

func AnyReal 

func AnyReal(ctx *z3.Context, name string) Real

AnyReal returns an unconstrained symbolic Real.

func (Real) Add 

func (x Real) Add(y Real) Real

func (Real) Eq 

func (x Real) Eq(y Real) Bool

func (Real) Eval 

func (x Real) Eval(m *z3.Model) *big.Rat

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Real) GE 

func (x Real) GE(y Real) Bool

func (Real) GT 

func (x Real) GT(y Real) Bool

func (Real) IsConcrete 

func (x Real) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Real) LE 

func (x Real) LE(y Real) Bool

func (Real) LT 

func (x Real) LT(y Real) Bool

func (Real) Mul 

func (x Real) Mul(y Real) Real

func (Real) NE 

func (x Real) NE(y Real) Bool

func (Real) Neg 

func (x Real) Neg() Real

func (Real) Quo 

func (x Real) Quo(y Real) Real

func (Real) String 

func (x Real) String() string

String returns x as a string.

func (Real) Sub 

func (x Real) Sub(y Real) Real

type Uint 

type Uint struct {
	C uint
	S z3.BV
}

Uint implements symbolic uint values.

func AnyUint 

func AnyUint(ctx *z3.Context, name string) Uint

AnyUint returns an unconstrained symbolic Uint.

func (Uint) Add 

func (x Uint) Add(y Uint) Uint

func (Uint) And 

func (x Uint) And(y Uint) Uint

func (Uint) AndNot 

func (x Uint) AndNot(y Uint) Uint

func (Uint) Eq 

func (x Uint) Eq(y Uint) Bool

func (Uint) Eval 

func (x Uint) Eval(m *z3.Model) uint

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uint) GE 

func (x Uint) GE(y Uint) Bool

func (Uint) GT 

func (x Uint) GT(y Uint) Bool

func (Uint) IsConcrete 

func (x Uint) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uint) LE 

func (x Uint) LE(y Uint) Bool

func (Uint) LT 

func (x Uint) LT(y Uint) Bool

func (Uint) Lsh 

func (x Uint) Lsh(y Uint64) Uint

func (Uint) Mul 

func (x Uint) Mul(y Uint) Uint

func (Uint) NE 

func (x Uint) NE(y Uint) Bool

func (Uint) Neg 

func (x Uint) Neg() Uint

func (Uint) Not 

func (x Uint) Not() Uint

func (Uint) Or 

func (x Uint) Or(y Uint) Uint

func (Uint) Quo 

func (x Uint) Quo(y Uint) Uint

func (Uint) Rem 

func (x Uint) Rem(y Uint) Uint

func (Uint) Rsh 

func (x Uint) Rsh(y Uint64) Uint

func (Uint) String 

func (x Uint) String() string

String returns x as a string.

func (Uint) Sub 

func (x Uint) Sub(y Uint) Uint

func (Uint) ToInt 

func (x Uint) ToInt() Int

func (Uint) ToInt16 

func (x Uint) ToInt16() Int16

func (Uint) ToInt32 

func (x Uint) ToInt32() Int32

func (Uint) ToInt64 

func (x Uint) ToInt64() Int64

func (Uint) ToInt8 

func (x Uint) ToInt8() Int8

func (Uint) ToUint 

func (x Uint) ToUint() Uint

func (Uint) ToUint16 

func (x Uint) ToUint16() Uint16

func (Uint) ToUint32 

func (x Uint) ToUint32() Uint32

func (Uint) ToUint64 

func (x Uint) ToUint64() Uint64

func (Uint) ToUint8 

func (x Uint) ToUint8() Uint8

func (Uint) ToUintptr 

func (x Uint) ToUintptr() Uintptr

func (Uint) Xor 

func (x Uint) Xor(y Uint) Uint

type Uint16 

type Uint16 struct {
	C uint16
	S z3.BV
}

Uint16 implements symbolic uint16 values.

func AnyUint16 

func AnyUint16(ctx *z3.Context, name string) Uint16

AnyUint16 returns an unconstrained symbolic Uint16.

func (Uint16) Add 

func (x Uint16) Add(y Uint16) Uint16

func (Uint16) And 

func (x Uint16) And(y Uint16) Uint16

func (Uint16) AndNot 

func (x Uint16) AndNot(y Uint16) Uint16

func (Uint16) Eq 

func (x Uint16) Eq(y Uint16) Bool

func (Uint16) Eval 

func (x Uint16) Eval(m *z3.Model) uint16

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uint16) GE 

func (x Uint16) GE(y Uint16) Bool

func (Uint16) GT 

func (x Uint16) GT(y Uint16) Bool

func (Uint16) IsConcrete 

func (x Uint16) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uint16) LE 

func (x Uint16) LE(y Uint16) Bool

func (Uint16) LT 

func (x Uint16) LT(y Uint16) Bool

func (Uint16) Lsh 

func (x Uint16) Lsh(y Uint64) Uint16

func (Uint16) Mul 

func (x Uint16) Mul(y Uint16) Uint16

func (Uint16) NE 

func (x Uint16) NE(y Uint16) Bool

func (Uint16) Neg 

func (x Uint16) Neg() Uint16

func (Uint16) Not 

func (x Uint16) Not() Uint16

func (Uint16) Or 

func (x Uint16) Or(y Uint16) Uint16

func (Uint16) Quo 

func (x Uint16) Quo(y Uint16) Uint16

func (Uint16) Rem 

func (x Uint16) Rem(y Uint16) Uint16

func (Uint16) Rsh 

func (x Uint16) Rsh(y Uint64) Uint16

func (Uint16) String 

func (x Uint16) String() string

String returns x as a string.

func (Uint16) Sub 

func (x Uint16) Sub(y Uint16) Uint16

func (Uint16) ToInt 

func (x Uint16) ToInt() Int

func (Uint16) ToInt16 

func (x Uint16) ToInt16() Int16

func (Uint16) ToInt32 

func (x Uint16) ToInt32() Int32

func (Uint16) ToInt64 

func (x Uint16) ToInt64() Int64

func (Uint16) ToInt8 

func (x Uint16) ToInt8() Int8

func (Uint16) ToUint 

func (x Uint16) ToUint() Uint

func (Uint16) ToUint16 

func (x Uint16) ToUint16() Uint16

func (Uint16) ToUint32 

func (x Uint16) ToUint32() Uint32

func (Uint16) ToUint64 

func (x Uint16) ToUint64() Uint64

func (Uint16) ToUint8 

func (x Uint16) ToUint8() Uint8

func (Uint16) ToUintptr 

func (x Uint16) ToUintptr() Uintptr

func (Uint16) Xor 

func (x Uint16) Xor(y Uint16) Uint16

type Uint32 

type Uint32 struct {
	C uint32
	S z3.BV
}

Uint32 implements symbolic uint32 values.

func AnyUint32 

func AnyUint32(ctx *z3.Context, name string) Uint32

AnyUint32 returns an unconstrained symbolic Uint32.

func (Uint32) Add 

func (x Uint32) Add(y Uint32) Uint32

func (Uint32) And 

func (x Uint32) And(y Uint32) Uint32

func (Uint32) AndNot 

func (x Uint32) AndNot(y Uint32) Uint32

func (Uint32) Eq 

func (x Uint32) Eq(y Uint32) Bool

func (Uint32) Eval 

func (x Uint32) Eval(m *z3.Model) uint32

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uint32) GE 

func (x Uint32) GE(y Uint32) Bool

func (Uint32) GT 

func (x Uint32) GT(y Uint32) Bool

func (Uint32) IsConcrete 

func (x Uint32) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uint32) LE 

func (x Uint32) LE(y Uint32) Bool

func (Uint32) LT 

func (x Uint32) LT(y Uint32) Bool

func (Uint32) Lsh 

func (x Uint32) Lsh(y Uint64) Uint32

func (Uint32) Mul 

func (x Uint32) Mul(y Uint32) Uint32

func (Uint32) NE 

func (x Uint32) NE(y Uint32) Bool

func (Uint32) Neg 

func (x Uint32) Neg() Uint32

func (Uint32) Not 

func (x Uint32) Not() Uint32

func (Uint32) Or 

func (x Uint32) Or(y Uint32) Uint32

func (Uint32) Quo 

func (x Uint32) Quo(y Uint32) Uint32

func (Uint32) Rem 

func (x Uint32) Rem(y Uint32) Uint32

func (Uint32) Rsh 

func (x Uint32) Rsh(y Uint64) Uint32

func (Uint32) String 

func (x Uint32) String() string

String returns x as a string.

func (Uint32) Sub 

func (x Uint32) Sub(y Uint32) Uint32

func (Uint32) ToInt 

func (x Uint32) ToInt() Int

func (Uint32) ToInt16 

func (x Uint32) ToInt16() Int16

func (Uint32) ToInt32 

func (x Uint32) ToInt32() Int32

func (Uint32) ToInt64 

func (x Uint32) ToInt64() Int64

func (Uint32) ToInt8 

func (x Uint32) ToInt8() Int8

func (Uint32) ToUint 

func (x Uint32) ToUint() Uint

func (Uint32) ToUint16 

func (x Uint32) ToUint16() Uint16

func (Uint32) ToUint32 

func (x Uint32) ToUint32() Uint32

func (Uint32) ToUint64 

func (x Uint32) ToUint64() Uint64

func (Uint32) ToUint8 

func (x Uint32) ToUint8() Uint8

func (Uint32) ToUintptr 

func (x Uint32) ToUintptr() Uintptr

func (Uint32) Xor 

func (x Uint32) Xor(y Uint32) Uint32

type Uint64 

type Uint64 struct {
	C uint64
	S z3.BV
}

Uint64 implements symbolic uint64 values.

func AnyUint64 

func AnyUint64(ctx *z3.Context, name string) Uint64

AnyUint64 returns an unconstrained symbolic Uint64.

func (Uint64) Add 

func (x Uint64) Add(y Uint64) Uint64

func (Uint64) And 

func (x Uint64) And(y Uint64) Uint64

func (Uint64) AndNot 

func (x Uint64) AndNot(y Uint64) Uint64

func (Uint64) Eq 

func (x Uint64) Eq(y Uint64) Bool

func (Uint64) Eval 

func (x Uint64) Eval(m *z3.Model) uint64

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uint64) GE 

func (x Uint64) GE(y Uint64) Bool

func (Uint64) GT 

func (x Uint64) GT(y Uint64) Bool

func (Uint64) IsConcrete 

func (x Uint64) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uint64) LE 

func (x Uint64) LE(y Uint64) Bool

func (Uint64) LT 

func (x Uint64) LT(y Uint64) Bool

func (Uint64) Lsh 

func (x Uint64) Lsh(y Uint64) Uint64

func (Uint64) Mul 

func (x Uint64) Mul(y Uint64) Uint64

func (Uint64) NE 

func (x Uint64) NE(y Uint64) Bool

func (Uint64) Neg 

func (x Uint64) Neg() Uint64

func (Uint64) Not 

func (x Uint64) Not() Uint64

func (Uint64) Or 

func (x Uint64) Or(y Uint64) Uint64

func (Uint64) Quo 

func (x Uint64) Quo(y Uint64) Uint64

func (Uint64) Rem 

func (x Uint64) Rem(y Uint64) Uint64

func (Uint64) Rsh 

func (x Uint64) Rsh(y Uint64) Uint64

func (Uint64) String 

func (x Uint64) String() string

String returns x as a string.

func (Uint64) Sub 

func (x Uint64) Sub(y Uint64) Uint64

func (Uint64) ToInt 

func (x Uint64) ToInt() Int

func (Uint64) ToInt16 

func (x Uint64) ToInt16() Int16

func (Uint64) ToInt32 

func (x Uint64) ToInt32() Int32

func (Uint64) ToInt64 

func (x Uint64) ToInt64() Int64

func (Uint64) ToInt8 

func (x Uint64) ToInt8() Int8

func (Uint64) ToUint 

func (x Uint64) ToUint() Uint

func (Uint64) ToUint16 

func (x Uint64) ToUint16() Uint16

func (Uint64) ToUint32 

func (x Uint64) ToUint32() Uint32

func (Uint64) ToUint64 

func (x Uint64) ToUint64() Uint64

func (Uint64) ToUint8 

func (x Uint64) ToUint8() Uint8

func (Uint64) ToUintptr 

func (x Uint64) ToUintptr() Uintptr

func (Uint64) Xor 

func (x Uint64) Xor(y Uint64) Uint64

type Uint8 

type Uint8 struct {
	C uint8
	S z3.BV
}

Uint8 implements symbolic uint8 values.

func AnyUint8 

func AnyUint8(ctx *z3.Context, name string) Uint8

AnyUint8 returns an unconstrained symbolic Uint8.

func (Uint8) Add 

func (x Uint8) Add(y Uint8) Uint8

func (Uint8) And 

func (x Uint8) And(y Uint8) Uint8

func (Uint8) AndNot 

func (x Uint8) AndNot(y Uint8) Uint8

func (Uint8) Eq 

func (x Uint8) Eq(y Uint8) Bool

func (Uint8) Eval 

func (x Uint8) Eval(m *z3.Model) uint8

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uint8) GE 

func (x Uint8) GE(y Uint8) Bool

func (Uint8) GT 

func (x Uint8) GT(y Uint8) Bool

func (Uint8) IsConcrete 

func (x Uint8) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uint8) LE 

func (x Uint8) LE(y Uint8) Bool

func (Uint8) LT 

func (x Uint8) LT(y Uint8) Bool

func (Uint8) Lsh 

func (x Uint8) Lsh(y Uint64) Uint8

func (Uint8) Mul 

func (x Uint8) Mul(y Uint8) Uint8

func (Uint8) NE 

func (x Uint8) NE(y Uint8) Bool

func (Uint8) Neg 

func (x Uint8) Neg() Uint8

func (Uint8) Not 

func (x Uint8) Not() Uint8

func (Uint8) Or 

func (x Uint8) Or(y Uint8) Uint8

func (Uint8) Quo 

func (x Uint8) Quo(y Uint8) Uint8

func (Uint8) Rem 

func (x Uint8) Rem(y Uint8) Uint8

func (Uint8) Rsh 

func (x Uint8) Rsh(y Uint64) Uint8

func (Uint8) String 

func (x Uint8) String() string

String returns x as a string.

func (Uint8) Sub 

func (x Uint8) Sub(y Uint8) Uint8

func (Uint8) ToInt 

func (x Uint8) ToInt() Int

func (Uint8) ToInt16 

func (x Uint8) ToInt16() Int16

func (Uint8) ToInt32 

func (x Uint8) ToInt32() Int32

func (Uint8) ToInt64 

func (x Uint8) ToInt64() Int64

func (Uint8) ToInt8 

func (x Uint8) ToInt8() Int8

func (Uint8) ToUint 

func (x Uint8) ToUint() Uint

func (Uint8) ToUint16 

func (x Uint8) ToUint16() Uint16

func (Uint8) ToUint32 

func (x Uint8) ToUint32() Uint32

func (Uint8) ToUint64 

func (x Uint8) ToUint64() Uint64

func (Uint8) ToUint8 

func (x Uint8) ToUint8() Uint8

func (Uint8) ToUintptr 

func (x Uint8) ToUintptr() Uintptr

func (Uint8) Xor 

func (x Uint8) Xor(y Uint8) Uint8

type Uintptr 

type Uintptr struct {
	C uintptr
	S z3.BV
}

Uintptr implements symbolic uintptr values.

func AnyUintptr 

func AnyUintptr(ctx *z3.Context, name string) Uintptr

AnyUintptr returns an unconstrained symbolic Uintptr.

func (Uintptr) Add 

func (x Uintptr) Add(y Uintptr) Uintptr

func (Uintptr) And 

func (x Uintptr) And(y Uintptr) Uintptr

func (Uintptr) AndNot 

func (x Uintptr) AndNot(y Uintptr) Uintptr

func (Uintptr) Eq 

func (x Uintptr) Eq(y Uintptr) Bool

func (Uintptr) Eval 

func (x Uintptr) Eval(m *z3.Model) uintptr

Eval returns x's concrete value in model m. This also evaluates x with model completion.

func (Uintptr) GE 

func (x Uintptr) GE(y Uintptr) Bool

func (Uintptr) GT 

func (x Uintptr) GT(y Uintptr) Bool

func (Uintptr) IsConcrete 

func (x Uintptr) IsConcrete() bool

IsConcrete returns true if x is concrete.

func (Uintptr) LE 

func (x Uintptr) LE(y Uintptr) Bool

func (Uintptr) LT 

func (x Uintptr) LT(y Uintptr) Bool

func (Uintptr) Lsh 

func (x Uintptr) Lsh(y Uint64) Uintptr

func (Uintptr) Mul 

func (x Uintptr) Mul(y Uintptr) Uintptr

func (Uintptr) NE 

func (x Uintptr) NE(y Uintptr) Bool

func (Uintptr) Neg 

func (x Uintptr) Neg() Uintptr

func (Uintptr) Not 

func (x Uintptr) Not() Uintptr

func (Uintptr) Or 

func (x Uintptr) Or(y Uintptr) Uintptr

func (Uintptr) Quo 

func (x Uintptr) Quo(y Uintptr) Uintptr

func (Uintptr) Rem 

func (x Uintptr) Rem(y Uintptr) Uintptr

func (Uintptr) Rsh 

func (x Uintptr) Rsh(y Uint64) Uintptr

func (Uintptr) String 

func (x Uintptr) String() string

String returns x as a string.

func (Uintptr) Sub 

func (x Uintptr) Sub(y Uintptr) Uintptr

func (Uintptr) ToInt 

func (x Uintptr) ToInt() Int

func (Uintptr) ToInt16 

func (x Uintptr) ToInt16() Int16

func (Uintptr) ToInt32 

func (x Uintptr) ToInt32() Int32

func (Uintptr) ToInt64 

func (x Uintptr) ToInt64() Int64

func (Uintptr) ToInt8 

func (x Uintptr) ToInt8() Int8

func (Uintptr) ToUint 

func (x Uintptr) ToUint() Uint

func (Uintptr) ToUint16 

func (x Uintptr) ToUint16() Uint16

func (Uintptr) ToUint32 

func (x Uintptr) ToUint32() Uint32

func (Uintptr) ToUint64 

func (x Uintptr) ToUint64() Uint64

func (Uintptr) ToUint8 

func (x Uintptr) ToUint8() Uint8

func (Uintptr) ToUintptr 

func (x Uintptr) ToUintptr() Uintptr

func (Uintptr) Xor 

func (x Uintptr) Xor(y Uintptr) Uintptr

Source Files

View all Source files

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.