Update info for 1.8 release (#4633)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 66872f61e7ea81efafc839c32d83a925d41d802b..e4d4aaeda274f47875eff792fee6308d3a8af1df 100644 (file)
--- 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 b95450dffb569fd882ad2f1d8343daab68e54a0d..0c78e9fb1822bc4f605b248ed0fdd663d1dcbfd0 100644 (file)
--- 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

diff --git a/NEWS b/NEWS
index d778540088bd8169ff69e86c2ceb2a755e82cf38..60ff9dbc8e8fda5f42e6f9082247d026f0fdebe8 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -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
 =================