diff options
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/CMakeLists.txt | 8 | ||||
-rw-r--r-- | examples/api/bitvectors-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/bitvectors.cpp | 3 | ||||
-rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/bitvectors_and_arrays.cpp | 4 | ||||
-rw-r--r-- | examples/api/combination-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/combination.cpp | 3 | ||||
-rw-r--r-- | examples/api/datatypes-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/datatypes.cpp | 5 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/extract.cpp | 3 | ||||
-rw-r--r-- | examples/api/helloworld-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/helloworld.cpp | 3 | ||||
-rw-r--r-- | examples/api/java/CMakeLists.txt | 26 | ||||
-rw-r--r-- | examples/api/linear_arith-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/linear_arith.cpp | 3 | ||||
-rw-r--r-- | examples/api/sets-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/sets.cpp | 5 | ||||
-rw-r--r-- | examples/api/strings-new.cpp | 3 | ||||
-rw-r--r-- | examples/api/strings.cpp | 5 |
20 files changed, 33 insertions, 62 deletions
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index c78c50466..b121c8833 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -19,12 +19,6 @@ set(CVC4_EXAMPLES_API strings-new ) -set(EXAMPLES_API_LINK_LIBS cvc4 cvc4parser) foreach(example ${CVC4_EXAMPLES_API}) - cvc4_add_example(${example} - "" "${EXAMPLES_API_LINK_LIBS}" "api") + cvc4_add_example(${example} "" "api") endforeach() - -if(BUILD_BINDINGS_JAVA) - add_subdirectory(java) -endif() diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index d0c26f134..58912a1bb 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace std; using namespace CVC4::api; diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 59257976d..259eb48ff 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -16,8 +16,7 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include <cvc4/cvc4.h> using namespace std; using namespace CVC4; diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp index 955a83cff..44b5aa018 100644 --- a/examples/api/bitvectors_and_arrays-new.cpp +++ b/examples/api/bitvectors_and_arrays-new.cpp @@ -17,8 +17,7 @@ #include <iostream> #include <cmath> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace std; using namespace CVC4::api; diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 983da71db..1820712bd 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -16,8 +16,8 @@ #include <iostream> #include <cmath> -// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" + +#include <cvc4/cvc4.h> using namespace std; using namespace CVC4; diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp index e78e8919f..5284a0119 100644 --- a/examples/api/combination-new.cpp +++ b/examples/api/combination-new.cpp @@ -18,8 +18,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace std; using namespace CVC4::api; diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 0d8ae0494..646e6b17a 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -18,8 +18,7 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include <cvc4/cvc4.h> using namespace std; using namespace CVC4; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 08918fc87..8c6257725 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace CVC4::api; diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 3bf1df12f..dabc1228f 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -15,9 +15,8 @@ **/ #include <iostream> -#include "options/language.h" // for use with make examples -#include "smt/smt_engine.h" // for use with make examples -//#include <cvc4/cvc4.h> // To follow the wiki + +#include <cvc4/cvc4.h> using namespace CVC4; diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index cb7d96fa5..0cb885b2c 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace std; using namespace CVC4::api; diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index c9240363e..a008ec718 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -16,8 +16,7 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include <cvc4/cvc4.h> using namespace std; using namespace CVC4; diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp index a7fbe22e9..ab869f03c 100644 --- a/examples/api/helloworld-new.cpp +++ b/examples/api/helloworld-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace CVC4::api; diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 1235c4c55..befeaa7bd 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -16,8 +16,7 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include <cvc4/cvc4.h> using namespace CVC4; int main() { diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt index dd7d6566f..2b364c3d1 100644 --- a/examples/api/java/CMakeLists.txt +++ b/examples/api/java/CMakeLists.txt @@ -1,6 +1,3 @@ -set(EXAMPLES_API_JAVA_BIN_DIR ${EXAMPLES_BIN_DIR}/api/java) -file(MAKE_DIRECTORY ${EXAMPLES_API_JAVA_BIN_DIR}) - set(EXAMPLES_API_JAVA BitVectors BitVectorsAndArrays @@ -19,22 +16,19 @@ set(EXAMPLES_API_JAVA ) 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_jar(${example} ${example}.java + INCLUDE_JARS "${CVC4_JAR}" + OUTPUT_DIR "${CMAKE_BINARY_DIR}/bin/api/java") + + set(EXAMPLE_TEST_NAME api/java/${example}) + add_test( - NAME ${example_test} + NAME ${EXAMPLE_TEST_NAME} COMMAND ${Java_JAVA_EXECUTABLE} - -Djava.library.path=${CMAKE_BINARY_DIR}/src/bindings/java/ - -cp "${EXAMPLES_JAVA_CLASSPATH}:${CMAKE_BINARY_DIR}/bin/examples/api/java/" + -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/bin/api/java/${example}.jar" + -Djava.library.path=${CVC4_JNI_PATH} ${example} ) - set_tests_properties(${example_test} PROPERTIES SKIP_RETURN_CODE 77) - set_tests_properties(${example_test} PROPERTIES LABELS "example") + set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES SKIP_RETURN_CODE 77) endforeach() diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp index 2edcaf71e..a4ff9a2cc 100644 --- a/examples/api/linear_arith-new.cpp +++ b/examples/api/linear_arith-new.cpp @@ -17,8 +17,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include "cvc4/api/cvc4cpp.h" using namespace std; using namespace CVC4::api; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 83a0064c9..f1c8b861c 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -17,8 +17,7 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" +#include <cvc4/cvc4.h> using namespace std; using namespace CVC4; diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp index 60df7a82f..2ca3db9d2 100644 --- a/examples/api/sets-new.cpp +++ b/examples/api/sets-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace std; using namespace CVC4::api; diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 3110c01e3..9fb342431 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -16,9 +16,8 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" -#include "options/set_language.h" +#include <cvc4/cvc4.h> +#include <cvc4/options/set_language.h> using namespace std; using namespace CVC4; diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp index 42630dc0e..e83ab89ff 100644 --- a/examples/api/strings-new.cpp +++ b/examples/api/strings-new.cpp @@ -16,8 +16,7 @@ #include <iostream> -// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed -#include "api/cvc4cpp.h" +#include <cvc4/api/cvc4cpp.h> using namespace CVC4::api; diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 96f4dd400..661ae0e77 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -16,9 +16,8 @@ #include <iostream> -//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed -#include "smt/smt_engine.h" -#include "options/set_language.h" +#include <cvc4/cvc4.h> +#include <cvc4/options/set_language.h> using namespace CVC4; |