FR: Construct regular expressions from automata (for SMT string solving)

[Ailuras]

Hi,

I saw that MATA supports translating SMT to automata, but I couldn’t find an interface for translating automata back to SMT constraints.

Is this direction difficult to support, or is it something that might be considered in the future?

Thanks!

[Adda0]

Hey. What exactly do you mean by "Mata supporting translating SMT to automata and back" in your case? Can you specify more clearly what you expect the input and the output of such an interface to be? From regexes and back? Length constraints? Some additional automata types? What would you want the interface to look like, so that is useful for your use cases?

Mata is primarily a general automata library. Specific use cases, such as SMT solving, are domain-specific extensions of the library, under the applications subfolders in this repository, but if there is a use case, we would be happy to help shape it so that it integrates nicely with the automata implementation's underlying interface.

[Ailuras]

Thanks for the quick reply!

To clarify further, we are currently using Mata as an Intermediate Representation for string constraint preprocessing. While z3-noodler is highly efficient at maintaining and processing automata, we still need a standalone "backward path" to bridge the conversion from automata back to SMT constraints.

Our requirement is actually straightforward — we are not dealing with length constraints at this stage, only Re constraints. We simply need SMT constraints, after being processed through Mata's powerful automata operations, to be convertible back into SMT constraints. For use cases that treat Mata as a general-purpose IR, we believe this functionality would be of great value.

[Adda0]

Thanks for the clarification. As of now, there is no interface for extracting regular expressions back from the NFAs. There are algorithms for that; we just have not had such a use case. This is certainly a reasonable feature to add, and we would like Mata to support it eventually. As of now, however, we do not have specific plans and cannot say when we will get to it. PRs are always welcome. If you are interested in Mata and how it could be utilised for your work, we welcome you to contact us directly through the contacts listed at https://github.com/VeriFIT/mata/blob/devel/AUTHORS.md#the-core-mata-group to set up a meeting to discuss next steps to support your use cases.

[Adda0]

Actually, I just found out that one of our students is already working on translating automata into regular expressions. In about a month and a half, he should be done. Are there any specifics of your use case that you want to make sure are covered by this work? Feel free to let us know or discuss this further in a meeting so we can see if and how we can better align the upcoming translation implementation with your needs.