cmake: Added target examples (currently .cpp examples only)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index a1d137232ee5455600203037a47b010636d9206d..7b8b1665c8cc037f2afa10baae44915749a0fba2 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -585,6 +585,7 @@ if(ENABLE_PROOFS)
 endif()
 
 add_subdirectory(doc)
+add_subdirectory(examples)
 add_subdirectory(src)
 add_subdirectory(test)
 

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..a3f4f5e30731889df6f18659b4074901498d5151 100644 (file)
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -0,0 +1,70 @@
+include_directories(${PROJECT_SOURCE_DIR}/src)
+include_directories(${PROJECT_SOURCE_DIR}/src/include)
+include_directories(${CMAKE_BINARY_DIR}/src)
+
+set(CVC4_EXAMPLES
+  simple_vc_cxx
+  simple_vc_quant_cxx
+  translator
+)
+set(CVC4_EXAMPLES_API
+  bitvectors
+  bitvectors-new
+  bitvectors_and_arrays
+  bitvectors_and_arrays-new
+  combination
+  combination-new
+  datatypes
+  datatypes-new
+  extract
+  extract-new
+  helloworld
+  helloworld-new
+  linear_arith
+  linear_arith-new
+  sets
+  sets-new
+  strings
+  strings-new
+)
+set(CVC4_EXAMPLES_HASHSMT
+  sha1_collision
+  sha1_inversion
+)
+set(CVC4_EXAMPLES_NRA_TRANSLATE
+  normalize
+  smt2info
+  smt2todreal
+  smt2toisat
+  smt2tomathematica
+  smt2toqepcad
+  smt2toredlog
+)
+set(CVC4_EXAMPLES_SETS_TRANSLATE
+  sets2arrays
+  sets2axioms
+)
+
+add_subdirectory(api)
+add_subdirectory(hashsmt)
+add_subdirectory(nra-translate)
+add_subdirectory(sets-translate)
+
+add_executable(simple_vc_cxx EXCLUDE_FROM_ALL simple_vc_cxx.cpp)
+target_link_libraries(simple_vc_cxx cvc4 cvc4parser)
+
+add_executable(simple_vc_quant_cxx EXCLUDE_FROM_ALL simple_vc_quant_cxx.cpp)
+target_link_libraries(simple_vc_quant_cxx cvc4 cvc4parser)
+
+add_executable(translator EXCLUDE_FROM_ALL translator.cpp)
+target_link_libraries(translator cvc4 cvc4parser)
+
+add_custom_target(examples
+  DEPENDS
+  ${CVC4_EXAMPLES}
+  ${CVC4_EXAMPLES_API}
+  ${CVC4_EXAMPLES_HASHSMT}
+  ${CVC4_EXAMPLES_NRA_TRANSLATE}
+  ${CVC4_EXAMPLES_SETS_TRANSLATE}
+)
+

diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..38dc563c0db0c0aedb6bad4241fb02e7a4e3cda2 100644 (file)
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -0,0 +1,10 @@
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/examples/api)
+
+foreach(example ${CVC4_EXAMPLES_API})
+  add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp)
+  target_link_libraries(${example} cvc4)
+endforeach()
+
+if(BUILD_BINDINGS_JAVA)
+  add_subdirectory(java)
+endif()

diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..5a0e484c86140c125e0186c9db7b902e101c3a0c 100644 (file)
--- a/examples/hashsmt/CMakeLists.txt
+++ b/examples/hashsmt/CMakeLists.txt
@@ -0,0 +1,9 @@
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/examples/hashsmt)
+
+include_directories(.)
+
+add_executable(sha1_inversion EXCLUDE_FROM_ALL sha1_inversion.cpp word.cpp)
+target_link_libraries(sha1_inversion cvc4)
+
+add_executable(sha1_collision EXCLUDE_FROM_ALL sha1_collision.cpp word.cpp)
+target_link_libraries(sha1_collision cvc4)

diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0d20e9fed8f1f88635e581457d5825708429592f 100644 (file)
--- a/examples/nra-translate/CMakeLists.txt
+++ b/examples/nra-translate/CMakeLists.txt
@@ -0,0 +1,6 @@
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/examples/nra-translate)
+
+foreach(example ${CVC4_EXAMPLES_NRA_TRANSLATE})
+  add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp)
+  target_link_libraries(${example} cvc4 cvc4parser)
+endforeach()

diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..8676994fd373e9584012431cf39d3cc8d315ac49 100644 (file)
--- a/examples/sets-translate/CMakeLists.txt
+++ b/examples/sets-translate/CMakeLists.txt
@@ -0,0 +1,8 @@
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin/examples/sets-translate)
+
+add_executable(sets2arrays EXCLUDE_FROM_ALL sets_translate.cpp)
+target_link_libraries(sets2arrays cvc4 cvc4parser)
+
+add_executable(sets2axioms EXCLUDE_FROM_ALL sets_translate.cpp)
+target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS)
+target_link_libraries(sets2axioms cvc4 cvc4parser)