NEWS

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