Use separate CMake project for CVC4 examples. (#3196)

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;