smt

Documentation

Index

• Variables
• func IsSymbol(sexp Sexp, id string) bool
• type App
• type BitVec
• type BitVecSort
• type Const
• type Identifier
• type Int
• type Let
• type Parser
  • func NewParser(r io.Reader) *Parser
  • func (p *Parser) Read() (Sexp, error)
• type SBitVec
  • func (s *SBitVec) String() string
• type SInt
  • func (s *SInt) String() string
• type SKeyword
  • func (s *SKeyword) String() string
• type SList
  • func (s *SList) String() string
• type SString
  • func (s *SString) String() string
• type SSymbol
  • func (s *SSymbol) String() string
• type Satisfiable
  • func (i Satisfiable) String() string
• type Sexp
  • func IdToSexp(id Identifier) Sexp
  • func SortToSexp(sort Sort) Sexp
  • func TermToSexp(term Term) Sexp
• type Solver
• type Sort
• type SortApp
• type SortName
• type String
• type Term
  • func Add(a, b Term) Term
  • func And(a, b Term) Term
  • func BVAShr(a, b Term) Term
  • func BVAdd(a, b Term) Term
  • func BVAnd(a, b Term) Term
  • func BVLShr(a, b Term) Term
  • func BVMul(a, b Term) Term
  • func BVNand(a, b Term) Term
  • func BVNeg(a Term) Term
  • func BVNor(a, b Term) Term
  • func BVNot(a Term) Term
  • func BVOr(a, b Term) Term
  • func BVSDiv(a, b Term) Term
  • func BVSMod(a, b Term) Term
  • func BVSRem(a, b Term) Term
  • func BVShl(a, b Term) Term
  • func BVSub(a, b Term) Term
  • func BVUDiv(a, b Term) Term
  • func BVURem(a, b Term) Term
  • func BVXNor(a, b Term) Term
  • func Equals(a, b Term) Term
  • func GT(a, b Term) Term
  • func GTE(a, b Term) Term
  • func IfThenElse(e1, e2, e3 Term) Term
  • func Implies(a, b Term) Term
  • func LT(a, b Term) Term
  • func LTE(a, b Term) Term
  • func Mul(a, b Term) Term
  • func NewApp(x string, args ...Term) Term
  • func NewBitVec(n, id int64) Term
  • func NewBool(b bool) Term
  • func NewConst(s string) Term
  • func NewInt(i int) Term
  • func Or(a, b Term) Term
  • func SexpToTerm(sexp Sexp) (Term, error)
  • func Sub(a, b Term) Term

Variables

var (
	IntSort  = &SortName{"Int"}
	BoolSort = &SortName{"Bool"}
)

var ParserEOF = errors.New("End-of-Input")

Functions

func IsSymbol

func IsSymbol(sexp Sexp, id string) bool

Types

type App

type App struct {
	Id   Identifier
	Args []Term
}

type BitVec

type BitVec struct {
	Value int64
	Width int64
}

type BitVecSort

type BitVecSort struct {
	Width int64
}

type Const

type Const struct {
	Id Identifier
}

type Identifier

type Identifier string

type Int

type Int struct {
	Int int64
}

type Let

type Let struct {
	Id    Identifier
	Value Term
	In    Term
}

type Parser

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

func NewParser

func NewParser(r io.Reader) *Parser

func (*Parser) Read

func (p *Parser) Read() (Sexp, error)

type SBitVec

type SBitVec struct {
	Value int64
	Width int64
}

func (*SBitVec) String

func (s *SBitVec) String() string

type SInt

type SInt struct {
	Int int64
}

func (*SInt) String

func (s *SInt) String() string

type SKeyword

type SKeyword struct {
	Keyword string
}

func (*SKeyword) String

func (s *SKeyword) String() string

type SList

type SList struct {
	List []Sexp
}

func (*SList) String

func (s *SList) String() string

type SString

type SString struct {
	Str string
}

func (*SString) String

func (s *SString) String() string

type SSymbol

type SSymbol struct {
	Symbol string
}

func (*SSymbol) String

func (s *SSymbol) String() string

type Satisfiable

type Satisfiable int

const (
	Sat Satisfiable = iota
	Unsat
	Unknown
)

func (Satisfiable) String

func (i Satisfiable) String() string

type Sexp

type Sexp interface {
	String() string
	// contains filtered or unexported methods
}

func IdToSexp

func IdToSexp(id Identifier) Sexp

func SortToSexp

func SortToSexp(sort Sort) Sexp

func TermToSexp

func TermToSexp(term Term) Sexp

type Solver

type Solver interface {
	Close()
	DeclareConst(id string, sort Sort) error
	Assert(t Term) error
	CheckSat() (Satisfiable, error)
	GetModel() (map[string]Term, error)
	Push()
	Pop() error

	// low-level interface
	Command(sexp Sexp) (Sexp, error)
}

type Sort

type Sort interface {
	// contains filtered or unexported methods
}

type SortApp

type SortApp struct {
	Id   Identifier
	Args []Sort
}

type SortName

type SortName struct {
	Id Identifier
}

type String

type String struct {
	String string
}

type Term

type Term interface {
	// contains filtered or unexported methods
}

func Add

func Add(a, b Term) Term

func And

func And(a, b Term) Term

func BVAShr

func BVAShr(a, b Term) Term

func BVAdd

func BVAdd(a, b Term) Term

func BVAnd

func BVAnd(a, b Term) Term

func BVLShr

func BVLShr(a, b Term) Term

func BVMul

func BVMul(a, b Term) Term

func BVNand

func BVNand(a, b Term) Term

func BVNeg

func BVNeg(a Term) Term

func BVNor

func BVNor(a, b Term) Term

func BVNot

func BVNot(a Term) Term

func BVOr

func BVOr(a, b Term) Term

func BVSDiv

func BVSDiv(a, b Term) Term

func BVSMod

func BVSMod(a, b Term) Term

func BVSRem

func BVSRem(a, b Term) Term

func BVShl

func BVShl(a, b Term) Term

func BVSub

func BVSub(a, b Term) Term

func BVUDiv

func BVUDiv(a, b Term) Term

func BVURem

func BVURem(a, b Term) Term

func BVXNor

func BVXNor(a, b Term) Term

func Equals

func Equals(a, b Term) Term

func GT

func GT(a, b Term) Term

func GTE

func GTE(a, b Term) Term

func IfThenElse

func IfThenElse(e1, e2, e3 Term) Term

func Implies

func Implies(a, b Term) Term

func LT

func LT(a, b Term) Term

func LTE

func LTE(a, b Term) Term

func Mul

func Mul(a, b Term) Term

func NewApp

func NewApp(x string, args ...Term) Term

func NewBitVec

func NewBitVec(n, id int64) Term

func NewBool

func NewBool(b bool) Term

func NewConst

func NewConst(s string) Term

func NewInt

func NewInt(i int) Term

func Or

func Or(a, b Term) Term

func SexpToTerm

func SexpToTerm(sexp Sexp) (Term, error)

func Sub

func Sub(a, b Term) Term