X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=NEWS;h=d9e1f9076de859d0863ed3d7fd0d72088a428593;hb=afc70ac962185b97e10f4e796f46c638ed1e18ab;hp=84debe315f92ee589bdad2e9d43e26a2e660de18;hpb=eb63fdb37b2784d6d4340402cd0ee00ceb8f5041;p=cvc5.git

diff --git a/NEWS b/NEWS
index 84debe315..d9e1f9076 100644
--- a/NEWS
+++ b/NEWS
@@ -1,12 +1,104 @@
 This file contains a summary of important user-visible changes.
 
+Changes since 1.6
+=================
+
+New Features:
+* Proofs:
+  * Support for bit-vector proofs with eager bitblasting (older versions only
+    supported proofs with lazy bitblasting).
+* Strings:
+  * Support for `str.replaceall` operator.
+  * New option `--re-elim` to reduce regular expressions to extended string
+    operators, resulting in better performance on regular expression benchmarks
+    (enabled by default).
+* SyGuS:
+  * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
+    CVC4's SyGuS solver to find a sufficient condition such that the
+    conjunction of the condition and the formula is unsatisfiable.
+  * Support for two new term enumerator strategies: variable agnostic
+    (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
+    By default, CVC4 tries to choose the best term enumerator strategy
+    automatically based on the input (`--sygus-active-gen=auto`).
+  * Support for streaming solutions of increasingly smaller size when using the
+    PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
+    and printed, the solver will continue to look for new solutions and print
+    those, if any, that are smaller than previously printed solutions.
+  * Support for unification-based techniques in non-separable specifications
+    (`--sygus-unif`). For solving invariant problems a dedicate mode
+    (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
+    solutions using heuristic decision tree learning.
+
+Improvements:
+* Strings:
+  * Significantly better performance on string benchmarks over the core theory
+    and those with extended string functions like substring, contains, and
+    replace.
+
+Changes:
+* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
+              actual behavior.
+* Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
+* The CVC3 compatibility layer has been removed.
+* The build system now uses CMake instead of Autotools. Please refer to
+  [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
+  up-to-date instructions on how to build CVC4.
+
+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). In SMT2 input, this
+  can be enabled by adding T to the logic (e.g., QF_NRAT).
+* 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.
+* 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
 =================
 
+* Improved heuristics for reasoning about non-linear arithmetic.
+* Native support for syntax-guided synthesis (sygus).
+* Support for many new heuristics for reasoning with quantifiers, including
+  finite model finding.
+* Support for proofs for uninterpreted functions, arrays, bitvectors, and
+  their combinations.
+* Performance improvements to existing theories.
+* A new theory of sets with cardinality and relations.
+* A new theory of strings.
 * Support for unsat cores.
+* Support for separation logic constraints.
 * Simplification mode "incremental" no longer supported.
 * Support for array constants in constraints.
-* Syntax for array models have changed in some language front-ends.
+* Syntax for array models has changed in some language front-ends.
+* New input/output languages supported: "smt2.0" and "smtlib2.0" to
+  force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
+  "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
+  "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
+  version 2.6.  If an :smt-lib-version is set in the input, that overrides
+  the command line.
+* Abstract values in SMT-LIB models are now ascribed types (with "as").
+* In SMT-LIB model output, real-sorted but integer-valued constants are
+  now printed in accordance with the standard (e.g. "1.0").
 
 Changes since 1.3
 =================
@@ -106,5 +198,3 @@ Changes since 1.0
   use -q.  Previously, this would silence all output (including "sat" or
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
-
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 02 Jul 2014 14:45:05 -0400