###############################################################################
# Top contributors (to current version):
-# Mathias Preiner
+# Mathias Preiner, Mudathir Mohamed
#
# This file is part of the cvc5 project.
#
# #############################################################################
#
# 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
# 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
--- /dev/null
+/******************************************************************************
+ * 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);
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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);
+ }
+}
--- /dev/null
+/******************************************************************************
+ * 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();
+}
--- /dev/null
+/******************************************************************************
+ * 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;
+}
--- /dev/null
+
+/******************************************************************************
+ * 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");
+ }
+}
import re
+
# get access to cvc5/src/api/parsekinds.py
sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api'))
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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);
+}
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()
--- /dev/null
+###############################################################################
+# 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
--- /dev/null
+/******************************************************************************
+ * 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"));
+ }
+}
projects / cvc5.git / commitdiff