revenant - Intersection of regular languages

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


Graeme Gange