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
-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
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.
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!
*** 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/
-Release Notes for CVC4 1.4, July 2014
+Release Notes for CVC4 1.5, July 2017
** Getting started
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
** 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
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
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
** 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
** 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
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.
projects / cvc5.git / commitdiff