blob: 33d341ac893fd23bdb04223c978847808ad9fe3f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
include_directories(${PROJECT_SOURCE_DIR}/src)
include_directories(${PROJECT_SOURCE_DIR}/src/include)
include_directories(${CMAKE_BINARY_DIR}/src)
# 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)
# 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)
# 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)
# The build target is created without the path prefix (not supported),
# e.g., for '<output_dir>/myexample.cpp'
# we create build target 'myexample'
# and build it with 'make myexample'.
# As a consequence, all build target names must be globally unique.
if("${src_files}" STREQUAL "")
set(src_files_list ${name}.cpp)
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,
# 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"'.
set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
if("${output_dir}" STREQUAL "")
set(example_test example/${name})
else()
set(example_test example/${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}" "")
if(BUILD_BINDINGS_JAVA)
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)
add_test(
NAME example/SimpleVCjava
COMMAND
${Java_JAVA_EXECUTABLE}
-Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
-cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/"
SimpleVC
)
set_tests_properties(example/SimpleVCjava PROPERTIES LABELS "example")
endif()
add_subdirectory(api)
add_subdirectory(hashsmt)
add_subdirectory(nra-translate)
add_subdirectory(sets-translate)
|
