search

regb / scala-smtlib

Scala library for parsing and printing the SMT-LIB format
MIT License
44 stars 23 forks source link

Full Code Examples #25

Open jgarci40 opened 7 years ago

jgarci40 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

Thank you very much for the thoughtful reply, Regis!