summaryrefslogtreecommitdiff
path: root/src/api/java
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/java')
-rw-r--r--src/api/java/CMakeLists.txt101
-rw-r--r--src/api/java/cvc5/CVC5ApiException.java24
-rw-r--r--src/api/java/cvc5/CVC5ApiRecoverableException.java25
-rw-r--r--src/api/java/cvc5/IPointer.java21
-rw-r--r--src/api/java/cvc5/Solver.java61
-rw-r--r--src/api/java/cvc5/Utils.java35
-rw-r--r--src/api/java/genkinds.py.in1
-rw-r--r--src/api/java/jni/cvc5JavaApi.h38
-rw-r--r--src/api/java/jni/cvc5_Solver.cpp63
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);
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback