Add Solver.java to the Java API (#6196)

PR changes:

    Add Solver.java and relation JNI c files
    Update FindJUnit to download JUnit5
    Add Java unit tests

13 files changed, 510 insertions, 28 deletions

diff --git a/cmake/FindJUnit.cmake b/cmake/FindJUnit.cmake
index caa2c3eb9..1532042a4 100644
--- a/cmake/FindJUnit.cmake
+++ b/cmake/FindJUnit.cmake
@@ -1,6 +1,6 @@
 ###############################################################################
 # Top contributors (to current version):
-#   Mathias Preiner
+#   Mathias Preiner, Mudathir Mohamed
 #
 # This file is part of the cvc5 project.
 #
@@ -11,29 +11,53 @@
 # #############################################################################
 #
 # Find JUnit
-# JUnit_FOUND - system has JUnit lib
-# JUnit_JAR - JUnit jar file
-# JUnit_JAR_DEPS - JUnit jar dependencies
+# JUnit_FOUND - should be true for testing
+# JUnit_JAR   - absolute path to JUnit5 jar file
 ##
 
-find_package(Java REQUIRED)
-include(UseJava)
-find_package(Hamcrest REQUIRED)
+include(deps-helper)
 
-find_jar(JUnit_JAR NAMES junit junit4)
+find_jar(JUnit_JAR junit-platform-console-standalone
+  PATHS
+    ${DEPS_BASE}/share/java
+    $ENV{PATH} $ENV{HOME} $ENV{CLASSPATH} $ENV{JUNIT_HOME}
+)
 
+set(JUnit_FOUND_SYSTEM FALSE)
 if(JUnit_JAR)
-  set(JUnit_JAR_DEPS ${Hamcrest_JAR})
-  # Determine version of JUnit
-  execute_process(
-    COMMAND ${Java_JAVA_EXECUTABLE} -cp ${JUnit_JAR} junit.runner.Version
-    OUTPUT_VARIABLE JUnit_VERSION
-    OUTPUT_STRIP_TRAILING_WHITESPACE)
+  set(JUnit_FOUND_SYSTEM TRUE)
 endif()
 
-include(FindPackageHandleStandardArgs)
-find_package_handle_standard_args(JUnit
-  REQUIRED_VARS JUnit_JAR JUnit_JAR_DEPS
-  VERSION_VAR JUnit_VERSION)
+if(NOT JUnit_FOUND_SYSTEM)
+  check_auto_download("JUnit" "")
+  set(JUNIT_VERSION 1.7.1)
+  include(ExternalProject)
 
-mark_as_advanced(JUnit_JAR JUnit_JAR_DEPS)
+  # Download junit generator jar
+  ExternalProject_Add(
+    JUnit-EP-jar
+    PREFIX ${DEPS_PREFIX}
+    URL https://repo1.maven.org/maven2/org/junit/platform/junit-platform-console-standalone/${JUNIT_VERSION}/junit-platform-console-standalone-${JUNIT_VERSION}.jar
+    URL_HASH SHA1=99245bde65d028a8b8ff604be26e929ab6ff2e58
+    DOWNLOAD_NO_EXTRACT ON
+    CONFIGURE_COMMAND ""
+    BUILD_COMMAND ""
+    INSTALL_COMMAND ${CMAKE_COMMAND} -E copy
+      <SOURCE_DIR>/../junit-platform-console-standalone-${JUNIT_VERSION}.jar
+      <INSTALL_DIR>/share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar
+    BUILD_BYPRODUCTS <INSTALL_DIR>/share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar
+  )
+
+  set(JUnit_JAR "${DEPS_BASE}/share/java/junit-platform-console-standalone-${JUNIT_VERSION}.jar")
+endif()
+
+set(JUnit_FOUND TRUE)
+
+mark_as_advanced(JUnit_JAR)
+mark_as_advanced(JUnit_FOUND)
+
+if(JUnit_FOUND_SYSTEM)
+  message(STATUS "Found JUnit: ${JUnit_JAR}")
+else()
+  message(STATUS "Downloading JUnit: ${JUnit_JAR}")
+endif()
\ No newline at end of file
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 51d44c822..d56f594ce 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -13,21 +13,104 @@
 # The build system configuration.
 ##
 
-# create a directory for the cvc package
-file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc")
+# create directories
+file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5")
+set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/jni")
+file(MAKE_DIRECTORY ${JNI_DIR})
 
-# Generate cvc/Kind.java
+# Generate cvc5/Kind.java
 configure_file(genkinds.py.in genkinds.py)
-add_custom_target(
-  gen-java-kinds
-  ALL
+
+set(JAVA_KIND_FILE
+  "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind.java"
+)
+
+add_custom_command(
+  OUTPUT
+    ${JAVA_KIND_FILE}
+  BYPRODUCTS
+    ${JAVA_KIND_FILE}
   COMMAND
     "${PYTHON_EXECUTABLE}"
     "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py"
     --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h"
-    --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc/Kind"
+    --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind"
   DEPENDS
     "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py"
-  COMMENT
-    "Generate Kind.java"
+    "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h"
+)
+
+add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE})
+
+# find java
+find_package(Java COMPONENTS Development REQUIRED)
+include(UseJava)
+
+# specify java source files
+set(JAVA_FILES
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiException.java
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiRecoverableException.java
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/IPointer.java
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/Solver.java
+  ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java
+  ${JAVA_KIND_FILE}
+)
+
+# specify generated jni headers
+set(JNI_HEADERS
+  ${JNI_DIR}/cvc5_Solver.h
+)
+
+# generate jni headers
+add_custom_command(
+  OUTPUT
+    ${JNI_HEADERS}
+  BYPRODUCTS
+    ${JNI_HEADERS}
+  COMMAND
+    # generate jni header files
+    ${Java_JAVAC_EXECUTABLE} -h ${JNI_DIR} ${JAVA_FILES} -d ${JNI_DIR}
+  DEPENDS
+    ${JAVA_FILES}
+  COMMENT "Generate jni headers"
+  VERBATIM
 )
+
+add_custom_target(generate-jni-headers DEPENDS ${JNI_HEADERS})
+add_dependencies(generate-jni-headers generate-java-kinds)
+
+# find jni package
+find_package(JNI REQUIRED)
+message(STATUS "JAVA_AWT_LIBRARY     : ${JAVA_AWT_LIBRARY}")
+message(STATUS "JNI_INCLUDE_DIRS     : ${JNI_INCLUDE_DIRS}")
+message(STATUS "JNI_LIBRARIES        : ${JNI_LIBRARIES} ")
+message(STATUS "JNI_FOUND            : ${JNI_FOUND}")
+message(STATUS "JAVA_AWT_LIBRARY     : ${JAVA_AWT_LIBRARY}")
+message(STATUS "JAVA_JVM_LIBRARY     : ${JAVA_JVM_LIBRARY}")
+message(STATUS "JAVA_INCLUDE_PATH    : ${JAVA_INCLUDE_PATH}")
+message(STATUS "JAVA_INCLUDE_PATH2   : ${JAVA_INCLUDE_PATH2}")
+message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}")
+
+add_library(cvc5jni SHARED jni/cvc5_Solver.cpp)
+add_dependencies(cvc5jni generate-jni-headers)
+
+target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS})
+target_include_directories(cvc5jni PUBLIC ${PROJECT_SOURCE_DIR}/src)
+target_include_directories(cvc5jni PUBLIC ${CMAKE_BINARY_DIR}/src/)
+target_include_directories(cvc5jni PUBLIC ${JNI_DIR})
+target_link_libraries(cvc5jni PRIVATE ${JNI_LIBRARIES})
+target_link_libraries(cvc5jni PRIVATE cvc5)
+
+set(CVC5_JAR "cvc5-${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}.jar")
+
+# create cvc5.jar file
+add_jar(cvc5jar
+  SOURCES
+  ${JAVA_FILES}
+  VERSION ${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}
+  OUTPUT_NAME cvc5
+)
+
+add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
+
+get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
\ No newline at end of file
diff --git a/src/api/java/cvc5/CVC5ApiException.java b/src/api/java/cvc5/CVC5ApiException.java
new file mode 100644
index 000000000..8b8b61198
--- /dev/null
+++ b/src/api/java/cvc5/CVC5ApiException.java
@@ -0,0 +1,24 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+public class CVC5ApiException extends Exception
+{
+  public CVC5ApiException(String message)
+  {
+    super(message);
+  }
+}
diff --git a/src/api/java/cvc5/CVC5ApiRecoverableException.java b/src/api/java/cvc5/CVC5ApiRecoverableException.java
new file mode 100644
index 000000000..3f434d0ff
--- /dev/null
+++ b/src/api/java/cvc5/CVC5ApiRecoverableException.java
@@ -0,0 +1,25 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+
+package cvc5;
+
+public class CVC5ApiRecoverableException extends CVC5ApiException
+{
+  public CVC5ApiRecoverableException(String message)
+  {
+    super(message);
+  }
+}
diff --git a/src/api/java/cvc5/IPointer.java b/src/api/java/cvc5/IPointer.java
new file mode 100644
index 000000000..fc9c95338
--- /dev/null
+++ b/src/api/java/cvc5/IPointer.java
@@ -0,0 +1,21 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+interface IPointer
+{
+  long getPointer();
+}
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
new file mode 100644
index 000000000..6bb1b6b1e
--- /dev/null
+++ b/src/api/java/cvc5/Solver.java
@@ -0,0 +1,61 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+import java.io.IOException;
+
+public class Solver implements IPointer
+{
+  private final long pointer;
+
+  public long getPointer()
+  {
+    return pointer;
+  }
+
+  public Solver()
+  {
+    this.pointer = newSolver();
+  }
+
+  private native long newSolver();
+
+  public void deletePointer()
+  {
+    deletePointer(pointer);
+  }
+
+  private static native void deletePointer(long solverPointer);
+
+  static
+  {
+    Utils.loadLibraries();
+  }
+
+  /**
+   * Set logic.
+   * SMT-LIB: ( set-logic <symbol> )
+   *
+   * @param logic
+   * @throws CVC5ApiException
+   */
+  public void setLogic(String logic) throws CVC5ApiException
+  {
+    setLogic(pointer, logic);
+  }
+
+  private native void setLogic(long solverPointer, String logic) throws CVC5ApiException;
+}
diff --git a/src/api/java/cvc5/Utils.java b/src/api/java/cvc5/Utils.java
new file mode 100644
index 000000000..7f32932e4
--- /dev/null
+++ b/src/api/java/cvc5/Utils.java
@@ -0,0 +1,35 @@
+
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 java API.
+ */
+
+package cvc5;
+
+import java.io.IOException;
+
+class Utils
+{
+  static
+  {
+    loadLibraries();
+  }
+
+  /**
+   * load cvc5 jni library
+   */
+  public static void loadLibraries()
+  {
+    System.loadLibrary("cvc5jni");
+  }
+}
diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in
index 89cf6e3de..15de21805 100644
--- a/src/api/java/genkinds.py.in
+++ b/src/api/java/genkinds.py.in
@@ -23,6 +23,7 @@ import sys
 import re
 
 
+
 # get access to cvc5/src/api/parsekinds.py
 sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api'))
 
diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h
new file mode 100644
index 000000000..2aa860f40
--- /dev/null
+++ b/src/api/java/jni/cvc5JavaApi.h
@@ -0,0 +1,38 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#ifndef CVC5__JAVA_API_H
+#define CVC5__JAVA_API_H
+
+#define CVC5_JAVA_API_TRY_CATCH_BEGIN \
+  try                                 \
+  {
+#define CVC5_JAVA_API_TRY_CATCH_END(env)                             \
+  }                                                                  \
+  catch (const CVC5ApiRecoverableException& e)                       \
+  {                                                                  \
+    jclass exceptionClass =                                          \
+        env->FindClass("cvc5/CVC5ApiRecoverableException");          \
+    env->ThrowNew(exceptionClass, e.what());                         \
+  }                                                                  \
+  catch (const CVC5ApiException& e)                                  \
+  {                                                                  \
+    jclass exceptionClass = env->FindClass("cvc5/CVC5ApiException"); \
+    env->ThrowNew(exceptionClass, e.what());                         \
+  }
+#define CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, returnValue) \
+  CVC5_JAVA_API_TRY_CATCH_END(env)                           \
+  return returnValue;
+#endif  // CVC5__JAVA_API_H
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
new file mode 100644
index 000000000..9d7690e59
--- /dev/null
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -0,0 +1,63 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mudathir Mohamed
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * The cvc5 Java API.
+ */
+
+#include "cvc5_Solver.h"
+
+#include "api/cpp/cvc5.h"
+#include "cvc5JavaApi.h"
+
+using namespace cvc5::api;
+
+/*
+ * Class:     cvc5_Solver
+ * Method:    newSolver
+ * Signature: ()J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_newSolver(JNIEnv*, jobject)
+{
+  Solver* solver = new Solver();
+  return ((jlong)solver);
+}
+
+/*
+ * Class:     cvc5_Solver
+ * Method:    deletePointer
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Solver_deletePointer(JNIEnv*,
+                                                     jclass,
+                                                     jlong pointer)
+{
+  delete ((Solver*)pointer);
+}
+
+/*
+ * Class:     cvc5_Solver
+ * Method:    setLogic
+ * Signature: (Ljava/lang/String;)V
+ */
+JNIEXPORT void JNICALL Java_cvc5_Solver_setLogic(JNIEnv* env,
+                                                jobject,
+                                                jlong solverPointer,
+                                                jstring jLogic)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+
+  Solver* solver = (Solver*)solverPointer;
+  const char* cLogic = env->GetStringUTFChars(jLogic, nullptr);
+  solver->setLogic(std::string(cLogic));
+
+  CVC5_JAVA_API_TRY_CATCH_END(env);
+}
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index c01b1cfe0..ae6db51ef 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -24,3 +24,6 @@ cvc5_add_unit_test_white(solver_white api)
 cvc5_add_unit_test_black(sort_black api)
 cvc5_add_unit_test_black(term_black api)
 cvc5_add_unit_test_white(term_white api)
+if (BUILD_BINDINGS_JAVA)
+  add_subdirectory(java)
+endif()
diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
new file mode 100644
index 000000000..0ef649b87
--- /dev/null
+++ b/test/unit/api/java/CMakeLists.txt
@@ -0,0 +1,60 @@
+###############################################################################
+# Top contributors (to current version):
+#   Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# The build system configuration.
+##
+
+find_package(Java REQUIRED)
+include(UseJava)
+find_package(JUnit REQUIRED)
+
+# specify source files for junit tests
+set(java_test_src_files
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SolverTest.java
+)
+
+# build junit tests
+add_custom_target(
+  build-junit-tests
+  ALL
+  COMMAND
+    ${Java_JAVAC_EXECUTABLE} ${java_test_src_files}
+    -cp ${JUnit_JAR}:${CVC5_JAR_PATH} # add JUnit and cvc5 jar files to the class path
+    -d . # specify the output directory for the generated .class files
+  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 cvc5
+  COMMENT "Run junit tests"
+  VERBATIM
+)
+
+add_dependencies(run-junit-tests build-junit-tests)
+add_dependencies(units run-junit-tests)
\ No newline at end of file
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
new file mode 100644
index 000000000..57758ff88
--- /dev/null
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -0,0 +1,44 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mudathir Mohamed, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Black box testing of the Solver class of the Java API.
+ */
+
+
+package cvc5;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+class SolverTest
+{
+  private Solver d_solver;
+
+  @BeforeEach void setUp()
+  {
+    d_solver = new Solver();
+  }
+
+  @AfterEach void tearDown()
+  {
+    d_solver.deletePointer();
+  }
+
+  @Test void setLogic()
+  {
+    assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV"));    
+  }
+}