diff options
Diffstat (limited to 'examples/CMakeLists.txt')
| -rw-r--r-- | examples/CMakeLists.txt | 96 |
1 files changed, 41 insertions, 55 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index f81c68236..43f4109a3 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -1,40 +1,30 @@ -include_directories(${PROJECT_SOURCE_DIR}/src) -include_directories(${PROJECT_SOURCE_DIR}/src/include) -include_directories(${CMAKE_BINARY_DIR}/src) +cmake_minimum_required(VERSION 3.2) + +project(cvc4-examples) + +enable_testing() + +# Find CVC4 package. If CVC4 is not installed into the default system location +# use `cmake .. -DCMAKE_PREFIX_PATH=path/to/lib/cmake` to specify the location +# of CVC4Config.cmake. +find_package(CVC4) # Some of the examples require boost. Enable these examples if boost is # installed. find_package(Boost 1.50.0) -set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples) - -# Create target examples. -# -# Only builds the examples, but does not run them. To run and build all -# examples, use target runexamples (below). -# Use macro cvc4_add_example to add examples. -add_custom_target(examples) - -# Create target runexamples. -# Builds and runs all examples. -add_custom_target(runexamples - COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $$ARGS - DEPENDS examples) +set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin) # Add example target and create test to run example with ctest. # # > name: The name of the example # > src_files: The list of source files passed as string "src1 src2 ..." # (alternative: "src1;src2;..."). If empty, <name>.cpp is assumed. -# > libs: The list of libraries to link the example against, passed as either -# - a list variable: set(<list name> <libs1> <libs2> ...) and pass -# as "${<list name>}" -# - a string: pass as "lib1 lib2 ..." (alternative: "lib1;lib2;...") # > output_dir: Determines the examples subdirectory and is empty (passed as # empty string) for the examples root directory (this) # > ARGN: Any additional arguments passed to the macro are interpreted as # as arguments to the test executable. -macro(cvc4_add_example name src_files libs output_dir) +macro(cvc4_add_example name src_files output_dir) # The build target is created without the path prefix (not supported), # e.g., for '<output_dir>/myexample.cpp' # we create build target 'myexample' @@ -45,56 +35,52 @@ macro(cvc4_add_example name src_files libs output_dir) else() string(REPLACE " " ";" src_files_list "${src_files}") endif() - add_executable(${name} EXCLUDE_FROM_ALL ${src_files_list}) - string(REPLACE " " ";" libs_list "${libs_list}") - target_link_libraries(${name} ${libs}) - add_dependencies(examples ${name}) - # The test target is prefixed with test identifier 'example/' and the path, + + add_executable(${name} ${src_files_list}) + target_link_libraries(${name} CVC4::cvc4 CVC4::cvc4parser) + + # The test target is prefixed with the path, # e.g., for '<output_dir>/myexample.cpp' - # we create test target 'example/<output_dir>/myexample' - # and run it with 'ctest -R "example/<output_dir>/myunittest"'. + # we create test target '<output_dir>/myexample' + # and run it with 'ctest -R "<output_dir>/myexample"'. set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir}) if("${output_dir}" STREQUAL "") - set(example_test example/${name}) + set(example_test ${name}) else() - set(example_test example/${output_dir}/${name}) + set(example_test ${output_dir}/${name}) endif() set_target_properties(${name} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${example_bin_dir}) add_test(${example_test} ${example_bin_dir}/${name} ${ARGN}) - set_tests_properties(${example_test} PROPERTIES LABELS "example") endmacro() -set(EXAMPLES_LINK_LIBS cvc4 cvc4parser) -cvc4_add_example(simple_vc_cxx "" "${EXAMPLES_LINK_LIBS}" "") -cvc4_add_example(simple_vc_quant_cxx "" "${EXAMPLES_LINK_LIBS}" "") -cvc4_add_example(translator "" "${EXAMPLES_LINK_LIBS}" "" +cvc4_add_example(simple_vc_cxx "" "") +cvc4_add_example(simple_vc_quant_cxx "" "") +cvc4_add_example(translator "" "" # argument to binary (for testing) ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) -if(BUILD_BINDINGS_JAVA) +add_subdirectory(api) +add_subdirectory(hashsmt) +add_subdirectory(nra-translate) +add_subdirectory(sets-translate) + +if(TARGET CVC4::cvc4jar) find_package(Java REQUIRED) - set(EXAMPLES_JAVA_CLASSPATH "${CMAKE_BINARY_DIR}/src/bindings/java/CVC4.jar") - add_custom_target(SimpleVCjava - COMMAND - ${Java_JAVAC_EXECUTABLE} - -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/SimpleVC.java - -d ${CMAKE_BINARY_DIR}/bin/examples - DEPENDS cvc4jar) - add_dependencies(examples SimpleVCjava) + include(UseJava) + + get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE) + + add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}") + add_test( - NAME example/SimpleVCjava + NAME java/SimpleVC COMMAND ${Java_JAVA_EXECUTABLE} - -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/ - -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/" + -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar" + -Djava.library.path=${CVC4_JNI_PATH} SimpleVC ) - set_tests_properties(example/SimpleVCjava PROPERTIES LABELS "example") -endif() - -add_subdirectory(api) -add_subdirectory(hashsmt) -add_subdirectory(nra-translate) -add_subdirectory(sets-translate) + add_subdirectory(api/java) +endif() |