diff --git a/.gitignore b/.gitignore index 58abdcf73..80a50ea9f 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 000000000..0e95cb65a --- /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 000000000..28f49cf27 --- /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 534c6c378..6052e2f91 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 000000000..a3c81fb25 --- /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 000000000..cbe8c2749 --- /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 000000000..d951805de --- /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 000000000..c214e4464 --- /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 000000000..b749750ef --- /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 000000000..68194cfe4 --- /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 000000000..8053e3532 --- /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 000000000..eebc0c8d9 --- /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 000000000..0c56bb0f6 --- /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 000000000..3eb1e2d34 --- /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 000000000..b8cecbe63 --- /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 000000000..85bbd77c7 --- /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 000000000..1a14573ac --- /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 000000000..caa6798c6 --- /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 000000000..6708f505e --- /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 000000000..93529ae12 --- /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 000000000..0fd012b87 --- /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 000000000..31b0fb576 --- /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 000000000..2279be716 --- /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 000000000..de0e4bdaf --- /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 000000000..12298b573 --- /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 000000000..ca38b4759 --- /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 000000000..30702cd8c --- /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 000000000..8cff3e739 --- /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 000000000..5c947adec --- /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 000000000..59834ea13 --- /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 000000000..9eea1558e --- /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 000000000..7597374a6 --- /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 000000000..80e12c995 --- /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 000000000..8b2d10eec --- /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 000000000..3aef1a553 --- /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 000000000..eb2d5c4f2 --- /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 000000000..949811b93 --- /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 000000000..1fffd24a8 --- /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 000000000..a72f02b28 --- /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 000000000..1b56c775f --- /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 000000000..2e44140b8 --- /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 000000000..390529b9d --- /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 000000000..1792f50aa --- /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 000000000..beb5f147b --- /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 000000000..6f965919d --- /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 000000000..be88f63cd --- /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 000000000..eedb0ed4d --- /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 000000000..0e685e07c --- /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 000000000..ec1ce47c3 --- /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 000000000..dcd99898e --- /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 000000000..32d9a928e --- /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 000000000..3fc1e1f19 --- /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 000000000..55d6bae5d --- /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 000000000..f005b88b1 --- /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 000000000..239c4df12 --- /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 000000000..ca2992b97 --- /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 000000000..720714ed8 --- /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 000000000..cfae51280 --- /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 000000000..6a0a1ac9c --- /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 000000000..d0c1379e5 --- /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 000000000..9ea26a0c5 --- /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 000000000..c50f8be52 --- /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 000000000..2edf7b679 --- /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 000000000..1467d95c6 --- /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 000000000..6ede4b773 --- /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 000000000..9db253bd6 --- /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 000000000..cfc3835c1 --- /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 000000000..14eb4ac25 --- /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 000000000..74aeba8b9 --- /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 000000000..65b97aaaf --- /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 000000000..e9306b2d6 --- /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 000000000..67224a287 --- /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 000000000..0539c0fb0 --- /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 000000000..b7525bda8 --- /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 000000000..5e76c91ce --- /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 000000000..318803cd2 --- /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 000000000..1e1a0d266 --- /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 000000000..cdc42367a --- /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 000000000..42cff2bfc --- /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 000000000..d59265c5c --- /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 000000000..d93cd5b82 --- /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 000000000..e28b11966 --- /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 000000000..d20af772b --- /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 000000000..8b720b333 --- /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 000000000..840dd008a --- /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 000000000..c1d6daaaa --- /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 000000000..b6166b3f8 --- /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 000000000..c2bc61ed5 --- /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 000000000..c85076531 --- /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 000000000..543c56e0e --- /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 000000000..2b9b5a071 --- /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 000000000..1c7e221ba --- /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 000000000..f8323d731 --- /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 000000000..c8b68049f --- /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 000000000..3f2e7c507 --- /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_unix_dist.py b/scripts/mk_unix_dist.py index 60a7cbdca..999d495a3 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -65,6 +65,7 @@ def parse_options(): 'silent', 'force', 'nojava', + 'nodotnet', 'githash' ]) for opt, arg in options: @@ -95,7 +96,7 @@ def check_build_dir(path): # Create a build directory using mk_make.py def mk_build_dir(path): if not check_build_dir(path) or FORCE_MK: - opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path, "--static"] + opts = ["python", os.path.join('scripts', 'mk_make.py'), "-b", path, "--staticlib"] if DOTNET_ENABLED: opts.append('--dotnet') if JAVA_ENABLED: diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 31f9ebbd8..b15399070 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -83,6 +83,7 @@ JAVA_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False +STATIC_BIN=False VER_MAJOR=None VER_MINOR=None VER_BUILD=None @@ -536,6 +537,9 @@ def get_version(): def build_static_lib(): return STATIC_LIB +def build_static_bin(): + return STATIC_BIN + def is_cr_lf(fname): # Check whether text files use cr/lf f = open(fname, 'r') @@ -622,6 +626,7 @@ def display_help(exit_code): print(" --ml generate OCaml bindings.") print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") + print(" --staticbin build a statically linked Z3 binary.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") @@ -652,14 +657,14 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED + global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python']) + 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python', 'staticbin']) except: print("ERROR: Invalid command line option") display_help(1) @@ -694,6 +699,8 @@ def parse_options(): DOTNET_ENABLED = True elif opt in ('--staticlib'): STATIC_LIB = True + elif opt in ('--staticbin'): + STATIC_BIN = True elif opt in ('--optimize'): SLOW_OPTIMIZE = True elif not IS_WINDOWS and opt in ('-p', '--prefix'): @@ -2212,14 +2219,19 @@ def mk_config(): extra_opt = ' -D_NO_OMP_' if GIT_HASH: extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) + if STATIC_BIN: + static_opt = '/MT' + else: + static_opt = '/MD' if DEBUG_MODE: + static_opt = static_opt + 'd' config.write( 'AR_FLAGS=/nologo\n' - 'LINK_FLAGS=/nologo /MDd\n' - 'SLINK_FLAGS=/nologo /LDd\n') + 'LINK_FLAGS=/nologo %s\n' + 'SLINK_FLAGS=/nologo /LDd\n' % static_opt) if VS_X64: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2228,7 +2240,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) + 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') @@ -2237,15 +2249,14 @@ def mk_config(): LTCG=' /LTCG' if SLOW_OPTIMIZE else '' GL = ' /GL' if SLOW_OPTIMIZE else '' config.write( - 'AR_FLAGS=/nologo%s\n' - 'LINK_FLAGS=/nologo /MD\n' - 'SLINK_FLAGS=/nologo /LD\n' - % LTCG) + 'AR_FLAGS=/nologo %s\n' + 'LINK_FLAGS=/nologo %s\n' + 'SLINK_FLAGS=/nologo /LD\n' % (LTCG, static_opt)) if TRACE: extra_opt = '%s /D _TRACE ' % extra_opt if VS_X64: config.write( - 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % (GL, extra_opt)) + 'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n' 'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n' % (LTCG, LTCG)) @@ -2254,7 +2265,7 @@ def mk_config(): exit(1) else: config.write( - 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % (GL, extra_opt)) + 'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt)) config.write( 'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n' % (LTCG, LTCG)) @@ -2363,7 +2374,9 @@ def mk_config(): LDFLAGS = '%s -m32' % LDFLAGS SLIBFLAGS = '%s -m32' % SLIBFLAGS if DEBUG_MODE: - CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS + CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS + else: + CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS if TRACE or DEBUG_MODE: CPPFLAGS = '%s -D_TRACE' % CPPFLAGS config.write('PREFIX=%s\n' % PREFIX) @@ -2379,7 +2392,10 @@ def mk_config(): config.write('AR_OUTFLAG=\n') config.write('EXE_EXT=\n') config.write('LINK=%s\n' % CXX) - config.write('LINK_FLAGS=\n') + if STATIC_BIN: + config.write('LINK_FLAGS=-static\n') + else: + config.write('LINK_FLAGS=\n') config.write('LINK_OUT_FLAG=-o \n') config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS) config.write('SO_EXT=%s\n' % SO_EXT) @@ -2511,10 +2527,10 @@ DOUBLE = 2 STRING = 3 SYMBOL = 4 UINT_MAX = 4294967295 -CURR_PYG = None +CURRENT_PYG_HPP_DEST_DIR = None -def get_curr_pyg(): - return CURR_PYG +def get_current_pyg_hpp_dest_dir(): + return CURRENT_PYG_HPP_DEST_DIR TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } @@ -2547,8 +2563,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) @@ -2613,28 +2629,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(): @@ -2652,15 +2671,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): @@ -2697,6 +2721,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 = [] @@ -2708,12 +2739,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: @@ -2766,6 +2796,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') @@ -2775,12 +2812,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: @@ -2825,11 +2861,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 = [] @@ -2840,12 +2883,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: @@ -2886,14 +2928,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: @@ -2959,7 +3009,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() @@ -2972,6 +3043,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("^ *//.*$") @@ -2980,14 +3062,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 @@ -3048,7 +3125,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 @@ -3480,7 +3557,7 @@ def mk_vs_proj_cl_compile(f, name, components, debug): if debug: f.write(' WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') else: - f.write(' WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') + f.write(' WIN32;NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)\n') if VS_PAR: f.write(' false\n') f.write(' true\n') diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py new file mode 100755 index 000000000..f1ada2b84 --- /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 57a3d6adb..bf3f90151 --- 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) @@ -422,10 +344,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') @@ -472,10 +392,8 @@ def mk_dotnet(): NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ] 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") @@ -560,16 +478,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') @@ -642,7 +557,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') @@ -805,7 +720,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): @@ -1080,7 +995,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)) @@ -1271,7 +1186,8 @@ def ml_set_wrap(t, d, n): pts = ml_plus_type(type2str(t)) return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';' -def mk_z3native_ml(ml_dir): +def mk_ml(ml_dir): + global Type2Str ml_nativef = os.path.join(ml_dir, 'z3native.ml') ml_native = open(ml_nativef, 'w') ml_native.write('(* Automatically generated file *)\n\n') @@ -1574,24 +1490,15 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write('#ifdef __cplusplus\n') ml_wrapper.write('}\n') ml_wrapper.write('#endif\n') - if is_verbose(): - print ('Generated "%s"' % ml_wrapperf) - -def mk_ml(): - global Type2Str - if not is_ml_enabled(): - return - - ml_dir = get_component('ml').src_dir - mk_z3native_ml(ml_dir) - mk_z3native_stubs_c(ml_dir) + 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 ') @@ -1603,24 +1510,200 @@ def def_APIs(): if m: eval(line) except Exception: - raise MKException("Failed to process API definition: %s" % line) -def_Types() -def_APIs() -mk_bindings() -mk_py_wrappers() -mk_dotnet() -mk_dotnet_wrappers() -mk_java() -mk_ml() + raise mk_exec_header.MKException("Failed to process API definition: %s" % line) -log_h.close() -log_c.close() -exe_c.close() -core_py.close() +def write_log_h_preamble(log_h): + log_h.write('// Automatically generated file\n') + log_h.write('#include\"z3.h\"\n') + log_h.write('#ifdef __GNUC__\n') + log_h.write('#define _Z3_UNUSED __attribute__((unused))\n') + log_h.write('#else\n') + log_h.write('#define _Z3_UNUSED\n') + log_h.write('#endif\n') + # + log_h.write('extern std::ostream * g_z3_log;\n') + log_h.write('extern bool g_z3_log_enabled;\n') + log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n') + log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n') + log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') + log_h.write('void _Z3_append_log(char const * msg);\n') -if is_verbose(): - print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h')) - print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp')) - print("Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp')) - print("Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py')) - print("Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs')) + +def write_log_c_preamble(log_c): + log_c.write('// Automatically generated file\n') + log_c.write('#include\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/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 310269fec..123b496a1 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -24,8 +24,7 @@ Revision History: class ackermannize_bv_tactic : public tactic { public: ackermannize_bv_tactic(ast_manager& m, params_ref const& p) - : m_m(m) - , m_p(p) + : m(m), m_p(p) {} virtual ~ackermannize_bv_tactic() { } @@ -36,7 +35,6 @@ public: proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; - ast_manager& m(g->m()); tactic_report report("ackermannize", *g); fail_if_unsat_core_generation("ackermannize", g); fail_if_proof_generation("ackermannize", g); @@ -44,11 +42,11 @@ public: expr_ref_vector flas(m); const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); - scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas, NULL); - flas.reset(); + lackr lackr(m, m_p, m_st, flas, NULL); + // mk result goal_ref resg(alloc(goal, *g, true)); - const bool success = imp->mk_ackermann(resg, m_lemma_limit); + const bool success = lackr.mk_ackermann(resg, m_lemma_limit); if (!success) { // Just pass on the input unchanged result.reset(); result.push_back(g.get()); @@ -60,12 +58,12 @@ public: result.push_back(resg.get()); // report model if (g->models_enabled()) { - mc = mk_ackermannize_bv_model_converter(m, imp->get_info()); + mc = mk_ackermannize_bv_model_converter(m, lackr.get_info()); } - resg->inc_depth(); - TRACE("ackermannize", resg->display(tout);); - SASSERT(resg->is_well_sorted()); + resg->inc_depth(); + TRACE("ackermannize", resg->display(tout);); + SASSERT(resg->is_well_sorted()); } @@ -86,7 +84,7 @@ public: return alloc(ackermannize_bv_tactic, m, m_p); } private: - ast_manager& m_m; + ast_manager& m; params_ref m_p; lackr_stats m_st; double m_lemma_limit; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 088cd0d4d..5727d2dfb 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8944,7 +8944,31 @@ def fpFP(sgn, exp, sig, ctx=None): return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx) def fpToFP(a1, a2=None, a3=None, ctx=None): - """Create a Z3 floating-point conversion expression from other terms.""" + """Create a Z3 floating-point conversion expression from other term sorts + to floating-point. + + From a bit-vector term in IEEE 754-2008 format: + >>> x = FPVal(1.0, Float32()) + >>> x_bv = fpToIEEEBV(x) + >>> simplify(fpToFP(x_bv, Float32())) + 1 + + From a floating-point term with different precision: + >>> x = FPVal(1.0, Float32()) + >>> x_db = fpToFP(RNE(), x, Float64()) + >>> x_db.sort() + FPSort(11, 53) + + From a real term: + >>> x_r = RealVal(1.5) + >>> simplify(fpToFP(RNE(), x_r, Float32())) + 1.5 + + From a signed bit-vector term: + >>> x_signed = BitVecVal(-5, BitVecSort(32)) + >>> simplify(fpToFP(RNE(), x_signed, Float32())) + -1.25*(2**2) + """ ctx = _get_ctx(ctx) if is_bv(a1) and is_fp_sort(a2): return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), a1.ast, a2.ast), ctx) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 55a1b93d9..5c7a819da 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -62,7 +62,7 @@ DEFINE_TYPE(Z3_rcf_num); - \c Z3_constructor: type constructor for a (recursive) datatype. - \c Z3_constructor_list: list of constructors for a (recursive) datatype. - \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc. - - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. + - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. - \c Z3_model: model for the constraints asserted into the logical context. - \c Z3_func_interp: interpretation of a function in a model. - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point. @@ -1129,7 +1129,7 @@ typedef enum { Z3_OP_SEQ_EXTRACT, Z3_OP_SEQ_REPLACE, Z3_OP_SEQ_AT, - Z3_OP_SEQ_LENGTH, + Z3_OP_SEQ_LENGTH, Z3_OP_SEQ_INDEX, Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, @@ -1457,7 +1457,7 @@ extern "C" { /*@{*/ /** - \deprecated + \deprecated \brief Create a context using the given configuration. After a context is created, the configuration cannot be changed, @@ -1474,6 +1474,11 @@ extern "C" { Z3_solver, Z3_func_interp have to be managed by the caller. Their reference counts are not handled by the context. + Further remarks: + - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's. + - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, + Z3 will return the same pointer twice. + \sa Z3_del_context def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) @@ -1492,11 +1497,13 @@ extern "C" { anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD. - Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are - Z3_ast's. + Remarks: - After a context is created, the configuration cannot be changed. - All main interaction with Z3 happens in the context of a \c Z3_context. + - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's. + - After a context is created, the configuration cannot be changed. + - All main interaction with Z3 happens in the context of a \c Z3_context. + - Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, + Z3 will return the same pointer twice. def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),)) */ @@ -3185,11 +3192,11 @@ extern "C" { def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST))) */ - Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); + Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); /** \brief Retrieve the string constant stored in \c s. - + \pre Z3_is_string(c, s) def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) @@ -3285,7 +3292,7 @@ extern "C" { def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); - + /** \brief Create a regular expression that accepts the sequence \c seq. @@ -4429,8 +4436,8 @@ extern "C" { Provides an interface to the AST simplifier used by Z3. It returns an AST object which is equal to the argument. - The returned AST is simplified using algebraic simplificaiton rules, - such as constant propagation (propagating true/false over logical connectives). + The returned AST is simplified using algebraic simplificaiton rules, + such as constant propagation (propagating true/false over logical connectives). def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST))) */ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 2cf33941e..6d139a5bd 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2095,6 +2095,7 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2 } app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) { + bool type_error = decl->get_arity() != num_args && !decl->is_right_associative() && !decl->is_left_associative() && !decl->is_chainable(); diff --git a/src/ast/ast.h b/src/ast/ast.h index c386ccd63..6c69e4037 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -972,7 +972,7 @@ public: */ virtual bool is_unique_value(app * a) const { return false; } - virtual bool are_equal(app * a, app * b) const { return a == b && is_unique_value(a) && is_unique_value(b); } + virtual bool are_equal(app * a, app * b) const { return a == b; } virtual bool are_distinct(app * a, app * b) const { return a != b && is_unique_value(a) && is_unique_value(b); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index e31e5aab6..7d5248b30 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1075,7 +1075,7 @@ public: if (strcmp(var_prefix, ALIAS_PREFIX) == 0) { var_prefix = "_a"; } - unsigned idx = 1; + unsigned idx = 0; for (unsigned i = 0; i < num; i++) { symbol name = next_name(var_prefix, idx); name = ensure_quote_sym(name); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 40bb7efe8..0d90e1c5a 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM)); TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl; - tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); + tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;); m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result); } @@ -113,9 +113,10 @@ void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * a result = m.mk_true(); for (unsigned i = 0; i < num; i++) { for (unsigned j = i+1; j < num; j++) { - expr_ref eq(m); + expr_ref eq(m), neq(m); mk_eq(args[i], args[j], eq); - m_simp.mk_and(result, m.mk_not(eq), result); + neq = m.mk_not(eq); + m_simp.mk_and(result, neq, result); } } } @@ -422,10 +423,11 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, if (log2(sbits + 2) < ebits + 2) { // cap the delta - expr_ref cap(m), cap_le_delta(m); + expr_ref cap(m), cap_le_delta(m), exp_delta_ext(m); cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); - m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta_ext = m_bv_util.mk_zero_extend(2, exp_delta); + m_simp.mk_ite(cap_le_delta, cap, exp_delta_ext, exp_delta); exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); dbg_decouple("fpa2bv_add_exp_cap", cap); } @@ -465,7 +467,7 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref eq_sgn(m); m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); - // dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); + dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn); TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; ); // two extra bits for catching the overflow. @@ -478,11 +480,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_c_sig", c_sig); dbg_decouple("fpa2bv_add_shifted_d_sig", shifted_d_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(c_sig, shifted_d_sig), - m_bv_util.mk_bv_sub(c_sig, shifted_d_sig), - sum); + expr_ref sum(m), c_plus_d(m), c_minus_d(m); + c_plus_d = m_bv_util.mk_bv_add(c_sig, shifted_d_sig); + c_minus_d = m_bv_util.mk_bv_sub(c_sig, shifted_d_sig); + m_simp.mk_ite(eq_sgn, c_plus_d, c_minus_d, sum); SASSERT(is_well_sorted(m, sum)); @@ -594,7 +595,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args, c6 = y_is_zero; v6 = x; - // Actual addition. + //// Actual addition. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -949,8 +950,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); expr_ref shift_cond(m); shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); - m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig); - m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp); + expr_ref res_sig_shifted(m), res_exp_shifted(m); + res_sig_shifted = m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount); + res_exp_shifted = m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits + 1, 0, res_sig_shift_amount)); + m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig); + m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp); round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8); @@ -1374,8 +1378,9 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // (x is 0) || (y is 0) -> z m_simp.mk_or(x_is_zero, y_is_zero, c7); - expr_ref ite_c(m); - m_simp.mk_and(z_is_zero, m.mk_not(rm_is_to_neg), ite_c); + expr_ref ite_c(m), rm_is_not_to_neg(m); + rm_is_not_to_neg = m.mk_not(rm_is_to_neg); + m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c); mk_ite(ite_c, pzero, z, v7); // else comes the fused multiplication. @@ -1512,11 +1517,10 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_fma_add_e_sig", e_sig); dbg_decouple("fpa2bv_fma_add_shifted_f_sig", shifted_f_sig); - expr_ref sum(m); - m_simp.mk_ite(eq_sgn, - m_bv_util.mk_bv_add(e_sig, shifted_f_sig), - m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), - sum); + expr_ref sum(m), e_plus_f(m), e_minus_f(m); + e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig); + e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig), + m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum); SASSERT(is_well_sorted(m, sum)); @@ -1664,10 +1668,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_e_is_odd", e_is_odd); dbg_decouple("fpa2bv_sqrt_real_exp", real_exp); - expr_ref sig_prime(m); - m_simp.mk_ite(e_is_odd, m_bv_util.mk_concat(a_sig, zero1), - m_bv_util.mk_concat(zero1, a_sig), - sig_prime); + expr_ref sig_prime(m), a_z(m), z_a(m); + a_z = m_bv_util.mk_concat(a_sig, zero1); + z_a = m_bv_util.mk_concat(zero1, a_sig); + m_simp.mk_ite(e_is_odd, a_z, z_a, sig_prime); SASSERT(m_bv_util.get_bv_size(sig_prime) == sbits+1); dbg_decouple("fpa2bv_sqrt_sig_prime", sig_prime); @@ -1696,21 +1700,22 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, SASSERT(m_bv_util.get_bv_size(S) == sbits + 5); SASSERT(m_bv_util.get_bv_size(T) == sbits + 6); - expr_ref t_lt_0(m); - m_simp.mk_eq(m_bv_util.mk_extract(sbits+5, sbits+5, T), one1, t_lt_0); + expr_ref t_lt_0(m), T_lsds5(m); + T_lsds5 = m_bv_util.mk_extract(sbits + 5, sbits + 5, T); + m_simp.mk_eq(T_lsds5, one1, t_lt_0); expr * or_args[2] = { Q, S }; - - m_simp.mk_ite(t_lt_0, Q, - m_bv_util.mk_bv_or(2, or_args), - Q); - m_simp.mk_ite(t_lt_0, m_bv_util.mk_concat(m_bv_util.mk_extract(sbits+3, 0, R), zero1), - m_bv_util.mk_extract(sbits+4, 0, T), - R); + expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m); + Q_or_S = m_bv_util.mk_bv_or(2, or_args); + m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q); + R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1); + T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T); + m_simp.mk_ite(t_lt_0, R_shftd, T_lsds4, R); } - expr_ref is_exact(m); - m_simp.mk_eq(R, m_bv_util.mk_numeral(0, sbits+5), is_exact); + expr_ref is_exact(m), zero_sbits5(m); + zero_sbits5 = m_bv_util.mk_numeral(0, sbits + 5); + m_simp.mk_eq(R, zero_sbits5, is_exact); dbg_decouple("fpa2bv_sqrt_is_exact", is_exact); expr_ref rest(m), last(m), q_is_odd(m), rest_ext(m); @@ -1719,10 +1724,10 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, dbg_decouple("fpa2bv_sqrt_last", last); dbg_decouple("fpa2bv_sqrt_rest", rest); rest_ext = m_bv_util.mk_zero_extend(1, rest); - expr_ref sticky(m); - m_simp.mk_ite(is_exact, m_bv_util.mk_zero_extend(sbits+3, last), - m_bv_util.mk_numeral(1, sbits+4), - sticky); + expr_ref sticky(m), last_ext(m), one_sbits4(m); + last_ext = m_bv_util.mk_zero_extend(sbits + 3, last); + one_sbits4 = m_bv_util.mk_numeral(1, sbits + 4); + m_simp.mk_ite(is_exact, last_ext, one_sbits4, sticky); expr * or_args[2] = { rest_ext, sticky }; res_sig = m_bv_util.mk_bv_or(2, or_args); @@ -1813,8 +1818,11 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * mk_one(f, one_1, none); mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone); - m_simp.mk_eq(a_sig, m_bv_util.mk_numeral(fu().fm().m_powers2(sbits-1), sbits), t1); - m_simp.mk_eq(a_exp, m_bv_util.mk_numeral(-1, ebits), t2); + expr_ref pow_2_sbitsm1(m), m1(m); + pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits); + m1 = m_bv_util.mk_numeral(-1, ebits); + m_simp.mk_eq(a_sig, pow_2_sbitsm1, t1); + m_simp.mk_eq(a_exp, m1, t2); m_simp.mk_and(t1, t2, tie); dbg_decouple("fpa2bv_r2i_c42_tie", tie); @@ -1896,14 +1904,17 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr * SASSERT(is_well_sorted(m, tie2_c)); SASSERT(is_well_sorted(m, v51)); - expr_ref c521(m), v52(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c521); - m_simp.mk_and(c521, m.mk_eq(res_sgn, zero_1), c521); + expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m); + rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1)); + sgn_eq_zero = m.mk_eq(res_sgn, zero_1); + m_simp.mk_not(rem_eq_0, c521); + m_simp.mk_and(c521, sgn_eq_zero, c521); m_simp.mk_ite(c521, div_p1, div, v52); - expr_ref c531(m), v53(m); - m_simp.mk_not(m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits+1)), c531); - m_simp.mk_and(c531, m.mk_eq(res_sgn, one_1), c531); + expr_ref c531(m), v53(m), sgn_eq_one(m); + sgn_eq_one = m.mk_eq(res_sgn, one_1); + m_simp.mk_not(rem_eq_0, c531); + m_simp.mk_and(c531, sgn_eq_one, c531); m_simp.mk_ite(c531, div_p1, div, v53); expr_ref c51(m), c52(m), c53(m); @@ -3377,9 +3388,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref zero_s = m_bv_util.mk_numeral(0, sbits); m_simp.mk_eq(zero_s, denormal_sig, is_sig_zero); - expr_ref lz_d(m); + expr_ref lz_d(m), norm_or_zero(m); mk_leading_zeros(denormal_sig, ebits, lz_d); - m_simp.mk_ite(m.mk_or(is_normal, is_sig_zero), zero_e, lz_d, lz); + norm_or_zero = m.mk_or(is_normal, is_sig_zero); + m_simp.mk_ite(norm_or_zero, zero_e, lz_d, lz); dbg_decouple("fpa2bv_unpack_lz", lz); expr_ref shift(m); @@ -3770,8 +3782,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re dbg_decouple("fpa2bv_rnd_rm_is_to_pos", rm_is_to_pos); - expr_ref sgn_is_zero(m); - m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), sgn_is_zero); + expr_ref sgn_is_zero(m), zero1(m); + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(sgn, zero1, sgn_is_zero); dbg_decouple("fpa2bv_rnd_sgn_is_zero", sgn_is_zero); expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 65d99d2c8..8dc3dc019 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -26,19 +26,6 @@ Notes: #include"bv_decl_plugin.h" #include"basic_simplifier_plugin.h" -struct func_decl_triple { - func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; } - func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp) - { - f_sgn = sgn; - f_sig = sig; - f_exp = exp; - } - func_decl * f_sgn; - func_decl * f_sig; - func_decl * f_exp; - }; - class fpa2bv_converter { protected: ast_manager & m; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp new file mode 100644 index 000000000..188a73e95 --- /dev/null +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -0,0 +1,270 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + fpa2bv_rewriter.cpp + +Abstract: + + Rewriter for converting FPA to BV + +Author: + + Christoph (cwinter) 2012-02-09 + +Notes: + +--*/ + + +#include"rewriter_def.h" +#include"fpa2bv_rewriter.h" +#include"cooperate.h" +#include"fpa2bv_rewriter_params.hpp" + + +fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) : + m_manager(m), + m_out(m), + m_conv(c), + m_bindings(m) +{ + updt_params(p); + // We need to make sure that the mananger has the BV plugin loaded. + symbol s_bv("bv"); + if (!m_manager.has_plugin(s_bv)) + m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); +} + +void fpa2bv_rewriter_cfg::updt_local_params(params_ref const & _p) { + fpa2bv_rewriter_params p(_p); + bool v = p.hi_fp_unspecified(); + m_conv.set_unspecified_fp_hi(v); +} + +void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) { + m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); + m_max_steps = p.get_uint("max_steps", UINT_MAX); + updt_local_params(p); +} + +bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const { + cooperate("fpa2bv"); + return num_steps > m_max_steps; +} + + +br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; ); + + if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) { + m_conv.mk_const(f, result); + return BR_DONE; + } + + if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) { + m_conv.mk_rm_const(f, result); + return BR_DONE; + } + + if (m().is_eq(f)) { + SASSERT(num == 2); + TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << + mk_ismt2_pp(args[1], m()) << ")" << std::endl;); + SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); + sort * ds = f->get_domain()[0]; + if (m_conv.is_float(ds)) { + m_conv.mk_eq(args[0], args[1], result); + return BR_DONE; + } + else if (m_conv.is_rm(ds)) { + result = m().mk_eq(args[0], args[1]); + return BR_DONE; + } + return BR_FAILED; + } + else if (m().is_ite(f)) { + SASSERT(num == 3); + if (m_conv.is_float(args[1])) { + m_conv.mk_ite(args[0], args[1], args[2], result); + return BR_DONE; + } + return BR_FAILED; + } + else if (m().is_distinct(f)) { + sort * ds = f->get_domain()[0]; + if (m_conv.is_float(ds) || m_conv.is_rm(ds)) { + m_conv.mk_distinct(f, num, args, result); + return BR_DONE; + } + return BR_FAILED; + } + + if (m_conv.is_float_family(f)) { + switch (f->get_decl_kind()) { + case OP_FPA_RM_NEAREST_TIES_TO_AWAY: + case OP_FPA_RM_NEAREST_TIES_TO_EVEN: + case OP_FPA_RM_TOWARD_NEGATIVE: + case OP_FPA_RM_TOWARD_POSITIVE: + case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; + case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; + case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; + case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; + case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; + case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; + case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; + case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE; + case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE; + case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE; + case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; + case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; + case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; + case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; + case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; + case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; + case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; + case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; + case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; + case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; + case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; + case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; + case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; + case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; + case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; + case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; + case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; + case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + + case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; + case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; + + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; + + case OP_FPA_INTERNAL_RM: + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; + default: + TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); + NOT_IMPLEMENTED_YET(); + } + } + else { + SASSERT(!m_conv.is_float_family(f)); + bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); + + for (unsigned i = 0; i < f->get_arity(); i++) { + sort * di = f->get_domain()[i]; + is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); + } + + if (is_float_uf) { + m_conv.mk_uninterpreted_function(f, num, args, result); + return BR_DONE; + } + } + + return BR_FAILED; +} + +bool fpa2bv_rewriter_cfg::pre_visit(expr * t) +{ + TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); + + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); + TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); + sort_ref_vector new_bindings(m_manager); + for (unsigned i = 0 ; i < q->get_num_decls(); i++) + new_bindings.push_back(q->get_decl_sort(i)); + SASSERT(new_bindings.size() == q->get_num_decls()); + m_bindings.append(new_bindings); + } + return true; +} + + +bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + unsigned curr_sz = m_bindings.size(); + SASSERT(old_q->get_num_decls() <= curr_sz); + unsigned num_decls = old_q->get_num_decls(); + unsigned old_sz = curr_sz - num_decls; + string_buffer<> name_buffer; + ptr_buffer new_decl_sorts; + sbuffer new_decl_names; + for (unsigned i = 0; i < num_decls; i++) { + symbol const & n = old_q->get_decl_name(i); + sort * s = old_q->get_decl_sort(i); + if (m_conv.is_float(s)) { + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + name_buffer.reset(); + name_buffer << n << ".bv"; + new_decl_names.push_back(symbol(name_buffer.c_str())); + new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); + } + else { + new_decl_sorts.push_back(s); + new_decl_names.push_back(n); + } + } + result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), + new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), + old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + m_bindings.shrink(old_sz); + TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << + " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} + +bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { + if (t->get_idx() >= m_bindings.size()) + return false; + // unsigned inx = m_bindings.size() - t->get_idx() - 1; + + expr_ref new_exp(m()); + sort * s = t->get_sort(); + if (m_conv.is_float(s)) + { + expr_ref new_var(m()); + unsigned ebits = m_conv.fu().get_ebits(s); + unsigned sbits = m_conv.fu().get_sbits(s); + new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); + m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), + m_conv.bu().mk_extract(ebits - 1, 0, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + new_exp); + } + else + new_exp = m().mk_var(t->get_idx(), s); + + result = new_exp; + result_pr = 0; + TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); + return true; +} + +template class rewriter_tpl; diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index c3720421c..a130c445b 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -20,15 +20,13 @@ Notes: #ifndef FPA2BV_REWRITER_H_ #define FPA2BV_REWRITER_H_ -#include"cooperate.h" -#include"rewriter_def.h" +#include"rewriter.h" #include"bv_decl_plugin.h" #include"fpa2bv_converter.h" -#include"fpa2bv_rewriter_params.hpp" struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - expr_ref_vector m_out; + ast_manager & m_manager; + expr_ref_vector m_out; fpa2bv_converter & m_conv; sort_ref_vector m_bindings; @@ -37,19 +35,9 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { ast_manager & m() const { return m_manager; } - fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p) : - m_manager(m), - m_out(m), - m_conv(c), - m_bindings(m) { - updt_params(p); - // We need to make sure that the mananger has the BV plugin loaded. - symbol s_bv("bv"); - if (!m_manager.has_plugin(s_bv)) - m_manager.register_plugin(s_bv, alloc(bv_decl_plugin)); - } + fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, params_ref const & p); - ~fpa2bv_rewriter_cfg() { + ~fpa2bv_rewriter_cfg() { } void cleanup_buffers() { @@ -59,241 +47,32 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { void reset() { } - void updt_local_params(params_ref const & _p) { - fpa2bv_rewriter_params p(_p); - bool v = p.hi_fp_unspecified(); - m_conv.set_unspecified_fp_hi(v); - } + void updt_local_params(params_ref const & _p); - void updt_params(params_ref const & p) { - m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_max_steps = p.get_uint("max_steps", UINT_MAX); - updt_local_params(p); - } + void updt_params(params_ref const & p); - bool max_steps_exceeded(unsigned num_steps) const { - cooperate("fpa2bv"); - return num_steps > m_max_steps; - } + bool max_steps_exceeded(unsigned num_steps) const; - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; ); + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); - if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) { - m_conv.mk_const(f, result); - return BR_DONE; - } + bool pre_visit(expr * t); - if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) { - m_conv.mk_rm_const(f, result); - return BR_DONE; - } - - if (m().is_eq(f)) { - SASSERT(num == 2); - TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << - mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); - sort * ds = f->get_domain()[0]; - if (m_conv.is_float(ds)) { - m_conv.mk_eq(args[0], args[1], result); - return BR_DONE; - } - else if (m_conv.is_rm(ds)) { - result = m().mk_eq(args[0], args[1]); - return BR_DONE; - } - return BR_FAILED; - } - else if (m().is_ite(f)) { - SASSERT(num == 3); - if (m_conv.is_float(args[1])) { - m_conv.mk_ite(args[0], args[1], args[2], result); - return BR_DONE; - } - return BR_FAILED; - } - else if (m().is_distinct(f)) { - sort * ds = f->get_domain()[0]; - if (m_conv.is_float(ds) || m_conv.is_rm(ds)) { - m_conv.mk_distinct(f, num, args, result); - return BR_DONE; - } - return BR_FAILED; - } - - if (m_conv.is_float_family(f)) { - switch (f->get_decl_kind()) { - case OP_FPA_RM_NEAREST_TIES_TO_AWAY: - case OP_FPA_RM_NEAREST_TIES_TO_EVEN: - case OP_FPA_RM_TOWARD_NEGATIVE: - case OP_FPA_RM_TOWARD_POSITIVE: - case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; - case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; - case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; - case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; - case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; - case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; - case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; - case OP_FPA_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE; - case OP_FPA_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE; - case OP_FPA_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE; - case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; - case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; - case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; - case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; - case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; - case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; - case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; - case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; - case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; - case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; - case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; - case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; - case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; - case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; - case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; - case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; - case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; - case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; - case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; - case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; - case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - - case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; - case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; - - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; - case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; - case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; - - case OP_FPA_INTERNAL_RM: - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; - default: - TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); - NOT_IMPLEMENTED_YET(); - } - } - else { - SASSERT(!m_conv.is_float_family(f)); - bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); - - for (unsigned i = 0; i < f->get_arity(); i++) { - sort * di = f->get_domain()[i]; - is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); - } - - if (is_float_uf) { - m_conv.mk_uninterpreted_function(f, num, args, result); - return BR_DONE; - } - } - - return BR_FAILED; - } - - bool pre_visit(expr * t) - { - TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); - - if (is_quantifier(t)) { - quantifier * q = to_quantifier(t); - TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); - sort_ref_vector new_bindings(m_manager); - for (unsigned i = 0 ; i < q->get_num_decls(); i++) - new_bindings.push_back(q->get_decl_sort(i)); - SASSERT(new_bindings.size() == q->get_num_decls()); - m_bindings.append(new_bindings); - } - return true; - } - - bool reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, - proof_ref & result_pr) { - unsigned curr_sz = m_bindings.size(); - SASSERT(old_q->get_num_decls() <= curr_sz); - unsigned num_decls = old_q->get_num_decls(); - unsigned old_sz = curr_sz - num_decls; - string_buffer<> name_buffer; - ptr_buffer new_decl_sorts; - sbuffer new_decl_names; - for (unsigned i = 0; i < num_decls; i++) { - symbol const & n = old_q->get_decl_name(i); - sort * s = old_q->get_decl_sort(i); - if (m_conv.is_float(s)) { - unsigned ebits = m_conv.fu().get_ebits(s); - unsigned sbits = m_conv.fu().get_sbits(s); - name_buffer.reset(); - name_buffer << n << ".bv"; - new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); - } - else { - new_decl_sorts.push_back(s); - new_decl_names.push_back(n); - } - } - result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(), - new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), - old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); - result_pr = 0; - m_bindings.shrink(old_sz); - TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << - mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << - " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; - tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); - return true; - } + proof_ref & result_pr); - bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { - if (t->get_idx() >= m_bindings.size()) - return false; - // unsigned inx = m_bindings.size() - t->get_idx() - 1; + bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr); - expr_ref new_exp(m()); - sort * s = t->get_sort(); - if (m_conv.is_float(s)) - { - expr_ref new_var(m()); - unsigned ebits = m_conv.fu().get_ebits(s); - unsigned sbits = m_conv.fu().get_sbits(s); - new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); - m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), - m_conv.bu().mk_extract(ebits - 1, 0, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), - new_exp); - } - else - new_exp = m().mk_var(t->get_idx(), s); - - result = new_exp; - result_pr = 0; - TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); - return true; - } }; -template class rewriter_tpl; struct fpa2bv_rewriter : public rewriter_tpl { fpa2bv_rewriter_cfg m_cfg; fpa2bv_rewriter(ast_manager & m, fpa2bv_converter & c, params_ref const & p): - rewriter_tpl(m, m.proofs_enabled(), m_cfg), + rewriter_tpl(m, m.proofs_enabled(), m_cfg), m_cfg(m, c, p) { } }; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index e48a4fd2a..d45a4b092 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -61,8 +61,10 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_ADD: st = mk_add_core(num_args, args, result); break; case OP_MUL: st = mk_mul_core(num_args, args, result); break; case OP_SUB: st = mk_sub(num_args, args, result); break; - case OP_DIV: SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; - case OP_IDIV: SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; + case OP_DIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; } + SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; + case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; } + SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break; case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break; case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; @@ -292,7 +294,7 @@ expr * arith_rewriter::reduce_power(expr * arg, bool is_eq) { for (unsigned i = 0; i < sz; i++) { expr * arg = args[i]; expr * arg0, *arg1; - if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() && + if (m_util.is_power(arg, arg0, arg1) && m_util.is_numeral(arg1, k) && k.is_int() && ((is_eq && k > rational(1)) || (!is_eq && k > rational(2)))) { if (is_eq || !k.is_even()) { new_args.push_back(arg0); diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 0b8a51fb4..71be3d1c2 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -572,35 +572,61 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ */ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) { - SASSERT(m().is_ite(ite)); + expr* cond, *t, *e; + VERIFY(m().is_ite(ite, cond, t, e)); SASSERT(m().is_value(val)); - expr * t = ite->get_arg(1); - expr * e = ite->get_arg(2); - if (!m().is_value(t) || !m().is_value(e)) - return BR_FAILED; - - if (t != val && e != val) { - TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n"; - tout << t << " " << e << " " << val << "\n";); - result = m().mk_false(); + if (m().is_value(t) && m().is_value(e)) { + if (t != val && e != val) { + TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n"; + tout << t << " " << e << " " << val << "\n";); + result = m().mk_false(); + } + else if (t == val && e == val) { + result = m().mk_true(); + } + else if (t == val) { + result = cond; + } + else { + SASSERT(e == val); + mk_not(cond, result); + } return BR_DONE; } - - if (t == val && e == val) { - result = m().mk_true(); - return BR_DONE; + if (m().is_value(t)) { + if (val == t) { + result = m().mk_or(cond, m().mk_eq(val, e)); + } + else { + mk_not(cond, result); + result = m().mk_and(result, m().mk_eq(val, e)); + } + return BR_REWRITE2; + } + if (m().is_value(e)) { + if (val == e) { + mk_not(cond, result); + result = m().mk_or(result, m().mk_eq(val, t)); + } + else { + result = m().mk_and(cond, m().mk_eq(val, t)); + } + return BR_REWRITE2; + } + expr* cond2, *t2, *e2; + if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { + try_ite_value(to_app(t), val, result); + result = m().mk_ite(cond, result, m().mk_eq(e, val)); + return BR_REWRITE2; + } + if (m().is_ite(e, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { + try_ite_value(to_app(e), val, result); + result = m().mk_ite(cond, m().mk_eq(t, val), result); + return BR_REWRITE2; } - if (t == val) { - result = ite->get_arg(0); - return BR_DONE; - } - - SASSERT(e == val); - - mk_not(ite->get_arg(0), result); - return BR_DONE; + return BR_FAILED; } #if 0 @@ -645,7 +671,7 @@ static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) { #endif br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { - if (lhs == rhs) { + if (m().are_equal(lhs, rhs)) { result = m().mk_true(); return BR_DONE; } diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp index e9f66f10c..2b5e7e006 100644 --- a/src/ast/rewriter/rewriter.cpp +++ b/src/ast/rewriter/rewriter.cpp @@ -51,6 +51,8 @@ void rewriter_core::cache_result(expr * k, expr * v) { TRACE("rewriter_cache_result", tout << mk_ismt2_pp(k, m()) << "\n--->\n" << mk_ismt2_pp(v, m()) << "\n";); + SASSERT(m().get_sort(k) == m().get_sort(v)); + m_cache->insert(k, v); #if 0 static unsigned num_cached = 0; diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index 934d186aa..44f436fa8 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -214,10 +214,12 @@ protected: unsigned m_num_steps; ptr_vector m_bindings; var_shifter m_shifter; + inv_var_shifter m_inv_shifter; expr_ref m_r; proof_ref m_pr; proof_ref m_pr2; - + unsigned_vector m_shifts; + svector & frame_stack() { return this->m_frame_stack; } svector const & frame_stack() const { return this->m_frame_stack; } expr_ref_vector & result_stack() { return this->m_result_stack; } @@ -225,6 +227,8 @@ protected: proof_ref_vector & result_pr_stack() { return this->m_result_pr_stack; } proof_ref_vector const & result_pr_stack() const { return this->m_result_pr_stack; } + void display_bindings(std::ostream& out); + void set_new_child_flag(expr * old_t) { SASSERT(frame_stack().empty() || frame_stack().back().m_state != PROCESS_CHILDREN || this->is_child_of_top_frame(old_t)); if (!frame_stack().empty()) @@ -232,7 +236,6 @@ protected: } void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); } - // cache the result of shared non atomic expressions. bool cache_results() const { return m_cfg.cache_results(); } // cache all results share and non shared expressions non atomic expressions. diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 9bfe47f46..6fff9aff4 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -24,11 +24,13 @@ template void rewriter_tpl::process_var(var * v) { if (m_cfg.reduce_var(v, m_r, m_pr)) { result_stack().push_back(m_r); + SASSERT(v->get_sort() == m().get_sort(m_r)); if (ProofGen) { result_pr_stack().push_back(m_pr); m_pr = 0; } set_new_child_flag(v); + TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";); m_r = 0; return; } @@ -36,18 +38,22 @@ void rewriter_tpl::process_var(var * v) { // bindings are only used when Proof Generation is not enabled. unsigned idx = v->get_idx(); if (idx < m_bindings.size()) { - expr * r = m_bindings[m_bindings.size() - idx - 1]; - TRACE("process_var", if (r) tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n"; - tout << "bindings:\n"; - for (unsigned i = 0; i < m_bindings.size(); i++) if (m_bindings[i]) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";); + unsigned index = m_bindings.size() - idx - 1; + expr * r = m_bindings[index]; if (r != 0) { - if (m_num_qvars == 0 || is_ground(r)) { - result_stack().push_back(r); + SASSERT(v->get_sort() == m().get_sort(r)); + if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { + + unsigned shift_amount = m_bindings.size() - m_shifts[index]; + expr_ref tmp(m()); + m_shifter(r, shift_amount, tmp); + result_stack().push_back(tmp); + TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n"; + display_bindings(tout);); } else { - expr_ref new_term(m()); - m_shifter(r, m_num_qvars, new_term); - result_stack().push_back(new_term); + result_stack().push_back(r); + TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";); } set_new_child_flag(v); return; @@ -64,6 +70,7 @@ template void rewriter_tpl::process_const(app * t) { SASSERT(t->get_num_args() == 0); br_status st = m_cfg.reduce_app(t->get_decl(), 0, 0, m_r, m_pr); + SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); SASSERT(st == BR_FAILED || st == BR_DONE); if (st == BR_DONE) { result_stack().push_back(m_r.get()); @@ -100,6 +107,7 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { proof * new_t_pr; if (m_cfg.get_subst(t, new_t, new_t_pr)) { TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";); + SASSERT(m().get_sort(t) == m().get_sort(new_t)); result_stack().push_back(new_t); set_new_child_flag(t, new_t); if (ProofGen) @@ -124,6 +132,7 @@ bool rewriter_tpl::visit(expr * t, unsigned max_depth) { #endif expr * r = get_cached(t); if (r) { + SASSERT(m().get_sort(r) == m().get_sort(t)); result_stack().push_back(r); set_new_child_flag(t, r); if (ProofGen) { @@ -213,6 +222,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { } } br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2); + SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); TRACE("reduce_app", tout << mk_ismt2_pp(t, m()) << "\n"; tout << "st: " << st; @@ -220,6 +230,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { tout << "\n";); if (st != BR_FAILED) { result_stack().shrink(fr.m_spos); + SASSERT(m().get_sort(m_r) == m().get_sort(t)); result_stack().push_back(m_r); if (ProofGen) { result_pr_stack().shrink(fr.m_spos); @@ -295,6 +306,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (get_macro(f, def, def_q, def_pr)) { SASSERT(!f->is_associative() || !flat_assoc(f)); SASSERT(new_num_args == t->get_num_args()); + SASSERT(m().get_sort(def) == m().get_sort(t)); if (is_ground(def)) { m_r = def; if (ProofGen) { @@ -317,16 +329,18 @@ void rewriter_tpl::process_app(app * t, frame & fr) { TRACE("get_macro", tout << "f: " << f->get_name() << ", def: \n" << mk_ismt2_pp(def, m()) << "\n"; tout << "Args num: " << num_args << "\n"; for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(new_args[i], m()) << "\n";); + unsigned sz = m_bindings.size(); unsigned i = num_args; while (i > 0) { --i; - m_bindings.push_back(new_args[i]); + m_bindings.push_back(new_args[i]); // num_args - i - 1]); + m_shifts.push_back(sz); } result_stack().push_back(def); - TRACE("get_macro", tout << "bindings:\n"; - for (unsigned j = 0; j < m_bindings.size(); j++) tout << j << ": " << mk_ismt2_pp(m_bindings[j], m()) << "\n";); + TRACE("get_macro", display_bindings(tout);); begin_scope(); - m_num_qvars = 0; + m_num_qvars += num_args; + //m_num_qvars = 0; m_root = def; push_frame(def, false, RW_UNBOUNDED_DEPTH); return; @@ -383,9 +397,17 @@ void rewriter_tpl::process_app(app * t, frame & fr) { SASSERT(fr.m_spos + t->get_num_args() + 2 == result_stack().size()); SASSERT(t->get_num_args() <= m_bindings.size()); if (!ProofGen) { - m_bindings.shrink(m_bindings.size() - t->get_num_args()); + expr_ref tmp(m()); + unsigned num_args = t->get_num_args(); + m_bindings.shrink(m_bindings.size() - num_args); + m_shifts.shrink(m_shifts.size() - num_args); + m_num_qvars -= num_args; end_scope(); m_r = result_stack().back(); + if (!is_ground(m_r)) { + m_inv_shifter(m_r, num_args, tmp); + m_r = tmp; + } result_stack().shrink(fr.m_spos); result_stack().push_back(m_r); cache_result(t, m_r, m_pr, fr.m_cache_result); @@ -411,23 +433,26 @@ template template void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { SASSERT(fr.m_state == PROCESS_CHILDREN); + unsigned num_decls = q->get_num_decls(); if (fr.m_i == 0) { if (!ProofGen) { begin_scope(); m_root = q->get_expr(); - } - m_num_qvars += q->get_num_decls(); - if (!ProofGen) { - for (unsigned i = 0; i < q->get_num_decls(); i++) + unsigned sz = m_bindings.size(); + for (unsigned i = 0; i < num_decls; i++) { m_bindings.push_back(0); + m_shifts.push_back(sz); + } } + m_num_qvars += num_decls; } unsigned num_children = rewrite_patterns() ? q->get_num_children() : 1; while (fr.m_i < num_children) { expr * child = q->get_child(fr.m_i); fr.m_i++; - if (!visit(child, fr.m_max_depth)) + if (!visit(child, fr.m_max_depth)) { return; + } } SASSERT(fr.m_spos + num_children == result_stack().size()); expr * const * it = result_stack().c_ptr() + fr.m_spos; @@ -456,6 +481,8 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { result_pr_stack().push_back(m_pr); } else { + expr_ref tmp(m()); + if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, m_r, m_pr)) { if (fr.m_new_child) { m_r = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body); @@ -468,9 +495,11 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { } result_stack().shrink(fr.m_spos); result_stack().push_back(m_r.get()); + SASSERT(m().is_bool(m_r)); if (!ProofGen) { - SASSERT(q->get_num_decls() <= m_bindings.size()); - m_bindings.shrink(m_bindings.size() - q->get_num_decls()); + SASSERT(num_decls <= m_bindings.size()); + m_bindings.shrink(m_bindings.size() - num_decls); + m_shifts.shrink(m_shifts.size() - num_decls); end_scope(); cache_result(q, m_r, m_pr, fr.m_cache_result); } @@ -496,6 +525,7 @@ rewriter_tpl::rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg m_cfg(cfg), m_num_steps(0), m_shifter(m), + m_inv_shifter(m), m_r(m), m_pr(m), m_pr2(m) { @@ -510,7 +540,9 @@ void rewriter_tpl::reset() { m_cfg.reset(); rewriter_core::reset(); m_bindings.reset(); + m_shifts.reset(); m_shifter.reset(); + m_inv_shifter.reset(); } template @@ -519,6 +551,17 @@ void rewriter_tpl::cleanup() { rewriter_core::cleanup(); m_bindings.finalize(); m_shifter.cleanup(); + m_shifts.finalize(); + m_inv_shifter.cleanup(); +} + +template +void rewriter_tpl::display_bindings(std::ostream& out) { + out << "bindings:\n"; + for (unsigned i = 0; i < m_bindings.size(); i++) { + if (m_bindings[i]) + out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n"; + } } template @@ -526,11 +569,14 @@ void rewriter_tpl::set_bindings(unsigned num_bindings, expr * const * bi SASSERT(!m_proof_gen); SASSERT(not_rewriting()); m_bindings.reset(); + m_shifts.reset(); unsigned i = num_bindings; while (i > 0) { --i; m_bindings.push_back(bindings[i]); + m_shifts.push_back(num_bindings); } + TRACE("rewriter", display_bindings(tout);); } template @@ -538,9 +584,12 @@ void rewriter_tpl::set_inv_bindings(unsigned num_bindings, expr * const SASSERT(!m_proof_gen); SASSERT(not_rewriting()); m_bindings.reset(); + m_shifts.reset(); for (unsigned i = 0; i < num_bindings; i++) { m_bindings.push_back(bindings[i]); + m_shifts.push_back(num_bindings); } + TRACE("rewriter", display_bindings(tout);); } template @@ -562,9 +611,11 @@ void rewriter_tpl::main_loop(expr * t, expr_ref & result, proof_ref & re result_pr = m().mk_reflexivity(t); SASSERT(result_pr_stack().empty()); } - return; } - resume_core(result, result_pr); + else { + resume_core(result, result_pr); + } + TRACE("rewriter", tout << mk_ismt2_pp(t, m()) << "\n=>\n" << result << "\n";;); } /** @@ -587,6 +638,7 @@ void rewriter_tpl::resume_core(expr_ref & result, proof_ref & result_pr) if (first_visit(fr) && fr.m_cache_result) { expr * r = get_cached(t); if (r) { + SASSERT(m().get_sort(r) == m().get_sort(t)); result_stack().push_back(r); if (ProofGen) { proof * pr = get_cached_pr(t); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f04d445e1..75c8266be 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -579,7 +579,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { unsigned lenA = 0, lenB = 0; bool lA = min_length(as.size(), as.c_ptr(), lenA); if (lA) { - bool lB = min_length(bs.size(), bs.c_ptr(), lenB); + min_length(bs.size(), bs.c_ptr(), lenB); if (lenB > lenA) { result = m().mk_false(); return BR_DONE; 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/model/model_core.cpp b/src/model/model_core.cpp index 5c2fd81d4..3a3a8a93a 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -29,7 +29,6 @@ model_core::~model_core() { decl2finterp::iterator it2 = m_finterp.begin(); decl2finterp::iterator end2 = m_finterp.end(); for (; it2 != end2; ++it2) { - func_decl* d = it2->m_key; m_manager.dec_ref(it2->m_key); dealloc(it2->m_value); } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index d417adc1b..486111ae4 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -31,8 +31,9 @@ Revision History: #include"rewriter_def.h" #include"cooperate.h" + struct evaluator_cfg : public default_rewriter_cfg { - model_core & m_model; + model_core & m_model; bool_rewriter m_b_rw; arith_rewriter m_a_rw; bv_rewriter m_bv_rw; @@ -59,9 +60,10 @@ struct evaluator_cfg : public default_rewriter_cfg { m_pb_rw(m), m_f_rw(m), m_seq_rw(m) { - m_b_rw.set_flat(false); - m_a_rw.set_flat(false); - m_bv_rw.set_flat(false); + bool flat = true; + m_b_rw.set_flat(flat); + m_a_rw.set_flat(flat); + m_bv_rw.set_flat(flat); m_bv_rw.set_mkbv2num(true); updt_params(p); } @@ -181,10 +183,12 @@ struct evaluator_cfg : public default_rewriter_cfg { } bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { - TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); + +#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); func_interp * fi = m_model.get_func_interp(f); if (fi != 0) { + TRACE_MACRO; if (fi->is_partial()) { if (m_model_completion) { sort * s = f->get_range(); @@ -204,6 +208,7 @@ struct evaluator_cfg : public default_rewriter_cfg { (f->get_family_id() == null_family_id || m().get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) { + TRACE_MACRO; sort * s = f->get_range(); expr * val = m_model.get_some_value(s); func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); diff --git a/src/model/model_params.pyg b/src/model/model_params.pyg index 14e83952c..dfa3748bc 100644 --- a/src/model/model_params.pyg +++ b/src/model/model_params.pyg @@ -4,5 +4,6 @@ def_module_params('model', ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), + ('new_eval', BOOL, True, 'use new evaluator (temporary parameter for testing)'), )) diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 1445ed611..411588d79 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -152,40 +152,7 @@ namespace smt { // 5) theory_arith fails to internalize (+ (* -1 x) (* -1 x)), and Z3 crashes. // -#if 0 - // This block of code uses the simplifier for creating the literals t1 >= t2 and t1 <= t2. - // It has serious performance problems in VCC benchmarks. - // The problem seems to be the following: - // t1 and t2 are slacks (i.e., names for linear polynomials). - // The simplifier will create inequalities that will indirectly imply that t1 >= t2 and t1 <= t2. - // Example if: t1 := 1 + a - // t2 := 2 + b - // the simplifier will create - // a - b >= -1 - // a - b <= -1 - // These inequalities imply that 1+a >= 2+b and 1+a <= 2+b, - // but the tableau is complete different. - - - // BTW, note that we don't really need to handle the is_numeral case when using - // the simplifier. However, doing that, it seems we minimize the performance problem. - expr_ref le(m); - expr_ref ge(m); - if (m_util.is_numeral(t1)) - std::swap(t1, t2); - if (m_util.is_numeral(t2)) { - le = m_util.mk_le(t1, t2); - ge = m_util.mk_ge(t1, t2); - } - else { - arith_simplifier_plugin & s = *(get_simplifier()); - s.mk_le(t1, t2, le); - s.mk_ge(t1, t2, ge); - } - TRACE("arith_eq_adapter_perf", tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";); -#else - // Old version that used to be buggy. - // I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2 + // Requires that the theory arithmetic internalizer accept non simplified terms of the form t1 - t2 // if t1 and t2 already have slacks (theory variables) associated with them. // It also accepts terms with repeated variables (Issue #429). app * le = 0; @@ -207,7 +174,6 @@ namespace smt { } TRACE("arith_eq_adapter_perf", tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";); -#endif ctx.push_trail(already_processed_trail(m_already_processed, n1, n2)); m_already_processed.insert(n1, n2, data(t1_eq_t2, le, ge)); diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h index ac3035c78..7e9a645e6 100644 --- a/src/smt/arith_eq_adapter.h +++ b/src/smt/arith_eq_adapter.h @@ -65,7 +65,6 @@ namespace smt { theory & m_owner; theory_arith_params & m_params; arith_util & m_util; - arith_simplifier_plugin * m_as; already_processed m_already_processed; enode_pair_vector m_restart_pairs; @@ -76,7 +75,7 @@ namespace smt { enode * get_enode(theory_var v) const { return m_owner.get_enode(v); } public: - arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {} + arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u) {} void new_eq_eh(theory_var v1, theory_var v2); void new_diseq_eh(theory_var v1, theory_var v2); void reset_eh(); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 485fe1751..cb6b8c68d 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -30,12 +30,14 @@ Revision History: proto_model::proto_model(ast_manager & m, simplifier & s, params_ref const & p): model_core(m), m_simplifier(s), - m_afid(m.mk_family_id(symbol("array"))) { + m_afid(m.mk_family_id(symbol("array"))), + m_eval(*this) { register_factory(alloc(basic_factory, m)); m_user_sort_factory = alloc(user_sort_factory, m); register_factory(m_user_sort_factory); m_model_partial = model_params(p).partial(); + m_use_new_eval = model_params(p).new_eval(); } @@ -157,6 +159,19 @@ bool proto_model::is_select_of_model_value(expr* e) const { So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers. */ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { + if (m_use_new_eval) { + m_eval.set_model_completion(model_completion); + try { + m_eval(e, result); + return true; + } + catch (model_evaluator_exception & ex) { + (void)ex; + TRACE("model_evaluator", tout << ex.msg() << "\n";); + return false; + } + } + bool is_ok = true; SASSERT(is_well_sorted(m_manager, e)); TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; diff --git a/src/smt/proto_model/proto_model.h b/src/smt/proto_model/proto_model.h index 1b63f8b20..2c27ac39a 100644 --- a/src/smt/proto_model/proto_model.h +++ b/src/smt/proto_model/proto_model.h @@ -29,6 +29,7 @@ Revision History: #define PROTO_MODEL_H_ #include"model_core.h" +#include"model_evaluator.h" #include"value_factory.h" #include"plugin_manager.h" #include"simplifier.h" @@ -44,8 +45,10 @@ class proto_model : public model_core { family_id m_afid; //!< array family id: hack for displaying models in V1.x style func_decl_set m_aux_decls; ptr_vector m_tmp; + model_evaluator m_eval; bool m_model_partial; + bool m_use_new_eval; expr * mk_some_interp_for(func_decl * d); diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index e4bfcc806..0d9c361f8 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -95,7 +95,8 @@ namespace smt { expr * e = *it; eqs.push_back(m.mk_eq(sk, e)); } - m_aux_context->assert_expr(m.mk_or(eqs.size(), eqs.c_ptr())); + expr_ref fml(m.mk_or(eqs.size(), eqs.c_ptr()), m); + m_aux_context->assert_expr(fml); } #define PP_DEPTH 8 @@ -105,9 +106,13 @@ namespace smt { The variables are replaced by skolem constants. These constants are stored in sks. */ + void model_checker::assert_neg_q_m(quantifier * q, expr_ref_vector & sks) { expr_ref tmp(m); - m_curr_model->eval(q->get_expr(), tmp, true); + if (!m_curr_model->eval(q->get_expr(), tmp, true)) { + return; + } + //std::cout << tmp << "\n"; TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";); ptr_buffer subst_args; unsigned num_decls = q->get_num_decls(); @@ -261,10 +266,11 @@ namespace smt { lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); - if (r == l_false) { + if (r != l_true) { m_aux_context->pop(1); - return true; // quantifier is satisfied by m_curr_model + return r == l_false; // quantifier is satisfied by m_curr_model } + model_ref complete_cex; m_aux_context->get_model(complete_cex); @@ -276,7 +282,7 @@ namespace smt { while (true) { lbool r = m_aux_context->check(); TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); - if (r == l_false) + if (r != l_true) break; model_ref cex; m_aux_context->get_model(cex); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 301b5d14d..291a0f0d8 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1619,6 +1619,7 @@ namespace smt { m_found_underspecified_op(false), m_arith_eq_adapter(*this, params, m_util), m_asserted_qhead(0), + m_row_vars_top(0), m_to_patch(1024), m_blands_rule(false), m_random(params.m_arith_random_seed), @@ -1631,7 +1632,6 @@ namespace smt { m_liberal_final_check(true), m_changed_assignment(false), m_assume_eq_head(0), - m_row_vars_top(0), m_nl_rounds(0), m_nl_gb_exhausted(false), m_nl_new_exprs(m), diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 551e80c85..5bd00db5d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1591,7 +1591,6 @@ bool theory_seq::solve_ne(unsigned idx) { } bool theory_seq::solve_nc(unsigned idx) { - context& ctx = get_context(); nc const& n = m_ncs[idx]; dependency* deps = n.deps(); diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index f4f7fac16..54c654d54 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -24,6 +24,7 @@ Notes: #include"params.h" #include"ast_pp.h" #include"bvarray2uf_rewriter.h" +#include"rewriter_def.h" // [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving // Quantified Bit-Vector Formulas, in Formal Methods in System Design, @@ -345,3 +346,5 @@ bool bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & NOT_IMPLEMENTED_YET(); return true; } + +template class rewriter_tpl; diff --git a/src/tactic/bv/bvarray2uf_rewriter.h b/src/tactic/bv/bvarray2uf_rewriter.h index e65340cc3..81b53ddd7 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.h +++ b/src/tactic/bv/bvarray2uf_rewriter.h @@ -20,7 +20,7 @@ Notes: #ifndef BVARRAY2UF_REWRITER_H_ #define BVARRAY2UF_REWRITER_H_ -#include"rewriter_def.h" +#include"rewriter.h" #include"extension_model_converter.h" #include"filter_model_converter.h" @@ -71,7 +71,6 @@ protected: func_decl_ref mk_uf_for_array(expr * e); }; -template class rewriter_tpl; struct bvarray2uf_rewriter : public rewriter_tpl { bvarray2uf_rewriter_cfg m_cfg; diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index cfedb66d7..28597c6ec 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -91,11 +91,10 @@ class fpa2bv_tactic : public tactic { // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation // has a value to propagate. expr * sgn, *sig, *exp; - expr_ref top_exp(m); m_conv.split_fp(new_curr, sgn, exp, sig); - m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)); - m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))); - m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))); + result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1))); + result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)))); + result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)))); } } } @@ -155,7 +154,7 @@ public: virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } diff --git a/src/test/main.cpp b/src/test/main.cpp index be12286fb..875f7bed0 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -226,6 +226,7 @@ int main(int argc, char ** argv) { TST(sat_user_scope); TST(pdr); TST_ARGV(ddnf); + TST(model_evaluator); //TST_ARGV(hs); } diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp new file mode 100644 index 000000000..6e3a1f441 --- /dev/null +++ b/src/test/model_evaluator.cpp @@ -0,0 +1,66 @@ +#include "model.h" +#include "model_evaluator.h" +#include "model_pp.h" +#include "arith_decl_plugin.h" +#include "reg_decl_plugins.h" +#include "ast_pp.h" + + +void tst_model_evaluator() { + ast_manager m; + reg_decl_plugins(m); + arith_util a(m); + + model mdl(m); + + sort* sI = a.mk_int(); + + sort* dom[2] = { sI, m.mk_bool_sort() }; + func_decl_ref f(m.mk_func_decl(symbol("f"), 2, dom, sI), m); + func_decl_ref g(m.mk_func_decl(symbol("g"), 2, dom, sI), m); + func_decl_ref h(m.mk_func_decl(symbol("h"), 2, dom, sI), m); + func_decl_ref F(m.mk_func_decl(symbol("F"), 2, dom, sI), m); + func_decl_ref G(m.mk_func_decl(symbol("G"), 2, dom, sI), m); + expr_ref vI0(m.mk_var(0, sI), m); + expr_ref vI1(m.mk_var(1, sI), m); + expr_ref vB0(m.mk_var(0, m.mk_bool_sort()), m); + expr_ref vB1(m.mk_var(1, m.mk_bool_sort()), m); + expr_ref vB2(m.mk_var(2, m.mk_bool_sort()), m); + expr_ref f01(m.mk_app(f, vI0, vB1), m); + expr_ref g01(m.mk_app(g, vI0, vB1), m); + expr_ref h01(m.mk_app(h, vI0, vB1), m); + func_interp* fi = alloc(func_interp, m, 2); + func_interp* gi = alloc(func_interp, m, 2); + func_interp* hi = alloc(func_interp, m, 2); + hi->set_else(m.mk_ite(vB1, m.mk_app(f, vI0, vB1), m.mk_app(g, vI0, vB1))); + mdl.register_decl(h, hi); + + + model_evaluator eval(mdl); + + expr_ref e(m), v(m); + + { + symbol nI("N"); + fi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(F, vI1, vB2))), vI0, a.mk_int(1))); + gi->set_else(m.mk_ite(m.mk_exists(1, &sI, &nI, a.mk_le(vI0, m.mk_app(G, vI1, vB2))), a.mk_int(2), vI0)); + mdl.register_decl(g, gi); + mdl.register_decl(f, fi); + model_pp(std::cout, mdl); + e = m.mk_app(h, vI0, vB1); + eval(e, v); + std::cout << e << " " << v << "\n"; + } + + { + fi->set_else(m.mk_app(F, vI0, vB1)); + gi->set_else(m.mk_app(G, vI0, vB1)); + mdl.register_decl(g, gi); + mdl.register_decl(h, hi); + model_pp(std::cout, mdl); + e = m.mk_app(h, vI0, vB1); + eval(e, v); + std::cout << e << " " << v << "\n"; + } + +} diff --git a/src/util/version.h.in b/src/util/version.h.in new file mode 100644 index 000000000..05b619f2d --- /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@