diff options
| -rw-r--r-- | CMakeLists.txt | 1 | ||||
| -rw-r--r-- | examples/CMakeLists.txt | 70 | ||||
| -rw-r--r-- | examples/api/CMakeLists.txt | 10 | ||||
| -rw-r--r-- | examples/hashsmt/CMakeLists.txt | 9 | ||||
| -rw-r--r-- | examples/nra-translate/CMakeLists.txt | 6 | ||||
| -rw-r--r-- | examples/sets-translate/CMakeLists.txt | 8 |
6 files changed, 104 insertions, 0 deletions
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) |