Difference between revisions of "Tutorials"
(→SMT-LIB) |
|||
| Line 7: | Line 7: | ||
=SMT-LIB= | =SMT-LIB= | ||
| − | + | We recommend [http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf David Cok's excellent tutorial on SMT-LIB]. When running examples from this tutorial, we recommend using CVC4's ''--smtlib'' and ''--interactive'' command line options, in that order, which enters a stricter compliance mode; ''--interactive'' enables text-editing capabilities with readline (if such support was compiled in when your CVC4 binary was built), making it an attractive mode for running tutorial examples, but currently there's a limitation that a command must occur in its entirety on a single line. | |
| − | + | CVC4 should be compliant with the standard, except for some unsupported functionality as outlined in the [[User's Manual#CVC4's support for the SMT-LIB language|SMT-LIB compliance section of the User's Manual]]. If you find something that you believe to be nonconformant, please [http://cvc4.cs.nyu.edu/bugs/ report it as a bug]. | |
=C++ API= | =C++ API= | ||
Revision as of 05:45, 9 October 2012
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
We recommend David Cok's excellent tutorial on SMT-LIB. When running examples from this tutorial, we recommend using CVC4's --smtlib and --interactive command line options, in that order, which enters a stricter compliance mode; --interactive enables text-editing capabilities with readline (if such support was compiled in when your CVC4 binary was built), making it an attractive mode for running tutorial examples, but currently there's a limitation that a command must occur in its entirety on a single line.
CVC4 should be compliant with the standard, 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
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.
