Revision as of 20:14, 5 December 2013

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)

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)