From: Gereon Kremer <nafur42@gmail.com>
Date: Sat, 6 Nov 2021 21:43:43 +0000 (-0700)
Subject: Integrate java unit tests into ctest (#7593)
X-Git-Tag: cvc5-1.0.0~867
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8a0a28a334ea7f52b9e42a870fd473cc15bd6720;p=cvc5.git

Integrate java unit tests into ctest (#7593)

This PR properly integrates the java api unit tests into ctest.
---

diff --git a/src/api/__pycache__/parsekinds.cpython-39.pyc b/src/api/__pycache__/parsekinds.cpython-39.pyc
deleted file mode 100644
index 34d010ce4..000000000
Binary files a/src/api/__pycache__/parsekinds.cpython-39.pyc and /dev/null differ
diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
index 61ae74fd2..5f573a117 100644
--- a/test/unit/api/java/CMakeLists.txt
+++ b/test/unit/api/java/CMakeLists.txt
@@ -18,6 +18,7 @@ include(UseJava)
 find_package(JUnit REQUIRED)
 
 get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
+get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)
 
 # specify source files for junit tests
 set(java_test_src_files
@@ -31,9 +32,9 @@ set(java_test_src_files
 )
 
 # build junit tests
-add_custom_target(
-  build-junit-tests
-  ALL
+add_custom_command(
+  OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/tests/SolverTest.class
+  DEPENDS JUnit-EP-jar cvc5jar ${java_test_src_files}
   COMMAND
     ${Java_JAVAC_EXECUTABLE} ${java_test_src_files}
     -cp ${JUnit_JAR}:${CVC5_JAR_PATH} # add JUnit and cvc5 jar files to the class path
@@ -41,29 +42,28 @@ add_custom_target(
   COMMENT "Build junit tests"
   VERBATIM
 )
-
-# make sure junit jar file is present
-add_dependencies(build-junit-tests JUnit-EP-jar)
-# make sure cvc.jar file is built first
-add_dependencies(build-junit-tests cvc5jar)
-
-get_filename_component(CVC5_JNI_PATH ${CVC5_JAR_PATH} DIRECTORY)
-
-# run junit tests
-add_custom_target(
-  run-junit-tests
-  ALL
-  COMMAND
-    # run junit tests
-    ${Java_JAVA_EXECUTABLE}
-    -Djava.library.path=${CVC5_JNI_PATH}
-    -jar ${JUnit_JAR}
-    -cp ${JUnit_JAR}:${CVC5_JAR_PATH}:.
-    -select-package tests
-  COMMENT "Run junit tests"
-  VERBATIM
+add_custom_target(build-junit-tests
+  DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/tests/SolverTest.class
 )
+add_dependencies(build-units build-junit-tests)
+
+macro(cvc5_add_java_api_test name)
+  add_test (NAME unit/api/java/${name}
+    COMMAND
+      ${Java_JAVA_EXECUTABLE}
+      -Djava.library.path=${CVC5_JNI_PATH}
+      -jar ${JUnit_JAR}
+      -cp ${JUnit_JAR}:${CVC5_JAR_PATH}:.
+      -select-package tests
+      -n tests.${name}
+  )
+  set_tests_properties(unit/api/java/${name} PROPERTIES LABELS "unit java")
+endmacro()
 
-add_dependencies(run-junit-tests build-junit-tests)
-add_dependencies(units run-junit-tests)
-add_dependencies(check run-junit-tests)
\ No newline at end of file
+cvc5_add_java_api_test(DatatypeTest)
+cvc5_add_java_api_test(GrammarTest)
+cvc5_add_java_api_test(OpTest)
+cvc5_add_java_api_test(ResultTest)
+cvc5_add_java_api_test(SolverTest)
+cvc5_add_java_api_test(SortTest)
+cvc5_add_java_api_test(TermTest)