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/nra-translate | |
| parent | ed8d326cbdec820d347d8b4b5ee7b23c3367d169 (diff) | |
cmake: Add target runexamples.
Diffstat (limited to 'examples/nra-translate')
| -rw-r--r-- | examples/nra-translate/CMakeLists.txt | 15 | ||||
| -rw-r--r-- | examples/nra-translate/nra-translate-example-input.smt2 | 11 |
2 files changed, 21 insertions, 5 deletions
diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt index 19317604c..b719ac2a4 100644 --- a/examples/nra-translate/CMakeLists.txt +++ b/examples/nra-translate/CMakeLists.txt @@ -10,10 +10,15 @@ set(CVC4_EXAMPLES_NRA_TRANSLATE 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() diff --git a/examples/nra-translate/nra-translate-example-input.smt2 b/examples/nra-translate/nra-translate-example-input.smt2 new file mode 100644 index 000000000..229c46d4a --- /dev/null +++ b/examples/nra-translate/nra-translate-example-input.smt2 @@ -0,0 +1,11 @@ +(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) |