diff options
Diffstat (limited to 'examples')
-rw-r--r-- | examples/README | 26 |
1 files changed, 12 insertions, 14 deletions
diff --git a/examples/README b/examples/README index df8cffe73..cc3c23f26 100644 --- a/examples/README +++ b/examples/README @@ -1,8 +1,11 @@ +Examples +-------- + 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.stanford.edu/wiki/Tutorials -*** Files named SimpleVC*, simple_vc* +### 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 @@ -10,24 +13,19 @@ 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. -*** Targeted examples +### Targeted examples The "api" directory contains some more specifically-targeted 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 -*** Building examples +The examples provided in this directory are not built by default. -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). + make examples # build all examples + make runexamples # build and run all examples + make <example> # build examples/<subdir>/<example>.<ext> + ctest example//<subdir>/<example> # run examples/<subdir>/<example>.<ext> +The examples binaries are built into `<build_dir>/bin/examples`. |