1 files changed, 46 insertions, 0 deletions
diff --git a/examples/README.md b/examples/README.md
new file mode 100644
index 000000000..18834719e
--- /dev/null
+++ b/examples/README.md
@@ -0,0 +1,46 @@
+# CVC4 API 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
+
+## Building Examples
+
+The examples provided in this directory are not built by default.
+
+```
+  mkdir <build_dir>
+  cd <build_dir>
+  cmake ..
+  make               # use -jN for parallel build with N threads
+
+  ctest              # run all examples
+  ctest -R <example> # run specific example '<example>'
+
+  # Or just run the binaries in directory <build_dir>/bin/, for example:
+  bin/api/bitvectors
+```
+
+**Note:** If you installed CVC4 in a non-standard location you have to
+additionally specify `CMAKE_PREFIX_PATH` to point to the location of
+`CVC4Config.cmake` (usually `<your-install-prefix>/lib/cmake`) as follows:
+
+```
+  cmake .. -DCMAKE_PREFIX_PATH=<your-install-prefix>/lib/cmake
+```
+
+The examples binaries are built into `<build_dir>/bin`.
+
+## 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.
+
+## 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.