NEWS

   1 This file contains a summary of important user-visible changes.
   2
   3 Changes since 1.2
   4 =================
   5
   6 * SMT-LIB support for abs, to_real, to_int, is_int
   7 * Expr::substitute() now capable of substituting operators (e.g.,
   8   function symbols under an APPLY_UF)
   9 * Support in linear logics for /, div, and mod by constants.
  10 * Support for TPTP's TFF and TFA formats.
  11 * We no longer permit model or proof generation if there's been an
  12   intervening push/pop.
  13 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
  14   resolved.
  15
  16 Changes since 1.1
  17 =================
  18
  19 * Real arithmetic now has three simplex solvers for exact precision linear
  20   arithmetic: the classical dual solver and two new solvers based on
  21   techniques for minimizing the sum of infeasibilities. GLPK can now be used
  22   as a heuristic backup to the exact precision solvers.  GLPK must be enabled
  23   at configure time. See --help for more information on enabling these solvers.
  24 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
  25 * support for theory "alternates": new ability to prototype new decision
  26   procedures that are selectable at runtime
  27 * various bugfixes
  28
  29 Changes since 1.0
  30 =================
  31
  32 * bit-vector solver now has a specialized decision procedure for unsigned bit-
  33   vector inequalities
  34 * numerous important bug fixes, performance improvements, and usability
  35   improvements
  36 * support for multiline input in interactive mode
  37 * Win32-building support via mingw
  38 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
  39 * user patterns for quantifier instantiation are now supported in the
  40   SMT-LIBv1.2 parser
  41 * --finite-model-find was incomplete when using --incremental, now fixed
  42 * the E-matching procedure is slightly improved
  43 * Boolean terms are now supported in datatypes
  44 * tuple and record support have been added to the compatibility library
  45 * driver verbosity change: for printing all commands as they're executed, you
  46   now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
  47   allows tracing the solver's activities (with -v and -vv) without having too
  48   much output.
  49 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
  50   use -q.  Previously, this would silence all output (including "sat" or
  51   "unsat") as well.  Now, single -q silences messages and warnings, and
  52   double -qq silences all output (except on exception or signal).
  53
  54 -- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 03 Apr 2013 13:06:35 -0400