Strings

Basic String Term Builders

cvc5.pythonic.StringSort(ctx=None)

Return the string sort in the given context. If ctx=None, then the global context is used.

>>> StringSort()
String
>>> a = Const('a', StringSort())
>>> a.sort() == StringSort()
True
cvc5.pythonic.String(name, ctx=None)

Return a string constant named name. If ctx=None, then the global context is used.

>>> s = String('s')
>>> s.sort()
String
cvc5.pythonic.Strings(names, ctx=None)

Return a tuple of string constants.

>>> x, y, z = Strings('x y z')
>>> Concat(x,y,z)
+(x, y, z)
>>> Concat(x,y,z).sort()
String
cvc5.pythonic.StringVal(val, ctx=None)

Return an SMT String value.

val is a string value

If ctx=None, then the global context is used.

>>> StringVal('hello')
"hello"
>>> StringVal('hello').sort()
String

String Operators

cvc5.pythonic.Length(s, ctx=None)

obtain the length of a string or sequence s

>>> s = StringVal('s')
>>> l = Length(s)
>>> simplify(l)
1
cvc5.pythonic.SubString(s, offset, length, ctx=None)

Extract substring starting at offset of size length

>>> simplify(SubString('hello',3,2))
"lo"
>>> simplify(SubString(StringVal('hello'),3,2))
"lo"
cvc5.pythonic.Contains(a, b, ctx=None)

check if a contains b

>>> simplify(Contains('ab','a'))
True
>>> a,b,c = Strings("a b c")
>>> s = Contains(a+b+c,b)
>>> simplify(s)
True
cvc5.pythonic.PrefixOf(a, b, ctx=None)

check if a is a prefix of b

>>> s1 = PrefixOf("ab","abc")
>>> simplify(s1)
True
>>> s2 = PrefixOf("bc","abc")
>>> simplify(s2)
False
cvc5.pythonic.SuffixOf(a, b, ctx=None)

check if a is a suffix of b

>>> s1 = SuffixOf("ab","abc")
>>> simplify(s1)
False
>>> s2 = SuffixOf("bc","abc")
>>> simplify(s2)
True
cvc5.pythonic.IndexOf(s, substr, offset=None)

retrieves the index of substr in s starting at offset, if offset is missing retrieves the first occurence

>>> simplify(IndexOf("abcabc", "bc"))
1
>>> simplify(IndexOf("abcabc", "bc", 0))
1
>>> simplify(IndexOf("abcabc", "bc", 2))
4
cvc5.pythonic.Replace(s, src, dst)

Replace the first occurence of src with dst in s

>>> simplify(Replace('hello','l','?'))
"he?lo"
>>> seq = Concat(Unit(IntVal(1)),Unit(IntVal(2)))
>>> seq
Concat(Unit(1), Unit(2))
>>> simplify(Replace(seq,Unit(IntVal(1)),Unit(IntVal(5))))
(seq.++ (seq.unit 5) (seq.unit 2))()
cvc5.pythonic.StrToInt(s)

Convert string expression to int

>>> a = StrToInt('1')
>>> simplify(a==1)
True
>>> b = StrToInt('123')
>>> simplify(b)
123
cvc5.pythonic.IntToStr(s)

Convert integer expression to string

>>> b = IntToStr(55)
>>> simplify(b)
"55"
>>> b = IntToStr(-5)
>>> simplify(b)
""
cvc5.pythonic.StrToCode(s)

Convert a unit length string to integer code

>>> simplify(StrToCode('a'))
97
>>> simplify(StrToCode('*'))
42
cvc5.pythonic.StrFromCode(c)

Convert code to a string

>>> a = StrFromCode(97)
>>> simplify(a == 'a')
True

See the following operator overload for string terms:

Basic Regular Expression Term Builders

cvc5.pythonic.Re(s, ctx=None)

The regular expression that accepts the string s

>>> re = Re('a')
>>> simplify(InRe('a',re))
True
>>> simplify(InRe('b',re))
False
cvc5.pythonic.Full(ctx=None)

Create the regular expression that accepts the universal language

>>> e = Full()
>>> print(e)
Full()
>>> s = String('s')
>>> simplify(InRe(s,e))
True
cvc5.pythonic.Option(re)

Create the regular expression that optionally accepts the argument.

>>> re = Option(Re("a"))
>>> print(simplify(InRe("a", re)))
True
>>> print(simplify(InRe("", re)))
True
>>> print(simplify(InRe("aa", re)))
False
cvc5.pythonic.Range(lo, hi, ctx=None)

Create the range regular expression over two sequences of length 1

>>> range = Range("a","z")
>>> print(simplify(InRe("b", range)))
True
>>> print(simplify(InRe("bb", range)))
False
cvc5.pythonic.AllChar()

Create a regular expression that accepts all single character strings

>>> re = AllChar()
>>> simplify(InRe('a',re))
True
>>> simplify(InRe('',re))
False
>>> simplify(InRe('ab',re))
False

Regular Expression Operators

cvc5.pythonic.InRe(s, re)

Create regular expression membership test

>>> re = Union(Re("a"),Re("b"))
>>> print (simplify(InRe("a", re)))
True
>>> print (simplify(InRe("b", re)))
True
>>> print (simplify(InRe("c", re)))
False
cvc5.pythonic.Union(*args)

create union of regular expressions

>>> re = Union(Re("a"), Re("b"), Re("c"))
>>> simplify(InRe('a',re))
True
>>> print (simplify(InRe("d", re)))
False
cvc5.pythonic.Intersect(*args)

Create intersection of regular expressions.

>>> re = Intersect(Re("a"), Re("b"), Re("c"))
>>> simplify(InRe('',re))
False
>>> re2 = Intersect(Star(Re("a")), Star(Re("b")), Star(Re("c")))
>>> simplify(InRe('',re2))
True
cvc5.pythonic.Complement(re)

Create the complement regular expression.

>>> re = Re('a')
>>> comp_re = Complement(re)
>>> simplify(InRe('a',comp_re))
False
>>> simplify(InRe('aa',comp_re))
True
cvc5.pythonic.Plus(re)

Create the regular expression accepting one or more repetitions of argument.

>>> re = Plus(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
False
cvc5.pythonic.Star(re)

Create the regular expression accepting zero or more repetitions of argument.

>>> re = Star(Re("a"))
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("ab", re)))
False
>>> print(simplify(InRe("", re)))
True
cvc5.pythonic.Loop(re, lo, hi=0)

Create the regular expression accepting between a lower and upper bound repetitions

>>> re = Loop(Re("a"), 1, 3)
>>> print(simplify(InRe("aa", re)))
True
>>> print(simplify(InRe("aaaa", re)))
False
>>> print(simplify(InRe("", re)))
False
cvc5.pythonic.Diff(a, b, ctx=None)

Create the difference regular expression

>>> r1 = Re('a')
>>> r2 = Re('a') + Re('b')
>>> simplify(InRe('a',Diff(r2,r1)))
False
>>> simplify(InRe('b',Diff(r2,r1)))
True

Classes (with overloads)

class cvc5.pythonic.StringSortRef(ast, ctx=None)

String sort.

cast(val)

Try to cast val as a String.

>>> string_sort = StringSort()
>>> string_sort.cast(10)
"10"
>>> string_sort.cast('hello')
"hello"
>>> string_sort.cast(10.5)
"10.5"
>>> string_sort.cast(RealVal(1.5))
"3/2"
>>> string_sort.cast(RealVal(1.5)).sort()
String
class cvc5.pythonic.StringRef(ast, ctx=None, reverse_children=False)

String expressions

__ge__(other)

Create the SMT expression other <= self based on a lexiographic ordering.

>>> s,t = Strings('s t')
>>> s >= t
t <= s
__getitem__(i)

Return string character at i

>>> StringVal("hello")[0]
At("hello", 0)
>>> simplify(StringVal("hello")[0])
"h"
__gt__(other)

Create the SMT expression other < self based on a lexiographic ordering.

>>> s,t = Strings('s t')
>>> s > t
t < s
__le__(other)

Create the SMT expression self <= other based on a lexiographic ordering.

>>> s,t = Strings('s t')
>>> s <= t
s <= t
__lt__(other)

Create the SMT expression self < other based on a lexiographic ordering.

>>> s,t = Strings('s t')
>>> s < t
s < t
at(i)

Return the sequence at index i

>>> seq = Const('seq',SeqSort(IntSort()))
>>> seq.at(0)
At(seq, 0)
>>> seq.at(0).sort()
(Seq Int)