smt

package
v0.1.0 Latest Latest
Warning

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

 Go to latest Published: Sep 9, 2022 License: MIT Imports: 4 Imported by: 0

Documentation

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type ArrayInt32 

type ArrayInt32 struct {
	S SymArrayInt32
	// contains filtered or unexported fields
}

func (ArrayInt32) InBounds 

func (a ArrayInt32) InBounds(idx Int32, s *Solver) bool

func (ArrayInt32) Read 

func (a ArrayInt32) Read(idx Int32, s *Solver) Int32

func (*ArrayInt32) Write 

func (a *ArrayInt32) Write(idx, val Int32, s *Solver)

func (*ArrayInt32) WriteInitial 

func (a *ArrayInt32) WriteInitial(idx, val Int32, s *Solver)

type Bool 

type Bool struct {
	C bool
	S SymBool
}

func (Bool) Concrete 

func (a Bool) Concrete() bool

func (Bool) Not 

func (a Bool) Not(s *Solver) Bool

func (Bool) Sym 

func (a Bool) Sym(s *Solver) SymBool

type CheckResult 

type CheckResult byte
const (
	Sat CheckResult = iota
	Unsat
	Unknown
)

type Int16 

type Int16 struct {
	C int16
	S SymInt16
}

func (Int16) Concrete 

func (a Int16) Concrete() bool

func (Int16) ToInt32s 

func (a Int16) ToInt32s(s *Solver) Int32

func (Int16) ToInt32z 

func (a Int16) ToInt32z(s *Solver) Int32

type Int32 

type Int32 struct {
	C int32
	S SymInt32
}

func (Int32) Add 

func (a Int32) Add(b Int32, s *Solver) Int32

func (Int32) And 

func (a Int32) And(b Int32, s *Solver) Int32

func (Int32) Concrete 

func (a Int32) Concrete() bool

func (Int32) Div 

func (a Int32) Div(b Int32, s *Solver) Int32

func (Int32) Divu 

func (a Int32) Divu(b Int32, s *Solver) Int32

func (Int32) Eqb 

func (a Int32) Eqb(b Int32, s *Solver) Bool

func (Int32) Eqz 

func (a Int32) Eqz(s *Solver) Bool

func (Int32) Mul 

func (a Int32) Mul(b Int32, s *Solver) Int32

func (Int32) NEqb 

func (a Int32) NEqb(b Int32, s *Solver) Bool

func (Int32) NEqz 

func (a Int32) NEqz(s *Solver) Bool

func (Int32) Not 

func (a Int32) Not(s *Solver) Int32

func (Int32) Or 

func (a Int32) Or(b Int32, s *Solver) Int32

func (Int32) Rem 

func (a Int32) Rem(b Int32, s *Solver) Int32

func (Int32) Remu 

func (a Int32) Remu(b Int32, s *Solver) Int32

func (Int32) Sgeb 

func (a Int32) Sgeb(b Int32, s *Solver) Bool

func (Int32) Sll 

func (a Int32) Sll(b Int32, s *Solver) Int32

func (Int32) Slt 

func (a Int32) Slt(b Int32, s *Solver) Int32

func (Int32) Sltb 

func (a Int32) Sltb(b Int32, s *Solver) Bool

func (Int32) Sra 

func (a Int32) Sra(b Int32, s *Solver) Int32

func (Int32) Srl 

func (a Int32) Srl(b Int32, s *Solver) Int32

func (Int32) String 

func (a Int32) String() string

func (Int32) Sub 

func (a Int32) Sub(b Int32, s *Solver) Int32

func (Int32) Sym 

func (a Int32) Sym(s *Solver) SymInt32

func (Int32) ToInt16 

func (a Int32) ToInt16(s *Solver) Int16

func (Int32) ToInt64s 

func (a Int32) ToInt64s(s *Solver) Int64

func (Int32) ToInt64z 

func (a Int32) ToInt64z(s *Solver) Int64

func (Int32) ToInt8 

func (a Int32) ToInt8(s *Solver) Int8

func (Int32) Ugeb 

func (a Int32) Ugeb(b Int32, s *Solver) Bool

func (Int32) Ult 

func (a Int32) Ult(b Int32, s *Solver) Int32

func (Int32) Ultb 

func (a Int32) Ultb(b Int32, s *Solver) Bool

func (Int32) Xor 

func (a Int32) Xor(b Int32, s *Solver) Int32

type Int64 

type Int64 struct {
	C int64
	S SymInt64
}

func (Int64) Concrete 

func (a Int64) Concrete() bool

func (Int64) Lower32 

func (a Int64) Lower32(s *Solver) Int32

func (Int64) Mul 

func (a Int64) Mul(b Int64, s *Solver) Int64

func (Int64) Sym 

func (a Int64) Sym(s *Solver) SymInt64

func (Int64) Upper32 

func (a Int64) Upper32(s *Solver) Int32

type Int8 

type Int8 struct {
	C int8
	S SymInt8
}

func (Int8) Concrete 

func (a Int8) Concrete() bool

func (Int8) ToInt32s 

func (a Int8) ToInt32s(s *Solver) Int32

func (Int8) ToInt32z 

func (a Int8) ToInt32z(s *Solver) Int32

type Model 

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

func (Model) Eval 

func (m Model) Eval(a Int32) int32

type Solver 

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

func NewSolver 

func NewSolver() *Solver

func (*Solver) AnyArrayInt32 

func (s *Solver) AnyArrayInt32(base, length uint32) ArrayInt32

func (*Solver) AnyInt32 

func (s *Solver) AnyInt32() Int32

func (*Solver) Assert 

func (s *Solver) Assert(b Bool)

func (*Solver) Check 

func (s *Solver) Check(model bool) CheckResult

func (*Solver) Model 

func (s *Solver) Model() Model

func (*Solver) Pop 

func (s *Solver) Pop()

func (*Solver) Push 

func (s *Solver) Push()

func (*Solver) String 

func (s *Solver) String() string

func (*Solver) ToSymBool 

func (s *Solver) ToSymBool(c bool) SymBool

func (*Solver) ToSymInt32 

func (s *Solver) ToSymInt32(c int32) SymInt32

func (*Solver) ToSymInt64 

func (s *Solver) ToSymInt64(c int64) SymInt64

type SymArrayInt32 

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

func (SymArrayInt32) Select 

func (a SymArrayInt32) Select(idx SymInt32, s *Solver) SymInt32

func (SymArrayInt32) Store 

func (a SymArrayInt32) Store(idx SymInt32, val SymInt32, s *Solver) SymArrayInt32

func (SymArrayInt32) StoreWithSelect 

func (a SymArrayInt32) StoreWithSelect(idx SymInt32, val SymInt32, s *Solver) SymArrayInt32

type SymBool 

type SymBool struct {
	BV *C.BoolectorNode
}

func (SymBool) Not 

func (a SymBool) Not(s *Solver) SymBool

func (SymBool) Valid 

func (a SymBool) Valid() bool

type SymInt16 

type SymInt16 struct {
	BV *C.BoolectorNode
}

func (SymInt16) ToInt32s 

func (a SymInt16) ToInt32s(s *Solver) SymInt32

func (SymInt16) ToInt32z 

func (a SymInt16) ToInt32z(s *Solver) SymInt32

func (SymInt16) Valid 

func (a SymInt16) Valid() bool

type SymInt32 

type SymInt32 struct {
	BV *C.BoolectorNode
}

func (SymInt32) Add 

func (a SymInt32) Add(b SymInt32, s *Solver) SymInt32

func (SymInt32) And 

func (a SymInt32) And(b SymInt32, s *Solver) SymInt32

func (SymInt32) Div 

func (a SymInt32) Div(b SymInt32, s *Solver) SymInt32

func (SymInt32) Divu 

func (a SymInt32) Divu(b SymInt32, s *Solver) SymInt32

func (SymInt32) Eqb 

func (a SymInt32) Eqb(b SymInt32, s *Solver) SymBool

func (SymInt32) Eqz 

func (a SymInt32) Eqz(s *Solver) SymBool

func (SymInt32) Mul 

func (a SymInt32) Mul(b SymInt32, s *Solver) SymInt32

func (SymInt32) NEqb 

func (a SymInt32) NEqb(b SymInt32, s *Solver) SymBool

func (SymInt32) NEqz 

func (a SymInt32) NEqz(s *Solver) SymBool

func (SymInt32) Not 

func (a SymInt32) Not(s *Solver) SymInt32

func (SymInt32) Or 

func (a SymInt32) Or(b SymInt32, s *Solver) SymInt32

func (SymInt32) Rem 

func (a SymInt32) Rem(b SymInt32, s *Solver) SymInt32

func (SymInt32) Remu 

func (a SymInt32) Remu(b SymInt32, s *Solver) SymInt32

func (SymInt32) Sgeb 

func (a SymInt32) Sgeb(b SymInt32, s *Solver) SymBool

func (SymInt32) Sll 

func (a SymInt32) Sll(b SymInt32, s *Solver) SymInt32

func (SymInt32) Slt 

func (a SymInt32) Slt(b SymInt32, s *Solver) SymInt32

func (SymInt32) Sltb 

func (a SymInt32) Sltb(b SymInt32, s *Solver) SymBool

func (SymInt32) Sra 

func (a SymInt32) Sra(b SymInt32, s *Solver) SymInt32

func (SymInt32) Srl 

func (a SymInt32) Srl(b SymInt32, s *Solver) SymInt32

func (SymInt32) Sub 

func (a SymInt32) Sub(b SymInt32, s *Solver) SymInt32

func (SymInt32) ToInt16 

func (a SymInt32) ToInt16(s *Solver) SymInt16

func (SymInt32) ToInt64s 

func (a SymInt32) ToInt64s(s *Solver) SymInt64

func (SymInt32) ToInt64z 

func (a SymInt32) ToInt64z(s *Solver) SymInt64

func (SymInt32) ToInt8 

func (a SymInt32) ToInt8(s *Solver) SymInt8

func (SymInt32) Ugeb 

func (a SymInt32) Ugeb(b SymInt32, s *Solver) SymBool

func (SymInt32) Ult 

func (a SymInt32) Ult(b SymInt32, s *Solver) SymInt32

func (SymInt32) Ultb 

func (a SymInt32) Ultb(b SymInt32, s *Solver) SymBool

func (SymInt32) Valid 

func (a SymInt32) Valid() bool

func (SymInt32) Xor 

func (a SymInt32) Xor(b SymInt32, s *Solver) SymInt32

type SymInt64 

type SymInt64 struct {
	BV *C.BoolectorNode
}

func (SymInt64) Lower32 

func (a SymInt64) Lower32(s *Solver) SymInt32

func (SymInt64) Mul 

func (a SymInt64) Mul(b SymInt64, s *Solver) SymInt64

func (SymInt64) Upper32 

func (a SymInt64) Upper32(s *Solver) SymInt32

func (SymInt64) Valid 

func (a SymInt64) Valid() bool

type SymInt8 

type SymInt8 struct {
	BV *C.BoolectorNode
}

func (SymInt8) ToInt32s 

func (a SymInt8) ToInt32s(s *Solver) SymInt32

func (SymInt8) ToInt32z 

func (a SymInt8) ToInt32z(s *Solver) SymInt32

func (SymInt8) Valid 

func (a SymInt8) Valid() bool

Source Files

View all Source files

Directories

Path Synopsis
z3
Package z3 checks the satisfiability of logical formulas.
 Package z3 checks the satisfiability of logical formulas.
z3log
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.