OSTRICH
An SMT Solver for String Constraints
OSTRICH is an SMT solver for string constraints.
Using Ostrich
After installing the Scala Build tool (SBT), you can assemble a JAR file using sbt assembly
. To run it, use either the ostrich
script in the root folder, or ostrich-client
. The latter transparently spins up a server that continuously serves requests from the client script; useful to avoid cold-starting the JVM if you are running many instances.
See ./ostrich -help
for more options.
Web Interface
For experiments, OSTRICH can also be used through the Princess web interface. Select the string solver option "OSTRICH" on the web interface for this purpose.
Input Format
OSTRICH accepts constraints written using the SMT-LIB theory of strings. At this point, most of the operators in the theory are supported, but inputs need to be straightline; see this paper for a definition.
In addition to the standardized SMT-LIB operators, OSTRICH can handle a number of further functions.
Additional string functions
Name | Explanation |
---|---|
str.reverse | Reverse a string |
Unary transducers
Finite-state transducers are a general way to introduce further string functions. Examples of functions that can be represented as transducers are encoders, decoders, extraction of sub-strings, removal of white-space characters, etc.
Finite-state transducers can be defined as (mutually) recursive functions, see this file for an example.
It is also possible to use prioritised finite-state transducers: multiple outgoing transitions from a state can be given priorities, and the transducer will take the transition with highest priority that will lead to a successful run. See this file for an example.
Additional regular expression constructors
Name | Explanation |
---|---|
re.from_ecma2020 | Parse a regular expression in textual ECMAScript 2020 format (example) |
re.from_ecma2020_flags | Parse a regular expression in textual ECMAScript 2020 format, with a second argument to specify flags (example) |
re.case_insensitive | Make any regular expression case insensitive (example) |
Handling of capture groups
OSTRICH can also process regular expressions that include capture groups, lazy quantifiers, and anchors, although this is more experimental. For this functionality, OSTRICH understands a number of additional regular expression operators:
Name | Explanation |
---|---|
re.*? | Non-greedy star: similar to re.* but matching as few characters as possible |
re.+? | Non-greedy plus |
re.opt? | Non-greedy option |
(_ re.loop? a b) | Non-greedy loop |
(_ re.capture n) | Capture group with index n |
(_ re.reference n) | Reference to the contents of capture group n |
re.begin-anchor | The anchor ^ |
re.end-anchor | The anchor $ |
Such augmented regular expressions can be used in combination with several new string functions. Those functions support in particular capture groups and references in the replacement strings:
Name | Explanation |
---|---|
(_ str.extract n) | Extract the contents of the n'th capture group (example) |
str.replace_cg | Replace the first match of a regular expression (example) |
str.replace_cg_all | Replace all matches of a regular expression (example) |