1 This file contains a summary of important user-visible changes.
12 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
14 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
15 * Support in linear logics for /, div, and mod by constants (with the
16 --rewrite-divk command line option).
17 * Parsing support for TPTP's TFF and TFA formats.
18 * A new theory of strings: word (dis-)equations, length constraints,
20 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
22 * New :command-verbosity SMT option to silence success and error messages
23 on a per-command basis, and API changes to Command infrastructure to
27 * It is no longer permitted to request model or proof generation if there's
28 been an intervening push/pop.
29 * User-defined symbols (define-funs) are no longer reported in the output
30 of get-model commands.
31 * Exit codes are now more standard for UNIX command-line tools. Exit code
32 zero means no error---but the result could be sat, unsat, or unknown---and
36 * Expr::substitute() now capable of substituting operators (e.g.,
37 function symbols under an APPLY_UF)
38 * Numerous improvements to the Java language bindings
43 * Real arithmetic now has three simplex solvers for exact precision linear
44 arithmetic: the classical dual solver and two new solvers based on
45 techniques for minimizing the sum of infeasibilities. GLPK can now be used
46 as a heuristic backup to the exact precision solvers. GLPK must be enabled
47 at configure time. See --help for more information on enabling these solvers.
48 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
49 * support for theory "alternates": new ability to prototype new decision
50 procedures that are selectable at runtime
56 * bit-vector solver now has a specialized decision procedure for unsigned bit-
58 * numerous important bug fixes, performance improvements, and usability
60 * support for multiline input in interactive mode
61 * Win32-building support via mingw
62 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
63 * user patterns for quantifier instantiation are now supported in the
65 * --finite-model-find was incomplete when using --incremental, now fixed
66 * the E-matching procedure is slightly improved
67 * Boolean terms are now supported in datatypes
68 * tuple and record support have been added to the compatibility library
69 * driver verbosity change: for printing all commands as they're executed, you
70 now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
71 allows tracing the solver's activities (with -v and -vv) without having too
73 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
74 use -q. Previously, this would silence all output (including "sat" or
75 "unsat") as well. Now, single -q silences messages and warnings, and
76 double -qq silences all output (except on exception or signal).
78 -- Morgan Deters <mdeters@cs.nyu.edu> Thu, 05 Dec 2013 14:22:26 -0500