Enable Java examples (#7702)

5 files changed, 71 insertions, 36 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index fb84058a3..ac654957a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -475,7 +475,6 @@ endif()
 
 if(BUILD_BINDINGS_JAVA)
   add_subdirectory(src/api/java)
-  message(WARNING "Java API is currently under development.")
 endif()
 
 if(BUILD_DOCS)
diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in
index 6b238fb38..11217e087 100644
--- a/cmake/cvc5Config.cmake.in
+++ b/cmake/cvc5Config.cmake.in
@@ -21,9 +21,7 @@ if(NOT TARGET cvc5::cvc5)
   include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake)
 endif()
 
-# TODO(project wishue #83): enable these lines
-# if(CVC5_BINDINGS_JAVA AND NOT TARGET cvc5::cvc5jar)
-#  set_and_check(CVC5_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@")
-# include(${CMAKE_CURRENT_LIST_DIR}/cvc5JavaTargets.cmake)
-# endif()
+if(CVC5_BINDINGS_JAVA AND NOT TARGET cvc5::cvc5jar)
+ include(${CMAKE_CURRENT_LIST_DIR}/cvc5JavaTargets.cmake)
+endif()
 
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index d08e63e0f..27ecd72b5 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -85,23 +85,39 @@ add_subdirectory(api/cpp)
 
 if(TARGET cvc5::cvc5jar)
   find_package(Java REQUIRED)
+  find_package(JNI REQUIRED)
   include(UseJava)
+  message(STATUS "JNI_LIBRARIES: ${JNI_LIBRARIES}")
 
-  ## disabled until bindings for the new API are in place (issue #2284)
-  # get_target_property(CVC5_JAR cvc5::cvc5jar JAR_FILE)
-  #
-  # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC5_JAR}")
-  #
-  # add_test(
-  #   NAME java/SimpleVC
-  #   COMMAND
-  #     ${Java_JAVA_EXECUTABLE}
-  #       -cp "${CVC5_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
-  #       -Djava.library.path=${CVC5_JNI_PATH}
-  #       SimpleVC
-  # )
-  # TODO(project wishue #83): enable java examples
-  # add_subdirectory(api/java)
+  # get the directories of libraries libjawt.so and libjvm.so
+  set(JNI_LIBRARIES_PATHS "")
+  foreach(LIB ${JNI_LIBRARIES})
+    get_filename_component(LIB_PATH ${LIB} DIRECTORY)
+    set(JNI_LIBRARIES_PATHS "${JNI_LIBRARIES_PATHS}${LIB_PATH}:")
+  endforeach()
+
+  message(STATUS "JNI_LIBRARIES_PATHS: ${JNI_LIBRARIES_PATHS}")
+  # get directory build/install/lib where libcvc5jni.so is installed
+  get_target_property(CVC5_LIB_FILE cvc5::cvc5 LOCATION)
+  get_filename_component(CVC5_JNI_PATH ${CVC5_LIB_FILE} DIRECTORY)
+  message(STATUS "CVC5_JNI_PATH: ${CVC5_JNI_PATH}")
+
+
+  get_target_property(CVC5_JAR cvc5::cvc5jar JAR_FILE)
+  message(STATUS "cvc5jar: ${CVC5_JAR}")
+
+  add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC5_JAR}")
+  add_test(
+    NAME java/SimpleVC
+    COMMAND
+      ${Java_JAVA_EXECUTABLE}
+        -cp "${CVC5_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
+        -Djava.library.path=${CVC5_JNI_PATH}
+        SimpleVC
+  )
+  set_tests_properties(java/SimpleVC PROPERTIES
+    ENVIRONMENT "LD_LIBRARY_PATH=${JNI_LIBRARIES_PATHS}")
+  add_subdirectory(api/java)
 endif()
 
 if(CVC5_BINDINGS_PYTHON)
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 29ca63b93..bd4eb179a 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -14,21 +14,26 @@
 ##
 
 set(EXAMPLES_API_JAVA
-  ## disabled until bindings for the new API are in place (issue #2284)
-  # BitVectors
-  # BitVectorsAndArrays
-  # CVC5Streams
-  # Combination
-  # Datatypes
-  # Exceptions
-  # FloatingPointArith
-  # HelloWorld
-  # LinearArith
-  # PipedInput
-  # Relations
-  # Statistics
-  # Strings
-  # UnsatCores
+   BitVectors
+   BitVectorsAndArrays
+   Combination
+   Datatypes
+   Exceptions
+   Extract
+   FloatingPointArith
+   HelloWorld
+   LinearArith
+   QuickStart
+   Relations
+   Sequences
+   Sets
+   Statistics
+   Strings
+   SygusFun
+   SygusGrammar
+   SygusInv
+   Transcendentals
+   UnsatCores
 )
 
 foreach(example ${EXAMPLES_API_JAVA})
@@ -47,4 +52,6 @@ foreach(example ${EXAMPLES_API_JAVA})
         ${example}
   )
   set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES SKIP_RETURN_CODE 77)
+  set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES
+    ENVIRONMENT "LD_LIBRARY_PATH=${JNI_LIBRARIES_PATHS}")
 endforeach()
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index ecfec2109..2c4151be7 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -142,3 +142,18 @@ add_jar(cvc5jar
 )
 
 add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
+
+# install in the same directory of cvc5-targets
+install(TARGETS cvc5jni
+  LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
+  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
+)
+
+install_jar(cvc5jar DESTINATION share/java)
+
+install_jar_exports(
+  TARGETS cvc5jar
+  NAMESPACE cvc5::
+  FILE cvc5JavaTargets.cmake
+  DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5
+)