Strings

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$.