Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.

diff --git a/AUTHORS b/AUTHORS
index 92a4b702f1f774825eaaeb50874bd3462fd189c0..1d4a67e5bf79db4a9c681a97ad146717b5210122 100644 (file)
--- a/AUTHORS
+++ b/AUTHORS
@@ -24,6 +24,7 @@ The core designers and authors of CVC4 are:
   Mathias Preiner, Stanford University
   Andrew Reynolds, The University of Iowa, EPFL
   Cesare Tinelli, The University of Iowa
+  Yoni Zohar, Stanford University
 
 Other contributors to the CVC4 codebase are listed in the THANKS file.
 

diff --git a/NEWS b/NEWS
index f23833bb630c6ed55450007a39120192fb68ec42..a9ce4d68f7d26f50d62cf465d32104b3efcf5b5b 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,34 @@
 This file contains a summary of important user-visible changes. 
 
+Changes since 1.5
+=================
+
+New Features:
+* A new theory of floating points.
+* Novel approach for solving quantified bit-vectors (BV).
+* Eager bit-blasting: Support for SAT solver CaDiCaL.
+* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
+* Support for transcendental functions (sin, cos, exp).
+* Support for new operators in strings, including string inequality (str.<=)
+  and string code (str.code).
+* Support for automated rewrite rule generation from sygus (*.sy) inputs using
+  syntax-guided enumeration (option --sygus-rr).
+
+Improvements:
+* Incremental unsat core support.
+* Strings rewriter.
+* Further development of rewrite rules for the theory of strings and regular
+  expressions.
+* Many optimizations for syntax-guided synthesis, including improved symmetry
+  breaking for enumerative search and specialized algorithms for
+  programming-by-examples conjectures.
+
+Changes:
+* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
+  support for CryptoMinisat 5.
+* The LFSC proof checker now resides in its own repository on GitHub at
+  https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
+
 Changes since 1.4
 =================
 

diff --git a/README b/README
index 593a18bf2acd3f52faca86257ff643f81d19774f..0a8a37879ce379020bbaf32b32067c2aafaacc57 100644 (file)
--- a/README
+++ b/README
@@ -1,4 +1,4 @@
-This is CVC4 release version 1.5.  For build and installation notes,
+This is CVC4 release version 1.6.  For build and installation notes,
 please see the INSTALL file included with this distribution.
 
 The project leaders are Clark Barrett (Stanford University) and Cesare

diff --git a/RELEASE-NOTES b/RELEASE-NOTES
index 02c201003bf153ae05bf72edc3a94ace6e026e6a..c9c1fabb5d8652d771b7d1aa278923aab9ea7f19 100644 (file)
--- a/RELEASE-NOTES
+++ b/RELEASE-NOTES
@@ -1,4 +1,4 @@
-Release Notes for CVC4 1.5, July 2017
+Release Notes for CVC4 1.6, June 2018
 
 ** Getting started
 
@@ -17,7 +17,7 @@ this, you can use the --lang option.
 
 The CVC family of systems relies on Type Correctness Conditions (TCCs) when
 mixing two types that have a compatible base type.  TCCs, and the checking of
-such, are not supported by CVC4 1.5.  This is an issue when mixing integers and
+such, are not supported by CVC4 1.6.  This is an issue when mixing integers and
 reals.  A function defined only on integers can be applied to REAL (as INT is a
 subtype of REAL), and CVC4 will not complain.  It is up to the user to ensure 
 that the REAL expression must be an integer.  If the REAL expression is not
@@ -117,14 +117,14 @@ heap.
 
 ** Proof support
 
-CVC4 1.5 has support for proofs when using uninterpreted functions, arrays,
+CVC4 1.6 has support for proofs when using uninterpreted functions, arrays,
 bitvectors, or their combinations, and proofs are enabled by default.
 (Run the configure script with --disable-proof to disable proofs).  Proofs
 are exported in LFSC format.
 
 ** Nonlinear arithmetic
 
-CVC4 1.5 has a state-of-the-art linear arithmetic solver as well as some
+CVC4 1.6 has a state-of-the-art linear arithmetic solver as well as some
 heuristic support for non-linear arithmetic.
 
 ** Portfolio solving

diff --git a/THANKS b/THANKS
index 09fd9d44a8090ed2ee97ce5a5b2f72930816fe1a..8eb19e8dbb27f309f90cee8b9f8163e2203bf8eb 100644 (file)
--- a/THANKS
+++ b/THANKS
@@ -16,6 +16,8 @@ Thanks to:
 - Finn Haedicke of University of Bremen, Germany for fixing namespace specifiers
   in CVC4's version of minisat in 2015.
 
+- Pat Hawks for writing tests for CVC4's Java API.
+
 - Thomas Hunger for some important patches to CVC4's SWIG interfaces in March
   2014.
 
@@ -28,7 +30,11 @@ Thanks to:
 - Jordy Ruiz of University of Toulouse for fixing throw specifiers on the theory
   output channels in 2015.
 
-- Fabian Wolff in 2016 for fixing several spelling mistakes.
-
 - Clement Pit-Claudel of MIT for improving the signal handling support for
   Windows builds in 2017.
+
+- Arjun Viswanathan for improvements in the CVC and the SMT2 parser.
+
+- Fabian Wolff in 2016 for fixing several spelling mistakes.
+
+- Justin Xu for contributing to refactoring CVC4's preprocessing infrastructure.