diff options
| -rw-r--r-- | NEWS | 16 | ||||
| -rw-r--r-- | README | 33 | ||||
| -rw-r--r-- | RELEASE-NOTES | 36 |
3 files changed, 45 insertions, 40 deletions
@@ -3,14 +3,24 @@ This file contains a summary of important user-visible changes. 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. * Simplification mode "incremental" no longer supported. * Support for array constants in constraints. -* Syntax for array models have changed in some language front-ends. +* 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. + 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.0. If an :smt-lib-version is set in the input, that overrides + 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 @@ -1,12 +1,9 @@ -This is CVC4 release version 1.4. For build and installation notes, +This is CVC4 release version 1.5. For build and installation notes, please see the INSTALL file included with this distribution. -This first official release of CVC4 is the result of more than three -years of efforts by researchers at New York University and The -University of Iowa. The project leaders are Clark Barrett (New York -University) and Cesare Tinelli (The University of Iowa). For a full -list of authors, please refer to the AUTHORS file in the source -distribution. +The project leaders are Clark Barrett (Stanford University) and Cesare Tinelli +(The University of Iowa). For a full list of authors, please refer to the +AUTHORS file in the source distribution. CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such @@ -28,7 +25,7 @@ distribution. We recommend that you visit our CVC4 tutorials online at: - http://cvc4.cs.nyu.edu/wiki/Tutorials + http://cvc4.cs.stanford.edu/wiki/Tutorials for help getting started using CVC4. @@ -36,24 +33,24 @@ for help getting started using CVC4. We are always happy to hear feedback from our users: -* if you need help with using CVC4, please write to the - cvc-users@cs.nyu.edu mailing list. +* if you need help with using CVC4, please refer to + http://cvc4.stanford.edu/#Technical_Support. * if you need to report a bug with CVC4, or make a feature request, - please visit our bugtracker at http://cvc4.cs.nyu.edu/bugs/ or write - to the cvc-bugs@cs.nyu.edu mailing list. We are very grateful for + please visit our bugtracker at http://cvc4.cs.stanford.edu/bugs/ or write + to the cvc-bugs@cs.stanford.edu mailing list. We are very grateful for bug reports, as they help us improve CVC4, and patches are generally reviewed and accepted quickly. * if you are using CVC4 in your work, or incorporating it into software of your own, we'd like to invite you to leave a description and link to your project/software on our "Third Party Applications" - page at http://cvc4.cs.nyu.edu/wiki/Public:Third_Party_Applications + page at http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications -* if you are interested in contributing code (for example, a new - decision procedure implementation) to the CVC4 project, please - contact us at cvc4-devel@cs.nyu.edu. We'd be happy to point you to - some internals documentation to help you out. +* if you are interested in contributing code (for example, a new decision + procedure implementation) to the CVC4 project, please contact one of the + project leaders. We'd be happy to point you to some internals documentation + to help you out. Thank you for using CVC4! @@ -100,4 +97,4 @@ in short order. *** For more information -More information about CVC4 is available at: http://cvc4.cs.nyu.edu/ +More information about CVC4 is available at: http://cvc4.cs.stanford.edu/ diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 2d6eaeab1..2534903d9 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,4 +1,4 @@ -Release Notes for CVC4 1.4, July 2014 +Release Notes for CVC4 1.5, July 2017 ** Getting started @@ -10,14 +10,14 @@ command line. For stricter adherence to the standard, use "--smtlib-strict" When a filename is given on the command line, the file's extension determines the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2 -is SMT-LIB 2.0, and file.cvc is the presentation language). To override +is SMT-LIB 2.6, and file.cvc is the presentation language). To override this, you can use the --lang option. ** Type correctness The CVC family of systems relies on Type Correctness Conditions (TCCs) when mixing two types that have a compatible base type. TCCs, and the checking of -such, are not supported by CVC4 1.4. This is an issue when mixing integers and +such, are not supported by CVC4 1.5. This is an issue when mixing integers and reals. A function defined only on integers can be applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain. It is up to the user to ensure that the REAL expression must be an integer. If the REAL expression is not @@ -74,7 +74,7 @@ planned for future releases. ** SMT-LIB compliance -Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0 +Every effort has been made to make CVC4 compliant with the SMT-LIB 2.6 standard (http://smtlib.org/). However, when parsing SMT-LIB input, certain default settings don't match what is stated in the official standard. To make CVC4 adhere more strictly to the standard, use the @@ -84,7 +84,7 @@ processed. For the latest news on SMT-LIB compliance, please check: - http://cvc4.cs.nyu.edu/wiki/SMT-LIB_Compliance + http://cvc4.cs.stanford.edu/wiki/SMT-LIB_Compliance ** Getting statistics @@ -96,10 +96,9 @@ the --stats command line option. CVC4 can be made to self-timeout after a given number of milliseconds. Use the --tlimit command line option to limit the entire run of CVC4, or use --tlimit-per to limit each individual query separately. -Preprocessing time is not counted by the time limit, so for some large -inputs which require aggressive preprocessing, you may notice that ---tlimit does not work very well. If you suspect this might be the -case, you can use "-vv" (double verbosity) to see what CVC4 is doing. +Occasionally, you may encounter a problem for which --tlimit does not work very +well. If you suspect this might be the case, please report it as a bug. You +can also use "-vv" (double verbosity) to see what CVC4 is doing. Time-limited runs are not deterministic; two consecutive runs with the same time limit might produce different results (i.e., one may time out @@ -118,16 +117,15 @@ heap. ** Proof support -CVC4 1.4 has limited support for proofs, and they are disabled by default. -(Run the configure script with --enable-proof to enable proofs). Proofs -are exported in LFSC format and are limited to the propositional backbone -of the discovered proof (theory lemmas are stated without proof in this -release). +CVC4 1.5 has support for proofs when using uninterpreted functions, arrays, +bitvectors, or their combinations, and proofs are enabled by default. +(Run the configure script with --disable-proof to disable proofs). Proofs +are exported in LFSC format. ** Nonlinear arithmetic -CVC4 1.4 has a state-of-the-art linear arithmetic solver. However, there -is extremely limited support for nonlinear arithmetic in this release. +CVC4 1.5 has a state-of-the-art linear arithmetic solver as well as some +heuristic support for non-linear arithmetic. ** Portfolio solving @@ -147,7 +145,7 @@ datatypes. This limitation will be addressed in a future release. ** Questions ?? CVC4 and its predecessors have an active user base. You might want to -subscribe to the mailing list (http://cs.nyu.edu/mailman/listinfo/cvc-users) +subscribe to the mailing list (http://cvc4.stanford.edu/#Technical_Support) and post a question there. ** Reporting bugs and making feature requests @@ -156,6 +154,6 @@ CVC4 is under active development. Should you find a bug in CVC4's documentation, behavior, API, or SMT-LIB compliance, or if you have a feature request, please let us know on our bugtracker at - http://cvc4.cs.nyu.edu/bugs/ + http://cvc4.cs.stanford.edu/bugs/ -or send an email to cvc-bugs@cims.nyu.edu. +or send an email to cvc-bugs@cs.stanford.edu. |