search

stanford-centaur / smt-switch

A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Other
103 stars 40 forks source link

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

Open jparsert opened 1 year ago

jparsert commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

jparsert commented 1 year ago

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 commented 1 year ago

Hi, and thanks again for your interest.

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