Why Go
- Case Studies
  
  Common problems companies solve with Go
- Use Cases
  
  Stories about how and why companies use Go
- Security
  
  How Go can help keep you secure by default
Learn
Docs
- Effective Go
  
  Tips for writing clear, performant, and idiomatic Go code
- Go User Manual
  
  A complete introduction to building software with Go
- Standard library
  
  Reference documentation for Go's standard library
- Release Notes
  
  Learn what's new in each Go release
Packages
Community
- Recorded Talks
  
  Videos from prior events
- Meetups
  
  Meet other local Go developers
- Conferences
  
  Learn and network with Go developers from around the world
- Go blog
  
  The Go project's official blog.
- Go project
  
  Get help and stay informed from Go
- Get connected

smt

package

Go to main page

Versions in this module

v0

v0.18.9

May 10, 2026

v0.18.8

May 9, 2026

v0.18.7

May 9, 2026

v0.18.6

May 9, 2026

v0.18.5

May 9, 2026

v0.18.4

May 8, 2026

v0.17.0

May 7, 2026

v0.16.2

May 6, 2026

v0.16.1

May 6, 2026

v0.16.0

May 6, 2026

v0.15.2

May 5, 2026

v0.15.1

May 5, 2026

v0.15.0

May 4, 2026

v0.14.3

May 2, 2026

Changes in this version

+ const ParamRenamePrefix

+ func DeclareDatatypesMutual(decls []string) string

+ func ExtractSortNameFromDecl(decl string) string

type CalleeDef

+ IsContract bool

+ ResultConst string

+ type ContractCalleeDecl struct

+ Name string

+ ResultConst string

+ SMTLib string

+ func EncodeCalleeByContract(spec ContractSpec, args []core.CoreExpr, callSiteIdx int) (*ContractCalleeDecl, error)

+ type ContractSpec struct

+ Ensures []*core.Contract

+ FuncName string

+ Params []FunctionParam

+ Requires []*core.Contract

+ ReturnSort string

+ func BuildContractSpec(funcName string, meta *core.DeclMeta, params []FunctionParam, ...) ContractSpec

type EncodeFunctionOpts

+ ImportedPrograms map[string]*core.Program

v0.14.2

Apr 26, 2026

v0.14.1

Apr 21, 2026

Changes in this version

+ var BuiltinToSMTOp = map[string]string

+ var ErrUnresolvableTypes = errors.New("unresolvable cross-module types")

+ var ListBuiltinSpecial = map[string]ListBuiltinSpec

+ var NumericBuiltinSpecial = map[string]NumericBuiltinSpec

+ var RecursiveListBuiltins = map[string]string

+ var StdlibListToSMT = map[string]string

+ var StdlibStringToSMT = map[string]string

+ var StringBuiltinSpecial = map[string]StringBuiltinSpec

+ func AllHigherOrderIsInlinable(body core.CoreExpr) bool

+ func Assert(expr string) string

+ func AssertNot(expr string) string

+ func CheckSat() string

+ func DeclareConst(name, sort string) string

+ func DeclareDatatype(typeName string, variants []ADTVariant) string

+ func DeclareEnumDatatype(typeName string, variants []string) string

+ func DeclareRecordDatatype(sortName string, fields map[string]string) string

+ func EncodeExpr(expr core.CoreExpr) (string, error)

+ func FindZ3() (string, error)

+ func GenerateListUnrolling(op string, depth int, elemSort string) []string

+ func GetModel() string

+ func IsRecursiveFunc(body core.CoreExpr, funcName string) bool

+ func IsUserDefinedCall(app *core.App, prog *core.Program) (string, bool)

+ func MapRecordFields(rec *types.TRecord) (map[string]string, error)

+ func MapRecordSortName(rec *types.TRecord) string

+ func MapType(t types.Type) (string, error)

+ func RecordConstructorName(sortName string) string

+ func ReplaceSelfCalls(expr core.CoreExpr, funcName, replacement string) core.CoreExpr

+ func ResolveStdlibToBuiltin(module, name string) (string, bool)

+ func SortedFieldNamesStr(fields map[string]string) []string

+ func SpecializeFilter(funcName string, lambda *core.Lambda, listParam string) (core.CoreExpr, string)

+ func SpecializeFoldl(funcName string, lambda *core.Lambda, listParam string) (core.CoreExpr, string)

+ func SpecializeMap(funcName string, lambda *core.Lambda, listParam string) (core.CoreExpr, string)

+ func SubstituteLambdaVar(body core.CoreExpr, paramName string, replacement core.CoreExpr) core.CoreExpr

+ func TopLevelUnrolledName(op string, depth int) string

+ func Z3Available() bool

+ func Z3Version() string

+ type ADTField struct

+ Name string

+ Sort string

+ type ADTVariant struct

+ Fields []ADTField

+ Name string

+ type CalleeDef struct

+ ADTDecl string

+ Name string

+ SMTLib string

+ func ResolveCallees(funcName string, body core.CoreExpr, prog *core.Program, ...) ([]CalleeDef, error)

+ type CalleeInfo struct

+ ADTTypes map[string][]ADTVariant

+ Body core.CoreExpr

+ Name string

+ Params []FunctionParam

+ ReturnSort string

+ type EncodeFunctionOpts struct

+ Body core.CoreExpr

+ Contracts []*core.Contract

+ ExtraDeclarations []string

+ HOFInlineDepth int

+ Program *core.Program

+ RecordTypeAliases map[string]*types.TRecord

+ RecursiveDepth int

+ ReturnType types.Type

+ SurfaceParams map[string][]FunctionParam

+ SurfaceReturnSorts map[string]string

+ type EncodeResult struct

+ Assertions []string

+ BodyExpr string

+ Declarations []string

+ SMTLib string

+ func EncodeFunction(funcName string, params []FunctionParam, body core.CoreExpr, returnSort string, ...) (*EncodeResult, error)

+ type FunctionParam struct

+ Name string

+ Type types.Type

+ type HOFKind int

+ const HOFFilter

+ const HOFFoldl

+ const HOFMap

+ type InlinableHOFCall struct

+ InitVal core.CoreExpr

+ Kind HOFKind

+ Lambda *core.Lambda

+ ListArg core.CoreExpr

+ Original *core.App

+ func IsInlinableHOF(body core.CoreExpr) []InlinableHOFCall

+ type InlineResult struct

+ NewBody core.CoreExpr

+ Specializations []SpecializationResult

+ func InlineHOFCalls(funcName string, body core.CoreExpr, depth int) *InlineResult

+ type ListBuiltinSpec struct

+ AppendZero bool

+ ConsMode bool

+ ContainsMode bool

+ Op string

+ TailMode bool

+ TernaryMode bool

+ Unary bool

+ type ModelBinding struct

+ Name string

+ Sort string

+ Value string

+ type NumericBuiltinSpec struct

+ Op string

+ Unary bool

+ type RecordTypeInfo struct

+ CtorName string

+ FieldNames []string

+ FieldSorts map[string]string

+ SortName string

+ type RejectionCode string

+ const RejectDeepPatterns

+ const RejectHigherOrder

+ const RejectNoContracts

+ const RejectNotPure

+ const RejectRecursive

+ const RejectUnencodable

+ type SMTContext struct

+ Declarations []string

+ DeclaredTypes map[string]bool

+ ResolvedCallees map[string]bool

+ Variables map[string]string

+ func NewSMTContext() *SMTContext

+ type SMTRejectionReason struct

+ Code RejectionCode

+ Hint string

+ Location string

+ Message string

+ func IsSMTEncodable(funcName string, meta *core.DeclMeta, body core.CoreExpr) (bool, []SMTRejectionReason)

+ func IsSMTEncodableForCallee(funcName string, meta *core.DeclMeta, body core.CoreExpr) (bool, []SMTRejectionReason)

+ func (r SMTRejectionReason) String() string

+ type SolverConfig struct

+ Timeout time.Duration

+ Z3Path string

+ func DefaultSolverConfig() SolverConfig

+ type SolverResult struct

+ Duration time.Duration

+ Error string

+ Model []ModelBinding

+ RawOutput string

+ SMTLib string

+ Status SolverStatus

+ func Solve(smtlib string, config SolverConfig) (*SolverResult, error)

+ func SolveFile(path string, config SolverConfig) (*SolverResult, error)

+ type SolverStatus int

+ const StatusCounterexample

+ const StatusError

+ const StatusUnknown

+ const StatusVerified

+ func (s SolverStatus) String() string

+ type SpecializationResult struct

+ Declarations []string

+ Kind HOFKind

+ TopLevelName string

+ type StringBuiltinSpec struct

+ AppendZero bool

+ FlipArgs bool

+ Op string

+ SubstrMode bool

+ Unary bool

+ type UnrollConfig struct

+ Body core.CoreExpr

+ Depth int

+ FuncName string

+ Params []FunctionParam

+ ReturnSort string

+ type UnrollResult struct

+ Declarations []string

+ TopLevelName string

+ func UnrollRecursiveFunction(cfg UnrollConfig) (*UnrollResult, error)