From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 13 Sep 2018 00:59:57 +0000 (-0700)
Subject: cmake: Added target examples (currently .cpp examples only)
X-Git-Tag: cvc5-1.0.0~4555
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dfdacd1fb241c08569cc20b2287c6aedc6b76d6a;p=cvc5.git

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

diff --git a/CMakeLists.txt b/CMakeLists.txt
index a1d137232..7b8b1665c 100644
--- 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 e69de29bb..a3f4f5e30 100644
--- 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 e69de29bb..38dc563c0 100644
--- 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 e69de29bb..5a0e484c8 100644
--- 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 e69de29bb..0d20e9fed 100644
--- 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 e69de29bb..8676994fd 100644
--- 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)