This file contains a summary of important user-visible changes.
-Changes since 1.3
-=================
-
-* Building with libc++ instead of libstdc++ (on Mac especially).
-* 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.
-* 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
-=================
-
-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
-=================
-
-* 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...)
-* 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).
-
--- Morgan Deters <mdeters@cs.nyu.edu> Mon, 16 Jun 2014 22:23:12 -0400
+Changes since CVC4 1.8
+======================
+
+New Features:
+* CaDiCaL is now a required dependency.
+* SymFPU is now a required dependency.
+* New unsat-core production modes based on the new proof infrastructure
+ (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption feature
+ of Minisat (`--unsat-cores-mode=assumptions`). The mode based on SAT
+ assumptions + preprocessing proofs is the new default.
+* A new parametric theory of sequences whose syntax is compatible with the
+ syntax for sequences used by Z3.
+* Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
+ if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
+* Integers:
+ * Support for an integer operator `(_ iand n)` that returns the bitwise `and`
+ of two integers, seen as integers modulo n.
+ * Support for an integer operator `int.pow2`, used as `(int.pow2 x)` which
+ represents 2 to the power of x.
+* Strings:
+ * Support for `str.indexof_re(s, r, n)`, which returns the index of the first
+ occurrence of a regular expression `r` in a string `s` after index `n` or
+ -1 if `r` does not match a substring after `n`.
+* A new option to compute minimal unsat cores (`--minimal-unsat-cores`).
+
+Improvements:
+* New API: Added functions to retrieve the heap/nil term when using separation
+ logic.
+
+Changes:
+* SyGuS: Removed support for SyGuS-IF 1.0.
+* Removed support for the (non-standard) `define` command.
+* Removed Java and Python bindings for the legacy API.
+* Interactive shell: the GPL-licensed Readline library has been replaced the
+ BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
+ of Readline. Without selecting optional GPL components, Editline-enabled CVC4
+ builds will be BSD licensed.
+* The semantics for division and remainder operators in the CVC language now
+ correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero
+ modulus results in a constant value, instead of an uninterpreted one). As a
+ result the option `--bv-div-zero-const` has been removed. Similarly, when no
+ language is set, the API semantics now correspond to the SMT-LIB 2.6
+ semantics.
+* The `competition` build type includes the dependencies used for SMT-COMP by
+ default. Note that this makes this build type produce GPL-licensed binaries.
+* Bit-vector operator bvxnor was previously mistakenly marked as
+ left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
+ now restrict bvxnor to only allow two operands in order to avoid confusion
+ about the semantics, since the behavior of n-ary operands to bvxnor is now
+ undefined in SMT-LIB.
+* SMT-LIB output for `get-model` command now conforms with the standard,
+ and does *not* begin with the keyword `model`. The output
+ is the same as before, only with this word removed from the beginning.
+* Building with Python 2 is now deprecated.
+* Removed the option `--rewrite-divk` (now effectively enabled by default).
+* Removed support for redundant logics ALL_SUPPORTED and QF_ALL_SUPPORTED,
+ use ALL and QF_ALL instead.
projects / cvc5.git / blobdiff