-This file contains a summary of important user-visible changes.
+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). 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 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
=================
-* Timed statistics are now properly updated even on process abort.
+* CVC4 now supports libc++ in addition to libstdc++ (this especially
+ helps on Mac OS Mavericks).
* The LFSC proof checker has been incorporated into CVC4 sources.
+* Theory of finite sets, handling the MLSS fragment (singleton, union,
+ intersection, set subtraction, membership and subset).
* By default, CVC4 builds in "production" mode (optimized, with fewer
internal checks on). The common alternative is a "debug" build, which
- is much slower. CVC4 also builds with GPL dependences by default now
- (if those libraries are available), as this is the best-performing
- version of CVC4. However, the new configure option "--bsd" disables
- these GPL dependences and builds the best-performing BSD-licenced version
- of CVC4.
+ is much slower. By default, CVC4 builds with no GPL'ed dependences.
+ However, this is not the best-performing version; for that, you should
+ configure with "--enable-gpl --best", which links against GPL'ed
+ libraries that improve usability and performance. For details on
+ licensing and dependences, see the README file.
+* Small API adjustments to Datatypes to even out the API and make it
+ function better in Java.
+* Timed statistics are now properly updated even on process abort.
+* Better automatic handling of output language setting when using CVC4
+ via API. Previously, the "automatic" language setting was sometimes
+ (though not always) defaulting to the internal "AST" language; it
+ should now (correctly) default to the same as the input language
+ (if the input language is supported as an output language), or the
+ "CVC4" native output language if no input language setting is applied.
+* The SmtEngine cannot be safely copied with the copy constructor.
+ Previous versions inadvertently permitted clients to do this via the
+ API. This has been corrected, copy and assignment of the SmtEngine
+ is no longer permitted.
Changes since 1.2
=================
"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> Thu, 05 Dec 2013 14:22:26 -0500