gosmt

package module
v0.26.0 Latest Latest
Warning

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

 Go to latest Published: Jul 23, 2026 License: MIT Imports: 5 Imported by: 0

README

GoSMT

GoSMT is a native Go+/Go SMT solver and compatibility project pinned against Microsoft Z3 4.16.0 (ddb49568d3520e99799e364fb22f35fc67d887b1, MIT). It does not bind to Z3: differential tests use Z3 as an oracle while released artifacts remain pure generated Go.

The essential, solver-neutral surface lives in goforge.dev/goplus/std/smt: sorted terms, exhaustive results, context-indexed models and proofs, checked incremental scopes, temporary assumptions, minimized unsat cores, and native Boolean, integer-difference, general exact-linear-integer, exact-linear-real, and typed unary/binary EUF solving, including finite, arbitrary-arity same-sort, mixed-sort, mutually recursive, unary/multi-parameter, and mutually parametric algebraic datatypes with exhaustive Bool/Int/Real/bit-vector/datatype pattern matching—including constructor selection from branch constraints—and typed field updates, plus Euclidean integer division/modulo by nonzero constants, plus bounded complete Boolean QF_DT branching and sound conjunctive combination while those signatures remain disjoint and fixed-point shared equality exchange for unary Real→Real EUF. Strings include exact ground regular-language membership, the core SMT-LIB regex algebra, and context-indexed GoSMT construction; the standard-library regex representation remains element-sort indexed. Function arguments and results retain Go+ sort indices. The solver-neutral SMT-LIB syntax lives in goforge.dev/goplus/std/smtlib. This module adds Z3-shaped contexts, SMT-LIB execution, theories, tactics, optimization, fixedpoint, compatibility, and portfolio engineering.

This repository is at foundation stage; see COMPATIBILITY.md for the versioned scope and ROADMAP.md for the non-negotiable path to broad Z3 functionality. Unsupported theories return unknown; they are not silently approximated.

Documentation

Overview

Package gosmt exposes Z3-shaped, context-indexed solver construction over the essential Go+ standard-library SMT core.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func AssumptionResultFold 

func AssumptionResultFold[R any](a AssumptionResult, cs AssumptionResultCases[R]) R

AssumptionResultFold reduces AssumptionResult by one-level case analysis.

func BitVecDatatypeMixedField added in v0.13.0 

func BitVecDatatypeMixedField(width int, name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

func BoolDatatypeMixedField added in v0.13.0 

func BoolDatatypeMixedField(name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

func CompareRational 

func CompareRational(left smt.Rational, right smt.Rational) int

func DatatypeReferenceMixedField added in v0.14.0 

func DatatypeReferenceMixedField(targetDatatype int, targetConstructors int, name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

func EmptyDatatypeMixedSignature added in v0.13.0 

func EmptyDatatypeMixedSignature() smt.MixedDatatypeSignature

func EvalBitVecArray added in v0.2.0 

func EvalBitVecArray(model Model, array BitVecArrayExpr, index smt.BitVectorValue) (smt.BitVectorValue, bool)

func EvalBool 

func EvalBool(model Model, expression BoolExpr) (bool, bool)

func EvalDatatype added in v0.9.0 

func EvalDatatype(datatype int, constructors int, model Model, expression DatatypeExpr) (smt.DatatypeValue, bool)

func EvalInt 

func EvalInt(model Model, expression IntExpr) (int64, bool)

func EvalIntArray 

func EvalIntArray(model Model, array ArrayExpr[smt.IntSort, smt.IntSort], index smt.IntegerValue) (smt.IntegerValue, bool)

func EvalIntExact 

func EvalIntExact(model Model, expression IntExpr) (smt.IntegerValue, bool)

func EvalReal 

func EvalReal(model Model, expression RealExpr) (smt.Rational, bool)

func EvalString added in v0.22.0 

func EvalString(model Model, expression StringExpr) (string, bool)

func ExecuteSMTLib 

func ExecuteSMTLib(source string) smtlib.ExecutionResult

func FirstDatatypeField added in v0.11.0 

func FirstDatatypeField() smt.BinaryDatatypeField

func IntDatatypeMixedField added in v0.13.0 

func IntDatatypeMixedField(name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

func ModelBitVec 

func ModelBitVec(model Model, term BitVecExpr) (smt.BitVectorValue, bool)

func ParseInteger 

func ParseInteger(value string) (smt.IntegerValue, error)

func ParseRational 

func ParseRational(value string) (smt.Rational, error)

func ParseSMTLib 

func ParseSMTLib(source string) smtlib.ParseResult

func Rational 

func Rational(numerator int64, denominator int64) smt.Rational

func RealDatatypeMixedField added in v0.13.0 

func RealDatatypeMixedField(name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

func ResultFold 

func ResultFold[R any](v Result, cs ResultCases[R]) R

ResultFold reduces Result by one-level case analysis.

func SecondDatatypeField added in v0.11.0 

func SecondDatatypeField() smt.BinaryDatatypeField

func SelectArray 

func SelectArray[I any, E any](array ArrayExpr[I, E], index smt.Term[I]) smt.Term[E]

func SelfDatatypeMixedField added in v0.13.0 

func SelfDatatypeMixedField(name string, rest smt.MixedDatatypeSignature) smt.MixedDatatypeSignature

Types

type ArrayExpr 

type ArrayExpr[I any, E any] interface {
	// contains filtered or unexported methods
}

func ArrayConst 

func ArrayConst[I any, E any](context Context, name string, id int) ArrayExpr[I, E]

func ConstArray 

func ConstArray[I any, E any](context Context, value smt.Term[E]) ArrayExpr[I, E]

func ConstIntArray 

func ConstIntArray(value IntExpr) ArrayExpr[smt.IntSort, smt.IntSort]

func IntArrayConst 

func IntArrayConst(context Context, name string, id int) ArrayExpr[smt.IntSort, smt.IntSort]

func StoreArray 

func StoreArray[I any, E any](array ArrayExpr[I, E], index smt.Term[I], value smt.Term[E]) ArrayExpr[I, E]

func StoreIntArray 

func StoreIntArray(array ArrayExpr[smt.IntSort, smt.IntSort], index IntExpr, value IntExpr) ArrayExpr[smt.IntSort, smt.IntSort]

type AssumptionResult 

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

func CheckAssuming 

func CheckAssuming(solver Solver, assumptions ...BoolExpr) AssumptionResult

type AssumptionResultCases 

type AssumptionResultCases[R any] struct {
	AssumptionSat     func(Value Model) R
	AssumptionUnsat   func(Context Context, Proof smt.Proof, Indices []int) R
	AssumptionUnknown func(Context Context, Proof smt.Proof, Reason smt.UnknownReason) R
}

AssumptionResultCases selects one handler per AssumptionResult variant for AssumptionResultFold.

type AssumptionSat 

type AssumptionSat struct {
	Value Model
}

type AssumptionUnknown 

type AssumptionUnknown struct {
	Context Context
	Proof   smt.Proof
	Reason  smt.UnknownReason
}

type AssumptionUnsat 

type AssumptionUnsat struct {
	Context Context
	Proof   smt.Proof
	Indices []int
}

type BinaryFunc 

type BinaryFunc = binaryFuncValue

func DeclareBinary 

func DeclareBinary(first int, second int, codomain int, context Context, name string, id int) BinaryFunc

type BitVecArrayExpr 

type BitVecArrayExpr = bitVecArrayExprValue

func BitVecArrayConst 

func BitVecArrayConst(indexWidth int, elementWidth int, context Context, name string, id int) BitVecArrayExpr

func ConstBitVecArray 

func ConstBitVecArray(indexWidth int, value BitVecExpr) BitVecArrayExpr

func StoreBitVecArray 

func StoreBitVecArray(array BitVecArrayExpr, index BitVecExpr, value BitVecExpr) BitVecArrayExpr

type BitVecBinaryFunc 

type BitVecBinaryFunc = bitVecBinaryFuncValue

func DeclareBitVecBinary 

func DeclareBitVecBinary(firstWidth int, secondWidth int, rangeWidth int, context Context, name string, id int) BitVecBinaryFunc

type BitVecExpr 

type BitVecExpr = bitVecExprValue

func AddBitVec 

func AddBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func AndBitVec 

func AndBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func ApplyBitVecBinary 

func ApplyBitVecBinary(function BitVecBinaryFunc, first BitVecExpr, second BitVecExpr) BitVecExpr

func ApplyBitVecFunction 

func ApplyBitVecFunction(function BitVecFunc, argument BitVecExpr) BitVecExpr

func AshrBitVec 

func AshrBitVec(value BitVecExpr, amount BitVecExpr) BitVecExpr

func BitVecConst 

func BitVecConst(width int, context Context, name string, id int) BitVecExpr

func BitVecValue 

func BitVecValue(width int, context Context, value uint64) BitVecExpr

func ConcatBitVec 

func ConcatBitVec(firstWidth int, secondWidth int, first BitVecExpr, second BitVecExpr) BitVecExpr

func ExtractBitVec 

func ExtractBitVec(high int, low int, value BitVecExpr) BitVecExpr

func IntToBitVec 

func IntToBitVec(width int, value IntExpr) BitVecExpr

IntToBitVec reduces an integer modulo 2^width. Its result width remains a dependent index, so mismatched widths are rejected by Go+ at compile time.

func LshrBitVec 

func LshrBitVec(value BitVecExpr, amount BitVecExpr) BitVecExpr

func MulBitVec 

func MulBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func NotBitVec 

func NotBitVec(value BitVecExpr) BitVecExpr

func OrBitVec 

func OrBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func RepeatBitVec 

func RepeatBitVec(count int, value BitVecExpr) BitVecExpr

func RotateLeftBitVec 

func RotateLeftBitVec(amount int, value BitVecExpr) BitVecExpr

func RotateRightBitVec 

func RotateRightBitVec(amount int, value BitVecExpr) BitVecExpr

func SdivBitVec 

func SdivBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func SelectBitVecArray 

func SelectBitVecArray(array BitVecArrayExpr, index BitVecExpr) BitVecExpr

func SelectMixedBitVecDatatypeField added in v0.13.0 

func SelectMixedBitVecDatatypeField(width int, cursor DatatypeMixedCursor, value DatatypeExpr) BitVecExpr

func ShlBitVec 

func ShlBitVec(value BitVecExpr, amount BitVecExpr) BitVecExpr

func SignExtendBitVec 

func SignExtendBitVec(additional int, value BitVecExpr) BitVecExpr

func SremBitVec 

func SremBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func SubBitVec 

func SubBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func UdivBitVec 

func UdivBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func UremBitVec 

func UremBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func XorBitVec 

func XorBitVec(left BitVecExpr, right BitVecExpr) BitVecExpr

func ZeroExtendBitVec 

func ZeroExtendBitVec(additional int, value BitVecExpr) BitVecExpr

type BitVecFunc 

type BitVecFunc = bitVecFuncValue

func DeclareBitVecFunction 

func DeclareBitVecFunction(domainWidth int, rangeWidth int, context Context, name string, id int) BitVecFunc

type BoolExpr 

type BoolExpr = boolExprValue

Expressions from different contexts cannot be composed in Go+.

func And 

func And(values ...BoolExpr) BoolExpr

func BoolConst 

func BoolConst(context Context, name string, id int) BoolExpr

func BoolValue 

func BoolValue(context Context, value bool) BoolExpr

func ContainsString added in v0.22.0 

func ContainsString(value StringExpr, substring StringExpr) BoolExpr

func EqArray 

func EqArray[I any, E any](left ArrayExpr[I, E], right ArrayExpr[I, E]) BoolExpr

func EqBitVec 

func EqBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func EqBitVecArray 

func EqBitVecArray(left BitVecArrayExpr, right BitVecArrayExpr) BoolExpr

func EqBool added in v0.19.0 

func EqBool(left BoolExpr, right BoolExpr) BoolExpr

func EqDatatype added in v0.9.0 

func EqDatatype(left DatatypeExpr, right DatatypeExpr) BoolExpr

func EqInt 

func EqInt(left IntExpr, right IntExpr) BoolExpr

func EqReal 

func EqReal(left RealExpr, right RealExpr) BoolExpr

func EqString added in v0.22.0 

func EqString(left StringExpr, right StringExpr) BoolExpr

func EqUninterpreted 

func EqUninterpreted(left UninterpretedExpr, right UninterpretedExpr) BoolExpr

func HasPrefixString added in v0.22.0 

func HasPrefixString(value StringExpr, prefix StringExpr) BoolExpr

func HasSuffixString added in v0.22.0 

func HasSuffixString(value StringExpr, suffix StringExpr) BoolExpr

func IffBool added in v0.5.0 

func IffBool(left BoolExpr, right BoolExpr) BoolExpr

func ImpliesBool added in v0.5.0 

func ImpliesBool(left BoolExpr, right BoolExpr) BoolExpr

func InRegexString added in v0.26.0 

func InRegexString(value StringExpr, expression RegexExpr) BoolExpr

func IsBinaryRecursiveDatatypeConstructor added in v0.11.0 

func IsBinaryRecursiveDatatypeConstructor(declaration DatatypeBinaryRecursiveConstructor, value DatatypeExpr) BoolExpr

func IsDatatypeConstructor added in v0.9.0 

func IsDatatypeConstructor(datatype int, constructors int, constructor int, value DatatypeExpr) BoolExpr

func IsDigitString added in v0.25.0 

func IsDigitString(value StringExpr) BoolExpr

func IsMixedDatatypeConstructor added in v0.13.0 

func IsMixedDatatypeConstructor(declaration DatatypeMixedConstructor, value DatatypeExpr) BoolExpr

func IsNaryRecursiveDatatypeConstructor added in v0.12.0 

func IsNaryRecursiveDatatypeConstructor(declaration DatatypeNaryRecursiveConstructor, value DatatypeExpr) BoolExpr

func IsRecursiveDatatypeConstructor added in v0.10.0 

func IsRecursiveDatatypeConstructor(declaration DatatypeRecursiveConstructor, value DatatypeExpr) BoolExpr

func Le 

func Le(left IntExpr, right IntExpr) BoolExpr

func LeReal 

func LeReal(left RealExpr, right RealExpr) BoolExpr

func Lt 

func Lt(left IntExpr, right IntExpr) BoolExpr

func LtReal 

func LtReal(left RealExpr, right RealExpr) BoolExpr

func NeInt added in v0.5.0 

func NeInt(left IntExpr, right IntExpr) BoolExpr

func NegOverflowBitVec 

func NegOverflowBitVec(value BitVecExpr) BoolExpr

func Not 

func Not(value BoolExpr) BoolExpr

func Or 

func Or(values ...BoolExpr) BoolExpr

func SaddOverflowBitVec 

func SaddOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func SdivOverflowBitVec 

func SdivOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func SelectMixedBoolDatatypeField added in v0.13.0 

func SelectMixedBoolDatatypeField(cursor DatatypeMixedCursor, value DatatypeExpr) BoolExpr

func SleBitVec 

func SleBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func SltBitVec 

func SltBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func SmulOverflowBitVec 

func SmulOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func SsubOverflowBitVec 

func SsubOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func UaddOverflowBitVec 

func UaddOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func UleBitVec 

func UleBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func UltBitVec 

func UltBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func UmulOverflowBitVec 

func UmulOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

func UsubOverflowBitVec 

func UsubOverflowBitVec(left BitVecExpr, right BitVecExpr) BoolExpr

type Context 

type Context = contextValue

func NewContext 

func NewContext(id int) Context

type DatatypeBinaryRecursiveConstructor added in v0.11.0 

type DatatypeBinaryRecursiveConstructor = datatypeBinaryRecursiveConstructorValue

func DeclareBinaryRecursiveDatatypeConstructor added in v0.11.0 

func DeclareBinaryRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, context Context, name string, firstSelectorName string, secondSelectorName string) DatatypeBinaryRecursiveConstructor

type DatatypeExpr added in v0.9.0 

type DatatypeExpr = datatypeExprValue

func ApplyBinaryRecursiveDatatypeConstructor added in v0.11.0 

func ApplyBinaryRecursiveDatatypeConstructor(declaration DatatypeBinaryRecursiveConstructor, first DatatypeExpr, second DatatypeExpr) DatatypeExpr

func ApplyMixedDatatypeConstructor added in v0.13.0 

func ApplyMixedDatatypeConstructor(declaration DatatypeMixedConstructor, arguments DatatypeMixedArguments) DatatypeExpr

func ApplyNaryRecursiveDatatypeConstructor added in v0.12.0 

func ApplyNaryRecursiveDatatypeConstructor(declaration DatatypeNaryRecursiveConstructor, values vec.Vec[DatatypeExpr]) DatatypeExpr

func ApplyRecursiveDatatypeConstructor added in v0.10.0 

func ApplyRecursiveDatatypeConstructor(declaration DatatypeRecursiveConstructor, value DatatypeExpr) DatatypeExpr

func DatatypeConst added in v0.9.0 

func DatatypeConst(datatype int, constructors int, context Context, name string, id int) DatatypeExpr

func DatatypeConstructor added in v0.9.0 

func DatatypeConstructor(datatype int, constructors int, constructor int, context Context, name string) DatatypeExpr

func SelectBinaryRecursiveDatatypeConstructor added in v0.11.0 

func SelectBinaryRecursiveDatatypeConstructor(field smt.BinaryDatatypeField, declaration DatatypeBinaryRecursiveConstructor, value DatatypeExpr) DatatypeExpr

func SelectMixedDatatypeReferenceField added in v0.14.0 

func SelectMixedDatatypeReferenceField(targetDatatype int, targetConstructors int, cursor DatatypeMixedCursor, value DatatypeExpr) DatatypeExpr

func SelectMixedSelfDatatypeField added in v0.13.0 

func SelectMixedSelfDatatypeField(cursor DatatypeMixedCursor, value DatatypeExpr) DatatypeExpr

func SelectNaryRecursiveDatatypeConstructor added in v0.12.0 

func SelectNaryRecursiveDatatypeConstructor(field vec.Fin, declaration DatatypeNaryRecursiveConstructor, value DatatypeExpr) DatatypeExpr

func SelectRecursiveDatatypeConstructor added in v0.10.0 

func SelectRecursiveDatatypeConstructor(declaration DatatypeRecursiveConstructor, value DatatypeExpr) DatatypeExpr

type DatatypeMixedArguments added in v0.13.0 

type DatatypeMixedArguments = datatypeMixedArgumentsValue

func BitVecDatatypeMixedArgument added in v0.13.0 

func BitVecDatatypeMixedArgument(width int, value BitVecExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

func BoolDatatypeMixedArgument added in v0.13.0 

func BoolDatatypeMixedArgument(value BoolExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

func DatatypeReferenceMixedArgument added in v0.14.0 

func DatatypeReferenceMixedArgument(targetDatatype int, targetConstructors int, value DatatypeExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

func EmptyDatatypeMixedArguments added in v0.13.0 

func EmptyDatatypeMixedArguments(context Context) DatatypeMixedArguments

func EmptyDatatypeMixedArgumentsFor added in v0.14.0 

func EmptyDatatypeMixedArgumentsFor(datatype int, constructors int, context Context) DatatypeMixedArguments

func IntDatatypeMixedArgument added in v0.13.0 

func IntDatatypeMixedArgument(value IntExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

func RealDatatypeMixedArgument added in v0.13.0 

func RealDatatypeMixedArgument(value RealExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

func SelfDatatypeMixedArgument added in v0.13.0 

func SelfDatatypeMixedArgument(value DatatypeExpr, rest DatatypeMixedArguments) DatatypeMixedArguments

type DatatypeMixedConstructor added in v0.13.0 

type DatatypeMixedConstructor = datatypeMixedConstructorValue

func DeclareMixedDatatypeConstructor added in v0.13.0 

func DeclareMixedDatatypeConstructor(datatype int, constructors int, constructor int, context Context, name string, signature smt.MixedDatatypeSignature) DatatypeMixedConstructor

type DatatypeMixedCursor added in v0.13.0 

type DatatypeMixedCursor = datatypeMixedCursorValue

func MixedDatatypeFields added in v0.13.0 

func MixedDatatypeFields(declaration DatatypeMixedConstructor) DatatypeMixedCursor

func NextMixedDatatypeField added in v0.13.0 

func NextMixedDatatypeField(cursor DatatypeMixedCursor) DatatypeMixedCursor

type DatatypeNaryRecursiveConstructor added in v0.12.0 

type DatatypeNaryRecursiveConstructor = datatypeNaryRecursiveConstructorValue

func DeclareNaryRecursiveDatatypeConstructor added in v0.12.0 

func DeclareNaryRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, arity int, context Context, name string, selectorNames vec.Vec[string]) DatatypeNaryRecursiveConstructor

type DatatypeRecursiveConstructor added in v0.10.0 

type DatatypeRecursiveConstructor = datatypeRecursiveConstructorValue

func DeclareRecursiveDatatypeConstructor added in v0.10.0 

func DeclareRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, context Context, name string, selectorName string) DatatypeRecursiveConstructor

type IntExpr 

type IntExpr = intExprValue

func Add 

func Add(values ...IntExpr) IntExpr

func BvToInt 

func BvToInt(value BitVecExpr) IntExpr

BvToInt interprets a bit vector using two's-complement signed semantics.

func BvToNat 

func BvToNat(value BitVecExpr) IntExpr

BvToNat interprets a bit vector as an unsigned mathematical integer.

func DivInt added in v0.6.0 

func DivInt(value IntExpr, divisor smt.IntegerValue) IntExpr

func DivInt64 added in v0.6.0 

func DivInt64(value IntExpr, divisor int64) IntExpr

func IndexOfString added in v0.24.0 

func IndexOfString(value StringExpr, substring StringExpr, offset IntExpr) IntExpr

func IntConst 

func IntConst(context Context, name string, id int) IntExpr

func IntVal 

func IntVal(context Context, value int64) IntExpr

func IntValExact 

func IntValExact(context Context, value smt.IntegerValue) IntExpr

func LengthString added in v0.22.0 

func LengthString(value StringExpr) IntExpr

func ModInt added in v0.6.0 

func ModInt(value IntExpr, divisor smt.IntegerValue) IntExpr

func ModInt64 added in v0.6.0 

func ModInt64(value IntExpr, divisor int64) IntExpr

func ScaleInt added in v0.3.0 

func ScaleInt(coefficient smt.IntegerValue, value IntExpr) IntExpr

func ScaleInt64 added in v0.3.0 

func ScaleInt64(coefficient int64, value IntExpr) IntExpr

func SelectIntArray 

func SelectIntArray(array ArrayExpr[smt.IntSort, smt.IntSort], index IntExpr) IntExpr

func SelectMixedIntDatatypeField added in v0.13.0 

func SelectMixedIntDatatypeField(cursor DatatypeMixedCursor, value DatatypeExpr) IntExpr

func Sub 

func Sub(left IntExpr, right IntExpr) IntExpr

func ToCodeString added in v0.25.0 

func ToCodeString(value StringExpr) IntExpr

func ToIntString added in v0.25.0 

func ToIntString(value StringExpr) IntExpr

type Model 

type Model = modelValue

type RealBinaryFunc 

type RealBinaryFunc = realBinaryFuncValue

func DeclareRealBinary 

func DeclareRealBinary(context Context, name string, id int) RealBinaryFunc

type RealExpr 

type RealExpr = realExprValue

func AddReal 

func AddReal(values ...RealExpr) RealExpr

func ApplyRealBinary 

func ApplyRealBinary(function RealBinaryFunc, first RealExpr, second RealExpr) RealExpr

func ApplyRealFunction 

func ApplyRealFunction(function RealFunc, argument RealExpr) RealExpr

func RealConst 

func RealConst(context Context, name string, id int) RealExpr

func RealVal 

func RealVal(context Context, value smt.Rational) RealExpr

func ScaleReal 

func ScaleReal(coefficient smt.Rational, value RealExpr) RealExpr

func SelectMixedRealDatatypeField added in v0.13.0 

func SelectMixedRealDatatypeField(cursor DatatypeMixedCursor, value DatatypeExpr) RealExpr

func SubReal 

func SubReal(left RealExpr, right RealExpr) RealExpr

type RealFunc 

type RealFunc = realFuncValue

func DeclareRealFunction 

func DeclareRealFunction(context Context, name string, id int) RealFunc

type RegexExpr added in v0.26.0 

type RegexExpr = regexExprValue

func AllCharStringRegex added in v0.26.0 

func AllCharStringRegex(context Context) RegexExpr

func ComplementRegexExpr added in v0.26.0 

func ComplementRegexExpr(value RegexExpr) RegexExpr

func ConcatRegexExpr added in v0.26.0 

func ConcatRegexExpr(left RegexExpr, right RegexExpr) RegexExpr

func DifferenceRegexExpr added in v0.26.0 

func DifferenceRegexExpr(left RegexExpr, right RegexExpr) RegexExpr

func EmptyStringRegex added in v0.26.0 

func EmptyStringRegex(context Context) RegexExpr

func FullStringRegex added in v0.26.0 

func FullStringRegex(context Context) RegexExpr

func IntersectRegexExpr added in v0.26.0 

func IntersectRegexExpr(left RegexExpr, right RegexExpr) RegexExpr

func LoopRegexExpr added in v0.26.0 

func LoopRegexExpr(minimum int, maximum int, value RegexExpr) RegexExpr

func OptionalRegexExpr added in v0.26.0 

func OptionalRegexExpr(value RegexExpr) RegexExpr

func PlusRegexExpr added in v0.26.0 

func PlusRegexExpr(value RegexExpr) RegexExpr

func RangeRegexString added in v0.26.0 

func RangeRegexString(low StringExpr, high StringExpr) RegexExpr

func StarRegexExpr added in v0.26.0 

func StarRegexExpr(value RegexExpr) RegexExpr

func ToRegexString added in v0.26.0 

func ToRegexString(value StringExpr) RegexExpr

func UnionRegexExpr added in v0.26.0 

func UnionRegexExpr(left RegexExpr, right RegexExpr) RegexExpr

type Result 

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

func Check 

func Check(solver Solver) Result

type ResultCases 

type ResultCases[R any] struct {
	Sat     func(Value Model) R
	Unsat   func(Context Context, Proof smt.Proof) R
	Unknown func(Context Context, Proof smt.Proof, Reason smt.UnknownReason) R
}

ResultCases selects one handler per Result variant for ResultFold.

type Sat 

type Sat struct {
	Value Model
}

type Solver 

type Solver = solverValue

func Assert 

func Assert(assertion int, solver Solver, formula BoolExpr) Solver

func NewSolver 

func NewSolver(context Context) Solver

type StringExpr added in v0.22.0 

type StringExpr = stringExprValue

func AtString added in v0.24.0 

func AtString(value StringExpr, index IntExpr) StringExpr

func ConcatString added in v0.22.0 

func ConcatString(values ...StringExpr) StringExpr

func FromCodeString added in v0.25.0 

func FromCodeString(value IntExpr) StringExpr

func FromIntString added in v0.25.0 

func FromIntString(value IntExpr) StringExpr

func ReplaceAllString added in v0.25.0 

func ReplaceAllString(value StringExpr, source StringExpr, replacement StringExpr) StringExpr

func ReplaceString added in v0.24.0 

func ReplaceString(value StringExpr, source StringExpr, replacement StringExpr) StringExpr

func StringConst added in v0.22.0 

func StringConst(context Context, name string, id int) StringExpr

func StringVal added in v0.22.0 

func StringVal(context Context, value string) StringExpr

func Substring added in v0.24.0 

func Substring(value StringExpr, offset IntExpr, length IntExpr) StringExpr

type UnaryFunc 

type UnaryFunc = unaryFuncValue

func DeclareUnary 

func DeclareUnary(domain int, codomain int, context Context, name string, id int) UnaryFunc

type UninterpretedExpr 

type UninterpretedExpr = uninterpretedExprValue

func ApplyBinaryUninterpreted 

func ApplyBinaryUninterpreted(function BinaryFunc, left UninterpretedExpr, right UninterpretedExpr) UninterpretedExpr

func ApplyUninterpreted 

func ApplyUninterpreted(function UnaryFunc, argument UninterpretedExpr) UninterpretedExpr

func UninterpretedConst 

func UninterpretedConst(sort int, context Context, name string, id int) UninterpretedExpr

type Unknown 

type Unknown struct {
	Context Context
	Proof   smt.Proof
	Reason  smt.UnknownReason
}

type Unsat 

type Unsat struct {
	Context Context
	Proof   smt.Proof
}

Source Files

View all Source files

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.