From 304bdf18169ab0070ddbd6d4c9ebea8be46314b1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 29 Sep 2012 16:19:01 +0000 Subject: [PATCH] draft RELEASE-NOTES file, and minor release stuff --- Makefile.am | 17 +- RELEASE-NOTES | 150 ++++++++++++++++++ configure.ac | 4 +- ...template.in => SmtEngine.3cvc_template.in} | 0 ...4_template.in => options.3cvc_template.in} | 0 src/options/Makefile.am | 4 +- 6 files changed, 163 insertions(+), 12 deletions(-) create mode 100644 RELEASE-NOTES rename doc/{SmtEngine.3cvc4_template.in => SmtEngine.3cvc_template.in} (100%) rename doc/{options.3cvc4_template.in => options.3cvc_template.in} (100%) 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.3cvc_template.in similarity index 100% rename from doc/SmtEngine.3cvc4_template.in rename to doc/SmtEngine.3cvc_template.in diff --git a/doc/options.3cvc4_template.in b/doc/options.3cvc_template.in similarity index 100% rename from doc/options.3cvc4_template.in rename to doc/options.3cvc_template.in 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)))") \ -- 2.30.2