Merge branch 'delcypher-cmake_build_system4'

.gitignore

@@ -75,3 +75,12 @@ src/api/ml/z3.mllib
 *.bak
 doc/api
 doc/code
+
+# CMake files copied over by the ``contrib/cmake/boostrap.py`` script
+# See #461
+examples/CMakeLists.txt
+examples/*/CMakeLists.txt
+src/CMakeLists.txt
+src/*/CMakeLists.txt
+src/*/*/CMakeLists.txt
+src/*/*/*/CMakeLists.txt

CMakeLists.txt

@@ -0,0 +1,366 @@
+# Enforce some CMake policies
+cmake_minimum_required(VERSION 2.8.12)
+if (POLICY CMP0054)
+  # FIXME: This is horrible. With the old behaviour,
+  # quoted strings like "MSVC" in if() conditionals
+  # get implicitly dereferenced. The NEW behaviour
+  # doesn't do this but CMP0054 was only introduced
+  # in CMake 3.1 and we support lower versions as the
+  # minimum. We could set NEW here but it would be very
+  # confusing to use NEW for some builds and OLD for others
+  # which could lead to some subtle bugs. Instead when the
+  # minimum version is 3.1 change this policy to NEW and remove
+  # the hacks in place to work around it.
+  cmake_policy(SET CMP0054 OLD)
+endif()
+
+# Provide a friendly message if the user hasn't run the bootstrap script
+# to copy all the CMake files into their correct location.
+# It is unfortunate that we have to do this, see #461 for the discussion
+# on this.
+if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt"))
+  message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\""
+          ". This probably means you need to run"
+          "``python contrib/cmake/bootstrap.py create``")
+endif()
+
+# This overrides the default flags for the different CMAKE_BUILD_TYPEs
+set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake")
+project(Z3 C CXX)
+
+################################################################################
+# Project version
+################################################################################
+set(Z3_VERSION_MAJOR 4)
+set(Z3_VERSION_MINOR 4)
+set(Z3_VERSION_PATCH 2)
+set(Z3_VERSION_TWEAK 0)
+set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
+message(STATUS "Z3 version ${Z3_VERSION}")
+
+################################################################################
+# Set various useful variables depending on CMake version
+################################################################################
+if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2"))
+  # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument
+  set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL")
+else()
+  set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "")
+endif()
+
+################################################################################
+# Message for polluted source tree sanity checks
+################################################################################
+set(z3_polluted_tree_msg
+  " should not exist and is polluting the source tree."
+  " It is likely that this file came from the Python build system which"
+  " generates files inside the source tree. This is bad practice and the CMake"
+  " build system is setup to make sure that the source tree is clean during"
+  " its configure step. If you are using git you can remove all untracked files"
+  " using ``git clean -fx``. Be careful when doing this. You should probably use"
+  " this with ``-n`` first to check which file(s) would be removed."
+)
+
+################################################################################
+# Sanity check - Disallow building in source
+################################################################################
+if ("${CMAKE_SOURCE_DIR}" STREQUAL "${CMAKE_BINARY_DIR}")
+  message(FATAL_ERROR "In source builds are not allowed. You should invoke "
+          "CMake from a different directory.")
+endif()
+
+################################################################################
+# Add our CMake module directory to the list of module search directories
+################################################################################
+list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules")
+
+################################################################################
+# Useful CMake functions/Macros
+################################################################################
+include(CheckCXXSourceCompiles)
+
+################################################################################
+# Compiler flags for Z3 components.
+# Subsequent commands will append to this
+################################################################################
+set(Z3_COMPONENT_CXX_DEFINES "")
+set(Z3_COMPONENT_CXX_FLAGS "")
+set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "")
+set(Z3_DEPENDENT_LIBS "")
+set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "")
+set(Z3_DEPENDENT_EXTRA_C_LINK_FLAGS "")
+
+################################################################################
+# Build type
+################################################################################
+message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi-configuration build (e.g. Visual Studio and Xcode). Here
+  # CMAKE_BUILD_TYPE doesn't matter
+  message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
+else()
+  # Single configuration generator (e.g. Unix Makefiles, Ninja)
+  set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
+  if(NOT CMAKE_BUILD_TYPE)
+    message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
+    message(STATUS "The available build types are: ${available_build_types}")
+    set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String
+        "Options are ${build_types}"
+        FORCE)
+    # Provide drop down menu options in cmake-gui
+    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
+  endif()
+  message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
+endif()
+
+# CMAKE_BUILD_TYPE has no meaning for multi-configuration generators
+# (e.g. Visual Studio) so use generator expressions instead to add
+# the right definitions when doing a particular build type.
+#
+# Note for some reason we have to leave off ``-D`` here otherwise
+# we get ``-D-DZ3DEBUG`` passed to the compiler
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:Z3DEBUG>)
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Release>:_EXTERNAL_RELEASE>)
+list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>)
+
+################################################################################
+# Find Python
+################################################################################
+find_package(PythonInterp REQUIRED)
+message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
+
+################################################################################
+# Target architecture detection
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake)
+detect_target_architecture(TARGET_ARCHITECTURE)
+message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}")
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_")
+endif()
+
+
+################################################################################
+# Function for detecting C++ compiler flag support
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake)
+
+################################################################################
+# Platform detection
+################################################################################
+if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
+  message(STATUS "Platform: Linux")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_")
+  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+    list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
+  endif()
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+  # Does OSX really not need any special flags?
+  message(STATUS "Platform: Darwin")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
+  message(STATUS "Platform: FreeBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
+  message(STATUS "Platform: OpenBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif (CYGWIN)
+  message(STATUS "Platform: Cygwin")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN")
+  z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED)
+elseif (WIN32)
+  message(STATUS "Platform: Windows")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS")
+else()
+  message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
+endif()
+
+
+################################################################################
+# GNU multiple precision library support
+################################################################################
+option(USE_LIB_GMP "Use GNU Multiple Precision Library" OFF)
+if (USE_LIB_GMP)
+  # Because this is off by default we will make the configure fail if libgmp
+  # can't be found
+  find_package(GMP REQUIRED)
+  message(STATUS "Using libgmp")
+  list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES})
+  list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS})
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
+else()
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")
+  message(STATUS "Not using libgmp")
+endif()
+
+################################################################################
+# FOCI2 support
+################################################################################
+# FIXME: What is this?
+option(USE_FOCI2 "Use FOCI2" OFF)
+if (USE_FOCI2)
+  message(FATAL_ERROR "TODO")
+  message(STATUS "Using FOCI2")
+else()
+  message(STATUS "Not using FOCI2")
+endif()
+
+################################################################################
+# OpenMP support
+################################################################################
+option(USE_OPENMP "Use OpenMP" ON)
+set(OPENMP_FOUND FALSE)
+if (USE_OPENMP)
+  # Because this is on by default we make the configure succeed with a warning
+  # if OpenMP support is not detected.
+  find_package(OpenMP)
+  if (NOT OPENMP_FOUND)
+    message(WARNING "OpenMP support was requested but your compiler doesn't support it")
+  endif()
+endif()
+if (OPENMP_FOUND)
+    list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS})
+    # GCC and Clang need to have additional flags passed to the linker.
+    # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})``
+    # because ``/openmp`` is interpreted as file name rather than a linker
+    # flag by MSVC and breaks the build
+    if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
+        ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+      list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_C_FLAGS})
+    endif()
+    if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR
+        ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU"))
+      list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_CXX_FLAGS})
+    endif()
+    unset(CMAKE_REQUIRED_FLAGS)
+    message(STATUS "Using OpenMP")
+else()
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_")
+  message(STATUS "Not using OpenMP")
+endif()
+
+################################################################################
+# FP math
+################################################################################
+# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
+    set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
+    # FIXME: Remove "x.." when CMP0054 is set to NEW
+  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+    set(SSE_FLAGS "/arch:SSE2")
+  else()
+    message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
+  endif()
+  CHECK_CXX_COMPILER_FLAG("${SSE_FLAGS}" HAS_SSE2)
+  if (HAS_SSE2)
+    list(APPEND Z3_COMPONENT_CXX_FLAGS ${SSE_FLAGS})
+  endif()
+  unset(SSE_FLAGS)
+endif()
+
+################################################################################
+# Threading support
+################################################################################
+find_package(Threads)
+list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
+
+################################################################################
+# Compiler warnings
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
+
+################################################################################
+# Option to control what type of library we build
+################################################################################
+option(BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON)
+
+
+################################################################################
+# Symbol visibility
+################################################################################
+if (NOT MSVC)
+  z3_add_cxx_flag("-fvisibility=hidden" REQUIRED)
+endif()
+
+################################################################################
+# Tracing
+################################################################################
+option(ENABLE_TRACING OFF "Enable tracing")
+if (ENABLE_TRACING)
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE")
+endif()
+# Should we always enable tracing when doing a debug build?
+#list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:Debug>:_TRACE>)
+
+################################################################################
+# Postion indepdent code
+################################################################################
+# This is required because code built in the components will end up in a shared
+# library. If not building a shared library ``-fPIC`` isn't needed and would add
+# unnecessary overhead.
+if (BUILD_LIBZ3_SHARED)
+  if (NOT MSVC)
+    z3_add_cxx_flag("-fPIC" REQUIRED)
+  endif()
+endif()
+
+################################################################################
+# Report Z3_COMPONENT flags
+################################################################################
+message(STATUS "Z3_COMPONENT_CXX_DEFINES: ${Z3_COMPONENT_CXX_DEFINES}")
+message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}")
+message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}")
+message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}")
+message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}")
+message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}")
+
+################################################################################
+# Z3 installation locations
+################################################################################
+set (Z3_INSTALL_LIB_DIR "lib")
+set (Z3_INSTALL_BIN_DIR "bin")
+set (Z3_INSTALL_INCLUDE_DIR "include")
+
+################################################################################
+# CMake build file locations
+################################################################################
+# To mimic the python build system output these into the root of the build
+# directory
+set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}")
+
+################################################################################
+# Z3 components, library and executables
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake)
+include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake)
+add_subdirectory(src)
+
+################################################################################
+# Examples
+################################################################################
+option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON)
+if (ENABLE_EXAMPLE_TARGETS)
+  add_subdirectory(examples)
+endif()
+
+################################################################################
+# Uninstall rule
+################################################################################
+configure_file(
+  "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in"
+  "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+  @ONLY
+)
+
+add_custom_target(uninstall
+  COMMAND
+  "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake"
+  COMMENT "Uninstalling..."
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  VERBATIM
+)

README-CMake.md

@@ -0,0 +1,401 @@
+# Z3's CMake build system
+
+[CMake](https://cmake.org/) is a "meta build system" that reads a description
+of the project written in the ``CMakeLists.txt`` files and emits a build
+system for that project of your choice using one of CMake's "generators".
+This allows CMake to support many different platforms and build tools.
+You can run ``cmake --help`` to see the list of supported "generators"
+on your platform. Example generators include "UNIX Makfiles" and "Visual Studio
+12 2013".
+
+## Getting started
+
+### Fixing a polluted source tree
+
+If you have never used the python build system you can skip this step.
+
+The existing Python build system creates generated source files in
+the source tree. The CMake build system will refuse to work if it
+detects this so you need to clean your source tree first.
+
+To do this run the following in the root of the repository
+
+```
+git clean -nx src
+```
+
+This will list everything that will be removed. If you are happy
+with this then run.
+
+```
+git clean -fx src
+```
+
+which will remove the generated source files.
+
+### Bootstrapping
+
+Most of Z3's CMake files do not live in their correct location. Instead those
+files live in the ``contrib/cmake`` folder and a script is provided that will
+copy (or hard link) the files into their correct location.
+
+To copy the files run
+
+```
+python contrib/cmake/bootstrap.py create
+```
+
+in the root of the repository. Once you have done this you can now build Z3 using CMake.
+Make sure you remember to rerun this command if you pull down new code/rebase/change branch so
+that the copied CMake files are up to date.
+
+To remove the copied files run
+
+```
+python contrib/cmake/bootstrap.py remove
+```
+
+Note if you plan to do development on Z3 you should read the developer
+notes on bootstrapping in this document.
+
+What follows is a brief walk through of how to build Z3 using some
+of the more commonly used CMake generators.
+
+### Unix Makefiles
+
+Run the following in the top level directory of the Z3 repository.
+
+```
+mkdir build
+cd build
+cmake -G "Unix Makefiles" ../
+make -j4 # Replace 4 with an appropriate number
+```
+
+Note that on some platforms "Unix Makesfiles" is the default generator so on those
+platforms you don't need to pass ``-G "Unix Makefiles"`` command line option to
+``cmake``.
+
+Note there is nothing special about the ``build`` directory name here. You can call
+it whatever you like.
+
+Note the "Unix Makefile" generator is a "single" configuration generator which
+means you pick the build type (e.g. ``Debug``, ``Release``) when you invoke CMake.
+You can set the build type by passing it to the ``cmake`` invocation like so:
+
+```
+cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../
+```
+
+See the section on "Build Types" for the different CMake build types.
+
+If you wish to use a different compiler set the CXX and CC environment variables
+passed to cmake. This must be done at the very first invocation to ``cmake``
+in the build directory because once configuration has happened the compiler
+is fixed. If you want to use a different compiler to the one you have already
+configured you either need to make a new build directory or delete the contents
+of the current build directory and start again.
+
+For example to use clang the ``cmake `` line would be
+
+```
+CC=clang CXX=clang++ cmake ../
+```
+
+Note that CMake build will detect the target architecture that compiler is set up
+to build for and the generated build system will build for that architecture.
+If there is a way to tell your compiler to build for a different architecture via
+compiler flags then you can set the ``CFLAGS`` and ``CXXFLAGS`` environment variables
+to have the build target that architecture.
+
+For example if you are on a x86_64 machine and you want to do a 32-bit build and have
+a multilib version of GCC you can run ``cmake`` like this
+
+```
+CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../
+```
+
+Note like with the ``CC`` and ``CXX`` flags this must be done on the very first invocation
+to CMake in the build directory.
+
+### Ninja
+
+[Ninja](https://ninja-build.org/) is a simple build system that is built for speed.
+It can be significantly faster than "UNIX Makefile"s because it is not a recursive
+build system and thus doesn't create a new process everytime it traverses into a directory.
+Ninja is particularly appropriate if you want fast incremental building.
+
+Basic usage is as follows:
+
+```
+mkdir build
+cd build
+cmake -G "Ninja" ../
+ninja
+```
+
+Note the discussion of the ``CC``, ``CXX``, ``CFLAGS`` and ``CXXFLAGS`` for "Unix Makefiles"
+also applies here.
+
+Note also that like the "Unix Makefiles" generator, the "Ninja" generator is a single configuration
+generator so you pick the build type when you invoke ``cmake`` by passing ``CMAKE_BUILD_TYPE=<build_type>``
+to ``cmake``. See the section on "Build Types".
+
+Note that Ninja runs in parallel by default. Use the ``-j`` flag to change this.
+
+Note that Ninja also runs on Windows. You just need to run ``cmake`` in an
+environment where the compiler can be found. If you have Visual Studio
+installed it typically ships with a "Developer Command Prompt Window" that you
+can use which has the environment variables setup for you.
+
+### NMake
+
+NMake is a build system that ships with Visual Studio. You are advised to use
+Ninja instead which is significantly faster due to supporting concurrent
+builds. However CMake does support NMake if you wish to use it. Note that
+NMake is a single configuration generator so you must set ``CMAKE_BUILD_TYPE``
+to set the build type.
+
+Basic usage:
+
+1. Launch the "Developer Command Prompt Windows"
+2. Change to the root of the Z3 repository
+
+```
+mkdir build
+cd build
+cmake -G "NMake Makefiles" ../
+nmake
+```
+
+### Visual Studio
+
+For the Visual Studio generators you need to know which version of Visual Studio you wish
+to use and also what architecture you want to build for.
+
+We'll use the ``cmake-gui`` here as it is easier to pick the right generator but this can
+be scripted if need be.
+
+Here are the basic steps:
+
+1. Create an empty build directory
+2. Start the cmake-gui program
+3. Set "where is the source code" to the root of the Z3 project repository. You can do this by pressing
+   the "Browse Source..." button and picking the directory.
+4. Set "where to build the binaries" to the empty build directory you just created. You can do this
+   by pressing the "Browse build..." button and picking the directory.
+5. Press the "Configure" button
+6. A window will appear asking you to pick the generator to use. Pick the
+   generator that matches the version of Visual Studio you are using. Note also
+   that some of the generator names contain ``Win64`` (e.g. ``Visual Studio 12
+   2013 Win64``) this indicates a x86 64-bit build. Generator names without
+   this (e.g. ``Visual Studio 12 2013``) are x86 32-bit build.
+7. Press the "Finish" button and wait for CMake to finish it's first configure.
+8. A set of configuration options will appear which will affect various aspects of the build.
+   Change them as you desire. If you change a set of options press the "Configure"
+   again. Additional options may appear when you do this.
+9. When you have finished changing configuration options press the "Generate" button.
+10. When generation is done close cmake-gui.
+11. In the build directory open the generated ``Z3.sln`` solution file created by CMake with
+    Visual Studio.
+12. In Visual Studio pick the build type (e.g. ``Debug``, ``Release``) you want.
+13. Click "BUILD > Build Solution".
+
+Note that unlike the "Unix Makefile" and "Ninja" generators the Visual Studio generators
+are multi-configuration generators which means you don't set the build type when invoking
+CMake. Instead you set the build type inside Visual Studio. See the "Build Type" section
+for more information.
+
+### General workflow
+
+The general workflow when using CMake is the following
+
+1. Create a new build directory
+2. Configure the project
+3. Generate the build system
+4. Invoke the build system to build the project
+
+To perform steps 2 and 3 you can choose from three different tools
+
+* cmake
+* ccmake
+* cmake-gui
+
+``cmake`` is a command line tool and is what you should use if you are
+writing a script to build Z3. This tool performs steps 1 and 2 in one
+go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are
+more interactive and allow you to change various options. In both these
+tools the basic steps to follow are:
+
+1. Configure.
+2. Change any options you wish. Everytime you change a set of options
+   You should configure again. This may cause new options to appear
+3. Generate.
+
+For information see https://cmake.org/runningcmake/
+
+Note when invoking CMake you give it the path to the source directory.
+This is the top-level directory in the Z3 repository containing a
+``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``.
+If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory)
+the configure step will fail.
+
+## Build Types
+
+Several build types are supported.
+
+* Release
+* Debug
+* RelWithDebInfo
+* MinSizeRel
+
+For the single configuration generators (e.g. "Unix Makefile" and "Ninja") you set the
+build type when invoking ``cmake`` by passing ``-DCMAKE_BUILD_TYPE=<build_type>`` where
+``<build_type>`` is one of the build types specified above.
+
+For multi-configuration generators (e.g. Visual Studio) you don't set the build type
+when invoking CMake and instead set the build type within Visual Studio itself.
+
+## Useful options
+
+The following useful options can be passed to CMake whilst configuring.
+
+* ``CMAKE_BUILD_TYPE`` - STRING. The build type to use. Only relevant for single configuration generators (e.g. "Unix Makefile" and "Ninja").
+* ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``)
+* ``ENABLE_TRACING`` - BOOL. If set to ``TRUE`` enable tracing, if set to ``FALSE`` disable tracing.
+* ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
+* ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
+* ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support.
+* ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation.
+* ``BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built.
+* ``INSTALL_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_PYTHON_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Python bindings.
+
+On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
+
+Example
+
+```
+cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../
+```
+
+## Developer/packager notes
+
+These notes are help developers and packagers of Z3.
+
+### Boostrapping the CMake build
+
+Z3's CMake system is experimental and not officially supported. Consequently
+Z3's developers have decided that they do not want the CMake files in the
+``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py``
+script copies or hard links them into the correct locations. For context
+on this decision see https://github.com/Z3Prover/z3/pull/461 .
+
+The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes
+development harder because you have to copy your modifications over to the
+files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like
+platform you can create hard links instead by running
+
+```
+contrib/cmake/boostrap.py create --hard-link
+```
+
+Using hard links means that modifying any of the "copied" files also modifies the
+file under version control. Using hard links also means that the file modification time
+will appear correct (i.e. the hard-linked "copies" have the same file modification time
+as the corresponding file under version control) which means CMake will correctly reconfigure
+when invoked. This is why using symbolic links is not an option because the file modification
+time of a symbolic link is not the same as the file modification of the file being pointed to.
+
+Unfortunately a downside to using hard links (or just plain copies) is that if
+you pull down new code (i.e. ``git pull``) then some of the CMake files under
+version control may change but the corresponding hard-linked "copies" will not.
+
+This mean that (regardless of whether or not you use hard links) every time you
+pull down new code or change branch or do an interactive rebase you must run
+(with or without ``--hard-link``):
+
+```
+contrb/cmake/boostrap.py create
+```
+
+in order to be sure that the copied CMake files are not out of date.
+
+### Install/Uninstall
+
+Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to set the install
+prefix.
+
+To install run
+
+```
+make install
+```
+
+To uninstall run
+
+```
+make uninstall
+```
+
+Note that ``DESTDIR`` is supported for [staged installs](https://www.gnu.org/prep/standards/html_node/DESTDIR.html).
+
+To install
+
+```
+mkdir staged
+make install DESTDIR=/full/path/to/staged/
+```
+
+to uninstall
+
+```
+make uninstall DESTDIR=/full/path/to/staged
+```
+
+The above also works for Ninja but ``DESTDIR`` must be an environment variable instead.
+
+### Examining invoked commands
+
+If you are using the "UNIX Makefiles" generator and want to see exactly the commands that are
+being run you can pass ``VERBOSE=1`` to make.
+
+```
+make VERBOSE=1
+```
+
+If you are using Ninja you can use the ``-v`` flag.
+
+### Additional targets
+
+To see the list of targets run
+
+```
+make help
+```
+
+There are a few special targets:
+
+* ``clean`` all the built targets in the current directory and below
+* ``edit_cache`` will invoke one of the CMake tools (depending on which is available) to let you change configuration options.
+* ``rebuild_cache`` will reinvoke ``cmake`` for the project.
+
+### Setting build type specific flags
+
+The build system supports single configuration and multi-configuration generators. This means
+it is not possible to know the build type at configure time and therefore ``${CMAKE_BUILD_TYPE}``
+should not be conditionally used to set compiler flags or definitions. Instead you should use Generator expressions which are evaluated by the generator.
+
+For example
+
+```
+$<$<CONFIG:Debug>:Z3DEBUG>
+```
+
+If the build type at build time is ``Debug`` this evaluates to ``Z3DEBUG`` but evaluates to nothing for all other configurations. You can see examples of this in the ``CMakeLists.txt`` files.
+
+### File-globbing
+
+It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files matching a pattern and
+use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake.
+
+Long story short. Don't use file globbing.

README.md

@@ -74,6 +74,11 @@ sudo make uninstall
 
 To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again.
 
+## Building Z3 using CMake
+
+Z3 has an unofficial build system using CMake. Read the [README-CMake.md](README-CMake.md)
+file for details.
+
 ## Z3 bindings
 
 Z3 has bindings for various programming languages.

contrib/cmake/bootstrap.py

@@ -0,0 +1,261 @@
+#!/usr/bin/env python
+"""
+This script is used to copy or delete the
+CMake build system files from the contrib/cmake
+folder into the their correct location in the Z3
+repository.
+
+It offers two modes
+
+* create - This will symlink the ``cmake`` directory and copy (or hard link)
+the appropriate files into their correct locations in the repository.
+
+* remove - This will remove the symlinked ``cmake``
+directory and remove the files added by the above
+methods.
+
+This has the advantage
+that editing the hard link edits the underlying file
+(making development easier because copying files is
+not neccessary) and CMake will regenerate correctly
+because the modification time stamps will be correct.
+
+"""
+import argparse
+import logging
+import os
+import pprint
+import shutil
+import sys
+
+def get_full_path_to_script():
+  return os.path.abspath(__file__)
+
+def get_cmake_contrib_dir():
+  return os.path.dirname(get_full_path_to_script())
+
+def get_repo_root_dir():
+  r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir()))
+  assert os.path.isdir(r)
+  return r
+
+# These are paths that should be ignored when checking if a folder
+# in the ``contrib/cmake`` exists in the root of the repository
+verificationExceptions = {
+  os.path.join(get_repo_root_dir(), 'cmake'),
+  os.path.join(get_repo_root_dir(), 'cmake', 'modules')
+}
+
+def contribPathToRepoPath(path):
+  assert path.startswith(get_cmake_contrib_dir())
+  stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash
+  assert not os.path.isabs(stripped)
+  logging.debug('stripped:{}'.format(stripped))
+  r = os.path.join(get_repo_root_dir(), stripped)
+  assert os.path.isabs(r)
+  logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r))
+  return r
+
+def verify_mirrored_directory_struture():
+  """
+  Check that the directories contained in ``contrib/cmake`` exist
+  in the root of the repo.
+  """
+  for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()):
+    expectedDir = contribPathToRepoPath(dirpath)
+    logging.debug('expectedDir:{}'.format(expectedDir))
+    if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and
+        expectedDir not in verificationExceptions):
+      logging.error(('Expected to find directory "{}" but it does not exist'
+                     ' or is not a directory').format(expectedDir))
+      return 1
+
+  return 0
+
+def mk_sym_link(target, linkName):
+  logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName))
+  if os.path.exists(linkName):
+    logging.info('Removing existing link "{}"'.format(linkName))
+    if not os.path.islink(linkName):
+      logging.warning('"{}" overwriting file that is not a symlink'.format(linkName))
+    delete_path(linkName)
+  if os.name == 'posix':
+    os.symlink(target, linkName)
+  else:
+    # TODO: Windows does support symlinks but the implementation to do that
+    # from python is a little complicated so for now lets just copy everyting
+    logging.warning('Creating symbolic links is not supported. Just making a copy instead')
+    if os.path.isdir(target):
+      # Recursively copy directory
+      shutil.copytree(src=target, dst=linkName, symlinks=False)
+    else:
+      # Copy file
+      assert os.path.isfile(target)
+      shutil.copy2(src=target, dst=linkName)
+
+def delete_path(path):
+  logging.info('Removing "{}"'.format(path))
+  if not os.path.exists(path):
+    logging.warning('"{}" does not exist'.format(path))
+    return
+  if os.path.isdir(path) and not os.path.islink(path):
+    # FIXME: If we can get symbolic link support on Windows we
+    # can disallow this completely.
+    assert os.name == 'nt'
+    shutil.rmtree(path)
+  else:
+    os.remove(path)
+
+def shouldSkipFile(path):
+  # Skip this script
+  if path == get_full_path_to_script():
+    return True
+  # Skip the maintainers file
+  if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'):
+    return True
+  # Skip Vim temporary files
+  if os.path.basename(path).startswith('.') and path.endswith('.swp'):
+    return True
+  return False
+
+
+def create(useHardLinks):
+  """
+    Copy or hard link files in the CMake contrib directory
+    into the repository where they are intended to live.
+
+    Note that symbolic links for the CMakeLists.txt files
+    are not appropriate because they won't have the right
+    file modification time when the files they point to
+    are modified. This would prevent CMake from correctly
+    reconfiguring when it detects this is required.
+  """
+
+  # Make the ``cmake`` directory a symbolic link.
+  # We treat this one specially as it is the only directory
+  # that doesn't already exist in the repository root so
+  # we can just use a symlink here
+  linkName = os.path.join(get_repo_root_dir(), 'cmake')
+  target = os.path.join(get_cmake_contrib_dir(), 'cmake')
+  specialDir = target
+  mk_sym_link(target, linkName)
+
+  for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()):
+    # Skip the special directory and its children
+    if dirPath.startswith(specialDir):
+      logging.info('Skipping directory "{}"'.format(dirPath))
+      continue
+
+    for fileName in fileNames:
+      fileInContrib = os.path.join(dirPath, fileName)
+      # Skip files
+      if shouldSkipFile(fileInContrib):
+        logging.info('Skipping "{}"'.format(fileInContrib))
+        continue
+      fileInRepo = contribPathToRepoPath(fileInContrib)
+      logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo))
+      if useHardLinks:
+        if not os.name == 'posix':
+          logging.error('Hard links are not supported on your platform')
+          return False
+        if os.path.exists(fileInRepo):
+          delete_path(fileInRepo)
+        os.link(fileInContrib, fileInRepo)
+      else:
+        try:
+          shutil.copy2(src=fileInContrib, dst=fileInRepo)
+        except shutil.Error as e:
+          # Can hit this if used created hard links first and then run again without
+          # wanting hard links
+          if sys.version_info.major <= 2:
+            logging.error(e.message)
+          else:
+            # Python >= 3
+            if isinstance(e, shutil.SameFileError):
+              logging.error('Trying to copy "{}" to "{}" but they are the same file'.format(
+                fileInContrib, fileInRepo))
+            else:
+              logging.error(e)
+          logging.error('You should remove the files using the "remove" mode '
+                        'and try to create again. You probably are mixing the '
+                        'hard-link and non-hard-link create modes')
+          return False
+  return True
+
+def remove():
+  """
+    Remove the CMake files from their intended location in
+    the repository. This is used to remove
+    the files created by the ``create()`` function.
+  """
+  # This directory is treated specially as it is normally
+  # a symlink.
+  linkName = os.path.join(get_repo_root_dir(), 'cmake')
+  delete_path(linkName)
+  specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake')
+
+  for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()):
+    # Skip the special directory and its children
+    if dirPath.startswith(specialDir):
+      logging.info('Skipping directory "{}"'.format(dirPath))
+      continue
+    for fileName in fileNames:
+      fileInContrib = os.path.join(dirPath, fileName)
+      # Skip files
+      if shouldSkipFile(fileInContrib):
+        logging.info('Skipping "{}"'.format(fileInContrib))
+        continue
+      fileInRepo = contribPathToRepoPath(fileInContrib)
+      if os.path.exists(fileInRepo):
+        logging.info('Removing "{}"'.format(fileInRepo))
+        delete_path(fileInRepo)
+  return True
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument('mode',
+    choices=['create', 'remove'],
+    help='The mode to use')
+  parser.add_argument("-l","--log-level",
+    type=str,
+    default="info",
+    dest="log_level",
+    choices=['debug','info','warning','error']
+  )
+  parser.add_argument("-H", "--hard-link",
+    action='store_true',
+    default=False,
+    dest='hard_link',
+    help='When using the create mode create hard links instead of copies'
+  )
+  pargs = parser.parse_args(args)
+
+  logLevel = getattr(logging, pargs.log_level.upper(),None)
+  logging.basicConfig(level=logLevel)
+
+  # Before we start make sure we can transplant the CMake files on to
+  # repository
+  if verify_mirrored_directory_struture() != 0:
+    logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir()))
+    return 1
+
+  if pargs.mode == "create":
+    if not create(useHardLinks=pargs.hard_link):
+      logging.error("Failed to create")
+      return 1
+  elif pargs.mode == "create_hard_link":
+    if not create(useHardLinks=True):
+      logging.error("Failed to create_hard_link")
+      return 1
+  elif pargs.mode == "remove":
+    if not remove():
+      logging.error("Failed to remove")
+      return 1
+  else:
+    logging.error('Unknown mode "{}"'.format(pargs.mode))
+
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))

contrib/cmake/cmake/cmake_uninstall.cmake.in

@@ -0,0 +1,24 @@
+if(NOT EXISTS "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt")
+  message(FATAL_ERROR "Cannot find install manifest: "
+          "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt")
+endif()
+
+file(READ "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt" files)
+string(REGEX REPLACE "\n" ";" files "${files}")
+foreach(file ${files})
+  set(_full_file_path "$ENV{DESTDIR}${file}")
+  message(STATUS "Uninstalling ${_full_file_path}")
+  if(IS_SYMLINK "${_full_file_path}" OR EXISTS "${_full_file_path}")
+    # We could use ``file(REMOVE ...)`` here but then we wouldn't
+    # know if the removal failed.
+    execute_process(COMMAND
+      "@CMAKE_COMMAND@" "-E" "remove" "${_full_file_path}"
+      RESULT_VARIABLE rm_retval
+    )
+    if(NOT "${rm_retval}" STREQUAL 0)
+      message(FATAL_ERROR "Problem when removing \"${_full_file_path}\"")
+    endif()
+  else()
+    message(STATUS "File \"${_full_file_path}\" does not exist.")
+  endif()
+endforeach()

contrib/cmake/cmake/compiler_flags_override.cmake

@@ -0,0 +1,37 @@
+# This file overrides the default compiler flags for CMake's built-in
+# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here.
+# The main purpose is to make sure ``-DNDEBUG`` is never set by default.
+if (CMAKE_C_COMPILER_ID)
+  set(_lang C)
+elseif(CMAKE_CXX_COMPILER_ID)
+  set(_lang CXX)
+else()
+  message(FATAL_ERROR "Unknown language")
+endif()
+
+if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU"))
+  # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed
+  set(CMAKE_${_lang}_FLAGS_INIT "")
+  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0")
+  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os")
+  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3")
+  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g")
+  # FIXME: Remove "x.." when CMP0054 is set to NEW
+elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC")
+  set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1")
+  set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT     "/MT /O1 /Ob1")
+  set(CMAKE_${_lang}_FLAGS_RELEASE_INIT        "/MT /O2 /Ob2")
+  set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1")
+  # Override linker flags (see Windows-MSVC.cmake for CMake's defaults)
+  # The stack size comes from the Python build system.
+  set(_msvc_stack_size "8388608")
+  set(CMAKE_EXE_LINKER_FLAGS_DEBUG_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}")
+  set(CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}")
+  set(CMAKE_EXE_LINKER_FLAGS_MINSIZEREL_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}")
+  set(CMAKE_EXE_LINKER_FLAGS_RELEASE_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}")
+  unset(_msvc_stack_size)
+else()
+  message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"")
+endif()
+
+unset(_lang)

contrib/cmake/cmake/compiler_warnings.cmake

@@ -0,0 +1,40 @@
+set(GCC_AND_CLANG_WARNINGS
+    "-Wall"
+)
+set(GCC_ONLY_WARNINGS "")
+set(CLANG_ONLY_WARNINGS "")
+set(MSVC_WARNINGS "/W3")
+
+set(WARNING_FLAGS_TO_CHECK "")
+if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
+elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
+  list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
+  # FIXME: Remove "x.." when CMP0054 is set to NEW
+elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
+else()
+  message(AUTHOR_WARNING "Unknown compiler")
+endif()
+
+# Loop through flags and use the ones which the compiler supports
+foreach (flag ${WARNING_FLAGS_TO_CHECK})
+  z3_add_cxx_flag("${flag}")
+endforeach()
+
+option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF)
+if (WARNINGS_AS_ERRORS)
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
+    # FIXME: Remove "x.." when CMP0054 is set to NEW
+  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
+  else()
+    message(AUTHOR_WARNING "Unknown compiler")
+  endif()
+  message(STATUS "Treating compiler warnings as errors")
+else()
+  message(STATUS "Not treating compiler warnings as errors")
+endif()

contrib/cmake/cmake/modules/FindGMP.cmake

@@ -0,0 +1,64 @@
+# Tries to find an install of the GNU multiple precision library
+#
+# Once done this will define
+#  GMP_FOUND - BOOL: System has the GMP library installed
+#  GMP_INCLUDE_DIRS - LIST:The GMP include directories
+#  GMP_C_LIBRARIES - LIST:The libraries needed to use GMP via it's C interface
+#  GMP_CXX_LIBRARIES - LIST:The libraries needed to use GMP via it's C++ interface
+
+include(FindPackageHandleStandardArgs)
+
+# Try to find libraries
+find_library(GMP_C_LIBRARIES
+  NAMES gmp
+  DOC "GMP C libraries"
+)
+if (GMP_C_LIBRARIES)
+  message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C library")
+endif()
+find_library(GMP_CXX_LIBRARIES
+  NAMES gmpxx
+  DOC "GMP C++ libraries"
+)
+if (GMP_CXX_LIBRARIES)
+  message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"")
+else()
+  message(STATUS "Could not find GMP C++ library")
+endif()
+
+# Try to find headers
+find_path(GMP_C_INCLUDES
+  NAMES gmp.h
+  DOC "GMP C header"
+)
+if (GMP_C_INCLUDES)
+  message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C include path")
+endif()
+
+find_path(GMP_CXX_INCLUDES
+  NAMES gmpxx.h
+  DOC "GMP C++ header"
+)
+if (GMP_CXX_INCLUDES)
+  message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"")
+else()
+  message(STATUS "Could not find GMP C++ include path")
+endif()
+
+if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES)
+  set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
+  list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
+  message(STATUS "Found GMP")
+else()
+  message(STATUS "Could not find GMP")
+endif()
+
+# TODO: We should check we can link some simple code against libgmp and libgmpxx
+
+# Handle QUIET and REQUIRED and check the necessary variables were set and if so
+# set ``GMP_FOUND``
+find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES)

contrib/cmake/cmake/target_arch_detect.cmake

@@ -0,0 +1,22 @@
+###############################################################################
+# Target detection
+#
+# We abuse the compiler preprocessor to work out what target the compiler is
+# building for. The nice thing about this approach is that we'll detect the
+# right target even if we are using a cross compiler.
+###############################################################################
+function(detect_target_architecture OUTPUT_VAR)
+  try_run(run_result
+    compile_result
+    "${CMAKE_BINARY_DIR}"
+    "${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cpp"
+    COMPILE_OUTPUT_VARIABLE compiler_output
+  )
+  if (compile_result)
+    message(FATAL_ERROR "Expected compile to fail")
+  endif()
+  string(REGEX MATCH "CMAKE_TARGET_ARCH_([a-zA-Z0-9_]+)" arch "${compiler_output}")
+  # Strip out prefix
+  string(REPLACE "CMAKE_TARGET_ARCH_" "" arch "${arch}")
+  set(${OUTPUT_VAR} "${arch}" PARENT_SCOPE)
+endfunction()

contrib/cmake/cmake/target_arch_detect.cpp

@@ -0,0 +1,10 @@
+// This is used by the CMake build to detect
+// what architecture the compiler is targeting.
+// TODO: Add more targets here
+#if defined(__i386__) || defined(_M_IX86)
+#error CMAKE_TARGET_ARCH_i686
+#elif defined(__x86_64__) || defined(_M_X64)
+#error CMAKE_TARGET_ARCH_x86_64
+#else
+#error CMAKE_TARGET_ARCH_unknown
+#endif

contrib/cmake/cmake/z3_add_component.cmake

@@ -0,0 +1,276 @@
+include(CMakeParseArguments)
+define_property(GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS
+                BRIEF_DOCS "List of Z3 components to use in libz3"
+                FULL_DOCS "List of Z3 components to use in libz3")
+
+function(z3_expand_dependencies output_var)
+  if (ARGC LESS 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  # Remaing args should be component names
+  set(_expanded_deps ${ARGN})
+  set(_old_number_of_deps 0)
+  list(LENGTH _expanded_deps _number_of_deps)
+  while (_number_of_deps GREATER _old_number_of_deps)
+    set(_old_number_of_deps "${_number_of_deps}")
+    # Loop over the known dependencies and retrieve their dependencies
+    set(_old_expanded_deps ${_expanded_deps})
+    foreach (dependency ${_old_expanded_deps})
+      get_property(_depdeps GLOBAL PROPERTY Z3_${dependency}_DEPS)
+      list(APPEND _expanded_deps ${_depdeps})
+      unset(_depdeps)
+    endforeach()
+    list(REMOVE_DUPLICATES _expanded_deps)
+    list(LENGTH _expanded_deps _number_of_deps)
+  endwhile()
+  set(${output_var} ${_expanded_deps} PARENT_SCOPE)
+endfunction()
+
+function(z3_add_component_dependencies_to_target target_name)
+  if (ARGC LESS 2)
+    message(FATAL_ERROR "Invalid number of arguments")
+  endif()
+  if (NOT (TARGET ${target_name}))
+    message(FATAL_ERROR "Target \"${target_name}\" does not exist")
+  endif()
+  # Remaing args should be component names
+  set(_expanded_deps ${ARGN})
+  foreach (dependency ${_expanded_deps})
+    # FIXME: Adding these include paths wouldn't be necessary if the sources
+    # used include paths rooted in the ``src`` directory.
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    foreach (inc_dir ${_dep_include_dirs})
+      target_include_directories(${target_name} PRIVATE "${inc_dir}")
+    endforeach()
+    unset(_dep_include_dirs)
+    # Ensure this component's dependencies are built before this component.
+    # This important because we might need the generated header files in
+    # other components.
+    add_dependencies(${target_name} ${dependency})
+  endforeach()
+endfunction()
+
+# z3_add_component(component_name
+#   [NOT_LIBZ3_COMPONENT]
+#   SOURCES source1 [source2...]
+#   [COMPONENT_DEPENDENCIES component1 [component2...]]
+#   [PYG_FILES pygfile1 [pygfile2...]]
+# )
+#
+# Declares a Z3 component (as a CMake "object library") with target name
+# ``component_name``.
+#
+# The option ``NOT_LIBZ3_COMPONENT`` declares that the
+# component should not be included in libz3. If this is not specified
+# the component will be included in libz3.
+#
+# The mandatory ``SOURCES`` keyword should be followed by the source files
+# (including any files generated at build or configure time) that are should be
+# included in the component. It is not necessary to list header files here as
+# CMake infers header file dependencies unless that header file is generated at
+# build time.
+#
+# The optional ``COMPONENT_DEPENDENCIES`` keyword should be followed by a list of
+# components that ``component_name`` should depend on. The components listed here
+# must have already been declared using ``z3_add_component()``. Listing components
+# here causes them to be built before ``component_name``. It also currently causes
+# the include directories used by the transistive closure of the dependencies
+# to be added to the list of include directories used to build ``component_name``.
+#
+# The optional ``PYG_FILES`` keyword should be followed by a list of one or
+# more ``<NAME>.pyg`` files that should used to be generate
+# ``<NAME>_params.hpp`` header files used by the ``component_name``.
+#
+macro(z3_add_component component_name)
+  CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN})
+  message(STATUS "Adding component ${component_name}")
+  # Note: We don't check the sources exist here because
+  # they might be generated files that don't exist yet.
+
+  set(_list_generated_headers "")
+  foreach (pyg_file ${Z3_MOD_PYG_FILES})
+    set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}")
+    if (NOT (EXISTS "${_full_pyg_file_path}"))
+      message(FATAL_ERROR "\"${_full_pyg_file_path}\" does not exist")
+    endif()
+    string(REPLACE ".pyg" ".hpp" _output_file "${pyg_file}")
+    if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}")
+      message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}\" "
+        ${z3_polluted_tree_msg}
+      )
+    endif()
+    set(_full_output_file_path "${CMAKE_CURRENT_BINARY_DIR}/${_output_file}")
+    message(STATUS "Adding rule to generate \"${_output_file}\"")
+    add_custom_command(OUTPUT "${_output_file}"
+      COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}"
+      MAIN_DEPENDENCY "${_full_pyg_file_path}"
+      DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+      COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\""
+      WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
+      ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+      VERBATIM
+    )
+    list(APPEND _list_generated_headers "${_full_output_file_path}")
+  endforeach()
+  unset(_full_include_dir_path)
+  unset(_full_output_file_path)
+  unset(_output_file)
+
+  # Using "object" libraries here means we have a convenient
+  # name to refer to a component in CMake but we don't actually
+  # create a static/library from them. This allows us to easily
+  # build a static or dynamic library from the object libraries
+  # on all platforms. Is this added flexibility worth the linking
+  # overhead it adds?
+  add_library(${component_name} OBJECT ${Z3_MOD_SOURCES} ${_list_generated_headers})
+  unset(_list_generated_headers)
+  # Add definitions
+  foreach (define ${Z3_COMPONENT_CXX_DEFINES})
+    target_compile_definitions(${component_name} PRIVATE ${define})
+  endforeach()
+  # Add compiler flags
+  foreach (flag ${Z3_COMPONENT_CXX_FLAGS})
+    target_compile_options(${component_name} PRIVATE ${flag})
+  endforeach()
+
+  # It's unfortunate that we have to manage the include directories and dependencies ourselves.
+  #
+  # If we weren't building "object" libraries we could use
+  # ```
+  # target_include_directories(${component_name} INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  # target_link_libraries(${component_name} INTERFACE ${Z3_MOD_COMPONENT_DEPENDENCIES})
+  # ```
+  # but we can't do that with "object" libraries.
+
+  # Record this component's include directories
+  set_property(GLOBAL PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_SOURCE_DIR}")
+  set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_BINARY_DIR}")
+  set_property(GLOBAL PROPERTY Z3_${component_name}_DEPS "")
+  # Record this component's dependencies
+  foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES})
+    if (NOT (TARGET ${dependency}))
+      message(FATAL_ERROR "Component \"${component_name}\" depends on a non existant component \"${dependency}\"")
+    endif()
+    set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_DEPS "${dependency}")
+  endforeach()
+
+  # Determine all the components that this component depends on
+  set(_expanded_deps "")
+  if (DEFINED Z3_MOD_COMPONENT_DEPENDENCIES)
+    z3_expand_dependencies(_expanded_deps ${Z3_MOD_COMPONENT_DEPENDENCIES})
+    z3_add_component_dependencies_to_target(${component_name} ${_expanded_deps})
+  endif()
+  #message(STATUS "Component \"${component_name}\" has the following dependencies ${_expanded_deps}")
+
+  # For any generated header files for this component
+  target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_BINARY_DIR}")
+  # So that any generated header files can refer to source files in the component's
+  # source tree
+  target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}")
+
+  # Add any extra include directories
+  foreach (extra_include ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+    target_include_directories(${component_name} PRIVATE "${extra_include}")
+  endforeach()
+
+  if (NOT Z3_MOD_NOT_LIBZ3_COMPONENT)
+    # Add this component to the global list of Z3 components for libz3
+    set_property(GLOBAL APPEND PROPERTY Z3_LIBZ3_COMPONENTS ${component_name})
+  endif()
+endmacro()
+
+macro(z3_add_install_tactic_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "install_tactic.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\""
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    VERBATIM
+  )
+endmacro()
+
+macro(z3_add_memory_initializer_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "mem_initializer.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\""
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    VERBATIM
+  )
+endmacro()
+
+macro(z3_add_gparams_register_modules_rule)
+  # Arguments should be component names to use
+  if (ARGC LESS 1)
+    message(FATAL_ERROR "There should be at least one component")
+  endif()
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp\""
+            ${z3_polluted_tree_msg}
+    )
+  endif()
+  z3_expand_dependencies(_expanded_components ${ARGN})
+  # Get paths to search
+  set(_search_paths "")
+  foreach (dependency ${_expanded_components})
+    get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
+    list(APPEND _search_paths ${_dep_include_dirs})
+  endforeach()
+  list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
+  add_custom_command(OUTPUT "gparams_register_modules.cpp"
+    COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    ${_search_paths}
+    DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py"
+            "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+            ${_expanded_components}
+    COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\""
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    VERBATIM
+  )
+endmacro()

contrib/cmake/cmake/z3_add_cxx_flag.cmake

@@ -0,0 +1,22 @@
+include(CheckCXXCompilerFlag)
+include(CMakeParseArguments)
+
+function(z3_add_cxx_flag flag)
+  CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN})
+  string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}")
+  string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}")
+  unset(HAS_${SANITIZED_FLAG_NAME})
+  CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME})
+  if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME})
+    message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it")
+  endif()
+  if (HAS_${SANITIZED_FLAG_NAME})
+    message(STATUS "C++ compiler supports ${flag}")
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}")
+    set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE)
+  else()
+    message(STATUS "C++ compiler does not support ${flag}")
+  endif()
+endfunction()

contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake

@@ -0,0 +1,17 @@
+# The LINK_FLAGS property of a target in CMake is unfortunately a string and
+# not a list. This function takes a list of linker flags and iterates through
+# them to append them as strings to the ``LINK_FLAGS`` property of
+# the specified target.
+# E.g.
+# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static")
+function(z3_append_linker_flag_list_to_target target)
+  if (NOT (TARGET "${target}"))
+    message(FATAL_ERROR "Specified target \"${target}\" is not a target")
+  endif()
+  foreach(flag ${ARGN})
+    #message(STATUS "Appending link flag \"${flag}\" to target ${target}")
+    # Note that space inside the quoted string is required so that the flags
+    # are space separated.
+    set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " ${flag}")
+  endforeach()
+endfunction()

contrib/cmake/examples/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_subdirectory(c)
+add_subdirectory(c++)

contrib/cmake/examples/c++/CMakeLists.txt

@@ -0,0 +1,4 @@
+add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp)
+target_link_libraries(cpp_example PRIVATE libz3)
+target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")
+target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++")

contrib/cmake/examples/c/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_executable(c_example EXCLUDE_FROM_ALL test_capi.c)
+target_link_libraries(c_example PRIVATE libz3)
+target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api")

contrib/cmake/maintainers.txt

@@ -0,0 +1,3 @@
+# Maintainers
+
+- Dan Liew (@delcypher)

contrib/cmake/src/CMakeLists.txt

@@ -0,0 +1,225 @@
+################################################################################
+# API header files
+################################################################################
+# This lists the API header files that are scanned by
+# some of the build rules to generate some files needed
+# by the build
+set(Z3_API_HEADER_FILES_TO_SCAN
+  z3_api.h
+  z3_ast_containers.h
+  z3_algebraic.h
+  z3_polynomial.h
+  z3_rcf.h
+  z3_fixedpoint.h
+  z3_optimization.h
+  z3_interp.h
+  z3_fpa.h
+)
+set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
+foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
+  set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
+  list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
+  if (NOT EXISTS "${full_path_api_header_file}")
+    message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
+  endif()
+endforeach()
+
+################################################################################
+# Traverse directories each adding a Z3 component
+################################################################################
+# I'm duplicating the order in ``mk_project.py`` for now to help us keep
+# the build systems in sync.
+#
+# The components in these directory explicitly declare their dependencies so
+# you may be able to re-order some of these directories but an error will be
+# raised if you try to declare a component is dependent on another component
+# that has not yet been declared.
+add_subdirectory(util)
+add_subdirectory(math/polynomial)
+add_subdirectory(sat)
+add_subdirectory(nlsat)
+add_subdirectory(math/hilbert)
+add_subdirectory(math/simplex)
+add_subdirectory(math/automata)
+add_subdirectory(math/interval)
+add_subdirectory(math/realclosure)
+add_subdirectory(math/subpaving)
+add_subdirectory(ast)
+add_subdirectory(ast/rewriter)
+add_subdirectory(ast/normal_forms)
+add_subdirectory(model)
+add_subdirectory(tactic)
+add_subdirectory(ast/substitution)
+add_subdirectory(parsers/util)
+add_subdirectory(math/grobner)
+add_subdirectory(math/euclid)
+add_subdirectory(tactic/core)
+add_subdirectory(sat/tactic)
+add_subdirectory(tactic/arith)
+add_subdirectory(nlsat/tactic)
+add_subdirectory(math/subpaving/tactic)
+add_subdirectory(tactic/aig)
+add_subdirectory(solver)
+add_subdirectory(ackermannization)
+add_subdirectory(interp)
+add_subdirectory(cmd_context)
+add_subdirectory(cmd_context/extra_cmds)
+add_subdirectory(parsers/smt2)
+add_subdirectory(ast/proof_checker)
+## Simplifier module will be deleted in the future.
+## It has been replaced with rewriter component.
+add_subdirectory(ast/simplifier)
+add_subdirectory(ast/fpa)
+add_subdirectory(ast/macros)
+add_subdirectory(ast/pattern)
+add_subdirectory(ast/rewriter/bit_blaster)
+add_subdirectory(smt/params)
+add_subdirectory(smt/proto_model)
+add_subdirectory(smt)
+add_subdirectory(tactic/bv)
+add_subdirectory(smt/tactic)
+add_subdirectory(tactic/sls)
+add_subdirectory(qe)
+add_subdirectory(duality)
+add_subdirectory(muz/base)
+add_subdirectory(muz/dataflow)
+add_subdirectory(muz/transforms)
+add_subdirectory(muz/rel)
+add_subdirectory(muz/pdr)
+add_subdirectory(muz/clp)
+add_subdirectory(muz/tab)
+add_subdirectory(muz/bmc)
+add_subdirectory(muz/ddnf)
+add_subdirectory(muz/duality)
+add_subdirectory(muz/fp)
+add_subdirectory(tactic/nlsat_smt)
+add_subdirectory(tactic/ufbv)
+add_subdirectory(sat/sat_solver)
+add_subdirectory(tactic/smtlogics)
+add_subdirectory(tactic/fpa)
+add_subdirectory(tactic/portfolio)
+add_subdirectory(parsers/smt)
+add_subdirectory(opt)
+add_subdirectory(api)
+add_subdirectory(api/dll)
+
+################################################################################
+# libz3
+################################################################################
+get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
+set (object_files "")
+foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
+  list(APPEND object_files $<TARGET_OBJECTS:${component}>)
+endforeach()
+if (BUILD_LIBZ3_SHARED)
+  set(lib_type "SHARED")
+else()
+  set(lib_type "STATIC")
+endif()
+add_library(libz3 ${lib_type} ${object_files})
+# FIXME: Set "VERSION" and "SOVERSION" properly
+set_target_properties(libz3 PROPERTIES
+  # FIXME: Should we be using ${Z3_VERSION} here?
+  # VERSION: Sets up symlinks, does it do anything else?
+  VERSION ${Z3_VERSION}
+  # SOVERSION: On platforms that use ELF this sets the API version
+  # and should be incremented everytime the API changes
+  SOVERSION ${Z3_VERSION})
+
+if (NOT MSVC)
+  # On UNIX like platforms if we don't change the OUTPUT_NAME
+  # the library gets a name like ``liblibz3.so`` so we change it
+  # here. We don't do a rename with MSVC because we get file naming
+  # conflicts (the z3 executable also has this OUTPUT_NAME) with
+  # ``.ilk``, ``.pdb``, ``.lib`` and ``.exp`` files sharing the same
+  # prefix.
+  set_target_properties(libz3 PROPERTIES OUTPUT_NAME z3)
+endif()
+
+# Using INTERFACE means that targets that try link against libz3 will
+# automatically link against the libs in Z3_DEPENDENT_LIBS
+target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS})
+
+z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+
+# Declare which header file are the public header files of libz3
+# these will automatically installed when the libz3 target is installed
+set (libz3_public_headers
+  z3_algebraic.h
+  z3_api.h
+  z3_ast_containers.h
+  z3_fixedpoint.h
+  z3_fpa.h
+  z3.h
+  c++/z3++.h
+  z3_interp.h
+  z3_macros.h
+  z3_optimization.h
+  z3_polynomial.h
+  z3_rcf.h
+  z3_v1.h
+)
+foreach (header ${libz3_public_headers})
+  set_property(TARGET libz3 APPEND PROPERTY
+    PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}")
+endforeach()
+
+install(TARGETS libz3
+  LIBRARY DESTINATION "${Z3_INSTALL_LIB_DIR}"
+  ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}"
+  PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}"
+)
+
+if (MSVC)
+  # Handle settings dll exports when using MSVC
+  # FIXME: This seems unnecessarily complicated but I'm doing
+  # this because this is what the python build system does.
+  # CMake has a much more elegant (see ``GenerateExportHeader.cmake``)
+  # way of handling this.
+  set(dll_module_exports_file "${CMAKE_CURRENT_BINARY_DIR}/api_dll.def")
+  add_custom_command(OUTPUT "${dll_module_exports_file}"
+    COMMAND
+      "${PYTHON_EXECUTABLE}"
+      "${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
+      "${dll_module_exports_file}"
+      "libz3"
+      ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    DEPENDS
+      "${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py"
+      "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+      ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    COMMENT "Generating \"${dll_module_exports_file}\""
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+    VERBATIM
+  )
+  add_custom_target(libz3_extra_depends
+    DEPENDS "${dll_module_exports_file}"
+  )
+  add_dependencies(libz3 libz3_extra_depends)
+  z3_append_linker_flag_list_to_target(libz3 "/DEF:${dll_module_exports_file}")
+endif()
+
+################################################################################
+# Z3 executable
+################################################################################
+add_subdirectory(shell)
+
+################################################################################
+# z3-test
+################################################################################
+add_subdirectory(test)
+
+
+################################################################################
+# Z3 API bindings
+################################################################################
+option(BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
+if (BUILD_PYTHON_BINDINGS)
+  if (NOT BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The python bindings will not work with a static libz3. "
+            "You either need to disable BUILD_PYTHON_BINDINGS or enable BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/python)
+endif()
+
+# TODO: Implement support for other bindigns

contrib/cmake/src/ackermannization/CMakeLists.txt

@@ -0,0 +1,20 @@
+z3_add_component(ackermannization
+  SOURCES
+    ackermannize_bv_model_converter.cpp
+    ackermannize_bv_tactic.cpp
+    ackr_bound_probe.cpp
+    ackr_helper.cpp
+    ackr_model_converter.cpp
+    lackr.cpp
+    lackr_model_constructor.cpp
+    lackr_model_converter_lazy.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    model
+    rewriter
+    solver
+    tactic
+  PYG_FILES
+    ackermannization_params.pyg
+    ackermannize_bv_tactic_params.pyg
+)

contrib/cmake/src/api/CMakeLists.txt

@@ -0,0 +1,72 @@
+set(generated_files
+  api_commands.cpp
+  api_log_macros.cpp
+  api_log_macros.h
+)
+
+# Sanity check
+foreach (gen_file ${generated_files})
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\""
+            ${z3_polluted_tree_msg})
+  endif()
+endforeach()
+
+set(full_path_generated_files "")
+foreach (gen_file ${generated_files})
+  list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}")
+endforeach()
+
+add_custom_command(OUTPUT ${generated_files}
+  COMMAND "${PYTHON_EXECUTABLE}"
+  "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+  ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+  "--api_output_dir"
+  "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+          ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+  COMMENT "Generating ${generated_files}"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  VERBATIM
+)
+
+z3_add_component(api
+  SOURCES
+    api_algebraic.cpp
+    api_arith.cpp
+    api_array.cpp
+    api_ast.cpp
+    api_ast_map.cpp
+    api_ast_vector.cpp
+    api_bv.cpp
+    api_config_params.cpp
+    api_context.cpp
+    api_datalog.cpp
+    api_datatype.cpp
+    api_fpa.cpp
+    api_goal.cpp
+    api_interp.cpp
+    api_log.cpp
+    api_model.cpp
+    api_numeral.cpp
+    api_opt.cpp
+    api_params.cpp
+    api_parsers.cpp
+    api_pb.cpp
+    api_polynomial.cpp
+    api_quant.cpp
+    api_rcf.cpp
+    api_seq.cpp
+    api_solver.cpp
+    api_stats.cpp
+    api_tactic.cpp
+    z3_replayer.cpp
+    ${full_path_generated_files}
+  COMPONENT_DEPENDENCIES
+    interp
+    opt
+    portfolio
+    realclosure
+    smtparser
+)

contrib/cmake/src/api/dll/CMakeLists.txt

@@ -0,0 +1,13 @@
+set(api_dll_deps api extra_cmds sat)
+z3_add_component(api_dll
+  SOURCES
+    dll.cpp
+    "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+    "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+    "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  COMPONENT_DEPENDENCIES
+    ${api_dll_deps}
+)
+z3_add_install_tactic_rule(${api_dll_deps})
+z3_add_memory_initializer_rule(${api_dll_deps})
+z3_add_gparams_register_modules_rule(${api_dll_deps})

contrib/cmake/src/api/python/CMakeLists.txt

@@ -0,0 +1,107 @@
+message(STATUS "Emitting rules to build Z3 python bindings")
+###############################################################################
+# Add target to build python bindings for the build directory
+###############################################################################
+# This allows the python bindings to be used directly from the build directory
+set(z3py_files
+  z3.py
+  z3num.py
+  z3poly.py
+  z3printer.py
+  z3rcf.py
+  z3test.py
+  z3types.py
+  z3util.py
+)
+
+set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}")
+
+set(build_z3_python_bindings_target_depends "")
+foreach (z3py_file ${z3py_files})
+  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}"
+    COMMAND "${CMAKE_COMMAND}" "-E" "copy"
+      "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
+      "${z3py_bindings_build_dest}"
+    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
+    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}"
+  )
+  list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}")
+endforeach()
+
+# Generate z3core.py
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--z3py-output-dir"
+    "${z3py_bindings_build_dest}"
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating z3core.py"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3core.py")
+
+# Generate z3consts.py
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--z3py-output-dir"
+    "${z3py_bindings_build_dest}"
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating z3consts.py"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3consts.py")
+
+# Convenient top-level target
+add_custom_target(build_z3_python_bindings
+  ALL
+  DEPENDS
+    ${build_z3_python_bindings_target_depends}
+)
+
+###############################################################################
+# Install
+###############################################################################
+option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
+if (INSTALL_PYTHON_BINDINGS)
+  # Determine the installation path for the bindings
+  message(STATUS "Emitting rules to install Z3 python bindings")
+  execute_process(
+    COMMAND "${PYTHON_EXECUTABLE}" "-c"
+      "import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
+    RESULT_VARIABLE exit_code
+    OUTPUT_VARIABLE python_pkg_dir
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+  )
+
+  if (NOT ("${exit_code}" EQUAL 0))
+    message(FATAL_ERROR "Failed to determine your Python package directory")
+  endif()
+  message(STATUS "Detected Python package directory: \"${python_pkg_dir}\"")
+
+  # Check if path exists under the install prefix
+  set(python_install_dir "")
+  string(FIND "${python_pkg_dir}" "${CMAKE_INSTALL_PREFIX}" position)
+  if (NOT ("${position}" EQUAL 0))
+    message(WARNING "The detected Python package directory \"${python_pkg_dir}\" "
+            "does not exist under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
+            " Running the install target may lead to a broken installation."
+           )
+  endif()
+  # Using DESTDIR still seems to work even if we use an absolute path
+  set(python_install_dir "${python_pkg_dir}")
+  message(STATUS "Python bindings will be installed to \"${python_install_dir}\"")
+  install(FILES ${build_z3_python_bindings_target_depends}
+    DESTINATION "${python_install_dir}"
+  )
+else()
+  message(STATUS "Not emitting rules to install Z3 python bindings")
+endif()

contrib/cmake/src/ast/CMakeLists.txt

@@ -0,0 +1,48 @@
+z3_add_component(ast
+  SOURCES
+    act_cache.cpp
+    arith_decl_plugin.cpp
+    array_decl_plugin.cpp
+    ast.cpp
+    ast_ll_pp.cpp
+    ast_lt.cpp
+    ast_pp_util.cpp
+    ast_printer.cpp
+    ast_smt2_pp.cpp
+    ast_smt_pp.cpp
+    ast_translation.cpp
+    ast_util.cpp
+    bv_decl_plugin.cpp
+    datatype_decl_plugin.cpp
+    decl_collector.cpp
+    dl_decl_plugin.cpp
+    expr2polynomial.cpp
+    expr2var.cpp
+    expr_abstract.cpp
+    expr_functors.cpp
+    expr_map.cpp
+    expr_stat.cpp
+    expr_substitution.cpp
+    for_each_ast.cpp
+    for_each_expr.cpp
+    format.cpp
+    fpa_decl_plugin.cpp
+    func_decl_dependencies.cpp
+    has_free_vars.cpp
+    macro_substitution.cpp
+    num_occurs.cpp
+    occurs.cpp
+    pb_decl_plugin.cpp
+    pp.cpp
+    reg_decl_plugins.cpp
+    seq_decl_plugin.cpp
+    shared_occs.cpp
+    static_features.cpp
+    used_vars.cpp
+    well_sorted.cpp
+  COMPONENT_DEPENDENCIES
+    polynomial
+    util # Unnecessary? polynomial already depends on util
+  PYG_FILES
+    pp_params.pyg
+)

contrib/cmake/src/ast/fpa/CMakeLists.txt

@@ -0,0 +1,10 @@
+z3_add_component(fpa
+  SOURCES
+    fpa2bv_converter.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    simplifier
+    util
+  PYG_FILES
+    fpa2bv_rewriter_params.pyg
+)

contrib/cmake/src/ast/macros/CMakeLists.txt

@@ -0,0 +1,9 @@
+z3_add_component(macros
+  SOURCES
+    macro_finder.cpp
+    macro_manager.cpp
+    macro_util.cpp
+    quasi_macros.cpp
+  COMPONENT_DEPENDENCIES
+    simplifier
+)

contrib/cmake/src/ast/normal_forms/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(normal_forms
+  SOURCES
+    defined_names.cpp
+    name_exprs.cpp
+    nnf.cpp
+    pull_quant.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    nnf_params.pyg
+)

contrib/cmake/src/ast/pattern/CMakeLists.txt

@@ -0,0 +1,36 @@
+# If this code for adding the rule to generate the database file is ever needed
+# for other components then we should refactor this code into
+# z3_add_component()
+if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h")
+  message(FATAL_ERROR "The generated file \"database.h\""
+          ${z3_polluted_tree_msg})
+endif()
+
+add_custom_command(OUTPUT "database.h"
+  COMMAND "${PYTHON_EXECUTABLE}"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
+          "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
+          "${CMAKE_CURRENT_BINARY_DIR}/database.h"
+  MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2"
+  DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py"
+          "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating \"database.h\""
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  VERBATIM
+)
+
+z3_add_component(pattern
+  SOURCES
+    expr_pattern_match.cpp
+    pattern_inference.cpp
+    pattern_inference_params.cpp
+    # Let CMake know this target depends on this generated
+    # header file
+    ${CMAKE_CURRENT_BINARY_DIR}/database.h
+  COMPONENT_DEPENDENCIES
+    normal_forms
+    simplifier
+    smt2parser
+  PYG_FILES
+    pattern_inference_params_helper.pyg
+)

contrib/cmake/src/ast/proof_checker/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(proof_checker
+  SOURCES
+    proof_checker.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+)

contrib/cmake/src/ast/rewriter/CMakeLists.txt

@@ -0,0 +1,34 @@
+z3_add_component(rewriter
+  SOURCES
+    arith_rewriter.cpp
+    array_rewriter.cpp
+    ast_counter.cpp
+    bool_rewriter.cpp
+    bv_rewriter.cpp
+    datatype_rewriter.cpp
+    der.cpp
+    dl_rewriter.cpp
+    expr_replacer.cpp
+    expr_safe_replace.cpp
+    factor_rewriter.cpp
+    fpa_rewriter.cpp
+    mk_simplified_app.cpp
+    pb_rewriter.cpp
+    quant_hoist.cpp
+    rewriter.cpp
+    seq_rewriter.cpp
+    th_rewriter.cpp
+    var_subst.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    automata
+    polynomial
+  PYG_FILES
+    arith_rewriter_params.pyg
+    array_rewriter_params.pyg
+    bool_rewriter_params.pyg
+    bv_rewriter_params.pyg
+    fpa_rewriter_params.pyg
+    poly_rewriter_params.pyg
+    rewriter_params.pyg
+)

contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(bit_blaster
+  SOURCES
+    bit_blaster.cpp
+    bit_blaster_rewriter.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+    simplifier
+)

contrib/cmake/src/ast/simplifier/CMakeLists.txt

@@ -0,0 +1,30 @@
+z3_add_component(simplifier
+  SOURCES
+    arith_simplifier_params.cpp
+    arith_simplifier_plugin.cpp
+    array_simplifier_params.cpp
+    array_simplifier_plugin.cpp
+    basic_simplifier_plugin.cpp
+    bit2int.cpp
+    bv_elim.cpp
+    bv_simplifier_params.cpp
+    bv_simplifier_plugin.cpp
+    datatype_simplifier_plugin.cpp
+    distribute_forall.cpp
+    elim_bounds.cpp
+    fpa_simplifier_plugin.cpp
+    inj_axiom.cpp
+    maximise_ac_sharing.cpp
+    poly_simplifier_plugin.cpp
+    pull_ite_tree.cpp
+    push_app_ite.cpp
+    seq_simplifier_plugin.cpp
+    simplifier.cpp
+    simplifier_plugin.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    arith_simplifier_params_helper.pyg
+    array_simplifier_params_helper.pyg
+    bv_simplifier_params_helper.pyg
+)

contrib/cmake/src/ast/substitution/CMakeLists.txt

@@ -0,0 +1,10 @@
+z3_add_component(substitution
+  SOURCES
+    matcher.cpp
+    substitution.cpp
+    substitution_tree.cpp
+    unifier.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    rewriter
+)

contrib/cmake/src/cmd_context/CMakeLists.txt

@@ -0,0 +1,21 @@
+z3_add_component(cmd_context
+  SOURCES
+    basic_cmds.cpp
+    check_logic.cpp
+    cmd_context.cpp
+    cmd_context_to_goal.cpp
+    cmd_util.cpp
+    context_params.cpp
+    echo_tactic.cpp
+    eval_cmd.cpp
+    interpolant_cmds.cpp
+    parametric_cmd.cpp
+    pdecl.cpp
+    simplify_cmd.cpp
+    tactic_cmds.cpp
+    tactic_manager.cpp
+  COMPONENT_DEPENDENCIES
+    interp
+    rewriter
+    solver
+)

contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt

@@ -0,0 +1,10 @@
+z3_add_component(extra_cmds
+  SOURCES
+    dbg_cmds.cpp
+    polynomial_cmds.cpp
+    subpaving_cmds.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    cmd_context
+    subpaving_tactic
+)

contrib/cmake/src/duality/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(duality
+  SOURCES
+    duality_profiling.cpp
+    duality_rpfp.cpp
+    duality_solver.cpp
+    duality_wrapper.cpp
+  COMPONENT_DEPENDENCIES
+    interp
+    qe
+    smt
+)

contrib/cmake/src/interp/CMakeLists.txt

@@ -0,0 +1,19 @@
+z3_add_component(interp
+  SOURCES
+    iz3base.cpp
+    iz3checker.cpp
+    iz3foci.cpp
+    iz3interp.cpp
+    iz3mgr.cpp
+    iz3pp.cpp
+    iz3profiling.cpp
+    iz3proof.cpp
+    iz3proof_itp.cpp
+    iz3scopes.cpp
+    iz3translate.cpp
+    iz3translate_direct.cpp
+  COMPONENT_DEPENDENCIES
+    solver
+  PYG_FILES
+    interp_params.pyg
+)

contrib/cmake/src/math/automata/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(automata
+  SOURCES
+    automaton.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)

contrib/cmake/src/math/euclid/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(euclid
+  SOURCES
+    euclidean_solver.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)

contrib/cmake/src/math/grobner/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(grobner
+  SOURCES
+    grobner.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+)

contrib/cmake/src/math/hilbert/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(hilbert
+  SOURCES
+    hilbert_basis.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)

contrib/cmake/src/math/interval/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(interval
+  SOURCES
+    interval_mpq.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)

contrib/cmake/src/math/polynomial/CMakeLists.txt

@@ -0,0 +1,16 @@
+z3_add_component(polynomial
+  SOURCES
+    algebraic_numbers.cpp
+    polynomial_cache.cpp
+    polynomial.cpp
+    polynomial_factorization.cpp
+    rpolynomial.cpp
+    sexpr2upolynomial.cpp
+    upolynomial.cpp
+    upolynomial_factorization.cpp
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    algebraic_params.pyg
+)
+

contrib/cmake/src/math/realclosure/CMakeLists.txt

@@ -0,0 +1,9 @@
+z3_add_component(realclosure
+  SOURCES
+    mpz_matrix.cpp
+    realclosure.cpp
+  COMPONENT_DEPENDENCIES
+    interval
+  PYG_FILES
+    rcf_params.pyg
+)

contrib/cmake/src/math/simplex/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(simplex
+  SOURCES
+    simplex.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)

contrib/cmake/src/math/subpaving/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(subpaving
+  SOURCES
+    subpaving.cpp
+    subpaving_hwf.cpp
+    subpaving_mpf.cpp
+    subpaving_mpff.cpp
+    subpaving_mpfx.cpp
+    subpaving_mpq.cpp
+  COMPONENT_DEPENDENCIES
+    interval
+)

contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(subpaving_tactic
+  SOURCES
+    expr2subpaving.cpp
+    subpaving_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    subpaving
+)

contrib/cmake/src/model/CMakeLists.txt

@@ -0,0 +1,18 @@
+z3_add_component(model
+  SOURCES
+    func_interp.cpp
+    model2expr.cpp
+    model_core.cpp
+    model.cpp
+    model_evaluator.cpp
+    model_implicant.cpp
+    model_pp.cpp
+    model_smt2_pp.cpp
+    model_v2_pp.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+  PYG_FILES
+    model_evaluator_params.pyg
+    model_params.pyg
+)
+

contrib/cmake/src/muz/base/CMakeLists.txt

@@ -0,0 +1,23 @@
+z3_add_component(muz
+  SOURCES
+    bind_variables.cpp
+    dl_boogie_proof.cpp
+    dl_context.cpp
+    dl_costs.cpp
+    dl_rule.cpp
+    dl_rule_set.cpp
+    dl_rule_subsumption_index.cpp
+    dl_rule_transformer.cpp
+    dl_util.cpp
+    hnf.cpp
+    proof_utils.cpp
+    rule_properties.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    qe
+    sat
+    smt
+    smt2parser
+  PYG_FILES
+    fixedpoint_params.pyg
+)

contrib/cmake/src/muz/bmc/CMakeLists.txt

@@ -0,0 +1,7 @@
+z3_add_component(bmc
+  SOURCES
+    dl_bmc_engine.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)

contrib/cmake/src/muz/clp/CMakeLists.txt

@@ -0,0 +1,7 @@
+z3_add_component(clp
+  SOURCES
+    clp_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)

contrib/cmake/src/muz/dataflow/CMakeLists.txt

@@ -0,0 +1,6 @@
+z3_add_component(dataflow
+  SOURCES
+    dataflow.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+)

contrib/cmake/src/muz/ddnf/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(ddnf
+  SOURCES
+    ddnf.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    rel
+    transforms
+)

contrib/cmake/src/muz/duality/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(duality_intf
+  SOURCES
+    duality_dl_interface.cpp
+  COMPONENT_DEPENDENCIES
+    duality
+    muz
+    transforms
+)

contrib/cmake/src/muz/fp/CMakeLists.txt

@@ -0,0 +1,16 @@
+z3_add_component(fp
+  SOURCES
+    datalog_parser.cpp
+    dl_cmds.cpp
+    dl_register_engine.cpp
+    horn_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bmc
+    clp
+    ddnf
+    duality_intf
+    muz
+    pdr
+    rel
+    tab
+)

contrib/cmake/src/muz/pdr/CMakeLists.txt

@@ -0,0 +1,20 @@
+z3_add_component(pdr
+  SOURCES
+    pdr_closure.cpp
+    pdr_context.cpp
+    pdr_dl_interface.cpp
+    pdr_farkas_learner.cpp
+    pdr_generalizers.cpp
+    pdr_manager.cpp
+    pdr_prop_solver.cpp
+    pdr_reachable_cache.cpp
+    pdr_smt_context_manager.cpp
+    pdr_sym_mux.cpp
+    pdr_util.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    core_tactics
+    muz
+    smt_tactic
+    transforms
+)

contrib/cmake/src/muz/rel/CMakeLists.txt

@@ -0,0 +1,32 @@
+z3_add_component(rel
+  SOURCES
+    aig_exporter.cpp
+    check_relation.cpp
+    dl_base.cpp
+    dl_bound_relation.cpp
+    dl_check_table.cpp
+    dl_compiler.cpp
+    dl_external_relation.cpp
+    dl_finite_product_relation.cpp
+    dl_instruction.cpp
+    dl_interval_relation.cpp
+    dl_lazy_table.cpp
+    dl_mk_explanations.cpp
+    dl_mk_partial_equiv.cpp
+    dl_mk_similarity_compressor.cpp
+    dl_mk_simple_joins.cpp
+    dl_product_relation.cpp
+    dl_relation_manager.cpp
+    dl_sieve_relation.cpp
+    dl_sparse_table.cpp
+    dl_table.cpp
+    dl_table_relation.cpp
+    doc.cpp
+    karr_relation.cpp
+    rel_context.cpp
+    tbv.cpp
+    udoc_relation.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)

contrib/cmake/src/muz/tab/CMakeLists.txt

@@ -0,0 +1,7 @@
+z3_add_component(tab
+  SOURCES
+    tab_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)

contrib/cmake/src/muz/transforms/CMakeLists.txt

@@ -0,0 +1,28 @@
+z3_add_component(transforms
+  SOURCES
+    dl_mk_array_blast.cpp
+    dl_mk_backwards.cpp
+    dl_mk_bit_blast.cpp
+    dl_mk_coalesce.cpp
+    dl_mk_coi_filter.cpp
+    dl_mk_filter_rules.cpp
+    dl_mk_interp_tail_simplifier.cpp
+    dl_mk_karr_invariants.cpp
+    dl_mk_loop_counter.cpp
+    dl_mk_magic_sets.cpp
+    dl_mk_magic_symbolic.cpp
+    dl_mk_quantifier_abstraction.cpp
+    dl_mk_quantifier_instantiation.cpp
+    dl_mk_rule_inliner.cpp
+    dl_mk_scale.cpp
+    dl_mk_separate_negated_tails.cpp
+    dl_mk_slice.cpp
+    dl_mk_subsumption_checker.cpp
+    dl_mk_unbound_compressor.cpp
+    dl_mk_unfold.cpp
+    dl_transforms.cpp
+  COMPONENT_DEPENDENCIES
+    dataflow
+    hilbert
+    muz
+)

contrib/cmake/src/nlsat/CMakeLists.txt

@@ -0,0 +1,14 @@
+z3_add_component(nlsat
+  SOURCES
+    nlsat_clause.cpp
+    nlsat_evaluator.cpp
+    nlsat_explain.cpp
+    nlsat_interval_set.cpp
+    nlsat_solver.cpp
+    nlsat_types.cpp
+  COMPONENT_DEPENDENCIES
+    polynomial
+    sat
+  PYG_FILES
+    nlsat_params.pyg
+)

contrib/cmake/src/nlsat/tactic/CMakeLists.txt

@@ -0,0 +1,10 @@
+z3_add_component(nlsat_tactic
+  SOURCES
+    goal2nlsat.cpp
+    nlsat_tactic.cpp
+    qfnra_nlsat_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    nlsat
+    sat_tactic
+)

contrib/cmake/src/opt/CMakeLists.txt

@@ -0,0 +1,26 @@
+z3_add_component(opt
+  SOURCES
+    bcd2.cpp
+    fu_malik.cpp
+    hitting_sets.cpp
+    maxhs.cpp
+    maxres.cpp
+    maxsls.cpp
+    maxsmt.cpp
+    mss.cpp
+    mus.cpp
+    opt_cmds.cpp
+    opt_context.cpp
+    opt_pareto.cpp
+    optsmt.cpp
+    opt_solver.cpp
+    pb_sls.cpp
+    wmax.cpp
+  COMPONENT_DEPENDENCIES
+    sat_solver
+    sls_tactic
+    smt
+    smtlogic_tactics
+  PYG_FILES
+    opt_params.pyg
+)

contrib/cmake/src/parsers/smt/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(smtparser
+  SOURCES
+    smtlib.cpp
+    smtlib_solver.cpp
+    smtparser.cpp
+  COMPONENT_DEPENDENCIES
+    portfolio
+)

contrib/cmake/src/parsers/smt2/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(smt2parser
+  SOURCES
+    smt2parser.cpp
+    smt2scanner.cpp
+  COMPONENT_DEPENDENCIES
+    cmd_context
+    parser_util
+)

contrib/cmake/src/parsers/util/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(parser_util
+  SOURCES
+    cost_parser.cpp
+    pattern_validation.cpp
+    scanner.cpp
+    simple_parser.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+  PYG_FILES
+    parser_params.pyg
+)

contrib/cmake/src/qe/CMakeLists.txt

@@ -0,0 +1,21 @@
+z3_add_component(qe
+  SOURCES
+    nlarith_util.cpp
+    qe_arith.cpp
+    qe_arith_plugin.cpp
+    qe_array_plugin.cpp
+    qe_bool_plugin.cpp
+    qe_bv_plugin.cpp
+    qe_cmd.cpp
+    qe.cpp
+    qe_datatype_plugin.cpp
+    qe_dl_plugin.cpp
+    qe_lite.cpp
+    qe_sat_tactic.cpp
+    qe_tactic.cpp
+    qe_util.cpp
+    vsubst_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    sat
+    smt
+)

contrib/cmake/src/sat/CMakeLists.txt

@@ -0,0 +1,29 @@
+z3_add_component(sat
+  SOURCES
+    dimacs.cpp
+    sat_asymm_branch.cpp
+    sat_bceq.cpp
+    sat_clause.cpp
+    sat_clause_set.cpp
+    sat_clause_use_list.cpp
+    sat_cleaner.cpp
+    sat_config.cpp
+    sat_elim_eqs.cpp
+    sat_iff3_finder.cpp
+    sat_integrity_checker.cpp
+    sat_model_converter.cpp
+    sat_mus.cpp
+    sat_probing.cpp
+    sat_scc.cpp
+    sat_simplifier.cpp
+    sat_sls.cpp
+    sat_solver.cpp
+    sat_watched.cpp
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    sat_asymm_branch_params.pyg
+    sat_params.pyg
+    sat_scc_params.pyg
+    sat_simplifier_params.pyg
+)

contrib/cmake/src/sat/sat_solver/CMakeLists.txt

@@ -0,0 +1,11 @@
+z3_add_component(sat_solver
+  SOURCES
+    inc_sat_solver.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    arith_tactics
+    bv_tactics
+    core_tactics
+    sat_tactic
+    solver
+)

contrib/cmake/src/sat/tactic/CMakeLists.txt

@@ -0,0 +1,9 @@
+z3_add_component(sat_tactic
+  SOURCES
+    atom2bool_var.cpp
+    goal2sat.cpp
+    sat_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    sat
+    tactic
+)

contrib/cmake/src/shell/CMakeLists.txt

@@ -0,0 +1,47 @@
+set (shell_object_files "")
+# FIXME: z3 should really link against libz3 and not the
+# individual components. Several things prevent us from
+# doing this
+# * The api_dll component in libz3 shouldn't be used the
+#   the z3 executable.
+# * The z3 executable uses symbols that are hidden in libz3
+
+# We are only using these dependencies to enforce a build
+# order. We don't use this list for actual linking.
+set(shell_deps api extra_cmds opt sat)
+z3_expand_dependencies(shell_expanded_deps ${shell_deps})
+get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
+foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
+  if (NOT ("${component}" STREQUAL "api_dll"))
+    # We don't use the api_dll component in the Z3 executable
+    list(APPEND shell_object_files $<TARGET_OBJECTS:${component}>)
+  endif()
+endforeach()
+add_executable(shell
+  datalog_frontend.cpp
+  dimacs_frontend.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+  "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+  main.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  opt_frontend.cpp
+  smtlib_frontend.cpp
+  z3_log_frontend.cpp
+# FIXME: shell should really link against libz3 but it can't due to requiring
+# use of some hidden symbols. Also libz3 has the ``api_dll`` component which
+# we don't want (I think).
+  ${shell_object_files}
+)
+z3_add_install_tactic_rule(${shell_deps})
+z3_add_memory_initializer_rule(${shell_deps})
+z3_add_gparams_register_modules_rule(${shell_deps})
+set_target_properties(shell PROPERTIES OUTPUT_NAME z3)
+target_compile_definitions(shell PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS})
+z3_add_component_dependencies_to_target(shell ${shell_expanded_deps})
+z3_append_linker_flag_list_to_target(shell ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+install(TARGETS shell
+  RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}"
+)

contrib/cmake/src/smt/CMakeLists.txt

@@ -0,0 +1,77 @@
+z3_add_component(smt
+  SOURCES
+    arith_eq_adapter.cpp
+    arith_eq_solver.cpp
+    asserted_formulas.cpp
+    cached_var_subst.cpp
+    cost_evaluator.cpp
+    dyn_ack.cpp
+    elim_term_ite.cpp
+    expr_context_simplifier.cpp
+    fingerprints.cpp
+    mam.cpp
+    old_interval.cpp
+    qi_queue.cpp
+    smt_almost_cg_table.cpp
+    smt_case_split_queue.cpp
+    smt_cg_table.cpp
+    smt_checker.cpp
+    smt_clause.cpp
+    smt_conflict_resolution.cpp
+    smt_context.cpp
+    smt_context_inv.cpp
+    smt_context_pp.cpp
+    smt_context_stat.cpp
+    smt_enode.cpp
+    smt_farkas_util.cpp
+    smt_for_each_relevant_expr.cpp
+    smt_implied_equalities.cpp
+    smt_internalizer.cpp
+    smt_justification.cpp
+    smt_kernel.cpp
+    smt_literal.cpp
+    smt_model_checker.cpp
+    smt_model_finder.cpp
+    smt_model_generator.cpp
+    smt_quantifier.cpp
+    smt_quantifier_stat.cpp
+    smt_quick_checker.cpp
+    smt_relevancy.cpp
+    smt_setup.cpp
+    smt_solver.cpp
+    smt_statistics.cpp
+    smt_theory.cpp
+    smt_value_sort.cpp
+    theory_arith.cpp
+    theory_array_base.cpp
+    theory_array.cpp
+    theory_array_full.cpp
+    theory_bv.cpp
+    theory_datatype.cpp
+    theory_dense_diff_logic.cpp
+    theory_diff_logic.cpp
+    theory_dl.cpp
+    theory_dummy.cpp
+    theory_fpa.cpp
+    theory_opt.cpp
+    theory_pb.cpp
+    theory_seq.cpp
+    theory_utvpi.cpp
+    theory_wmaxsat.cpp
+    uses_theory.cpp
+    watch_list.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    cmd_context
+    euclid
+    fpa
+    grobner
+    macros
+    normal_forms
+    parser_util
+    pattern
+    proof_checker
+    proto_model
+    simplex
+    substitution
+)

contrib/cmake/src/smt/params/CMakeLists.txt

@@ -0,0 +1,18 @@
+z3_add_component(smt_params
+  SOURCES
+    dyn_ack_params.cpp
+    preprocessor_params.cpp
+    qi_params.cpp
+    smt_params.cpp
+    theory_arith_params.cpp
+    theory_array_params.cpp
+    theory_bv_params.cpp
+    theory_pb_params.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    bit_blaster
+    pattern
+    simplifier
+  PYG_FILES
+    smt_params_helper.pyg
+)

contrib/cmake/src/smt/proto_model/CMakeLists.txt

@@ -0,0 +1,13 @@
+z3_add_component(proto_model
+  SOURCES
+    array_factory.cpp
+    datatype_factory.cpp
+    numeral_factory.cpp
+    proto_model.cpp
+    struct_factory.cpp
+    value_factory.cpp
+  COMPONENT_DEPENDENCIES
+    model
+    simplifier
+    smt_params
+)

contrib/cmake/src/smt/tactic/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(smt_tactic
+  SOURCES
+    ctx_solver_simplify_tactic.cpp
+    smt_tactic.cpp
+    unit_subsumption_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    smt
+)

contrib/cmake/src/solver/CMakeLists.txt

@@ -0,0 +1,13 @@
+z3_add_component(solver
+  SOURCES
+    check_sat_result.cpp
+    combined_solver.cpp
+    solver.cpp
+    solver_na2as.cpp
+    tactic2solver.cpp
+  COMPONENT_DEPENDENCIES
+    model
+    tactic
+  PYG_FILES
+    combined_solver_params.pyg
+)

contrib/cmake/src/tactic/CMakeLists.txt

@@ -0,0 +1,20 @@
+z3_add_component(tactic
+  SOURCES
+    equiv_proof_converter.cpp
+    extension_model_converter.cpp
+    filter_model_converter.cpp
+    goal.cpp
+    goal_num_occurs.cpp
+    goal_shared_occs.cpp
+    goal_util.cpp
+    horn_subsume_model_converter.cpp
+    model_converter.cpp
+    probe.cpp
+    proof_converter.cpp
+    replace_proof_converter.cpp
+    tactical.cpp
+    tactic.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    model
+)

contrib/cmake/src/tactic/aig/CMakeLists.txt

@@ -0,0 +1,7 @@
+z3_add_component(aig_tactic
+  SOURCES
+    aig.cpp
+    aig_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    tactic
+)

contrib/cmake/src/tactic/arith/CMakeLists.txt

@@ -0,0 +1,31 @@
+z3_add_component(arith_tactics
+  SOURCES
+    add_bounds_tactic.cpp
+    arith_bounds_tactic.cpp
+    bound_manager.cpp
+    bound_propagator.cpp
+    bv2int_rewriter.cpp
+    bv2real_rewriter.cpp
+    card2bv_tactic.cpp
+    degree_shift_tactic.cpp
+    diff_neq_tactic.cpp
+    elim01_tactic.cpp
+    eq2bv_tactic.cpp
+    factor_tactic.cpp
+    fix_dl_var_tactic.cpp
+    fm_tactic.cpp
+    lia2card_tactic.cpp
+    lia2pb_tactic.cpp
+    linear_equation.cpp
+    nla2bv_tactic.cpp
+    normalize_bounds_tactic.cpp
+    pb2bv_model_converter.cpp
+    pb2bv_tactic.cpp
+    probe_arith.cpp
+    propagate_ineqs_tactic.cpp
+    purify_arith_tactic.cpp
+    recover_01_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    sat
+)

contrib/cmake/src/tactic/bv/CMakeLists.txt

@@ -0,0 +1,16 @@
+z3_add_component(bv_tactics
+  SOURCES
+    bit_blaster_model_converter.cpp
+    bit_blaster_tactic.cpp
+    bv1_blaster_tactic.cpp
+    bvarray2uf_rewriter.cpp
+    bvarray2uf_tactic.cpp
+    bv_bounds_tactic.cpp
+    bv_size_reduction_tactic.cpp
+    elim_small_bv_tactic.cpp
+    max_bv_sharing_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    core_tactics
+    tactic
+)

contrib/cmake/src/tactic/core/CMakeLists.txt

@@ -0,0 +1,25 @@
+z3_add_component(core_tactics
+  SOURCES
+    blast_term_ite_tactic.cpp
+    cofactor_elim_term_ite.cpp
+    cofactor_term_ite_tactic.cpp
+    ctx_simplify_tactic.cpp
+    der_tactic.cpp
+    distribute_forall_tactic.cpp
+    elim_term_ite_tactic.cpp
+    elim_uncnstr_tactic.cpp
+    nnf_tactic.cpp
+    occf_tactic.cpp
+    pb_preprocess_tactic.cpp
+    propagate_values_tactic.cpp
+    reduce_args_tactic.cpp
+    simplify_tactic.cpp
+    solve_eqs_tactic.cpp
+    split_clause_tactic.cpp
+    symmetry_reduce_tactic.cpp
+    tseitin_cnf_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    normal_forms
+    tactic
+)
+

contrib/cmake/src/tactic/fpa/CMakeLists.txt

@@ -0,0 +1,14 @@
+z3_add_component(fpa_tactics
+  SOURCES
+    fpa2bv_model_converter.cpp
+    fpa2bv_tactic.cpp
+    qffp_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    arith_tactics
+    bv_tactics
+    core_tactics
+    fpa
+    sat_tactic
+    smtlogic_tactics
+    smt_tactic
+)

contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt

@@ -0,0 +1,7 @@
+z3_add_component(nlsat_smt_tactic
+  SOURCES
+    nl_purify_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    nlsat_tactic
+    smt_tactic
+)

contrib/cmake/src/tactic/portfolio/CMakeLists.txt

@@ -0,0 +1,15 @@
+z3_add_component(portfolio
+  SOURCES
+    default_tactic.cpp
+    smt_strategic_solver.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    fp
+    fpa_tactics
+    qe
+    sat_solver
+    sls_tactic
+    smtlogic_tactics
+    subpaving_tactic
+    ufbv_tactic
+)

contrib/cmake/src/tactic/sls/CMakeLists.txt

@@ -0,0 +1,13 @@
+z3_add_component(sls_tactic
+  SOURCES
+    bvsls_opt_engine.cpp
+    sls_engine.cpp
+    sls_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bv_tactics
+    core_tactics
+    normal_forms
+    tactic
+  PYG_FILES
+    sls_params.pyg
+)

contrib/cmake/src/tactic/smtlogics/CMakeLists.txt

@@ -0,0 +1,31 @@
+z3_add_component(smtlogic_tactics
+  SOURCES
+    nra_tactic.cpp
+    qfaufbv_tactic.cpp
+    qfauflia_tactic.cpp
+    qfbv_tactic.cpp
+    qfidl_tactic.cpp
+    qflia_tactic.cpp
+    qflra_tactic.cpp
+    qfnia_tactic.cpp
+    qfnra_tactic.cpp
+    qfufbv_ackr_model_converter.cpp
+    qfufbv_tactic.cpp
+    qfufnra_tactic.cpp
+    qfuf_tactic.cpp
+    quant_tactics.cpp
+  COMPONENT_DEPENDENCIES
+    ackermannization
+    aig_tactic
+    arith_tactics
+    bv_tactics
+    fp
+    muz
+    nlsat_tactic
+    nlsat_smt_tactic
+    qe
+    sat_solver
+    smt_tactic
+  PYG_FILES
+    qfufbv_tactic_params.pyg
+)

contrib/cmake/src/tactic/ufbv/CMakeLists.txt

@@ -0,0 +1,14 @@
+z3_add_component(ufbv_tactic
+  SOURCES
+    macro_finder_tactic.cpp
+    quasi_macros_tactic.cpp
+    ufbv_rewriter.cpp
+    ufbv_rewriter_tactic.cpp
+    ufbv_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    core_tactics
+    macros
+    normal_forms
+    rewriter
+    smt_tactic
+)

contrib/cmake/src/test/CMakeLists.txt

@@ -0,0 +1,126 @@
+add_subdirectory(fuzzing)
+################################################################################
+# z3-test executable
+################################################################################
+set(z3_test_deps api fuzzing simplex)
+z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
+set (z3_test_extra_object_files "")
+foreach (component ${z3_test_expanded_deps})
+  list(APPEND z3_test_extra_object_files $<TARGET_OBJECTS:${component}>)
+endforeach()
+add_executable(test-z3
+  EXCLUDE_FROM_ALL
+  algebraic.cpp
+  api_bug.cpp
+  api.cpp
+  arith_rewriter.cpp
+  arith_simplifier_plugin.cpp
+  ast.cpp
+  bit_blaster.cpp
+  bits.cpp
+  bit_vector.cpp
+  buffer.cpp
+  bv_simplifier_plugin.cpp
+  chashtable.cpp
+  check_assumptions.cpp
+  datalog_parser.cpp
+  ddnf.cpp
+  diff_logic.cpp
+  dl_context.cpp
+  dl_product_relation.cpp
+  dl_query.cpp
+  dl_relation.cpp
+  dl_table.cpp
+  dl_util.cpp
+  doc.cpp
+  escaped.cpp
+  ex.cpp
+  expr_rand.cpp
+  expr_substitution.cpp
+  ext_numeral.cpp
+  f2n.cpp
+  factor_rewriter.cpp
+  fixed_bit_vector.cpp
+  for_each_file.cpp
+  get_implied_equalities.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp"
+  hashtable.cpp
+  heap.cpp
+  heap_trie.cpp
+  hilbert_basis.cpp
+  horn_subsume_model_converter.cpp
+  hwf.cpp
+  inf_rational.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp"
+  interval.cpp
+  karr.cpp
+  list.cpp
+  main.cpp
+  map.cpp
+  matcher.cpp
+  "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
+  memory.cpp
+  model2expr.cpp
+  model_retrieval.cpp
+  mpbq.cpp
+  mpf.cpp
+  mpff.cpp
+  mpfx.cpp
+  mpq.cpp
+  mpz.cpp
+  nlarith_util.cpp
+  nlsat.cpp
+  no_overflow.cpp
+  object_allocator.cpp
+  old_interval.cpp
+  optional.cpp
+  parray.cpp
+  pdr.cpp
+  permutation.cpp
+  polynomial.cpp
+  polynomial_factorization.cpp
+  polynorm.cpp
+  prime_generator.cpp
+  proof_checker.cpp
+  qe_arith.cpp
+  quant_elim.cpp
+  quant_solve.cpp
+  random.cpp
+  rational.cpp
+  rcf.cpp
+  region.cpp
+  sat_user_scope.cpp
+  simple_parser.cpp
+  simplex.cpp
+  simplifier.cpp
+  small_object_allocator.cpp
+  smt2print_parse.cpp
+  smt_context.cpp
+  sorting_network.cpp
+  stack.cpp
+  string_buffer.cpp
+  substitution.cpp
+  symbol.cpp
+  symbol_table.cpp
+  tbv.cpp
+  theory_dl.cpp
+  theory_pb.cpp
+  timeout.cpp
+  total_order.cpp
+  trigo.cpp
+  udoc_relation.cpp
+  uint_set.cpp
+  upolynomial.cpp
+  var_subst.cpp
+  vector.cpp
+  ${z3_test_extra_object_files}
+)
+z3_add_install_tactic_rule(${z3_test_deps})
+z3_add_memory_initializer_rule(${z3_test_deps})
+z3_add_gparams_register_modules_rule(${z3_test_deps})
+target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS})
+target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
+z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps})

contrib/cmake/src/test/fuzzing/CMakeLists.txt

@@ -0,0 +1,8 @@
+z3_add_component(fuzzing
+  NOT_LIBZ3_COMPONENT # Don't put this component inside libz3
+  SOURCES
+    expr_delta.cpp
+    expr_rand.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+)

contrib/cmake/src/util/CMakeLists.txt

@@ -0,0 +1,60 @@
+if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
+  message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\""
+          ${z3_polluted_tree_msg}
+  )
+endif()
+configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY)
+
+z3_add_component(util
+  SOURCES
+    approx_nat.cpp
+    approx_set.cpp
+    bit_util.cpp
+    bit_vector.cpp
+    cmd_context_types.cpp
+    common_msgs.cpp
+    cooperate.cpp
+    debug.cpp
+    env_params.cpp
+    fixed_bit_vector.cpp
+    gparams.cpp
+    hash.cpp
+    hwf.cpp
+    inf_int_rational.cpp
+    inf_rational.cpp
+    inf_s_integer.cpp
+    lbool.cpp
+    luby.cpp
+    memory_manager.cpp
+    mpbq.cpp
+    mpf.cpp
+    mpff.cpp
+    mpfx.cpp
+    mpn.cpp
+    mpq.cpp
+    mpq_inf.cpp
+    mpz.cpp
+    page.cpp
+    params.cpp
+    permutation.cpp
+    prime_generator.cpp
+    rational.cpp
+    region.cpp
+    rlimit.cpp
+    scoped_ctrl_c.cpp
+    scoped_timer.cpp
+    sexpr.cpp
+    s_integer.cpp
+    small_object_allocator.cpp
+    smt2_util.cpp
+    stack.cpp
+    statistics.cpp
+    symbol.cpp
+    timeit.cpp
+    timeout.cpp
+    timer.cpp
+    trace.cpp
+    util.cpp
+    warning.cpp
+    z3_exception.cpp
+)

scripts/mk_consts_files.py

@@ -0,0 +1,47 @@
+#!/usr/bin/env python
+"""
+Reads a list of Z3 API header files and
+generate the constant declarations need
+by one or more Z3 language bindings
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def check_dir(output_dir):
+  if not os.path.isdir(output_dir):
+    logging.error('"{}" is not an existing directory'.format(output_dir))
+    return 1
+  return 0
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("api_files", nargs="+")
+  parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
+  pargs = parser.parse_args(args)
+
+  for api_file in pargs.api_files:
+    if not os.path.exists(api_file):
+      logging.error('"{}" does not exist'.format(api_file))
+      return 1
+
+  count = 0
+
+  if pargs.z3py_output_dir:
+    if check_dir(pargs.z3py_output_dir) != 0:
+      return 1
+    mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir)
+    count += 1
+
+  if count == 0:
+    logging.info('No files generated. You need to specific an output directory'
+                 ' for the relevant langauge bindings')
+  # TODO: Add support for other bindings
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_def_file.py

@@ -0,0 +1,36 @@
+#!/usr/bin/env python
+"""
+Reads a list of Z3 API header files and
+generate a ``.def`` file to define the
+exported symbols of a dll. This file
+can be passed to the ``/DEF`` to the
+linker used by MSVC.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("output_file", help="output def file path")
+  parser.add_argument("dllname", help="dllname to use in def file")
+  parser.add_argument("api_files", nargs="+")
+  pargs = parser.parse_args(args)
+
+  for api_file in pargs.api_files:
+    if not os.path.exists(api_file):
+      logging.error('"{}" does not exist'.format(api_file))
+      return 1
+
+  mk_util.mk_def_file_internal(
+    pargs.output_file,
+    pargs.dllname,
+    pargs.api_files)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_gparams_register_modules_cpp.py

@@ -0,0 +1,47 @@
+#!/usr/bin/env python
+"""
+Determines the available global parameters
+in header files in the list of source directions
+and generates a ``gparams_register_modules.cpp`` file in
+the destination directory that defines a function
+``void gparams_register_modules()``.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def check_dir(path):
+  if not os.path.exists(path):
+    logging.error('"{}" does not exist'.format(path))
+    return 1
+
+  if not os.path.isdir(path):
+    logging.error('"{}" is not a directory'.format(path))
+    return 1
+
+  return 0
+
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("destination_dir", help="destination directory")
+  parser.add_argument("source_dirs", nargs="+",
+                      help="One or more source directories to search")
+  pargs = parser.parse_args(args)
+
+  if check_dir(pargs.destination_dir) != 0:
+    return 1
+
+  for source_dir in pargs.source_dirs:
+    if check_dir(source_dir) != 0:
+      return 1
+
+  mk_util.mk_gparams_register_modules_internal(pargs.source_dirs, pargs.destination_dir)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_install_tactic_cpp.py

@@ -0,0 +1,47 @@
+#!/usr/bin/env python
+"""
+Determines the available tactics
+in header files in the list of source directions
+and generates a ``install_tactic.cpp`` file in
+the destination directory that defines a function
+``void install_tactics(tactic_manager& ctx)``.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def check_dir(path):
+  if not os.path.exists(path):
+    logging.error('"{}" does not exist'.format(path))
+    return 1
+
+  if not os.path.isdir(path):
+    logging.error('"{}" is not a directory'.format(path))
+    return 1
+
+  return 0
+
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("destination_dir", help="destination directory")
+  parser.add_argument("source_dirs", nargs="+",
+                      help="One or more source directories to search")
+  pargs = parser.parse_args(args)
+
+  if check_dir(pargs.destination_dir) != 0:
+    return 1
+
+  for source_dir in pargs.source_dirs:
+    if check_dir(source_dir) != 0:
+      return 1
+
+  mk_util.mk_install_tactic_cpp_internal(pargs.source_dirs, pargs.destination_dir)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_mem_initializer_cpp.py

@@ -0,0 +1,48 @@
+#!/usr/bin/env python
+"""
+Scans the source directories for
+memory initializers and finalizers and
+emits and implementation of
+``void mem_initialize()`` and
+``void mem_finalize()`` into ``mem_initializer.cpp``
+in the destination directory.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def check_dir(path):
+  if not os.path.exists(path):
+    logging.error('"{}" does not exist'.format(path))
+    return 1
+
+  if not os.path.isdir(path):
+    logging.error('"{}" is not a directory'.format(path))
+    return 1
+
+  return 0
+
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("destination_dir", help="destination directory")
+  parser.add_argument("source_dirs", nargs="+",
+                      help="One or more source directories to search")
+  pargs = parser.parse_args(args)
+
+  if check_dir(pargs.destination_dir) != 0:
+    return 1
+
+  for source_dir in pargs.source_dirs:
+    if check_dir(source_dir) != 0:
+      return 1
+
+  mk_util.mk_mem_initializer_cpp_internal(pargs.source_dirs, pargs.destination_dir)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_pat_db.py

@@ -0,0 +1,34 @@
+#!/usr/bin/env python
+"""
+Reads a pattern database and generates the corresponding
+header file.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("db_file", help="pattern database file")
+  parser.add_argument("output_file", help="output header file path")
+  pargs = parser.parse_args(args)
+
+  if not os.path.exists(pargs.db_file):
+    logging.error('"{}" does not exist'.format(pargs.db_file))
+    return 1
+
+  if (os.path.exists(pargs.output_file) and
+     not os.path.isfile(pargs.output_file)):
+       logging.error('Refusing to overwrite "{}"'.format(
+         pargs.output_file))
+       return 1
+
+  mk_util.mk_pat_db_internal(pargs.db_file, pargs.output_file)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/mk_util.py

@@ -2504,10 +2504,10 @@ DOUBLE = 2
 STRING = 3
 SYMBOL = 4
 UINT_MAX = 4294967295
-CURR_PYG = None
+CURRENT_PYG_HPP_DEST_DIR = None
 
-def get_curr_pyg():
-    return CURR_PYG
+def get_current_pyg_hpp_dest_dir():
+    return CURRENT_PYG_HPP_DEST_DIR
 
 TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL',  DOUBLE : 'CPK_DOUBLE',  STRING : 'CPK_STRING',  SYMBOL : 'CPK_SYMBOL' }
 TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' }
@@ -2540,8 +2540,8 @@ def to_c_method(s):
     return s.replace('.', '_')
 
 def def_module_params(module_name, export, params, class_name=None, description=None):
-    pyg = get_curr_pyg()
-    dirname = os.path.split(get_curr_pyg())[0]
+    dirname = get_current_pyg_hpp_dest_dir()
+    assert(os.path.exists(dirname))
     if class_name is None:
         class_name = '%s_params' % module_name
     hpp = os.path.join(dirname, '%s.hpp' % class_name)
@@ -2606,28 +2606,31 @@ def _execfile(file, globals=globals(), locals=locals()):
 
 # Execute python auxiliary scripts that generate extra code for Z3.
 def exec_pyg_scripts():
-    global CURR_PYG
+    global CURRENT_PYG_HPP_DEST_DIR
     for root, dirs, files in os.walk('src'):
         for f in files:
             if f.endswith('.pyg'):
                 script = os.path.join(root, f)
-                CURR_PYG = script
+                CURRENT_PYG_HPP_DEST_DIR = root
                 _execfile(script, PYG_GLOBALS)
 
 # TODO: delete after src/ast/pattern/expr_pattern_match
 # database.smt ==> database.h
 def mk_pat_db():
     c = get_component(PATTERN_COMPONENT)
-    fin  = open(os.path.join(c.src_dir, 'database.smt2'), 'r')
-    fout = open(os.path.join(c.src_dir, 'database.h'), 'w')
-    fout.write('static char const g_pattern_database[] =\n')
-    for line in fin:
-        fout.write('"%s\\n"\n' % line.strip('\n'))
-    fout.write(';\n')
-    fin.close()
-    fout.close()
+    fin  = os.path.join(c.src_dir, 'database.smt2')
+    fout = os.path.join(c.src_dir, 'database.h')
+    mk_pat_db_internal(fin, fout)
+
+def mk_pat_db_internal(inputFilePath, outputFilePath):
+    with open(inputFilePath, 'r') as fin:
+        with open(outputFilePath, 'w') as fout:
+            fout.write('static char const g_pattern_database[] =\n')
+            for line in fin:
+                fout.write('"%s\\n"\n' % line.strip('\n'))
+            fout.write(';\n')
     if VERBOSE:
-        print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
+        print("Generated '%s'" % outputFilePath)
 
 # Update version numbers
 def update_version():
@@ -2645,15 +2648,20 @@ def update_version():
 # Update files with the version number
 def mk_version_dot_h(major, minor, build, revision):
     c = get_component(UTIL_COMPONENT)
-    fout = open(os.path.join(c.src_dir, 'version.h'), 'w')
-    fout.write('// automatically generated file.\n')
-    fout.write('#define Z3_MAJOR_VERSION   %s\n' % major)
-    fout.write('#define Z3_MINOR_VERSION   %s\n' % minor)
-    fout.write('#define Z3_BUILD_NUMBER    %s\n' % build)
-    fout.write('#define Z3_REVISION_NUMBER %s\n' % revision)
-    fout.close()
+    version_template = os.path.join(c.src_dir, 'version.h.in')
+    version_header_output = os.path.join(c.src_dir, 'version.h')
+    # Note the substitution names are what is used by the CMake
+    # builds system. If you change these you should change them
+    # in the CMake build too
+    configure_file(version_template, version_header_output,
+        { 'Z3_VERSION_MAJOR': str(major),
+          'Z3_VERSION_MINOR': str(minor),
+          'Z3_VERSION_PATCH': str(build),
+          'Z3_VERSION_TWEAK': str(revision),
+        }
+    )
     if VERBOSE:
-        print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
+        print("Generated '%s'" % version_header_output)
 
 # Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template
 def mk_all_assembly_infos(major, minor, build, revision):
@@ -2690,6 +2698,13 @@ def ADD_PROBE(name, descr, cmd):
 # It installs all tactics in the given component (name) list cnames
 # The procedure looks for ADD_TACTIC commands in the .h files of these components.
 def mk_install_tactic_cpp(cnames, path):
+  component_src_dirs = []
+  for cname in cnames:
+    c = get_component(cname)
+    component_src_dirs.append(c.src_dir)
+  mk_install_tactic_cpp_internal(component_src_dirs, path)
+
+def mk_install_tactic_cpp_internal(component_src_dirs, path):
     global ADD_TACTIC_DATA, ADD_PROBE_DATA
     ADD_TACTIC_DATA = []
     ADD_PROBE_DATA = []
@@ -2701,12 +2716,11 @@ def mk_install_tactic_cpp(cnames, path):
     fout.write('#include"cmd_context.h"\n')
     tactic_pat   = re.compile('[ \t]*ADD_TACTIC\(.*\)')
     probe_pat    = re.compile('[ \t]*ADD_PROBE\(.*\)')
-    for cname in cnames:
-        c = get_component(cname)
-        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
+    for component_src_dir in component_src_dirs:
+        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
         for h_file in h_files:
             added_include = False
-            fin = open(os.path.join(c.src_dir, h_file), 'r')
+            fin = open(os.path.join(component_src_dir, h_file), 'r')
             for line in fin:
                 if tactic_pat.match(line):
                     if not added_include:
@@ -2759,6 +2773,13 @@ def mk_all_install_tactic_cpps():
 #    void mem_finalize()
 # These procedures are invoked by the Z3 memory_manager
 def mk_mem_initializer_cpp(cnames, path):
+  component_src_dirs = []
+  for cname in cnames:
+    c = get_component(cname)
+    component_src_dirs.append(c.src_dir)
+  mk_mem_initializer_cpp_internal(component_src_dirs, path)
+
+def mk_mem_initializer_cpp_internal(component_src_dirs, path):
     initializer_cmds = []
     finalizer_cmds   = []
     fullname = os.path.join(path, 'mem_initializer.cpp')
@@ -2768,12 +2789,11 @@ def mk_mem_initializer_cpp(cnames, path):
     # ADD_INITIALIZER with priority
     initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
     finalizer_pat        = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
-    for cname in cnames:
-        c = get_component(cname)
-        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
+    for component_src_dir in component_src_dirs:
+        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
         for h_file in h_files:
             added_include = False
-            fin = open(os.path.join(c.src_dir, h_file), 'r')
+            fin = open(os.path.join(component_src_dir, h_file), 'r')
             for line in fin:
                 m = initializer_pat.match(line)
                 if m:
@@ -2818,11 +2838,18 @@ def mk_all_mem_initializer_cpps():
                 cnames.append(c.name)
                 mk_mem_initializer_cpp(cnames, c.src_dir)
 
-# Generate an mem_initializer.cpp at path.
+# Generate an ``gparams_register_modules.cpp`` at path.
 # This file implements the procedure
 #    void gparams_register_modules()
 # This procedure is invoked by gparams::init()
 def mk_gparams_register_modules(cnames, path):
+  component_src_dirs = []
+  for cname in cnames:
+    c = get_component(cname)
+    component_src_dirs.append(c.src_dir)
+  mk_gparams_register_modules_internal(component_src_dirs, path)
+
+def mk_gparams_register_modules_internal(component_src_dirs, path):
     cmds = []
     mod_cmds = []
     mod_descrs = []
@@ -2833,12 +2860,11 @@ def mk_gparams_register_modules(cnames, path):
     reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
     reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
     reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
-    for cname in cnames:
-        c = get_component(cname)
-        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
+    for component_src_dir in component_src_dirs:
+        h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
         for h_file in h_files:
             added_include = False
-            fin = open(os.path.join(c.src_dir, h_file), 'r')
+            fin = open(os.path.join(component_src_dir, h_file), 'r')
             for line in fin:
                 m = reg_pat.match(line)
                 if m:
@@ -2879,14 +2905,22 @@ def mk_all_gparams_register_modules():
 
 # Generate a .def based on the files at c.export_files slot.
 def mk_def_file(c):
-    pat1 = re.compile(".*Z3_API.*")
     defname = '%s.def' % os.path.join(c.src_dir, c.name)
-    fout = open(defname, 'w')
-    fout.write('LIBRARY "%s"\nEXPORTS\n' % c.dll_name)
-    num = 1
+    dll_name = c.dll_name
+    export_header_files = []
     for dot_h in c.export_files:
         dot_h_c = c.find_file(dot_h, c.name)
-        api = open(os.path.join(dot_h_c.src_dir, dot_h), 'r')
+        api = os.path.join(dot_h_c.src_dir, dot_h)
+        export_header_files.append(api)
+    mk_def_file_internal(defname, dll_name, export_header_files)
+
+def mk_def_file_internal(defname, dll_name, export_header_files):
+    pat1 = re.compile(".*Z3_API.*")
+    fout = open(defname, 'w')
+    fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name)
+    num = 1
+    for export_header_file in export_header_files:
+        api = open(export_header_file, 'r')
         for line in api:
             m = pat1.match(line)
             if m:
@@ -2952,7 +2986,28 @@ def mk_bindings(api_files):
         if is_java_enabled():
             check_java()
             mk_z3consts_java(api_files)
-        _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
+        # Generate some of the bindings and "api" module files
+        import update_api
+        dotnet_output_dir = None
+        if is_dotnet_enabled():
+          dotnet_output_dir = get_component('dotnet').src_dir
+        java_output_dir = None
+        java_package_name = None
+        if is_java_enabled():
+          java_output_dir = get_component('java').src_dir
+          java_package_name = get_component('java').package_name
+        ml_output_dir = None
+        if is_ml_enabled():
+          ml_output_dir = get_component('ml').src_dir
+        # Get the update_api module to do the work for us
+        update_api.generate_files(api_files=new_api_files,
+          api_output_dir=get_component('api').src_dir,
+          z3py_output_dir=get_z3py_dir(),
+          dotnet_output_dir=dotnet_output_dir,
+          java_output_dir=java_output_dir,
+          java_package_name=java_package_name,
+          ml_output_dir=ml_output_dir
+        )
         cp_z3py_to_build()
         if is_ml_enabled():
             check_ml()
@@ -2965,6 +3020,17 @@ def mk_bindings(api_files):
 def mk_z3consts_py(api_files):
     if Z3PY_SRC_DIR is None:
         raise MKException("You must invoke set_z3py_dir(path):")
+    full_path_api_files = []
+    api_dll = get_component(Z3_DLL_COMPONENT)
+    for api_file in api_files:
+        api_file_c = api_dll.find_file(api_file, api_dll.name)
+        api_file   = os.path.join(api_file_c.src_dir, api_file)
+        full_path_api_files.append(api_file)
+    mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)
+
+def mk_z3consts_py_internal(api_files, output_dir):
+    assert os.path.isdir(output_dir)
+    assert isinstance(api_files, list)
 
     blank_pat      = re.compile("^ *\r?$")
     comment_pat    = re.compile("^ *//.*$")
@@ -2973,14 +3039,9 @@ def mk_z3consts_py(api_files):
     openbrace_pat  = re.compile("{ *")
     closebrace_pat = re.compile("}.*;")
 
-    z3consts  = open(os.path.join(Z3PY_SRC_DIR, 'z3consts.py'), 'w')
+    z3consts  = open(os.path.join(output_dir, 'z3consts.py'), 'w')
     z3consts.write('# Automatically generated file\n\n')
-
-    api_dll = get_component(Z3_DLL_COMPONENT)
-
     for api_file in api_files:
-        api_file_c = api_dll.find_file(api_file, api_dll.name)
-        api_file   = os.path.join(api_file_c.src_dir, api_file)
         api = open(api_file, 'r')
 
         SEARCHING  = 0
@@ -3041,7 +3102,7 @@ def mk_z3consts_py(api_files):
         api.close()
     z3consts.close()
     if VERBOSE:
-        print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
+        print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py'))
 
 
 # Extract enumeration types from z3_api.h, and add .Net definitions

scripts/pyg2hpp.py

@@ -0,0 +1,42 @@
+#!/usr/bin/env python
+"""
+Reads a pyg file and emits the corresponding
+C++ header file into the specified destination
+directory.
+"""
+import mk_util
+import argparse
+import logging
+import os
+import sys
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("pyg_file", help="pyg file")
+  parser.add_argument("destination_dir", help="destination directory")
+  pargs = parser.parse_args(args)
+
+  if not os.path.exists(pargs.pyg_file):
+    logging.error('"{}" does not exist'.format(pargs.pyg_file))
+    return 1
+
+  if not os.path.exists(pargs.destination_dir):
+    logging.error('"{}" does not exist'.format(pargs.destination_dir))
+    return 1
+
+  if not os.path.isdir(pargs.destination_dir):
+    logging.error('"{}" is not a directory'.format(pargs.destination_dir))
+    return 1
+
+  pyg_full_path = os.path.abspath(pargs.pyg_file)
+  destination_dir_full_path = os.path.abspath(pargs.destination_dir)
+  logging.info('Using {}'.format(pyg_full_path))
+  # Use the existing infrastructure to do this
+  mk_util.CURRENT_PYG_HPP_DEST_DIR = destination_dir_full_path
+  mk_util._execfile(pyg_full_path, mk_util.PYG_GLOBALS)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))
+

scripts/update_api.py

@@ -1,113 +1,36 @@
-
+#!/usr/bin/env python
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
-# 
-# Scripts for generating Makefiles and Visual 
+#
+# Scripts for generating Makefiles and Visual
 # Studio project files.
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-from mk_util import *
-from mk_exception import *
+"""
+This script generates the ``api_log_macros.h``,
+``api_log_macros.cpp`` and ``api_commands.cpp``
+files for the "api" module based on parsing
+several API header files. It can also optionally
+emit some of the files required for Z3's different
+language bindings.
+"""
+import mk_util
+import mk_exception
+import argparse
+import logging
+import re
+import os
+import sys
 
 ##########################################################
 # TODO: rewrite this file without using global variables.
 # This file is a big HACK.
 # It started as small simple script.
 # Now, it is too big, and is invoked from mk_make.py
-# The communication uses 
 #
 ##########################################################
 
-#
-# Generate logging support and bindings
-#
-api_dir     = get_component('api').src_dir
-dotnet_dir  = get_component('dotnet').src_dir
-
-log_h   = open(os.path.join(api_dir, 'api_log_macros.h'), 'w')
-log_c   = open(os.path.join(api_dir, 'api_log_macros.cpp'), 'w')
-exe_c   = open(os.path.join(api_dir, 'api_commands.cpp'), 'w')
-core_py = open(os.path.join(get_z3py_dir(), 'z3core.py'), 'w')
-dotnet_fileout = os.path.join(dotnet_dir, 'Native.cs')
-##
-log_h.write('// Automatically generated file\n')
-log_h.write('#include\"z3.h\"\n')
-log_h.write('#ifdef __GNUC__\n')
-log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
-log_h.write('#else\n')
-log_h.write('#define _Z3_UNUSED\n')
-log_h.write('#endif\n')
-
-##
-log_c.write('// Automatically generated file\n')
-log_c.write('#include<iostream>\n')
-log_c.write('#include\"z3.h\"\n')
-log_c.write('#include\"api_log_macros.h\"\n')
-log_c.write('#include\"z3_logger.h\"\n')
-##
-exe_c.write('// Automatically generated file\n')
-exe_c.write('#include\"z3.h\"\n')
-exe_c.write('#include\"z3_replayer.h\"\n')
-##
-log_h.write('extern std::ostream * g_z3_log;\n')
-log_h.write('extern bool           g_z3_log_enabled;\n')
-log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n')
-log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n')
-log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
-log_h.write('void _Z3_append_log(char const * msg);\n')
-##
-exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
-##
-core_py.write('# Automatically generated file\n')
-core_py.write('import sys, os\n')
-core_py.write('import ctypes\n')
-core_py.write('from z3types import *\n')
-core_py.write('from z3consts import *\n')
-core_py.write("""
-_lib = None
-def lib():
-  global _lib
-  if _lib == None:
-    _dir = os.path.dirname(os.path.abspath(__file__))
-    for ext in ['dll', 'so', 'dylib']:
-      try:
-        init('libz3.%s' % ext)
-        break
-      except:
-        pass
-      try:
-        init(os.path.join(_dir, 'libz3.%s' % ext))
-        break
-      except:
-        pass
-    if _lib == None:
-        raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
-  return _lib
-
-def _to_ascii(s):
-  if isinstance(s, str):
-    return s.encode('ascii')
-  else:
-    return s
-
-if sys.version < '3':
-  def _to_pystr(s):
-     return s
-else:
-  def _to_pystr(s):
-     if s != None:
-        enc = sys.stdout.encoding
-        if enc != None: return s.decode(enc)
-        else: return s.decode('ascii')
-     else:
-        return ""
-
-def init(PATH):
-  global _lib
-  _lib = ctypes.CDLL(PATH)
-""")
-
 IN          = 0
 OUT         = 1
 INOUT       = 2
@@ -176,10 +99,9 @@ def def_Type(var, c_type, py_type):
     Type2PyStr[next_type_id] = py_type
     next_type_id    = next_type_id + 1
 
-def def_Types():
-    import re
+def def_Types(api_files):
     pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
-    for api_file in API_FILES:
+    for api_file in api_files:
         api = open(api_file, 'r')
         for line in api:
             m = pat1.match(line)
@@ -418,10 +340,8 @@ def reg_dotnet(name, result, params):
     global _dotnet_decls
     _dotnet_decls.append((name, result, params))
 
-def mk_dotnet():
+def mk_dotnet(dotnet):
     global Type2Str
-    global dotnet_fileout
-    dotnet = open(dotnet_fileout, 'w')
     dotnet.write('// Automatically generated file\n')
     dotnet.write('using System;\n')
     dotnet.write('using System.Collections.Generic;\n')
@@ -468,10 +388,8 @@ def mk_dotnet():
 NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
 Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
 
-def mk_dotnet_wrappers():
+def mk_dotnet_wrappers(dotnet):
     global Type2Str
-    global dotnet_fileout
-    dotnet = open(dotnet_fileout, 'a')
     dotnet.write("\n")
     dotnet.write("        public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) {\n")
     dotnet.write("            LIB.Z3_set_error_handler(a0, a1);\n")
@@ -556,16 +474,13 @@ def java_array_element_type(p):
     else:
         return 'jlong'
 
-def mk_java():
-    if not is_java_enabled():
-        return
-    java_dir      = get_component('java').src_dir
+def mk_java(java_dir, package_name):
     java_nativef  = os.path.join(java_dir, 'Native.java')
     java_wrapperf = os.path.join(java_dir, 'Native.cpp')
     java_native   = open(java_nativef, 'w')
     java_native.write('// Automatically generated file\n')
-    java_native.write('package %s;\n' % get_component('java').package_name)
-    java_native.write('import %s.enumerations.*;\n' % get_component('java').package_name)
+    java_native.write('package %s;\n' % package_name)
+    java_native.write('import %s.enumerations.*;\n' % package_name)
     java_native.write('public final class Native {\n')
     java_native.write('  public static class IntPtr { public int value; }\n')
     java_native.write('  public static class LongPtr { public long value; }\n')
@@ -638,7 +553,7 @@ def mk_java():
         java_native.write('  }\n\n')
     java_native.write('}\n')
     java_wrapper = open(java_wrapperf, 'w')
-    pkg_str = get_component('java').package_name.replace('.', '_')
+    pkg_str = package_name.replace('.', '_')
     java_wrapper.write('// Automatically generated file\n')
     java_wrapper.write('#ifdef _CYGWIN\n')
     java_wrapper.write('typedef long long __int64;\n')
@@ -801,7 +716,7 @@ def mk_java():
     java_wrapper.write('#ifdef __cplusplus\n')
     java_wrapper.write('}\n')
     java_wrapper.write('#endif\n')
-    if is_verbose():
+    if mk_util.is_verbose():
         print("Generated '%s'" % java_nativef)
 
 def mk_log_header(file, name, params):
@@ -1076,7 +991,7 @@ def def_API(name, result, params):
         mk_log_result_macro(log_h, name, result, params)
     next_id = next_id + 1
 
-def mk_bindings():
+def mk_bindings(exe_c):
     exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n")
     for key, val in API2Id.items():
         exe_c.write("  in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val))
@@ -1160,11 +1075,8 @@ def ml_set_wrap(t, d, n):
         ts = type2str(t)
         return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));'
 
-def mk_ml():
+def mk_ml(ml_dir):
     global Type2Str
-    if not is_ml_enabled():
-        return
-    ml_dir      = get_component('ml').src_dir
     ml_nativef  = os.path.join(ml_dir, 'z3native.ml')
     ml_nativefi = os.path.join(ml_dir, 'z3native.mli')
     ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
@@ -1534,14 +1446,14 @@ def mk_ml():
     ml_wrapper.write('#ifdef __cplusplus\n')
     ml_wrapper.write('}\n')
     ml_wrapper.write('#endif\n')
-    if is_verbose():
+    if mk_util.is_verbose():
         print ('Generated "%s"' % ml_nativef)
 
 # Collect API(...) commands from
-def def_APIs():
+def def_APIs(api_files):
     pat1 = re.compile(" *def_API.*")
     pat2 = re.compile(" *extra_API.*")
-    for api_file in API_FILES:
+    for api_file in api_files:
         api = open(api_file, 'r')
         for line in api:
             line = line.strip('\r\n\t ')
@@ -1553,24 +1465,200 @@ def def_APIs():
                 if m:
                     eval(line)
             except Exception:
-                raise MKException("Failed to process API definition: %s" % line)
-def_Types()
-def_APIs()
-mk_bindings()
-mk_py_wrappers()
-mk_dotnet()
-mk_dotnet_wrappers()
-mk_java()
-mk_ml()
+                raise mk_exec_header.MKException("Failed to process API definition: %s" % line)
 
-log_h.close()
-log_c.close()
-exe_c.close()
-core_py.close()
+def write_log_h_preamble(log_h):
+  log_h.write('// Automatically generated file\n')
+  log_h.write('#include\"z3.h\"\n')
+  log_h.write('#ifdef __GNUC__\n')
+  log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
+  log_h.write('#else\n')
+  log_h.write('#define _Z3_UNUSED\n')
+  log_h.write('#endif\n')
+  #
+  log_h.write('extern std::ostream * g_z3_log;\n')
+  log_h.write('extern bool           g_z3_log_enabled;\n')
+  log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n')
+  log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n')
+  log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
+  log_h.write('void _Z3_append_log(char const * msg);\n')
 
-if is_verbose():
-    print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h'))
-    print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp'))
-    print("Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp'))
-    print("Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py'))
-    print("Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs'))
+
+def write_log_c_preamble(log_c):
+  log_c.write('// Automatically generated file\n')
+  log_c.write('#include<iostream>\n')
+  log_c.write('#include\"z3.h\"\n')
+  log_c.write('#include\"api_log_macros.h\"\n')
+  log_c.write('#include\"z3_logger.h\"\n')
+
+def write_exe_c_preamble(exe_c):
+  exe_c.write('// Automatically generated file\n')
+  exe_c.write('#include\"z3.h\"\n')
+  exe_c.write('#include\"z3_replayer.h\"\n')
+  #
+  exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
+
+def write_core_py_preamble(core_py):
+  core_py.write('# Automatically generated file\n')
+  core_py.write('import sys, os\n')
+  core_py.write('import ctypes\n')
+  core_py.write('from z3types import *\n')
+  core_py.write('from z3consts import *\n')
+  core_py.write(
+"""
+_lib = None
+def lib():
+  global _lib
+  if _lib == None:
+    _dir = os.path.dirname(os.path.abspath(__file__))
+    for ext in ['dll', 'so', 'dylib']:
+      try:
+        init('libz3.%s' % ext)
+        break
+      except:
+        pass
+      try:
+        init(os.path.join(_dir, 'libz3.%s' % ext))
+        break
+      except:
+        pass
+    if _lib == None:
+        raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
+  return _lib
+
+def _to_ascii(s):
+  if isinstance(s, str):
+    return s.encode('ascii')
+  else:
+    return s
+
+if sys.version < '3':
+  def _to_pystr(s):
+     return s
+else:
+  def _to_pystr(s):
+     if s != None:
+        enc = sys.stdout.encoding
+        if enc != None: return s.decode(enc)
+        else: return s.decode('ascii')
+     else:
+        return ""
+
+def init(PATH):
+  global _lib
+  _lib = ctypes.CDLL(PATH)
+"""
+  )
+
+log_h = None
+log_c = None
+exe_c = None
+core_py = None
+
+# FIXME: This can only be called once from this module
+# due to its use of global state!
+def generate_files(api_files,
+                   api_output_dir=None,
+                   z3py_output_dir=None,
+                   dotnet_output_dir=None,
+                   java_output_dir=None,
+                   java_package_name=None,
+                   ml_output_dir=None):
+  """
+    Scan the api files in ``api_files`` and emit
+    the relevant ``api_*.h`` and ``api_*.cpp`` files
+    for the api modules into the ``api_output_dir``
+    directory.
+
+    For the remaining arguments, if said argument is
+    not ``None`` the relevant files for that language
+    binding will be emitted to the specified directory.
+  """
+  # FIXME: These should not be global
+  global log_h, log_c, exe_c, core_py
+  assert isinstance(api_files, list)
+
+  # Hack: Avoid emitting files when we don't want them
+  # by writing to temporary files that get deleted when
+  # closed. This allows us to work around the fact that
+  # existing code is designed to always emit these files.
+  def mk_file_or_temp(output_dir, file_name, mode='w'):
+    if output_dir != None:
+      assert os.path.exists(output_dir) and os.path.isdir(output_dir)
+      return open(os.path.join(output_dir, file_name), mode)
+    else:
+      # Return a file that we can write to without caring
+      print("Faking emission of '{}'".format(file_name))
+      import tempfile
+      return tempfile.TemporaryFile(mode=mode)
+
+  with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h:
+    with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c:
+      with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c:
+        with mk_file_or_temp(z3py_output_dir, 'z3core.py') as core_py:
+          # Write preambles
+          write_log_h_preamble(log_h)
+          write_log_c_preamble(log_c)
+          write_exe_c_preamble(exe_c)
+          write_core_py_preamble(core_py)
+
+          # FIXME: these functions are awful
+          def_Types(api_files)
+          def_APIs(api_files)
+          mk_bindings(exe_c)
+          mk_py_wrappers()
+
+          if mk_util.is_verbose():
+            print("Generated '{}'".format(log_h.name))
+            print("Generated '{}'".format(log_c.name))
+            print("Generated '{}'".format(exe_c.name))
+            print("Generated '{}'".format(core_py.name))
+
+  if dotnet_output_dir:
+    with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file:
+      mk_dotnet(dotnet_file)
+      mk_dotnet_wrappers(dotnet_file)
+      if mk_util.is_verbose():
+        print("Generated '{}'".format(dotnet_file.name))
+
+  if java_output_dir:
+    mk_java(java_output_dir, java_package_name)
+  if ml_output_dir:
+    mk_ml(ml_output_dir)
+
+def main(args):
+  logging.basicConfig(level=logging.INFO)
+  parser = argparse.ArgumentParser(description=__doc__)
+  parser.add_argument("api_files", nargs="+",
+                      help="API header files to generate files from")
+  parser.add_argument("--api_output_dir",
+                      help="Directory to emit files for api module",
+                      default=None)
+  parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
+  parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None)
+  parser.add_argument("--java-output-dir", dest="java_output_dir", default=None)
+  parser.add_argument("--java-package-name", dest="java_package_name", default=None)
+  parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None)
+  pargs = parser.parse_args(args)
+
+  if pargs.java_output_dir:
+    if pargs.java_package_name == None:
+      logging.error('--java-package-name must be specified')
+      return 1
+
+  for api_file in pargs.api_files:
+    if not os.path.exists(api_file):
+      logging.error('"{}" does not exist'.format(api_file))
+      return 1
+
+  generate_files(api_files=pargs.api_files,
+                 api_output_dir=pargs.api_output_dir,
+                 z3py_output_dir=pargs.z3py_output_dir,
+                 dotnet_output_dir=pargs.dotnet_output_dir,
+                 java_output_dir=pargs.java_output_dir,
+                 java_package_name=pargs.java_package_name,
+                 ml_output_dir=pargs.ml_output_dir)
+  return 0
+
+if __name__ == '__main__':
+  sys.exit(main(sys.argv[1:]))