diff options
author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-05-18 01:18:23 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-18 06:18:23 +0000 |
commit | c781d274fbaf6f4b3e419140c5834511d6b7c7a0 (patch) | |
tree | 66b2a214b02b2a12f988b8b83a9463ee1b9b5a43 /src/api | |
parent | 59d935b0210fe20cdddf5de2be91bb26a66d05fb (diff) |
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
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/java/CMakeLists.txt | 101 | ||||
-rw-r--r-- | src/api/java/cvc5/CVC5ApiException.java | 24 | ||||
-rw-r--r-- | src/api/java/cvc5/CVC5ApiRecoverableException.java | 25 | ||||
-rw-r--r-- | src/api/java/cvc5/IPointer.java | 21 | ||||
-rw-r--r-- | src/api/java/cvc5/Solver.java | 61 | ||||
-rw-r--r-- | src/api/java/cvc5/Utils.java | 35 | ||||
-rw-r--r-- | src/api/java/genkinds.py.in | 1 | ||||
-rw-r--r-- | src/api/java/jni/cvc5JavaApi.h | 38 | ||||
-rw-r--r-- | src/api/java/jni/cvc5_Solver.cpp | 63 |
9 files changed, 360 insertions, 9 deletions
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); +} |