diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-18 17:57:56 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | d78113d408d706d44c1d8cfc379fa86cd8e20460 (patch) | |
| tree | f56be50b213272c6d14516df475ed5fcb2fd6b57 /examples/sets-translate | |
| parent | ed8d326cbdec820d347d8b4b5ee7b23c3367d169 (diff) | |
cmake: Add target runexamples.
Diffstat (limited to 'examples/sets-translate')
| -rw-r--r-- | examples/sets-translate/CMakeLists.txt | 22 | ||||
| -rw-r--r-- | examples/sets-translate/sets-translate-example-input.smt2 | 22 |
2 files changed, 32 insertions, 12 deletions
diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt index bcf220f32..1c34d3aaf 100644 --- a/examples/sets-translate/CMakeLists.txt +++ b/examples/sets-translate/CMakeLists.txt @@ -1,16 +1,14 @@ -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() diff --git a/examples/sets-translate/sets-translate-example-input.smt2 b/examples/sets-translate/sets-translate-example-input.smt2 new file mode 100644 index 000000000..3bf1a9b6a --- /dev/null +++ b/examples/sets-translate/sets-translate-example-input.smt2 @@ -0,0 +1,22 @@ +; 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) + |