summaryrefslogtreecommitdiff
path: root/examples
diff options
context:
space:
mode:
Diffstat (limited to 'examples')
-rw-r--r--examples/README26
-rw-r--r--examples/hashsmt/sha1_inversion.cpp6
2 files changed, 18 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`.
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 652fc4e5b..ef5191cb7 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -22,7 +22,13 @@
* Author: dejan
*/
+#include <boost/version.hpp>
+#if BOOST_VERSION > 106700
+#include <boost/uuid/detail/sha1.hpp>
+#else
#include <boost/uuid/sha1.hpp>
+#endif
+
#include <fstream>
#include <iostream>
#include <sstream>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback