Difference between revisions of "Strings"

From CVC4
Jump to: navigation, search
(Created page with "This page is about strings in CVC4 =Syntax= =Example=")
 
Line 2: Line 2:
  
 
=Syntax=
 
=Syntax=
 +
The Theory of String logic symbol:
 +
\begin{lstlisting}[style=smtlib]
 +
(set-logic QF_S)
 +
\end{lstlisting}
 +
 +
To set string alphabet cardinality:
 +
\begin{lstlisting}[style=smtlib]
 +
(set-option :fmf-strings true)
 +
\end{lstlisting}
 +
The default value is false.
 +
 +
To use finite model finding:
 +
\begin{lstlisting}[style=smtlib]
 +
(set-option :str-alphabet-card n)
 +
\end{lstlisting}
 +
 +
To define a string variable:
 +
\begin{lstlisting}[style=smtlib]
 +
(def-fun x  () String)
 +
\end{lstlisting}
 +
 +
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$.
  
  
 
=Example=
 
=Example=

Revision as of 14:53, 5 December 2013

This page is about strings in CVC4

Syntax

The Theory of String logic symbol: \begin{lstlisting}[style=smtlib] (set-logic QF_S) \end{lstlisting}

To set string alphabet cardinality: \begin{lstlisting}[style=smtlib] (set-option :fmf-strings true) \end{lstlisting} The default value is false.

To use finite model finding: \begin{lstlisting}[style=smtlib] (set-option :str-alphabet-card n) \end{lstlisting}

To define a string variable: \begin{lstlisting}[style=smtlib] (def-fun x () String) \end{lstlisting}

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


Example

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Strings&oldid=4839"