1 This file contains a summary of important user-visible changes.
8 * Support for bit-vector proofs with eager bitblasting (older versions only
9 supported proofs with lazy bitblasting).
11 * Support for `str.replaceall` operator.
12 * New option `--re-elim` to reduce regular expressions to extended string
13 operators, resulting in better performance on regular expression benchmarks
16 * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
17 CVC4's SyGuS solver to find a sufficient condition such that the
18 conjunction of the condition and the formula is unsatisfiable.
19 * Support for two new term enumerator strategies: variable agnostic
20 (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
21 By default, CVC4 tries to choose the best term enumerator strategy
22 automatically based on the input (`--sygus-active-gen=auto`).
26 * Significantly better performance on string benchmarks over the core theory
27 and those with extended string functions like substring, contains, and
31 * API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
33 * Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
34 * The CVC3 compatibility layer has been removed.
35 * The build system now uses CMake instead of Autotools. Please refer to
36 [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
37 up-to-date instructions on how to build CVC4.
43 * A new theory of floating points.
44 * Novel approach for solving quantified bit-vectors (BV).
45 * Eager bit-blasting: Support for SAT solver CaDiCaL.
46 * A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
47 * Support for transcendental functions (sin, cos, exp). In SMT2 input, this
48 can be enabled by adding T to the logic (e.g., QF_NRAT).
49 * Support for new operators in strings, including string inequality (str.<=)
50 and string code (str.code).
51 * Support for automated rewrite rule generation from sygus (*.sy) inputs using
52 syntax-guided enumeration (option --sygus-rr).
55 * Incremental unsat core support.
56 * Further development of rewrite rules for the theory of strings and regular
58 * Many optimizations for syntax-guided synthesis, including improved symmetry
59 breaking for enumerative search and specialized algorithms for
60 programming-by-examples conjectures.
63 * Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
64 support for CryptoMinisat 5.
65 * The LFSC proof checker now resides in its own repository on GitHub at
66 https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
71 * Improved heuristics for reasoning about non-linear arithmetic.
72 * Native support for syntax-guided synthesis (sygus).
73 * Support for many new heuristics for reasoning with quantifiers, including
75 * Support for proofs for uninterpreted functions, arrays, bitvectors, and
77 * Performance improvements to existing theories.
78 * A new theory of sets with cardinality and relations.
79 * A new theory of strings.
80 * Support for unsat cores.
81 * Support for separation logic constraints.
82 * Simplification mode "incremental" no longer supported.
83 * Support for array constants in constraints.
84 * Syntax for array models has changed in some language front-ends.
85 * New input/output languages supported: "smt2.0" and "smtlib2.0" to
86 force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
87 "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
88 "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
89 version 2.6. If an :smt-lib-version is set in the input, that overrides
91 * Abstract values in SMT-LIB models are now ascribed types (with "as").
92 * In SMT-LIB model output, real-sorted but integer-valued constants are
93 now printed in accordance with the standard (e.g. "1.0").
98 * CVC4 now supports libc++ in addition to libstdc++ (this especially
99 helps on Mac OS Mavericks).
100 * The LFSC proof checker has been incorporated into CVC4 sources.
101 * Theory of finite sets, handling the MLSS fragment (singleton, union,
102 intersection, set subtraction, membership and subset).
103 * By default, CVC4 builds in "production" mode (optimized, with fewer
104 internal checks on). The common alternative is a "debug" build, which
105 is much slower. By default, CVC4 builds with no GPL'ed dependences.
106 However, this is not the best-performing version; for that, you should
107 configure with "--enable-gpl --best", which links against GPL'ed
108 libraries that improve usability and performance. For details on
109 licensing and dependences, see the README file.
110 * Small API adjustments to Datatypes to even out the API and make it
111 function better in Java.
112 * Timed statistics are now properly updated even on process abort.
113 * Better automatic handling of output language setting when using CVC4
114 via API. Previously, the "automatic" language setting was sometimes
115 (though not always) defaulting to the internal "AST" language; it
116 should now (correctly) default to the same as the input language
117 (if the input language is supported as an output language), or the
118 "CVC4" native output language if no input language setting is applied.
119 * The SmtEngine cannot be safely copied with the copy constructor.
120 Previous versions inadvertently permitted clients to do this via the
121 API. This has been corrected, copy and assignment of the SmtEngine
122 is no longer permitted.
128 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
130 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
131 * Support in linear logics for /, div, and mod by constants (with the
132 --rewrite-divk command line option).
133 * Parsing support for TPTP's TFF and TFA formats.
134 * A new theory of strings: word (dis-)equations, length constraints,
136 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
138 * New :command-verbosity SMT option to silence success and error messages
139 on a per-command basis, and API changes to Command infrastructure to
143 * It is no longer permitted to request model or proof generation if there's
144 been an intervening push/pop.
145 * User-defined symbols (define-funs) are no longer reported in the output
146 of get-model commands.
147 * Exit codes are now more standard for UNIX command-line tools. Exit code
148 zero means no error---but the result could be sat, unsat, or unknown---and
152 * Expr::substitute() now capable of substituting operators (e.g.,
153 function symbols under an APPLY_UF)
154 * Numerous improvements to the Java language bindings
159 * Real arithmetic now has three simplex solvers for exact precision linear
160 arithmetic: the classical dual solver and two new solvers based on
161 techniques for minimizing the sum of infeasibilities. GLPK can now be used
162 as a heuristic backup to the exact precision solvers. GLPK must be enabled
163 at configure time. See --help for more information on enabling these solvers.
164 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
165 * support for theory "alternates": new ability to prototype new decision
166 procedures that are selectable at runtime
172 * bit-vector solver now has a specialized decision procedure for unsigned bit-
174 * numerous important bug fixes, performance improvements, and usability
176 * support for multiline input in interactive mode
177 * Win32-building support via mingw
178 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
179 * user patterns for quantifier instantiation are now supported in the
181 * --finite-model-find was incomplete when using --incremental, now fixed
182 * the E-matching procedure is slightly improved
183 * Boolean terms are now supported in datatypes
184 * tuple and record support have been added to the compatibility library
185 * driver verbosity change: for printing all commands as they're executed, you
186 now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v). This
187 allows tracing the solver's activities (with -v and -vv) without having too
189 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
190 use -q. Previously, this would silence all output (including "sat" or
191 "unsat") as well. Now, single -q silences messages and warnings, and
192 double -qq silences all output (except on exception or signal).