NEWS

   1 This file contains a summary of important user-visible changes.
   2
   3 Changes since 1.8
   4 =================
   5
   6 New Features:
   7 * A new parametric theory of sequences whose syntax is compatible with the
   8   syntax for sequences used by Z3.
   9 * Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
  10   if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
  11 * Support for an integer operator `(_ iand n)` that returns the bitwise `and`
  12   of two integers, seen as integers modulo n.
  13
  14 Improvements:
  15 * New API: Added functions to retrieve the heap/nil term when using separation
  16   logic.
  17
  18 Changes:
  19 * SyGuS: Removed support for SyGuS-IF 1.0.
  20 * Removed Java and Python bindings for the legacy API
  21 * Interactive shell: the GPL-licensed Readline library has been replaced the
  22   BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
  23   of Readline. Without selecting optional GPL components, Editline-enabled CVC4
  24   builds will be BSD licensed.
  25
  26 Changes since 1.7
  27 =================
  28
  29 New Features:
  30 * New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
  31   make CVC4 1.8 the last version that ships with the legacy API.
  32 * Strings: Full support of the new SMT-LIB standard for the theory of strings,
  33   including:
  34   * Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`,
  35     `str.from_code`, `re.diff`, and `re.comp`
  36   * Support for new operator names (e.g. `str.in_re` instead of `str.in.re`),
  37     new escape sequences. The new syntax is enabled by default for smt2 files.
  38 * Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
  39   examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`.
  40 * Support for higher-order constraints. This includes treating function sorts
  41   (constructible by `->`) as first-class sorts and handling partially applied
  42   function symbols. Support for higher-order constraints can be enabled by
  43   the option `--uf-ho`.
  44 * Support for set comprehension binders `comprehension`.
  45 * Eager bit-blasting: Support for SAT solver Kissat.
  46
  47 Improvements:
  48 * API: Function definitions can now be requested to be global. If the `global`
  49   parameter is set to true, they persist after popping the user context.
  50 * Java/Python bindings: The bindings now allow users to catch exceptions
  51 * Arithmetic: Performance improvements
  52   * Linear solver: New lemmas inspired by unit-cube tests
  53   * Non-linear solver: Expanded set of axioms
  54 * Ackermannization: The Ackermannization preprocessing pass now supports
  55   uninterpreted sorts and as a result all QF_UFBV problems are supported in
  56   combination with eager bit blasting.
  57
  58 Changes:
  59 * CVC language: Models printed in the CVC language now include an explicit end
  60   marker to facilitate the communication over pipes with CVC4.
  61 * API change: `SmtEngine::query()` has been renamed to
  62   `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
  63   `Result::Entailment` along with corresponding changes to the enum values.
  64 * Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
  65   instead of `edu.nyu.acsys.CVC4`.
  66 * The default output language is changed from CVC to SMT-LIB 2.6. The
  67   default output language is used when the problem language cannot be
  68   easily inferred (for example when CVC4 is used from the API).
  69 * Printing of BV constants: previously CVC4 would print BV constant
  70   values as indexed symbols by default and in binary notation with the
  71   option --bv-print-consts-in-binary. To be SMT-LIB compliant the
  72   default behavior is now to print BV constant values in binary
  73   notation and as indexed symbols with the new option
  74   --bv-print-consts-as-indexed-symbols. The option
  75   --bv-print-consts-in-binary has been removed.
  76 * Updated to SyGuS language version 2.0 by default. This is the last release
  77   that will support the SyGuS language version 1.0 (`--lang=sygus1`). A
  78   script is provided to convert version 1.0 files to version 2.0, see
  79   `./contrib/sygus-v1-to-v2.sh`.
  80 * Support for user-provided rewrite rule quantifiers have been removed.
  81 * Support for certain option aliases have been removed.
  82 * Support for parallel portfolio builds has been removed.
  83
  84 Changes since 1.6
  85 =================
  86
  87 New Features:
  88 * Proofs:
  89   * Support for bit-vector proofs with eager bitblasting (older versions only
  90     supported proofs with lazy bitblasting).
  91 * Strings:
  92   * Support for `str.replaceall` operator.
  93   * New option `--re-elim` to reduce regular expressions to extended string
  94     operators, resulting in better performance on regular expression benchmarks
  95     (enabled by default).
  96 * SyGuS:
  97   * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
  98     CVC4's SyGuS solver to find a sufficient condition such that the
  99     conjunction of the condition and the formula is unsatisfiable.
 100   * Support for two new term enumerator strategies: variable agnostic
 101     (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
 102     By default, CVC4 tries to choose the best term enumerator strategy
 103     automatically based on the input (`--sygus-active-gen=auto`).
 104   * Support for streaming solutions of increasingly smaller size when using the
 105     PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
 106     and printed, the solver will continue to look for new solutions and print
 107     those, if any, that are smaller than previously printed solutions.
 108   * Support for unification-based techniques in non-separable specifications
 109     (`--sygus-unif`). For solving invariant problems a dedicate mode
 110     (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
 111     solutions using heuristic decision tree learning.
 112
 113 Improvements:
 114 * Strings:
 115   * Significantly better performance on string benchmarks over the core theory
 116     and those with extended string functions like substring, contains, and
 117     replace.
 118
 119 Changes:
 120 * API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
 121               actual behavior.
 122 * Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
 123 * The CVC3 compatibility layer has been removed.
 124 * The build system now uses CMake instead of Autotools. Please refer to
 125   [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
 126   up-to-date instructions on how to build CVC4.
 127
 128 Changes since 1.5
 129 =================
 130
 131 New Features:
 132 * A new theory of floating points.
 133 * Novel approach for solving quantified bit-vectors (BV).
 134 * Eager bit-blasting: Support for SAT solver CaDiCaL.
 135 * A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
 136 * Support for transcendental functions (sin, cos, exp). In SMT2 input, this
 137   can be enabled by adding T to the logic (e.g., QF_NRAT).
 138 * Support for new operators in strings, including string inequality (str.<=)
 139   and string code (str.code).
 140 * Support for automated rewrite rule generation from sygus (*.sy) inputs using
 141   syntax-guided enumeration (option --sygus-rr).
 142
 143 Improvements:
 144 * Incremental unsat core support.
 145 * Further development of rewrite rules for the theory of strings and regular
 146   expressions.
 147 * Many optimizations for syntax-guided synthesis, including improved symmetry
 148   breaking for enumerative search and specialized algorithms for
 149   programming-by-examples conjectures.
 150
 151 Changes:
 152 * Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
 153   support for CryptoMinisat 5.
 154 * The LFSC proof checker now resides in its own repository on GitHub at
 155   https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
 156
 157 Changes since 1.4
 158 =================
 159
 160 * Improved heuristics for reasoning about non-linear arithmetic.
 161 * Native support for syntax-guided synthesis (sygus).
 162 * Support for many new heuristics for reasoning with quantifiers, including
 163   finite model finding.
 164 * Support for proofs for uninterpreted functions, arrays, bitvectors, and
 165   their combinations.
 166 * Performance improvements to existing theories.
 167 * A new theory of sets with cardinality and relations.
 168 * A new theory of strings.
 169 * Support for unsat cores.
 170 * Support for separation logic constraints.
 171 * Simplification mode "incremental" no longer supported.
 172 * Support for array constants in constraints.
 173 * Syntax for array models has changed in some language front-ends.
 174 * New input/output languages supported: "smt2.0" and "smtlib2.0" to
 175   force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5;
 176   "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6;
 177   "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard
 178   version 2.6.  If an :smt-lib-version is set in the input, that overrides
 179   the command line.
 180 * Abstract values in SMT-LIB models are now ascribed types (with "as").
 181 * In SMT-LIB model output, real-sorted but integer-valued constants are
 182   now printed in accordance with the standard (e.g. "1.0").
 183
 184 Changes since 1.3
 185 =================
 186
 187 * CVC4 now supports libc++ in addition to libstdc++ (this especially
 188   helps on Mac OS Mavericks).
 189 * The LFSC proof checker has been incorporated into CVC4 sources.
 190 * Theory of finite sets, handling the MLSS fragment (singleton, union,
 191   intersection, set subtraction, membership and subset).
 192 * By default, CVC4 builds in "production" mode (optimized, with fewer
 193   internal checks on).  The common alternative is a "debug" build, which
 194   is much slower.  By default, CVC4 builds with no GPL'ed dependences.
 195   However, this is not the best-performing version; for that, you should
 196   configure with "--enable-gpl --best", which links against GPL'ed
 197   libraries that improve usability and performance.  For details on
 198   licensing and dependences, see the README file.
 199 * Small API adjustments to Datatypes to even out the API and make it
 200   function better in Java.
 201 * Timed statistics are now properly updated even on process abort.
 202 * Better automatic handling of output language setting when using CVC4
 203   via API.  Previously, the "automatic" language setting was sometimes
 204   (though not always) defaulting to the internal "AST" language; it
 205   should now (correctly) default to the same as the input language
 206   (if the input language is supported as an output language), or the
 207   "CVC4" native output language if no input language setting is applied.
 208 * The SmtEngine cannot be safely copied with the copy constructor.
 209   Previous versions inadvertently permitted clients to do this via the
 210   API.  This has been corrected, copy and assignment of the SmtEngine
 211   is no longer permitted.
 212
 213 Changes since 1.2
 214 =================
 215
 216 New features:
 217 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
 218   previously missing
 219 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
 220 * Support in linear logics for /, div, and mod by constants (with the
 221   --rewrite-divk command line option).
 222 * Parsing support for TPTP's TFF and TFA formats.
 223 * A new theory of strings: word (dis-)equations, length constraints,
 224   regular expressions.
 225 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
 226   resolved.
 227 * New :command-verbosity SMT option to silence success and error messages
 228   on a per-command basis, and API changes to Command infrastructure to
 229   support this.
 230
 231 Behavioral changes:
 232 * It is no longer permitted to request model or proof generation if there's
 233   been an intervening push/pop.
 234 * User-defined symbols (define-funs) are no longer reported in the output
 235   of get-model commands.
 236 * Exit codes are now more standard for UNIX command-line tools.  Exit code
 237   zero means no error---but the result could be sat, unsat, or unknown---and
 238   nonzero means error.
 239
 240 API changes:
 241 * Expr::substitute() now capable of substituting operators (e.g.,
 242   function symbols under an APPLY_UF)
 243 * Numerous improvements to the Java language bindings
 244
 245 Changes since 1.1
 246 =================
 247
 248 * Real arithmetic now has three simplex solvers for exact precision linear
 249   arithmetic: the classical dual solver and two new solvers based on
 250   techniques for minimizing the sum of infeasibilities. GLPK can now be used
 251   as a heuristic backup to the exact precision solvers.  GLPK must be enabled
 252   at configure time. See --help for more information on enabling these solvers.
 253 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
 254 * support for theory "alternates": new ability to prototype new decision
 255   procedures that are selectable at runtime
 256 * various bugfixes
 257
 258 Changes since 1.0
 259 =================
 260
 261 * bit-vector solver now has a specialized decision procedure for unsigned bit-
 262   vector inequalities
 263 * numerous important bug fixes, performance improvements, and usability
 264   improvements
 265 * support for multiline input in interactive mode
 266 * Win32-building support via mingw
 267 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
 268 * user patterns for quantifier instantiation are now supported in the
 269   SMT-LIBv1.2 parser
 270 * --finite-model-find was incomplete when using --incremental, now fixed
 271 * the E-matching procedure is slightly improved
 272 * Boolean terms are now supported in datatypes
 273 * tuple and record support have been added to the compatibility library
 274 * driver verbosity change: for printing all commands as they're executed, you
 275   now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
 276   allows tracing the solver's activities (with -v and -vv) without having too
 277   much output.
 278 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
 279   use -q.  Previously, this would silence all output (including "sat" or
 280   "unsat") as well.  Now, single -q silences messages and warnings, and
 281   double -qq silences all output (except on exception or signal).