Difference between revisions of "Strings"
| Line 9: | Line 9: | ||
(set-option :strings-fmf true) | (set-option :strings-fmf true) | ||
| − | |||
| − | |||
To use finite model finding: | To use finite model finding: | ||
| Line 22: | Line 20: | ||
String Concatenation: | String Concatenation: | ||
| − | + | ||
| − | (str.++ s t) | + | (str.++ s t) |
| − | + | ||
| − | where | + | where s, t are string terms. |
String Length: | String Length: | ||
| − | + | ||
| − | (str.len s) | + | (str.len s) |
| − | + | ||
| − | where | + | where s is a string term. |
Membership Constraint: | Membership Constraint: | ||
| − | + | ||
| − | (str.in.re s r) | + | (str.in.re s r) |
| − | + | ||
| − | where | + | where s is a string term and r is a regular expression. |
String to Regular Expression Conversion: | String to Regular Expression Conversion: | ||
| − | + | ||
| − | (str.to.re s) | + | (str.to.re s) |
| − | + | ||
| − | where | + | where s is a string term. The statement turns a regular expression that only contains a string s. |
Regular Expression Concatenation: | Regular Expression Concatenation: | ||
| − | + | ||
| − | (re.++ r_1 r_2 ... r_n) | + | (re.++ r_1 r_2 ... r_n) |
| − | + | ||
| − | where | + | where r_1, r_2, ..., r_n are regular expressions. |
Regular Expression Alternation: | Regular Expression Alternation: | ||
| − | + | ||
| − | (re.or r_1 r_2 ... r_n) | + | (re.or r_1 r_2 ... r_n) |
| − | + | ||
| − | where | + | where r_1, r_2, ..., r_n are regular expressions. |
Regular Expression Intersection: | Regular Expression Intersection: | ||
| − | + | ||
| − | (re.itr r_1 r_2 ... r_n) | + | (re.itr r_1 r_2 ... r_n) |
| − | + | ||
| − | where | + | where r_1, r_2, ..., r_n are regular expressions. |
Regular Expression Kleene-Star: | Regular Expression Kleene-Star: | ||
| − | + | ||
| − | (re.* r) | + | (re.* r) |
| − | + | ||
| − | where | + | where r is a regular expression. |
Regular Expression Kleene-Cross: | Regular Expression Kleene-Cross: | ||
| − | + | ||
| − | (re.+ r) | + | (re.+ r) |
| − | + | ||
| − | where | + | where r is a regular expression. |
Regular Expression Option: | Regular Expression Option: | ||
| − | + | ||
| − | (re.opt r) | + | (re.opt r) |
| − | + | ||
| − | where | + | where r is a regular expression. |
Regular Expression Range: | Regular Expression Range: | ||
| − | + | ||
| − | (re.range s t) | + | (re.range s t) |
| − | + | ||
| − | where | + | where s, t are single characters in double quotes, e.g. ``a", ``b". |
| − | It returns a regular expression that contains any character between | + | It returns a regular expression that contains any character between s and t. |
=Example= | =Example= | ||
Revision as of 15:58, 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 :strings-fmf true)
To use finite model finding:
(set-option :str-alphabet-card n)
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.
