revenant is a tool for testing emptiness of a set of regular languages. Unlike most string solvers, it doesn't use classical product automaton construction algorithms; instead, it uses interpolation-based unbounded model checking techniques.
revenant takes input from stdin, of the form:
(elem (x) ([a-c]+[bc]))
(elem (x) ([a-c]+[ac]))
(elem (x) ([a-c]+[ab]))
revenant currently only supports constraints on single variables; we intend to add
support for concatenation constraints in the future. This version requires
MathSat 5.1.12.
| File | Description |
|---|---|
| revenant_x86.tar.gz | 32-bit Linux binary |