diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-04-08 17:11:57 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-04-08 17:11:57 -0700 |
commit | 10c06247232c096e09363120a903abc6bc5b71ab (patch) | |
tree | ce42e757eb0f4fb67e748c36e148255c882c07c1 /RELEASE-NOTES | |
parent | 30b9f4ae91c9dba12ac0d9253d71bbd21a073e04 (diff) |
Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.
Diffstat (limited to 'RELEASE-NOTES')
-rw-r--r-- | RELEASE-NOTES | 155 |
1 files changed, 0 insertions, 155 deletions
diff --git a/RELEASE-NOTES b/RELEASE-NOTES deleted file mode 100644 index 6e8d99700..000000000 --- a/RELEASE-NOTES +++ /dev/null @@ -1,155 +0,0 @@ -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. |