Revision as of 18:40, 5 December 2013

This page is about strings in CVC4

Syntax

The Theory of String logic symbol:

 (set-logic QF_S)

To set string alphabet cardinality:

 (set-option :str-alphabet-card n)

To use finite model finding:

 (set-option :strings-fmf true)

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.

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.

Example

x y != y x