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
The above example shows two useful options, incremental and produce-models.
-icommand line option to CVC4.
-mcommand 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>
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.,
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 $
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
cvc4 -v file.smt2
For even more verbosity, you can pass CVC4 an additional
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)
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.
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.
This section describes some features of CVC4 of interest to developers and advanced users.
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-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.
CVC4 1.7 supports proofs in the LFSC proof format for quantifier-free reasoning in the theories of
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.