kdrag.theories.regex

Theory of regular expressions

Functions

ReSort(S)

Regular expression sort.

kdrag.theories.regex.ReSort(S: SortRef) → ReSortRef

Regular expression sort. Sort parameter needs to be a sequence sort. https://en.wikipedia.org/wiki/Kleene_algebra

>>> T = ReSort(smt.SeqSort(smt.IntSort()))
>>> x,y,z = smt.Consts("x y z", T)
>>> x + y
Union(x, y)
>>> x | y
Union(x, y)
>>> x * y
re.++(x, y)
>>> x & y
Intersect(x, y)
>>> ~x
Complement(x)
>>> x[smt.Unit(smt.IntVal(0))] # A regular expression is something like a predicate on sequences
InRe(Unit(0), x)
>>> x - y
re.diff(x, y)

Parameters:

S (SortRef)

Return type:

ReSortRef