draft RELEASE-NOTES file, and minor release stuff

6 files changed, 163 insertions, 12 deletions

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
index 99b0451f6..99b0451f6 100644
--- a/doc/SmtEngine.3cvc4_template.in
+++ b/doc/SmtEngine.3cvc_template.in
diff --git a/doc/options.3cvc4_template.in b/doc/options.3cvc_template.in
index 8ee39b761..8ee39b761 100644
--- a/doc/options.3cvc4_template.in
+++ b/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)))") \