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 Tue, 24 Dec 2013 09:12:59 -0500