diff --git a/.gitignore b/.gitignore index 58abdcf7379..80a50ea9f14 100644 --- a/.gitignore +++ b/.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 diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000000..0e95cb65a4e --- /dev/null +++ b/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 $<$:Z3DEBUG>) +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_EXTERNAL_RELEASE>) +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_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 $<$:_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 +) diff --git a/README-CMake.md b/README-CMake.md new file mode 100644 index 00000000000..28f49cf2716 --- /dev/null +++ b/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=`` +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=`` where +```` 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 + +``` +$<$: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. diff --git a/README.md b/README.md index 534c6c378da..6052e2f9129 100644 --- a/README.md +++ b/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. diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py new file mode 100755 index 00000000000..a3c81fb250c --- /dev/null +++ b/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:])) diff --git a/contrib/cmake/cmake/cmake_uninstall.cmake.in b/contrib/cmake/cmake/cmake_uninstall.cmake.in new file mode 100644 index 00000000000..cbe8c274977 --- /dev/null +++ b/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() diff --git a/contrib/cmake/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake new file mode 100644 index 00000000000..d951805deb6 --- /dev/null +++ b/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) diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake new file mode 100644 index 00000000000..c214e446466 --- /dev/null +++ b/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() diff --git a/contrib/cmake/cmake/modules/FindGMP.cmake b/contrib/cmake/cmake/modules/FindGMP.cmake new file mode 100644 index 00000000000..b749750efc5 --- /dev/null +++ b/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) diff --git a/contrib/cmake/cmake/target_arch_detect.cmake b/contrib/cmake/cmake/target_arch_detect.cmake new file mode 100644 index 00000000000..68194cfe47d --- /dev/null +++ b/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() diff --git a/contrib/cmake/cmake/target_arch_detect.cpp b/contrib/cmake/cmake/target_arch_detect.cpp new file mode 100644 index 00000000000..8053e3532e5 --- /dev/null +++ b/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 diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/contrib/cmake/cmake/z3_add_component.cmake new file mode 100644 index 00000000000..eebc0c8d96f --- /dev/null +++ b/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 ``.pyg`` files that should used to be generate +# ``_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() diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/contrib/cmake/cmake/z3_add_cxx_flag.cmake new file mode 100644 index 00000000000..0c56bb0f612 --- /dev/null +++ b/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() diff --git a/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake b/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake new file mode 100644 index 00000000000..3eb1e2d340d --- /dev/null +++ b/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() diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt new file mode 100644 index 00000000000..b8cecbe631e --- /dev/null +++ b/contrib/cmake/examples/CMakeLists.txt @@ -0,0 +1,2 @@ +add_subdirectory(c) +add_subdirectory(c++) diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt new file mode 100644 index 00000000000..85bbd77c712 --- /dev/null +++ b/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++") diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt new file mode 100644 index 00000000000..1a14573ac38 --- /dev/null +++ b/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") diff --git a/contrib/cmake/maintainers.txt b/contrib/cmake/maintainers.txt new file mode 100644 index 00000000000..caa6798c66d --- /dev/null +++ b/contrib/cmake/maintainers.txt @@ -0,0 +1,3 @@ +# Maintainers + +- Dan Liew (@delcypher) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt new file mode 100644 index 00000000000..6708f505e27 --- /dev/null +++ b/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 $) +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 diff --git a/contrib/cmake/src/ackermannization/CMakeLists.txt b/contrib/cmake/src/ackermannization/CMakeLists.txt new file mode 100644 index 00000000000..93529ae1286 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt new file mode 100644 index 00000000000..0fd012b87bd --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/api/dll/CMakeLists.txt b/contrib/cmake/src/api/dll/CMakeLists.txt new file mode 100644 index 00000000000..31b0fb576c6 --- /dev/null +++ b/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}) diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt new file mode 100644 index 00000000000..2279be716b3 --- /dev/null +++ b/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() diff --git a/contrib/cmake/src/ast/CMakeLists.txt b/contrib/cmake/src/ast/CMakeLists.txt new file mode 100644 index 00000000000..de0e4bdaf7c --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/fpa/CMakeLists.txt b/contrib/cmake/src/ast/fpa/CMakeLists.txt new file mode 100644 index 00000000000..12298b573b4 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/macros/CMakeLists.txt b/contrib/cmake/src/ast/macros/CMakeLists.txt new file mode 100644 index 00000000000..ca38b4759c8 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/normal_forms/CMakeLists.txt b/contrib/cmake/src/ast/normal_forms/CMakeLists.txt new file mode 100644 index 00000000000..30702cd8c0f --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/contrib/cmake/src/ast/pattern/CMakeLists.txt new file mode 100644 index 00000000000..8cff3e739d5 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/proof_checker/CMakeLists.txt b/contrib/cmake/src/ast/proof_checker/CMakeLists.txt new file mode 100644 index 00000000000..5c947adec48 --- /dev/null +++ b/contrib/cmake/src/ast/proof_checker/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(proof_checker + SOURCES + proof_checker.cpp + COMPONENT_DEPENDENCIES + rewriter +) diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt new file mode 100644 index 00000000000..59834ea1316 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt new file mode 100644 index 00000000000..9eea1558ec7 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/contrib/cmake/src/ast/simplifier/CMakeLists.txt new file mode 100644 index 00000000000..7597374a614 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/ast/substitution/CMakeLists.txt b/contrib/cmake/src/ast/substitution/CMakeLists.txt new file mode 100644 index 00000000000..80e12c9953b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/cmd_context/CMakeLists.txt b/contrib/cmake/src/cmd_context/CMakeLists.txt new file mode 100644 index 00000000000..8b2d10eec0e --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt b/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt new file mode 100644 index 00000000000..3aef1a55396 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/duality/CMakeLists.txt b/contrib/cmake/src/duality/CMakeLists.txt new file mode 100644 index 00000000000..eb2d5c4f287 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/interp/CMakeLists.txt b/contrib/cmake/src/interp/CMakeLists.txt new file mode 100644 index 00000000000..949811b93f2 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/math/automata/CMakeLists.txt b/contrib/cmake/src/math/automata/CMakeLists.txt new file mode 100644 index 00000000000..1fffd24a84f --- /dev/null +++ b/contrib/cmake/src/math/automata/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(automata + SOURCES + automaton.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/contrib/cmake/src/math/euclid/CMakeLists.txt b/contrib/cmake/src/math/euclid/CMakeLists.txt new file mode 100644 index 00000000000..a72f02b2809 --- /dev/null +++ b/contrib/cmake/src/math/euclid/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(euclid + SOURCES + euclidean_solver.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/contrib/cmake/src/math/grobner/CMakeLists.txt b/contrib/cmake/src/math/grobner/CMakeLists.txt new file mode 100644 index 00000000000..1b56c775fdb --- /dev/null +++ b/contrib/cmake/src/math/grobner/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(grobner + SOURCES + grobner.cpp + COMPONENT_DEPENDENCIES + ast +) diff --git a/contrib/cmake/src/math/hilbert/CMakeLists.txt b/contrib/cmake/src/math/hilbert/CMakeLists.txt new file mode 100644 index 00000000000..2e44140b8ad --- /dev/null +++ b/contrib/cmake/src/math/hilbert/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(hilbert + SOURCES + hilbert_basis.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/contrib/cmake/src/math/interval/CMakeLists.txt b/contrib/cmake/src/math/interval/CMakeLists.txt new file mode 100644 index 00000000000..390529b9dff --- /dev/null +++ b/contrib/cmake/src/math/interval/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(interval + SOURCES + interval_mpq.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/contrib/cmake/src/math/polynomial/CMakeLists.txt b/contrib/cmake/src/math/polynomial/CMakeLists.txt new file mode 100644 index 00000000000..1792f50aaa5 --- /dev/null +++ b/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 +) + diff --git a/contrib/cmake/src/math/realclosure/CMakeLists.txt b/contrib/cmake/src/math/realclosure/CMakeLists.txt new file mode 100644 index 00000000000..beb5f147b54 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/math/simplex/CMakeLists.txt b/contrib/cmake/src/math/simplex/CMakeLists.txt new file mode 100644 index 00000000000..6f965919d5a --- /dev/null +++ b/contrib/cmake/src/math/simplex/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(simplex + SOURCES + simplex.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/contrib/cmake/src/math/subpaving/CMakeLists.txt b/contrib/cmake/src/math/subpaving/CMakeLists.txt new file mode 100644 index 00000000000..be88f63cd1f --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt b/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt new file mode 100644 index 00000000000..eedb0ed4da1 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/model/CMakeLists.txt b/contrib/cmake/src/model/CMakeLists.txt new file mode 100644 index 00000000000..0e685e07cf5 --- /dev/null +++ b/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 +) + diff --git a/contrib/cmake/src/muz/base/CMakeLists.txt b/contrib/cmake/src/muz/base/CMakeLists.txt new file mode 100644 index 00000000000..ec1ce47c301 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/muz/bmc/CMakeLists.txt b/contrib/cmake/src/muz/bmc/CMakeLists.txt new file mode 100644 index 00000000000..dcd99898e85 --- /dev/null +++ b/contrib/cmake/src/muz/bmc/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(bmc + SOURCES + dl_bmc_engine.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/contrib/cmake/src/muz/clp/CMakeLists.txt b/contrib/cmake/src/muz/clp/CMakeLists.txt new file mode 100644 index 00000000000..32d9a928ebf --- /dev/null +++ b/contrib/cmake/src/muz/clp/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(clp + SOURCES + clp_context.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/contrib/cmake/src/muz/dataflow/CMakeLists.txt b/contrib/cmake/src/muz/dataflow/CMakeLists.txt new file mode 100644 index 00000000000..3fc1e1f1955 --- /dev/null +++ b/contrib/cmake/src/muz/dataflow/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(dataflow + SOURCES + dataflow.cpp + COMPONENT_DEPENDENCIES + muz +) diff --git a/contrib/cmake/src/muz/ddnf/CMakeLists.txt b/contrib/cmake/src/muz/ddnf/CMakeLists.txt new file mode 100644 index 00000000000..55d6bae5d25 --- /dev/null +++ b/contrib/cmake/src/muz/ddnf/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(ddnf + SOURCES + ddnf.cpp + COMPONENT_DEPENDENCIES + muz + rel + transforms +) diff --git a/contrib/cmake/src/muz/duality/CMakeLists.txt b/contrib/cmake/src/muz/duality/CMakeLists.txt new file mode 100644 index 00000000000..f005b88b1c4 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/muz/fp/CMakeLists.txt b/contrib/cmake/src/muz/fp/CMakeLists.txt new file mode 100644 index 00000000000..239c4df124b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/muz/pdr/CMakeLists.txt b/contrib/cmake/src/muz/pdr/CMakeLists.txt new file mode 100644 index 00000000000..ca2992b9792 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/muz/rel/CMakeLists.txt b/contrib/cmake/src/muz/rel/CMakeLists.txt new file mode 100644 index 00000000000..720714ed854 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/muz/tab/CMakeLists.txt b/contrib/cmake/src/muz/tab/CMakeLists.txt new file mode 100644 index 00000000000..cfae51280a0 --- /dev/null +++ b/contrib/cmake/src/muz/tab/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(tab + SOURCES + tab_context.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/contrib/cmake/src/muz/transforms/CMakeLists.txt b/contrib/cmake/src/muz/transforms/CMakeLists.txt new file mode 100644 index 00000000000..6a0a1ac9c23 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/nlsat/CMakeLists.txt b/contrib/cmake/src/nlsat/CMakeLists.txt new file mode 100644 index 00000000000..d0c1379e586 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/nlsat/tactic/CMakeLists.txt b/contrib/cmake/src/nlsat/tactic/CMakeLists.txt new file mode 100644 index 00000000000..9ea26a0c586 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/contrib/cmake/src/opt/CMakeLists.txt new file mode 100644 index 00000000000..c50f8be52bb --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/parsers/smt/CMakeLists.txt b/contrib/cmake/src/parsers/smt/CMakeLists.txt new file mode 100644 index 00000000000..2edf7b6794d --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/parsers/smt2/CMakeLists.txt b/contrib/cmake/src/parsers/smt2/CMakeLists.txt new file mode 100644 index 00000000000..1467d95c6f1 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/parsers/util/CMakeLists.txt b/contrib/cmake/src/parsers/util/CMakeLists.txt new file mode 100644 index 00000000000..6ede4b77305 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/contrib/cmake/src/qe/CMakeLists.txt new file mode 100644 index 00000000000..9db253bd605 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt new file mode 100644 index 00000000000..cfc3835c11b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/sat/sat_solver/CMakeLists.txt b/contrib/cmake/src/sat/sat_solver/CMakeLists.txt new file mode 100644 index 00000000000..14eb4ac2550 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/sat/tactic/CMakeLists.txt b/contrib/cmake/src/sat/tactic/CMakeLists.txt new file mode 100644 index 00000000000..74aeba8b962 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/contrib/cmake/src/shell/CMakeLists.txt new file mode 100644 index 00000000000..65b97aaafc0 --- /dev/null +++ b/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 $) + 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}" +) diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/contrib/cmake/src/smt/CMakeLists.txt new file mode 100644 index 00000000000..e9306b2d693 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/smt/params/CMakeLists.txt b/contrib/cmake/src/smt/params/CMakeLists.txt new file mode 100644 index 00000000000..67224a2876b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/smt/proto_model/CMakeLists.txt b/contrib/cmake/src/smt/proto_model/CMakeLists.txt new file mode 100644 index 00000000000..0539c0fb0c6 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/smt/tactic/CMakeLists.txt b/contrib/cmake/src/smt/tactic/CMakeLists.txt new file mode 100644 index 00000000000..b7525bda846 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt new file mode 100644 index 00000000000..5e76c91ce76 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/contrib/cmake/src/tactic/CMakeLists.txt new file mode 100644 index 00000000000..318803cd218 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/aig/CMakeLists.txt b/contrib/cmake/src/tactic/aig/CMakeLists.txt new file mode 100644 index 00000000000..1e1a0d26690 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/arith/CMakeLists.txt b/contrib/cmake/src/tactic/arith/CMakeLists.txt new file mode 100644 index 00000000000..cdc42367a2b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/contrib/cmake/src/tactic/bv/CMakeLists.txt new file mode 100644 index 00000000000..42cff2bfc33 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt new file mode 100644 index 00000000000..d59265c5cda --- /dev/null +++ b/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 +) + diff --git a/contrib/cmake/src/tactic/fpa/CMakeLists.txt b/contrib/cmake/src/tactic/fpa/CMakeLists.txt new file mode 100644 index 00000000000..d93cd5b821d --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt b/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt new file mode 100644 index 00000000000..e28b1196651 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt new file mode 100644 index 00000000000..d20af772b8b --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/sls/CMakeLists.txt b/contrib/cmake/src/tactic/sls/CMakeLists.txt new file mode 100644 index 00000000000..8b720b333dc --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt b/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt new file mode 100644 index 00000000000..840dd008a7c --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/tactic/ufbv/CMakeLists.txt b/contrib/cmake/src/tactic/ufbv/CMakeLists.txt new file mode 100644 index 00000000000..c1d6daaaa18 --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt new file mode 100644 index 00000000000..b6166b3f8b8 --- /dev/null +++ b/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 $) +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}) diff --git a/contrib/cmake/src/test/fuzzing/CMakeLists.txt b/contrib/cmake/src/test/fuzzing/CMakeLists.txt new file mode 100644 index 00000000000..c2bc61ed5cb --- /dev/null +++ b/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 +) diff --git a/contrib/cmake/src/util/CMakeLists.txt b/contrib/cmake/src/util/CMakeLists.txt new file mode 100644 index 00000000000..c8507653179 --- /dev/null +++ b/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 +) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py new file mode 100755 index 00000000000..543c56e0e0d --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py new file mode 100755 index 00000000000..2b9b5a0716c --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py new file mode 100755 index 00000000000..1c7e221ba41 --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py new file mode 100755 index 00000000000..f8323d73149 --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py new file mode 100755 index 00000000000..c8b68049f1a --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py new file mode 100755 index 00000000000..3f2e7c50775 --- /dev/null +++ b/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:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a02a9b40fee..1185217edf8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2488,10 +2488,10 @@ def mk_auto_src(): 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' } @@ -2524,8 +2524,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) @@ -2590,28 +2590,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(): @@ -2629,15 +2632,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): @@ -2674,6 +2682,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 = [] @@ -2685,12 +2700,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: @@ -2743,6 +2757,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') @@ -2752,12 +2773,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: @@ -2802,11 +2822,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 = [] @@ -2817,12 +2844,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: @@ -2863,14 +2889,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: @@ -2936,7 +2970,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() @@ -2949,6 +3004,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("^ *//.*$") @@ -2957,14 +3023,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 @@ -3025,7 +3086,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 diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py new file mode 100755 index 00000000000..f1ada2b84ae --- /dev/null +++ b/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:])) + diff --git a/scripts/update_api.py b/scripts/update_api.py old mode 100644 new mode 100755 index badd960ccc6..d5cc92a7f72 --- a/scripts/update_api.py +++ b/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\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() - -log_h.close() -log_c.close() -exe_c.close() -core_py.close() - -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')) + raise mk_exec_header.MKException("Failed to process API definition: %s" % line) + +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') + + +def write_log_c_preamble(log_c): + log_c.write('// Automatically generated file\n') + log_c.write('#include\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:])) diff --git a/src/interp/iz3params.pyg b/src/interp/interp_params.pyg similarity index 100% rename from src/interp/iz3params.pyg rename to src/interp/interp_params.pyg diff --git a/src/math/polynomial/algebraic.pyg b/src/math/polynomial/algebraic_params.pyg similarity index 100% rename from src/math/polynomial/algebraic.pyg rename to src/math/polynomial/algebraic_params.pyg diff --git a/src/math/realclosure/rcf.pyg b/src/math/realclosure/rcf_params.pyg similarity index 100% rename from src/math/realclosure/rcf.pyg rename to src/math/realclosure/rcf_params.pyg diff --git a/src/util/version.h.in b/src/util/version.h.in new file mode 100644 index 00000000000..05b619f2d67 --- /dev/null +++ b/src/util/version.h.in @@ -0,0 +1,5 @@ +// automatically generated file. +#define Z3_MAJOR_VERSION @Z3_VERSION_MAJOR@ +#define Z3_MINOR_VERSION @Z3_VERSION_MINOR@ +#define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@ +#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@