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
- type SBitVec
- type SInt
- type SKeyword
- type SList
- type SString
- type SSymbol
- type Satisfiable
- type 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
Constants ¶
This section is empty.
Variables ¶
View Source
var ( IntSort = &SortName{"Int"} BoolSort = &SortName{"Bool"} )
View Source
var ParserEOF = errors.New("End-of-Input")
Functions ¶
Types ¶
type App ¶
type App struct { Id Identifier Args []Term }
type BitVecSort ¶
type BitVecSort struct {
Width int64
}
type Const ¶
type Const struct {
Id Identifier
}
type Identifier ¶
type Identifier string
type Let ¶
type Let struct { Id Identifier Value Term In Term }
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 TermToSexp ¶
type SortApp ¶
type SortApp struct { Id Identifier Args []Sort }
type SortName ¶
type SortName struct {
Id Identifier
}
type Term ¶
type Term interface {
// contains filtered or unexported methods
}
func IfThenElse ¶
func SexpToTerm ¶
Click to show internal directories.
Click to hide internal directories.