-This file contains a summary of important user-visible changes.
+This file contains a summary of important user-visible changes.
+
+Changes since 1.8
+=================
+
+New Features:
+* A new parametric theory of sequences whose syntax is compatible with the
+ syntax for sequences used by Z3.
+* Arrays: Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
+ if arrays `a` and `b` are equal on all indices within indices `i` and `j`.
+* Support for an integer operator `(_ iand n)` that returns the bitwise `and`
+ of two integers, seen as integers modulo n.
+
+Improvements:
+* New API: Added functions to retrieve the heap/nil term when using separation
+ logic.
+
+Changes:
+* SyGuS: Removed support for SyGuS-IF 1.0.
+* Removed Java and Python bindings for the legacy API
+* Interactive shell: the GPL-licensed Readline library has been replaced the
+ BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
+ of Readline. Without selecting optional GPL components, Editline-enabled CVC4
+ builds will be BSD licensed.
+* The semantics for division and remainder operators in the CVC language now
+ correspond to SMT-LIB 2.6 semantics (i.e. a division by zero or a zero
+ modulus results in a constant value, instead of an uninterpreted one).
+ Similarly, when no language is set, the API semantics now correspond to the
+ SMT-LIB 2.6 semantics.
+* The `competition` build type includes the dependencies used for SMT-COMP by
+ default. Note that this makes this build type produce GPL-licensed binaries.
+* Bit-vector operator bvxnor was previously mistakenly marked as
+ left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
+ now restrict bvxnor to only allow two operands in order to avoid confusion
+ about the semantics, since the behavior of n-ary operands to bvxnor is now
+ undefined in SMT-LIB.
+* SMT-LIB output for `get-model` command now conforms with the standard,
+ and does *not* begin with the keyword `model`. The output
+ is the same as before, only with this word removed from the beginning.
+
+
+Changes since 1.7
+=================
+
+New Features:
+* New C++ and Python API: CVC4 has a new, more streamlined API. We plan to
+ make CVC4 1.8 the last version that ships with the legacy API.
+* Strings: Full support of the new SMT-LIB standard for the theory of strings,
+ including:
+ * Support for `str.replace_re`, `str.replace_re_all`, `str.is_digit`,
+ `str.from_code`, `re.diff`, and `re.comp`
+ * Support for new operator names (e.g. `str.in_re` instead of `str.in.re`),
+ new escape sequences. The new syntax is enabled by default for smt2 files.
+* Support for syntax-guided synthesis (SyGuS) problems in the new API. C++
+ examples of the SyGuS API can be found in `./examples/api/sygus_*.cpp`.
+* Support for higher-order constraints. This includes treating function sorts
+ (constructible by `->`) as first-class sorts and handling partially applied
+ function symbols. Support for higher-order constraints can be enabled by
+ the option `--uf-ho`.
+* Support for set comprehension binders `comprehension`.
+* Eager bit-blasting: Support for SAT solver Kissat.
+
+Improvements:
+* API: Function definitions can now be requested to be global. If the `global`
+ parameter is set to true, they persist after popping the user context.
+* Java/Python bindings: The bindings now allow users to catch exceptions
+* Arithmetic: Performance improvements
+ * Linear solver: New lemmas inspired by unit-cube tests
+ * Non-linear solver: Expanded set of axioms
+* Ackermannization: The Ackermannization preprocessing pass now supports
+ uninterpreted sorts and as a result all QF_UFBV problems are supported in
+ combination with eager bit blasting.
+
+Changes:
+* CVC language: Models printed in the CVC language now include an explicit end
+ marker to facilitate the communication over pipes with CVC4.
+* API change: `SmtEngine::query()` has been renamed to
+ `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to
+ `Result::Entailment` along with corresponding changes to the enum values.
+* Java API change: The name of CVC4's package is now `edu.stanford.CVC4`
+ instead of `edu.nyu.acsys.CVC4`.
+* The default output language is changed from CVC to SMT-LIB 2.6. The
+ default output language is used when the problem language cannot be
+ easily inferred (for example when CVC4 is used from the API).
+* Printing of BV constants: previously CVC4 would print BV constant
+ values as indexed symbols by default and in binary notation with the
+ option --bv-print-consts-in-binary. To be SMT-LIB compliant the
+ default behavior is now to print BV constant values in binary
+ notation and as indexed symbols with the new option
+ --bv-print-consts-as-indexed-symbols. The option
+ --bv-print-consts-in-binary has been removed.
+* Updated to SyGuS language version 2.0 by default. This is the last release
+ that will support the SyGuS language version 1.0 (`--lang=sygus1`). A
+ script is provided to convert version 1.0 files to version 2.0, see
+ `./contrib/sygus-v1-to-v2.sh`.
+* Support for user-provided rewrite rule quantifiers have been removed.
+* Support for certain option aliases have been removed.
+* Support for parallel portfolio builds has been removed.
+
+Changes since 1.6
+=================
+
+New Features:
+* Proofs:
+ * Support for bit-vector proofs with eager bitblasting (older versions only
+ supported proofs with lazy bitblasting).
+* Strings:
+ * Support for `str.replaceall` operator.
+ * New option `--re-elim` to reduce regular expressions to extended string
+ operators, resulting in better performance on regular expression benchmarks
+ (enabled by default).
+* SyGuS:
+ * Support for abduction (`--sygus-abduct`). Given a formula, this option uses
+ CVC4's SyGuS solver to find a sufficient condition such that the
+ conjunction of the condition and the formula is unsatisfiable.
+ * Support for two new term enumerator strategies: variable agnostic
+ (`--sygus-active-gen=var-agnostic`) and fast (`--sygus-active-gen=enum`).
+ By default, CVC4 tries to choose the best term enumerator strategy
+ automatically based on the input (`--sygus-active-gen=auto`).
+ * Support for streaming solutions of increasingly smaller size when using the
+ PBE solver (`--sygus-stream --sygus-pbe`). After the first solution is found
+ and printed, the solver will continue to look for new solutions and print
+ those, if any, that are smaller than previously printed solutions.
+ * Support for unification-based techniques in non-separable specifications
+ (`--sygus-unif`). For solving invariant problems a dedicate mode
+ (`--sygus-unif-boolean-heuristic-dt`) is available that builds candidate
+ solutions using heuristic decision tree learning.
+
+Improvements:
+* Strings:
+ * Significantly better performance on string benchmarks over the core theory
+ and those with extended string functions like substring, contains, and
+ replace.
+
+Changes:
+* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
+ actual behavior.
+* Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
+* The CVC3 compatibility layer has been removed.
+* The build system now uses CMake instead of Autotools. Please refer to
+ [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md) for
+ up-to-date instructions on how to build CVC4.
+
+Changes since 1.5
+=================
+
+New Features:
+* A new theory of floating points.
+* Novel approach for solving quantified bit-vectors (BV).
+* Eager bit-blasting: Support for SAT solver CaDiCaL.
+* A new Gaussian Elimination preprocessing pass for the theory of bit-vectors.
+* Support for transcendental functions (sin, cos, exp). In SMT2 input, this
+ can be enabled by adding T to the logic (e.g., QF_NRAT).
+* Support for new operators in strings, including string inequality (str.<=)
+ and string code (str.code).
+* Support for automated rewrite rule generation from sygus (*.sy) inputs using
+ syntax-guided enumeration (option --sygus-rr).
+
+Improvements:
+* Incremental unsat core support.
+* Further development of rewrite rules for the theory of strings and regular
+ expressions.
+* Many optimizations for syntax-guided synthesis, including improved symmetry
+ breaking for enumerative search and specialized algorithms for
+ programming-by-examples conjectures.
+
+Changes:
+* Eager bit-blasting: Removed support for SAT solver CryptoMinisat 4, added
+ support for CryptoMinisat 5.
+* The LFSC proof checker now resides in its own repository on GitHub at
+ https://github.com/CVC4/LFSC. It is not distributed with CVC4 anymore.
Changes since 1.4
=================
* A new theory of sets with cardinality and relations.
* A new theory of strings.
* Support for unsat cores.
+* Support for separation logic constraints.
* Simplification mode "incremental" no longer supported.
* Support for array constants in constraints.
* Syntax for array models has changed in some language front-ends.
use -q. Previously, this would silence all output (including "sat" or
"unsat") as well. Now, single -q silences messages and warnings, and
double -qq silences all output (except on exception or signal).
-
--- Morgan Deters <mdeters@cs.nyu.edu> Wed, 02 Jul 2014 14:45:05 -0400
projects / cvc5.git / blobdiff