1 This file contains a summary of important user-visible changes.
6 * Improved heuristics for reasoning about non-linear arithmetic.
7 * Native support for syntax-guided synthesis (sygus).
8 * Support for many new heuristics for reasoning with quantifiers, including
10 * Support for proofs for uninterpreted functions, arrays, bitvectors, and
12 * Performance improvements to existing theories.
13 * A new theory of sets with cardinality and relations.
14 * A new theory of strings.
15 * Support for unsat cores.
16 * Support for separation logic constraints.
17 * Simplification mode "incremental" no longer supported.
18 * Support for array constants in constraints.
19 * Syntax for array models has changed in some language front-ends.
20 * New input/output languages supported: "smt2.0" and "smtlib2.0" to
21 force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
22 "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
23 "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
24 version 2.6. If an :smt-lib-version is set in the input, that overrides
26 * Abstract values in SMT-LIB models are now ascribed types (with "as").
27 * In SMT-LIB model output, real-sorted but integer-valued constants are
28 now printed in accordance with the standard (e.g. "1.0").
33 * CVC4 now supports libc++ in addition to libstdc++ (this especially
34 helps on Mac OS Mavericks).
35 * The LFSC proof checker has been incorporated into CVC4 sources.
36 * Theory of finite sets, handling the MLSS fragment (singleton, union,
37 intersection, set subtraction, membership and subset).
38 * By default, CVC4 builds in "production" mode (optimized, with fewer
39 internal checks on). The common alternative is a "debug" build, which
40 is much slower. By default, CVC4 builds with no GPL'ed dependences.
41 However, this is not the best-performing version; for that, you should
42 configure with "--enable-gpl --best", which links against GPL'ed
43 libraries that improve usability and performance. For details on
44 licensing and dependences, see the README file.
45 * Small API adjustments to Datatypes to even out the API and make it
46 function better in Java.
47 * Timed statistics are now properly updated even on process abort.
48 * Better automatic handling of output language setting when using CVC4
49 via API. Previously, the "automatic" language setting was sometimes
50 (though not always) defaulting to the internal "AST" language; it
51 should now (correctly) default to the same as the input language
52 (if the input language is supported as an output language), or the
53 "CVC4" native output language if no input language setting is applied.
54 * The SmtEngine cannot be safely copied with the copy constructor.
55 Previous versions inadvertently permitted clients to do this via the
56 API. This has been corrected, copy and assignment of the SmtEngine
57 is no longer permitted.
63 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
65 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
66 * Support in linear logics for /, div, and mod by constants (with the
67 --rewrite-divk command line option).
68 * Parsing support for TPTP's TFF and TFA formats.
69 * A new theory of strings: word (dis-)equations, length constraints,
71 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
73 * New :command-verbosity SMT option to silence success and error messages
74 on a per-command basis, and API changes to Command infrastructure to
78 * It is no longer permitted to request model or proof generation if there's
79 been an intervening push/pop.
80 * User-defined symbols (define-funs) are no longer reported in the output
81 of get-model commands.
82 * Exit codes are now more standard for UNIX command-line tools. Exit code
83 zero means no error---but the result could be sat, unsat, or unknown---and
87 * Expr::substitute() now capable of substituting operators (e.g.,
88 function symbols under an APPLY_UF)
89 * Numerous improvements to the Java language bindings
94 * Real arithmetic now has three simplex solvers for exact precision linear
95 arithmetic: the classical dual solver and two new solvers based on
96 techniques for minimizing the sum of infeasibilities. GLPK can now be used
97 as a heuristic backup to the exact precision solvers. GLPK must be enabled
98 at configure time. See --help for more information on enabling these solvers.
99 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
100 * support for theory "alternates": new ability to prototype new decision
101 procedures that are selectable at runtime
107 * bit-vector solver now has a specialized decision procedure for unsigned bit-
109 * numerous important bug fixes, performance improvements, and usability
111 * support for multiline input in interactive mode
112 * Win32-building support via mingw
113 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
114 * user patterns for quantifier instantiation are now supported in the
116 * --finite-model-find was incomplete when using --incremental, now fixed
117 * the E-matching procedure is slightly improved
118 * Boolean terms are now supported in datatypes
119 * tuple and record support have been added to the compatibility library
120 * driver verbosity change: for printing all commands as they're executed, you
121 now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
122 allows tracing the solver's activities (with -v and -vv) without having too
124 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
125 use -q. Previously, this would silence all output (including "sat" or
126 "unsat") as well. Now, single -q silences messages and warnings, and
127 double -qq silences all output (except on exception or signal).
129 -- Morgan Deters <mdeters@cs.nyu.edu> Wed, 02 Jul 2014 14:45:05 -0400