diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-07 16:56:58 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-09-07 16:56:58 +0200 |
| commit | 4bfaa0e4f2f9c2e05c245258b95bc3fe643f3e25 (patch) | |
| tree | e3730bfb8cf0ea2b322777708a20cc6588c891a5 /INSTALL.md | |
| parent | a8863500307f01b9df6d13b19db61066d219c553 (diff) | |
| parent | 6a3458f997f5e0033f9cd7f8302dd92fa4fad337 (diff) | |
| download | smtcoq-4bfaa0e4f2f9c2e05c245258b95bc3fe643f3e25.tar.gz smtcoq-4bfaa0e4f2f9c2e05c245258b95bc3fe643f3e25.zip | |
Merge remote-tracking branch 'remotes/origin/master' into coq-8.10
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 19 |
1 files changed, 10 insertions, 9 deletions
@@ -140,13 +140,13 @@ make install To use SMTCoq, we recommend installing the following two SMT solvers: -- [CVC4](http://cvc4.cs.nyu.edu) +- CVC4 - [veriT](https://verit.loria.fr) SMTCoq also supports the following SAT solver for propositional reasoning: -- [zChaff](http://www.princeton.edu/~chaff/zchaff.html) +- [ZChaff](http://www.princeton.edu/~chaff/zchaff.html) Please download the solvers you would like to use via the links below (since SMTCoq might not support other versions), and follow the @@ -156,10 +156,11 @@ proof production mode**, as detailed below. ### CVC4 -Use the stable version 1.6 of CVC4 that is available in the **stable -versions** column at [http://cvc4.cs.stanford.edu/downloads]. You can -either get a binary (recommended) or compile it from the sources using -the following commands: +Use the stable version 1.6 of CVC4 that is available either: +- as a [Linux binary](http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.6-x86_64-linux-opt) +- as a [Windows binary](http://cvc4.cs.stanford.edu/downloads/builds/win64-opt/cvc4-1.6-win64-opt.exe) +- as a [MacOs binary](https://github.com/cvc5/cvc5/releases/download/1.6/cvc4-1.6-macos-opt) +- from [the sources](https://github.com/cvc5/cvc5/releases/tag/1.6), using the following commands: ``` ./configure make @@ -177,7 +178,7 @@ your shell), export the following environment variable to make it point at the export LFSCSIGS="$HOME/path/to/smtcoq/src/lfsc/tests/signatures/" ``` -If you installed SMTCoq via opam (recommended), the path for to SMTCoq +If you installed SMTCoq via opam (recommended), the path to SMTCoq (to replace `path/to/smtcoq`) is `.opam/NAMEOFTHESWITCH/.opam-switch/sources/coq-smtcoq.dev+COQVERSION` where `NAMEOFTHESWITCH` must be replaced by the name of the opam switch @@ -209,9 +210,9 @@ your path. If you encounter problems to compile it, please report an issue. -### zChaff +### ZChaff -zChaff can be downloaded +ZChaff can be downloaded [here](http://www.princeton.edu/~chaff/zchaff.html). It is not actively maintained, so you might encounter problems to compile it on modern platforms. [This |