1.1 Starting CVC

The distribution contains a pre-compiled Linux binary, bin/cvc. This binary reads commands in CVC's presentation language from standard input.

1.2 Running CVC on the examples

The distribution comes with several illustrative examples, which are docs/examples/*.cvc. If docs/examples/ is the current working directory, then the following command will run CVC on the example arrays.cvc:

../../bin/cvc < arrays.cvc


1.3 Command-line options

The following command-line options are accepted by CVC:
+sat SAT mode: use Chaff as the SAT solver. When using Chaff, CVC cannot produce proofs or manipulate contexts, but it may run much faster.
-sat (default) use very simple SAT solver
+proofs produce proofs.
-proofs (default) do not produce proofs (CVC will run faster).
+dagify_proofs (default) print proofs with all common subexpressions shared.
-dagify_proofs do not print proofs with all common subexpressions shared. (See remark for -dagify_exprs below.)
+dagify_exprs (default) print CVC expressions with all common subexpressions shared.
-dagify_exprs do not print CVC expressions with all common subexprs shared. The exprs may be easier to read. On the other hand, printing dags as trees can incur exponential blow, so they could be huge.


Unique prefixes, like "+g" and "+p" can be used. So can "+de" for "+dagify_exprs", etc.