Can this library also be used as a parser etc. for SMT problems?

[jparsert]

Essentially, I would like to be able to parse an SMT problem and traverse the AST etc. Is this possible with this library? The documentation points to the /test dir which leads me to smtlib_reader.h. However, this only contains SmtLibReader which also requires a solver and it is also not entirely clear to me how to SmtLibReader to traverse the AST of an SMT lib parsed problem.

[yoni206]

Hi, and thank you for opening this issue.
This seems related to #304 .
Unfortunately, we do not currently support this functionality, although it is in our wish list.

@makaimann :
I suggest we leave this issue open.
Also: what do you think will be the main challenge in adding a parse_smt function to the solver API?

[jparsert]

To be honest. I don't think there are a lot of "theoretical" challenges. It's mostly just some engineering work to write an AST and maybe some helper classes. Further, one would probably want to have a solver.solve(AST* ast) function. Given that ANTLR4 grammars for smtlib exist (https://smtlib.cs.uiowa.edu/utilities.shtml) I would recommend basing the AST on that. Nnote that ANTLR4 does not have ASTs but ParseTrees hence all that is required writing a function that transforms the Antlr4 parse tree to a smt-switch specific AST and all the additional helper functions that one would want in this library.

[yoni206]

We already have a flex/bison parser, so no need for antlr, but yeah, it is just a matter of hooking it up into the API.

[jparsert]

Even better. I think if someone knows the codebase well this should not take too long.

[jparsert]

We already have a flex/bison parser, so no need for antlr, but yeah, it is just a matter of hooking it up into the API.

Is there any update on this?

[yoni206]

Hi, and thanks again for your interest.

Unfortunately, this is still an item in our wish list.