RELEASE-NOTES

   1 Release Notes for CVC4 1.5, July 2017
   2
   3 ** Getting started
   4
   5 If you run CVC4 without arguments, you will find yourself in an interactive
   6 CVC4 session, which expects commands in CVC4's native language (the so-called
   7 "presentation" language).  To use SMT-LIB, use the "--lang smt" option on the
   8 command line.  For stricter adherence to the standard, use "--smtlib-strict"
   9 (see below regarding SMT-LIB compliance).
  10
  11 When a filename is given on the command line, the file's extension determines
  12 the language parser that's used (e.g., file.smt is SMT-LIB 1.2, file.smt2
  13 is SMT-LIB 2.6, and file.cvc is the presentation language).  To override
  14 this, you can use the --lang option.
  15
  16 ** Type correctness
  17
  18 The CVC family of systems relies on Type Correctness Conditions (TCCs) when
  19 mixing two types that have a compatible base type.  TCCs, and the checking of
  20 such, are not supported by CVC4 1.5.  This is an issue when mixing integers and
  21 reals.  A function defined only on integers can be applied to REAL (as INT is a
  22 subtype of REAL), and CVC4 will not complain.  It is up to the user to ensure
  23 that the REAL expression must be an integer.  If the REAL expression is not
  24 an integer and is used where an INT is expected, CVC4 may produce strange
  25 results.
  26
  27 For example:
  28
  29   f : INT -> INT;
  30   ASSERT f(1/3) = 0;
  31   ASSERT f(2/3) = 1;
  32   CHECKSAT;
  33   % sat
  34   COUNTEREXAMPLE;
  35   % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
  36
  37 This kind of problem can be identified by checking TCCs.  Though CVC4 does not
  38 (yet) support TCCs, CVC3 can be used to produce TCCs for this input (with the
  39 +dump-tcc option). The TCC can then be checked by CVC4 or another solver.
  40 (CVC3 can also check TCCs at the same time it creates them, with +tcc.)
  41
  42 ** Changes in CVC's Presentation Language
  43
  44 The native language of all solvers in the CVC family, referred to as the
  45 "presentation language," has undergone some revisions for CVC4.  The
  46 most notable is that CVC4 does _not_ add counterexample assertions to
  47 the current assertion set after a SAT/INVALID result.  For example:
  48
  49   x, y : INT;
  50   ASSERT x = 1 OR x = 2;
  51   ASSERT y = 1 OR y = 2;
  52   ASSERT x /= y;
  53   CHECKSAT;
  54   % sat
  55   QUERY x = 1;
  56   % invalid
  57   QUERY x = 2;
  58   % invalid
  59
  60 Here, CVC4 responds "invalid" to the second and third queries, because
  61 each has a counterexample (x=2 is a counterexample to the first, and
  62 x=1 is a counterexample to the second).  However, CVC3 will respond
  63 with "valid" to one of these two, as the first query (the CHECKSAT)
  64 had the side-effect of locking CVC3 into one of the two cases; the
  65 later queries are effectively querying the counterexample that was
  66 found by the first.  CVC4 removes this side-effect of the CHECKSAT and
  67 QUERY commands.
  68
  69 CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
  70 support decimals.
  71
  72 CVC4 does not have support for predicate subtypes, although these are
  73 planned for future releases.
  74
  75 ** SMT-LIB compliance
  76
  77 Every effort has been made to make CVC4 compliant with the SMT-LIB 2.6
  78 standard (http://smtlib.org/).  However, when parsing SMT-LIB input,
  79 certain default settings don't match what is stated in the official
  80 standard.  To make CVC4 adhere more strictly to the standard, use the
  81 "--smtlib-strict" command-line option.  Even with this setting, CVC4 is
  82 somewhat lenient; some non-conforming input may still be parsed and
  83 processed.
  84
  85 For the latest news on SMT-LIB compliance, please check:
  86
  87   http://cvc4.cs.stanford.edu/wiki/SMT-LIB_Compliance
  88
  89 ** Getting statistics
  90
  91 Statistics can be dumped on exit (both normal and abnormal exits) with
  92 the --stats command line option.
  93
  94 ** Time and resource limits
  95
  96 CVC4 can be made to self-timeout after a given number of milliseconds.
  97 Use the --tlimit command line option to limit the entire run of
  98 CVC4, or use --tlimit-per to limit each individual query separately.
  99 Occasionally, you may encounter a problem for which --tlimit does not work very
 100 well.  If you suspect this might be the case, please report it as a bug.  You
 101 can also use "-vv" (double verbosity) to see what CVC4 is doing.
 102
 103 Time-limited runs are not deterministic; two consecutive runs with the
 104 same time limit might produce different results (i.e., one may time out
 105 and respond with "unknown", while the other completes and provides an
 106 answer).  To ensure that results are reproducible, use --rlimit or
 107 --rlimit-per.  These options take a "resource count" (presently, based on
 108 the number of SAT conflicts) that limits the search time.  A word of
 109 caution, though: there is no guarantee that runs of different versions of
 110 CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different
 111 features enabled, or for different architectures) will interpret the resource
 112 count in the same manner.
 113
 114 CVC4 does not presently have a way to limit its memory use; you may opt
 115 to run it from a shell after using "ulimit" to limit the size of the
 116 heap.
 117
 118 ** Proof support
 119
 120 CVC4 1.5 has support for proofs when using uninterpreted functions, arrays,
 121 bitvectors, or their combinations, and proofs are enabled by default.
 122 (Run the configure script with --disable-proof to disable proofs).  Proofs
 123 are exported in LFSC format.
 124
 125 ** Nonlinear arithmetic
 126
 127 CVC4 1.5 has a state-of-the-art linear arithmetic solver as well as some
 128 heuristic support for non-linear arithmetic.
 129
 130 ** Portfolio solving
 131
 132 If enabled at configure-time (./configure --with-portfolio), a second
 133 CVC4 binary will be produced ("pcvc4").  This binary has support for
 134 running multiple instances of CVC4 in different threads.  Use --threads=N
 135 to specify the number of threads, and use --thread0="options for thread 0"
 136 --thread1="options for thread 1", etc., to specify a configuration for the
 137 threads.  Lemmas are *not* shared between the threads by default; to adjust
 138 this, use the --filter-lemma-length=N option to share lemmas of N literals
 139 (or smaller).  (Some lemmas are ineligible for sharing because they include
 140 literals that are "local" to one thread.)
 141
 142 Currently, the portfolio **does not work** with the theory of inductive
 143 datatypes. This limitation will be addressed in a future release.
 144
 145 ** Questions ??
 146
 147 CVC4 and its predecessors have an active user base.  You might want to
 148 subscribe to the mailing list (http://cvc4.stanford.edu/#Technical_Support)
 149 and post a question there.
 150
 151 ** Reporting bugs and making feature requests
 152
 153 CVC4 is under active development.  Should you find a bug in CVC4's
 154 documentation, behavior, API, or SMT-LIB compliance, or if you have
 155 a feature request, please let us know on our bugtracker at
 156
 157   https://github.com/CVC4/CVC4/issues
 158
 159 or send an email to cvc-bugs@cs.stanford.edu.