Tutorials
Contents
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
has a tutorial elsewhere
but maybe some content here is useful
C++ API
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.
