diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/CMakeLists.txt | 62 | ||||
| -rw-r--r-- | examples/api/CMakeLists.txt | 24 | ||||
| -rw-r--r-- | examples/hashsmt/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 1 | ||||
| -rw-r--r-- | examples/nra-translate/CMakeLists.txt | 13 | ||||
| -rw-r--r-- | examples/sets-translate/CMakeLists.txt | 21 |
6 files changed, 68 insertions, 67 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 37efb84e1..493a7b3bb 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -2,72 +2,30 @@ 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 -) +# Some of the examples require boost. Enable these examples if boost is +# installed. +find_package(Boost) -set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples) +set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples) + +# Create target examples. Add a dependency for each examples you add. +add_custom_target(examples) add_executable(simple_vc_cxx EXCLUDE_FROM_ALL simple_vc_cxx.cpp) target_link_libraries(simple_vc_cxx cvc4 cvc4parser) +add_dependencies(examples simple_vc_cxx) add_executable(simple_vc_quant_cxx EXCLUDE_FROM_ALL simple_vc_quant_cxx.cpp) target_link_libraries(simple_vc_quant_cxx cvc4 cvc4parser) +add_dependencies(examples simple_vc_quant_cxx) add_executable(translator EXCLUDE_FROM_ALL translator.cpp) target_link_libraries(translator cvc4 cvc4parser) +add_dependencies(examples translator) set_target_properties(simple_vc_cxx simple_vc_quant_cxx translator PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_BIN_DIR}) -add_custom_target(examples - DEPENDS - ${CVC4_EXAMPLES} - ${CVC4_EXAMPLES_API} - ${CVC4_EXAMPLES_HASHSMT} - ${CVC4_EXAMPLES_NRA_TRANSLATE} - ${CVC4_EXAMPLES_SETS_TRANSLATE} -) - if(BUILD_BINDINGS_JAVA) find_package(Java REQUIRED) set(EXAMPLES_JAVA_CLASSPATH "${CMAKE_BINARY_DIR}/src/bindings/java/CVC4.jar") diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 55651e238..4e4d81ed3 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -1,10 +1,32 @@ -set(EXAMPLES_API_BIN_DIR ${EXAMPLES_BIN_DIR}/api) +set(EXAMPLES_API_BIN_DIR ${EXAMPLES_BIN_DIR}/api) + +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 +) foreach(example ${CVC4_EXAMPLES_API}) add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp) target_link_libraries(${example} cvc4) set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_API_BIN_DIR}) + add_dependencies(examples ${example}) endforeach() if(BUILD_BINDINGS_JAVA) diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt index 718399f79..bf7c910b9 100644 --- a/examples/hashsmt/CMakeLists.txt +++ b/examples/hashsmt/CMakeLists.txt @@ -1,12 +1,18 @@ include_directories(.) -set(EXAMPLES_HASHSMT_BIN_DIR ${EXAMPLES_BIN_DIR}/hashsmt) +set(EXAMPLES_HASHSMT_BIN_DIR ${EXAMPLES_BIN_DIR}/hashsmt) -add_executable(sha1_inversion EXCLUDE_FROM_ALL sha1_inversion.cpp word.cpp) -target_link_libraries(sha1_inversion cvc4) +if(Boost_FOUND) + add_executable(sha1_inversion EXCLUDE_FROM_ALL sha1_inversion.cpp word.cpp) + target_link_libraries(sha1_inversion cvc4) + add_dependencies(examples sha1_inversion) + set_target_properties(sha1_inversion + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_HASHSMT_BIN_DIR}) +endif() add_executable(sha1_collision EXCLUDE_FROM_ALL sha1_collision.cpp word.cpp) target_link_libraries(sha1_collision cvc4) +add_dependencies(examples sha1_collision) -set_target_properties(sha1_inversion sha1_collision +set_target_properties(sha1_collision PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_HASHSMT_BIN_DIR}) diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index 49e028614..352707455 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -22,7 +22,6 @@ * Author: dejan */ -#include <boost/uuid/sha1.hpp> #include <fstream> #include <iostream> #include <sstream> diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt index 2b1a849de..19317604c 100644 --- a/examples/nra-translate/CMakeLists.txt +++ b/examples/nra-translate/CMakeLists.txt @@ -1,8 +1,19 @@ -set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate) +set(EXAMPLES_NRA_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/nra-translate) + +set(CVC4_EXAMPLES_NRA_TRANSLATE + normalize + smt2info + smt2todreal + smt2toisat + smt2tomathematica + smt2toqepcad + smt2toredlog +) foreach(example ${CVC4_EXAMPLES_NRA_TRANSLATE}) add_executable(${example} EXCLUDE_FROM_ALL ${example}.cpp) target_link_libraries(${example} cvc4 cvc4parser) set_target_properties(${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_NRA_TRANSLATE_BIN_DIR}) + add_dependencies(examples ${example}) endforeach() diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt index fcbb8e3c8..bcf220f32 100644 --- a/examples/sets-translate/CMakeLists.txt +++ b/examples/sets-translate/CMakeLists.txt @@ -1,11 +1,16 @@ -set(EXAMPLES_SETS_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/sets-translate) +set(EXAMPLES_SETS_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/sets-translate) -add_executable(sets2arrays EXCLUDE_FROM_ALL sets_translate.cpp) -target_link_libraries(sets2arrays cvc4 cvc4parser) +if(Boost_FOUND) + add_executable(sets2arrays EXCLUDE_FROM_ALL sets_translate.cpp) + target_link_libraries(sets2arrays cvc4 cvc4parser) + add_dependencies(examples sets2arrays) -add_executable(sets2axioms EXCLUDE_FROM_ALL sets_translate.cpp) -target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS) -target_link_libraries(sets2axioms cvc4 cvc4parser) + add_executable(sets2axioms EXCLUDE_FROM_ALL sets_translate.cpp) + target_compile_definitions(sets2axioms PRIVATE -DENABLE_AXIOMS) + target_link_libraries(sets2axioms cvc4 cvc4parser) + add_dependencies(examples sets2axioms) + + set_target_properties(sets2arrays sets2axioms + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_SETS_TRANSLATE_BIN_DIR}) +endif() -set_target_properties(sets2arrays sets2axioms - PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_SETS_TRANSLATE_BIN_DIR}) |