java-smt
java-smt copied to clipboard
Extend Solver Independent SMTLib2 Parser/Generator
This PR extends JavaSMT with an independent SMTLib2 parser/generator layer. Every solver can use the layer to generate or parse SMTLib2, independent of their own implementation. The parsing directly uses the API of the solver. Generating tracks all API usage independently into SMTLib2.
Additionally, we offer a complete solver-independent layer, that is usable with no solver installed. This layer can generate SMTLib2, but also parse SMTLib2 to manipulate the given formula.
Ideally, we also want to support usage of the solvers binaries with SMTLib2 directly. This has been tested for Princess, but has not been implemented for all solvers. My suggestion would be to remove/extract it from this PR and work on it separately.
TODO:
- [x] Add a full visitor implementation for the solver-independent layer.
- [ ] Transform the layer into a delegate.
- [x] Add appropriate options for the generator/parser.
- [ ] Check if its possible to clean up the auto-generated files from ANTLR, or generate them when building the project (similar to the other auto-generated files).
Note: we need to find a way of cleaning up the generated files for the parser as much as possible before merging!
A problem within JavaSMT is that it allows only one single assert in an smt2 String. This needs to be corrected to support all Strings. Momentarily the Generator can be used as a workaround as it builds Strings with only one assert statement.
@DavidGalllob please do not force-push! Force-push rewrites the history and can lead to conflicts locally!
Also, please do not resolve threads opened by others, as it is hard to confirm that changes have resolved the issues when they are not shown anymore!