Difference between revisions of "User Manual"

From CVC4

Latest revision as of 09:31, 26 January 2019

This manual includes information on installing and using CVC4. It is a work in progress.

Getting CVC4

Both pre-compiled binaries and the source code for CVC4 are available for download from http://cvc4.cs.stanford.edu/downloads/builds/.

Getting CVC4 binaries

The most recent binaries can be downloaded from our Nightly Builds pages:

Optimized binaries (statically linked)
Debug binaries (statically linked)

Building CVC4 from source

Sources are available from the same site as the binaries. The source-code is also available in the CVC4 source repository.

For a comprehensive list of dependencies and more detailed build instructions see Building CVC4 from source.

Using the CVC4 binary

Once installed, the CVC4 driver binary ("cvc4") can be executed to directly enter into interactive mode:

$ cvc4
cvc4 1.0 assertions:off
CVC4>

You can then enter commands into CVC4 interactively:

CVC4> OPTION "incremental";
CVC4> OPTION "produce-models";
CVC4> TRANSFORM 25*25;
625
CVC4> x, y : INT;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = -1;
y : INT = 0;
CVC4> ASSERT x >= 0;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = 0;
y : INT = 1;
CVC4>

The above example shows two useful options, incremental and produce-models.

The incremental option allows you to issue multiple QUERY (or CHECKSAT) commands, and allows the use of the PUSH and POP commands. Without this option, CVC4 optimizes itself for a single QUERY or CHECKSAT command (though you may issue any number of ASSERT commands). The incremental option may also be given by passing the -i command line option to CVC4.
The produce-models option allows you to query the model (here, with the COUNTERMODEL command) after an "invalid" QUERY (or "satisfiable" CHECK-SAT). Without it, CVC4 doesn't do the bookkeeping necessary to support model generation. The produce-models option may also be given by passing the -m command line option to CVC4.

So, if you invoke CVC4 with -im, you don't need to pass those options at all:

$ cvc4 -im
cvc4 1.0 assertions:off
CVC4> x, y : INT;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = -1;
y : INT = 0;
CVC4> ASSERT x >= 0;
CVC4> QUERY x = y;
invalid
CVC4> COUNTERMODEL;
x : INT = 0;
y : INT = 1;
CVC4>

By default, CVC4 operates in CVC-language mode. If you enter something that looks like SMT-LIB, it will suggest that you use the "--lang smt" command-line option for SMT-LIB mode:

CVC4> (declare-fun x () Int)
Parse Error: <shell>:1.7: In CVC4 presentation language mode, but SMT-LIB format detected.  Use --lang smt for SMT-LIB support.
CVC4>

Verbosity

CVC4 has various levels of verbosity. By default, CVC4 is pretty quiet, only reporting serious warnings and notices. If you're curious about what it's doing, you can pass CVC4 the -v option:

$ cvc4 -v file.smt2
Invoking: (set-logic AUFLIRA)
Invoking: (set-info :smt-lib-version 2.000000)
Invoking: (set-info :category "crafted")
Invoking: (set-info :status unsat)
Invoking: (declare-fun x () Real)
etc...

For even more verbosity, you can pass CVC4 an additional -v:

$ cvc4 -vv file.smt2
Invoking: (set-logic AUFLIRA)
Invoking: (set-info :smt-lib-version 2.000000)
Invoking: (set-info :category "crafted")
Invoking: (set-info :status unsat)
Invoking: (declare-fun x () Real)
etc...
expanding definitions...
constraining subtypes...
applying substitutions...
simplifying assertions...
doing static learning...
etc...

Internally, verbosity is just an integer value. It starts at 0, and with every -v on the command line it is incremented; with every -q, decremented. It can also be set directly. From CVC language:

CVC4> OPTION "verbosity" 2;

Or from SMT-LIB language:

CVC4> (set-option :verbosity 2)

Getting statistics

Statistics can be dumped on exit (both normal and abnormal exits) with the --statistics command line option.

$ cvc4 --statistics foo.smt2
sat
sat::decisions, 0
sat::propagations, 3
sat::starts, 1
theory::uf::TheoryUF::functionTermsCount, 2
theory::uf::TheoryUF::mergesCount, 2
theory::uf::TheoryUF::termsCount, 6
theory<THEORY_UF>::propagations, 1 
driver::filename, foo.smt2
driver::sat/unsat, sat
driver::totalTime, 0.02015373
[many others]

Many statistics name-value pairs follow, one comma-separated pair per line.

Exit status

Successful exit is marked by the exit code 0. Most "normal errors" return a 1 as the exit code, but out of memory conditions, terminating signals, and other conditions can produce different (nonzero) exit codes. In interactive mode, parse errors are ignored and the next line read; so in interactive mode, you may see an exit code of 0 even in the presence of such an error.

Note on previous versions: Up to version 1.2 of CVC4, exit status depended on the result ("sat" results caused an exit code of 10, "unsat" of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

CVC4's input languages

When not used in interactive mode, CVC4 can read its input from an external file. It accepts the following input languages:

CVC4's native language
SMT-LIB 2.0 (see David Cok's SMT-LIB tutorial)
SMT-LIB 1.0

CVC4 tries to automatically recognize the input language based on the file's extension: .cvc for CVC4's native language, .smt2 for SMT-LIB 2.0 and .smt for SMT-LIB 1.0. If the file extension does not match one of the previously mentioned ones you can specify the input language via the command line flag --lang. To see all language options type:

$ cvc4 --lang help

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 "--smtlib" command-line option. Even with this setting, CVC4 is somewhat lenient; some non-conforming input may still be parsed and processed.

Supported Theories

The following theories are currently fully supported

Booleans
Uninterpreted functions
Arrays [with extensionality]
Inductive datatypes
Tuples and record types
Fixed width bitvectors
Linear mixed real integer arithmetic
- Integer division and modulus by integer constants is supported by the "--rewrite-divk" flag
Finite sets

CVC4 supports first-order quantification and theory combinations of the above theories.

The following theories are currently partially supported and are undergoing development:

Strings

Theories with highly limited support:

CVC4's non-linear real and non-linear integer arithmetic support is currently unlikely to satisfy a user's needs. The current support is for parsing, rewrites, and a very limited class of proofs of unsatisifiability. The class of proofs is what is provable by linear arithmetic where each monomial (e.g. "xxy") is treated as a unique variable.

The CVC4 library interface (API)

There are a number of examples of using CVC4 as a library distributed with the source code of the project. There are given in the "/examples" directory.

Using CVC4 in a C++ project

A basic C++ example for using cvc4 is given in the file /examples/simple_vc_cxx.cpp. The file goes through the examples for the basic interaction with CVC4:

Constructing an ExprManager em
Constructing an SmtEngine w.r.t. em.
Getting a copy of the Type for mathematical integers from em, em.integerType().
Constructing new Expressions
1. Integer variables x and y: Expr x = em.mkVar("x", integer);
2. The rational constant 0: em.mkConst(Rational(0));
3. Constructing new expressions existing expressions: em.mkExpr(kind::GT, x, zero);
Querying the SmtEngine whether or not a formula is valid.

More information on the interfaces for Expr, Type, ExprManager and SmtEngine can be found in their respective header files.

To compile simple_vc_cxx.cpp, there are different build instructions for whether or not you are compiling against a version of CVC4 in a local build directory or one installed via "make install" into a directory $PREFIX.

Local Build Directory: If you have build cvc4 via the "make" command before, you can compile simple_vc_cxx.cpp via "make examples". The executable will then be "./builds/examples/simple_vc_cxx".

   $ make examples
   [...]
   $ ./builds/examples/simple_vc_cxx 
   Checking validity of formula ((x > 0) AND (y > 0)) => (((2 * x) + y) >= 3) with CVC4.
   CVC4 should report VALID.
   Result from CVC4 is: valid

Installed Copy: If you have installed CVC4 via "make install" into the directory $PREFIX (which you can configure via "./configure --prefix=$PREFIX" you will need to modify lines 21-22.

   //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
   #include "smt/smt_engine.h"

First, uncomment line 21 and comment out line 22. You may now

You can now compile and run by executing

   g++ -I$PREFIX/include -L$PREFIX/lib -lcvc4 examples/simple_vc_cxx.cpp -o simple_vc_cxx
   ./simple_vc_cxx

You may need to add $PREFIX/lib is LD_LIBRARY_PATH or the equivalent.

Using CVC4 from Java

The compatibility interface

Upgrading from CVC3 to CVC4

Features not supported by CVC4 (yet)

Type Correctness Conditions (TCCs)

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). The TCC can be checked by CVC3 or another solver. (CVC3 can also check TCCs while solving with +tcc.)

If you were using the text interfaces of CVC3

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.

If you were using the library ("in-memory") interface of CVC3

If you were using CVC3 from C

If you were using CVC3 from Java

Advanced features

This section describes some features of CVC4 of interest to developers and advanced users.

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.

Dumping API calls or preprocessed output

[to do]

Changing the output language

[to do]

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).

Parallel solving

[Builds not ported to Stanford yet] The most recent binaries with support for parallel solving can be downloaded from our Nightly Builds pages:

Optimized binaries (statically linked)
Debug binaries (statically linked)

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.

See more details and examples in the tutorial.

Emacs support

For a suggestion of editing CVC4 source code with emacs, see the file contrib/editing-with-emacs. For a CVC language mode (the native input language for CVC4), see contrib/cvc-mode.el.

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=User_Manual&oldid=5738"