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. 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.
+* 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.
+
Changes since 1.2
=================
-* SMT-LIB support for abs, to_real, to_int, is_int
-* Expr::substitute() now capable of substituting operators (e.g.,
- function symbols under an APPLY_UF)
-* Support in linear logics for /, div, and mod by constants.
-* Support for TPTP's TFF and TFA formats.
-* We no longer permit model or proof generation if there's been an
- intervening push/pop.
+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. API changes to Command infrastructure to support.
-* A new theory of strings: word (dis-)equations, length constraints,
- regular expressions.
+ 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.
-* bv2nat/int2bv functionality
-* User-defined symbols (define-funs) are no longer reported in the output
- of get-model commands.
+
+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
=================
"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> Mon, 02 Dec 2013 16:58:50 -0500
+-- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500
projects / cvc5.git / blobdiff