diff options
| -rw-r--r-- | CMakeLists.txt | 4 | ||||
| -rw-r--r-- | INSTALL.md | 20 | ||||
| -rw-r--r-- | NEWS | 13 |
3 files changed, 26 insertions, 11 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 66872f61e..e4d4aaeda 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -10,10 +10,10 @@ set(CVC4_MINOR 8) # Minor component of the version of CVC4. set(CVC4_RELEASE 0) # Release component of the version of CVC4. # Extraversion component of the version of CVC4. -set(CVC4_EXTRAVERSION "-prerelease") +set(CVC4_EXTRAVERSION "") # Shared library versioning. Increment SOVERSION for every new CVC4 release. -set(CVC4_SOVERSION 6) +set(CVC4_SOVERSION 7) # Full release string for CVC4. if(CVC4_RELEASE) 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 @@ -4,6 +4,8 @@ Changes since 1.7 ================= New Features: +* New C++ and Python API: CVC4 has a new, more streamlined API. We plan to + make CVC4 1.8 the last version that ships with the legacy API. * Strings: Full support of the new SMT-LIB standard for the theory of strings, including: * Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`, @@ -17,12 +19,22 @@ New Features: function symbols. Support for higher-order constraints can be enabled by the option `--uf-ho`. * Support for set comprehension binders `comprehension`. +* Eager bit-blasting: Support for SAT solver Kissat. Improvements: * API: Function definitions can now be requested to be global. If the `global` parameter is set to true, they persist after popping the user context. +* Java/Python bindings: The bindings now allow users to catch exceptions +* Arithmetic: Performance improvements + * Linear solver: New lemmas inspired by unit-cube tests + * Non-linear solver: Expanded set of axioms +* Ackermannization: The Ackermannization preprocessing pass now supports + uninterpreted sorts and as a result all QF_UFBV problems are supported in + combination with eager bit blasting. Changes: +* CVC language: Models printed in the CVC language now include an explicit end + marker to facilitate the communication over pipes with CVC4. * API change: `SmtEngine::query()` has been renamed to `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to `Result::Entailment` along with corresponding changes to the enum values. @@ -44,6 +56,7 @@ Changes: `./contrib/sygus-v1-to-v2.sh`. * Support for user-provided rewrite rule quantifiers have been removed. * Support for certain option aliases have been removed. +* Support for parallel portfolio builds has been removed. Changes since 1.6 ================= |