set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin/examples)
-# Create target examples. Add a dependency for each examples you add.
+# 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)
-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)
+# 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_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 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;...")
+# > ouput_dir: Determines the examples subdirectory and is empty (passed as
+# empty string) for the examples root director (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 '<subdirs>/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 '<subdirs>/myexample.cpp'
+ # we create test target 'example/<subdirs>/myexample'
+ # and run it with 'ctest -R "example/<subdirs>/<example>"'.
+ if("${output_dir}" STREQUAL "")
+ set(example_test example/${name})
+ set(example_bin_dir ${EXAMPLES_BIN_DIR})
+ else()
+ set(example_test example/${output_dir}/${name})
+ set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
+ 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()
-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})
+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)
-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)
-set(EXAMPLES_API_BIN_DIR ${EXAMPLES_BIN_DIR}/api)
-
set(CVC4_EXAMPLES_API
bitvectors
bitvectors-new
strings-new
)
+set(EXAMPLES_API_LINK_LIBS cvc4 cvc4parser)
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})
+ cvc4_add_example(${example}
+ "" "${EXAMPLES_API_LINK_LIBS}" "api")
endforeach()
if(BUILD_BINDINGS_JAVA)
-set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_API_BIN_DIR}/java)
+set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_BIN_DIR}/api/java)
file(MAKE_DIRECTORY ${EXAMPLES_API_JAVA_BIN_DIR})
-add_custom_target(BitVectorsjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/BitVectors.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples BitVectorsjava)
-
-add_custom_target(BitVectorsAndArraysjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/BitVectorsAndArrays.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples BitVectorsAndArraysjava)
-
-## disabled until bindings for the new API are in place (issue #2284)
-# add_custom_target(CVC4Streamsjava
-# COMMAND
-# ${Java_JAVAC_EXECUTABLE}
-# -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/CVC4Streams.java
-# -d ${CMAKE_BINARY_DIR}/bin/examples/api/java
-# DEPENDS cvc4jar)
-# add_dependencies(examples CVC4Streamsjava)
-
-add_custom_target(Combinationjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Combination.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples Combinationjava)
-
-add_custom_target(Datatypesjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Datatypes.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples Datatypesjava)
-
-add_custom_target(HelloWorldjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/HelloWorld.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples HelloWorldjava)
-
-add_custom_target(LinearArithjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/LinearArith.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples LinearArithjava)
-
-## disabled until bindings for the new API are in place (issue #2284)
-# add_custom_target(PipedInputjava
-# COMMAND
-# ${Java_JAVAC_EXECUTABLE}
-# -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/PipedInput.java
-# -d ${EXAMPLES_API_JAVA_BIN_DIR}
-# DEPENDS cvc4jar)
-# add_dependencies(examples PipedInputjava)
-
-add_custom_target(Stringsjava
- COMMAND
- ${Java_JAVAC_EXECUTABLE}
- -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/Strings.java
- -d ${EXAMPLES_API_JAVA_BIN_DIR}
- DEPENDS cvc4jar)
-add_dependencies(examples Stringsjava)
+set(EXAMPLES_API_JAVA
+ BitVectors
+ BitVectorsAndArrays
+ ## disabled until bindings for the new API are in place (issue #2284)
+ #CVC4Streams
+ Combination
+ Datatypes
+ HelloWorld
+ LinearArith
+ ## disabled until bindings for the new API are in place (issue #2284)
+ #PipedInput
+ Strings
+)
+
+foreach(example ${EXAMPLES_API_JAVA})
+ add_custom_target(${example}
+ COMMAND
+ ${Java_JAVAC_EXECUTABLE}
+ -cp ${EXAMPLES_JAVA_CLASSPATH} ${CMAKE_CURRENT_SOURCE_DIR}/${example}.java
+ -d ${EXAMPLES_API_JAVA_BIN_DIR}
+ DEPENDS cvc4jar)
+ add_dependencies(examples ${example})
+ set(example_test example/api/java/${example})
+ add_test(
+ NAME ${example_test}
+ COMMAND
+ ${Java_JAVA_EXECUTABLE}
+ -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/
+ -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/api/java/"
+ ${example}
+ )
+ set_tests_properties(${example_test} PROPERTIES LABELS "example")
+endforeach()
include_directories(.)
-set(EXAMPLES_HASHSMT_BIN_DIR ${EXAMPLES_BIN_DIR}/hashsmt)
+set(EXAMPLES_HASHSMT_LINK_LIBS 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})
+ cvc4_add_example(sha1_inversion
+ "sha1_inversion.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
+ "a" "sha1_inversion.outfile") # arguments to binary (for testing)
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_collision
- PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${EXAMPLES_HASHSMT_BIN_DIR})
+cvc4_add_example(sha1_collision
+ "sha1_collision.cpp word.cpp" "${EXAMPLES_HASHSMT_LINK_LIBS}" "hashsmt"
+ "1" "1" "sha1_collision.outfile") # arguments to binary (for testing)
smt2toredlog
)
+set(EXAMPLES_NRA_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
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})
+ cvc4_add_example(${example}
+ "" "${EXAMPLES_NRA_TRANSLATE_LINK_LIBS}" "nra-translate"
+ # arguments to binary (for testing)
+ # input file is required by all tests
+ ${CMAKE_CURRENT_SOURCE_DIR}/nra-translate-example-input.smt2
+ # This is a dummy argument for smt2toredlog (argument is only printed, can
+ # be anything for testing purposes). We pass this to all examples since the
+ # other examples ignore additional arguments.
+ "foo")
endforeach()
--- /dev/null
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status sat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (+ x n) 0))
+(assert (= (+ y n) 1))
+
+(check-sat)
-set(EXAMPLES_SETS_TRANSLATE_BIN_DIR ${EXAMPLES_BIN_DIR}/sets-translate)
-
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)
+ set(EXAMPLES_SETS_TRANSLATE_LINK_LIBS cvc4 cvc4parser)
+ cvc4_add_example(sets2arrays
+ "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+ # argument to binary (for testing)
+ ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
+
+ cvc4_add_example(sets2axioms
+ "sets_translate.cpp" "${EXAMPLES_SETS_TRANSLATE_LINK_LIBS}" "sets-translate"
+ # argument to binary (for testing)
+ ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
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()
--- /dev/null
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun k (Atom Atom) (Set Atom))
+
+(declare-fun t0 () Atom)
+(declare-fun t1 () Atom)
+(declare-fun t2 () Atom)
+(declare-fun v () Atom)
+(declare-fun b2 () Atom)
+
+(assert (forall ((b Atom)) (or
+(member v (k t0 b))
+(member v (k t1 b))
+) ))
+
+(assert (not (member v (k t2 b2))))
+
+(check-sat)
+
projects / cvc5.git / commitdiff