diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | examples/sets-translate/sets-translate-example-input.smt2 | 2 | ||||
| -rw-r--r-- | examples/translator-example-input.smt2 | 20 |
3 files changed, 23 insertions, 3 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 33d341ac8..68eb06074 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -68,7 +68,9 @@ 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(translator "" "${EXAMPLES_LINK_LIBS}" "" + # argument to binary (for testing) + ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) if(BUILD_BINDINGS_JAVA) find_package(Java REQUIRED) diff --git a/examples/sets-translate/sets-translate-example-input.smt2 b/examples/sets-translate/sets-translate-example-input.smt2 index 3bf1a9b6a..be230b113 100644 --- a/examples/sets-translate/sets-translate-example-input.smt2 +++ b/examples/sets-translate/sets-translate-example-input.smt2 @@ -1,5 +1,3 @@ -; COMMAND-LINE: --finite-model-find -; EXPECT: sat (set-logic ALL) (declare-sort Atom 0) diff --git a/examples/translator-example-input.smt2 b/examples/translator-example-input.smt2 new file mode 100644 index 000000000..be230b113 --- /dev/null +++ b/examples/translator-example-input.smt2 @@ -0,0 +1,20 @@ +(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) + |