Difference between revisions of "Tutorials"

From CVC4
Jump to: navigation, search
(Starting Out: helloworld)
(helloworld)
Line 58: Line 58:
 
  $ ./helloworld
 
  $ ./helloworld
 
  Hello World! is invalid
 
  Hello World! is invalid
This should all work if libcvc4 was installed using <code>make install</code>.  If you used <code>make install</code> to a non-standard location, look at instructions for [[Build Problems]].
+
This should all work if libcvc4 was installed using <code>make install</code>.  If you used <code>make install</code> to a non-standard location, look at instructions for [[Build Problems#make install to a non-standard prefix|using non-standard prefix]].
  
 
=Java API=
 
=Java API=

Revision as of 15:25, 28 November 2012

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, 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

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++ barbones.cpp -o barebones -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.

Java API