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))))
))
Limitation
The decidability of this theory is unknown. For satisfiable problems (without extensions), our solver is sound, complete and terminating in the FMF mode. For unsatisfiable problems, the termination is not guaranteed; however, user can tune the options for termination.
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)
Find assignments for x, y, z, where x, y and z are distinct and their length equals to 1.
(declare-fun x () String) (declare-fun y () String) (declare-fun z () String) (declare-fun i () Int) (assert (= i 1)) (assert (= (Length x) i)) (assert (= (Length y) i)) (assert (= (Length z) i)) (assert (not (= x y))) (assert (not (= x z))) (assert (not (= z y))) (check-sat)
Find assignments for x and y, where x.y != y.x.
(set-logic QF_S) (set-info :status sat) (declare-fun x () String) (declare-fun y () String) (assert (not (= (str.++ x y) (str.++ y x)))) (check-sat)
