This file contains a summary of important user-visible changes.
+Changes since 1.3
+=================
+
+* Timed statistics are now properly updated even on process abort.
+* The LFSC proof checker has been incorporated into CVC4 sources.
+* 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.
+* Small API adjustments to Datatypes to even out the API and make it
+ function better in Java.
+
+Changes since 1.2
+=================
+
+New features:
+* SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
+ previously missing
+* New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
+* Support in linear logics for /, div, and mod by constants (with the
+ --rewrite-divk command line option).
+* Parsing support for TPTP's TFF and TFA formats.
+* A new theory of strings: word (dis-)equations, length constraints,
+ regular expressions.
+* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
+ resolved.
+* New :command-verbosity SMT option to silence success and error messages
+ on a per-command basis, and API changes to Command infrastructure to
+ support this.
+
+Behavioral changes:
+* It is no longer permitted to request model or proof generation if there's
+ been an intervening push/pop.
+* User-defined symbols (define-funs) are no longer reported in the output
+ of get-model commands.
+* Exit codes are now more standard for UNIX command-line tools. Exit code
+ zero means no error---but the result could be sat, unsat, or unknown---and
+ nonzero means error.
+
+API changes:
+* Expr::substitute() now capable of substituting operators (e.g.,
+ function symbols under an APPLY_UF)
+* Numerous improvements to the Java language bindings
+
+Changes since 1.1
+=================
+
+* Real arithmetic now has three simplex solvers for exact precision linear
+ arithmetic: the classical dual solver and two new solvers based on
+ techniques for minimizing the sum of infeasibilities. GLPK can now be used
+ as a heuristic backup to the exact precision solvers. GLPK must be enabled
+ at configure time. See --help for more information on enabling these solvers.
+* added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
+* support for theory "alternates": new ability to prototype new decision
+ procedures that are selectable at runtime
+* various bugfixes
+
Changes since 1.0
=================
-* tuple and record support in the compatibility library
-* user patterns are now supported in the SMT-LIBv1.2 parser
+* bit-vector solver now has a specialized decision procedure for unsigned bit-
+ vector inequalities
+* numerous important bug fixes, performance improvements, and usability
+ improvements
+* support for multiline input in interactive mode
+* Win32-building support via mingw
* SMT-LIB get-model output now is easier to machine-parse: contains (model...)
-* Win32 support via mingw
-* for printing commands as they're invoked from the driver, you now need
- verbosity of 3 or higher (e.g. -vvv) instead of verbosity 1 or higher (-v).
- This allows tracing the solver's activities without having too much output.
-* multiline support in interactive mode
-* To make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
+* user patterns for quantifier instantiation are now supported in the
+ SMT-LIBv1.2 parser
+* --finite-model-find was incomplete when using --incremental, now fixed
+* the E-matching procedure is slightly improved
+* Boolean terms are now supported in datatypes
+* tuple and record support have been added to the compatibility library
+* driver verbosity change: for printing all commands as they're executed, you
+ now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
+ allows tracing the solver's activities (with -v and -vv) without having too
+ much output.
+* to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
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).
-* Boolean term support in datatypes
--- Morgan Deters <mdeters@cs.nyu.edu> Wed, 20 Mar 2013 20:03:50 -0400
+-- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500
projects / cvc5.git / blobdiff