Full Code Examples

[jgarci40]

I appreciate the small examples in the Getting Started section of the README page. Are there full code examples that use scala-smtlib similar to those found in that Getting Started section? I tried browsing through the codebase, but there does not seem to be full examples included. Please correct me if I'm wrong.

Thanks,
Josh

[regb]

Unfortunately, there is indeed a lack of in-depth documentation for the library. The README tries to give an overview and points to the main entry points, but then more detailed documentation is only available in the sources with a few comments here and there.

The main project that uses scala-smtlib is Leon (https://github.com/epfl-lara/leon), and you could look at the file that translates internal AST of Leon into scala-smtlib SMT-LIB trees:
https://github.com/epfl-lara/leon/blob/master/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

Another source that you could look at are the unit tests:
https://github.com/regb/scala-smtlib/tree/master/src/test/scala/smtlib
They show some of the expected behaviour of internal APIs.

An example of full code that you can run can be found in the integration tests:
https://github.com/regb/scala-smtlib/blob/master/src/it/scala/smtlib/it/SmtLibRunnerTests.scala
This test uses the library to parse a file and send each command one by one to an SMT solver, and compare it with the result of directly executing the file with the SMT solver (that is, without using scala-smtlib).

Finally, if you don't find what you need, feel free to open an issue to ask a precise question on how to accomplish something.

Regis

[jgarci40]

Thank you very much for the thoughtful reply, Regis!