X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=NEWS;h=d9e1f9076de859d0863ed3d7fd0d72088a428593;hb=afc70ac962185b97e10f4e796f46c638ed1e18ab;hp=9f17bfaa4622ba19d56fa03e7b3edd6818ba4097;hpb=5186ca79710fe935d1f7ed27c4a34e913ab547e8;p=cvc5.git diff --git a/NEWS b/NEWS index 9f17bfaa4..d9e1f9076 100644 --- a/NEWS +++ b/NEWS @@ -1,10 +1,133 @@ This file contains a summary of important user-visible changes. +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 ================= -* Timed statistics are now properly updated even on process abort. +* 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. + However, this is not the best-performing version; for that, you should + configure with "--enable-gpl --best", which links against GPL'ed + libraries that improve usability and performance. For details on + licensing and dependences, see the README file. +* Small API adjustments to Datatypes to even out the API and make it + function better in Java. +* Timed statistics are now properly updated even on process abort. +* Better automatic handling of output language setting when using CVC4 + via API. Previously, the "automatic" language setting was sometimes + (though not always) defaulting to the internal "AST" language; it + should now (correctly) default to the same as the input language + (if the input language is supported as an output language), or the + "CVC4" native output language if no input language setting is applied. +* The SmtEngine cannot be safely copied with the copy constructor. + Previous versions inadvertently permitted clients to do this via the + API. This has been corrected, copy and assignment of the SmtEngine + is no longer permitted. Changes since 1.2 ================= @@ -75,5 +198,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 Thu, 05 Dec 2013 14:22:26 -0500