Difference between revisions of "Strings"
| Line 2: | Line 2: | ||
=Syntax= | =Syntax= | ||
| − | The Theory of | + | The Theory of Strings logic symbol: |
| − | + | ||
(set-logic QF_S) | (set-logic QF_S) | ||
| − | To set string alphabet cardinality: | + | ==Options== |
| − | + | To set string alphabet cardinality (256 by default): | |
| − | (set-option : | + | (set-option :strings-alphabet-card n) |
To use finite model finding: | To use finite model finding: | ||
(set-option :strings-fmf true) | (set-option :strings-fmf true) | ||
| + | ==Strings== | ||
To define a string variable: | To define a string variable: | ||
| − | + | (def-fun x () String) | |
| − | (def-fun x | + | |
| − | + | ||
String Concatenation: | String Concatenation: | ||
| − | |||
(str.++ s t) | (str.++ s t) | ||
| − | |||
where s, t are string terms. | where s, t are string terms. | ||
String Length: | String Length: | ||
| − | |||
(str.len s) | (str.len s) | ||
| − | |||
where s is a string term. | where s is a string term. | ||
| + | ==Regular Expression== | ||
Membership Constraint: | Membership Constraint: | ||
| − | |||
(str.in.re s r) | (str.in.re s r) | ||
| − | |||
where s is a string term and r is a regular expression. | 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 s is a string term. The statement turns a regular expression that only contains a string s. | where s is a string term. The statement turns a regular expression that only contains a string s. | ||
Revision as of 18:43, 5 December 2013
This page is about strings in CVC4
Syntax
The Theory of Strings logic symbol:
(set-logic QF_S)
Options
To set string alphabet cardinality (256 by default):
(set-option :strings-alphabet-card n)
To use finite model finding:
(set-option :strings-fmf true)
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.
Example
x y != y x
