diff --git a/.gitattributes b/.gitattributes index 5e578ec..009da46 100644 --- a/.gitattributes +++ b/.gitattributes @@ -1 +1 @@ -src/it/resources/regression/* linguist-vendored +*.smt2 linguist-vendored diff --git a/.gitignore b/.gitignore index 8af905b..80fcfec 100644 --- a/.gitignore +++ b/.gitignore @@ -11,4 +11,6 @@ target project/.bloop project/metals.sbt project/project -.DS_Store \ No newline at end of file +.DS_Store + +scripts/solvers diff --git a/CHANGELOG.md b/CHANGELOG.md index d7bf22f..6b5f985 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,7 +4,26 @@ Changelog Unreleased ---------- -> Nothing yet +* Add Bitwuzla solver support +* Fix interpreter handling of complex executable names with arguments +* Add continuous integration (CI) pipeline +* Update to Scala 3.7.0 +* Update sbt to 1.11.1 +* Add floating point theory support +* Support for cvc5 solver +* Upgrade to Scala 3.3 +* Make some arithmetic operations n-ary +* Add int2bv and bv2nat operations +* Read stderr and return error if not empty +* Cross-compilation for Scala 3.0 +* Add lexing for #unspecified literal (Z3 4.8.10) +* Remove bintray settings +* Make model token optional when parsing solver output +* Fix SimpleTreeTransformer +* Fix or operation +* Minor changes and upgrade to Scala 2.13.1 +* Remove hack for CVC4 and add -i flag as default +* Various CVC4 compatibility fixes v0.2.4 ------ diff --git a/README.md b/README.md index 9f32064..2a22fec 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -Scala SMT-LIB [![Build Status](http://laraquad4.epfl.ch:9000/epfl-lara/scala-smtlib/status/master)](http://laraquad4.epfl.ch:9000/epfl-lara/scala-smtlib) +Scala SMT-LIB [![scala-smtlib CI](https://github.com/epfl-lara/scala-smtlib/actions/workflows/scala-smtlib-CI.yml/badge.svg)](https://github.com/epfl-lara/scala-smtlib/actions/workflows/scala-smtlib-CI.yml) ============= Scala SMT-LIB is a lightweight, no dependency, abstraction over the @@ -47,8 +47,28 @@ You may want to use Scala SMT-LIB if: Setup ----- -The latest stable release for Scala 2.11 is available on Sonatype, simply add -the following to your `build.sbt`: +To include Scala SMT-LIB in your project, you can add it as a dependency +referring to a commit hash. You can add the following to your `build.sbt`: + +```scala +def remoteProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) + +// Choose a commit hash to pin the Scala SMT-LIB version (replace with the latest or chosen commit): +val smtlibRepository = "https://github.com/epfl-lara/scala-smtlib.git" +val smtlibCommitHash = "a8fc084fa48a59f0f58b6f3fba5433b8fe5eb280" // example commit + +lazy val scalaSmtlib = remoteProject(smtlibRepository, smtlibCommitHash) + +// And depend on it in your project +lazy val yourProject = (project in file(".")) + .settings( + // ... + ) + .dependsOn(scalaSmtlib) // <<< +``` + +The last stable release for Scala 2.11 is available on Sonatype, add the +following to your project settings in `build.sbt`: ```scala libraryDependencies += "com.regblanc" %% "scala-smtlib" % "0.2.2" @@ -57,7 +77,7 @@ libraryDependencies += "com.regblanc" %% "scala-smtlib" % "0.2.2" Getting Started with Examples ----------------------------- -To construct a parser, you will need a java.io.Reader and a lexer: +To construct a parser, you will need a `java.io.Reader` and a lexer: ```scala val is = new java.io.FileReader("INPUT") @@ -103,10 +123,10 @@ val formula = Assert(LessThan(NumeralLit(0), Plus(x, y))) smtlib.printer.RecursivePrinter.toString(formula) //(assert (< 0 (+ x y))) ``` -The above is a little bit verbose due to the objective of supporting all of -SMT-LIB. We are hoping to provide a nicer API in the future to build SMT-LIB -scripts, at least in the common cases, but the AST will probably remain at the -core of the library. +The above is a bit verbose due to the objective of supporting all of SMT-LIB. We +are hoping to provide a nicer API in the future to build SMT-LIB scripts, at +least in the common cases, but the AST will probably remain at the core of the +library. Low Level API ------------- @@ -147,14 +167,14 @@ such as `stdin`). The following two exceptions can be thrown by the lexer: throw the exception on the first `f`. The exception indicates the position in the input. * `UnexpectedEOFException` occurs when the EOF is reached in the middle of an - un-completed token. For example, a string literal which is not closed before - the EOF. + incomplete token. For example, a string literal which is not closed before the + EOF. ### Parsing Usually one does not need to work on a token by token basis, and is only -interested in fully formated SMT-LIB expressions. The +interested in fully formatted SMT-LIB expressions. The [`parser`](/src/main/scala/smtlib/parser) provides the extraction of SMT-LIB expressions. The [`Parser`](/src/main/scala/smtlib/parser/Parser.scala) consumes tokens generated by the above lexer: @@ -184,68 +204,82 @@ parameter a `Term`. Their ASTs are defined ### Printing The [`printer`](/src/main/scala/smtlib/printer) helps with printing out SMT-LIB -complient commands. This means that the output of a printer can be send +compliant commands. This means that the output of a printer can be sent directly to an SMT solver. ### Standard Theories -Finally the [`theories`](/src/main/scala/smtlib/theories) module provides tree -builders to create theory-specific formulas. Each theory module provides -`apply` and `unapply` methods on various object to manipulate the `Term` -representing the actual theory expression. +Finally, the [`theories`](/src/main/scala/smtlib/theories) module provides tree +builders to create theory-specific formulas. Each theory module provides `apply` +and `unapply` methods on various object to manipulate the `Term` representing +the actual theory expression. Development ----------- -The library is still under development and the API will likely go through quite a few -changes. It was originally part of [CafeSat](https://github.com/regb/scabolic) -and has been made standalone in order for the -[Leon](https://github.com/epfl-lara/leon) project to rely on it. +The library is still under development and the API will likely go through quite +a few changes. It was originally part of +[CafeSat](https://github.com/regb/cafesat) and has been made standalone in order +for the [Inox](https://github.com/epfl-lara/inox) and +[Stainless](https://github.com/epfl-lara/stainless) projects to rely on it. Hopefully, it can be useful to other people as well. ### Testing -In order to attain a decent level of quality, there is a relatively strict policy for testing. -Testing is separated in two levels of testing: unit tests and integration tests. Unit test -are dependency free and run entirely in memory. While integration tests will rely on things -like file system and external solvers. Unit test are very fast and should be easy to run as part -of a regular build cycle (you can run them after each compile), while integration tests are a bit -slower and are meant to pass on each commit. +In order to attain a decent level of quality, there is a relatively strict +policy for testing. Testing is separated in two levels of testing: unit tests +and integration tests. Unit test are dependency free and run entirely in memory. +While integration tests will rely on things like file system and external +solvers. Unit test are very fast and should be easy to run as part of a regular +build cycle (you can run them after each compile), while integration tests are a +bit slower and are meant to pass on each commit. In SBT, the command `sbt test` will run the unit test suite, while the command -`sbt it:test` will run the integration test suite. During developement, it -should be fine to run in mode `~testQuick`. +`sbt IntegrationTest/test` will run the integration test suite. During +development, it should be fine to run in [quick-testing mode](https://www.scala-sbt.org/1.x/docs/Testing.html#testQuick), as `sbt ~testQuick`, running only previously failing tests or those expected to change on file save. ### Building the Sources The project is built with [sbt](http://www.scala-sbt.org/). To build the library, just type: - sbt package +```console +$ sbt package +``` It will produce a jar that you can add to the classpath of your own project. -If you are building your project using sbt, it is possible to setup a reference -to this github repository in the build system to automatically get the most -recent build. [Here](https://github.com/regb/cafesat/blob/master/build.sbt) is -an example of how to do it, you can pick any commit. If you are interested in -this route, you should check the sbt official documentation. - Optionally, you can test Scala SMT-LIB in your environment by running the test suite. The tests are organized in unit and functional tests. Tu run the unit tests (very fast) you can type: - sbt test +```console +$ sbt test +``` + +The integration tests test end-to-end flows of Scala SMT-LIB. They do take +a bit more time and require some setup in your environment. In particular, they +will try to use the SMT solvers `z3`, `cvc4`, `cvc5`, and `bitwuzla` if they are +available in your PATH (the commands tried are exactly the solver names as +listed). If present in the PATH, Scala SMT-LIB will test its interpreter module +directly against these SMT solvers. -All tests should pass. Please open an issue if any test is failing. The -functional tests are testing end-to-end flows of Scala SMT-LIB. They do take a -bit more time and require some setup in your environment. In particular, they -will try to use the SMT solvers `z3` and/or `cvc4` if they are available in -your PATH (the commands tried are exactly `z3` and `cvc4`). If present in the -PATH, Scala SMT-LIB will test its interpreter module directly against these SMT -solvers. You can run those tests with: +The solvers binaries can also be obtained through the +[`scripts/install_solvers.sh`](scripts/install_solvers.sh) script. You can run +it with: - sbt it:test +```console +$ INSTALL_SOLVERS=1 scripts/install_solvers.sh +``` + +Default known versions of the solvers are used in the script unless given on the +command line. + +You can run those tests with: + +```console +$ sbt IntegrationTest/test +``` Changelog ---------