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)