Merge pull request #1070 from delcypher/cmake_file_move

[CMake] Move CMake files into their intended location
2025-04-24 09:35:32 +00:00 · 2017-06-13 13:27:25 -07:00 · 2017-06-13 13:27:25 -07:00 · 5066bd01f7
commit 5066bd01f7
parent 90a38c9a35 814fcd6a17
100 changed files with 10 additions and 310 deletions
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@ -0,0 +1,261 @@
+################################################################################
+# 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(util/lp)
+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})
+set_target_properties(libz3 PROPERTIES
+  # VERSION determines the version in the filename of the shared library.
+  # SOVERSION determines the value of the DT_SONAME field on ELF platforms.
+  # On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z
+  # but symlinks will be made to this file from libz3.so and also from
+  # libz3.so.W.X.
+  # This indicates that no breaking API changes will be made within a single
+  # minor version.
+  VERSION ${Z3_VERSION}
+  SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
+
+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()
+
+# The `PRIVATE` usage requirement is specified so that when building Z3 as a
+# shared library the dependent libraries are specified on the link command line
+# so that if those are also shared libraries they are referenced by `libz3.so`.
+target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
+
+# This is currently only for the OpenMP flags. It needs to be set
+# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`
+# because when building the `libz3` as a static library when the target is exported
+# the link dependencies need to be exported too.
+foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+  target_link_libraries(libz3 PRIVATE ${flag_name})
+endforeach()
+
+# 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
+  EXPORT Z3_EXPORTED_TARGETS
+  LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+  ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
+  RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake
+  PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
+)
+
+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"
+      ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+      ${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()
+
+################################################################################
+# .NET bindings
+################################################################################
+option(BUILD_DOTNET_BINDINGS "Build .NET bindings for Z3" OFF)
+if (BUILD_DOTNET_BINDINGS)
+  if (NOT BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The .NET bindings will not work with a static libz3. "
+      "You either need to disable BUILD_DOTNET_BINDINGS or enable BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/dotnet)
+endif()
+
+################################################################################
+# Java bindings
+################################################################################
+option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF)
+if (BUILD_JAVA_BINDINGS)
+  if (NOT BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The Java bindings will not work with a static libz3. "
+      "You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/java)
+endif()
+
+# TODO: Implement support for other bindigns
--- a/src/ackermannization/CMakeLists.txt
+++ b/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
+)
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@ -0,0 +1,74 @@
+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"
+          ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+          ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+          # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
+          "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  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
+)
--- a/src/api/dll/CMakeLists.txt
+++ b/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})
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@ -0,0 +1,291 @@
+find_package(DotNetToolchain REQUIRED)
+
+# Configure AssemblyInfo.cs
+set(VER_MAJOR "${Z3_VERSION_MAJOR}")
+set(VER_MINOR "${Z3_VERSION_MINOR}")
+set(VER_BUILD "${Z3_VERSION_PATCH}")
+set(VER_REVISION "${Z3_VERSION_TWEAK}")
+set(Z3_DOTNET_ASSEMBLY_INFO_FILE "${CMAKE_CURRENT_BINARY_DIR}/Properties/AssemblyInfo.cs")
+configure_file("Properties/AssemblyInfo.cs.in" "${Z3_DOTNET_ASSEMBLY_INFO_FILE}" @ONLY)
+
+# Generate Native.cs
+set(Z3_DOTNET_NATIVE_FILE "${CMAKE_CURRENT_BINARY_DIR}/Native.cs")
+add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--dotnet-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
+    "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating ${Z3_DOTNET_NATIVE_FILE}"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+# Generate Enumerations.cs
+set(Z3_DOTNET_CONST_FILE "${CMAKE_CURRENT_BINARY_DIR}/Enumerations.cs")
+add_custom_command(OUTPUT "${Z3_DOTNET_CONST_FILE}"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--dotnet-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generating ${Z3_DOTNET_CONST_FILE}"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
+	AlgebraicNum.cs
+	ApplyResult.cs
+	ArithExpr.cs
+	ArithSort.cs
+	ArrayExpr.cs
+	ArraySort.cs
+	AST.cs
+	ASTMap.cs
+	ASTVector.cs
+	BitVecExpr.cs
+	BitVecNum.cs
+	BitVecSort.cs
+	BoolExpr.cs
+	BoolSort.cs
+	Constructor.cs
+	ConstructorList.cs
+	Context.cs
+	DatatypeExpr.cs
+	DatatypeSort.cs
+	Deprecated.cs
+	EnumSort.cs
+	Expr.cs
+	FiniteDomainExpr.cs
+	FiniteDomainNum.cs
+	FiniteDomainSort.cs
+	Fixedpoint.cs
+	FPExpr.cs
+	FPNum.cs
+	FPRMExpr.cs
+	FPRMNum.cs
+	FPRMSort.cs
+	FPSort.cs
+	FuncDecl.cs
+	FuncInterp.cs
+	Global.cs
+	Goal.cs
+	IDecRefQueue.cs
+	InterpolationContext.cs
+	IntExpr.cs
+	IntNum.cs
+	IntSort.cs
+	IntSymbol.cs
+	ListSort.cs
+	Log.cs
+	Model.cs
+	Optimize.cs
+	ParamDescrs.cs
+	Params.cs
+	Pattern.cs
+	Probe.cs
+	Quantifier.cs
+	RatNum.cs
+	RealExpr.cs
+	RealSort.cs
+	ReExpr.cs
+	RelationSort.cs
+	ReSort.cs
+	SeqExpr.cs
+	SeqSort.cs
+	SetSort.cs
+	Solver.cs
+	Sort.cs
+	Statistics.cs
+	Status.cs
+	StringSymbol.cs
+	Symbol.cs
+	Tactic.cs
+	TupleSort.cs
+	UninterpretedSort.cs
+	Version.cs
+	Z3Exception.cs
+	Z3Object.cs
+)
+
+set(Z3_DOTNET_ASSEMBLY_SOURCES "")
+# Make paths to source files absolute
+foreach (csfile ${Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE})
+  list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES "${CMAKE_CURRENT_SOURCE_DIR}/${csfile}")
+endforeach()
+
+# Add generated files
+list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES
+  "${Z3_DOTNET_CONST_FILE}"
+  "${Z3_DOTNET_NATIVE_FILE}"
+  "${Z3_DOTNET_ASSEMBLY_INFO_FILE}"
+)
+
+# ``csc.exe`` doesn't like UNIX style paths so convert them
+# if necessary first to native paths.
+set(Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "")
+foreach (csfile_path ${Z3_DOTNET_ASSEMBLY_SOURCES})
+  file(TO_NATIVE_PATH "${csfile_path}" csfile_path_native)
+  list(APPEND Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH "${csfile_path_native}")
+endforeach()
+
+set(CSC_FLAGS "")
+if (DOTNET_TOOLCHAIN_IS_WINDOWS)
+  # FIXME: Why use these flags?
+  # Note these flags have been copied from the Python build system.
+  list(APPEND CSC_FLAGS
+    "/noconfig"
+    "/nostdlib+"
+    "/reference:mscorlib.dll"
+  )
+  # FIXME: This flag only works when the working directory of csc.exe is
+  # the directory containing the ``libz3`` target. I can't get this to work
+  # correctly with multi-configuration generators (i.e. Visual Studio) so
+  # just don't set the flag for now.
+  #list(APPEND CSC_FLAGS "/linkresource:$<TARGET_FILE_NAME:libz3>")
+elseif (DOTNET_TOOLCHAIN_IS_MONO)
+  # We need to give the assembly a strong name so that it can be installed
+  # into the GAC.
+  list(APPEND CSC_FLAGS
+    "/keyfile:${CMAKE_CURRENT_SOURCE_DIR}/Microsoft.Z3.snk"
+  )
+else()
+  message(FATAL_ERROR "Unknown .NET toolchain")
+endif()
+
+# Common flags
+list(APPEND CSC_FLAGS
+  "/unsafe+"
+  "/nowarn:1701,1702"
+  "/errorreport:prompt"
+  "/warn:4"
+  "/reference:System.Core.dll"
+  "/reference:System.dll"
+  "/reference:System.Numerics.dll"
+  "/filealign:512" # Why?
+  "/target:library"
+)
+
+# Set the build type flags. The build type for the assembly roughly corresponds
+# with the native code build type.
+list(APPEND CSC_FLAGS
+  # Debug flags, expands to nothing if we aren't doing a debug build
+  "$<$<CONFIG:Debug>:/debug+>"
+  "$<$<CONFIG:Debug>:/debug:full>"
+  "$<$<CONFIG:Debug>:/optimize->"
+  # This has to be quoted otherwise the ``;`` is interpreted as a command separator
+  "$<$<CONFIG:Debug>:\"/define:DEBUG$<SEMICOLON>TRACE\">"
+  # Release flags, expands to nothing if we are doing a debug build
+  "$<$<NOT:$<CONFIG:Debug>>:/optimize+>"
+)
+
+# Mono's gacutil crashes when trying to install an assembly if we set the
+# platform in some cases, so only set it on Windows.  This bug has been
+# reported at https://bugzilla.xamarin.com/show_bug.cgi?id=39955 . However mono
+# ignores the platform of an assembly when running it (
+# http://lists.ximian.com/pipermail/mono-devel-list/2015-November/043370.html )
+# so this shouldn't matter in practice.
+if (DOTNET_TOOLCHAIN_IS_WINDOWS)
+  # Set platform for assembly
+  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+    list(APPEND CSC_FLAGS "/platform:x64")
+  elseif ("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+    list(APPEND CSC_FLAGS "/platform:x86")
+  endif()
+endif()
+
+# FIXME: Ideally we should emit files into a configuration specific directory
+# when using multi-configuration generators so that the files generated by each
+# configuration don't clobber each other. Unfortunately the ``get_property()``
+# command only works correctly for single configuration generators so we can't
+# use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
+# argument to ``add_custom_commands()`` won't accept it.
+# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html
+#
+# For now just output file to the root binary directory like the Python build
+# system does and emit a warning when appropriate.
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi-configuration build (e.g. Visual Studio and Xcode).
+  message(WARNING "You are using a multi-configuration generator. The build rules for"
+    " the \".NET\" bindings currently do not emit files per configuration so previously"
+    " generated files for other configurations will be overwritten.")
+endif()
+
+set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}")
+set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll")
+set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}")
+# csc.exe doesn't work with UNIX style paths so convert to native path
+file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL}" Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH)
+set(Z3_DOTNET_ASSEMBLY_DLL_DOC "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/Microsoft.Z3.xml")
+file(TO_NATIVE_PATH "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH)
+add_custom_command(OUTPUT "${Z3_DOTNET_ASSEMBLY_DLL}" "${Z3_DOTNET_ASSEMBLY_DLL_DOC}"
+  COMMAND
+    "${DOTNET_CSC_EXECUTABLE}"
+    ${CSC_FLAGS}
+    "/out:${Z3_DOTNET_ASSEMBLY_DLL_NATIVE_PATH}"
+    "/doc:${Z3_DOTNET_ASSEMBLY_DLL_DOC_NATIVE_PATH}"
+    ${Z3_DOTNET_ASSEMBLY_SOURCES_NATIVE_PATH}
+  DEPENDS
+    ${Z3_DOTNET_ASSEMBLY_SOURCES}
+    libz3
+  WORKING_DIRECTORY "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}"
+  COMMENT "Building \"${Z3_DOTNET_ASSEMBLY_DLL}\""
+)
+
+# Convenient top-level target
+add_custom_target(build_z3_dotnet_bindings
+  ALL
+  DEPENDS
+    "${Z3_DOTNET_ASSEMBLY_DLL}"
+)
+
+###############################################################################
+# Install
+###############################################################################
+option(INSTALL_DOTNET_BINDINGS "Install .NET bindings when invoking install target" ON)
+set(GAC_PKG_NAME "Microsoft.Z3.Sharp")
+set(PREFIX "${CMAKE_INSTALL_PREFIX}")
+set(VERSION "${Z3_VERSION}")
+set(Z3_DOTNET_PKGCONFIG_FILE "${CMAKE_CURRENT_BINARY_DIR}/Microsoft.Z3.Sharp.pc")
+configure_file("Microsoft.Z3.Sharp.pc.in" "${Z3_DOTNET_PKGCONFIG_FILE}" @ONLY)
+
+if (DOTNET_TOOLCHAIN_IS_MONO)
+  message(STATUS "Emitting install rules for .NET bindings")
+  # Install pkgconfig file for the assembly. This is needed by Monodevelop
+  # to find the assembly
+  install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
+
+  # Configure the install and uninstall scripts.
+  # Note: If multi-configuration generator support is ever fixed then these
+  # scripts will be broken.
+  configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
+  configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
+
+  # Tell CMake to Invoke a script to install assembly to the GAC during install
+  install(SCRIPT "${CMAKE_CURRENT_BINARY_DIR}/cmake_install_gac.cmake")
+
+  # Add custom target to uninstall the assembly from the GAC
+  add_custom_target(remove_dotnet_dll_from_gac
+    COMMAND "${CMAKE_COMMAND}" "-P" "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall_gac.cmake"
+    COMMENT "Uninstalling ${Z3_DOTNET_ASSEMBLY_NAME} from the GAC"
+    ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+  )
+  add_dependencies(uninstall remove_dotnet_dll_from_gac)
+
+elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
+  # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
+  # installation directory.
+  install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
+  install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
+else()
+  message(FATAL_ERROR "Unknown .NET toolchain")
+endif()
--- a/src/api/dotnet/cmake_install_gac.cmake.in
+++ b/src/api/dotnet/cmake_install_gac.cmake.in
@ -0,0 +1,18 @@
+# Install assembly to the GAC
+set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
+execute_process(COMMAND
+  "@DOTNET_GACUTIL_EXECUTABLE@"
+  "-i"
+  "@Z3_DOTNET_ASSEMBLY_DLL@"
+  "-f"
+  "-package" "@GAC_PKG_NAME@"
+  "-root" "${GAC_ROOT}"
+  WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
+  RESULT_VARIABLE gacutil_exit_code
+)
+
+if ("${gacutil_exit_code}" EQUAL 0)
+  message(STATUS "Installed \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
+else()
+  message(FATAL_ERROR "Failed to install \"@Z3_DOTNET_ASSEMBLY_DLL@\" to the GAC")
+endif()
--- a/src/api/dotnet/cmake_uninstall_gac.cmake.in
+++ b/src/api/dotnet/cmake_uninstall_gac.cmake.in
@ -0,0 +1,20 @@
+# Uninstall assembly from the GAC
+set(GAC_ROOT "$ENV{DESTDIR}@CMAKE_INSTALL_FULL_LIBDIR@")
+execute_process(COMMAND
+  "@DOTNET_GACUTIL_EXECUTABLE@"
+  # Note ``-us`` takes assembly file name rather than
+  # ``-u`` which takes an assembly display name
+  "-us"
+  "@Z3_DOTNET_ASSEMBLY_NAME@"
+  "-f"
+  "-package" "@GAC_PKG_NAME@"
+  "-root" "${GAC_ROOT}"
+  WORKING_DIRECTORY "@CMAKE_CURRENT_BINARY_DIR@"
+  RESULT_VARIABLE gacutil_exit_code
+)
+
+if ("${gacutil_exit_code}" EQUAL 0)
+  message(STATUS "Uninstalled \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
+else()
+  message(FATAL_ERROR "Failed to uninstall \"@Z3_DOTNET_ASSEMBLY_NAME@\" from the GAC")
+endif()
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@ -0,0 +1,236 @@
+find_package(Java REQUIRED)
+find_package(JNI REQUIRED)
+include(UseJava)
+
+# Sanity check for dirty source tree
+foreach (file_name "enumerations" "Native.cpp" "Native.java")
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
+            ${z3_polluted_tree_msg})
+  endif()
+endforeach()
+
+set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
+
+# Rule to generate ``Native.java`` and ``Native.cpp``
+set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
+set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
+add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--java-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    "--java-package-name"
+    ${Z3_JAVA_PACKAGE_NAME}
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
+    "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+# Add rule to build native code that provides a bridge between
+# ``Native.java`` and libz3's interfac3.
+add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
+target_link_libraries(z3java PRIVATE libz3)
+# FIXME:
+# Not sure if using all the flags used by the Z3 components is really necessary
+# here.  At the bare minimum setting _AMD64_ depending on the target is
+# necessary but seeing as the Python build system uses all the flags used for building
+# Z3's components to build ``Native.cpp`` lets do the same for now.
+target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+target_include_directories(z3java PRIVATE
+  "${CMAKE_SOURCE_DIR}/src/api"
+  "${CMAKE_BINARY_DIR}/src/api"
+  ${JNI_INCLUDE_DIRS}
+)
+# FIXME: Should this library have SONAME and VERSION set?
+
+# This prevents CMake from automatically defining ``z3java_EXPORTS``
+set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
+
+# Rule to generate the ``com.microsoft.z3.enumerations`` package
+# FIXME: This list of files is fragile
+set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
+  Z3_ast_kind.java
+  Z3_ast_print_mode.java
+  Z3_decl_kind.java
+  Z3_error_code.java
+  Z3_goal_prec.java
+  Z3_lbool.java
+  Z3_param_kind.java
+  Z3_parameter_kind.java
+  Z3_sort_kind.java
+  Z3_symbol_kind.java
+)
+set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
+foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
+  list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
+    "${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
+  )
+endforeach()
+add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--java-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    "--java-package-name"
+    ${Z3_JAVA_PACKAGE_NAME}
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+set(Z3_JAVA_JAR_SOURCE_FILES
+  AlgebraicNum.java
+  ApplyResultDecRefQueue.java
+  ApplyResult.java
+  ArithExpr.java
+  ArithSort.java
+  ArrayExpr.java
+  ArraySort.java
+  ASTDecRefQueue.java
+  AST.java
+  AstMapDecRefQueue.java
+  ASTMap.java
+  AstVectorDecRefQueue.java
+  ASTVector.java
+  BitVecExpr.java
+  BitVecNum.java
+  BitVecSort.java
+  BoolExpr.java
+  BoolSort.java
+  ConstructorDecRefQueue.java
+  Constructor.java
+  ConstructorListDecRefQueue.java
+  ConstructorList.java
+  Context.java
+  DatatypeExpr.java
+  DatatypeSort.java
+  EnumSort.java
+  Expr.java
+  FiniteDomainExpr.java
+  FiniteDomainNum.java
+  FiniteDomainSort.java
+  FixedpointDecRefQueue.java
+  Fixedpoint.java
+  FPExpr.java
+  FPNum.java
+  FPRMExpr.java
+  FPRMNum.java
+  FPRMSort.java
+  FPSort.java
+  FuncDecl.java
+  FuncInterpDecRefQueue.java
+  FuncInterpEntryDecRefQueue.java
+  FuncInterp.java
+  Global.java
+  GoalDecRefQueue.java
+  Goal.java
+  IDecRefQueue.java
+  InterpolationContext.java
+  IntExpr.java
+  IntNum.java
+  IntSort.java
+  IntSymbol.java
+  ListSort.java
+  Log.java
+  ModelDecRefQueue.java
+  Model.java
+  OptimizeDecRefQueue.java
+  Optimize.java
+  ParamDescrsDecRefQueue.java
+  ParamDescrs.java
+  ParamsDecRefQueue.java
+  Params.java
+  Pattern.java
+  ProbeDecRefQueue.java
+  Probe.java
+  Quantifier.java
+  RatNum.java
+  RealExpr.java
+  RealSort.java
+  ReExpr.java
+  RelationSort.java
+  ReSort.java
+  SeqExpr.java
+  SeqSort.java
+  SetSort.java
+  SolverDecRefQueue.java
+  Solver.java
+  Sort.java
+  StatisticsDecRefQueue.java
+  Statistics.java
+  Status.java
+  StringSymbol.java
+  Symbol.java
+  TacticDecRefQueue.java
+  Tactic.java
+  TupleSort.java
+  UninterpretedSort.java
+  Version.java
+  Z3Exception.java
+  Z3Object.java
+)
+set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
+foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
+  list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
+endforeach()
+# Add generated files to list
+list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
+  ${Z3_JAVA_NATIVE_JAVA}
+  ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
+)
+
+# Convenient top-level target
+add_custom_target(build_z3_java_bindings
+  ALL
+  DEPENDS
+    z3java
+    z3JavaJar
+)
+
+# Rule to build ``com.microsoft.z3.jar``
+# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
+add_jar(z3JavaJar
+  SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
+  OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
+  OUTPUT_DIR "${CMAKE_BINARY_DIR}"
+  VERSION "${Z3_VERSION}"
+)
+
+###############################################################################
+# Install
+###############################################################################
+option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
+if (INSTALL_JAVA_BINDINGS)
+  # Provide cache variables for the install locations that the user can change.
+  # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
+  # files on Linux distributions
+  set(Z3_JAVA_JAR_INSTALLDIR
+    "${CMAKE_INSTALL_DATAROOTDIR}/java"
+    CACHE
+    PATH
+    "Directory to install Z3 Java jar file relative to install prefix"
+  )
+  # FIXME: I don't think this the right installation location
+  set(Z3_JAVA_JNI_LIB_INSTALLDIR
+    "${CMAKE_INSTALL_LIBDIR}"
+    CACHE
+    PATH
+    "Directory to install Z3 Java JNI bridge library relative to install prefix"
+  )
+  install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
+  # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
+  # with CMake 2.8.12.2 handles that incorrectly.
+  install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
+endif()
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@ -0,0 +1,143 @@
+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/__init__.py
+  z3/z3.py
+  z3/z3num.py
+  z3/z3poly.py
+  z3/z3printer.py
+  z3/z3rcf.py
+  z3test.py
+  z3/z3types.py
+  z3/z3util.py
+)
+
+set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}/python")
+file(MAKE_DIRECTORY "${z3py_bindings_build_dest}")
+file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3")
+
+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}/${z3py_file}"
+    DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}"
+    COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}/${z3py_file}"
+  )
+  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}/z3/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"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
+    "${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}/z3/z3core.py")
+
+# Generate z3consts.py
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/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"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generating z3consts.py"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3/z3consts.py")
+
+if (UNIX)
+  set(LINK_COMMAND "create_symlink")
+else()
+  set(LINK_COMMAND "copy")
+endif()
+
+# Link libz3 into the python directory so bindings work out of the box
+add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+  COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
+    "${CMAKE_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+  DEPENDS libz3
+  COMMENT "Linking libz3 into python directory"
+)
+
+# Convenient top-level target
+add_custom_target(build_z3_python_bindings
+  ALL
+  DEPENDS
+    ${build_z3_python_bindings_target_depends}
+    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+)
+
+###############################################################################
+# Install
+###############################################################################
+option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON)
+if (INSTALL_PYTHON_BINDINGS)
+  message(STATUS "Emitting rules to install Z3 python bindings")
+  # Try to guess the installation path for the bindings
+  if (NOT DEFINED CMAKE_INSTALL_PYTHON_PKG_DIR)
+    message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
+    execute_process(
+      COMMAND "${PYTHON_EXECUTABLE}" "-c"
+        "import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
+      RESULT_VARIABLE exit_code
+      OUTPUT_VARIABLE CMAKE_INSTALL_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: \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
+    # Set a cache variable that the user can modify if needed
+    set(CMAKE_INSTALL_PYTHON_PKG_DIR
+      "${CMAKE_INSTALL_PYTHON_PKG_DIR}"
+      CACHE PATH
+      "Path to install python bindings. This can be relative or absolute.")
+    mark_as_advanced(CMAKE_INSTALL_PYTHON_PKG_DIR)
+  else()
+    message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR already set (\"${CMAKE_INSTALL_PYTHON_PKG_DIR}\")"
+                   ". Not trying to guess.")
+  endif()
+
+  # Check if path exists under the install prefix if it is absolute. If the
+  # path is relative it will be installed under the install prefix so there
+  # if nothing to check
+  if (IS_ABSOLUTE "${CMAKE_INSTALL_PYTHON_PKG_DIR}")
+    string(FIND "${CMAKE_INSTALL_PYTHON_PKG_DIR}" "${CMAKE_INSTALL_PREFIX}" position)
+    if (NOT ("${position}" EQUAL 0))
+      message(WARNING "The directory to install the python bindings \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\" "
+              "is not under the install prefix \"${CMAKE_INSTALL_PREFIX}\"."
+              " Running the install target may lead to a broken installation. "
+              "To change the install directory modify the CMAKE_INSTALL_PYTHON_PKG_DIR cache variable."
+              )
+    endif()
+  endif()
+  # Using DESTDIR still seems to work even if we use an absolute path
+  message(STATUS "Python bindings will be installed to \"${CMAKE_INSTALL_PYTHON_PKG_DIR}\"")
+  install(FILES ${build_z3_python_bindings_target_depends}
+    DESTINATION "${CMAKE_INSTALL_PYTHON_PKG_DIR}/z3"
+  )
+else()
+  message(STATUS "Not emitting rules to install Z3 python bindings")
+endif()
--- a/src/ast/CMakeLists.txt
+++ b/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
+)
--- a/src/ast/fpa/CMakeLists.txt
+++ b/src/ast/fpa/CMakeLists.txt
@ -0,0 +1,13 @@
+z3_add_component(fpa
+  SOURCES
+    bv2fpa_converter.cpp
+    fpa2bv_converter.cpp
+    fpa2bv_rewriter.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    simplifier
+    model
+    util
+  PYG_FILES
+    fpa2bv_rewriter_params.pyg
+)
--- a/src/ast/macros/CMakeLists.txt
+++ b/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
+)
--- a/src/ast/normal_forms/CMakeLists.txt
+++ b/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
+)
--- a/src/ast/pattern/CMakeLists.txt
+++ b/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"
+          ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  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
+)
--- a/src/ast/proof_checker/CMakeLists.txt
+++ b/src/ast/proof_checker/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(proof_checker
+  SOURCES
+    proof_checker.cpp
+  COMPONENT_DEPENDENCIES
+    rewriter
+)
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@ -0,0 +1,41 @@
+z3_add_component(rewriter
+  SOURCES
+    arith_rewriter.cpp
+    array_rewriter.cpp
+    ast_counter.cpp
+    bool_rewriter.cpp
+    bv_bounds.cpp
+    bv_rewriter.cpp
+    datatype_rewriter.cpp
+    der.cpp
+    distribute_forall.cpp
+    dl_rewriter.cpp
+    enum2bv_rewriter.cpp
+    expr_replacer.cpp
+    expr_safe_replace.cpp
+    factor_rewriter.cpp
+    fpa_rewriter.cpp
+    label_rewriter.cpp
+    mk_simplified_app.cpp
+    pb_rewriter.cpp
+    pb2bv_rewriter.cpp
+    quant_hoist.cpp
+    rewriter.cpp
+    seq_rewriter.cpp
+    th_rewriter.cpp
+    var_subst.cpp
+    bv_trailing.cpp
+    mk_extract_proc.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
+)
--- a/src/ast/rewriter/bit_blaster/CMakeLists.txt
+++ b/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
+)
--- a/src/ast/simplifier/CMakeLists.txt
+++ b/src/ast/simplifier/CMakeLists.txt
@ -0,0 +1,29 @@
+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
+    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
+)
--- a/src/ast/substitution/CMakeLists.txt
+++ b/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
+)
--- a/src/cmd_context/CMakeLists.txt
+++ b/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
+)
--- a/src/cmd_context/extra_cmds/CMakeLists.txt
+++ b/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
+)
--- a/src/duality/CMakeLists.txt
+++ b/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
+)
--- a/src/interp/CMakeLists.txt
+++ b/src/interp/CMakeLists.txt
@ -0,0 +1,18 @@
+z3_add_component(interp
+  SOURCES
+    iz3base.cpp
+    iz3checker.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
+)
--- a/src/math/automata/CMakeLists.txt
+++ b/src/math/automata/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(automata
+  SOURCES
+    automaton.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
--- a/src/math/euclid/CMakeLists.txt
+++ b/src/math/euclid/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(euclid
+  SOURCES
+    euclidean_solver.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
--- a/src/math/grobner/CMakeLists.txt
+++ b/src/math/grobner/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(grobner
+  SOURCES
+    grobner.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+)
--- a/src/math/hilbert/CMakeLists.txt
+++ b/src/math/hilbert/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(hilbert
+  SOURCES
+    hilbert_basis.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
--- a/src/math/interval/CMakeLists.txt
+++ b/src/math/interval/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(interval
+  SOURCES
+    interval_mpq.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
--- a/src/math/polynomial/CMakeLists.txt
+++ b/src/math/polynomial/CMakeLists.txt
@ -0,0 +1,15 @@
+z3_add_component(polynomial
+  SOURCES
+    algebraic_numbers.cpp
+    polynomial_cache.cpp
+    polynomial.cpp
+    rpolynomial.cpp
+    sexpr2upolynomial.cpp
+    upolynomial.cpp
+    upolynomial_factorization.cpp
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    algebraic_params.pyg
+)
+
--- a/src/math/realclosure/CMakeLists.txt
+++ b/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
+)
--- a/src/math/simplex/CMakeLists.txt
+++ b/src/math/simplex/CMakeLists.txt
@ -0,0 +1,7 @@
+z3_add_component(simplex
+  SOURCES
+    simplex.cpp
+    model_based_opt.cpp
+  COMPONENT_DEPENDENCIES
+    util
+)
--- a/src/math/subpaving/CMakeLists.txt
+++ b/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
+)
--- a/src/math/subpaving/tactic/CMakeLists.txt
+++ b/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
+)
--- a/src/model/CMakeLists.txt
+++ b/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
+)
+
--- a/src/muz/base/CMakeLists.txt
+++ b/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
+)
--- a/src/muz/bmc/CMakeLists.txt
+++ b/src/muz/bmc/CMakeLists.txt
@ -0,0 +1,7 @@
+z3_add_component(bmc
+  SOURCES
+    dl_bmc_engine.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
--- a/src/muz/clp/CMakeLists.txt
+++ b/src/muz/clp/CMakeLists.txt
@ -0,0 +1,7 @@
+z3_add_component(clp
+  SOURCES
+    clp_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
--- a/src/muz/dataflow/CMakeLists.txt
+++ b/src/muz/dataflow/CMakeLists.txt
@ -0,0 +1,6 @@
+z3_add_component(dataflow
+  SOURCES
+    dataflow.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+)
--- a/src/muz/ddnf/CMakeLists.txt
+++ b/src/muz/ddnf/CMakeLists.txt
@ -0,0 +1,8 @@
+z3_add_component(ddnf
+  SOURCES
+    ddnf.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    rel
+    transforms
+)
--- a/src/muz/duality/CMakeLists.txt
+++ b/src/muz/duality/CMakeLists.txt
@ -0,0 +1,8 @@
+z3_add_component(duality_intf
+  SOURCES
+    duality_dl_interface.cpp
+  COMPONENT_DEPENDENCIES
+    duality
+    muz
+    transforms
+)
--- a/src/muz/fp/CMakeLists.txt
+++ b/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
+)
--- a/src/muz/pdr/CMakeLists.txt
+++ b/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
+)
--- a/src/muz/rel/CMakeLists.txt
+++ b/src/muz/rel/CMakeLists.txt
@ -0,0 +1,31 @@
+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_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
+)
--- a/src/muz/tab/CMakeLists.txt
+++ b/src/muz/tab/CMakeLists.txt
@ -0,0 +1,7 @@
+z3_add_component(tab
+  SOURCES
+    tab_context.cpp
+  COMPONENT_DEPENDENCIES
+    muz
+    transforms
+)
--- a/src/muz/transforms/CMakeLists.txt
+++ b/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
+)
--- a/src/nlsat/CMakeLists.txt
+++ b/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
+)
--- a/src/nlsat/tactic/CMakeLists.txt
+++ b/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
+)
--- a/src/opt/CMakeLists.txt
+++ b/src/opt/CMakeLists.txt
@ -0,0 +1,21 @@
+z3_add_component(opt
+  SOURCES
+    maxres.cpp
+    maxsmt.cpp
+    mss.cpp
+    opt_cmds.cpp
+    opt_context.cpp
+    opt_pareto.cpp
+    optsmt.cpp
+    opt_solver.cpp
+    pb_sls.cpp
+    sortmax.cpp
+    wmax.cpp
+  COMPONENT_DEPENDENCIES
+    sat_solver
+    sls_tactic
+    smt
+    smtlogic_tactics
+  PYG_FILES
+    opt_params.pyg
+)
--- a/src/parsers/smt/CMakeLists.txt
+++ b/src/parsers/smt/CMakeLists.txt
@ -0,0 +1,8 @@
+z3_add_component(smtparser
+  SOURCES
+    smtlib.cpp
+    smtlib_solver.cpp
+    smtparser.cpp
+  COMPONENT_DEPENDENCIES
+    portfolio
+)
--- a/src/parsers/smt2/CMakeLists.txt
+++ b/src/parsers/smt2/CMakeLists.txt
@ -0,0 +1,8 @@
+z3_add_component(smt2parser
+  SOURCES
+    smt2parser.cpp
+    smt2scanner.cpp
+  COMPONENT_DEPENDENCIES
+    cmd_context
+    parser_util
+)
--- a/src/parsers/util/CMakeLists.txt
+++ b/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
+)
--- a/src/qe/CMakeLists.txt
+++ b/src/qe/CMakeLists.txt
@ -0,0 +1,28 @@
+z3_add_component(qe
+  SOURCES
+    nlarith_util.cpp
+    nlqsat.cpp
+    qe_arith.cpp
+    qe_arith_plugin.cpp
+    qe_array_plugin.cpp
+    qe_arrays.cpp
+    qe_bool_plugin.cpp
+    qe_bv_plugin.cpp
+    qe_cmd.cpp
+    qe.cpp
+    qe_datatype_plugin.cpp
+    qe_datatypes.cpp
+    qe_dl_plugin.cpp
+    qe_lite.cpp
+    qe_mbp.cpp
+    qe_sat_tactic.cpp
+    qe_tactic.cpp
+    qsat.cpp
+    vsubst_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    nlsat_tactic
+    nlsat
+    sat
+    smt   
+    tactic 
+)
--- a/src/sat/CMakeLists.txt
+++ b/src/sat/CMakeLists.txt
@ -0,0 +1,28 @@
+z3_add_component(sat
+  SOURCES
+    dimacs.cpp
+    sat_asymm_branch.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_par.cpp
+    sat_probing.cpp
+    sat_scc.cpp
+    sat_simplifier.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
+)
--- a/src/sat/sat_solver/CMakeLists.txt
+++ b/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
+)
--- a/src/sat/tactic/CMakeLists.txt
+++ b/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
+)
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@ -0,0 +1,48 @@
+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
+  lp_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 "${CMAKE_INSTALL_BINDIR}"
+)
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@ -0,0 +1,82 @@
+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_consequences.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
+    smt2_extra_cmds.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_lra.cpp
+    theory_opt.cpp
+    theory_pb.cpp
+    theory_seq.cpp
+    theory_str.cpp
+    theory_utvpi.cpp
+    theory_wmaxsat.cpp
+    uses_theory.cpp
+    watch_list.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    cmd_context
+    euclid
+    fpa
+    grobner
+    lp
+    macros
+    normal_forms
+    parser_util
+    pattern
+    proof_checker
+    proto_model
+    simplex
+    substitution
+)
--- a/src/smt/params/CMakeLists.txt
+++ b/src/smt/params/CMakeLists.txt
@ -0,0 +1,19 @@
+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
+    theory_str_params.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    bit_blaster
+    pattern
+    simplifier
+  PYG_FILES
+    smt_params_helper.pyg
+)
--- a/src/smt/proto_model/CMakeLists.txt
+++ b/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
+)
--- a/src/smt/tactic/CMakeLists.txt
+++ b/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
+)
--- a/src/solver/CMakeLists.txt
+++ b/src/solver/CMakeLists.txt
@ -0,0 +1,16 @@
+z3_add_component(solver
+  SOURCES
+    check_sat_result.cpp
+    combined_solver.cpp
+    mus.cpp
+    smt_logics.cpp
+    solver.cpp
+    solver_na2as.cpp
+    solver2tactic.cpp
+    tactic2solver.cpp
+  COMPONENT_DEPENDENCIES
+    model
+    tactic
+  PYG_FILES
+    combined_solver_params.pyg
+)
--- a/src/tactic/CMakeLists.txt
+++ b/src/tactic/CMakeLists.txt
@ -0,0 +1,21 @@
+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
+    sine_filter.cpp
+    tactical.cpp
+    tactic.cpp
+  COMPONENT_DEPENDENCIES
+    ast
+    model
+)
--- a/src/tactic/aig/CMakeLists.txt
+++ b/src/tactic/aig/CMakeLists.txt
@ -0,0 +1,7 @@
+z3_add_component(aig_tactic
+  SOURCES
+    aig.cpp
+    aig_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    tactic
+)
--- a/src/tactic/arith/CMakeLists.txt
+++ b/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
+)
--- a/src/tactic/bv/CMakeLists.txt
+++ b/src/tactic/bv/CMakeLists.txt
@ -0,0 +1,18 @@
+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_bound_chk_tactic.cpp
+    bv_bounds_tactic.cpp
+    bv_size_reduction_tactic.cpp
+    dt2bv_tactic.cpp
+    elim_small_bv_tactic.cpp
+    max_bv_sharing_tactic.cpp
+  COMPONENT_DEPENDENCIES
+    bit_blaster
+    core_tactics
+    tactic
+)
--- a/src/tactic/core/CMakeLists.txt
+++ b/src/tactic/core/CMakeLists.txt
@ -0,0 +1,27 @@
+z3_add_component(core_tactics
+  SOURCES
+    blast_term_ite_tactic.cpp
+    cofactor_elim_term_ite.cpp
+    cofactor_term_ite_tactic.cpp
+    collect_statistics_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
+    collect_occs.cpp
+  COMPONENT_DEPENDENCIES
+    normal_forms
+    tactic
+)
+
--- a/src/tactic/fpa/CMakeLists.txt
+++ b/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
+)
--- a/src/tactic/nlsat_smt/CMakeLists.txt
+++ b/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
+)
--- a/src/tactic/portfolio/CMakeLists.txt
+++ b/src/tactic/portfolio/CMakeLists.txt
@ -0,0 +1,19 @@
+z3_add_component(portfolio
+  SOURCES
+    default_tactic.cpp
+    enum2bv_solver.cpp
+    pb2bv_solver.cpp
+    bounded_int2bv_solver.cpp
+    fd_solver.cpp
+    smt_strategic_solver.cpp
+  COMPONENT_DEPENDENCIES
+    aig_tactic
+    fp
+    fpa_tactics
+    qe
+    sat_solver
+    sls_tactic
+    smtlogic_tactics
+    subpaving_tactic
+    ufbv_tactic
+)
--- a/src/tactic/sls/CMakeLists.txt
+++ b/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
+)
--- a/src/tactic/smtlogics/CMakeLists.txt
+++ b/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
+)
--- a/src/tactic/ufbv/CMakeLists.txt
+++ b/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
+)
--- a/src/test/CMakeLists.txt
+++ b/src/test/CMakeLists.txt
@ -0,0 +1,134 @@
+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
+  cnf_backbones.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_consequences.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_based_opt.cpp
+  model_evaluator.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
+  pb2bv.cpp
+  pdr.cpp
+  permutation.cpp
+  polynomial.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
+  lp.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})
+
+
+
--- a/src/test/fuzzing/CMakeLists.txt
+++ b/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
+)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@ -0,0 +1,62 @@
+if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h")
+  message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\""
+          ${z3_polluted_tree_msg}
+  )
+endif()
+
+set(Z3_FULL_VERSION "\"${Z3_FULL_VERSION_STR}\"")
+configure_file(version.h.cmake.in ${CMAKE_CURRENT_BINARY_DIR}/version.h)
+
+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
+)
--- a/src/util/lp/CMakeLists.txt
+++ b/src/util/lp/CMakeLists.txt
@ -0,0 +1,35 @@
+z3_add_component(lp
+  SOURCES
+    lp_utils.cpp
+    binary_heap_priority_queue_instances.cpp
+    binary_heap_upair_queue_instances.cpp
+    bound_propagator.cpp
+    core_solver_pretty_printer_instances.cpp
+    dense_matrix_instances.cpp
+    eta_matrix_instances.cpp
+    indexed_vector_instances.cpp
+    lar_core_solver_instances.cpp
+    lp_core_solver_base_instances.cpp
+    lp_dual_core_solver_instances.cpp
+    lp_dual_simplex_instances.cpp
+    lp_primal_core_solver_instances.cpp
+    lp_primal_simplex_instances.cpp
+    lp_settings_instances.cpp
+    lp_solver_instances.cpp
+    lu_instances.cpp
+    matrix_instances.cpp
+    permutation_matrix_instances.cpp
+	quick_xplain.cpp
+    row_eta_matrix_instances.cpp
+    scaler_instances.cpp
+    sparse_matrix_instances.cpp
+    square_dense_submatrix_instances.cpp
+    static_matrix_instances.cpp
+    random_updater_instances.cpp      
+  COMPONENT_DEPENDENCIES
+    util
+  PYG_FILES
+    lp_params.pyg
+)
+
+include_directories(${src_SOURCE_DIR})