1 This file contains a summary of important user-visible changes.
6 * SMT-LIB support for abs, to_real, to_int, is_int
7 * Expr::substitute() now capable of substituting operators (e.g.,
8 function symbols under an APPLY_UF)
9 * Support in linear logics for /, div, and mod by constants.
10 * Support for TPTP's TFF and TFA formats.
11 * We no longer permit model or proof generation if there's been an
13 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
15 * New :command-verbosity SMT option to silence success and error messages
16 on a per-command basis. API changes to Command infrastructure to support.
17 * A new theory of strings. Currently, only word equations are supported.
22 * Real arithmetic now has three simplex solvers for exact precision linear
23 arithmetic: the classical dual solver and two new solvers based on
24 techniques for minimizing the sum of infeasibilities. GLPK can now be used
25 as a heuristic backup to the exact precision solvers. GLPK must be enabled
26 at configure time. See --help for more information on enabling these solvers.
27 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
28 * support for theory "alternates": new ability to prototype new decision
29 procedures that are selectable at runtime
35 * bit-vector solver now has a specialized decision procedure for unsigned bit-
37 * numerous important bug fixes, performance improvements, and usability
39 * support for multiline input in interactive mode
40 * Win32-building support via mingw
41 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
42 * user patterns for quantifier instantiation are now supported in the
44 * --finite-model-find was incomplete when using --incremental, now fixed
45 * the E-matching procedure is slightly improved
46 * Boolean terms are now supported in datatypes
47 * tuple and record support have been added to the compatibility library
48 * driver verbosity change: for printing all commands as they're executed, you
49 now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
50 allows tracing the solver's activities (with -v and -vv) without having too
52 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
53 use -q. Previously, this would silence all output (including "sat" or
54 "unsat") as well. Now, single -q silences messages and warnings, and
55 double -qq silences all output (except on exception or signal).
57 -- Morgan Deters <mdeters@cs.nyu.edu> Wed, 03 Apr 2013 13:06:35 -0400