WIP: Migrating OCaml binding to CMake (#7254)

* Update doc for `mk_context`. * Migrating to cmake. * Migrating to cmake. It builds both internal or external libz3. * Start to work on platform-specific problem. * Messy notes. * debug. * Cleanup a bit. * Fixing shared lib extension. * Minor. * Resume working on this PR. * Remove including `AddOCaml`. * Keep `z3.ml` and `z3.mli` in the src but specify the generated file in the bin. * Keep `ml_example.ml` in the src. * Try github action for ocaml. * Add workflow using matrix. * Fix mac linking once more. * Bypass @rpath in building sanity check.
2025-04-20 23:56:37 +00:00 · 2025-04-19 16:41:27 -04:00 · 2025-04-19 16:41:27 -04:00 · f7aec02503
parent ab9f3307d6
commit f7aec02503
8 changed files with 1104 additions and 3 deletions
--- a/.github/workflows/ocaml-all.yaml
+++ 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
--- a/.github/workflows/ocaml.yaml
+++ 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
--- 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.
--- a/cmake/modules/FindOCaml.cmake
+++ 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()
--- a/400
+++ b/400
@ -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
+# )
--- 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
 ################################################################################
--- a/src/api/ml/CMakeLists.txt
+++ 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<pkg>.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 "$<TARGET_FILE:libz3>" "$<TARGET_FILE:libz3>"
+    COMMAND install_name_tool -change "@rpath/libz3.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.dylib" "$<TARGET_FILE:libz3>" "${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()
--- 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