From: Morgan Deters Date: Sat, 29 Sep 2012 16:19:01 +0000 (+0000) Subject: draft RELEASE-NOTES file, and minor release stuff X-Git-Tag: cvc5-1.0.0~7762 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=304bdf18169ab0070ddbd6d4c9ebea8be46314b1;p=cvc5.git draft RELEASE-NOTES file, and minor release stuff --- diff --git a/Makefile.am b/Makefile.am index eb527f8cc..9f65e0a64 100644 --- a/Makefile.am +++ b/Makefile.am @@ -101,14 +101,15 @@ EXTRA_DIST = \ Makefile.builds.in \ Makefile.subdir \ library_versions \ + RELEASE-NOTES \ config/build-type \ config/mkbuilddir \ config/doxygen.cfg \ doc/cvc4.1_template.in \ doc/cvc4.5.in \ doc/libcvc4.3_template.in \ - doc/SmtEngine.3cvc4_template.in \ - doc/options.3cvc4_template.in \ + doc/SmtEngine.3cvc_template.in \ + doc/options.3cvc_template.in \ doc/libcvc4parser.3.in \ doc/libcvc4compat.3.in man_MANS = \ @@ -116,8 +117,8 @@ man_MANS = \ doc/pcvc4.1 \ doc/cvc4.5 \ doc/libcvc4.3 \ - doc/SmtEngine.3cvc4 \ - doc/options.3cvc4 \ + doc/SmtEngine.3cvc \ + doc/options.3cvc \ doc/libcvc4parser.3 \ doc/libcvc4compat.3 @@ -140,7 +141,7 @@ DISTCLEANFILES = \ doc/libcvc4.3_template \ doc/libcvc4compat.3 \ doc/libcvc4parser.3 \ - doc/SmtEngine.3cvc4 \ - doc/SmtEngine.3cvc4_template \ - doc/options.3cvc4 \ - doc/options.3cvc4_template + doc/SmtEngine.3cvc \ + doc/SmtEngine.3cvc_template \ + doc/options.3cvc \ + doc/options.3cvc_template diff --git a/RELEASE-NOTES b/RELEASE-NOTES new file mode 100644 index 000000000..243fa9215 --- /dev/null +++ b/RELEASE-NOTES @@ -0,0 +1,150 @@ +Release Notes for CVC4 1.0, October 2012 + +** Getting started + +If you run CVC4 without arguments, you will find yourself in an interactive +CVC4 session, which expects commands in CVC4's native language (the so-called +"presentation" language). To use SMT-LIB, use the "--lang smt" option on the +command line. For stricter adherence to the standard, use "--smtlib2" +(see below). + +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 +this, you can use the --lang option. + +** Type correctness + +Type Correctness Conditions (TCCs), and the checking of such, are not +supported by CVC4 1.0. Thus, a function defined only on integers can be +applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain, +but may produce strange results. For example: + + f : INT -> INT; + ASSERT f(1/3) = 0; + ASSERT f(2/3) = 1; + CHECKSAT; + % sat + COUNTEREXAMPLE; + % f : (INT) -> INT = LAMBDA(x1:INT) : 0; + +CVC3 can be used to produce TCCs for this input (with the +dump-tcc option), +and the TCC can be checked with CVC4. + +** Changes in CVC's Presentation Language + +The native language of all solvers in the CVC family, referred to as the +"presentation language," has undergone some revisions for CVC4. The +most notable is that CVC4 does _not_ add counterexample assertions to +the current assertion set after a SAT/INVALID result. For example: + + x, y : INT; + ASSERT x = 1 OR x = 2; + ASSERT y = 1 OR y = 2; + ASSERT x /= y; + CHECKSAT; + % sat + QUERY x = 1; + % invalid + QUERY x = 2; + % invalid + +Here, CVC4 responds "invalid" to the second and third queries, because +each has a counterexample (x=2 is a counterexample to the first, and +x=1 is a counterexample to the second). However, CVC3 will respond +with "valid" to one of these two, as the first query (the CHECKSAT) +had the side-effect of locking CVC3 into one of the two cases; the +later queries are effectively querying the counterexample that was +found by the first. CVC4 removes this side-effect of the CHECKSAT and +QUERY commands. + +CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not +support decimals. + +CVC4 does not have support for the IS_INTEGER predicate. + +** SMT-LIB compliance + +Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0 +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 +"--smtlib2" command-line option. Even with this setting, CVC4 is +somewhat lenient; some non-conforming input may still be parsed and +processed. + +** Getting statistics + +Statistics can be dumped on exit (both normal and abnormal exits) + +** Time and resource limits + +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. + +Time-limited runs are not deterministic; two consecutive runs with the +same time limit might produce different results (i.e., one may time out +and responds with "unknown", while the other completes and provides an +answer). To ensure that results are reproducible, use --rlimit or +--rlimit-per. These options take a "resource count" (presently, based on +the number of SAT conflicts) that limits the search time. A word of +caution, though: there is no guarantee that runs of different versions of +CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different +features enabled, or for different architectures) will interpret the resource +count in the same manner. + +CVC4 does not presently have a way to limit its memory use; you may opt +to run it from a shell after using "ulimit" to limit the size of the +heap. + +** Proof support + +CVC4 1.0 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). + +** Nonlinear arithmetic + +CVC4 1.0 has a state-of-the-art linear arithmetic solver. However, there +is extremely limited support for nonlinear arithmetic in this release. +Nontrivial nonlinear input will most likely result in an "unknown" answer +from the solver. + +** Portfolio solving + +If enabled at configure-time (./configure --with-portfolio), a second +CVC4 binary will be produced ("pcvc4"). This binary has support for +running multiple instances of CVC4 in different threads. Use --threads=N +to specify the number of threads, and use --thread0="options for thread 0" +--thread1="options for thread 1", etc., to specify a configuration for the +threads. Lemmas are *not* shared between the threads by default; to adjust +this, use the --filter-lemma-length=N option to share lemmas of N literals +(or smaller). (Some lemmas are ineligible for sharing because they include +literals that are "local" to one thread.) + +Currently, the portfolio **does not work** with quantifiers or with +the theory of inductive datatypes. These limitations 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) +and post a question there. + +** Reporting bugs and making feature requests + +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://church.cims.nyu.edu/bugs/ + +or send an email to cvc-bugs@cims.nyu.edu. diff --git a/configure.ac b/configure.ac index 40dd6df2c..e4805fd0c 100644 --- a/configure.ac +++ b/configure.ac @@ -1136,8 +1136,8 @@ CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/tls.h]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.1_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/cvc4.5]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4.3_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc4_template]) -CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc4_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/SmtEngine.3cvc_template]) +CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/options.3cvc_template]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4parser.3]) CVC4_CONFIG_FILE_ONLY_IF_CHANGED([doc/libcvc4compat.3]) diff --git a/doc/SmtEngine.3cvc4_template.in b/doc/SmtEngine.3cvc4_template.in deleted file mode 100644 index 99b0451f6..000000000 --- a/doc/SmtEngine.3cvc4_template.in +++ /dev/null @@ -1,51 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii SmtEngine.3cvc4 -.\" -.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" -.SH NAME -SmtEngine \- the primary interface to CVC4's theorem-proving capabilities -.SH DESCRIPTION -.B SmtEngine -is the main entry point into the CVC4 theorem prover API. - -.SH SMTENGINE OPTIONS - -The SmtEngine is in charge of setting and getting information and options. -Numerous options are available via the -.I SmtEngine::setOption() -call. -.I SmtEngine::setOption() -and -.I SmtEngine::getOption() -use the following option keys. - -.RS -.TP 10 -.I "COMMON OPTIONS" -${common_manpage_smt_documentation} - -${remaining_manpage_smt_documentation} -.PD -.RE - -.SH VERSION -This manual page refers to -.B CVC4 -version @VERSION@. -.SH BUGS -A Bugzilla for the CVC4 project is maintained at -.BR http://church.cims.nyu.edu/bugzilla3/ . -.SH AUTHORS -.B CVC4 -is developed by a team of researchers at New York University -and the University of Iowa. -See the AUTHORS file in the distribution for a full list of -contributors. -.SH "SEE ALSO" -.BR libcvc4 (3), -.BR libcvc4parser (3), -.BR libcvc4compat (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/SmtEngine.3cvc_template.in b/doc/SmtEngine.3cvc_template.in new file mode 100644 index 000000000..99b0451f6 --- /dev/null +++ b/doc/SmtEngine.3cvc_template.in @@ -0,0 +1,51 @@ +.\" Process this file with +.\" groff -man -Tascii SmtEngine.3cvc4 +.\" +.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces" +.SH NAME +SmtEngine \- the primary interface to CVC4's theorem-proving capabilities +.SH DESCRIPTION +.B SmtEngine +is the main entry point into the CVC4 theorem prover API. + +.SH SMTENGINE OPTIONS + +The SmtEngine is in charge of setting and getting information and options. +Numerous options are available via the +.I SmtEngine::setOption() +call. +.I SmtEngine::setOption() +and +.I SmtEngine::getOption() +use the following option keys. + +.RS +.TP 10 +.I "COMMON OPTIONS" +${common_manpage_smt_documentation} + +${remaining_manpage_smt_documentation} +.PD +.RE + +.SH VERSION +This manual page refers to +.B CVC4 +version @VERSION@. +.SH BUGS +A Bugzilla for the CVC4 project is maintained at +.BR http://church.cims.nyu.edu/bugzilla3/ . +.SH AUTHORS +.B CVC4 +is developed by a team of researchers at New York University +and the University of Iowa. +See the AUTHORS file in the distribution for a full list of +contributors. +.SH "SEE ALSO" +.BR libcvc4 (3), +.BR libcvc4parser (3), +.BR libcvc4compat (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/options.3cvc4_template.in b/doc/options.3cvc4_template.in deleted file mode 100644 index 8ee39b761..000000000 --- a/doc/options.3cvc4_template.in +++ /dev/null @@ -1,39 +0,0 @@ -.\" Process this file with -.\" groff -man -Tascii options.3cvc4 -.\" -.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation" -.SH NAME -options \- the options infrastructure - -.SH AVAILABLE INTERNAL OPTIONS - -.RS -.TP 10 -.I "COMMON OPTIONS" -${common_manpage_internals_documentation} - -${remaining_manpage_internals_documentation} -.PD -.RE - -.SH VERSION -This manual page refers to -.B CVC4 -version @VERSION@. -.SH BUGS -A Bugzilla for the CVC4 project is maintained at -.BR http://church.cims.nyu.edu/bugzilla3/ . -.SH AUTHORS -.B CVC4 -is developed by a team of researchers at New York University -and the University of Iowa. -See the AUTHORS file in the distribution for a full list of -contributors. -.SH "SEE ALSO" -.BR libcvc4 (3), -.BR libcvc4parser (3), -.BR libcvc4compat (3) - -Additionally, the CVC4 wiki contains useful information about the -design and internals of CVC4. It is maintained at -.BR http://church.cims.nyu.edu/wiki/ . diff --git a/doc/options.3cvc_template.in b/doc/options.3cvc_template.in new file mode 100644 index 000000000..8ee39b761 --- /dev/null +++ b/doc/options.3cvc_template.in @@ -0,0 +1,39 @@ +.\" Process this file with +.\" groff -man -Tascii options.3cvc4 +.\" +.TH OPTIONS 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Internals Documentation" +.SH NAME +options \- the options infrastructure + +.SH AVAILABLE INTERNAL OPTIONS + +.RS +.TP 10 +.I "COMMON OPTIONS" +${common_manpage_internals_documentation} + +${remaining_manpage_internals_documentation} +.PD +.RE + +.SH VERSION +This manual page refers to +.B CVC4 +version @VERSION@. +.SH BUGS +A Bugzilla for the CVC4 project is maintained at +.BR http://church.cims.nyu.edu/bugzilla3/ . +.SH AUTHORS +.B CVC4 +is developed by a team of researchers at New York University +and the University of Iowa. +See the AUTHORS file in the distribution for a full list of +contributors. +.SH "SEE ALSO" +.BR libcvc4 (3), +.BR libcvc4parser (3), +.BR libcvc4compat (3) + +Additionally, the CVC4 wiki contains useful information about the +design and internals of CVC4. It is maintained at +.BR http://church.cims.nyu.edu/wiki/ . diff --git a/src/options/Makefile.am b/src/options/Makefile.am index d4d5b2861..155c1b249 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -177,8 +177,8 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options @srcdir@/../smt/smt_options_template.cpp @builddir@/../smt/smt_options.cpp \ @top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \ @top_builddir@/doc/libcvc4.3_template @top_builddir@/doc/libcvc4.3 \ - @top_builddir@/doc/SmtEngine.3cvc4_template @top_builddir@/doc/SmtEngine.3cvc4 \ - @top_builddir@/doc/options.3cvc4_template @top_builddir@/doc/options.3cvc4 \ + @top_builddir@/doc/SmtEngine.3cvc_template @top_builddir@/doc/SmtEngine.3cvc \ + @top_builddir@/doc/options.3cvc_template @top_builddir@/doc/options.3cvc \ -t \ @srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \ $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(patsubst %/,%,$(dir $(o)))") \