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

Jump to

Keyboard shortcuts

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