Update readme to be current version compatible; add github status

Author: sankalpgambhir

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 `~testQuick` mode.
 
 ### 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 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`, `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
 ---------