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.
|revenant_x86.tar.gz||32-bit Linux binary|