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
Together with other engine in CVC4, we can extend new functionality in the theory of strings. For example, we define the “str.contains” function (given two strings x and s, test whether s contains x) as follows:
(define-fun str.contains ((?x String) (?s String)) Bool
(or (= ?x ?s)
(exists ((?y String))
(and (= ?x (str.++ ?y ?s))
(> 0 (str.len ?y))))
(exists ((?z String))
(and (= ?x (str.++ ?s ?z))
(> 0 (str.len ?z))))
(exists ((?y String) (?z String))
(and (= ?x (str.++ ?y ?s ?z))
(> 0 (str.len ?y))
(> 0 (str.len ?z))))
))
Example
Find an assignment for x, where x."aa"="aa".x and the length of x equals to 7.
(set-logic QF_S) (declare-fun x () String) (assert (= (str.++ x "aa") (str.++ "aa" x))) (assert (= (str.len x) 7)) (check-sat)
x y != y x
