seq.go - Z3 Go API

MkEmptySeq

func (c *Context) MkEmptySeq(sort *Sort) *Expr

MkEmptySeq creates an empty sequence.

MkInRe

func (c *Context) MkInRe(seq, re *Expr) *Expr

MkInRe creates a membership predicate for a sequence in a regular expression.

MkIntToStr

func (c *Context) MkIntToStr(num *Expr) *Expr

MkIntToStr creates an integer-to-string conversion.

MkReAllchar

func (c *Context) MkReAllchar(sort *Sort) *Expr

MkReAllchar creates a regular expression that accepts all single characters.

MkReComplement

func (c *Context) MkReComplement(re *Expr) *Expr

MkReComplement creates the complement of a regular expression.

MkReConcat

func (c *Context) MkReConcat(regexes ...*Expr) *Expr

MkReConcat creates a concatenation of regular expressions.

MkReDiff

func (c *Context) MkReDiff(a, b *Expr) *Expr

MkReDiff creates the difference of two regular expressions (a - b).

MkReEmpty

func (c *Context) MkReEmpty(sort *Sort) *Expr

MkReEmpty creates an empty regular expression (accepts no strings).

MkReFull

func (c *Context) MkReFull(sort *Sort) *Expr

MkReFull creates a full regular expression (accepts all strings).

MkReIntersect

func (c *Context) MkReIntersect(regexes ...*Expr) *Expr

MkReIntersect creates an intersection of regular expressions.

MkReLoop

func (c *Context) MkReLoop(re *Expr, lo, hi uint) *Expr

MkReLoop creates a regular expression with bounded repetition (between lo and hi times). If hi is 0, it means unbounded (at least lo times).

MkReOption

func (c *Context) MkReOption(re *Expr) *Expr

MkReOption creates an optional regular expression (zero or one repetition).

MkRePlus

func (c *Context) MkRePlus(re *Expr) *Expr

MkRePlus creates a Kleene plus (one or more repetitions) of a regular expression.

MkRePower

func (c *Context) MkRePower(re *Expr, n uint) *Expr

MkRePower creates a regular expression that matches exactly n repetitions.

MkReRange

func (c *Context) MkReRange(lo, hi *Expr) *Expr

MkReRange creates a regular expression for a character range [lo, hi].

MkReSort

func (c *Context) MkReSort(seqSort *Sort) *Sort

Regular expression operations MkReSort creates a regular expression sort.

MkReStar

func (c *Context) MkReStar(re *Expr) *Expr

MkReStar creates a Kleene star (zero or more repetitions) of a regular expression.

MkReUnion

func (c *Context) MkReUnion(regexes ...*Expr) *Expr

MkReUnion creates a union (alternation) of regular expressions.

MkSeqAt

func (c *Context) MkSeqAt(seq, index *Expr) *Expr

MkSeqAt creates a sequence element access operation.

MkSeqConcat

func (c *Context) MkSeqConcat(exprs ...*Expr) *Expr

MkSeqConcat creates a sequence concatenation.

MkSeqContains

func (c *Context) MkSeqContains(seq, substr *Expr) *Expr

MkSeqContains creates a sequence contains predicate.

MkSeqExtract

func (c *Context) MkSeqExtract(seq, offset, length *Expr) *Expr

MkSeqExtract creates a sequence extract (substring) operation.

MkSeqFoldl

func (c *Context) MkSeqFoldl(f, a, seq *Expr) *Expr

MkSeqFoldl applies a fold-left operation to a sequence.

MkSeqFoldli

func (c *Context) MkSeqFoldli(f, i, a, seq *Expr) *Expr

MkSeqFoldli applies an indexed fold-left operation to a sequence.

MkSeqIndexOf

func (c *Context) MkSeqIndexOf(seq, substr, offset *Expr) *Expr

MkSeqIndexOf creates a sequence index-of operation.

MkSeqLastIndex

func (c *Context) MkSeqLastIndex(seq, substr *Expr) *Expr

MkSeqLastIndex returns the last index of substr in seq.

MkSeqLength

func (c *Context) MkSeqLength(seq *Expr) *Expr

MkSeqLength creates a sequence length operation.

MkSeqMap

func (c *Context) MkSeqMap(f, seq *Expr) *Expr

MkSeqMap applies a function to each element of a sequence, returning a new sequence.

MkSeqMapi

func (c *Context) MkSeqMapi(f, i, seq *Expr) *Expr

MkSeqMapi applies an indexed function to each element of a sequence, returning a new sequence.

MkSeqNth

func (c *Context) MkSeqNth(seq, index *Expr) *Expr

MkSeqNth retrieves the n-th element of a sequence as a single-element expression.

MkSeqPrefix

func (c *Context) MkSeqPrefix(prefix, seq *Expr) *Expr

MkSeqPrefix creates a sequence prefix predicate.

MkSeqReplace

func (c *Context) MkSeqReplace(seq, src, dst *Expr) *Expr

MkSeqReplace creates a sequence replace operation.

MkSeqReplaceAll

func (c *Context) MkSeqReplaceAll(seq, src, dst *Expr) *Expr

MkSeqReplaceAll replaces all occurrences of src with dst in seq.

MkSeqReplaceRe

func (c *Context) MkSeqReplaceRe(seq, re, replacement *Expr) *Expr

MkSeqReplaceRe replaces the first occurrence matching a regular expression.

MkSeqReplaceReAll

func (c *Context) MkSeqReplaceReAll(seq, re, replacement *Expr) *Expr

MkSeqReplaceReAll replaces all occurrences matching a regular expression.

MkSeqSort

func (c *Context) MkSeqSort(elemSort *Sort) *Sort

Sequence and string operations MkSeqSort creates a sequence sort.

MkSeqSuffix

func (c *Context) MkSeqSuffix(suffix, seq *Expr) *Expr

MkSeqSuffix creates a sequence suffix predicate.

MkSeqUnit

func (c *Context) MkSeqUnit(elem *Expr) *Expr

MkSeqUnit creates a unit sequence containing a single element.

MkStrLe

func (c *Context) MkStrLe(s1, s2 *Expr) *Expr

MkStrLe creates a string less-than-or-equal comparison.

MkStrLt

func (c *Context) MkStrLt(s1, s2 *Expr) *Expr

MkStrLt creates a string less-than comparison.

MkStrToInt

func (c *Context) MkStrToInt(str *Expr) *Expr

MkStrToInt creates a string-to-integer conversion.

MkString

func (c *Context) MkString(value string) *Expr

MkString creates a string constant.

MkStringFromCode

func (c *Context) MkStringFromCode(code *Expr) *Expr

MkStringFromCode converts a Unicode code point to a single-character string.

MkStringSort

func (c *Context) MkStringSort() *Sort

MkStringSort creates a string sort (sequence of characters).

MkStringToCode

func (c *Context) MkStringToCode(s *Expr) *Expr

MkStringToCode converts a single-character string to its Unicode code point.

MkToRe

func (c *Context) MkToRe(seq *Expr) *Expr

MkToRe converts a sequence to a regular expression that accepts exactly that sequence.

Functions