Difference between revisions of "Strings"
| Line 3: | Line 3: | ||
=Syntax= | =Syntax= | ||
The Theory of String logic symbol: | The Theory of String logic symbol: | ||
| − | + | ||
| − | (set-logic QF_S) | + | (set-logic QF_S) |
| − | + | ||
To set string alphabet cardinality: | To set string alphabet cardinality: | ||
| − | + | ||
| − | (set-option : | + | (set-option :strings-fmf true) |
| − | + | ||
The default value is false. | The default value is false. | ||
To use finite model finding: | To use finite model finding: | ||
| − | + | ||
| − | (set-option :str-alphabet-card n) | + | (set-option :str-alphabet-card n) |
| − | + | ||
To define a string variable: | To define a string variable: | ||
| − | + | ||
| − | (def-fun x () String) | + | (def-fun x () String) |
| − | + | ||
String Concatenation: | String Concatenation: | ||
Revision as of 15:55, 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)
The default value is false.
To use finite model finding:
(set-option :str-alphabet-card n)
To define a string variable:
(def-fun x () String)
String Concatenation:
\begin{lstlisting}[style=smtlib]
(str.++ s t)
\end{lstlisting}
where $s, t$ are string terms.
String Length: \begin{lstlisting}[style=smtlib] (str.len s) \end{lstlisting} where $s$ is a string term.
Membership Constraint: \begin{lstlisting}[style=smtlib] (str.in.re s r) \end{lstlisting} where $s$ is a string term and $r$ is a regular expression.
String to Regular Expression Conversion: \begin{lstlisting}[style=smtlib] (str.to.re s) \end{lstlisting} where $s$ is a string term. The statement turns a regular expression that only contains a string $s$.
Regular Expression Concatenation: \begin{lstlisting}[style=smtlib] (re.++ r_1 r_2 ... r_n) \end{lstlisting} where $r_1, r_2, \cdots, r_n$ are regular expressions.
Regular Expression Alternation: \begin{lstlisting}[style=smtlib] (re.or r_1 r_2 ... r_n) \end{lstlisting} where $r_1, r_2, \cdots, r_n$ are regular expressions.
Regular Expression Intersection: \begin{lstlisting}[style=smtlib] (re.itr r_1 r_2 ... r_n) \end{lstlisting} where $r_1, r_2, \cdots, r_n$ are regular expressions.
Regular Expression Kleene-Star: \begin{lstlisting}[style=smtlib] (re.* r) \end{lstlisting} where $r$ is a regular expression.
Regular Expression Kleene-Cross: \begin{lstlisting}[style=smtlib] (re.+ r) \end{lstlisting} where $r$ is a regular expression.
Regular Expression Option: \begin{lstlisting}[style=smtlib] (re.opt r) \end{lstlisting} where $r$ is a regular expression.
Regular Expression Range: \begin{lstlisting}[style=smtlib] (re.range s t) \end{lstlisting} 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$.
