NEWS

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