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.

MkSeqIndexOf

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

MkSeqIndexOf creates a sequence index-of operation.

MkSeqLength

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

MkSeqLength creates a sequence length operation.

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.

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.

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.

MkStringSort

func (c *Context) MkStringSort() *Sort

MkStringSort creates a string sort (sequence of characters).

MkToRe

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

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

Functions