mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Merge 4b3207505b into 8d81a2dcaf

Browse source
This commit is contained in:
Shiwei Weng 翁士伟 2025-03-29 17:57:30 +00:00 committed by GitHub
parent 8d81a2dcaf 4b3207505b
commit f22e6af344
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 1140 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
README-CMake.md
View file

@ -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.

269
cmake/modules/AddOCaml.cmake Normal file
View file

@ -0,0 +1,269 @@
# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/AddOCaml.cmake
# Modified by arbipher at 05/2024
#
# CMake build rules for the OCaml language.
# Assumes FindOCaml is used.
# http://ocaml.org/
#
# Example usage:
#
# add_ocaml_library(pkg_a OCAML mod_a OCAMLDEP pkg_b C mod_a_stubs PKG ctypes LLVM core)
#
# Unnamed parameters:
#
# * Library name.
#
# Named parameters:
#
# OCAML OCaml module names. Imply presence of a corresponding .ml and .mli files.
# OCAMLDEP Names of libraries this library depends on.
# C C stub sources. Imply presence of a corresponding .c file.
# INCLUDES Path for header files for C sources.
# CFLAGS Additional arguments passed when compiling C stubs.
# PKG Names of ocamlfind packages this library depends on.
# LLVM Names of LLVM libraries this library depends on.
# GEN Generated files. Do not need to copy.
# NOCOPY Do not automatically copy sources (.c, .ml, .mli) from the source directory,
# e.g. if they are generated.
#
function(add_ocaml_library name)
## Argument Setting ##
# CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;LLVM" ${ARGN})
CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;GEN" ${ARGN})
set(src ${CMAKE_CURRENT_SOURCE_DIR})
set(bin ${CMAKE_CURRENT_BINARY_DIR})
# TODO: incorrect
set(ocaml_pkgs)
foreach( ocaml_pkg ${ARG_PKG} )
list(APPEND ocaml_pkgs "-package" "${ocaml_pkg}")
endforeach()
set(sources)
set(ocaml_inputs)
set(ocaml_outputs "${bin}/${name}.cma")
if( ARG_C )
list(APPEND ocaml_outputs
"${bin}/lib${name}${CMAKE_STATIC_LIBRARY_SUFFIX}")
if ( BUILD_SHARED_LIBS )
list(APPEND ocaml_outputs
"${bin}/dll${name}${CMAKE_SHARED_LIBRARY_SUFFIX}")
endif()
endif()
if( HAVE_OCAMLOPT )
list(APPEND ocaml_outputs
"${bin}/${name}.cmxa"
"${bin}/${name}${CMAKE_STATIC_LIBRARY_SUFFIX}")
endif()
set(ocaml_flags "-lstdc++" "-ldopt" "-L${LLVM_LIBRARY_DIR}"
"-ccopt" "-L\\$CAMLORIGIN/../.."
"-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.."
${ocaml_pkgs})
foreach( ocaml_dep ${ARG_OCAMLDEP} )
get_target_property(dep_ocaml_flags "ocaml_${ocaml_dep}" OCAML_FLAGS)
list(APPEND ocaml_flags ${dep_ocaml_flags})
endforeach()
if( NOT BUILD_SHARED_LIBS )
list(APPEND ocaml_flags "-custom")
endif()
# if(LLVM_LINK_LLVM_DYLIB)
# list(APPEND ocaml_flags "-lLLVM")
# else()
# explicit_map_components_to_libraries(llvm_libs ${ARG_LLVM})
# foreach( llvm_lib ${llvm_libs} )
# list(APPEND ocaml_flags "-l${llvm_lib}" )
# endforeach()
# get_property(system_libs TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS)
# foreach(system_lib ${system_libs})
# if (system_lib MATCHES "^-")
# # If it's an option, pass it without changes.
# list(APPEND ocaml_flags "${system_lib}" )
# else()
# # Otherwise assume it's a library name we need to link with.
# list(APPEND ocaml_flags "-l${system_lib}" )
# endif()
# endforeach()
# endif()
string(REPLACE ";" " " ARG_CFLAGS "${ARG_CFLAGS}")
set(c_flags "${ARG_CFLAGS} ${LLVM_DEFINITIONS}")
foreach( include_dir ${LLVM_INCLUDE_DIR} ${LLVM_MAIN_INCLUDE_DIR} )
set(c_flags "${c_flags} -I${include_dir}")
endforeach()
# include -D/-UNDEBUG to match dump function visibility
# regex from HandleLLVMOptions.cmake
string(REGEX MATCH "(^| )[/-][UD] *NDEBUG($| )" flag_matches
"${CMAKE_C_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_C_FLAGS}")
set(c_flags "${c_flags} ${flag_matches}")
foreach( ocaml_file ${ARG_OCAML} )
if (EXISTS "${bin}/${ocaml_file}.mli")
list(APPEND sources "${ocaml_file}.mli")
else()
add_custom_command(
OUTPUT "${bin}/${ocaml_file}.mli"
COMMAND "${OCAMLFIND}" "ocamlc" "${ocaml_pkgs}" "-i" "-I" "${bin}" "-c" "${bin}/${ocaml_file}.ml" ">" "${bin}/${ocaml_file}.mli"
DEPENDS "${bin}/${ocaml_file}.ml"
COMMENT "Building OCaml mli file if non-exist"
VERBATIM)
endif()
list(APPEND sources "${ocaml_file}.ml")
list(APPEND ocaml_inputs "${bin}/${ocaml_file}.mli" "${bin}/${ocaml_file}.ml")
list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmi" "${bin}/${ocaml_file}.cmo")
list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmti" "${bin}/${ocaml_file}.cmt")
if( HAVE_OCAMLOPT )
list(APPEND ocaml_outputs
"${bin}/${ocaml_file}.cmx"
# "${bin}/${ocaml_file}.o"
)
endif()
endforeach()
## Compiling ML files ##
foreach( c_file ${ARG_C} )
list(APPEND sources "${c_file}.c")
list(APPEND c_inputs "${bin}/${c_file}.c")
list(APPEND c_outputs "${bin}/${c_file}.o")
endforeach()
if( NOT ARG_NOCOPY )
foreach( source ${sources} )
if (NOT "${bin}/${source}" IN_LIST ARG_GEN)
add_custom_command(
OUTPUT "${bin}/${source}"
COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${src}/${source}" "${bin}"
DEPENDS "${src}/${source}"
COMMENT "Copying ${source} to build area")
endif()
endforeach()
endif()
## Compiling C Stub ##
foreach( c_input ${c_inputs} )
get_filename_component(basename "${c_input}" NAME_WE)
add_custom_command(
OUTPUT "${bin}/${basename}.o"
COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${bin}/${basename}.o" "-c" "${c_input}" -ccopt ${c_flags}
DEPENDS "${c_input}"
COMMENT "Building OCaml stub object file ${bin}/${basename}.o"
VERBATIM)
endforeach()
## Setting linking argument and run mklib ##
set(ocaml_params)
foreach( ocaml_input ${ocaml_inputs} ${c_outputs})
get_filename_component(filename "${ocaml_input}" NAME)
list(APPEND ocaml_params "${filename}")
endforeach()
if( APPLE )
set(ocaml_rpath "@executable_path/../../../lib${LLVM_LIBDIR_SUFFIX}")
elseif( UNIX )
set(ocaml_rpath "\\$ORIGIN/../../../lib${LLVM_LIBDIR_SUFFIX}")
endif()
list(APPEND ocaml_flags "-ldopt" "-Wl,-rpath,${ocaml_rpath}")
add_custom_command(
OUTPUT ${ocaml_outputs}
COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot"
"-o" "${name}" ${ocaml_flags} ${ocaml_params}
DEPENDS ${ocaml_inputs} ${c_outputs}
COMMENT "Building OCaml library ${name}"
VERBATIM)
## Build document
add_custom_command(
OUTPUT "${bin}/${name}.odoc"
COMMAND "${OCAMLFIND}" "ocamldoc"
"-I" "${bin}"
"-I" "${LLVM_LIBRARY_DIR}/ocaml/llvm/"
"-dump" "${bin}/${name}.odoc"
${ocaml_pkgs} ${ocaml_inputs}
DEPENDS ${ocaml_inputs} ${ocaml_outputs}
COMMENT "Building OCaml documentation for ${name}"
VERBATIM)
add_custom_target("ocaml_${name}" ALL DEPENDS ${ocaml_outputs} "${bin}/${name}.odoc")
set_target_properties("ocaml_${name}" PROPERTIES
OCAML_FLAGS "-I;${bin}")
set_target_properties("ocaml_${name}" PROPERTIES
OCAML_ODOC "${bin}/${name}.odoc")
## Setting dependencies
foreach( ocaml_dep ${ARG_OCAMLDEP} )
add_dependencies("ocaml_${name}" "ocaml_${ocaml_dep}")
endforeach()
if( NOT LLVM_OCAML_OUT_OF_TREE )
foreach( llvm_lib ${llvm_libs} )
add_dependencies("ocaml_${name}" "${llvm_lib}")
endforeach()
endif()
## Configurating installation
set(install_files)
set(install_shlibs)
foreach( ocaml_output ${ocaml_inputs} ${ocaml_outputs} )
get_filename_component(ext "${ocaml_output}" EXT)
if( NOT (ext STREQUAL ".cmo" OR
ext STREQUAL ".ml" OR
ext STREQUAL ".o" OR
ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX) )
list(APPEND install_files "${ocaml_output}")
elseif( ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX)
list(APPEND install_shlibs "${ocaml_output}")
endif()
endforeach()
install(FILES ${install_files}
DESTINATION "${LLVM_OCAML_INSTALL_PATH}/llvm")
install(FILES ${install_shlibs}
PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE
GROUP_READ GROUP_EXECUTE
WORLD_READ WORLD_EXECUTE
DESTINATION "${LLVM_OCAML_INSTALL_PATH}/stublibs")
foreach( install_file ${install_files} ${install_shlibs} )
get_filename_component(filename "${install_file}" NAME)
add_custom_command(TARGET "ocaml_${name}" POST_BUILD
COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${install_file}"
"${LLVM_LIBRARY_DIR}/ocaml/llvm/"
COMMENT "Copying OCaml library component ${filename} to intermediate area"
VERBATIM)
add_dependencies("ocaml_${name}" ocaml_make_directory)
endforeach()
endfunction()
# add_custom_target(ocaml_make_directory
# COMMAND "${CMAKE_COMMAND}" "-E" "make_directory" "${LLVM_LIBRARY_DIR}/ocaml/llvm")
add_custom_target("ocaml_make_directory")
# add_custom_target("ocaml_all")
# set_target_properties(ocaml_all PROPERTIES FOLDER "Misc")
# set_target_properties(ocaml_make_directory PROPERTIES FOLDER "Misc")

107
cmake/modules/FindOCaml.cmake Normal file
View file

@ -0,0 +1,107 @@
# 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 )
include(AddOCaml)
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()

400
makefile Normal file
View file

@ -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
# )

12
src/CMakeLists.txt
View file

@ -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
################################################################################

320
src/api/ml/CMakeLists.txt Normal file
View file

@ -0,0 +1,320 @@
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
)
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")
set(z3ml_common_flags "-package" "zarith"
"-I" "${z3ml_bin}")
# 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)
# 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"
DEPENDS ${z3ml_bin}/z3enums.cmo
${z3ml_bin}/z3native.cmo
${z3ml_bin}/z3.ml
${z3ml_bin}/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 "-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}")
endif()
list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath})
# 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}
"-L${libz3_path}"
"-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
###############################################################################
add_custom_command(
OUTPUT ${z3ml_bin}/ml_example.ml
COMMAND "${CMAKE_COMMAND}" "-E"
"copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml"
DEPENDS ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml
COMMENT "Copying ml_example.ml to build area")
execute_process(
COMMAND ${OCAMLFIND} query zarith
OUTPUT_VARIABLE ocaml_pkg_zarith_path
OUTPUT_STRIP_TRAILING_WHITESPACE)
# "-I" "+threads"
add_custom_command(
OUTPUT ${z3ml_bin}/ml_example${bc_ext}
${z3ml_bin}/ml_example.bc.log
COMMAND "${OCAMLFIND}" "ocamlc"
"-o" "${z3ml_bin}/ml_example${bc_ext}"
"-package" "zarith"
"-I" "${z3ml_bin}"
"-dllpath" "${z3ml_bin}"
"-I" ${ocaml_stublibs_path}
"-dllpath" ${ocaml_stublibs_path}
"${ocaml_pkg_zarith_path}/zarith.cma"
"${z3ml_bin}/z3ml.cma"
"${z3ml_bin}/ml_example.ml"
COMMAND
"ocamlrun" "${z3ml_bin}/ml_example${bc_ext}"
">" "${z3ml_bin}/ml_example.bc.log"
DEPENDS
${z3ml_bin}/z3ml.cma
${z3ml_bin}/dllz3ml.so
${z3ml_bin}/ml_example.ml
COMMENT "Testing build and run ml_example bytecode"
VERBATIM)
# "-I" "+threads"
add_custom_command(
OUTPUT ${z3ml_bin}/ml_example${exe_ext}
${z3ml_bin}/ml_example.log
COMMAND "${OCAMLFIND}" "ocamlopt"
"-o" "${z3ml_bin}/ml_example${exe_ext}"
"-package" "zarith"
"-linkpkg"
"-I" "${z3ml_bin}"
"${z3ml_bin}/z3ml.cmxa"
"${z3ml_bin}/ml_example.ml"
COMMAND "${z3ml_bin}/ml_example${exe_ext}"
">" "${z3ml_bin}/ml_example.log"
DEPENDS
${z3ml_bin}/z3ml.cmxa
${z3ml_bin}/dllz3ml.so
${z3ml_bin}/ml_example.ml
COMMENT "Testing build and run ml_example natively"
VERBATIM)
add_custom_target(build_ocaml_example
ALL
DEPENDS
${z3ml_bin}/ml_example${bc_ext}
${z3ml_bin}/ml_example${exe_ext}
)
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
build_ocaml_example
)
###############################################################################
# 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()

32
src/api/ml/z3.mli
View file

@ -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