search

Robbepop / stevia

A simple (unfinished) SMT solver for QF_ABV.
Other
36 stars 5 forks source link

Implement SMTLib2 parser #5

Open Robbepop opened 6 years ago

Robbepop commented 6 years ago

Stevia requires support for SMTLib2 parsing to make it work with SMTLib2 inputs.

Implementation Status

Past Discussion & Design

For this the rsmt2 crate provides parsing support, however, its current implementation isn't flexible enough to allow for decoupled integration of other SMT solver than the currently implemented ones (Z3 and CVC4). This issue is described in detail here. Adrien Champion reported that this was a wrong assumption about rsmt2.

For the parsing of SMTLib2 there are effectively two approaches.

The eager approach would simply parse an SMTLib2 input, process it and directly returns the entire parsed construct represented as an apropriate data structure to feed into stevia. This approach is simple, however, has the downside to be very inflexible and may require more memory to store a temporary data structure and maybe even has negative performance implications.

A more flexible and thus superior approach is to define an interface to let an underlying SMT solver know about newly parsed entities. In this situation a proper interface has yet to be found but the advantage is that this should be more optimal for memory consumption and runtime performance.

AdrienChampion commented 6 years ago

I'm not sure I understand how rsmt2 fits here.

rsmt2 requires your solver to support (some slight variations of) SMT-LIB 2, in an interactive manner on stdin / stdout. In that case, what it does is expose an SMT-LIB-2-style API to interact with it for someone writing, say, a model-checker.

What it does not do is help SMT solvers handle SMT-LIB 2 input, which is what you seem to be suggesting here.

Robbepop commented 6 years ago

Thank you for clearing my confusion about rsmt2 ...

So in order to implement my solver for rsmt2 I need an actual implementation of an SMT parser first. But at least now the question whether I need to implement a parser myself has been answered ... xD

Sorry for the confusion!

AdrienChampion commented 6 years ago

No worries.

So yeah, if you want rsmt2 to be able to use your solver you need to be able to read SMT-LIB 2 from your standard input interactively, and print answers in SMT-LIB 2 on your stdout.

Assuming you do not differ from z3's interpretation of SMT-LIB 2, at least in the theories that you support, then you won't need to do anything for rsmt2 to support your solver. Otherwise a few lines of code might be necessary depending on what the differences are.

Parsing / printing SMT-LIB 2 is pretty easy by the way since it's nothing but s-expressions. That's the main reason SMT-LIB 2 is designed that way, so that it's easy for computers to manipulate.

Robbepop commented 6 years ago

Yeah so I guess I have to implement parsing. But never mind, I have already implemented some parsers in the past so it should be all right.

Thank you very much for your help! I really appreciate it. :)