--- /dev/null
+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.
+++ /dev/null
-.\" 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/ .
--- /dev/null
+.\" 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/ .
projects / cvc5.git / commitdiff