diff --git a/.github/workflows/ocaml-all.yaml b/.github/workflows/ocaml-all.yaml new file mode 100644 index 000000000..c225666c1 --- /dev/null +++ b/.github/workflows/ocaml-all.yaml @@ -0,0 +1,125 @@ +name: OCaml Binding CI (Ubuntu + macOS) + +on: + push: + branches: [ "**" ] + pull_request: + branches: [ "**" ] + +jobs: + build-test: + strategy: + matrix: + os: [ ubuntu-latest, macos-latest] + ocaml-version: ["5"] + fail-fast: false + runs-on: ${{ matrix.os }} + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + # Cache ccache (shared across runs) + - name: Cache ccache + uses: actions/cache@v4 + with: + path: ~/.ccache + key: ${{ runner.os }}-ccache-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-ccache- + + # Cache opam (compiler + packages) + - name: Cache opam + uses: actions/cache@v4 + with: + path: ~/.opam + key: ${{ runner.os }}-opam-${{ matrix.ocaml-version }}-${{ github.sha }} + restore-keys: | + ${{ runner.os }}-opam-${{ matrix.ocaml-version }}- + + # Setup OCaml via action + - uses: ocaml/setup-ocaml@v3 + with: + ocaml-compiler: ${{ matrix.ocaml-version }} + opam-disable-sandboxing: true + + # Platform-specific dependencies + - name: Install system dependencies (Ubuntu) + if: matrix.os == 'ubuntu-latest' + run: | + sudo apt-get update + sudo apt-get install -y \ + bubblewrap m4 libgmp-dev pkg-config ninja-build ccache + + - name: Install system dependencies (macOS) + if: matrix.os == 'macos-latest' + run: | + brew install gmp pkg-config ninja ccache + + - name: Install required opam packages + run: opam install -y ocamlfind zarith + + # Configure + - name: Configure with CMake + env: + RUNNER_OS: ${{ runner.os }} + CC: ${{ matrix.os == 'macos-latest' && 'ccache clang' || 'ccache gcc' }} + CXX: ${{ matrix.os == 'macos-latest' && 'ccache clang++' || 'ccache g++' }} + run: | + mkdir -p build + cd build + eval $(opam env) + echo "CC: $CC" + echo "CXX: $CXX" + echo "OCAMLFIND: $(which ocamlfind)" + echo "OCAMLC: $(which ocamlc)" + echo "OCAMLOPT: $(which ocamlopt)" + echo "OCAML_VERSION: $(ocamlc -version)" + echo "OCAMLLIB: $OCAMLLIB" + env | grep OCAML + cmake .. \ + -G Ninja \ + -DZ3_BUILD_LIBZ3_SHARED=ON \ + -DZ3_BUILD_OCAML_BINDINGS=ON \ + -DZ3_BUILD_JAVA_BINDINGS=OFF \ + -DZ3_BUILD_PYTHON_BINDINGS=OFF \ + -DZ3_BUILD_CLI=OFF \ + -DZ3_BUILD_TEST_EXECUTABLES=OFF \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE + + - name: Build Z3 and OCaml bindings + run: | + ccache -z || true + eval $(opam env) + cd build + ninja build_z3_ocaml_bindings + ccache -s || true + + - name: Compile ml_example.byte + run: | + eval $(opam env) + ocamlfind ocamlc -o ml_example.byte \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + -dllpath build/src/api/ml \ + build/src/api/ml/z3ml.cma \ + examples/ml/ml_example.ml + + - name: Run ml_example.byte + run: | + eval $(opam env) + ocamlrun ./ml_example.byte + + - name: Compile ml_example (native) + run: | + eval $(opam env) + ocamlfind ocamlopt -o ml_example \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + build/src/api/ml/z3ml.cmxa \ + examples/ml/ml_example.ml + + - name: Run ml_example (native) + run: ./ml_example \ No newline at end of file diff --git a/.github/workflows/ocaml.yaml b/.github/workflows/ocaml.yaml new file mode 100644 index 000000000..d8b64b992 --- /dev/null +++ b/.github/workflows/ocaml.yaml @@ -0,0 +1,99 @@ +name: OCaml Binding CI (Ubuntu) + +on: + push: + branches: [ "**" ] + pull_request: + branches: [ "**" ] + +jobs: + build-test-ocaml: + runs-on: ubuntu-latest + + steps: + - name: Checkout code + uses: actions/checkout@v4 + + - name: Cache ccache + uses: actions/cache@v4 + with: + path: ~/.ccache + key: ${{ runner.os }}-ccache-${{ github.ref }} + restore-keys: | + ${{ runner.os }}-ccache- + + - name: Install system dependencies + run: | + sudo apt-get update + sudo apt-get install -y \ + opam bubblewrap m4 \ + libgmp-dev pkg-config \ + ninja-build ccache + + - name: Init opam (no sandbox, no default switch) + run: | + opam init --bare --no-setup --disable-sandboxing + opam switch create 5.3.0 + eval $(opam env) + opam install -y ocamlfind zarith + eval $(opam env) + + - name: Configure with CMake + run: | + eval $(opam env) + export CC="ccache gcc" + export CXX="ccache g++" + mkdir -p build + cd build + cmake .. \ + -G Ninja \ + -DZ3_BUILD_LIBZ3_SHARED=ON \ + -DZ3_BUILD_OCAML_BINDINGS=ON \ + -DZ3_BUILD_JAVA_BINDINGS=OFF \ + -DZ3_BUILD_PYTHON_BINDINGS=OFF \ + -DZ3_BUILD_CLI=OFF \ + -DZ3_BUILD_TEST_EXECUTABLES=OFF \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE + + - name: Build Z3 and OCaml bindings + run: | + eval $(opam env) + export CC="ccache gcc" + export CXX="ccache g++" + ocamlc -version + ccache -z # reset stats + cd build + ninja build_z3_ocaml_bindings + ccache -s # show stats + + - name: Compile ml_example.byte + run: | + eval $(opam env) + ocamlc -version + ocamlfind ocamlc -o ml_example.byte \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + -dllpath build/src/api/ml \ + build/src/api/ml/z3ml.cma \ + examples/ml/ml_example.ml + + - name: Run ml_example.byte + run: | + eval $(opam env) + ocamlrun ./ml_example.byte + + - name: Compile ml_example (native) + run: | + eval $(opam env) + ocamlopt -version + ocamlfind ocamlopt -o ml_example \ + -package zarith \ + -linkpkg \ + -I build/src/api/ml \ + build/src/api/ml/z3ml.cmxa \ + examples/ml/ml_example.ml + + - name: Run ml_example (native) + run: | + ./ml_example diff --git a/README-CMake.md b/README-CMake.md index c004f5c7c..dc1f33ec6 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -292,6 +292,9 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings. * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. +* ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built. +* ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built. +* ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings. * ``Z3_INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. * ``Z3_INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. * ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. diff --git a/cmake/modules/FindOCaml.cmake b/cmake/modules/FindOCaml.cmake new file mode 100644 index 000000000..a1bbcd228 --- /dev/null +++ b/cmake/modules/FindOCaml.cmake @@ -0,0 +1,106 @@ +# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/FindOCaml.cmake +# Modified by arbipher at 05/2024 +# +# CMake find_package() module for the OCaml language. +# Assumes ocamlfind will be used for compilation. +# http://ocaml.org/ +# +# Example usage: +# +# find_package(OCaml) +# +# If successful, the following variables will be defined: +# OCAMLFIND +# OCAML_VERSION +# OCAML_STDLIB_PATH +# HAVE_OCAMLOPT +# +# Also provides find_ocamlfind_package() macro. +# +# Example usage: +# +# find_ocamlfind_package(ctypes) +# +# In any case, the following variables are defined: +# +# HAVE_OCAML_${pkg} +# +# If successful, the following variables will be defined: +# +# OCAML_${pkg}_VERSION + +include( FindPackageHandleStandardArgs ) + +find_program(OCAMLFIND + NAMES ocamlfind) + +if( OCAMLFIND ) + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_VARIABLE OCAML_VERSION + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -where + OUTPUT_VARIABLE OCAML_STDLIB_PATH + OUTPUT_STRIP_TRAILING_WHITESPACE) + + execute_process( + COMMAND ${OCAMLFIND} ocamlc -version + OUTPUT_QUIET + RESULT_VARIABLE find_ocaml_result) + if( find_ocaml_result EQUAL 0 ) + set(HAVE_OCAMLOPT TRUE) + else() + set(HAVE_OCAMLOPT FALSE) + endif() +endif() + +find_package_handle_standard_args( OCaml DEFAULT_MSG + OCAMLFIND + OCAML_VERSION + OCAML_STDLIB_PATH) + +mark_as_advanced( + OCAMLFIND) + +function(find_ocamlfind_package pkg) + CMAKE_PARSE_ARGUMENTS(ARG "OPTIONAL" "VERSION" "" ${ARGN}) + + execute_process( + COMMAND "${OCAMLFIND}" "query" "${pkg}" "-format" "%v" + RESULT_VARIABLE result + OUTPUT_VARIABLE version + ERROR_VARIABLE error + OUTPUT_STRIP_TRAILING_WHITESPACE + ERROR_STRIP_TRAILING_WHITESPACE) + + if( NOT result EQUAL 0 AND NOT ARG_OPTIONAL ) + message(FATAL_ERROR ${error}) + endif() + + if( result EQUAL 0 ) + set(found TRUE) + else() + set(found FALSE) + endif() + + if( found AND ARG_VERSION ) + if( version VERSION_LESS ARG_VERSION AND ARG_OPTIONAL ) + # If it's optional and the constraint is not satisfied, pretend + # it wasn't found. + set(found FALSE) + elseif( version VERSION_LESS ARG_VERSION ) + message(FATAL_ERROR + "ocamlfind package ${pkg} should have version ${ARG_VERSION} or newer") + endif() + endif() + + string(TOUPPER ${pkg} pkg) + + set(HAVE_OCAML_${pkg} ${found} + PARENT_SCOPE) + + set(OCAML_${pkg}_VERSION ${version} + PARENT_SCOPE) +endfunction() diff --git a/makefile b/makefile new file mode 100644 index 000000000..4bce3411d --- /dev/null +++ b/makefile @@ -0,0 +1,400 @@ +# ${PROJECT_SOURCE_DIR}: /vendor/z3 +# ${PROJECT_BINARY_DIR}: /vendor/z3/build +# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml +# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml + +# TODO: add `-bin-annot` to more `ocamlc` +# Question: who will set `CAMLORIGIN` +# - -dllpath $$CAMLORIGIN/../.. \ +# Q: is `ocamlmklib -ldopt -Lfoo` the same as `ocamlmklib -Lfoo` +# it doesn't looks right (item 4) +# https://www.ocaml.org/manual/5.2/runtime.html#s:ocamlrun-dllpath +# +# if external libz3 is given, no files should be build +# +# find_program(OCAMLFIND +# NAMES ocamlfind) +# find_library(ocaml) +# include(FindOCaml) +# Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html +# for rpath, see https://discourse.cmake.org/t/how-to-get-an-lc-rpath-and-rpath-prefix-on-a-dylib-on-macos/5540 + +# Generate ``z3native.ml`` and ``z3native_stubs.c`` + +# set(z3ml_generated_files +# "${z3ml_bin}/z3native.ml" +# "${z3ml_bin}/z3native_stubs.c" +# "${z3ml_enums_ml}" +# ) + +# add_custom_target(ocaml_generated DEPENDS +# ${z3ml_generated_files} +# ) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3enums.mli" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-i" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3enums.ml" +# ">" "${z3ml_bin}/z3enums.mli" +# DEPENDS "${z3ml_enums_ml}" +# COMMENT "Building z3enums.mli" +# VERBATIM) + +# "-ldopt" +# "-ccopt" "-L\\$CAMLORIGIN/../.." +# "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.." + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3native.cmx" +# COMMAND "${OCAMLFIND}" "ocamlopt" +# "-package" "zarith" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3native.ml" +# DEPENDS "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.mli" +# "${z3ml_bin}/z3native.cmi" +# "${z3ml_bin}/z3native.ml" +# COMMENT "Building z3native.cmx" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3enums.cmo" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3enums.ml" +# DEPENDS "${z3ml_enums_ml}" +# COMMENT "Building z3enums.cmo" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3native.mli" +# COMMAND "${OCAMLFIND}" "ocamlc" +# "-package" "zarith" +# "-i" +# "-I" "${z3ml_bin}" +# "-c" "${z3ml_bin}/z3native.ml" +# ">" "${z3ml_bin}/z3native.mli" +# DEPENDS "${z3ml_enums_ml}" +# "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.ml" +# COMMENT "Building z3native.mli" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3.cmx" +# COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} +# "-c" "${z3ml_bin}/z3.ml" +# DEPENDS "${z3ml_bin}/z3enums.cmo" +# "${z3ml_bin}/z3native.cmo" +# "${z3ml_bin}/z3.ml" +# "${z3ml_bin}/z3.mli" +# "${z3ml_bin}/z3.cmi" +# COMMENT "Building z3.cmx" +# VERBATIM) + +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3ml.cmxa" +# COMMAND "${OCAMLFIND}" "ocamlmklib" +# "-o" z3ml +# ${ocamlmklib_flags} +# "-I" "${z3ml_bin}" +# "${z3ml_bin}/z3enums.cmx" +# "${z3ml_bin}/z3native.cmx" +# "${z3ml_bin}/z3native_stubs.o" +# "${z3ml_bin}/z3.cmx" +# DEPENDS +# libz3 +# "${z3ml_bin}/z3enums.cmx" +# "${z3ml_bin}/z3native.cmx" +# "${z3ml_bin}/z3native_stubs.o" +# "${z3ml_bin}/z3.cmx" +# COMMENT "Building OCaml library ${name}" +# VERBATIM) +# add_custom_command( +# OUTPUT "${z3ml_bin}/z3ml.cmxs" +# COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" +# "-o" "${z3ml_bin}/z3ml.cmxs" +# "-I" "." +# "-I" "${z3ml_bin}" +# "${z3ml_bin}/z3ml.cmxa" +# DEPENDS +# "${z3ml_bin}/z3ml.cmxa" +# COMMENT "Building OCaml library ${name}" +# VERBATIM) + +# "${z3ml_bin}/z3enums.cmi" + +ML_LIB=/home/ex/.opam/5.2.0/lib +ML_LIB=/Users/ex/.opam/5.2.0/lib +ROOT=$$(pwd) +MY_Z3=/home/ex/my_z3 +MY_Z3=/Users/ex/code/tmp/my-z3 + +ml0: + mkdir -p build + cd build && cmake -G "Ninja" \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + ../ + +# -DGRAPHVIZ_EXECUTABLES=FALSE \ +# -DGRAPHVIZ_INTERFACE_LIBS=FALSE \ +# --graphviz=deps.dot \ + +ml-inner-mk: + mkdir -p build + cd build && cmake \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + -DZ3_BUILD_PYTHON_BINDINGS=TRUE \ + --debug-trycompile \ + ../ + +ml-mk: + mkdir -p build + cd build && cmake \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \ + --debug-trycompile \ + ../ + +ml-inner: + mkdir -p build + cd build && cmake \ + -G "Ninja" \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + --debug-trycompile \ + ../ + +ml: + mkdir -p build + cd build && cmake \ + -G "Ninja" \ + -DCMAKE_VERBOSE_MAKEFILE=TRUE \ + -DZ3_BUILD_LIBZ3_SHARED=TRUE \ + -DZ3_BUILD_OCAML_BINDINGS=TRUE \ + --debug-trycompile \ + ../ + +# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \ +# -DZ3_USE_LIB_GMP=TRUE \ + +# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example + +build-all: + cd build && make -j16 + +build-mk: + cd build && make -j16 build_z3_ocaml_bindings +.PHONY:build + +build-nj: + cd build && ninja +.PHONY:build-nj + +build: + cd build && ninja build_z3_ocaml_bindings +.PHONY:build + +dot: + cd build && dot -Tpng -o deps.png deps.dot + +clean: + rm -rf build + +MKLIB_FLAGS = \ + ocamlfind ocamlmklib \ + -ocamlcflags -bin-annot \ + -package zarith \ + -lz3 -lstdc++ -lpthread\ + -lgmp \ + -L$(ROOT)/build \ + -dllpath $(ROOT)/build \ + -L$(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ + -I build/src/api/ml \ + -o build/src/api/ml/z3ml + +om: + $(MKLIB_FLAGS) \ + build/src/api/ml/z3enums.cmo \ + build/src/api/ml/z3native.cmo \ + build/src/api/ml/z3native_stubs.o \ + build/src/api/ml/z3.cmo + + $(MKLIB_FLAGS) \ + build/src/api/ml/z3enums.cmx \ + build/src/api/ml/z3native.cmx \ + build/src/api/ml/z3native_stubs.o \ + build/src/api/ml/z3.cmx + +# why? +# DEPENDS "${z3ml_bin}/z3enums.cmo" +# -I +threads \ + +or1: + ocamlfind ocamlc -verbose \ + -o ml_example.byte \ + -package zarith \ + -I $(ROOT)/build/src/api/ml \ + -dllpath $(ROOT)/build/src/api/ml \ + -I $(ML_LIB)/stublibs \ + -dllpath $(ML_LIB)/stublibs \ + $(ML_LIB)/zarith/zarith.cma \ + $(ROOT)/build/src/api/ml/z3ml.cma \ + $(ROOT)/build/src/api/ml/ml_example.ml \ + +# -linkpkg \ + +or2: + ocamlrun ml_example.byte + +# -I $(ML_LIB)/stublibs \ + # "-cclib" "-L${PROJECT_BINARY_DIR}" + # "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + # "-linkpkg" +# "-cclib" "-L${PROJECT_BINARY_DIR}" +# "-cclib" [[-L. -lpthread -lstdc++ -lz3]] + +# -I +threads \ + +oc1: + ocamlfind ocamlopt \ + -o ml_example \ + -package zarith \ + -linkpkg \ + -I $(ROOT)/build/src/api/ml \ + z3ml.cmxa \ + $(ROOT)/build/src/api/ml/ml_example.ml + +oc2: + ./ml_example + +# must have +# $(ML_LIB)/zarith/zarith.cma +# -I $(ROOT)/build/src/api/ml + +# can be removed +# -cclib "-lstdc++ -lz3" +# -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith " +# -L$(ROOT)/build +# -package zarith +# -linkpkg +# -lpthread +# -package z3 +# -I $(ML_LIB)/zarith + +# must not have +# -custom + +# -o $(ROOT)/build/src/api/ml/ml_example.byte + +# CAML_LD_LIBRARY_PATH=$(ML_LIB)/stublibs:$(ROOT)/build:$(ROOT)/build/src/api/ml:$(ML_LIB)/zarith + +or3: + ocamlrun -I $(ML_LIB)/zarith -I $(ML_LIB)/stublibs -I $(ML_LIB)/zarith ml_example.byte + +# -I $(ML_LIB)/zarith +# -I $(ML_LIB)/stublibs +# -I $(ROOT)/build +# -I $(ROOT)/build/src/api/ml +# -t -b + + +# -cclib "-L. -lpthread -lstdc++ -lz3" + +# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"") +#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}" + +# Link libz3 into the python directory so bindings work out of the box +# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" +# "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}" +# DEPENDS libz3 +# COMMENT "Linking libz3 into python directory" +# ) + +# add_ocaml_library(z3ml +# OCAML z3enums z3native z3 +# # OCAMLDEP llvm +# PKG zarith +# C z3native_stubs +# CFLAGS "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)" +# GEN "${OCAML_GENERATED_FILES}" +# # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm +# # LLVM IRReader) +# ) + + +# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api") +# target_sources(z3ml PRIVATE +# z3native_stubs.h +# ${z3_c_api_path}) + + +# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}") +# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}") + +# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}") +# target_sources(ocaml_z3 +# PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE}) + +# target_include_directories(ocaml_z3 +# PUBLIC ${CMAKE_CURRENT_BINARY_DIR} +# ) + +# add_custom_target (LibCoreBC DEPENDS libcore.bc) + +# target_sources(src/api/ml/z3natives_stubs.c +# PUBLIC Z3_OCAML_NATIVE_STUB_FILE) + +# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS +# ${Z3_OCAML_NATIVE_STUB_PRE_FILE}) + +# target_precompile_headers( +# ocaml_z3 PRIVATE +# z3native_stubs.h +# ) + +# target_sources(ocaml_z3 PRIVATE +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml" +# "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c") + +# add_dependencies(ocaml_z3 +# "${PROJECT_SOURCE_DIR}/src/api" +# "${PROJECT_BINARY_DIR}/src/api" +# ) + +# find_package(OCaml) +# message("DDDebug ${OCAMLFIND}") +# message("DDDebug ${pkg}") +# find_ocamlfind_package(ctypes) +# # find_ocamlfind_package("nonexist") +# message(small " ${HAVE_OCAML_ctype}") +# message(caps " ${HAVE_OCAML_CTYPES}") +# message(small " ${OCAML_ctype_VERSION}") +# message(caps " ${OCAML_CTYPES_VERSION}") +# find_package(ocaml REQUIRED) + +# add_custom_target(ocaml_post_z3enums DEPENDS +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo" +# "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx" +# ) +# add_custom_target(z3.ml DEPENDS +# ocaml_post_z3enums +# ) +# add_custom_target(z3native.ml DEPENDS +# ocaml_post_z3enums +# ) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5faede21f..071436200 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -299,6 +299,18 @@ if (Z3_BUILD_JAVA_BINDINGS) add_subdirectory(api/java) endif() +################################################################################ +# OCaml bindings +################################################################################ +option(Z3_BUILD_OCAML_BINDINGS "Build OCaml bindings for Z3" OFF) +if (Z3_BUILD_OCAML_BINDINGS) + if (NOT Z3_BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The OCaml bindings will not work with a static libz3. " + "You either need to disable Z3_BUILD_OCAML_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED") + endif() + add_subdirectory(api/ml) +endif() + ################################################################################ # Julia bindings ################################################################################ diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt new file mode 100644 index 000000000..e3f3168ad --- /dev/null +++ b/src/api/ml/CMakeLists.txt @@ -0,0 +1,330 @@ +find_package(OCaml REQUIRED) + +set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX}) +set(so_ext ${CMAKE_SHARED_LIBRARY_SUFFIX}) +set(bc_ext ".byte") + +set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR}) +set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR}) + +if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3) + add_custom_target(libz3_z3ml + ALL + DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext} + ) + set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}) +else() + add_custom_target(libz3_z3ml + ALL + DEPENDS libz3 + ) + set(libz3_path ${PROJECT_BINARY_DIR}) +endif() + +add_custom_command( + OUTPUT + ${z3ml_bin}/z3native.ml + ${z3ml_bin}/z3native_stubs.c + COMMAND "${Python3_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-src-dir" + "${CMAKE_CURRENT_SOURCE_DIR}" + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/update_api.py + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c" + VERBATIM +) + +add_custom_command( + OUTPUT + ${z3ml_bin}/z3enums.ml + COMMAND "${Python3_EXECUTABLE}" + "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--ml-output-dir" + "${CMAKE_CURRENT_BINARY_DIR}" + DEPENDS + ${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + COMMENT "Generating ${z3ml_bin}/z3enums.ml" + VERBATIM +) + + +set(z3ml_common_flags "-package" "zarith" + "-I" "${z3ml_bin}") + + # add_custom_command( +# OUTPUT ${z3ml_bin}/z3.ml +# ${z3ml_bin}/z3.mli +# COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml" +# COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli" +# DEPENDS ${z3ml_src}/z3.ml +# ${z3ml_src}/z3.mli +# COMMENT "Copying z3.ml and z3.mli to build area") + +# z3native_stubs.c depends on nothing +execute_process( + COMMAND ${OCAMLFIND} ocamlc "-where" + OUTPUT_VARIABLE ocaml_stub_lib_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +add_custom_command( + OUTPUT ${z3ml_bin}/z3native_stubs.o + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3native_stubs.o" + "-I" "${z3ml_src}" + "-I" "${PROJECT_SOURCE_DIR}/src/api" + "-I" "${ocaml_stub_lib_path}" + "-c" "${z3ml_bin}/z3native_stubs.c" + DEPENDS ${z3ml_bin}/z3native_stubs.c + COMMENT "Building z3native_stubs.o" + VERBATIM) + +message(STATUS "PATH: $ENV{PATH}") +message(STATUS "OCAMLFIND: $ENV{OCAMLFIND}") + +# z3enum.ml depends on nothing +add_custom_command( + OUTPUT ${z3ml_bin}/z3enums.mli + ${z3ml_bin}/z3enums.cmi + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3enums.cmx + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3enums.ml" + ">" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3enums.ml" + DEPENDS ${z3ml_bin}/z3enums.ml + COMMENT "Building z3enums.{mli,cmi,cmo,cmx}" + VERBATIM) + +# z3native.ml depends on z3enums +add_custom_command( + OUTPUT ${z3ml_bin}/z3native.mli + ${z3ml_bin}/z3native.cmi + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3native.cmx + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-i" + "-c" "${z3ml_bin}/z3native.ml" + ">" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.mli" + COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.ml" + COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-c" "${z3ml_bin}/z3native.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.ml + COMMENT "Building z3native.{mli,cmi,cmo,cmx}" + VERBATIM) + +# z3.ml depends on z3enums and z3native +add_custom_command( + OUTPUT ${z3ml_bin}/z3.cmi + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3.cmx + # COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.mli" + # COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.ml" + # COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + # "-c" "${z3ml_bin}/z3.ml" +COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmi" + "-c" "${z3ml_src}/z3.mli" +COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmo" + "-c" "${z3ml_src}/z3.ml" +COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags} + "-o" "${z3ml_bin}/z3.cmx" + "-c" "${z3ml_src}/z3.ml" + DEPENDS ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + # ${z3ml_bin}/z3.ml + # ${z3ml_bin}/z3.mli + ${z3ml_src}/z3.ml + ${z3ml_src}/z3.mli + COMMENT "Building z3.cmo" + VERBATIM) + +# making ocaml stublibs +execute_process( + COMMAND ${OCAMLFIND} printconf destdir + OUTPUT_VARIABLE ocaml_destdir_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs") + +set(c_lib_deps "-L${libz3_path}" "-lz3" "-lstdc++" "-lpthread") +if (Z3_USE_LIB_GMP) + list(APPEND c_lib_deps "-lgmp") +endif() + +if( APPLE ) + # set(ocaml_rpath "@executable_path/../libz3${so_ext}") +elseif( UNIX ) + set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}") + list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath}) +endif() + +# We may not directly use CMake's BUILD_RPATH or INSTALL_RPATH since they don't set +# the ocaml stub libraries as a normal library target. + +set(ocamlmklib_flags "-o" "z3ml" + "-ocamlcflags" "-bin-annot" + "-package" "zarith" + ${c_lib_deps} + "-dllpath" "${libz3_path}" + "-L${ocaml_stublibs_path}" + "-dllpath" "${ocaml_stublibs_path}" + "-dllpath" "@rpath/dllz3ml.so" + "-I" "${z3ml_bin}") + +# OCaml's dll stublib hava platform-independent name `dll.so` + +add_custom_command( + OUTPUT ${z3ml_bin}/dllz3ml.so + ${z3ml_bin}/libz3ml.a + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmo" + "${z3ml_bin}/z3native.cmo" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmo" + COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags} + "${z3ml_bin}/z3enums.cmx" + "${z3ml_bin}/z3native.cmx" + "${z3ml_bin}/z3native_stubs.o" + "${z3ml_bin}/z3.cmx" + COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared" + "-o" "${z3ml_bin}/z3ml.cmxs" + "-I" "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + DEPENDS + libz3_z3ml + ${z3ml_bin}/z3native_stubs.o + ${z3ml_bin}/z3enums.cmo + ${z3ml_bin}/z3native.cmo + ${z3ml_bin}/z3.cmo + ${z3ml_bin}/z3enums.cmx + ${z3ml_bin}/z3native.cmx + ${z3ml_bin}/z3.cmx + COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a" + VERBATIM) + +############################################################################### +# Example +############################################################################### + +execute_process( + COMMAND ${OCAMLFIND} query zarith + OUTPUT_VARIABLE ocaml_pkg_zarith_path + OUTPUT_STRIP_TRAILING_WHITESPACE) + +# Always define patch_z3ml_dylib for dependency consistency +if(APPLE) + add_custom_command( + OUTPUT ${z3ml_bin}/patched_dllz3ml + COMMAND install_name_tool -id "$" "$" + COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$" "${z3ml_bin}/dllz3ml.so" + COMMAND touch ${z3ml_bin}/patched_dllz3ml + DEPENDS ${z3ml_bin}/dllz3ml.so + COMMENT "Patch install name and reference for macOS" + VERBATIM + ) +else() + add_custom_command( + OUTPUT ${z3ml_bin}/patched_dllz3ml + COMMAND ${CMAKE_COMMAND} -E touch ${z3ml_bin}/patched_dllz3ml + COMMENT "Dummy patch target for non-macOS" + VERBATIM + ) +endif() + +add_custom_target(patch_z3ml_dylib ALL + DEPENDS ${z3ml_bin}/patched_dllz3ml) + +add_custom_target(build_z3_ocaml_bindings + ALL + DEPENDS + ${z3ml_bin}/z3ml.cma + ${z3ml_bin}/z3ml.cmxa + ${z3ml_bin}/z3ml.cmxs + ${z3ml_bin}/dllz3ml.so + ${z3ml_bin}/libz3ml.a + patch_z3ml_dylib +) + +# test + +set(z3ml_example_src ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml) + +add_custom_command( + TARGET build_z3_ocaml_bindings POST_BUILD + COMMAND "${OCAMLFIND}" ocamlc + -o "${z3ml_bin}/ml_example.byte" + -package zarith + -linkpkg + -I "${z3ml_bin}" + -dllpath "${z3ml_bin}" + "${z3ml_bin}/z3ml.cma" + "${z3ml_example_src}" + COMMAND ocamlrun "${z3ml_bin}/ml_example.byte" > "${z3ml_bin}/ml_example.bc.log" + COMMENT "Run OCaml bytecode example" + VERBATIM +) + +add_custom_command( + TARGET build_z3_ocaml_bindings POST_BUILD + COMMAND "${OCAMLFIND}" ocamlopt + -o "${z3ml_bin}/ml_example" + -package zarith + -linkpkg + -I "${z3ml_bin}" + "${z3ml_bin}/z3ml.cmxa" + "${z3ml_example_src}" + COMMAND "${z3ml_bin}/ml_example" > "${z3ml_bin}/ml_example.log" + COMMENT "Run OCaml native example" + VERBATIM +) + +############################################################################### +# Install +############################################################################### + +# Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace. +# I don't know how to use conditional `COMMAND` nor specify a file dependency for itself +# Renaming it and back seems a simple solution. + +# COMMAND mv "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/dllz3ml.pre.so" +# if (NOT APPLE) +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}" +# DEPENDS "${z3ml_bin}/dllz3ml.pre.so" +# ) +# else() +# # if IS_OSX: +# # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib +# # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so +# add_custom_command( +# OUTPUT "${z3ml_bin}/dllz3ml.so" +# COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so" +# DEPENDS "${z3ml_bin}/dllz3ml.so" +# ) +# endif() \ No newline at end of file diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 5320fc38e..0b31874e1 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -42,9 +42,10 @@ type context - timeout (unsigned) default timeout (in milliseconds) used for solvers - well_sorted_check type checker - auto_config use heuristics to automatically select solver and configure it - - model model generation for solvers, this parameter can be overwritten when creating a solver - - model_validate validate models produced by solvers - - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - model (Boolean) model generation for solvers, this parameter can be overwritten when creating a solver + - model_validate (Boolean) validate models produced by solvers + - unsat_core (Boolean) unsat-core generation for solvers, this parameter can be overwritten when creating a solver + - encoding the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit) *) val mk_context : (string * string) list -> context @@ -3712,6 +3713,31 @@ end For example: (set_global_param "pp.decimal" "true") will set the parameter "decimal" in the module "pp" to true. + + Legal parameters are: + auto_config (bool) (default: true) + debug_ref_count (bool) (default: false) + dot_proof_file (string) (default: proof.dot) + dump_models (bool) (default: false) + encoding (string) (default: unicode) + memory_high_watermark (unsigned int) (default: 0) + memory_high_watermark_mb (unsigned int) (default: 0) + memory_max_alloc_count (unsigned int) (default: 0) + memory_max_size (unsigned int) (default: 0) + model (bool) (default: true) + model_validate (bool) (default: false) + proof (bool) (default: false) + rlimit (unsigned int) (default: 0) + smtlib2_compliant (bool) (default: false) + stats (bool) (default: false) + timeout (unsigned int) (default: 4294967295) + trace (bool) (default: false) + trace_file_name (string) (default: z3.log) + type_check (bool) (default: true) + unsat_core (bool) (default: false) + verbose (unsigned int) (default: 0) + warning (bool) (default: true) + well_sorted_check (bool) (default: false) *) val set_global_param : string -> string -> unit