diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-19 09:59:27 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-19 09:59:27 -0700 |
commit | 5247901077efbc7b9016ba35fded7a6ab459a379 (patch) | |
tree | b0ffb77db20ef3cb5fde3210dbd866f3f5536063 /INSTALL.md | |
parent | 039a642610f570f3367a73a3a29082152a2736f2 (diff) |
Update info for 1.8 release (#4633)
Diffstat (limited to 'INSTALL.md')
-rw-r--r-- | INSTALL.md | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/INSTALL.md b/INSTALL.md index b95450dff..0c78e9fb1 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,5 +1,5 @@ -CVC4 prerelease version 1.8. -============================ +CVC4 release version 1.8 +======================== ## Building CVC4 @@ -114,6 +114,15 @@ It can be installed using the `contrib/get-cryptominisat` script. Configure CVC4 with `configure.sh --cryptominisat` to build with this dependency. +### Kissat (Optional SAT solver) + +[Kissat](https://github.com/arminbiere/kissat) +is a SAT solver that can be used for solving bit-vector problems with eager +bit-blasting. This dependency may improve performance. +It can be installed using the `contrib/get-kissat` script. +Configure CVC4 with `configure.sh --kissat` to build with this +dependency. + ### LFSC (The LFSC Proof Checker) [LFSC](https://github.com/CVC4/LFSC) is required to check proofs internally @@ -179,13 +188,6 @@ If you choose to use CVC4 with GNU Readline support, you are licensing CVC4 under that same license. (Usually CVC4's license is more permissive; see above discussion.) -### libboost_thread: The Boost C++ threading library (Portfolio Builds) - -The [Boost](http://www.boost.org) C++ threading library (often packaged -independently of the Boost base library) is needed to run CVC4 in "portfolio" -(multithreaded) mode. -Check your distribution for a package named "libboost-thread-dev" or similar. - ### Boost C++ base libraries (Examples) The [Boost](http://www.boost.org) C++ base library is needed for some examples |