Tutorials

CVC language

Finding these examples

Except where noted below, tutorial code appearing in this section is kept in the examples/cvc directory of the CVC4 source distribution. However, tutorial material on this page might be more recent than your CVC4 download. Please refer to the most recent nightly build for the most recent tutorial code.

SMT-LIB

We recommend David Cok's excellent tutorial on SMT-LIB. When running examples from this tutorial, we recommend using CVC4's --smtlib-strict command line option, which enters a stricter compliance mode.

CVC4 should be compliant with the standard, and thus also with David Cok's tutorial, except for some unsupported functionality as outlined in the SMT-LIB compliance section of the User's Manual. If you find something that you believe to be nonconformant, please report it as a bug.

C++ API

• helloworld : a simple example to start off with
• linear_arith : real and integer linear arithmetic
• combination : integer and uninterpreted function example
• bitvectors : bit-vectors example
• bitvectors_and_arrays : integer and uninterpreted function example
• quantifiers

Finding and compiling these examples

Except where noted below, tutorial code appearing in this section is kept in the examples/api directory of the CVC4 source distribution. However, tutorial material on this page might be more recent than your CVC4 download. Please refer to the most recent nightly build for the most recent tutorial code.

To compile everything in the examples/ directory, you can issue the command make examples from the top-level of the source distribution. This will first build CVC4 (if it isn't already built) and then the examples. Some examples from the directory may not be compiled, if (for instance) you haven't built with support for Java, or if you haven't built with support for the compatibility interface; however, all native C++ API examples should be, and those are the only ones appearing in this section.

Note that the example API code in the examples/ directory is intended to be compiled and linked against a CVC4 library built from the source tree. If you try to compile them yourself, against a CVC4 library installed (for example) in /usr, you may find that certain headers cannot be found. There is an easy fix. CVC4 #includes like the following:

#include "expr/expr.h"

should be rewritten to this form:

#include <cvc4/expr/expr.h>

or, most likely, you can remove all such #includes and replace with this single one:

#include <cvc4/cvc4.h>

The example code is not installed by make install.

helloworld

To get used to CVC4, let us go through the following example line-by-line:

 #include <iostream>
 #include <cvc4/cvc4.h>
 using namespace CVC4;
 int main() {
   ExprManager em;
   Expr helloworld = em.mkVar("Hello World!", em.booleanType());
   SmtEngine smt(&em);
   std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
   return 0;
 }

(The example can be found in examples/api/helloworld.cpp.)

First we include the standard <iostream> library, and next we include the public interface for CVC4:

 #include <cvc4/cvc4.h>

cvc4/cvc4.h includes definitions for all of the classes we'll need including ExprManager, Expr and SmtEngine. All of CVC4 lives in the namespace CVC4 and to save a bit of typing let's use the namespace. Now construct a new ExprManager named em.

   ExprManager em;

ExprManagers are in charge of constructing and managing symbolic expressions in CVC4. We then construct the expression Expr helloworld.

   Expr helloworld = em.mkVar("Hello World!", em.booleanType());

helloworld is a symbolic variable with the name "Hello World!" and the type boolean. Note that we ask em to both make the variable and to get em.booleanType(). We now make the main driver for CVC4 reasoning the SmtEngine smt using em as its ExprManager.

 SmtEngine smt(&em);

Finally we print helloworld and query the SmtEngine if the boolean variable helloworld is valid.

 std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;

We can compile the program helloworld from helloworld.cpp by linking against -lcvc4

$ g++ helloworld.cpp -o helloworld -lcvc4
$ ./helloworld
Hello World! is invalid

This should all work if libcvc4 was installed using make install. If you used make install to a non-standard location, look at instructions for using non-standard prefix. If you insist on not-using make, look at instructions for Build_Problems#libcvc4_without_make_install.

linear_arith

With helloworld under our belt, let's try to work through the more advanced examples/api/linear_arith.cpp . In this example, we'll try to show that for $x \in \mathbb{Z}, y \in \mathbb{R}$ if $x \geq 3 y, x \leq y, -2 < x$ then $\max y - x = \frac{2}{3}$. We can do this by first showing that these assumptions entail $y - x \leq \frac{2}{3}$, and then showing that $y - x = \frac{2}{3}$ is consistent with the assumptions.

We use the same basic skeleton of includes/namespaces/main as before. We make an ExprManager and SmtEngine as before.

 ExprManager em;
 SmtEngine smt(&em);

We now set on option on the SmtEngine to enable incremental or multiple query solving, which we will take advantage of.

 smt.setOption("incremental", SExpr("true")); // Enable incremental solving

We get the Types real and integer from em, and we make x and y variables of the respective types.

 Type real = em.realType();
 Type integer = em.integerType();
 Expr x = em.mkVar("x", integer);
 Expr y = em.mkVar("y", real);

We now make Exprs for the 3 Rational constants in the formulas using em.mkConst():

 Expr three = em.mkConst(Rational(3));
 Expr neg2 = em.mkConst(Rational(-2));
 Expr two_thirds = em.mkConst(Rational(2,3));

We will now make the intermediate terms using mkExpr.

 Expr three_y = em.mkExpr(kind::MULT, three, y);
 Expr diff = em.mkExpr(kind::MINUS, y, x);

The first argument to mkExpr is a Kind. Kind is an enum covering all of the various expressions that CVC4 can make. Common operators have fairly standard ALL_CAPS names, such as LEQ, MINUS, AND, BITVECTOR_NAND, and so on. Kind's are in the namespace CVC4::kind. For more information see Expr#Constants.

Using these intermediate terms, we make the following formulas in the same way we made terms.

 Expr x_geq_3y = em.mkExpr(kind::GEQ, x, three_y);
 Expr x_leq_y = em.mkExpr(kind::LEQ, x, y);
 Expr neg2_lt_x = em.mkExpr(kind::LT, neg2, x);

We now assert the assumptions in the SmtEngine:

 Expr assumptions =
   em.mkExpr(kind::AND, x_geq_3y, x_leq_y, neg2_lt_x);
 smt.assertFormula(assumptions);

Alternatively, we could have asserted x_geq_3y, x_leq_y, and neg2_lt_x individually. It is worth pointing out that these are asserted at decision level 0. Modern DPLL(T) solvers are stack based. We can push the stack(), add assertions and then pop() assertions off of the stack.

We can now prove that $y - x \leq \frac{2}{3}$. We first make an Expr for this literal. We now push() the SmtEngine, query the SmtEngine for the validity of the literal given the assumptions, and pop() the SmtEngine.

 smt.push();
 Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds);
 cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
 cout << "CVC4 should report VALID." << endl;
 cout << "Result from CVC4 is: " << smt.query(diff_leq_two_thirds) << endl;
 smt.pop();

It is worth noting that the push() and pop() are not strictly needed in order to not effect context level 0. This is because SmtEngine guards query(phi), checkSat(phi) with internal pushes and pops so phi does not effect the current context. It is needed below; however, as the second lemma is proved in the following fashion:

 smt.push();
 Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds);
 smt.assertFormula(diff_is_two_thirds);
 cout << "Show that the asserts are consistent with " << endl;
 cout << diff_is_two_thirds << " with CVC4." << endl;
 cout << "CVC4 should report SAT." << endl;
 cout << "Result from CVC4 is: " << smt.checkSat(em.mkConst(true)) << endl;
 smt.pop();

Parallel Solving

Obtaining

• Download a statically built binary supporting parallel solving: Optimized build
• If compiling from source, specify by --with-portfolio option to the configure script. This will create an additional binary pcvc4 which supports parallel solving.

./configure --with-portfolio [...]

Running

• The pcvc4 binary allows the user to run multiple instances of the solver simultaneously on the input problem. Each thread can be configured differently by specifying thread-specific options using --threadN=" <thread-specific-options> ". For example,

pcvc4 --thread0="--decision=internal" --thread1="--decision=justification" input.smt2

will run two solver threads with different decision heuristics. The solver will stop as soon as one of threads has an answer.

• The default number of threads is 2. The number of threads can be specified using --threads option. Note that any of the options specified outside all of the --threadi="..." will be applied to all threads. For instance, in

pcvc4 --threads=3 \
       --thread0="--random-seed=10" \
       --thread1="--random-seed=20" \
       --thread2="--random-seed=30" \
       --simplification=none \
       input.smt2

three threads will be run, all with simplification disabled, and different random seeds for the SAT solver.

• We also allow sharing of conflict clauses across different threads. By default, this is disabled but may he enabled by using the --filter-lemma-length option. For example,

pcvc4 --filter-lemma-length=5 ...

will share all lemmas having 5 or less literals.