Strings
This page is about strings in CVC4
Syntax
The Theory of Strings logic symbol:
(set-logic QF_S)
Options
To set up string alphabet cardinality (256 by default):
(set-option :strings-alphabet-card n)
To use finite model finding mode (false by default):
(set-option :strings-fmf true)
To set up depth of unrolling regular expression used by the theory of strings (10 by default):
(set-option :strings-regexp-depth 20)
To select the strategy of LB rule application: 0-lazy, 1-eager, 2-no (0 by default):
(set-option :strings-lb 1)
Strings
To define a string variable:
(def-fun x () String)
String Concatenation:
(str.++ s t)
where s, t are string terms.
String Length:
(str.len s)
where s is a string term.
Regular Expression
Membership Constraint:
(str.in.re s r)
where s is a string term and r is a regular expression.
String to Regular Expression Conversion:
(str.to.re s)
where s is a string term. The statement turns a regular expression that only contains a string s.
Regular Expression Concatenation:
(re.++ r_1 r_2 ... r_n)
where r_1, r_2, ..., r_n are regular expressions.
Regular Expression Alternation:
(re.or r_1 r_2 ... r_n)
where r_1, r_2, ..., r_n are regular expressions.
Regular Expression Intersection:
(re.itr r_1 r_2 ... r_n)
where r_1, r_2, ..., r_n are regular expressions.
Regular Expression Kleene-Star:
(re.* r)
where r is a regular expression.
Regular Expression Kleene-Cross:
(re.+ r)
where r is a regular expression.
Regular Expression Option:
(re.opt r)
where r is a regular expression.
Regular Expression Range:
(re.range s t)
where s, t are single characters in double quotes, e.g. "a", "b". It returns a regular expression that contains any character between s and t.
Extension
Example
x y != y x
