NEWS

   1 This file contains a summary of important user-visible changes.
   2
   3 Changes since 1.3
   4 =================
   5
   6 * Timed statistics are now properly updated even on process abort.
   7 * The LFSC proof checker has been incorporated into CVC4 sources.
   8 * By default, CVC4 builds in "production" mode (optimized, with fewer
   9   internal checks on).  The common alternative is a "debug" build, which
  10   is much slower.  CVC4 also builds with GPL dependences by default now
  11   (if those libraries are available), as this is the best-performing
  12   version of CVC4.  However, the new configure option "--bsd" disables
  13   these GPL dependences and builds the best-performing BSD-licenced version
  14   of CVC4.
  15 * Small API adjustments to Datatypes to even out the API and make it
  16   function better in Java.
  17
  18 Changes since 1.2
  19 =================
  20
  21 New features:
  22 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
  23   previously missing
  24 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
  25 * Support in linear logics for /, div, and mod by constants (with the
  26   --rewrite-divk command line option).
  27 * Parsing support for TPTP's TFF and TFA formats.
  28 * A new theory of strings: word (dis-)equations, length constraints,
  29   regular expressions.
  30 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
  31   resolved.
  32 * New :command-verbosity SMT option to silence success and error messages
  33   on a per-command basis, and API changes to Command infrastructure to
  34   support this.
  35
  36 Behavioral changes:
  37 * It is no longer permitted to request model or proof generation if there's
  38   been an intervening push/pop.
  39 * User-defined symbols (define-funs) are no longer reported in the output
  40   of get-model commands.
  41 * Exit codes are now more standard for UNIX command-line tools.  Exit code
  42   zero means no error---but the result could be sat, unsat, or unknown---and
  43   nonzero means error.
  44
  45 API changes:
  46 * Expr::substitute() now capable of substituting operators (e.g.,
  47   function symbols under an APPLY_UF)
  48 * Numerous improvements to the Java language bindings
  49
  50 Changes since 1.1
  51 =================
  52
  53 * Real arithmetic now has three simplex solvers for exact precision linear
  54   arithmetic: the classical dual solver and two new solvers based on
  55   techniques for minimizing the sum of infeasibilities. GLPK can now be used
  56   as a heuristic backup to the exact precision solvers.  GLPK must be enabled
  57   at configure time. See --help for more information on enabling these solvers.
  58 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
  59 * support for theory "alternates": new ability to prototype new decision
  60   procedures that are selectable at runtime
  61 * various bugfixes
  62
  63 Changes since 1.0
  64 =================
  65
  66 * bit-vector solver now has a specialized decision procedure for unsigned bit-
  67   vector inequalities
  68 * numerous important bug fixes, performance improvements, and usability
  69   improvements
  70 * support for multiline input in interactive mode
  71 * Win32-building support via mingw
  72 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
  73 * user patterns for quantifier instantiation are now supported in the
  74   SMT-LIBv1.2 parser
  75 * --finite-model-find was incomplete when using --incremental, now fixed
  76 * the E-matching procedure is slightly improved
  77 * Boolean terms are now supported in datatypes
  78 * tuple and record support have been added to the compatibility library
  79 * driver verbosity change: for printing all commands as they're executed, you
  80   now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
  81   allows tracing the solver's activities (with -v and -vv) without having too
  82   much output.
  83 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
  84   use -q.  Previously, this would silence all output (including "sat" or
  85   "unsat") as well.  Now, single -q silences messages and warnings, and
  86   double -qq silences all output (except on exception or signal).
  87
  88 -- Morgan Deters <mdeters@cs.nyu.edu>  Thu, 05 Dec 2013 14:22:26 -0500