[go: up one dir, main page]

Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Full Code Examples #25

Open
jgarci40 opened this issue Jan 30, 2017 · 2 comments
Open

Full Code Examples #25

jgarci40 opened this issue Jan 30, 2017 · 2 comments

Comments

@jgarci40
Copy link

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
Copy link
Owner
regb commented Jan 30, 2017

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
Copy link
Author

Thank you very much for the thoughtful reply, Regis!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants