From 4ab9ed885784fdb1e52e0d1f12587ede305d1d9b Mon Sep 17 00:00:00 2001 From: Emiko Soroka Date: Sun, 7 Jul 2024 13:29:39 -0700 Subject: [PATCH] Fix confusing mess about Z3 being installed automatically --- docs/src/installation.md | 35 ++++++++++++++++++++++++----------- docs/src/release_notes.md | 4 ++++ 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/docs/src/installation.md b/docs/src/installation.md index 68639c9..fedc1cf 100644 --- a/docs/src/installation.md +++ b/docs/src/installation.md @@ -4,7 +4,9 @@ Pages = ["installation.md"] Depth = 3 ``` -**NOTE: To successfully use this package you will need to install a back-end solver.** [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) and [cvc5](https://cvc5.github.io/) are currently supported. You should be able to [use other solvers](advanced.md#Custom-solver-options-and-using-other-solvers) as long as they implement the SMT-LIB standard. +**NOTE: To successfully use this package you need a back-end solver installed.** [Z3](https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/) will automatically be installed using `z3_jll`. + +You can also use [cvc5](https://cvc5.github.io/) (although you will have to install it yourself). To use other solvers that implement the SMT-LIB standard, [check this page](advanced.md#Custom-solver-options-and-using-other-solvers) for guidelines. ## Installing Satisfiability The usual way! `using Pkg; Pkg.add("Satisfiability")` @@ -14,8 +16,6 @@ Satisfiability will automatically install Z3 on your system if it isn't already Satisfiability uses Julia's Base.Process library to interact with solvers. To successfully install a solver for this package, all you need to do is make sure the appropriate command works in your machine's terminal. ### Debian Linux -**To install Z3 manually** (you shouldn't need to do this), use `sudo apt-get install z3`. -If you can launch Z3 from the command line by typing `z3 -smt2 -in`, your installation is correct. **To install CVC5:** * Download the appropriate binary [here](https://cvc5.github.io/downloads.html) and save it as `cvc5`. (Note: if you already have `cvc5` installed under the name `cvc5-linux`, make a symlink to the name `cvc5` or [customize your solver command](advanced.md#Custom-solver-options-and-using-other-solvers) to use the name `cvc5-linux`.) @@ -23,17 +23,35 @@ If you can launch Z3 from the command line by typing `z3 -smt2 -in`, your instal * Most users should move the binary to `/usr/local/bin`. This allows it to be found from the command line. If you can launch CVC5 from the command line by typing `cvc5 --interactive --produce-models`, your installation is correct. +**To install Z3 manually** (you shouldn't need to do this), use `sudo apt-get install z3`. +If you can launch Z3 from the command line by typing `z3 -smt2 -in`, your installation is correct. + ### MacOS -**To install Z3 manually** (you shouldn't need to do this): -* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases) and install following the instructions on that page. -* If you can open your Terminal and launch z3 by typing `z3 -smt2 -in`, your installation is correct. **To install CVC5** * Download the appropriate binary [here](https://cvc5.github.io/downloads.html) and save it as `cvc5`. (Note: if you already have `cvc5` installed under another name, make a symlink to the name `cvc5` or [customize your solver command](advanced.md#Custom-solver-options-and-using-other-solvers) to use the name you already have.) * Most users should move the binary to `/usr/local/bin`. This allows it to be found from the command line. * If you can open your Terminal and launch CVC5 by typing `cvc5 --interactive --produce-models`, your installation is correct. + +**To install Z3 manually** (you shouldn't need to do this): + +* `brew install z3` should work if you have Homebrew installed. + +Alternatively: + +* Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases) and install following the instructions on that page. +* If you can open your Terminal and launch z3 by typing `z3 -smt2 -in`, your installation is correct. + + ### Windows + +**To install cvc5** +* Download the [latest release](https://github.com/cvc5/cvc5/releases/) of cvc5. Make sure you save the exe file as `cvc5.exe`, not `cvc5-Win64.exe` or anything else. +* Make a note of the file path where you put cvc5.exe. +* Add the cvc5.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)). +If you can open the Windows command line and launch cvc5 by typing `cvc5 --interactive --produce-models`, your installation is correct. + **To install Z3 manually** (you shouldn't need to do this): * Download the appropriate zip file for the [latest Z3 release](https://github.com/Z3Prover/z3/releases). * Unzip the file and put it in your applications folder. @@ -41,11 +59,6 @@ If you can launch CVC5 from the command line by typing `cvc5 --interactive --pro * Add the z3.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)). If you can open the WIndows command line and launch z3 by typing `z3.exe -smt2 -in`, your installation is correct. -**To install cvc5** -* Download the [latest release](https://github.com/cvc5/cvc5/releases/) of cvc5. Make sure you save the exe file as `cvc5.exe`, not `cvc5-Win64.exe` or anything else. -* Make a note of the file path where you put cvc5.exe. -* Add the cvc5.exe file path to your PATH environment variable ([here's how to do this](https://helpdeskgeek.com/windows-10/add-windows-path-environment-variable/)). -If you can open the Windows command line and launch cvc5 by typing `cvc5 --interactive --produce-models`, your installation is correct. ### Installing Yices Please follow the [official instructions](https://yices.csl.sri.com/). diff --git a/docs/src/release_notes.md b/docs/src/release_notes.md index 4d7f3e9..eddf9b0 100644 --- a/docs/src/release_notes.md +++ b/docs/src/release_notes.md @@ -3,6 +3,10 @@ Pages = ["release_notes.md"] Depth = 3 ``` + +# Version 0.1.3 (May 23, 2024) +* Automatically download Z3 using `z3_jll` when Satisfiability.jl is installed. + # Version 0.1.1 (December 15, 2023) * Fixed bugs in issues #21 and #26. * Added remaining operators defined in SMT-LIB QF_BV (bitvector) specification (issue #22)