Skip to content

Commit 3c4b620

Browse files
sankalpgambhirvkuncak
sankalpgambhir
authored and
vkuncak
committed
Update Readme
1 parent ff2d068 commit 3c4b620

File tree

1 file changed

+94
-96
lines changed

1 file changed

+94
-96
lines changed

‎README.md‎

Lines changed: 94 additions & 96 deletions
Original file line numberDiff line numberDiff line change
@@ -1,169 +1,167 @@
1-
[![Build Status](https://github.com/epfl-lara/inox/actions/workflows/inox-CI.yml/badge.svg?branch=main)](https://github.com/epfl-lara/inox/actions/workflows/inox-CI.yml/?branch=main) [<img src="https://img.shields.io/maven-central/v/ch.epfl.lara/inox_2.11.svg?label=latest%20release%20for%202.11"/>](http://search.maven.org/#search%7Cga%7C1%7Cg%3Ach.epfl.lara%20a%3Ainox_2.11) [<img src="https://img.shields.io/maven-central/v/ch.epfl.lara/inox_2.12.svg?label=latest%20release%20for%202.12"/>](http://search.maven.org/#search%7Cga%7C1%7Cg%3Ach.epfl.lara%20a%3Ainox_2.12)
1+
[![Build
2+
Status](https://github.com/epfl-lara/inox/actions/workflows/inox-CI.yml/badge.svg?branch=main)](https://github.com/epfl-lara/inox/actions/workflows/inox-CI.yml/?branch=main)
3+
[<img
4+
src="https://img.shields.io/maven-central/v/ch.epfl.lara/inox_2.11.svg?label=latest%20release%20for%202.11"/>](http://search.maven.org/#search%7Cga%7C1%7Cg%3Ach.epfl.lara%20a%3Ainox_2.11)
5+
[<img
6+
src="https://img.shields.io/maven-central/v/ch.epfl.lara/inox_2.12.svg?label=latest%20release%20for%202.12"/>](http://search.maven.org/#search%7Cga%7C1%7Cg%3Ach.epfl.lara%20a%3Ainox_2.12)
27
==========
38

4-
Inox is a solver for higher-order functional programs which provides first-class support for
5-
features such as:
9+
Inox is a solver for higher-order functional programs which provides first-class
10+
support for features such as:
611
- Recursive and first-class functions
712
- ADTs, integers, bitvectors, strings, set-multiset-map abstractions
813
- Quantifiers
914
- ADT invariants
1015
- Dependent types
1116

12-
Interfacing with the solver can take place through the Scala API by constructing the AST
13-
corresponding to the query of interest and then feeding it to one of the solvers. For more
14-
information, see:
15-
- The usage [tutorial](doc/tutorial.md) gives some insight on how to use Inox as a library.
16-
- The tree [interpolators](doc/interpolations.md) provide easy tree construction/extraction for library use.
17-
- A more detailed description of the available solver/evaluator [API](doc/API.md) calls.
17+
Interfacing with the solver can take place through the Scala API by constructing
18+
the AST corresponding to the query of interest and then feeding it to one of the
19+
solvers. For more information, see:
20+
- The usage [tutorial](doc/tutorial.md) gives some insight on how to use Inox as
21+
a library.
22+
- The tree [interpolators](doc/interpolations.md) provide easy tree
23+
construction/extraction for library use.
24+
- A more detailed description of the available solver/evaluator
25+
[API](doc/API.md) calls.
1826
- A description of the [trees](doc/trees.md) API and how to extend them.
1927

2028
### Add Inox as a dependency
2129

22-
To add Inox as a dependency of your project, add the following lines to your `build.sbt`,
23-
where `VERSION` can be replaced by a tag (eg. `v1.1.5`), a branch name (eg. `master`)
24-
or a commit hash (eg. `6dfb351eee`).
30+
To use Inox as a Scala 3 dependency, refer to a specific git commit in your
31+
`build.sbt` file as follows:
2532

2633
```scala
27-
resolvers += "jitpack" at "https://jitpack.io"
28-
resolvers += "uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven"
34+
def remoteProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
2935

30-
libraryDependencies += "com.github.epfl-lara" % "inox" % "VERSION"
31-
```
32-
33-
Please see the [releases page](https://github.com/epfl-lara/inox/releases) for the latest Inox release.
34-
35-
**Use without the jitpack.io resolver**
36+
// choose a commit hash to pin Inox version
37+
val inoxRepository = "https://github.com/epfl-lara/inox.git"
38+
val inoxCommitHash = "467725efc4f7d7cf92017581ded04e257bee7368" // example commit
3639

37-
Alternatively, one can depend on Inox without using the [jitpack.io](jitpack.io) resolver
38-
in the following way:
39-
40-
```scala
41-
resolvers += "uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven"
40+
lazy val inox = remoteProject(inoxRepository, inoxCommitHash)
4241

43-
def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
44-
45-
lazy val inox = ghProject(
46-
"https://github.com/epfl-lara/inox.git",
47-
"6dfb351eeee44a3f13152bf510aceba7936d0e4d"
48-
)
42+
// and depend on it in your project
43+
lazy val yourProject = (project in file("."))
44+
.settings(
45+
// ...
46+
)
47+
.dependsOn(inox) // <<<
4948
```
5049

5150
Command-line Interface
5251
----------------------
5352

54-
One can also use Inox through command-line by using the [TIP](https://tip-org.github.io/) format
55-
to describe the relevant query. The easiest way to use the Inox command line is to simply
56-
[build](#building-inox) the project and use the generated script.
53+
One can also use Inox through command-line by using the
54+
[TIP](https://tip-org.github.io/) format to describe the relevant query. The
55+
easiest way to use the Inox command line is to simply [build](#building-inox)
56+
the project and use the generated `inox` script.
5757

5858
Solver Backends
5959
---------------
6060

61-
Inox relies on SMT solvers to solve the constraints it generates.
62-
Inox ships with the JVM SMT solver
63-
[Princess](http://www.philipp.ruemmer.org/princess.shtml)
64-
which should work out of the box on any system.
61+
Inox relies on SMT solvers to solve the constraints it generates. Inox ships
62+
with the JVM SMT solver [Princess](https://github.com/uuverifiers/princess) and
63+
Horn solver [Eldarica](https://github.com/uuverifiers/eldarica) which should
64+
work out of the box on any system.
6565

6666
You can also use the following external SMT solvers:
6767

6868
* Z3, https://github.com/Z3Prover/z3
69-
* CVC5, https://cvc5.github.io/
69+
* cvc5, https://cvc5.github.io/
7070
* CVC4, http://cvc4.cs.stanford.edu
7171

72-
Solver binaries that you install should match your operating
73-
system and your architecture. We recommend that you install
74-
these solvers as a binary and have their binaries available
75-
in the ``$PATH`` (as `z3` or `cvc4`). Once they are installed,
76-
you can instruct Inox to use a given sequence of solvers.
77-
The more solvers you have installed, the more successful Inox might get,
78-
because solver capabilities are incomparable.
72+
Solver binaries that you install should match your operating system and your
73+
architecture. We recommend that you install these solvers as a binary and have
74+
their binaries available in the ``$PATH`` (as `z3` or `cvc5`). Once they are
75+
installed, you can instruct Inox to use a given sequence of solvers. The more
76+
solvers you have installed, the more successful Inox might be, because solver
77+
capabilities are incomparable.
7978

8079
### Native Z3 API
8180

82-
In addition to these external binaries, a native Z3 API for
83-
Linux is bundled with Inox and should work out of the box
84-
(although having an external Z3 binary is a good idea in any
85-
case). If you [build](#building-inox) yourself, the generated
86-
script should put the native API onto your classpath. Otherwise,
87-
you will have to make sure the relevant jar from "unmanaged"
88-
is on your runtime classpath.
89-
90-
For other platforms than Linux, you will have to recompile the
91-
native Z3 communication layer yourself; see
92-
[ScalaZ3](https://github.com/epfl-lara/ScalaZ3) repository for
93-
information about how to build and package the project. You will
94-
then need to copy the resulting jar into the "unmanaged" directory
95-
named "scalaz3-$os-$arch-$scalaBinaryVersion.jar" (replace the
96-
$ variables by the relevant values).
81+
In addition to these external binaries, a native Z3 API for Linux is bundled
82+
with Inox and should work out of the box (although having an external Z3 binary
83+
is a good idea in any case). If you [build](#building-inox) yourself, the
84+
generated script should put the native API onto your classpath. Otherwise, you
85+
will have to make sure the relevant jar from [unmanaged](./unmanaged/) is on
86+
your runtime classpath.
87+
88+
For other platforms than Linux, you will have to recompile the native Z3
89+
communication layer yourself; see
90+
[ScalaZ3](https://github.com/epfl-lara/ScalaZ3) repository for information about
91+
how to build and package the project. You will then need to copy the resulting
92+
jar into the [unmanaged](./unmanaged/) directory named
93+
"scalaz3-$os-$arch-$scalaBinaryVersion.jar" (replace the $ variables by the
94+
relevant values).
9795

9896
### Solver Defaults
9997

100-
As of now the default solver is the native Z3 API. If that solver
101-
is unavailable, a series of fallbacks take place until the
102-
*princess* solver. You can specify which solver to use by
103-
e.g. giving the option
104-
``--solvers=smt-cvc4`` to use CVC4. Check the ``--solvers``
105-
line in Inox' help.
98+
As of now, the default solver is the native Z3 API. If that solver is
99+
unavailable, a series of fallbacks take place until the *princess* solver. You
100+
can specify which solver to use by e.g. giving the option ``--solvers=smt-cvc5``
101+
to use cvc5. Check the ``--solvers`` line in Inox' help.
106102

107103
Building Inox
108104
-------------
109105

110-
Inox is probably easiest to build on Linux-like platforms, but read on regarding other platforms.
106+
Inox is probably easiest to build on Linux-like platforms, but read on regarding
107+
other platforms.
111108

112-
Due to its nature, this documentation section may not always
113-
be up to date; we welcome pull requests with carefully
114-
written and tested improvements to the information below.
109+
Due to its nature, this documentation section may not always be up to date for
110+
different platforms; we welcome pull requests with carefully written and tested
111+
improvements to the information below.
115112

116113
**Requirements:**
117114

118-
* [Java SE Development Kit 8](http://www.oracle.com/technetwork/java/javase/downloads/jdk8-downloads-2133151.html) or [Java SE Development Kit 7](http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html) for your platform
119-
* SBT 0.13.x (Available from http://www.scala-sbt.org/)
120-
* The [git](https://git-scm.com/) command on your path
121-
**Note:** this is *only* required for version computation and
122-
you can avoid installing Git by using JGit (see the
123-
[related documentation](https://github.com/sbt/sbt-git#using-jgit)
124-
in `sbt-git`).
115+
* [Java Development Kit 17](https://openjdk.org/projects/jdk/17/) for your
116+
platform (and the corresponding runtime environment)
117+
* sbt >= 1.6.0 (Available from http://www.scala-sbt.org/)
118+
* The [git](https://git-scm.com/) command on your path
125119

126-
### Linux & Mac OS-X
120+
### Linux and macOS
127121

128122
Get the sources of Inox by cloning the official Inox repository:
129123

130-
```
131-
$ git clone https://github.com/epfl-lara/inox.git
124+
```console
125+
$ git clone https://github.com/epfl-lara/inox
132126
Cloning into 'inox'...
133127
// ...
134128
$ cd inox
135129
$ sbt clean compile
136130
// takes about 1 minutes
137131
```
138132

139-
Inox compilation generates an ``inox`` bash script that runs Inox with all
140-
the appropriate settings. This script expects argument files in the
141-
[TIP](https://tip-org.github.io/) input format and will report SAT or UNSAT
142-
to the specified properties.
133+
Inox compilation generates an ``inox`` bash script that runs Inox with all the
134+
appropriate settings. This script expects argument files in the
135+
[TIP](https://tip-org.github.io/) input format and will report SAT or UNSAT to
136+
the specified properties.
143137

144138
See ``./inox --help`` for more information about script usage.
145139

146140
### Windows
147141

148-
__Not yet tested!__
142+
__Not well tested!__
149143

150-
You will need a Git shell for windows, e.g.
151-
[Git for Windows](https://git-for-windows.github.io/).
152-
Building then proceeds as described [above](#linux--mac-os-x).
144+
We generally recommend the use of [Windows Subsystem for Linux
145+
(WSL)](https://learn.microsoft.com/en-us/windows/wsl/install) to run Inox on
146+
Windows. Hoewever, if you really wish to run Inox natively on Windows:
153147

154-
You will then need to either port the bash ``inox`` script to Windows, or run it
155-
under Cygwin.
148+
You will need a Git shell for Windows, e.g. [Git for
149+
Windows](https://git-for-windows.github.io/). Building then proceeds as
150+
described [above](#linux--mac-os-x).
151+
152+
You will then need to either port the ``inox`` bash script to Windows, or run it
153+
under [Cygwin](https://cygwin.com/).
156154

157155
You may be able to obtain additional tips on getting Inox to work on Windows
158-
from [Mikael Mayer](http://people.epfl.ch/mikael.mayer) or on
159-
[his dedicated web page](http://lara.epfl.ch/~mayer/leon/).
156+
from [Mikael Mayer](http://people.epfl.ch/mikael.mayer) or on [his dedicated web
157+
page](http://lara.epfl.ch/~mayer/leon/).
160158

161159
### Running Tests
162160

163-
Inox comes with a test suite. Consider running the following commands to
164-
invoke different test suites:
161+
Inox comes with a test suite. You can run the following commands to invoke
162+
different test suites:
165163

166-
```
164+
```console
167165
$ sbt test
168166
$ sbt it:test
169167
```

0 commit comments

Comments
 (0)