smt

package
v0.122.0 Latest Latest
Warning

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

 Go to latest Published: Jul 24, 2026 License: MIT Imports: 11 Imported by: 0

Documentation

Overview

Package smt provides the essential sorted-term and incremental-solver core shared by native Go+ theorem provers. It is intentionally independent of any one solver's compatibility API.

Index

Constants

View Source 
const (
	CompactStringEqual = iota
	CompactStringLengthEqual
	CompactStringLengthLess
	CompactStringLengthLessEqual
	CompactStringContains
	CompactStringPrefix
	CompactStringSuffix
	CompactStringLess
	CompactStringLessEqual
)
View Source 
const (
	CompactStringAtEquality = iota
	CompactStringSubstringEquality
)

Variables

This section is empty.

Functions

func AnyTermEqual 

func AnyTermEqual(a, b AnyTerm) bool

AnyTermEqual reports structural equality of a and b.

func AnyTermEqualWith 

func AnyTermEqualWith(a, b AnyTerm, ov AnyTermEqOverrides) bool

AnyTermEqualWith reports structural equality of a and b under ov.

func AnyTermFold 

func AnyTermFold[R any](a AnyTerm, cs AnyTermCases[R]) R

AnyTermFold reduces AnyTerm by one-level case analysis.

func AssumptionCheckResultFold 

func AssumptionCheckResultFold[R any](a AssumptionCheckResult, cs AssumptionCheckResultCases[R]) R

AssumptionCheckResultFold reduces AssumptionCheckResult by one-level case analysis.

func BinaryDatatypeFieldEqual added in v0.38.0 

func BinaryDatatypeFieldEqual(a, b BinaryDatatypeField) bool

BinaryDatatypeFieldEqual reports structural equality of a and b.

func BinaryDatatypeFieldEqualWith added in v0.38.0 

func BinaryDatatypeFieldEqualWith(a, b BinaryDatatypeField, ov BinaryDatatypeFieldEqOverrides) bool

BinaryDatatypeFieldEqualWith reports structural equality of a and b under ov.

func BinaryDatatypeFieldFold added in v0.38.0 

func BinaryDatatypeFieldFold[R any](b BinaryDatatypeField, cs BinaryDatatypeFieldCases[R]) R

BinaryDatatypeFieldFold reduces BinaryDatatypeField by one-level case analysis.

func BitVecUnaryFunctionInfo 

func BitVecUnaryFunctionInfo[D any, R any](function SortedUnaryFunction[D, R]) (int, int, int)

func BoolValue 

func BoolValue(model Model, term Term[BoolSort]) (bool, bool)

func CheckResultFold 

func CheckResultFold[R any](v CheckResult, cs CheckResultCases[R]) R

CheckResultFold reduces CheckResult by one-level case analysis.

func CompactStringBooleanValue added in v0.58.0 

func CompactStringBooleanValue(model Model, formula CompactStringBooleanFormula) (bool, bool)

func CompactStringModelValue added in v0.58.0 

func CompactStringModelValue(model Model, term CompactStringTerm) (string, bool)

func CompactStringRelationValue added in v0.58.0 

func CompactStringRelationValue(model Model, relation CompactStringRelation) (bool, bool)

func CompactStringWordEquationValue added in v0.59.0 

func CompactStringWordEquationValue(model Model, equation CompactStringWordEquation) (bool, bool)

func CompareIntegerValue 

func CompareIntegerValue(left, right IntegerValue) int

func CompareRational 

func CompareRational(left, right Rational) int

func CompareSignedBitVectorValue 

func CompareSignedBitVectorValue(left, right BitVectorValue) int

func CompareStringValues added in v0.115.0 

func CompareStringValues(left, right string) int

CompareStringValues compares SMT-LIB strings by Unicode code point without allocating decoded rune slices. It returns -1, 0, or 1.

func CompareUnsignedBitVectorValue 

func CompareUnsignedBitVectorValue(left, right BitVectorValue) int

func ContextID 

func ContextID(context int, assertion int) int

func DatatypeFieldListEqual added in v0.40.0 

func DatatypeFieldListEqual(a, b DatatypeFieldList) bool

DatatypeFieldListEqual reports structural equality of a and b.

func DatatypeFieldListEqualWith added in v0.40.0 

func DatatypeFieldListEqualWith(a, b DatatypeFieldList, ov DatatypeFieldListEqOverrides) bool

DatatypeFieldListEqualWith reports structural equality of a and b under ov.

func DatatypeFieldListFold added in v0.40.0 

func DatatypeFieldListFold[R any](d DatatypeFieldList, cs DatatypeFieldListCases[R]) R

DatatypeFieldListFold reduces DatatypeFieldList by one-level case analysis.

func DatatypeFieldListUniverse added in v0.40.0 

func DatatypeFieldListUniverse(d DatatypeFieldList) iter.Seq[DatatypeFieldList]

DatatypeFieldListUniverse yields d and all transitive DatatypeFieldList subterms, preorder.

func DatatypeFieldSortEqual added in v0.40.0 

func DatatypeFieldSortEqual(a, b DatatypeFieldSort) bool

DatatypeFieldSortEqual reports structural equality of a and b.

func DatatypeFieldSortEqualWith added in v0.40.0 

func DatatypeFieldSortEqualWith(a, b DatatypeFieldSort, ov DatatypeFieldSortEqOverrides) bool

DatatypeFieldSortEqualWith reports structural equality of a and b under ov.

func DatatypeFieldSortFold added in v0.40.0 

func DatatypeFieldSortFold[R any](d DatatypeFieldSort, cs DatatypeFieldSortCases[R]) R

DatatypeFieldSortFold reduces DatatypeFieldSort by one-level case analysis.

func DecodeStringCodePoints added in v0.54.0 

func DecodeStringCodePoints(value string) []rune

DecodeStringCodePoints decodes the SMT-LIB character domain, including surrogate code points represented with their three-byte WTF-8 encoding.

func DivModIntegerValue added in v0.33.0 

func DivModIntegerValue(dividend, divisor IntegerValue) (IntegerValue, IntegerValue, bool)

DivModIntegerValue implements SMT-LIB Euclidean division for every nonzero divisor: dividend = divisor*quotient + remainder and 0 <= remainder < abs(divisor).

func EncodeStringCodePoint added in v0.54.0 

func EncodeStringCodePoint(value int64) (string, bool)

func EqualBitVectorValue 

func EqualBitVectorValue(left, right BitVectorValue) bool

func IntValue 

func IntValue(model Model, term Term[IntSort]) (int64, bool)

func IntegerSymbol added in v0.111.0 

func IntegerSymbol(term Term[IntSort]) (int, string, bool)

IntegerSymbol identifies a direct integer symbol without materializing or exposing the internal variable representation.

func IntegerVariableID 

func IntegerVariableID(term Term[IntSort]) (int, bool)

func MemoizedContextView added in v0.38.0 

func MemoizedContextView(solver Solver, key any, context int, build func(int, CheckResult) any) any

MemoizedContextView is the non-capturing form of MemoizedView for adapters whose result also retains an erased context witness. Passing a package-level build function avoids allocating a closure on the cold path while preserving the same immutable one-view cache and allocation-free warm checks.

func MemoizedView 

func MemoizedView(solver Solver, key any, build func(CheckResult) any) any

MemoizedView lets a compatibility layer derive one immutable result view without maintaining a second heap-resident cache. key must be a package-unique comparable value and remains fixed for this solver state.

func NegOverflowBitVectorValue 

func NegOverflowBitVectorValue(value BitVectorValue) bool

func SignedAddOverflowBitVectorValue 

func SignedAddOverflowBitVectorValue(left, right BitVectorValue) bool

func SignedDivOverflowBitVectorValue 

func SignedDivOverflowBitVectorValue(left, right BitVectorValue) bool

func SignedMulOverflowBitVectorValue 

func SignedMulOverflowBitVectorValue(left, right BitVectorValue) bool

func SignedSubOverflowBitVectorValue 

func SignedSubOverflowBitVectorValue(left, right BitVectorValue) bool

func StringIntegerModelValue added in v0.50.0 

func StringIntegerModelValue(model Model, term Term[IntSort]) (int64, bool)

func StringModelValue added in v0.50.0 

func StringModelValue(model Model, term Term[StringSort]) (string, bool)

func StringReplaceRegexAllValue added in v0.114.0 

func StringReplaceRegexAllValue(
	value string,
	expression Regex[StringSort],
	replacement string,
) (string, bool)

StringReplaceRegexAllValue replaces each shortest non-empty match in a ground string, scanning from left to right.

func StringReplaceRegexValue added in v0.114.0 

func StringReplaceRegexValue(
	value string,
	expression Regex[StringSort],
	replacement string,
) (string, bool)

StringReplaceRegexValue replaces the shortest leftmost match in a ground string. The result is unknown only when the regular expression contains symbolic leaves that cannot be evaluated without a model.

func TermFold 

func TermFold[S any, R any](t Term[S], cs TermCases[S, R]) R

TermFold reduces Term[S] by one-level case analysis.

func UnknownReasonEqual 

func UnknownReasonEqual(a, b UnknownReason) bool

UnknownReasonEqual reports structural equality of a and b.

func UnknownReasonEqualWith 

func UnknownReasonEqualWith(a, b UnknownReason, ov UnknownReasonEqOverrides) bool

UnknownReasonEqualWith reports structural equality of a and b under ov.

func UnknownReasonFold 

func UnknownReasonFold[R any](u UnknownReason, cs UnknownReasonCases[R]) R

UnknownReasonFold reduces UnknownReason by one-level case analysis.

func UnsignedAddOverflowBitVectorValue 

func UnsignedAddOverflowBitVectorValue(left, right BitVectorValue) bool

func UnsignedMulOverflowBitVectorValue 

func UnsignedMulOverflowBitVectorValue(left, right BitVectorValue) bool

func UnsignedSubOverflowBitVectorValue 

func UnsignedSubOverflowBitVectorValue(left, right BitVectorValue) bool

Types

type Add 

type Add struct {
	Values []Term[IntSort]
}

type And 

type And struct {
	Values []Term[BoolSort]
}

type AnyTerm 

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

type AnyTermCases 

type AnyTermCases[R any] struct {
	SomeBool func(Value Term[BoolSort]) R
	SomeInt  func(Value Term[IntSort]) R
	SomeReal func(Value Term[RealSort]) R
}

AnyTermCases selects one handler per AnyTerm variant for AnyTermFold.

type AnyTermEqOverrides 

type AnyTermEqOverrides struct {
	SomeBool func(x, y SomeBool) (eq, handled bool)
	SomeInt  func(x, y SomeInt) (eq, handled bool)
	SomeReal func(x, y SomeReal) (eq, handled bool)
}

AnyTermEqOverrides carries optional per-variant hooks for AnyTermEqualWith. A hook returning handled=false falls through to the derived comparison.

type ArrayCongruenceConjunction 

type ArrayCongruenceConjunction struct {
	Equality ArrayEqualityRelation
	Read     ArrayReadRelation
}

type ArrayConstantEqualityRelation 

type ArrayConstantEqualityRelation struct {
	ArrayID int
	Default IntegerValue
	Negated bool
}

type ArrayConstantReadConjunction 

type ArrayConstantReadConjunction struct {
	Equality ArrayConstantEqualityRelation
	Read     ArrayReadValueRelation
}

type ArrayEqualityRelation 

type ArrayEqualityRelation struct {
	LeftID  int
	RightID int
	Negated bool
}

type ArrayExtensionalReadConjunction added in v0.38.0 

type ArrayExtensionalReadConjunction struct {
	Equality ArrayEqualityRelation
	Read     ArrayReadValueRelation
}

type ArrayIntegerEqualityExchange 

type ArrayIntegerEqualityExchange struct {
	First  IntegerDifferenceConstraint
	Second IntegerDifferenceConstraint
	Read   ArrayStoreReadValueRelation
}

type ArrayIntegerSymbolEqualityExchange added in v0.38.0 

type ArrayIntegerSymbolEqualityExchange struct {
	LeftID  int
	RightID int
	Read    ArrayStoreReadValueRelation
}

ArrayIntegerSymbolEqualityExchange is the compact two-atom form of i = j together with a store-at-i/read-at-j relation. It avoids routing a common array law through the general LIA/array combination machinery.

type ArrayReadRelation 

type ArrayReadRelation struct {
	LeftID     int
	RightID    int
	LeftIndex  IntegerValue
	RightIndex IntegerValue
	Negated    bool
}

func CompactIntegerArrayReadEquality 

func CompactIntegerArrayReadEquality(left, right Term[IntSort]) (ArrayReadRelation, bool)

type ArrayReadValueRelation 

type ArrayReadValueRelation struct {
	ArrayID int
	Index   IntegerValue
	Value   IntegerValue
	Negated bool
}

func CompactIntegerArrayReadValueEquality 

func CompactIntegerArrayReadValueEquality(left, right Term[IntSort]) (ArrayReadValueRelation, bool)

type ArraySort 

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

type ArrayStoreBridgeReadConjunction 

type ArrayStoreBridgeReadConjunction struct {
	Store ArrayStoreEqualityRelation
	Read  ArrayReadRelation
}

type ArrayStoreEqualityRelation 

type ArrayStoreEqualityRelation struct {
	LeftID     int
	RightID    int
	LeftIndex  IntegerValue
	RightIndex IntegerValue
	LeftValue  IntegerValue
	RightValue IntegerValue
	Negated    bool
}

type ArrayStoreReadValueRelation 

type ArrayStoreReadValueRelation struct {
	ArrayID       int
	StoreIndexID  int
	ReadIndexID   int
	StoredValue   IntegerValue
	ComparedValue IntegerValue
	Negated       bool
}

func CompactIntegerArrayStoreReadValueEquality 

func CompactIntegerArrayStoreReadValueEquality(left, right Term[IntSort]) (ArrayStoreReadValueRelation, bool)

type AssumptionCheckResult 

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

func CheckAssuming 

func CheckAssuming(solver Solver, assumptions ...Term[BoolSort]) AssumptionCheckResult

CheckAssuming solves with temporary Boolean assumptions. An unsatisfiable result carries a deletion-minimized set of indices into assumptions.

type AssumptionCheckResultCases 

type AssumptionCheckResultCases[R any] struct {
	AssumptionsSatisfiable   func(Value Model) R
	AssumptionsUnsatisfiable func(Value Proof, Indices []int) R
	AssumptionsUnknown       func(Context Proof, Reason UnknownReason) R
}

AssumptionCheckResultCases selects one handler per AssumptionCheckResult variant for AssumptionCheckResultFold.

type AssumptionsSatisfiable 

type AssumptionsSatisfiable struct {
	Value Model
}

type AssumptionsUnknown 

type AssumptionsUnknown struct {
	Context Proof
	Reason  UnknownReason
}

type AssumptionsUnsatisfiable 

type AssumptionsUnsatisfiable struct {
	Value   Proof
	Indices []int
}

type BinaryDatatypeField added in v0.38.0 

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

type BinaryDatatypeFieldCases added in v0.38.0 

type BinaryDatatypeFieldCases[R any] struct {
	FirstDatatypeField  func() R
	SecondDatatypeField func() R
}

BinaryDatatypeFieldCases selects one handler per BinaryDatatypeField variant for BinaryDatatypeFieldFold.

type BinaryDatatypeFieldEqOverrides added in v0.38.0 

type BinaryDatatypeFieldEqOverrides struct {
	FirstDatatypeField  func(x, y FirstDatatypeField) (eq, handled bool)
	SecondDatatypeField func(x, y SecondDatatypeField) (eq, handled bool)
}

BinaryDatatypeFieldEqOverrides carries optional per-variant hooks for BinaryDatatypeFieldEqualWith. A hook returning handled=false falls through to the derived comparison.

type BinaryFunction 

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

BinaryFunction[a,b,r] retains both argument sorts and its result sort. Go+ rejects swapped or otherwise ill-sorted applications before generation.

func DeclareBinaryFunction 

func DeclareBinaryFunction(first int, second int, codomain int, id int, name string) BinaryFunction

type BinaryRecursiveDatatypeConstructor added in v0.38.0 

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

BinaryRecursiveDatatypeConstructor witnesses a branching constructor whose two fields both have the enclosing datatype sort.

func DeclareBinaryRecursiveDatatypeConstructor added in v0.38.0 

func DeclareBinaryRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, name string, firstSelectorName string, secondSelectorName string) BinaryRecursiveDatatypeConstructor

type BitVecDatatypeFieldSort added in v0.40.0 

type BitVecDatatypeFieldSort struct {
	Width int
}

type BitVecSort 

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

type BitVectorArrayEqualityExchange 

type BitVectorArrayEqualityExchange struct {
	Equality BitVectorEUFRelation
	Read     BitVectorArrayStoreReadValueRelation
}

BitVectorArrayEqualityExchange fuses an address equality with the array read that consumes it, avoiding general term allocation on the hot path.

type BitVectorArrayEqualityRelation added in v0.29.0 

type BitVectorArrayEqualityRelation struct {
	LeftID, RightID          int
	IndexWidth, ElementWidth int
	Negated                  bool
}

type BitVectorArrayStoreReadValueRelation 

type BitVectorArrayStoreReadValueRelation struct {
	ArrayID, StoreIndexID, ReadIndexID int
	IndexWidth, ElementWidth           int
	StoredValue, ComparedValue         BitVectorValue
	Negated                            bool
}

BitVectorArrayStoreReadValueRelation is the compact official-API form of a symbolic-address read from a one-store array compared with an exact value.

type BitVectorConjunction 

type BitVectorConjunction struct {
	Count    int
	Inline   [4]BitVectorRelation
	Overflow []BitVectorRelation
}

type BitVectorEUFConjunction 

type BitVectorEUFConjunction struct {
	Count    int
	Inline   [4]BitVectorEUFRelation
	Overflow []BitVectorEUFRelation
}

type BitVectorEUFRelation 

type BitVectorEUFRelation struct {
	Left    BitVectorEUFTerm
	Right   BitVectorEUFTerm
	Negated bool
}

type BitVectorEUFTerm 

type BitVectorEUFTerm struct {
	Kind       uint8
	Width      int
	SymbolID   int
	FunctionID int
	FirstID    int
	FirstWidth int
}

type BitVectorIntegerRelation 

type BitVectorIntegerRelation struct {
	SymbolID  int
	Width     int
	Signed    bool
	Constant  IntegerValue
	Operation int8
	Reverse   bool
	Negated   bool
}

BitVectorIntegerRelation is the compact, allocation-free boundary between a bit-vector symbol conversion and an exact integer constant.

func CompactBitVectorIntegerEquality 

func CompactBitVectorIntegerEquality(left, right Term[IntSort]) (BitVectorIntegerRelation, bool)

CompactBitVectorIntegerEquality recognizes the common symbol-conversion equality without exposing the internal indexed term representation.

type BitVectorMixedConjunction 

type BitVectorMixedConjunction struct {
	BitVectorCount int
	BitVectors     [4]BitVectorRelation
	IntegerCount   int
	Integers       [4]BitVectorIntegerRelation
}

type BitVectorRelation 

type BitVectorRelation struct {
	Width      int
	SymbolID   int
	Value      BitVectorValue
	Mask       BitVectorValue
	Masked     bool
	Negated    bool
	Order      uint8
	Operation  uint8
	Operand    BitVectorValue
	ParameterA int
	ParameterB int
	Predicate  uint8
}

BitVectorRelation is a compact unary equality or disequality retained by compatibility layers. If Masked is set it denotes symbol & Mask = Value.

type BitVectorValue 

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

BitVectorValue is an exact unsigned bit pattern with an explicit positive width. Values are reduced modulo 2^width. Widths through 64 stay inline; larger values retain an arbitrary-precision representation.

func AddBitVectorValue 

func AddBitVectorValue(left, right BitVectorValue) BitVectorValue

func AndBitVectorValue 

func AndBitVectorValue(left, right BitVectorValue) BitVectorValue

func ArithmeticShiftRightBitVectorValue 

func ArithmeticShiftRightBitVectorValue(value, amount BitVectorValue) BitVectorValue

func BitVecModelValue 

func BitVecModelValue(model Model, term Term[BitVecSort]) (BitVectorValue, bool)

func BitVectorArrayValue added in v0.29.0 

func BitVectorArrayValue(model Model, array Term[ArraySort[BitVecSort, BitVecSort]], index BitVectorValue) (BitVectorValue, bool)

func ConcatBitVectorValue 

func ConcatBitVectorValue(first, second BitVectorValue) BitVectorValue

func ExtractBitVectorValue 

func ExtractBitVectorValue(value BitVectorValue, high, low int) BitVectorValue

func IntegerToBitVectorValue 

func IntegerToBitVectorValue(width int, value IntegerValue) BitVectorValue

func LogicalShiftRightBitVectorValue 

func LogicalShiftRightBitVectorValue(value, amount BitVectorValue) BitVectorValue

func MulBitVectorValue 

func MulBitVectorValue(left, right BitVectorValue) BitVectorValue

func NewBitVectorUint64 

func NewBitVectorUint64(width int, value uint64) BitVectorValue

func NotBitVectorValue 

func NotBitVectorValue(value BitVectorValue) BitVectorValue

func OrBitVectorValue 

func OrBitVectorValue(left, right BitVectorValue) BitVectorValue

func ParseBitVector 

func ParseBitVector(width int, value string) (BitVectorValue, error)

func RepeatBitVectorValue 

func RepeatBitVectorValue(value BitVectorValue, count int) BitVectorValue

func RotateLeftBitVectorValue 

func RotateLeftBitVectorValue(value BitVectorValue, amount int) BitVectorValue

func RotateRightBitVectorValue 

func RotateRightBitVectorValue(value BitVectorValue, amount int) BitVectorValue

func ShiftLeftBitVectorValue 

func ShiftLeftBitVectorValue(value, amount BitVectorValue) BitVectorValue

func SignExtendBitVectorValue 

func SignExtendBitVectorValue(value BitVectorValue, additional int) BitVectorValue

func SignedDivBitVectorValue 

func SignedDivBitVectorValue(left, right BitVectorValue) BitVectorValue

func SignedRemBitVectorValue 

func SignedRemBitVectorValue(left, right BitVectorValue) BitVectorValue

func SubBitVectorValue 

func SubBitVectorValue(left, right BitVectorValue) BitVectorValue

func UnsignedDivBitVectorValue 

func UnsignedDivBitVectorValue(left, right BitVectorValue) BitVectorValue

func UnsignedRemBitVectorValue 

func UnsignedRemBitVectorValue(left, right BitVectorValue) BitVectorValue

func XorBitVectorValue 

func XorBitVectorValue(left, right BitVectorValue) BitVectorValue

func ZeroExtendBitVectorValue 

func ZeroExtendBitVectorValue(value BitVectorValue, additional int) BitVectorValue

func (BitVectorValue) Bit 

func (value BitVectorValue) Bit(index int) bool

func (BitVectorValue) Uint64 

func (value BitVectorValue) Uint64() (uint64, bool)

func (BitVectorValue) Width 

func (value BitVectorValue) Width() int

type Bool 

type Bool struct {
	Value bool
}

type BoolDatatypeFieldSort added in v0.40.0 

type BoolDatatypeFieldSort struct{}

type BoolSort 

type BoolSort struct{}

type BoolSymbol 

type BoolSymbol struct {
	ID   int
	Name string
}

type BooleanCNF 

type BooleanCNF struct {
	Literals   []int
	ClauseEnds []int
}

type BooleanClause 

type BooleanClause struct {
	Literals []int
}

type BooleanConjunction 

type BooleanConjunction struct {
	Count           int
	InlineTerms     [4]Term[BoolSort]
	InlineNegated   [4]bool
	OverflowTerms   []Term[BoolSort]
	OverflowNegated []bool
}

BooleanConjunction is a compact conjunction with per-item polarity. It lets compatibility layers fuse Not/And construction while preserving ordinary Boolean semantics for every solver backend.

type BooleanInlineCNF added in v0.34.0 

type BooleanInlineCNF struct {
	LiteralCount int
	ClauseCount  int
	Literals     [16]int
	ClauseEnds   [8]int
}

BooleanInlineCNF is the allocation-free representation for small authored CNF systems. Literals use the public BooleanVariable convention encoded as +(ID+1) and -(ID+1); ClauseEnds contains cumulative literal counts. Larger systems continue to use BooleanCNF and the watched-literal solver.

type BooleanVariable 

type BooleanVariable struct {
	ID int
}

type Canceled 

type Canceled struct{}

type CheckResult 

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

func Check 

func Check(solver Solver) CheckResult

type CheckResultCases 

type CheckResultCases[R any] struct {
	Satisfiable   func(Value Model) R
	Unsatisfiable func(Value Proof) R
	Unknown       func(Context Proof, Reason UnknownReason) R
}

CheckResultCases selects one handler per CheckResult variant for CheckResultFold.

type Checkpoint 

type Checkpoint = checkpointValue

Checkpoint packages the pre-push context. Restore requires the exact checkpoint rather than accepting an untyped integer depth.

func Previous 

func Previous(pushed Pushed) Checkpoint

type CompactConditionalIntegerEUFSystem added in v0.121.0 

type CompactConditionalIntegerEUFSystem struct {
	Base        CompactIntegerEUFSystem
	Conditional IntegerConditionalComparison
}

type CompactGroundIndexedStringFormula added in v0.111.0 

type CompactGroundIndexedStringFormula struct {
	AssignmentCount uint8
	Assignments     [4]IntegerLinearEquality
	EqualityCount   uint8
	Equalities      [4]CompactStringIndexedEquality
}

CompactGroundIndexedStringFormula groups ground integer assignments with indexed-string equalities without allocating an interface-backed conjunction.

type CompactGroundStringEvaluationFormula added in v0.112.0 

type CompactGroundStringEvaluationFormula struct {
	StringAssignmentCount  uint8
	StringAssignments      [4]CompactStringRelation
	IntegerAssignmentCount uint8
	IntegerAssignments     [4]IntegerLinearEquality
	IndexOfCount           uint8
	IndexOf                [4]CompactStringIndexOfEquality
}

CompactGroundStringEvaluationFormula groups direct ground assignments and derived index-of equalities without an allocating general conjunction.

type CompactIntegerEUFSystem added in v0.118.0 

type CompactIntegerEUFSystem struct {
	EqualityCount              int
	EqualityLeft               [4]int
	EqualityRight              [4]int
	OverflowEqualityLeft       []int
	OverflowEqualityRight      []int
	UnaryComparisonCount       int
	UnaryComparisons           [4]IntegerUnaryComparison
	OverflowUnaryComparisons   []IntegerUnaryComparison
	BinaryComparisonCount      int
	BinaryComparisons          [4]IntegerBinaryComparison
	OverflowBinaryComparisons  []IntegerBinaryComparison
	TernaryComparisonCount     int
	TernaryComparisons         [4]IntegerTernaryComparison
	OverflowTernaryComparisons []IntegerTernaryComparison
	DifferenceCount            int
	Differences                [4]IntegerDifferenceConstraint
	OverflowDifferences        []IntegerDifferenceConstraint
	RelationCount              int
	Relations                  [4]UninterpretedEUFRelation
	OverflowRelations          []UninterpretedEUFRelation
}

type CompactIntegerSequence added in v0.77.0 

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

CompactIntegerSequence is an inline ground Seq Int term used by typed façades to avoid allocating a unit/concat AST during construction.

func AppendCompactIntegerSequence added in v0.77.0 

func AppendCompactIntegerSequence(
	left,
	right CompactIntegerSequence,
) CompactIntegerSequence

AppendCompactIntegerSequence appends right to left.

func EmptyCompactIntegerSequence added in v0.77.0 

func EmptyCompactIntegerSequence() CompactIntegerSequence

EmptyCompactIntegerSequence constructs an empty compact sequence.

func UnitCompactIntegerSequence added in v0.77.0 

func UnitCompactIntegerSequence(element IntegerValue) CompactIntegerSequence

UnitCompactIntegerSequence constructs a one-element compact sequence.

type CompactStringBooleanFormula added in v0.58.0 

type CompactStringBooleanFormula struct {
	AtomCount int
	NodeCount int
	Atoms     [4]CompactStringRegexLiteralAtom
	Nodes     [32]uint8
}

CompactStringBooleanFormula is an allocation-free postfix formula over up to four singleton-regex membership atoms. Larger formulas use the general Boolean and regular-expression terms.

func CompactStringBooleanAndFormula added in v0.58.0 

func CompactStringBooleanAndFormula(left, right CompactStringBooleanFormula) (CompactStringBooleanFormula, bool)

func CompactStringBooleanConstant added in v0.58.0 

func CompactStringBooleanConstant(value bool) CompactStringBooleanFormula

func CompactStringBooleanNotFormula added in v0.58.0 

func CompactStringBooleanNotFormula(value CompactStringBooleanFormula) (CompactStringBooleanFormula, bool)

func CompactStringBooleanOrFormula added in v0.58.0 

func CompactStringBooleanOrFormula(left, right CompactStringBooleanFormula) (CompactStringBooleanFormula, bool)

func CompactStringRegexLiteralFormula added in v0.58.0 

func CompactStringRegexLiteralFormula(symbol CompactStringTerm, literal string) (CompactStringBooleanFormula, bool)

type CompactStringIndexOfEquality added in v0.112.0 

type CompactStringIndexOfEquality struct {
	TextID       int
	TextName     string
	NeedleID     int
	NeedleName   string
	Offset       int64
	OffsetID     int
	OffsetName   string
	OffsetSymbol bool
	Result       int64
	ResultID     int
	ResultName   string
	ResultSymbol bool
}

CompactStringIndexOfEquality represents str.indexof(text, needle, offset) = result for direct symbols.

type CompactStringIndexedEquality added in v0.102.0 

type CompactStringIndexedEquality struct {
	Kind         uint8
	SymbolID     int
	SymbolName   string
	Offset       int64
	OffsetID     int
	OffsetName   string
	OffsetSymbol bool
	Length       int64
	LengthID     int
	LengthName   string
	LengthSymbol bool
	Target       string
}

CompactStringIndexedEquality is the allocation-light representation of a direct-symbol str.at or str.substr equality with ground indices and result. Kind is CompactStringAtEquality or CompactStringSubstringEquality; Offset is the at index or substring offset, and Length is used by substring.

type CompactStringLengthRelation added in v0.73.0 

type CompactStringLengthRelation struct {
	Left  CompactStringTerm
	Right CompactStringTerm
	Order uint8
}

CompactStringLengthRelation compares the code-point lengths of two compact string expressions. Order is 0 for equality, 1 for strict less-than, and 2 for less-than-or-equal.

type CompactStringPattern added in v0.59.0 

type CompactStringPattern struct {
	Count       int
	SymbolIDs   [4]int
	SymbolNames [4]string
	Delimiters  [5]string
}

CompactStringPattern is a bounded literal-delimited sequence of string symbols. Delimiters[0] is the prefix, Delimiters[Count] the suffix, and the intervening entries separate adjacent symbols.

type CompactStringRegexLiteralAtom added in v0.58.0 

type CompactStringRegexLiteralAtom struct {
	SymbolID   int
	SymbolName string
	Literal    string
}

type CompactStringRelation added in v0.52.0 

type CompactStringRelation struct {
	Kind    uint8
	Negated bool
	Left    CompactStringTerm
	Right   CompactStringTerm
	Integer int64
}

type CompactStringReplaceEquality added in v0.104.0 

type CompactStringReplaceEquality struct {
	SymbolID          int
	SymbolName        string
	Source            string
	SourceID          int
	SourceName        string
	SourceSymbol      bool
	Replacement       string
	ReplacementID     int
	ReplacementName   string
	ReplacementSymbol bool
	Target            string
	TargetID          int
	TargetName        string
	TargetSymbol      bool
	All               bool
}

CompactStringReplaceEquality is the allocation-light representation of str.replace(x, source, replacement) = target for a direct symbol x and ground string operands.

type CompactStringSystem added in v0.52.0 

type CompactStringSystem struct {
	Count    int
	Inline   [8]CompactStringRelation
	Overflow []CompactStringRelation
}

func AppendCompactStringRelation added in v0.52.0 

func AppendCompactStringRelation(system CompactStringSystem, relation CompactStringRelation) CompactStringSystem

type CompactStringTerm added in v0.52.0 

type CompactStringTerm struct {
	Kind   uint8
	ID     int
	Name   string
	Value  string
	Suffix string
}

func CompactStringLiteralTerm added in v0.52.0 

func CompactStringLiteralTerm(value string) CompactStringTerm

func CompactStringSingleSymbolConcatTerm added in v0.58.0 

func CompactStringSingleSymbolConcatTerm(prefix string, id int, name, suffix string) CompactStringTerm

func CompactStringSymbolTerm added in v0.52.0 

func CompactStringSymbolTerm(id int, name string) CompactStringTerm

type CompactStringWordEquation added in v0.59.0 

type CompactStringWordEquation struct {
	Pattern CompactStringPattern
	Target  string
}

CompactStringWordEquation equates a bounded symbolic pattern with a ground target. Standalone solving searches all bounded splits; conjunction propagation only commits uniquely forced splits.

type DatatypeChildren added in v0.39.0 

type DatatypeChildren struct {
	Count    int
	Inline   [4]DatatypeValue
	Overflow []DatatypeValue
}

DatatypeChildren keeps the common arity-at-most-four case in one retained object while permitting arbitrary arity. DatatypeValue itself remains comparable because it contains only this pointer, preserving generated equality APIs in packages that embed model values.

func (*DatatypeChildren) At added in v0.39.0 

func (children *DatatypeChildren) At(index int) (DatatypeValue, bool)

func (*DatatypeChildren) Len added in v0.39.0 

func (children *DatatypeChildren) Len() int

type DatatypeFieldCons added in v0.40.0 

type DatatypeFieldCons struct {
	Head DatatypeFieldSort
	Tail DatatypeFieldList
}

type DatatypeFieldList added in v0.40.0 

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

func DatatypeFieldListChildren added in v0.40.0 

func DatatypeFieldListChildren(d DatatypeFieldList) []DatatypeFieldList

DatatypeFieldListChildren lists the direct DatatypeFieldList subterms of d.

func DatatypeFieldListTransform added in v0.40.0 

func DatatypeFieldListTransform(d DatatypeFieldList, f func(DatatypeFieldList) DatatypeFieldList) DatatypeFieldList

DatatypeFieldListTransform rewrites d bottom-up: children first, then f at each node.

type DatatypeFieldListCases added in v0.40.0 

type DatatypeFieldListCases[R any] struct {
	NoDatatypeFields  func() R
	DatatypeFieldCons func(Head DatatypeFieldSort, Tail DatatypeFieldList) R
}

DatatypeFieldListCases selects one handler per DatatypeFieldList variant for DatatypeFieldListFold.

type DatatypeFieldListEqOverrides added in v0.40.0 

type DatatypeFieldListEqOverrides struct {
	NoDatatypeFields  func(x, y NoDatatypeFields) (eq, handled bool)
	DatatypeFieldCons func(x, y DatatypeFieldCons) (eq, handled bool)
}

DatatypeFieldListEqOverrides carries optional per-variant hooks for DatatypeFieldListEqualWith. A hook returning handled=false falls through to the derived comparison.

type DatatypeFieldSort added in v0.40.0 

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

DatatypeFieldSort is the first-order universe of field sorts supported by the native mixed-datatype kernel. DatatypeFieldList is a recursive index domain, so a signature is a genuine type-level heterogeneous list.

type DatatypeFieldSortCases added in v0.40.0 

type DatatypeFieldSortCases[R any] struct {
	BoolDatatypeFieldSort      func() R
	IntDatatypeFieldSort       func() R
	RealDatatypeFieldSort      func() R
	BitVecDatatypeFieldSort    func(Width int) R
	SelfDatatypeFieldSort      func() R
	DatatypeReferenceFieldSort func(Datatype int, Constructors int) R
}

DatatypeFieldSortCases selects one handler per DatatypeFieldSort variant for DatatypeFieldSortFold.

type DatatypeFieldSortEqOverrides added in v0.40.0 

type DatatypeFieldSortEqOverrides struct {
	BoolDatatypeFieldSort      func(x, y BoolDatatypeFieldSort) (eq, handled bool)
	IntDatatypeFieldSort       func(x, y IntDatatypeFieldSort) (eq, handled bool)
	RealDatatypeFieldSort      func(x, y RealDatatypeFieldSort) (eq, handled bool)
	BitVecDatatypeFieldSort    func(x, y BitVecDatatypeFieldSort) (eq, handled bool)
	SelfDatatypeFieldSort      func(x, y SelfDatatypeFieldSort) (eq, handled bool)
	DatatypeReferenceFieldSort func(x, y DatatypeReferenceFieldSort) (eq, handled bool)
}

DatatypeFieldSortEqOverrides carries optional per-variant hooks for DatatypeFieldSortEqualWith. A hook returning handled=false falls through to the derived comparison.

type DatatypeFieldValue added in v0.40.0 

type DatatypeFieldValue struct {
	Kind      int
	Width     int
	Boolean   bool
	Integer   IntegerValue
	Real      Rational
	BitVector BitVectorValue
	Datatype  *DatatypeValue
}

DatatypeFieldValue is one exact field in a mixed-constructor model. Exactly one value member is meaningful according to Kind.

type DatatypeFields added in v0.40.0 

type DatatypeFields struct {
	Count    int
	Inline   [4]DatatypeFieldValue
	Overflow []DatatypeFieldValue
}

func (*DatatypeFields) At added in v0.40.0 

func (fields *DatatypeFields) At(index int) (DatatypeFieldValue, bool)

func (*DatatypeFields) Len added in v0.40.0 

func (fields *DatatypeFields) Len() int

type DatatypeReferenceFieldSort added in v0.41.0 

type DatatypeReferenceFieldSort struct {
	Datatype     int
	Constructors int
}

type DatatypeSort added in v0.36.0 

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

DatatypeSort retains both the declaration identity and finite constructor cardinality. Go+ therefore rejects terms from distinct datatype declarations even when they happen to have the same number of constructors.

type DatatypeValue added in v0.36.0 

type DatatypeValue struct {
	DatatypeID       int
	ConstructorCount int
	ConstructorID    int
	ConstructorName  string
	Child            *DatatypeValue
	SecondChild      *DatatypeValue
	// Children is populated for arbitrary-arity recursive constructors. Unary
	// and binary values retain Child/SecondChild for source compatibility.
	Children *DatatypeChildren
	// Fields is populated for mixed-sort recursive constructors.
	Fields *DatatypeFields
}

DatatypeValue is the exact model value of a supported algebraic datatype. IDs are declaration-local ordinals; ConstructorName is retained when the corresponding constructor appeared in the authored formula.

func DatatypeModelValue added in v0.36.0 

func DatatypeModelValue(datatype int, constructors int, model Model, term Term[DatatypeSort]) (DatatypeValue, bool)

type EmptyMixedDatatypeArguments added in v0.40.0 

type EmptyMixedDatatypeArguments struct{}

type EmptyMixedDatatypeSignature added in v0.40.0 

type EmptyMixedDatatypeSignature struct{}

type Equal 

type Equal struct {
	Left  any
	Right any
}

type FirstDatatypeField added in v0.38.0 

type FirstDatatypeField struct{}

type If 

type If[S any] struct {
	Condition Term[BoolSort]
	Then      Term[S]
	Else      Term[S]
}

type Iff 

type Iff struct {
	Left  Term[BoolSort]
	Right Term[BoolSort]
}

type Implies 

type Implies struct {
	Left  Term[BoolSort]
	Right Term[BoolSort]
}

type IntDatatypeFieldSort added in v0.40.0 

type IntDatatypeFieldSort struct{}

type IntSort 

type IntSort struct{}

type IntSymbol 

type IntSymbol struct {
	ID   int
	Name string
}

type Integer 

type Integer struct {
	Value int64
}

type IntegerBinaryComparison added in v0.118.0 

type IntegerBinaryComparison struct {
	FunctionID        int
	FirstArgumentID   int
	SecondArgumentID  int
	Bound             IntegerValue
	ApplicationOnLeft bool
	Strict            bool
}

type IntegerConditionalBranch added in v0.121.0 

type IntegerConditionalBranch struct {
	Application bool
	FunctionID  int
	ArgumentID  int
	Constant    IntegerValue
}

type IntegerConditionalComparison added in v0.121.0 

type IntegerConditionalComparison struct {
	Condition         IntegerDifferenceConstraint
	Then              IntegerConditionalBranch
	Else              IntegerConditionalBranch
	Bound             IntegerValue
	ApplicationOnLeft bool
	Strict            bool
}

type IntegerDifferenceConstraint 

type IntegerDifferenceConstraint struct {
	PositiveID  int
	NegativeID  int
	HasPositive bool
	HasNegative bool
	Bound       int64
	WideBound   IntegerValue
	Wide        bool
	Strict      bool
}

type IntegerDifferenceSystem 

type IntegerDifferenceSystem struct {
	Count    int
	Inline   [4]IntegerDifferenceConstraint
	Overflow []IntegerDifferenceConstraint
}

type IntegerDiv added in v0.33.0 

type IntegerDiv struct {
	Dividend Term[IntSort]
	Divisor  IntegerValue
}

type IntegerDivModRelation added in v0.33.0 

type IntegerDivModRelation struct {
	SymbolID  int
	Divisor   IntegerValue
	Expected  IntegerValue
	Remainder bool
}

func CompactIntegerDivModEquality added in v0.33.0 

func CompactIntegerDivModEquality(left, right Term[IntSort]) (IntegerDivModRelation, bool)

type IntegerDivModSystem added in v0.33.0 

type IntegerDivModSystem struct {
	EqualityCount int
	RelationCount int
	Equalities    [4]IntegerLinearEquality
	Relations     [4]IntegerDivModRelation
}

type IntegerLinearChoice added in v0.32.0 

type IntegerLinearChoice struct {
	First  IntegerLinearEquality
	Second IntegerLinearEquality
}

type IntegerLinearDisequality added in v0.32.0 

type IntegerLinearDisequality struct{ Equality IntegerLinearEquality }

type IntegerLinearEquality added in v0.30.0 

type IntegerLinearEquality struct {
	ID          int
	Coefficient int64
	Value       IntegerValue
}

IntegerLinearEquality is the allocation-conscious normal form a compatibility layer can use for coefficient*x = value.

func CompactIntegerLinearEquality added in v0.30.0 

func CompactIntegerLinearEquality(left, right Term[IntSort]) (IntegerLinearEquality, bool)

type IntegerMod added in v0.33.0 

type IntegerMod struct {
	Dividend Term[IntSort]
	Divisor  IntegerValue
}

type IntegerScale added in v0.30.0 

type IntegerScale struct {
	Coefficient IntegerValue
	Value       Term[IntSort]
}

type IntegerSequenceValue added in v0.77.0 

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

IntegerSequenceValue is an exact ground Seq Int value. The first eight elements remain inline so ordinary constructed sequences need no result allocation.

func IntegerSequenceModelValue added in v0.77.0 

func IntegerSequenceModelValue(
	model Model,
	term Term[SequenceSort[IntSort]],
) (IntegerSequenceValue, bool)

IntegerSequenceModelValue evaluates an integer sequence in model.

func IntegerSequenceSymbolModelValue added in v0.100.0 

func IntegerSequenceSymbolModelValue(
	model Model,
	id int,
) (IntegerSequenceValue, bool)

IntegerSequenceSymbolModelValue returns the exact value of an integer sequence symbol without materializing an expression node.

func (IntegerSequenceValue) At added in v0.77.0 

func (value IntegerSequenceValue) At(index int) (IntegerValue, bool)

At returns the element at index.

func (IntegerSequenceValue) Len added in v0.77.0 

func (value IntegerSequenceValue) Len() int

Len reports the number of elements.

type IntegerTernaryComparison added in v0.119.0 

type IntegerTernaryComparison struct {
	FunctionID        int
	FirstArgumentID   int
	SecondArgumentID  int
	ThirdArgumentID   int
	Bound             IntegerValue
	ApplicationOnLeft bool
	Strict            bool
}

type IntegerUnaryComparison added in v0.118.0 

type IntegerUnaryComparison struct {
	FunctionID        int
	ArgumentID        int
	Bound             IntegerValue
	ApplicationOnLeft bool
	Strict            bool
}

type IntegerValue 

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

IntegerValue is an exact mathematical integer. Values fitting int64 remain inline; larger magnitudes use an immutable arbitrary-precision payload.

func AddIntegerValue 

func AddIntegerValue(left, right IntegerValue) IntegerValue

func BitVectorToIntegerValue 

func BitVectorToIntegerValue(value BitVectorValue, signed bool) IntegerValue

func ExactIntValue 

func ExactIntValue(model Model, term Term[IntSort]) (IntegerValue, bool)

func ExactIntegerConstant 

func ExactIntegerConstant(term Term[IntSort]) (IntegerValue, bool)

ExactIntegerConstant exposes constant folding to compatibility layers while keeping symbolic integer terms opaque.

func ExactStringIntegerModelValue added in v0.54.0 

func ExactStringIntegerModelValue(model Model, term Term[IntSort]) (IntegerValue, bool)

func IntegerArrayValue 

func IntegerArrayValue(model Model, array Term[ArraySort[IntSort, IntSort]], index IntegerValue) (IntegerValue, bool)

func IntegerModelValue 

func IntegerModelValue(model Model, term Term[IntSort]) (IntegerValue, bool)

func MultiplyIntegerValue added in v0.30.0 

func MultiplyIntegerValue(left, right IntegerValue) IntegerValue

func NegateIntegerValue 

func NegateIntegerValue(value IntegerValue) IntegerValue

func NewIntegerValue 

func NewIntegerValue(value int64) IntegerValue

func ParseIntegerValue 

func ParseIntegerValue(text string) (IntegerValue, error)

func SubIntegerValue 

func SubIntegerValue(left, right IntegerValue) IntegerValue

func (IntegerValue) Int64 

func (value IntegerValue) Int64() (int64, bool)

func (IntegerValue) String 

func (value IntegerValue) String() string

type Less 

type Less struct {
	Left  Term[IntSort]
	Right Term[IntSort]
}

type LessEqual 

type LessEqual struct {
	Left  Term[IntSort]
	Right Term[IntSort]
}

type LinearRealConstraint 

type LinearRealConstraint struct {
	Count                int
	Symbols              [4]int
	Coefficients         [4]Rational
	OverflowSymbols      []int
	OverflowCoefficients []Rational
	Constant             Rational
	Strict               bool
}

LinearRealConstraint is a compact affine relation used by compatibility layers that already normalized a linear expression. The inline form keeps common constraints allocation-free; the overflow fields preserve an unbounded surface for larger expressions.

type LinearRealSystem 

type LinearRealSystem struct {
	Count    int
	Inline   [4]LinearRealConstraint
	Overflow []LinearRealConstraint
}

LinearRealSystem is an allocation-conscious conjunction of normalized affine constraints. Four relations cover common small solver queries; overflow remains available for unbounded inputs.

type MixedDatatypeArguments added in v0.40.0 

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

func BitVecDatatypeArgument added in v0.40.0 

func BitVecDatatypeArgument(width int, value Term[BitVecSort], rest MixedDatatypeArguments) MixedDatatypeArguments

func BoolDatatypeArgument added in v0.40.0 

func BoolDatatypeArgument(value Term[BoolSort], rest MixedDatatypeArguments) MixedDatatypeArguments

func DatatypeReferenceArgument added in v0.41.0 

func DatatypeReferenceArgument(targetDatatype int, targetConstructors int, value Term[DatatypeSort], rest MixedDatatypeArguments) MixedDatatypeArguments

func EmptyMixedDatatypeArgumentsFor added in v0.41.0 

func EmptyMixedDatatypeArgumentsFor(datatype int, constructors int) MixedDatatypeArguments

func IntDatatypeArgument added in v0.40.0 

func IntDatatypeArgument(value Term[IntSort], rest MixedDatatypeArguments) MixedDatatypeArguments

func RealDatatypeArgument added in v0.40.0 

func RealDatatypeArgument(value Term[RealSort], rest MixedDatatypeArguments) MixedDatatypeArguments

func SelfDatatypeArgument added in v0.40.0 

func SelfDatatypeArgument(value Term[DatatypeSort], rest MixedDatatypeArguments) MixedDatatypeArguments

type MixedDatatypeCursor added in v0.40.0 

type MixedDatatypeCursor = mixedDatatypeCursorValue

MixedDatatypeCursor is a typed cursor into a constructor signature. Moving to the tail changes its list index; selecting the head therefore returns the statically correct SMT sort without an untyped field-number API.

func MixedDatatypeFields added in v0.40.0 

func MixedDatatypeFields(declaration MixedRecursiveDatatypeConstructor) MixedDatatypeCursor

func NextMixedDatatypeField added in v0.40.0 

func NextMixedDatatypeField(cursor MixedDatatypeCursor) MixedDatatypeCursor

type MixedDatatypeFieldSpec added in v0.40.0 

type MixedDatatypeFieldSpec struct {
	Kind             int
	Width            int
	Name             string
	DatatypeID       int
	ConstructorCount int
}

type MixedDatatypeFieldSpecs added in v0.40.0 

type MixedDatatypeFieldSpecs struct {
	Count    int
	Inline   [4]MixedDatatypeFieldSpec
	Overflow []MixedDatatypeFieldSpec
}

func (MixedDatatypeFieldSpecs) At added in v0.40.0 

func (specs MixedDatatypeFieldSpecs) At(index int) MixedDatatypeFieldSpec

func (MixedDatatypeFieldSpecs) Len added in v0.40.0 

func (specs MixedDatatypeFieldSpecs) Len() int

type MixedDatatypeSignature added in v0.40.0 

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

func BitVecDatatypeField added in v0.40.0 

func BitVecDatatypeField(width int, name string, rest MixedDatatypeSignature) MixedDatatypeSignature

func BoolDatatypeField added in v0.40.0 

func BoolDatatypeField(name string, rest MixedDatatypeSignature) MixedDatatypeSignature

func DatatypeReferenceField added in v0.41.0 

func DatatypeReferenceField(targetDatatype int, targetConstructors int, name string, rest MixedDatatypeSignature) MixedDatatypeSignature

func IntDatatypeField added in v0.40.0 

func IntDatatypeField(name string, rest MixedDatatypeSignature) MixedDatatypeSignature

func RealDatatypeField added in v0.40.0 

func RealDatatypeField(name string, rest MixedDatatypeSignature) MixedDatatypeSignature

func SelfDatatypeField added in v0.40.0 

func SelfDatatypeField(name string, rest MixedDatatypeSignature) MixedDatatypeSignature

type MixedDatatypeTermValue added in v0.40.0 

type MixedDatatypeTermValue struct {
	Kind             int
	Width            int
	Term             any
	DatatypeID       int
	ConstructorCount int
}

type MixedDatatypeTermValues added in v0.40.0 

type MixedDatatypeTermValues struct {
	Count    int
	Inline   [4]MixedDatatypeTermValue
	Overflow []MixedDatatypeTermValue
}

func (MixedDatatypeTermValues) At added in v0.40.0 

func (values MixedDatatypeTermValues) At(index int) MixedDatatypeTermValue

func (MixedDatatypeTermValues) Len added in v0.40.0 

func (values MixedDatatypeTermValues) Len() int

type MixedRecursiveDatatypeConstructor added in v0.40.0 

type MixedRecursiveDatatypeConstructor = mixedRecursiveDatatypeConstructorValue

func DeclareMixedRecursiveDatatypeConstructor added in v0.40.0 

func DeclareMixedRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, name string, signature MixedDatatypeSignature) MixedRecursiveDatatypeConstructor

type Model 

type Model = modelValue

Model[c] and Proof[c] can only be consumed with terms/assertions from the checked solver context that produced them.

type NaryDatatypeSelectors added in v0.39.0 

type NaryDatatypeSelectors struct {
	Count    int
	Inline   [4]string
	Overflow []string
}

NaryDatatypeSelectors is the compact erased representation of an indexed selector-name vector. Arity at most four requires no backing allocation.

func (*NaryDatatypeSelectors) Append added in v0.39.0 

func (values *NaryDatatypeSelectors) Append(value string)

func (NaryDatatypeSelectors) At added in v0.39.0 

func (values NaryDatatypeSelectors) At(index int) string

func (NaryDatatypeSelectors) Len added in v0.39.0 

func (values NaryDatatypeSelectors) Len() int

type NaryDatatypeTerms added in v0.39.0 

type NaryDatatypeTerms struct {
	Count    int
	Inline   [4]Term[DatatypeSort]
	Overflow []Term[DatatypeSort]
}

NaryDatatypeTerms is the compact erased representation of an indexed term vector. Arity at most four remains entirely inline.

func (*NaryDatatypeTerms) Append added in v0.39.0 

func (values *NaryDatatypeTerms) Append(value Term[DatatypeSort])

func (NaryDatatypeTerms) At added in v0.39.0 

func (values NaryDatatypeTerms) At(index int) Term[DatatypeSort]

func (NaryDatatypeTerms) Len added in v0.39.0 

func (values NaryDatatypeTerms) Len() int

type NaryRecursiveDatatypeConstructor added in v0.39.0 

type NaryRecursiveDatatypeConstructor = naryRecursiveDatatypeConstructorValue

NaryRecursiveDatatypeConstructor witnesses an arbitrary nonempty vector of fields, all recursively carrying the enclosing datatype sort. Its arity is a dependent index shared by declaration, application, and selector proof.

func DeclareNaryRecursiveDatatypeConstructor added in v0.39.0 

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

func DeclareNaryRecursiveDatatypeConstructorCompact added in v0.39.0 

func DeclareNaryRecursiveDatatypeConstructorCompact(datatype, constructors, constructor int, name string, names NaryDatatypeSelectors) NaryRecursiveDatatypeConstructor

DeclareNaryRecursiveDatatypeConstructorCompact is the allocation-free erased boundary used by generated façades and SMT-LIB execution.

func DeclareNaryRecursiveDatatypeConstructorDynamic added in v0.39.0 

func DeclareNaryRecursiveDatatypeConstructorDynamic(datatype, constructors, constructor int, name string, selectorNames []string) NaryRecursiveDatatypeConstructor

DeclareNaryRecursiveDatatypeConstructorDynamic is the runtime-checked compatibility boundary for parsers and generated-Go façades that have already erased the arity index. Go+ callers should prefer the Vec-indexed DeclareNaryRecursiveDatatypeConstructor API.

type NegatedBooleanVariable 

type NegatedBooleanVariable struct {
	ID int
}

type NoDatatypeFields added in v0.40.0 

type NoDatatypeFields struct{}

type Not 

type Not struct {
	Value Term[BoolSort]
}

type Or 

type Or struct {
	Values []Term[BoolSort]
}

type Proof 

type Proof = proofValue

type PushResult 

type PushResult struct {
	Current  Solver
	Previous Checkpoint
}

type Pushed 

type Pushed = PushResult

func Push 

func Push(solver Solver) Pushed

type Rational 

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

Rational is an immutable arbitrary-precision rational. Its zero value is exactly zero. Operations never expose or mutate the retained big.Rat.

func AddRational 

func AddRational(left, right Rational) Rational

func DivideRational 

func DivideRational(left, right Rational) Rational

func MultiplyRational 

func MultiplyRational(left, right Rational) Rational

func MustParseRational 

func MustParseRational(text string) Rational

func NegateRational 

func NegateRational(value Rational) Rational

func NewRational 

func NewRational(numerator, denominator int64) Rational

func ParseRational 

func ParseRational(text string) (Rational, error)

func RealValue 

func RealValue(model Model, term Term[RealSort]) (Rational, bool)

func SubtractRational 

func SubtractRational(left, right Rational) Rational

func (Rational) Denominator 

func (value Rational) Denominator() string

func (Rational) IsInteger 

func (value Rational) IsInteger() bool

func (Rational) Numerator 

func (value Rational) Numerator() string

func (Rational) Sign 

func (value Rational) Sign() int

func (Rational) String 

func (value Rational) String() string

type Real 

type Real struct {
	Value Rational
}

type RealAdd 

type RealAdd struct {
	Values []Term[RealSort]
}

type RealBinaryComparison 

type RealBinaryComparison struct {
	FunctionID        int
	FirstArgumentID   int
	SecondArgumentID  int
	Bound             Rational
	ApplicationOnLeft bool
	Strict            bool
}

RealBinaryComparison compares one Real×Real->Real application with an exact rational bound without boxing the application tree.

type RealDatatypeFieldSort added in v0.40.0 

type RealDatatypeFieldSort struct{}

type RealLess 

type RealLess struct {
	Left  Term[RealSort]
	Right Term[RealSort]
}

type RealLessEqual 

type RealLessEqual struct {
	Left  Term[RealSort]
	Right Term[RealSort]
}

type RealScale 

type RealScale struct {
	Coefficient Rational
	Value       Term[RealSort]
}

type RealSort 

type RealSort struct{}

type RealSubtract 

type RealSubtract struct {
	Left  Term[RealSort]
	Right Term[RealSort]
}

type RealSymbol 

type RealSymbol struct {
	ID   int
	Name string
}

type RealSymbolEquality 

type RealSymbolEquality struct {
	LeftID  int
	RightID int
}

RealSymbolEquality is the normalized equality of two named real symbols.

type RealUnaryComparison 

type RealUnaryComparison struct {
	FunctionID        int
	ArgumentID        int
	Bound             Rational
	ApplicationOnLeft bool
	Strict            bool
}

RealUnaryComparison compares one Real->Real application with an exact constant. When ApplicationOnLeft is true it denotes f(x) op Bound; otherwise it denotes Bound op f(x). Strict selects < instead of <=.

type RealUnaryEquality 

type RealUnaryEquality struct {
	LeftFunctionID  int
	LeftArgumentID  int
	RightFunctionID int
	RightArgumentID int
}

RealUnaryEquality is the compact normalized equality of two applications of Real->Real uninterpreted functions to named real symbols.

type RecursiveDatatypeConstructor added in v0.37.0 

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

RecursiveDatatypeConstructor is a declaration witness for one unary constructor whose field recursively has the enclosing datatype sort.

func DeclareRecursiveDatatypeConstructor added in v0.37.0 

func DeclareRecursiveDatatypeConstructor(datatype int, constructors int, constructor int, name string, selectorName string) RecursiveDatatypeConstructor

type Regex added in v0.55.0 

type Regex[S any] struct {
	// contains filtered or unexported fields
}

func AllCharRegex added in v0.55.0 

func AllCharRegex[S any]() Regex[S]

func ComplementRegex added in v0.55.0 

func ComplementRegex[S any](value Regex[S]) Regex[S]

func ConcatRegex added in v0.55.0 

func ConcatRegex[S any](left, right Regex[S]) Regex[S]

func DifferenceRegex added in v0.55.0 

func DifferenceRegex[S any](left, right Regex[S]) Regex[S]

func EmptyRegex added in v0.55.0 

func EmptyRegex[S any]() Regex[S]

func FullRegex added in v0.55.0 

func FullRegex[S any]() Regex[S]

func IntersectRegex added in v0.55.0 

func IntersectRegex[S any](left, right Regex[S]) Regex[S]

func LoopRegex added in v0.55.0 

func LoopRegex[S any](minimum, maximum int, value Regex[S]) Regex[S]

func OptionalRegex added in v0.55.0 

func OptionalRegex[S any](value Regex[S]) Regex[S]

func PlusRegex added in v0.55.0 

func PlusRegex[S any](value Regex[S]) Regex[S]

func StarRegex added in v0.55.0 

func StarRegex[S any](value Regex[S]) Regex[S]

func StringLiteralRegex added in v0.56.0 

func StringLiteralRegex(value string) Regex[StringSort]

func StringRangeRegex added in v0.55.0 

func StringRangeRegex(low, high Term[StringSort]) Regex[StringSort]

func StringToRegex added in v0.55.0 

func StringToRegex(value Term[StringSort]) Regex[StringSort]

func StringValueRangeRegex added in v0.56.0 

func StringValueRangeRegex(low, high string) Regex[StringSort]

func UnionRegex added in v0.55.0 

func UnionRegex[S any](left, right Regex[S]) Regex[S]

type ResourceLimit 

type ResourceLimit struct {
	Limit int
}

type Satisfiable 

type Satisfiable struct {
	Value Model
}

type SecondDatatypeField added in v0.38.0 

type SecondDatatypeField struct{}

type SelfDatatypeFieldSort added in v0.40.0 

type SelfDatatypeFieldSort struct{}

type SequenceSort added in v0.50.0 

type SequenceSort[E any] interface {
	// contains filtered or unexported methods
}

SequenceSort retains its element sort in Go+ so sequence operations cannot mix incompatible alphabets. StringSort is the SMT-LIB Unicode-string specialization with native UTF-8 source representation.

type Solver 

type Solver = solverValue

Solver[c,d] has assertion fingerprint c and scope depth d. Constructors are sealed so generated Go callers cross runtime witness checks.

func Assert 

func Assert(assertion int, solver Solver, formula Term[BoolSort]) Solver

func Current 

func Current(pushed Pushed) Solver

func New 

func New() Solver

func Restore 

func Restore(solver Solver, checkpoint Checkpoint) Solver

type SomeBool 

type SomeBool struct {
	Value Term[BoolSort]
}

type SomeInt 

type SomeInt struct {
	Value Term[IntSort]
}

type SomeReal 

type SomeReal struct {
	Value Term[RealSort]
}

type SortedBinaryFunction 

type SortedBinaryFunction[A any, B any, R any] interface {
	// contains filtered or unexported methods
}

SortedBinaryFunction[A,B,R] extends typed binary EUF to built-in sorts. All three sort indices are checked before Go generation.

func DeclareBitVecBinaryFunction 

func DeclareBitVecBinaryFunction(firstWidth int, secondWidth int, rangeWidth int, id int, name string) SortedBinaryFunction[BitVecSort, BitVecSort, BitVecSort]

func DeclareIntBinaryFunction added in v0.117.0 

func DeclareIntBinaryFunction(id int, name string) SortedBinaryFunction[IntSort, IntSort, IntSort]

func DeclareIntBinaryPredicate added in v0.120.0 

func DeclareIntBinaryPredicate(id int, name string) SortedBinaryFunction[IntSort, IntSort, BoolSort]

func DeclareRealBinaryFunction 

func DeclareRealBinaryFunction(id int, name string) SortedBinaryFunction[RealSort, RealSort, RealSort]

func DeclareRealBinaryPredicate added in v0.122.0 

func DeclareRealBinaryPredicate(id int, name string) SortedBinaryFunction[RealSort, RealSort, BoolSort]

type SortedTernaryFunction added in v0.119.0 

type SortedTernaryFunction[A any, B any, C any, R any] interface {
	// contains filtered or unexported methods
}

SortedTernaryFunction[A,B,C,R] retains all three argument sorts and the result sort. Go+ rejects a misplaced argument before Go generation.

func DeclareIntTernaryFunction added in v0.119.0 

func DeclareIntTernaryFunction(id int, name string) SortedTernaryFunction[IntSort, IntSort, IntSort, IntSort]

type SortedUnaryFunction 

type SortedUnaryFunction[D any, R any] interface {
	// contains filtered or unexported methods
}

SortedUnaryFunction[D,R] extends typed EUF to built-in sorts. The type indices prevent applying a Real function to an Int or uninterpreted term.

func DeclareBitVecUnaryFunction 

func DeclareBitVecUnaryFunction(domainWidth int, rangeWidth int, id int, name string) SortedUnaryFunction[BitVecSort, BitVecSort]

func DeclareIntPredicate added in v0.120.0 

func DeclareIntPredicate(id int, name string) SortedUnaryFunction[IntSort, BoolSort]

func DeclareIntUnaryFunction added in v0.117.0 

func DeclareIntUnaryFunction(id int, name string) SortedUnaryFunction[IntSort, IntSort]

func DeclareRealPredicate added in v0.122.0 

func DeclareRealPredicate(id int, name string) SortedUnaryFunction[RealSort, BoolSort]

func DeclareRealUnaryFunction 

func DeclareRealUnaryFunction(id int, name string) SortedUnaryFunction[RealSort, RealSort]

type StringSort added in v0.50.0 

type StringSort struct{}

type Subtract 

type Subtract struct {
	Left  Term[IntSort]
	Right Term[IntSort]
}

type Term 

type Term[S any] interface {
	// contains filtered or unexported methods
}

Term[S] makes ill-sorted formulas unrepresentable in Go+.

func ApplyBinary 

func ApplyBinary(function BinaryFunction, left Term[UninterpretedSort], right Term[UninterpretedSort]) Term[UninterpretedSort]

func ApplyBinaryRecursiveDatatypeConstructor added in v0.38.0 

func ApplyBinaryRecursiveDatatypeConstructor(declaration BinaryRecursiveDatatypeConstructor, first Term[DatatypeSort], second Term[DatatypeSort]) Term[DatatypeSort]

func ApplyBitVecBinary 

func ApplyBitVecBinary(function SortedBinaryFunction[BitVecSort, BitVecSort, BitVecSort], first Term[BitVecSort], second Term[BitVecSort]) Term[BitVecSort]

func ApplyBitVecUnary 

func ApplyBitVecUnary(function SortedUnaryFunction[BitVecSort, BitVecSort], argument Term[BitVecSort]) Term[BitVecSort]

func ApplyMixedRecursiveDatatypeConstructor added in v0.40.0 

func ApplyMixedRecursiveDatatypeConstructor(declaration MixedRecursiveDatatypeConstructor, arguments MixedDatatypeArguments) Term[DatatypeSort]

func ApplyNaryRecursiveDatatypeConstructor added in v0.39.0 

func ApplyNaryRecursiveDatatypeConstructor(declaration NaryRecursiveDatatypeConstructor, values vec.Vec[Term[DatatypeSort]]) Term[DatatypeSort]

func ApplyNaryRecursiveDatatypeConstructorCompact added in v0.39.0 

func ApplyNaryRecursiveDatatypeConstructorCompact(declaration NaryRecursiveDatatypeConstructor, values NaryDatatypeTerms) Term[DatatypeSort]

ApplyNaryRecursiveDatatypeConstructorCompact checks an erased compact term vector without introducing a backing slice for the common small arities.

func ApplyNaryRecursiveDatatypeConstructorDynamic added in v0.39.0 

func ApplyNaryRecursiveDatatypeConstructorDynamic(declaration NaryRecursiveDatatypeConstructor, values []Term[DatatypeSort]) Term[DatatypeSort]

ApplyNaryRecursiveDatatypeConstructorDynamic checks erased arity and sort witnesses before retaining a normalized compact argument vector.

func ApplyRecursiveDatatypeConstructor added in v0.37.0 

func ApplyRecursiveDatatypeConstructor(declaration RecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[DatatypeSort]

func ApplySortedBinary 

func ApplySortedBinary[A any, B any, R any](function SortedBinaryFunction[A, B, R], first Term[A], second Term[B]) Term[R]

func ApplySortedTernary added in v0.119.0 

func ApplySortedTernary[A any, B any, C any, R any](function SortedTernaryFunction[A, B, C, R], first Term[A], second Term[B], third Term[C]) Term[R]

func ApplySortedUnary 

func ApplySortedUnary[D any, R any](function SortedUnaryFunction[D, R], argument Term[D]) Term[R]

func ApplyUnary 

func ApplyUnary(function UnaryFunction, argument Term[UninterpretedSort]) Term[UninterpretedSort]

func ArrayConst 

func ArrayConst[I any, E any](id int, name string) Term[ArraySort[I, E]]

func BitVecASHR 

func BitVecASHR(value Term[BitVecSort], amount Term[BitVecSort]) Term[BitVecSort]

func BitVecAdd 

func BitVecAdd(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecAnd 

func BitVecAnd(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecConcat 

func BitVecConcat(firstWidth int, secondWidth int, first Term[BitVecSort], second Term[BitVecSort]) Term[BitVecSort]

func BitVecConst 

func BitVecConst(width int, id int, name string) Term[BitVecSort]

func BitVecExtract 

func BitVecExtract(high int, low int, value Term[BitVecSort]) Term[BitVecSort]

func BitVecLSHR 

func BitVecLSHR(value Term[BitVecSort], amount Term[BitVecSort]) Term[BitVecSort]

func BitVecMul 

func BitVecMul(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecNegOverflow 

func BitVecNegOverflow(value Term[BitVecSort]) Term[BoolSort]

func BitVecNot 

func BitVecNot(value Term[BitVecSort]) Term[BitVecSort]

func BitVecOr 

func BitVecOr(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecRepeat 

func BitVecRepeat(count int, value Term[BitVecSort]) Term[BitVecSort]

func BitVecRotateLeft 

func BitVecRotateLeft(amount int, value Term[BitVecSort]) Term[BitVecSort]

func BitVecRotateRight 

func BitVecRotateRight(amount int, value Term[BitVecSort]) Term[BitVecSort]

func BitVecSAddOverflow 

func BitVecSAddOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSDiv 

func BitVecSDiv(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecSDivOverflow 

func BitVecSDivOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSHL 

func BitVecSHL(value Term[BitVecSort], amount Term[BitVecSort]) Term[BitVecSort]

func BitVecSLE 

func BitVecSLE(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSLT 

func BitVecSLT(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSMulOverflow 

func BitVecSMulOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSRem 

func BitVecSRem(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecSSubOverflow 

func BitVecSSubOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecSignExtend 

func BitVecSignExtend(additional int, value Term[BitVecSort]) Term[BitVecSort]

func BitVecSub 

func BitVecSub(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecToInt 

func BitVecToInt(value Term[BitVecSort]) Term[IntSort]

func BitVecToNat 

func BitVecToNat(value Term[BitVecSort]) Term[IntSort]

func BitVecUAddOverflow 

func BitVecUAddOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecUDiv 

func BitVecUDiv(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecULE 

func BitVecULE(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecULT 

func BitVecULT(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecUMulOverflow 

func BitVecUMulOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecURem 

func BitVecURem(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecUSubOverflow 

func BitVecUSubOverflow(left Term[BitVecSort], right Term[BitVecSort]) Term[BoolSort]

func BitVecVal 

func BitVecVal(width int, value uint64) Term[BitVecSort]

func BitVecXor 

func BitVecXor(left Term[BitVecSort], right Term[BitVecSort]) Term[BitVecSort]

func BitVecZeroExtend 

func BitVecZeroExtend(additional int, value Term[BitVecSort]) Term[BitVecSort]

func BitVectorArrayConst added in v0.29.0 

func BitVectorArrayConst(indexWidth, elementWidth, id int, name string) Term[ArraySort[BitVecSort, BitVecSort]]

BitVectorArrayConst constructs a width-aware array symbol for the erased Go boundary. Go+ callers should retain the widths in their dependent result.

func BitVectorTerm 

func BitVectorTerm(value BitVectorValue) Term[BitVecSort]

BitVectorTerm exposes an already validated exact value at the erased Go boundary used by SMT-LIB. Go+ callers normally use the indexed BitVecVal.

func CompactStringAssertions added in v0.52.0 

func CompactStringAssertions(system CompactStringSystem) Term[BoolSort]

func ConstArray 

func ConstArray[I any, E any](value Term[E]) Term[ArraySort[I, E]]

func DatatypeConst added in v0.36.0 

func DatatypeConst(datatype int, constructors int, id int, name string) Term[DatatypeSort]

DatatypeConst creates a symbolic value of an algebraic datatype. datatype is its declaration identity; constructors is retained in the sort.

func DatatypeConstructor added in v0.36.0 

func DatatypeConstructor(datatype int, constructors int, constructor int, name string) Term[DatatypeSort]

DatatypeConstructor creates one nullary constructor value. The constructor ordinal is checked at runtime and the datatype/cardinality remain indexed.

func DivInteger added in v0.33.0 

func DivInteger(dividend Term[IntSort], divisor IntegerValue) Term[IntSort]

func IntToBitVec 

func IntToBitVec(width int, value Term[IntSort]) Term[BitVecSort]

func IntToString added in v0.54.0 

func IntToString(value Term[IntSort]) Term[StringSort]

func IntegerArrayRead 

func IntegerArrayRead(arrayID int, index IntegerValue) Term[IntSort]

func IntegerTerm 

func IntegerTerm(value IntegerValue) Term[IntSort]

func IntegerVariable 

func IntegerVariable(id int) Term[IntSort]

func IsBinaryRecursiveDatatypeConstructor added in v0.38.0 

func IsBinaryRecursiveDatatypeConstructor(declaration BinaryRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[BoolSort]

func IsDatatypeConstructor added in v0.36.0 

func IsDatatypeConstructor(datatype int, constructors int, constructor int, value Term[DatatypeSort]) Term[BoolSort]

func IsMixedRecursiveDatatypeConstructor added in v0.40.0 

func IsMixedRecursiveDatatypeConstructor(declaration MixedRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[BoolSort]

func IsNaryRecursiveDatatypeConstructor added in v0.39.0 

func IsNaryRecursiveDatatypeConstructor(declaration NaryRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[BoolSort]

func IsRecursiveDatatypeConstructor added in v0.37.0 

func IsRecursiveDatatypeConstructor(declaration RecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[BoolSort]

func MaterializeCompactStringTerm added in v0.58.0 

func MaterializeCompactStringTerm(term CompactStringTerm) Term[StringSort]

func ModInteger added in v0.33.0 

func ModInteger(dividend Term[IntSort], divisor IntegerValue) Term[IntSort]

func ScaleInteger added in v0.30.0 

func ScaleInteger(coefficient IntegerValue, value Term[IntSort]) Term[IntSort]

func Select 

func Select[I any, E any](array Term[ArraySort[I, E]], index Term[I]) Term[E]

func SelectBinaryRecursiveDatatypeConstructor added in v0.38.0 

func SelectBinaryRecursiveDatatypeConstructor(field BinaryDatatypeField, declaration BinaryRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[DatatypeSort]

func SelectMixedBitVecDatatypeField added in v0.40.0 

func SelectMixedBitVecDatatypeField(width int, cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[BitVecSort]

func SelectMixedBoolDatatypeField added in v0.40.0 

func SelectMixedBoolDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[BoolSort]

func SelectMixedDatatypeReferenceField added in v0.41.0 

func SelectMixedDatatypeReferenceField(targetDatatype int, targetConstructors int, cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[DatatypeSort]

func SelectMixedIntDatatypeField added in v0.40.0 

func SelectMixedIntDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[IntSort]

func SelectMixedRealDatatypeField added in v0.40.0 

func SelectMixedRealDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[RealSort]

func SelectMixedSelfDatatypeField added in v0.40.0 

func SelectMixedSelfDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort]) Term[DatatypeSort]

func SelectNaryRecursiveDatatypeConstructor added in v0.39.0 

func SelectNaryRecursiveDatatypeConstructor(field vec.Fin, declaration NaryRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[DatatypeSort]

func SelectNaryRecursiveDatatypeConstructorDynamic added in v0.39.0 

func SelectNaryRecursiveDatatypeConstructorDynamic(field int, declaration NaryRecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[DatatypeSort]

SelectNaryRecursiveDatatypeConstructorDynamic checks an erased field index.

func SelectRecursiveDatatypeConstructor added in v0.37.0 

func SelectRecursiveDatatypeConstructor(declaration RecursiveDatatypeConstructor, value Term[DatatypeSort]) Term[DatatypeSort]

func SequenceAt added in v0.78.0 

func SequenceAt[E any](value Term[SequenceSort[E]], index Term[IntSort]) Term[SequenceSort[E]]

func SequenceConcat added in v0.50.0 

func SequenceConcat[E any](values ...Term[SequenceSort[E]]) Term[SequenceSort[E]]

func SequenceConst added in v0.79.0 

func SequenceConst[E any](id int, name string) Term[SequenceSort[E]]

func SequenceContains added in v0.78.0 

func SequenceContains[E any](value Term[SequenceSort[E]], subsequence Term[SequenceSort[E]]) Term[BoolSort]

func SequenceEmpty added in v0.50.0 

func SequenceEmpty[E any]() Term[SequenceSort[E]]

func SequenceExtract added in v0.78.0 

func SequenceExtract[E any](value Term[SequenceSort[E]], offset Term[IntSort], length Term[IntSort]) Term[SequenceSort[E]]

func SequenceHasPrefix added in v0.78.0 

func SequenceHasPrefix[E any](value Term[SequenceSort[E]], prefix Term[SequenceSort[E]]) Term[BoolSort]

func SequenceHasSuffix added in v0.78.0 

func SequenceHasSuffix[E any](value Term[SequenceSort[E]], suffix Term[SequenceSort[E]]) Term[BoolSort]

func SequenceIndexOf added in v0.78.0 

func SequenceIndexOf[E any](value Term[SequenceSort[E]], subsequence Term[SequenceSort[E]], offset Term[IntSort]) Term[IntSort]

func SequenceLength added in v0.50.0 

func SequenceLength[E any](value Term[SequenceSort[E]]) Term[IntSort]

func SequenceReplace added in v0.78.0 

func SequenceReplace[E any](value Term[SequenceSort[E]], source Term[SequenceSort[E]], replacement Term[SequenceSort[E]]) Term[SequenceSort[E]]

func SequenceUnit added in v0.50.0 

func SequenceUnit[E any](value Term[E]) Term[SequenceSort[E]]

func Store 

func Store[I any, E any](array Term[ArraySort[I, E]], index Term[I], value Term[E]) Term[ArraySort[I, E]]

func StringAt added in v0.53.0 

func StringAt(value Term[StringSort], index Term[IntSort]) Term[StringSort]

func StringCharacter added in v0.116.0 

func StringCharacter(value int64) (Term[StringSort], bool)

func StringConcat added in v0.50.0 

func StringConcat(values ...Term[StringSort]) Term[StringSort]

func StringConst added in v0.50.0 

func StringConst(id int, name string) Term[StringSort]

func StringContains added in v0.50.0 

func StringContains(value Term[StringSort], substring Term[StringSort]) Term[BoolSort]

func StringFromCode added in v0.54.0 

func StringFromCode(value Term[IntSort]) Term[StringSort]

func StringHasPrefix added in v0.50.0 

func StringHasPrefix(value Term[StringSort], prefix Term[StringSort]) Term[BoolSort]

func StringHasSuffix added in v0.50.0 

func StringHasSuffix(value Term[StringSort], suffix Term[StringSort]) Term[BoolSort]

func StringInRegex added in v0.55.0 

func StringInRegex(value Term[StringSort], expression Regex[StringSort]) Term[BoolSort]

func StringIndexOf added in v0.53.0 

func StringIndexOf(value Term[StringSort], substring Term[StringSort], offset Term[IntSort]) Term[IntSort]

func StringIsDigit added in v0.54.0 

func StringIsDigit(value Term[StringSort]) Term[BoolSort]

func StringLength added in v0.50.0 

func StringLength(value Term[StringSort]) Term[IntSort]

func StringLess added in v0.115.0 

func StringLess(left Term[StringSort], right Term[StringSort]) Term[BoolSort]

func StringLessEqual added in v0.115.0 

func StringLessEqual(left Term[StringSort], right Term[StringSort]) Term[BoolSort]

func StringReplace added in v0.53.0 

func StringReplace(value Term[StringSort], source Term[StringSort], replacement Term[StringSort]) Term[StringSort]

func StringReplaceAll added in v0.54.0 

func StringReplaceAll(value Term[StringSort], source Term[StringSort], replacement Term[StringSort]) Term[StringSort]

func StringReplaceRegex added in v0.114.0 

func StringReplaceRegex(value Term[StringSort], expression Regex[StringSort], replacement Term[StringSort]) Term[StringSort]

func StringReplaceRegexAll added in v0.114.0 

func StringReplaceRegexAll(value Term[StringSort], expression Regex[StringSort], replacement Term[StringSort]) Term[StringSort]

func StringSubstring added in v0.53.0 

func StringSubstring(value Term[StringSort], offset Term[IntSort], length Term[IntSort]) Term[StringSort]

func StringToCode added in v0.54.0 

func StringToCode(value Term[StringSort]) Term[IntSort]

func StringToInt added in v0.54.0 

func StringToInt(value Term[StringSort]) Term[IntSort]

func StringVal added in v0.50.0 

func StringVal(value string) Term[StringSort]

func SymbolicIntegerArrayStoreRead 

func SymbolicIntegerArrayStoreRead(arrayID int, storeIndexID int, readIndexID int, value IntegerValue) Term[IntSort]

func UninterpretedConstant 

func UninterpretedConstant(sort int, id int, name string) Term[UninterpretedSort]

func UpdateMixedBitVecDatatypeField added in v0.43.0 

func UpdateMixedBitVecDatatypeField(width int, cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[BitVecSort]) Term[DatatypeSort]

func UpdateMixedBoolDatatypeField added in v0.43.0 

func UpdateMixedBoolDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[BoolSort]) Term[DatatypeSort]

func UpdateMixedDatatypeReferenceField added in v0.43.0 

func UpdateMixedDatatypeReferenceField(targetDatatype int, targetConstructors int, cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[DatatypeSort]) Term[DatatypeSort]

func UpdateMixedIntDatatypeField added in v0.43.0 

func UpdateMixedIntDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[IntSort]) Term[DatatypeSort]

func UpdateMixedRealDatatypeField added in v0.43.0 

func UpdateMixedRealDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[RealSort]) Term[DatatypeSort]

func UpdateMixedSelfDatatypeField added in v0.43.0 

func UpdateMixedSelfDatatypeField(cursor MixedDatatypeCursor, value Term[DatatypeSort], replacement Term[DatatypeSort]) Term[DatatypeSort]

type TermCases 

type TermCases[S any, R any] struct {
	Bool                   func(Value bool) R
	BoolSymbol             func(ID int, Name string) R
	BooleanVariable        func(ID int) R
	NegatedBooleanVariable func(ID int) R
	BooleanClause          func(Literals []int) R
	BooleanCNF             func(Literals []int, ClauseEnds []int) R
	Not                    func(Value Term[BoolSort]) R
	And                    func(Values []Term[BoolSort]) R
	Or                     func(Values []Term[BoolSort]) R
	Implies                func(Left Term[BoolSort], Right Term[BoolSort]) R
	Iff                    func(Left Term[BoolSort], Right Term[BoolSort]) R
	If                     func(Condition Term[BoolSort], Then Term[S], Else Term[S]) R
	Equal                  func(Left any, Right any) R
	Integer                func(Value int64) R

	IntSymbol func(ID int, Name string) R

	Add           func(Values []Term[IntSort]) R
	Subtract      func(Left Term[IntSort], Right Term[IntSort]) R
	IntegerScale  func(Coefficient IntegerValue, Value Term[IntSort]) R
	IntegerDiv    func(Dividend Term[IntSort], Divisor IntegerValue) R
	IntegerMod    func(Dividend Term[IntSort], Divisor IntegerValue) R
	LessEqual     func(Left Term[IntSort], Right Term[IntSort]) R
	Less          func(Left Term[IntSort], Right Term[IntSort]) R
	Real          func(Value Rational) R
	RealSymbol    func(ID int, Name string) R
	RealAdd       func(Values []Term[RealSort]) R
	RealSubtract  func(Left Term[RealSort], Right Term[RealSort]) R
	RealScale     func(Coefficient Rational, Value Term[RealSort]) R
	RealLessEqual func(Left Term[RealSort], Right Term[RealSort]) R
	RealLess      func(Left Term[RealSort], Right Term[RealSort]) R
	// contains filtered or unexported fields
}

TermCases selects one handler per Term variant for TermFold.

type TheoryConjunction 

type TheoryConjunction struct {
	AtomCount                 int
	Atoms                     [4]Term[BoolSort]
	AtomNegated               [4]bool
	OverflowAtoms             []Term[BoolSort]
	OverflowNegated           []bool
	RealCount                 int
	Reals                     [4]LinearRealConstraint
	OverflowReals             []LinearRealConstraint
	SymbolEqualityCount       int
	SymbolEqualities          [4]RealSymbolEquality
	OverflowSymbolEqualities  []RealSymbolEquality
	UnaryComparisonCount      int
	UnaryComparisons          [4]RealUnaryComparison
	OverflowUnaryComparisons  []RealUnaryComparison
	BinaryComparisonCount     int
	BinaryComparisons         [4]RealBinaryComparison
	OverflowBinaryComparisons []RealBinaryComparison
}

TheoryConjunction is a compact mixed conjunction produced after a compatibility layer has already normalized affine real constraints while retaining other Boolean atoms and their polarity.

type UnaryFunction 

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

UnaryFunction[d,r] retains its uninterpreted domain and range sorts. Go+ rejects applying it to a term from another domain before Go generation.

func DeclareUnaryFunction 

func DeclareUnaryFunction(domain int, codomain int, id int, name string) UnaryFunction

type UninterpretedEUFConjunction added in v0.34.0 

type UninterpretedEUFConjunction struct {
	Count    int
	Inline   [4]UninterpretedEUFRelation
	Overflow []UninterpretedEUFRelation
}

type UninterpretedEUFRelation added in v0.34.0 

type UninterpretedEUFRelation struct {
	Left    UninterpretedEUFTerm
	Right   UninterpretedEUFTerm
	Negated bool
}

type UninterpretedEUFTerm added in v0.34.0 

type UninterpretedEUFTerm struct {
	Kind         uint8
	SortID       int
	SymbolID     int
	FunctionID   int
	FirstSortID  int
	SecondSortID int
	FirstID      int
	SecondID     int
	Constant     string
}

UninterpretedEUFTerm is the compact, name-independent representation of a ground uninterpreted-sort symbol or an application whose arguments are symbols. Kind 1 is a symbol, 2 a unary application, and 3 a binary application. The ordinary typed EUF AST remains the general fallback.

type UninterpretedSort 

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

type Unknown 

type Unknown struct {
	Context Proof
	Reason  UnknownReason
}

type UnknownReason 

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

type UnknownReasonCases 

type UnknownReasonCases[R any] struct {
	UnsupportedTheory func(Name string) R
	ResourceLimit     func(Limit int) R
	Canceled          func() R
}

UnknownReasonCases selects one handler per UnknownReason variant for UnknownReasonFold.

type UnknownReasonEqOverrides 

type UnknownReasonEqOverrides struct {
	UnsupportedTheory func(x, y UnsupportedTheory) (eq, handled bool)
	ResourceLimit     func(x, y ResourceLimit) (eq, handled bool)
	Canceled          func(x, y Canceled) (eq, handled bool)
}

UnknownReasonEqOverrides carries optional per-variant hooks for UnknownReasonEqualWith. A hook returning handled=false falls through to the derived comparison.

type Unsatisfiable 

type Unsatisfiable struct {
	Value Proof
}

type UnsupportedTheory 

type UnsupportedTheory struct {
	Name string
}

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.