+++ /dev/null
-Release Notes for CVC4 1.7, April 2019
-
-** 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 "--smtlib-strict"
-(see below regarding SMT-LIB compliance).
-
-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.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.7. 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
-an integer and is used where an INT is expected, CVC4 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;
-
-This kind of problem can be identified by checking TCCs. Though CVC4 does not
-(yet) support TCCs, CVC3 can be used to produce TCCs for this input (with the
-+dump-tcc option). The TCC can then be checked by CVC4 or another solver.
-(CVC3 can also check TCCs at the same time it creates them, with +tcc.)
-
-** 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 predicate subtypes, although these are
-planned for future releases.
-
-** SMT-LIB compliance
-
-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
-"--smtlib-strict" 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) with
-the --stats command line option.
-
-** 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.
-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
-and respond 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.7 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.7 has a state-of-the-art linear arithmetic solver as well as some
-heuristic support for non-linear arithmetic.
-
-** 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 the theory of inductive
-datatypes. This limitation 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://cvc4.stanford.edu/#Technical_Support)
-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
-
- https://github.com/CVC4/CVC4/issues
-
-or send an email to cvc-bugs@cs.stanford.edu.
projects / cvc5.git / commitdiff