X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=NEWS;h=b25f4517ad15b9eb2991c37d556a2ddc44b2e2a7;hb=2a38d482462fdf30376c984e7a82c99d08e75f92;hp=f75febe02e418ddc46378fe3a5330558aa01fb30;hpb=7a25f18c805579770a064218385cfd7050b3f3ec;p=cvc5.git diff --git a/NEWS b/NEWS index f75febe02..b25f4517a 100644 --- a/NEWS +++ b/NEWS @@ -1,9 +1,120 @@ This file contains a summary of important user-visible changes. +Changes since 1.7 +================= + +Changes: +* Java API change: The name of CVC4's package is now `edu.stanford.CVC4` + instead of `edu.nyu.acsys.CVC4`. + +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 +================= + +* Improved heuristics for reasoning about non-linear arithmetic. +* Native support for syntax-guided synthesis (sygus). +* Support for many new heuristics for reasoning with quantifiers, including + finite model finding. +* Support for proofs for uninterpreted functions, arrays, bitvectors, and + their combinations. +* Performance improvements to existing theories. +* 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. +* New input/output languages supported: "smt2.0" and "smtlib2.0" to + force SMT-LIB v2.0; "smt2.5" and "smtlib2.5" to force SMT-LIB v2.5; + "smt2.6" and "smtlib2.6" to force SMT-LIB v2.6; + "smt", "smtlib", "smt2", and "smtlib2" all refer to the current standard + version 2.6. If an :smt-lib-version is set in the input, that overrides + the command line. +* Abstract values in SMT-LIB models are now ascribed types (with "as"). +* In SMT-LIB model output, real-sorted but integer-valued constants are + now printed in accordance with the standard (e.g. "1.0"). + Changes since 1.3 ================= +* CVC4 now supports libc++ in addition to libstdc++ (this especially + helps on Mac OS Mavericks). * The LFSC proof checker has been incorporated into CVC4 sources. +* Theory of finite sets, handling the MLSS fragment (singleton, union, + intersection, set subtraction, membership and subset). * By default, CVC4 builds in "production" mode (optimized, with fewer internal checks on). The common alternative is a "debug" build, which is much slower. By default, CVC4 builds with no GPL'ed dependences. @@ -94,5 +205,3 @@ Changes since 1.0 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 Mon, 16 Jun 2014 22:23:12 -0400