RELEASE-NOTES

   1 Release Notes for CVC4 1.0, October 2012
   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"
   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.0, and file.cvc is the presentation language).  To override
  14 this, you can use the --lang option.
  15
  16 ** Type correctness
  17
  18 Type Correctness Conditions (TCCs), and the checking of such, are not
  19 supported by CVC4 1.0.  Thus, a function defined only on integers can be
  20 applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain,
  21 but may produce strange results.  For example:
  22
  23   f : INT -> INT;
  24   ASSERT f(1/3) = 0;
  25   ASSERT f(2/3) = 1;
  26   CHECKSAT;
  27   % sat
  28   COUNTEREXAMPLE;
  29   % f : (INT) -> INT = LAMBDA(x1:INT) : 0;
  30
  31 CVC3 can be used to produce TCCs for this input (with the +dump-tcc option),
  32 and the TCC can be checked with CVC4.
  33
  34 ** Changes in CVC's Presentation Language
  35
  36 The native language of all solvers in the CVC family, referred to as the
  37 "presentation language," has undergone some revisions for CVC4.  The
  38 most notable is that CVC4 does _not_ add counterexample assertions to
  39 the current assertion set after a SAT/INVALID result.  For example:
  40
  41   x, y : INT;
  42   ASSERT x = 1 OR x = 2;
  43   ASSERT y = 1 OR y = 2;
  44   ASSERT x /= y;
  45   CHECKSAT;
  46   % sat
  47   QUERY x = 1;
  48   % invalid
  49   QUERY x = 2;
  50   % invalid
  51
  52 Here, CVC4 responds "invalid" to the second and third queries, because
  53 each has a counterexample (x=2 is a counterexample to the first, and
  54 x=1 is a counterexample to the second).  However, CVC3 will respond
  55 with "valid" to one of these two, as the first query (the CHECKSAT)
  56 had the side-effect of locking CVC3 into one of the two cases; the
  57 later queries are effectively querying the counterexample that was
  58 found by the first.  CVC4 removes this side-effect of the CHECKSAT and
  59 QUERY commands.
  60
  61 CVC4 supports rational literals (of type REAL) in decimal; CVC3 did not
  62 support decimals.
  63
  64 CVC4 does not have support for the IS_INTEGER predicate.
  65
  66 ** SMT-LIB compliance
  67
  68 Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0
  69 standard (http://smtlib.org/).  However, when parsing SMT-LIB input,
  70 certain default settings don't match what is stated in the official
  71 standard.  To make CVC4 adhere more strictly to the standard, use the
  72 "--smtlib" command-line option.  Even with this setting, CVC4 is
  73 somewhat lenient; some non-conforming input may still be parsed and
  74 processed.
  75
  76 ** Getting statistics
  77
  78 Statistics can be dumped on exit (both normal and abnormal exits)
  79
  80 ** Time and resource limits
  81
  82 CVC4 can be made to self-timeout after a given number of milliseconds.
  83 Use the --tlimit command line option to limit the entire run of
  84 CVC4, or use --tlimit-per to limit each individual query separately.
  85 Preprocessing time is not counted by the time limit, so for some large
  86 inputs which require aggressive preprocessing, you may notice that
  87 --tlimit does not work very well.  If you suspect this might be the
  88 case, you can use "-vv" (double verbosity) to see what CVC4 is doing.
  89
  90 Time-limited runs are not deterministic; two consecutive runs with the
  91 same time limit might produce different results (i.e., one may time out
  92 and responds with "unknown", while the other completes and provides an
  93 answer).  To ensure that results are reproducible, use --rlimit or
  94 --rlimit-per.  These options take a "resource count" (presently, based on
  95 the number of SAT conflicts) that limits the search time.  A word of
  96 caution, though: there is no guarantee that runs of different versions of
  97 CVC4 or of different builds of CVC4 (e.g., two CVC4 binaries with different
  98 features enabled, or for different architectures) will interpret the resource
  99 count in the same manner.
 100
 101 CVC4 does not presently have a way to limit its memory use; you may opt
 102 to run it from a shell after using "ulimit" to limit the size of the
 103 heap.
 104
 105 ** Proof support
 106
 107 CVC4 1.0 has limited support for proofs, and they are disabled by default.
 108 (Run the configure script with --enable-proof to enable proofs).  Proofs
 109 are exported in LFSC format and are limited to the propositional backbone
 110 of the discovered proof (theory lemmas are stated without proof in this
 111 release).
 112
 113 ** Nonlinear arithmetic
 114
 115 CVC4 1.0 has a state-of-the-art linear arithmetic solver.  However, there
 116 is extremely limited support for nonlinear arithmetic in this release.
 117
 118 ** Portfolio solving
 119
 120 If enabled at configure-time (./configure --with-portfolio), a second
 121 CVC4 binary will be produced ("pcvc4").  This binary has support for
 122 running multiple instances of CVC4 in different threads.  Use --threads=N
 123 to specify the number of threads, and use --thread0="options for thread 0"
 124 --thread1="options for thread 1", etc., to specify a configuration for the
 125 threads.  Lemmas are *not* shared between the threads by default; to adjust
 126 this, use the --filter-lemma-length=N option to share lemmas of N literals
 127 (or smaller).  (Some lemmas are ineligible for sharing because they include
 128 literals that are "local" to one thread.)
 129
 130 Currently, the portfolio **does not work** with quantifiers or with
 131 the theory of inductive datatypes.  These limitations will be addressed
 132 in a future release.
 133
 134 ** Questions ??
 135
 136 CVC4 and its predecessors have an active user base.  You might want to
 137 subscribe to the mailing list (http://cs.nyu.edu/mailman/listinfo/cvc-users)
 138 and post a question there.
 139
 140 ** Reporting bugs and making feature requests
 141
 142 CVC4 is under active development.  Should you find a bug in CVC4's
 143 documentation, behavior, API, or SMT-LIB compliance, or if you have
 144 a feature request, please let us know on our bugtracker at
 145
 146   http://church.cims.nyu.edu/bugs/
 147
 148 or send an email to cvc-bugs@cims.nyu.edu.