NEWS

   1 This file contains a summary of important user-visible changes.
   2
   3 Changes since 1.4
   4 =================
   5
   6 * Support for unsat cores.
   7 * Simplification mode "incremental" no longer supported.
   8 * Support for array constants in constraints.
   9 * Syntax for array models have changed in some language front-ends.
  10 * In SMT-LIB model output, real-sorted but integer-valued constants are
  11   now printed in accordance with the standard (e.g. "1.0").
  12
  13 Changes since 1.3
  14 =================
  15
  16 * CVC4 now supports libc++ in addition to libstdc++ (this especially
  17   helps on Mac OS Mavericks).
  18 * The LFSC proof checker has been incorporated into CVC4 sources.
  19 * Theory of finite sets, handling the MLSS fragment (singleton, union,
  20   intersection, set subtraction, membership and subset).
  21 * By default, CVC4 builds in "production" mode (optimized, with fewer
  22   internal checks on).  The common alternative is a "debug" build, which
  23   is much slower.  By default, CVC4 builds with no GPL'ed dependences.
  24   However, this is not the best-performing version; for that, you should
  25   configure with "--enable-gpl --best", which links against GPL'ed
  26   libraries that improve usability and performance.  For details on
  27   licensing and dependences, see the README file.
  28 * Small API adjustments to Datatypes to even out the API and make it
  29   function better in Java.
  30 * Timed statistics are now properly updated even on process abort.
  31 * Better automatic handling of output language setting when using CVC4
  32   via API.  Previously, the "automatic" language setting was sometimes
  33   (though not always) defaulting to the internal "AST" language; it
  34   should now (correctly) default to the same as the input language
  35   (if the input language is supported as an output language), or the
  36   "CVC4" native output language if no input language setting is applied.
  37 * The SmtEngine cannot be safely copied with the copy constructor.
  38   Previous versions inadvertently permitted clients to do this via the
  39   API.  This has been corrected, copy and assignment of the SmtEngine
  40   is no longer permitted.
  41
  42 Changes since 1.2
  43 =================
  44
  45 New features:
  46 * SMT-LIB-compliant support for abs, to_real, to_int, is_int, which were
  47   previously missing
  48 * New bv2nat/int2bv operators for bitvector/integer inter-compatibility.
  49 * Support in linear logics for /, div, and mod by constants (with the
  50   --rewrite-divk command line option).
  51 * Parsing support for TPTP's TFF and TFA formats.
  52 * A new theory of strings: word (dis-)equations, length constraints,
  53   regular expressions.
  54 * Increased compliance to SMT-LIBv2, numerous bugs and usability issues
  55   resolved.
  56 * New :command-verbosity SMT option to silence success and error messages
  57   on a per-command basis, and API changes to Command infrastructure to
  58   support this.
  59
  60 Behavioral changes:
  61 * It is no longer permitted to request model or proof generation if there's
  62   been an intervening push/pop.
  63 * User-defined symbols (define-funs) are no longer reported in the output
  64   of get-model commands.
  65 * Exit codes are now more standard for UNIX command-line tools.  Exit code
  66   zero means no error---but the result could be sat, unsat, or unknown---and
  67   nonzero means error.
  68
  69 API changes:
  70 * Expr::substitute() now capable of substituting operators (e.g.,
  71   function symbols under an APPLY_UF)
  72 * Numerous improvements to the Java language bindings
  73
  74 Changes since 1.1
  75 =================
  76
  77 * Real arithmetic now has three simplex solvers for exact precision linear
  78   arithmetic: the classical dual solver and two new solvers based on
  79   techniques for minimizing the sum of infeasibilities. GLPK can now be used
  80   as a heuristic backup to the exact precision solvers.  GLPK must be enabled
  81   at configure time. See --help for more information on enabling these solvers.
  82 * added support for "bit0" and "bit1" bitvector constants in SMT-LIB v1.2
  83 * support for theory "alternates": new ability to prototype new decision
  84   procedures that are selectable at runtime
  85 * various bugfixes
  86
  87 Changes since 1.0
  88 =================
  89
  90 * bit-vector solver now has a specialized decision procedure for unsigned bit-
  91   vector inequalities
  92 * numerous important bug fixes, performance improvements, and usability
  93   improvements
  94 * support for multiline input in interactive mode
  95 * Win32-building support via mingw
  96 * SMT-LIB get-model output now is easier to machine-parse: contains (model...)
  97 * user patterns for quantifier instantiation are now supported in the
  98   SMT-LIBv1.2 parser
  99 * --finite-model-find was incomplete when using --incremental, now fixed
 100 * the E-matching procedure is slightly improved
 101 * Boolean terms are now supported in datatypes
 102 * tuple and record support have been added to the compatibility library
 103 * driver verbosity change: for printing all commands as they're executed, you
 104   now need verbosity level >= 3 (e.g., -vvv) instead of level 1 (-v).  This
 105   allows tracing the solver's activities (with -v and -vv) without having too
 106   much output.
 107 * to make CVC4 quieter in abnormal (e.g., "warning" conditions), you can
 108   use -q.  Previously, this would silence all output (including "sat" or
 109   "unsat") as well.  Now, single -q silences messages and warnings, and
 110   double -qq silences all output (except on exception or signal).
 111
 112 -- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 02 Jul 2014 14:45:05 -0400