README

This directory contains usage examples of CVC4's different language
bindings, library APIs, and also tutorial examples from the tutorials
available at http://cvc4.cs.nyu.edu/wiki/Tutorials

*** Files named SimpleVC*, simple_vc*

These are examples of how to use CVC4 with each of its library
interfaces (APIs) and language bindings.  They are essentially "hello
world" examples, and do not fully demonstrate the interfaces, but
function as a starting point to using simple expressions and solving
functionality through each library.

*** Targetted examples

The "api" directory contains some more specifically-targetted
examples (for bitvectors, for arithmetic, etc.).  The "api/java"
directory contains the same examples in Java.

*** Installing example source code

Examples are not automatically installed by "make install".  If you
wish to install them, use "make install-examples" after you configure
your CVC4 source tree.  They'll appear in your documentation
directory, under the "examples" subdirectory (so, by default,
in /usr/local/share/doc/cvc4/examples).

*** Building examples

Examples can be built as a separate step, after building CVC4 from
source.  After building CVC4, you can run "make examples".  You'll
find the built binaries in builds/examples (or just in "examples" if
you configured a build directory outside of the source tree).

-- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 24 Dec 2013 09:12:59 -0500