Difference between revisions of "Tutorials"
(→C++ API) |
(→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 | + | 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-strict'' command line option, which enters a stricter compliance mode. |
CVC4 should be compliant with [http://www.smtlib.org/ the standard], and thus also with David Cok's tutorial, 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]. | CVC4 should be compliant with [http://www.smtlib.org/ the standard], and thus also with David Cok's tutorial, 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]. |
Revision as of 14:48, 30 November 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-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 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 if
then
.
We can do this by first showing that these assumptions entail
, and then showing that
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 . 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();