java-smt icon indicating copy to clipboard operation
java-smt copied to clipboard

Extend Solver Independent SMTLib2 Parser/Generator

Open baierd opened this issue 9 months ago • 3 comments

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).

baierd avatar Feb 17 '25 17:02 baierd

Note: we need to find a way of cleaning up the generated files for the parser as much as possible before merging!

baierd avatar Feb 28 '25 12:02 baierd

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 avatar Apr 03 '25 12:04 DavidGalllob

@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!

baierd avatar Apr 15 '25 19:04 baierd