Getting Started

Using CVC4 Interactively

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

 $ cvc4
 CVC4>

You can then enter commands 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>

Various options can be set when running CVC4. For a complete list, see cvc4 -h.

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 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” CHECKSAT). 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> 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 uses CVC4’s native input language.
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>

When using the correct option, SMT-LIB input can be used:

$ cvc4 --lang smt
CVC4> (set-logic ALL)
CVC4> (declare-fun a () Int)
CVC4>

Using CVC4 with an input file

You can call CVC4 with an input file. The input language will be detected by the file extension. You can also set the input language, as above, using, e.g., --lang=smt.

For example, if example.smt2 has the following content:

(set-logic ALL)
(declare-fun x () Int)
(assert (= (+ x x) (* x 2)))
(check-sat)

The result will be:

$ cvc4 file.smt2
sat
$

Verbosity

CVC4 has various levels of verbosity. By default, CVC4 is 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

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

cvc4 -vv file.smt2

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. Using CVC language:

 CVC4> OPTION "verbosity" 2;

Or using 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
 expr::ExprManager::EQUAL, 1
 expr::ExprManager::MULT, 1
 expr::ExprManager::PLUS, 1
 expr::ExprManager::REGEXP_EMPTY, 1
 expr::ExprManager::REGEXP_SIGMA, 2
 [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 an exit code of 20). This behavior was deemed nonstandard and is no longer the case; successful exits are always 0 in version 1.3 and later.

Advanced features

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

Resource limits

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

Proof support

CVC4 1.7 supports proofs in the LFSC proof format for quantifier-free reasoning in the theories of

• Boolean logic (resolution, DRAT, and LRAT)
• Equality and uninterpreted functions
• Fixed-width bit-vectors
• Extensional arrays

and combinations thereof. For more details on the architecture of proof production in CVC4 see this paper.

Proofs can be generated via the commands

$ cvc4 --dump-proof

Proof checking is available via the LFSC checker.

CVC4 proofs can also be used together with Coq. For more details see SMTCoq.

Emacs support

For a suggestion of editing CVC4 source code with emacs, see this file. For a CVC language mode (the native input language for CVC4), see this file.