CMakeLists.txt

find_package(Java REQUIRED)
find_package(JNI REQUIRED)
include(UseJava)

# Sanity check for dirty source tree
foreach (file_name "enumerations" "Native.cpp" "Native.java")
  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
            ${z3_polluted_tree_msg})
  endif()
endforeach()

set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")

# Rule to generate ``Native.java`` and ``Native.cpp``
set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
  COMMAND "${Python3_EXECUTABLE}"
    "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
    "--java-input-dir"
    "${CMAKE_CURRENT_SOURCE_DIR}"
    "--java-output-dir"
    "${CMAKE_CURRENT_BINARY_DIR}"
    "--java-package-name"
    ${Z3_JAVA_PACKAGE_NAME}
  DEPENDS
    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
    "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
  COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
  USES_TERMINAL
)

# Add rule to build native code that provides a bridge between
# ``Native.java`` and libz3's interfac3.
add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
target_link_libraries(z3java PRIVATE libz3)
# FIXME:
# Not sure if using all the flags used by the Z3 components is really necessary
# here. The Python build system uses all the flags used for building
# Z3's components to build ``Native.cpp`` lets do the same for now.
target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
target_include_directories(z3java PRIVATE
  "${PROJECT_SOURCE_DIR}/src/api"
  "${PROJECT_BINARY_DIR}/src/api"
  ${JNI_INCLUDE_DIRS}
)
# FIXME: Should this library have SONAME and VERSION set?

# This prevents CMake from automatically defining ``z3java_EXPORTS``
set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")

# Rule to generate the ``com.microsoft.z3.enumerations`` package
# FIXME: This list of files is fragile
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
  Z3_ast_kind.java
  Z3_ast_print_mode.java
  Z3_decl_kind.java
  Z3_error_code.java
  Z3_goal_prec.java
  Z3_lbool.java
  Z3_param_kind.java
  Z3_parameter_kind.java
  Z3_sort_kind.java
  Z3_symbol_kind.java
)
set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
  list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
    "${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
  )
endforeach()
add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
  COMMAND "${Python3_EXECUTABLE}"
    "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
    "--java-output-dir"
    "${CMAKE_CURRENT_BINARY_DIR}"
    "--java-package-name"
    ${Z3_JAVA_PACKAGE_NAME}
  DEPENDS
    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
    "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
  COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
  USES_TERMINAL
)

set(Z3_JAVA_JAR_SOURCE_FILES
  AlgebraicNum.java
  ApplyResultDecRefQueue.java
  ApplyResult.java
  ArithExpr.java
  ArithSort.java
  ArrayExpr.java
  ArraySort.java
  ASTDecRefQueue.java
  AST.java
  AstMapDecRefQueue.java
  ASTMap.java
  AstVectorDecRefQueue.java
  ASTVector.java
  BitVecExpr.java
  BitVecNum.java
  BitVecSort.java
  BoolExpr.java
  BoolSort.java
  CharSort.java
  ConstructorDecRefQueue.java
  Constructor.java
  ConstructorListDecRefQueue.java
  ConstructorList.java
  Context.java
  DatatypeExpr.java
  DatatypeSort.java
  EnumSort.java
  Expr.java
  FiniteDomainExpr.java
  FiniteDomainNum.java
  FiniteDomainSort.java
  FixedpointDecRefQueue.java
  Fixedpoint.java
  FPExpr.java
  FPNum.java
  FPRMExpr.java
  FPRMNum.java
  FPRMSort.java
  FPSort.java
  FuncDecl.java
  FuncInterpDecRefQueue.java
  FuncInterpEntryDecRefQueue.java
  FuncInterp.java
  Global.java
  GoalDecRefQueue.java
  Goal.java
  IDecRefQueue.java
  IntExpr.java
  IntNum.java
  IntSort.java
  IntSymbol.java
  Lambda.java
  ListSort.java
  Log.java
  ModelDecRefQueue.java
  Model.java
  OptimizeDecRefQueue.java
  Optimize.java
  ParamDescrsDecRefQueue.java
  ParamDescrs.java
  ParamsDecRefQueue.java
  Params.java
  Pattern.java
  ProbeDecRefQueue.java
  Probe.java
  Quantifier.java
  RatNum.java
  RealExpr.java
  RealSort.java
  ReExpr.java
  RelationSort.java
  ReSort.java
  SeqExpr.java
  SeqSort.java
  SetSort.java
  Simplifier.java
  SimplifierDecRefQueue.java
  SolverDecRefQueue.java
  Solver.java
  Sort.java
  StatisticsDecRefQueue.java
  Statistics.java
  Status.java
  StringSymbol.java
  Symbol.java
  TacticDecRefQueue.java
  Tactic.java
  TupleSort.java
  UninterpretedSort.java
  UserPropagatorBase.java
  Version.java
  Z3Exception.java
  Z3Object.java
)
set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
  list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
endforeach()
# Add generated files to list
list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
  ${Z3_JAVA_NATIVE_JAVA}
  ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
)

# Convenient top-level target
add_custom_target(build_z3_java_bindings
  ALL
  DEPENDS
    z3java
    z3JavaJar
)

# Rule to build ``com.microsoft.z3.jar``
# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
add_jar(z3JavaJar
  SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
  OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
  OUTPUT_DIR "${PROJECT_BINARY_DIR}"
  VERSION "${Z3_VERSION}"
)

###############################################################################
# Install
###############################################################################
option(Z3_INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
if (Z3_INSTALL_JAVA_BINDINGS)
  # Provide cache variables for the install locations that the user can change.
  # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
  # files on Linux distributions
  set(Z3_JAVA_JAR_INSTALLDIR
    "${CMAKE_INSTALL_DATAROOTDIR}/java"
    CACHE
    PATH
    "Directory to install Z3 Java jar file relative to install prefix"
  )
  # FIXME: I don't think this the right installation location
  set(Z3_JAVA_JNI_LIB_INSTALLDIR
    "${CMAKE_INSTALL_LIBDIR}"
    CACHE
    PATH
    "Directory to install Z3 Java JNI bridge library relative to install prefix"
  )
  install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
  # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
  # with CMake 2.8.12.2 handles that incorrectly.
  install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
endif()