Revision as of 18:49, 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

Example

x y != y x