Generic, SMT-LIB-based backend for solvers

[hajduakos]

Currently we have a generic solver interface, realized by a wrapper for Z3 that uses the Java API of Z3. While using such APIs is efficient, it requires a significant effort to integrate a new solver. It would be nice to have a generic implementation, which serializes the expressions as SMT-LIB string (possibly to an in-memory file for efficiency) and passes it to an arbitrary binary that can consume the format. This would make it much more easier to integrate new solvers.

[hajduakos]

@as3810t I assigned you because you already started working on it on the smtlib-solver branch

[as3810t]

This feature is rather huge, so it will be implemented over multiple pull requests to the master, to gather feedback between steps.

Road to SMT-LIB solvers

• [x] Initial implementation ( #143 )
  • [x] Works on Linux
  • [x] Works with some, SMT-LIB compliant solvers (CVC4, recent Z3)
  • [x] Works with other SMT-LIB compliant solvers (older Z3, MathSAT5, Princess, SMTInterpol, Yices2, Boolector)
  • [x] Works with interpolation supported on some solvers (older Z3, MathSAT5, Princess, SMTInterpol)
  • [x] Works in the CFA cli frontend
• [ ] Integration with the rest of the CLI tools
  • [ ] STS
  • [ ] XSTS
  • [ ] XTA
• [ ] Works on Windows (maybe MacOS) with some solvers (not all support Windows / MacOS)
• [ ] Testing, testing, testing
  • [ ] First of all, there should be a test suite targeting different solvers and versions and testing their supported features for regression testing. The "soul" of the integration is an ANTLR grammar, which can easily break. The problem is that the number of supported features are huge, plus there is a huge amount of solver versions, across which the supported features change. The test suite should be designed in a way, that most tests are reusable.
  • [ ] Second, a regression testing should be performed to check, that the algorithms indeed work, and there are no glaring mistakes in the implementation.
• [ ] Code cleanup

Nice to have features

This list contains features that would be nice to have, but require big, architecture changing decisions to implement, so they are out-of-scope.

• There is no theory detection, so the solving process is not always the best.
• If using unsupported features, the failure is detected by the solver. It would be better, if Theta could catch these before sending the unsupported command down to the solver.

[leventeBajczi]

I think this was solved with #143, closing.