diff --git a/CMakeLists.txt b/CMakeLists.txt index cf46e7012..19c56a413 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,9 +24,8 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) "``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) +set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") +project(Z3 CXX) ################################################################################ # Project version @@ -43,10 +42,13 @@ 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 + # In CMake >= 3.2 add_custom_command() and add_custom_target() + # supports a ``USES_TERMINAL`` argument set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL") + set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "USES_TERMINAL") else() set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "") + set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "") endif() ################################################################################ @@ -152,13 +154,13 @@ set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "") # Build type ################################################################################ message(STATUS "CMake generator: ${CMAKE_GENERATOR}") +set(available_build_types Debug Release RelWithDebInfo MinSizeRel) 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}") @@ -323,6 +325,15 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST unset(SSE_FLAGS) endif() +# FIXME: Remove "x.." when CMP0054 is set to NEW +if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + # This is the default for MSVC already but to replicate the + # python/Makefile build system behaviour this flag is set + # explicitly. + z3_add_cxx_flag("/fp:precise" REQUIRED) +endif() +# There doesn't seem to be an equivalent for clang/gcc + ################################################################################ # Threading support ################################################################################ @@ -373,6 +384,41 @@ if (BUILD_LIBZ3_SHARED) endif() endif() +################################################################################ +# Link time optimization +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake) + +################################################################################ +# MSVC specific flags inherited from old build system +################################################################################ +# FIXME: Remove "x.." when CMP0054 is set to NEW +if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake) +endif() + +################################################################################ +# Report default CMake flags +################################################################################ +# This is mainly for debugging. +message(STATUS "CMAKE_CXX_FLAGS: \"${CMAKE_CXX_FLAGS}\"") +message(STATUS "CMAKE_EXE_LINKER_FLAGS: \"${CMAKE_EXE_LINKER_FLAGS}\"") +message(STATUS "CMAKE_STATIC_LINKER_FLAGS: \"${CMAKE_STATIC_LINKER_FLAGS}\"") +message(STATUS "CMAKE_SHARED_LINKER_FLAGS: \"${CMAKE_SHARED_LINKER_FLAGS}\"") +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi configuration generator + string(TOUPPER "${available_build_types}" build_types_to_report) +else() + # Single configuration generator + string(TOUPPER "${CMAKE_BUILD_TYPE}" build_types_to_report) +endif() +foreach (_build_type ${build_types_to_report}) + message(STATUS "CMAKE_CXX_FLAGS_${_build_type}: \"${CMAKE_CXX_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_EXE_LINKER_FLAGS_${_build_type}: \"${CMAKE_EXE_LINKER_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_SHARED_LINKER_FLAGS_${_build_type}: \"${CMAKE_SHARED_LINKER_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_STATIC_LINKER_FLAGS_${_build_type}: \"${CMAKE_STATIC_LINKER_FLAGS_${_build_type}}\"") +endforeach() + ################################################################################ # Report Z3_COMPONENT flags ################################################################################ @@ -528,3 +574,14 @@ option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON) if (ENABLE_EXAMPLE_TARGETS) add_subdirectory(examples) endif() + +################################################################################ +# Documentation +################################################################################ +option(BUILD_DOCUMENTATION "Build API documentation" OFF) +if (BUILD_DOCUMENTATION) + message(STATUS "Building documentation enabled") + add_subdirectory(doc) +else() + message(STATUS "Building documentation disabled") +endif() diff --git a/README-CMake.md b/README-CMake.md index 6a78b5d4c..9289d40f1 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -268,6 +268,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files. * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. * ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``). +* ``CMAKE_INSTALL_API_BINDINGS_DOC`` - STRING. The path to install documentation for API bindings. * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``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. @@ -286,6 +287,12 @@ The following useful options can be passed to CMake whilst configuring. * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``. * ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build. * ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build. +* ``BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target. +* ``INSTALL_API_BINDINGS_DOCUMENTATION`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION` is ``TRUE`` then documentation for API bindings will be installed + when running the ``install`` target. +* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built. + Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target. +* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. 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. @@ -417,6 +424,7 @@ 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. +* ``api_docs`` will build the documentation for the API bindings. ### Setting build type specific flags diff --git a/contrib/cmake/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake deleted file mode 100644 index c6005396b..000000000 --- a/contrib/cmake/cmake/compiler_flags_override.cmake +++ /dev/null @@ -1,43 +0,0 @@ -# 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 have very fine grained control of the compiler flags. -if (CMAKE_C_COMPILER_ID) - set(_lang C) -elseif(CMAKE_CXX_COMPILER_ID) - set(_lang CXX) -else() - message(FATAL_ERROR "Unknown language") -endif() - -# TODO: The value of doing this is debatable. The flags set here are pretty -# much the CMake defaults now (they didn't use to be) and makes extra work for -# us when supporting different compilers. Perhaps we should move the remaining -# code that sets non-default flags out into the CMakeLists.txt files and remove -# any overrides here? -if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU")) - # Taken from Modules/Compiler/GNU.cmake - set(CMAKE_${_lang}_FLAGS_INIT "") - set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3 -DNDEBUG") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG") - # FIXME: Remove "x.." when CMP0054 is set to NEW -elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") - # FIXME: Perhaps we should be using /MD instead? - set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1 /D NDEBUG") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2 /D NDEBUG") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1 /D NDEBUG") - # 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_lto.cmake b/contrib/cmake/cmake/compiler_lto.cmake new file mode 100644 index 000000000..b90890f59 --- /dev/null +++ b/contrib/cmake/cmake/compiler_lto.cmake @@ -0,0 +1,52 @@ +option(LINK_TIME_OPTIMIZATION "Use link time optimiziation" OFF) + +if (LINK_TIME_OPTIMIZATION) + message(STATUS "LTO enabled") + set(build_types_with_lto "RELEASE" "RELWITHDEBINFO") + if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi configuration generator + message(STATUS "Note LTO is only enabled for the following configurations: ${build_types_with_lto}") + else() + # Single configuration generator + string(TOUPPER "${CMAKE_BUILD_TYPE}" _build_type_upper) + list(FIND build_types_with_lto "${_build_type_upper}" _index) + if ("${_index}" EQUAL -1) + message(FATAL_ERROR "Configuration ${CMAKE_BUILD_TYPE} does not support LTO." + "You should set LINK_TIME_OPTIMIZATION to OFF.") + endif() + endif() + + set(_lto_compiler_flag "") + set(_lto_linker_flag "") + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR + ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + set(_lto_compiler_flag "-flto") + set(_lto_linker_flag "-flto") + # FIXME: Remove "x.." when CMP0054 is set to NEW + elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + set(_lto_compiler_flag "/GL") + set(_lto_linker_flag "/LTCG") + else() + message(FATAL_ERROR "Can't enable LTO for compiler \"${CMAKE_CXX_COMPILER_ID}\"." + "You should set LINK_TIME_OPTIMIZATION to OFF.") + endif() + CHECK_CXX_COMPILER_FLAG("${_lto_compiler_flag}" HAS_LTO) + if (NOT HAS_LTO) + message(FATAL_ERROR "Compiler does not support LTO") + endif() + + foreach (_config ${build_types_with_lto}) + # Set flags compiler and linker flags globally rather than using + # `Z3_COMPONENT_CXX_FLAGS` and `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS` + # respectively. We need per configuration compiler and linker flags. The + # `LINK_FLAGS` property (which we populate with + # `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`) doesn't seem to support generator + # expressions so we can't do `$<$:${_lto_linker_flag}>`. + set(CMAKE_CXX_FLAGS_${_config} "${CMAKE_CXX_FLAGS_${_config}} ${_lto_compiler_flag}") + set(CMAKE_EXE_LINKER_FLAGS_${_config} "${CMAKE_EXE_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + set(CMAKE_SHARED_LINKER_FLAGS_${_config} "${CMAKE_SHARED_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + set(CMAKE_STATIC_LINKER_FLAGS_${_config} "${CMAKE_STATIC_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + endforeach() +else() + message(STATUS "LTO disabled") +endif() diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake index c214e4464..e02b28b2c 100644 --- a/contrib/cmake/cmake/compiler_warnings.cmake +++ b/contrib/cmake/cmake/compiler_warnings.cmake @@ -15,6 +15,13 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") # 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}) + + # CMake's default flags include /W3 already so remove them if + # they already exist. + if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3") + string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}") + set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE) + endif() else() message(AUTHOR_WARNING "Unknown compiler") endif() @@ -37,4 +44,11 @@ if (WARNINGS_AS_ERRORS) message(STATUS "Treating compiler warnings as errors") else() message(STATUS "Not treating compiler warnings as errors") + # FIXME: Remove "x.." when CMP0054 is set to NEW + if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + # Warnings as errors is off by default for MSVC so setting this + # is not necessary but this duplicates the behaviour of the old + # build system. + list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-") + endif() endif() diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake new file mode 100644 index 000000000..59966f424 --- /dev/null +++ b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake @@ -0,0 +1,14 @@ +# 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 have very fine grained control of the compiler flags. + +# We only override the defaults for Clang and GCC right now. +# CMake's MSVC logic is complicated so for now it's better to just inherit CMake's defaults. +if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + # Taken from Modules/Compiler/GNU.cmake + set(CMAKE_CXX_FLAGS_INIT "") + set(CMAKE_CXX_FLAGS_DEBUG_INIT "-g -O0") + set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG") + set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3 -DNDEBUG") + set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG") +endif() diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake new file mode 100644 index 000000000..2ca20277c --- /dev/null +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -0,0 +1,194 @@ +# This file ether sets or notes various compiler and linker flags for MSVC that +# were defined by the old python/Makefile based build system but +# don't obviously belong in the other sections in the CMake build system. + +################################################################################ +# Compiler definitions +################################################################################ +# FIXME: All the commented out defines should be removed once +# we are confident it is correct to not set them. +set(Z3_MSVC_LEGACY_DEFINES + # Don't set `_DEBUG`. The old build sytem sets this but this + # is wrong. MSVC will set this depending on which runtime is being used. + # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx + # _DEBUG + + # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release. + # That seems completly wrong so set it for all configurations. + # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/ + # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files. + # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx + UNICODE + _UNICODE +) + +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_MSVC_LEGACY_DEFINES "" + # Don't set `_LIB`. The old build system sets this for x86_64 release + # build. This flag doesn't seem to be documented but a stackoverflow + # post hints that this is usually set when building a static library. + # See http://stackoverflow.com/questions/35034683/how-to-tell-if-current-project-is-dll-or-static-lib + # This seems wrong give that the old build system set this regardless + # whether or not libz3 was static or shared so its probably best + # to not set for now. + #$<$:_LIB> + #$<$:_LIB> + + # Don't set `_CONSOLE`. The old build system sets for all configurations + # except x86_64 release. It seems ( https://codeyarns.com/2010/12/02/visual-c-windows-and-console-subsystems/ ) + # that `_CONSOLE` used to be defined by older Visual C++ environments. + # Setting this undocumented option seems like a bad idea so let's not do it. + #$<$ + #$<$ + + # Don't set `ASYNC_COMMANDS`. The old build system sets this for x86_64 + # release but this macro does not appear to be used anywhere and is not + # documented so don't set it for now. + #$<$:ASYNC_COMMANDS> + #$<$:ASYNC_COMMANDS> + ) +else() + list(APPEND Z3_MSVC_LEGACY_DEFINES "" + # Don't set `_CONSOLE`. See reasoning above. + #_CONSOLE + ) +endif() + +# Note we don't set WIN32 or _WINDOWS because +# CMake provides that for us. As a sanity check make sure the option +# is present. +if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*WIN32") + message(FATAL_ERROR "\"/D WIN32\" is missing") +endif() +if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*_WINDOWS") + message(FATAL_ERROR "\"/D _WINDOWS\" is missing") +endif() + +list(APPEND Z3_COMPONENT_CXX_DEFINES ${Z3_MSVC_LEGACY_DEFINES}) + +################################################################################ +# Compiler flags +################################################################################ +# By default in MSVC this is on but the old build system set this explicitly so +# for completeness set it too. +# See https://msdn.microsoft.com/en-us/library/dh8che7s.aspx +z3_add_cxx_flag("/Zc:wchar_t" REQUIRED) +# By default in MSVC this on but the old build system set this explicitly so +# for completeness set it too. +z3_add_cxx_flag("/Zc:forScope" REQUIRED) + +# FIXME: We might want to move this out somewhere else if we decide +# we want to set `-fno-omit-frame-pointer` for gcc/clang. +# No omit frame pointer +set(NO_OMIT_FRAME_POINTER_MSVC_FLAG "/Oy-") +CHECK_CXX_COMPILER_FLAG(${NO_OMIT_FRAME_POINTER_MSVC_FLAG} HAS_MSVC_NO_OMIT_FRAME_POINTER) +if (NOT HAS_MSVC_NO_OMIT_FRAME_POINTER) + message(FATAL_ERROR "${NO_OMIT_FRAME_POINTER_MSVC_FLAG} flag not supported") +endif() + +# FIXME: This doesn't make a huge amount of sense but the old +# build system kept the frame pointer for all configurations +# except x86_64 release (I don't know why the frame pointer +# is kept for i686 release). +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_COMPONENT_CXX_FLAGS + $<$:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> + $<$:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> + ) +else() + list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG}) +endif() + +if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) + # Use __cdecl calling convention. Apparently this is MSVC's default + # but the old build system set it so for completeness set it too. + # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx + z3_add_cxx_flag("/Gd" REQUIRED) +endif() + +# FIXME: The old build system explicitly disables code analysis. +# I don't know why. Duplicate this behaviour for now. +# See https://msdn.microsoft.com/en-us/library/ms173498.aspx +z3_add_cxx_flag("/analyze-" REQUIRED) + +################################################################################ +# Linker flags +################################################################################ + +# By default CMake enables incremental linking for Debug and RelWithDebInfo +# builds. The old build sytem disables it for all builds so try to do the same +# by changing all configurations if necessary +string(TOUPPER "${available_build_types}" _build_types_as_upper) +foreach (_build_type ${_build_types_as_upper}) + foreach (t EXE SHARED STATIC) + set(_replacement "/INCREMENTAL:NO") + # Remove any existing incremental flags + string(REGEX REPLACE + "/INCREMENTAL:YES" + "${_replacement}" + _replaced_linker_flags + "${CMAKE_${t}_LINKER_FLAGS_${_build_type}}") + string(REGEX REPLACE + "(/INCREMENTAL$)|(/INCREMENTAL )" + "${_replacement} " + _replaced_linker_flags + "${_replaced_linker_flags}") + if (NOT "${_replaced_linker_flags}" MATCHES "${_replacement}") + # Flag not present. Add it + string(APPEND _replaced_linker_flags " ${_replacement}") + endif() + set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}") + endforeach() +endforeach() + +# The original build system passes `/STACK:` to the linker. +# This size comes from the original build system. +# FIXME: What is the rationale behind this? +set(STACK_SIZE_MSVC_LINKER 8388608) +# MSVC documentation (https://msdn.microsoft.com/en-us/library/35yc2tc3.aspx) +# says this only matters for executables which is why this is not being +# set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS. +string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}") + +# The original build system passes `/SUBSYSTEM:` to the linker where `` +# depends on what is being linked. Where `` is `CONSOLE` for executables +# and `WINDOWS` for shard libraries. +# We don't need to pass `/SUBSYSTEM:CONSOLE` because CMake will do this for +# us when building executables because we don't pass the `WIN32` argument to +# `add_executable()`. +# FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx +# suggests that `/SUBSYSTEM:` only matters for executables. +string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS") + +# FIXME: The following linker flags are weird. They are set in all configurations +# in the old build system except release x86_64. We try to emulate this here but +# this is likely the wrong thing to do. +foreach (_build_type ${_build_types_as_upper}) + if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND + ("${_build_type}" STREQUAL "RELEASE" OR + "${_build_type}" STREQUAL "RELWITHDEBINFO") + ) + message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}") + else() + # Linker optimizations. + # See https://msdn.microsoft.com/en-us/library/bxwfs976.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF") + + # FIXME: This is not necessary. This is MSVC's default. + # See https://msdn.microsoft.com/en-us/library/b1kw34cb.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /TLBID:1") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /TLBID:1") + + # FIXME: This is not necessary. This is MSVC's default. + # Address space layout randomization + # See https://msdn.microsoft.com/en-us/library/bb384887.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /DYNAMICBASE") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO") + + # FIXME: This is not necessary. This is MSVC's default. + # Indicate that the executable is compatible with DEP + # See https://msdn.microsoft.com/en-us/library/ms235442.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT") + endif() +endforeach() diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/contrib/cmake/cmake/z3_add_cxx_flag.cmake index 0c56bb0f6..8bffd7de3 100644 --- a/contrib/cmake/cmake/z3_add_cxx_flag.cmake +++ b/contrib/cmake/cmake/z3_add_cxx_flag.cmake @@ -7,6 +7,7 @@ function(z3_add_cxx_flag 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}") + 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}) diff --git a/contrib/cmake/doc/CMakeLists.txt b/contrib/cmake/doc/CMakeLists.txt new file mode 100644 index 000000000..86e208ab1 --- /dev/null +++ b/contrib/cmake/doc/CMakeLists.txt @@ -0,0 +1,93 @@ +find_package(Doxygen REQUIRED) +message(STATUS "DOXYGEN_EXECUTABLE: \"${DOXYGEN_EXECUTABLE}\"") +message(STATUS "DOXYGEN_VERSION: \"${DOXYGEN_VERSION}\"") + +set(DOC_DEST_DIR "${CMAKE_CURRENT_BINARY_DIR}/api") +set(DOC_TEMP_DIR "${CMAKE_CURRENT_BINARY_DIR}/temp") +set(MK_API_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_api_doc.py") + +set(PYTHON_API_OPTIONS "") +set(DOTNET_API_OPTIONS "") +set(JAVA_API_OPTIONS "") +SET(DOC_EXTRA_DEPENDS "") + +if (BUILD_PYTHON_BINDINGS) + # FIXME: Don't hard code this path + list(APPEND PYTHON_API_OPTIONS "--z3py-package-path" "${CMAKE_BINARY_DIR}/python/z3") + list(APPEND DOC_EXTRA_DEPENDS "build_z3_python_bindings") +else() + list(APPEND PYTHON_API_OPTIONS "--no-z3py") +endif() + +if (BUILD_DOTNET_BINDINGS) + # FIXME: Don't hard code these paths + list(APPEND DOTNET_API_OPTIONS "--dotnet-search-paths" + "${CMAKE_SOURCE_DIR}/src/api/dotnet" + "${CMAKE_BINARY_DIR}/src/api/dotnet" + ) + list(APPEND DOC_EXTRA_DEPENDS "build_z3_dotnet_bindings") +else() + list(APPEND DOTNET_API_OPTIONS "--no-dotnet") +endif() + +if (BUILD_JAVA_BINDINGS) + # FIXME: Don't hard code these paths + list(APPEND JAVA_API_OPTIONS "--java-search-paths" + "${CMAKE_SOURCE_DIR}/src/api/java" + "${CMAKE_BINARY_DIR}/src/api/java" + ) + list(APPEND DOC_EXTRA_DEPENDS "build_z3_java_bindings") +else() + list(APPEND JAVA_API_OPTIONS "--no-java") +endif() + +option(ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON) +if (ALWAYS_BUILD_DOCS) + set(ALWAYS_BUILD_DOCS_ARG "ALL") +else() + set(ALWAYS_BUILD_DOCS_ARG "") + # FIXME: This sucks but there doesn't seem to be a way to make the top level + # install target depend on the `api_docs` target. + message(WARNING "Building documentation for API bindings is not part of the" + " all target. This may result in stale files being installed when running" + " the install target. You should run the api_docs target before running" + " the install target. Alternatively Set ALWAYS_BUILD_DOCS to ON to" + " automatically build documentation when running the install target." + ) +endif() + +add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG} + COMMAND + "${PYTHON_EXECUTABLE}" "${MK_API_DOC_SCRIPT}" + --doxygen-executable "${DOXYGEN_EXECUTABLE}" + --output-dir "${DOC_DEST_DIR}" + --temp-dir "${DOC_TEMP_DIR}" + ${PYTHON_API_OPTIONS} + ${DOTNET_API_OPTIONS} + ${JAVA_API_OPTIONS} + DEPENDS + ${DOC_EXTRA_DEPENDS} + BYPRODUCTS "${DOC_DEST_DIR}" + COMMENT "Generating documentation" + ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG} +) + +# Remove generated documentation when running `clean` target. +set_property(DIRECTORY APPEND PROPERTY + ADDITIONAL_MAKE_CLEAN_FILES + "${DOC_DEST_DIR}" +) + +option(INSTALL_API_BINDINGS_DOCUMENTATION "Install documentation for API bindings" ON) +set(CMAKE_INSTALL_API_BINDINGS_DOC + "${CMAKE_INSTALL_DOCDIR}" + CACHE + PATH + "Path to install documentation for API bindings" +) +if (INSTALL_API_BINDINGS_DOCUMENTATION) + install( + DIRECTORY "${DOC_DEST_DIR}" + DESTINATION "${CMAKE_INSTALL_API_BINDINGS_DOC}" + ) +endif() diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index edabcbd1b..014a152b4 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -1,5 +1,9 @@ # Copyright (c) Microsoft Corporation 2015 +""" +Z3 API documentation generator script +""" +import argparse import os import shutil import re @@ -11,124 +15,291 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' - -def display_help(exit_code): - print("mk_api_doc.py: Z3 documentation generator\n") - print("\nOptions:") - print(" -h, --help display this message.") - print(" -b , --build= subdirectory where Z3 is built (default: ../build).") - print(" --ml include ML/OCaml API documentation.") +DOXYGEN_EXE='doxygen' +TEMP_DIR=os.path.join(os.getcwd(), 'tmp') +OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') +Z3PY_PACKAGE_PATH='../src/api/python/z3' +Z3PY_ENABLED=True +DOTNET_ENABLED=True +JAVA_ENABLED=True +DOTNET_API_SEARCH_PATHS=['../src/api/dotnet'] +JAVA_API_SEARCH_PATHS=['../src/api/java'] +SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__)) def parse_options(): - global ML_ENABLED, BUILD_DIR - - try: - options, remainder = getopt.gnu_getopt(sys.argv[1:], - 'b:h', - ['build=', 'help', 'ml']) - except: - print("ERROR: Invalid command line option") - display_help(1) - - for opt, arg in options: - if opt in ('-b', '--build'): - BUILD_DIR = mk_util.norm_path(arg) - elif opt in ('h', '--help'): - display_help() - exit(1) - elif opt in ('--ml'): - ML_ENABLED=True - else: - print("ERROR: Invalid command line option: %s" % opt) - display_help(1) - - - + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY + global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED + global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('-b', + '--build', + default=BUILD_DIR, + help='Directory where Z3 is built (default: %(default)s)', + ) + parser.add_argument('--ml', + action='store_true', + default=False, + help='Include ML/OCaml API documentation' + ) + parser.add_argument('--doxygen-executable', + dest='doxygen_executable', + default=DOXYGEN_EXE, + help='Doxygen executable to use (default: %(default)s)', + ) + parser.add_argument('--temp-dir', + dest='temp_dir', + default=TEMP_DIR, + help='Path to directory to use as temporary directory. ' + '(default: %(default)s)', + ) + parser.add_argument('--output-dir', + dest='output_dir', + default=OUTPUT_DIRECTORY, + help='Path to output directory (default: %(default)s)', + ) + parser.add_argument('--z3py-package-path', + dest='z3py_package_path', + default=Z3PY_PACKAGE_PATH, + help='Path to directory containing Z3py package (default: %(default)s)', + ) + # FIXME: I would prefer not to have negative options (i.e. `--z3py` + # instead of `--no-z3py`) but historically these bindings have been on by + # default so we have options to disable generating documentation for these + # bindings rather than enable them. + parser.add_argument('--no-z3py', + dest='no_z3py', + action='store_true', + default=False, + help='Do not generate documentation for Python bindings', + ) + parser.add_argument('--no-dotnet', + dest='no_dotnet', + action='store_true', + default=False, + help='Do not generate documentation for .NET bindings', + ) + parser.add_argument('--no-java', + dest='no_java', + action='store_true', + default=False, + help='Do not generate documentation for Java bindings', + ) + parser.add_argument('--dotnet-search-paths', + dest='dotnet_search_paths', + nargs='+', + default=DOTNET_API_SEARCH_PATHS, + help='Specify one or more path to look for .NET files (default: %(default)s).', + ) + parser.add_argument('--java-search-paths', + dest='java_search_paths', + nargs='+', + default=JAVA_API_SEARCH_PATHS, + help='Specify one or more paths to look for Java files (default: %(default)s).', + ) + pargs = parser.parse_args() + ML_ENABLED = pargs.ml + BUILD_DIR = pargs.build + DOXYGEN_EXE = pargs.doxygen_executable + TEMP_DIR = pargs.temp_dir + OUTPUT_DIRECTORY = pargs.output_dir + Z3PY_PACKAGE_PATH = pargs.z3py_package_path + if not os.path.exists(Z3PY_PACKAGE_PATH): + raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH)) + if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3': + raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH)) + Z3PY_ENABLED = not pargs.no_z3py + DOTNET_ENABLED = not pargs.no_dotnet + JAVA_ENABLED = not pargs.no_java + DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths + JAVA_API_SEARCH_PATHS = pargs.java_search_paths + return def mk_dir(d): if not os.path.exists(d): os.makedirs(d) -# Eliminate def_API and extra_API directives from file 'inf'. +# Eliminate def_API, extra_API, and def_Type directives from file 'inf'. # The result is stored in 'outf'. def cleanup_API(inf, outf): pat1 = re.compile(".*def_API.*") pat2 = re.compile(".*extra_API.*") + pat3 = re.compile(r".*def_Type\(.*") _inf = open(inf, 'r') _outf = open(outf, 'w') for line in _inf: - if not pat1.match(line) and not pat2.match(line): + if not pat1.match(line) and not pat2.match(line) and not pat3.match(line): _outf.write(line) +def configure_file(template_file_path, output_file_path, substitutions): + """ + Read a template file ``template_file_path``, perform substitutions + found in the ``substitutions`` dictionary and write the result to + the output file ``output_file_path``. + + The template file should contain zero or more template strings of the + form ``@NAME@``. + + The substitutions dictionary maps old strings (without the ``@`` + symbols) to their replacements. + """ + assert isinstance(template_file_path, str) + assert isinstance(output_file_path, str) + assert isinstance(substitutions, dict) + assert len(template_file_path) > 0 + assert len(output_file_path) > 0 + print("Generating {} from {}".format(output_file_path, template_file_path)) + + if not os.path.exists(template_file_path): + raise Exception('Could not find template file "{}"'.format(template_file_path)) + + # Read whole template file into string + template_string = None + with open(template_file_path, 'r') as f: + template_string = f.read() + + # Do replacements + for (old_string, replacement) in substitutions.items(): + template_string = template_string.replace('@{}@'.format(old_string), replacement) + + # Write the string to the file + with open(output_file_path, 'w') as f: + f.write(template_string) + try: parse_options() - fi = open('website.dox', 'r') - fo = open('website-adj.dox', 'w') + print("Creating temporary directory \"{}\"".format(TEMP_DIR)) + mk_dir(TEMP_DIR) + # Short-hand for path to temporary file + def temp_path(path): + return os.path.join(TEMP_DIR, path) + # Short-hand for path to file in `doc` directory + def doc_path(path): + return os.path.join(SCRIPT_DIR, path) - for line in fi: - if (line != '[ML]\n'): - fo.write(line) - elif (ML_ENABLED): - fo.write(' - ML/OCaml API\n') - fi.close() - fo.close() + # Create configuration file from template + doxygen_config_substitutions = { + 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, + 'TEMP_DIR': TEMP_DIR, + 'CXX_API_SEARCH_PATHS': doc_path('../src/api/c++'), + } - mk_dir('api/html') - mk_dir('tmp') - shutil.copyfile('website-adj.dox', 'tmp/website.dox') - os.remove('website-adj.dox') - shutil.copyfile('../src/api/python/z3/z3.py', 'tmp/z3py.py') - cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h') - cleanup_API('../src/api/z3_ast_containers.h', 'tmp/z3_ast_containers.h') - cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h') - cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h') - cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') - cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h') - cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h') - cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') - cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h') + if Z3PY_ENABLED: + print("Z3Py documentation enabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py' + else: + print("Z3Py documentation disabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = '' + if DOTNET_ENABLED: + print(".NET documentation enabled") + doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs' + dotnet_api_search_path_str = "" + for p in DOTNET_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + dotnet_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = dotnet_api_search_path_str + else: + print(".NET documentation disabled") + doxygen_config_substitutions['DOTNET_API_FILES'] = '' + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '' + if JAVA_ENABLED: + print("Java documentation enabled") + doxygen_config_substitutions['JAVA_API_FILES'] = '*.java' + java_api_search_path_str = "" + for p in JAVA_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + java_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = java_api_search_path_str + else: + print("Java documentation disabled") + doxygen_config_substitutions['JAVA_API_FILES'] = '' + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '' + + doxygen_config_file = temp_path('z3api.cfg') + configure_file( + doc_path('z3api.cfg.in'), + doxygen_config_file, + doxygen_config_substitutions) + + website_dox_substitutions = {} + bullet_point_prefix='\n - ' + if Z3PY_ENABLED: + website_dox_substitutions['PYTHON_API'] = ( + '{prefix}Python API ' + '(also available in pydoc format)' + ).format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['PYTHON_API'] = '' + if DOTNET_ENABLED: + website_dox_substitutions['DOTNET_API'] = ( + '{prefix}' + '' + '.NET API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['DOTNET_API'] = '' + if JAVA_ENABLED: + website_dox_substitutions['JAVA_API'] = ( + '{prefix}' + 'Java API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['JAVA_API'] = '' + if ML_ENABLED: + website_dox_substitutions['OCAML_API'] = ( + 'ML/OCaml API' + ).format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['OCAML_API'] = '' + configure_file( + doc_path('website.dox.in'), + temp_path('website.dox'), + website_dox_substitutions) + + mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) + if Z3PY_ENABLED: + shutil.copyfile(doc_path('../src/api/python/z3/z3.py'), temp_path('z3py.py')) + cleanup_API(doc_path('../src/api/z3_api.h'), temp_path('z3_api.h')) + cleanup_API(doc_path('../src/api/z3_ast_containers.h'), temp_path('z3_ast_containers.h')) + cleanup_API(doc_path('../src/api/z3_algebraic.h'), temp_path('z3_algebraic.h')) + cleanup_API(doc_path('../src/api/z3_polynomial.h'), temp_path('z3_polynomial.h')) + cleanup_API(doc_path('../src/api/z3_rcf.h'), temp_path('z3_rcf.h')) + cleanup_API(doc_path('../src/api/z3_fixedpoint.h'), temp_path('z3_fixedpoint.h')) + cleanup_API(doc_path('../src/api/z3_optimization.h'), temp_path('z3_optimization.h')) + cleanup_API(doc_path('../src/api/z3_interp.h'), temp_path('z3_interp.h')) + cleanup_API(doc_path('../src/api/z3_fpa.h'), temp_path('z3_fpa.h')) print("Removed annotations from z3_api.h.") try: - if subprocess.call(['doxygen', 'z3api.dox']) != 0: + if subprocess.call([DOXYGEN_EXE, doxygen_config_file]) != 0: print("ERROR: doxygen returned nonzero return code") exit(1) except: print("ERROR: failed to execute 'doxygen', make sure doxygen (http://www.doxygen.org) is available in your system.") exit(1) - print("Generated C and .NET API documentation.") - os.remove('tmp/z3_api.h') - os.remove('tmp/z3_ast_containers.h') - os.remove('tmp/z3_algebraic.h') - os.remove('tmp/z3_polynomial.h') - os.remove('tmp/z3_rcf.h') - os.remove('tmp/z3_fixedpoint.h') - os.remove('tmp/z3_optimization.h') - os.remove('tmp/z3_interp.h') - os.remove('tmp/z3_fpa.h') - print("Removed temporary file header files.") - - os.remove('tmp/website.dox') - print("Removed temporary file website.dox") - os.remove('tmp/z3py.py') - print("Removed temporary file z3py.py") - os.removedirs('tmp') - print("Removed temporary directory tmp.") - sys.path.append('../src/api/python/z3') - pydoc.writedoc('z3') - shutil.move('z3.html', 'api/html/z3.html') - print("Generated Python documentation.") + print("Generated Doxygen based documentation") + shutil.rmtree(os.path.realpath(TEMP_DIR)) + print("Removed temporary directory \"{}\"".format(TEMP_DIR)) + if Z3PY_ENABLED: + # Put z3py at the beginning of the search path to try to avoid picking up + # an installed copy of Z3py. + sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) + pydoc.writedoc('z3') + shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) + print("Generated pydoc Z3Py documentation.") if ML_ENABLED: - mk_dir('api/html/ml') - if subprocess.call(['ocamldoc', '-html', '-d', 'api\html\ml', '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../src/api/ml/z3.mli']) != 0: + ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') + mk_dir(ml_output_dir) + if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0: print("ERROR: ocamldoc failed.") exit(1) print("Generated ML/OCaml documentation.") - print("Documentation was successfully generated at subdirectory './api/html'.") -except: + print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY)) +except Exception: exctype, value = sys.exc_info()[:2] print("ERROR: failed to generate documentation: %s" % value) exit(1) diff --git a/doc/website.dox b/doc/website.dox.in similarity index 67% rename from doc/website.dox rename to doc/website.dox.in index 799949752..17a8552d1 100644 --- a/doc/website.dox +++ b/doc/website.dox.in @@ -10,11 +10,7 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref capi - - \ref cppapi - - .NET API - - Java API - - Python API (also available in pydoc format) -[ML] + - \ref capi + - \ref cppapi @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ - Try Z3 online at RiSE4Fun. */ diff --git a/doc/z3api.dox b/doc/z3api.cfg.in similarity index 99% rename from doc/z3api.dox rename to doc/z3api.cfg.in index c96a7be73..9e946aa7f 100644 --- a/doc/z3api.dox +++ b/doc/z3api.cfg.in @@ -52,7 +52,7 @@ PROJECT_LOGO = # If a relative path is entered, it will be relative to the location # where doxygen was started. If left blank the current directory will be used. -OUTPUT_DIRECTORY = api +OUTPUT_DIRECTORY = "@OUTPUT_DIRECTORY@" # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create # 4096 sub-directories (in 2 levels) under the output directory of each output @@ -681,10 +681,9 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = ../src/api/dotnet \ - ../src/api/java \ - ../src/api/c++ \ - ./tmp +INPUT = "@TEMP_DIR@" \ + "@CXX_API_SEARCH_PATHS@" \ + @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is @@ -703,16 +702,14 @@ INPUT_ENCODING = UTF-8 # *.f90 *.f *.for *.vhd *.vhdl FILE_PATTERNS = website.dox \ - z3_api.h \ - z3_algebraic.h \ - z3_polynomial.h \ - z3_rcf.h \ - z3_interp.h \ - z3_fpa.h \ + z3_api.h \ + z3_algebraic.h \ + z3_polynomial.h \ + z3_rcf.h \ + z3_interp.h \ + z3_fpa.h \ z3++.h \ - z3py.py \ - *.cs \ - *.java + @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@ # The RECURSIVE tag can be used to turn specify whether or not subdirectories # should be searched for input files as well. Possible values are YES and NO. diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 272c94dda..45065f856 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1500,7 +1500,7 @@ extern "C" { All main interaction with Z3 happens in the context of a \c Z3_context. In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects - are determined by the scope level of #Z3_push and #Z3_pop. + are determined by the scope level of #Z3_solver_push and #Z3_solver_pop. In other words, a Z3_ast object remains valid until there is a call to Z3_pop that takes the current scope below the level where the object was created. @@ -3091,8 +3091,8 @@ extern "C" { \brief Create a numeral of a given sort. \param c logical context. - \param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}. - If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}. + \param numeral A string representing the numeral value in decimal notation. The string may be of the form `[num]*[.[num]*][E[+|-][num]+]`. + If the given sort is a real, then the numeral can be a rational, that is, a string of the form `[num]* / [num]*` . \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size. \sa Z3_mk_int @@ -3306,7 +3306,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst); /** - \brief Retrieve from \s the unit sequence positioned at position \c index. + \brief Retrieve from \c s the unit sequence positioned at position \c index. def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST))) */ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7be7300a2..5f2de5170 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include"ast.h" #include"ast_pp.h" #include"ast_ll_pp.h" diff --git a/src/ast/ast.h b/src/ast/ast.h index 9259d5431..6bb3b01c9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -117,6 +117,9 @@ public: explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); + } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 3737f4651..85d2ba749 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con switch(f->get_decl_kind()) { case OP_SEQ_UNIT: - return BR_FAILED; + SASSERT(num_args == 1); + return mk_seq_unit(args[0], result); case OP_SEQ_EMPTY: return BR_FAILED; case OP_RE_PLUS: @@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_re_union(args[0], args[1], result); case OP_RE_RANGE: - return BR_FAILED; + SASSERT(num_args == 2); + return mk_re_range(args[0], args[1], result); case OP_RE_INTERSECT: SASSERT(num_args == 2); return mk_re_inter(args[0], args[1], result); @@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return BR_FAILED; } +/* + * (seq.unit (_ BitVector 8)) ==> String constant + */ +br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { + sort * s = m().get_sort(e); + bv_util bvu(m()); + + if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) { + // specifically we want (_ BitVector 8) + rational n_val; + unsigned int n_size; + if (bvu.is_numeral(e, n_val, n_size)) { + if (n_size == 8) { + // convert to string constant + char ch = (char)n_val.get_int32(); + TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); + char s_tmp[2] = {ch, '\0'}; + symbol s(s_tmp); + result = m_util.str.mk_string(s); + return BR_DONE; + } + } + } + + return BR_FAILED; +} + /* string + string = string a + (b + c) = (a + b) + c @@ -1401,6 +1430,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { return BR_FAILED; } +/* + * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + */ +br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { + TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); + zstring str_lo, str_hi; + if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { + if (str_lo.length() == 1 && str_hi.length() == 1) { + unsigned int c1 = str_lo[0]; + unsigned int c2 = str_hi[0]; + if (c1 > c2) { + // exchange c1 and c2 + unsigned int tmp = c1; + c2 = c1; + c1 = tmp; + } + zstring s(c1); + expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); + for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { + zstring s_ch(ch); + expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); + acc = m_util.re.mk_union(acc, acc2); + } + result = acc; + return BR_REWRITE2; + } else { + m().raise_exception("string constants in re.range must have length 1"); + } + } + + return BR_FAILED; +} + /* emp+ = emp all+ = all @@ -1430,9 +1492,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { return BR_DONE; } - return BR_FAILED; -// result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); -// return BR_REWRITE2; + //return BR_FAILED; + result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); + return BR_REWRITE2; } br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 2b434f475..210b2d72c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -98,6 +98,7 @@ class seq_rewriter { re2automaton m_re2aut; expr_ref_vector m_es, m_lhs, m_rhs; + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_seq_length(expr* a, expr_ref& result); br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result); @@ -119,6 +120,7 @@ class seq_rewriter { br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result); + br_status mk_re_range(expr* lo, expr* hi, expr_ref& result); bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs); bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f282043e6..bf238d8c5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol init(); sort_names.push_back(builtin_name("Seq", SEQ_SORT)); sort_names.push_back(builtin_name("RegEx", RE_SORT)); + // SMT-LIB 2.5 compatibility sort_names.push_back(builtin_name("String", _STRING_SORT)); + sort_names.push_back(builtin_name("StringSequence", _STRING_SORT)); } app* seq_decl_plugin::mk_string(symbol const& s) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 2882e905d..76b5ebe31 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -273,6 +273,15 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } + bool is_string_term(expr const * n) const { + sort * s = get_sort(n); + return u.is_string(s); + } + + bool is_non_string_sequence(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && !u.is_string(s)); + } MATCH_BINARY(is_concat); MATCH_UNARY(is_length); diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 328128794..daf20e095 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m): m_bvutil(m), m_arrayutil(m), m_fpautil(m), + m_sequtil(m), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), @@ -77,6 +78,8 @@ void static_features::reset() { m_has_real = false; m_has_bv = false; m_has_fpa = false; + m_has_str = false; + m_has_seq_non_str = false; m_has_arrays = false; m_arith_k_sum .reset(); m_num_arith_terms = 0; @@ -279,6 +282,11 @@ void static_features::update_core(expr * e) { m_has_fpa = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; + if (!m_has_str && m_sequtil.str.is_string_term(e)) + m_has_str = true; + if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) { + m_has_seq_non_str = true; + } if (is_app(e)) { family_id fid = to_app(e)->get_family_id(); mark_theory(fid); diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 8b20c5463..e7f69e041 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -24,6 +24,7 @@ Revision History: #include"bv_decl_plugin.h" #include"array_decl_plugin.h" #include"fpa_decl_plugin.h" +#include"seq_decl_plugin.h" #include"map.h" struct static_features { @@ -32,6 +33,7 @@ struct static_features { bv_util m_bvutil; array_util m_arrayutil; fpa_util m_fpautil; + seq_util m_sequtil; family_id m_bfid; family_id m_afid; family_id m_lfid; @@ -77,6 +79,8 @@ struct static_features { bool m_has_real; // bool m_has_bv; // bool m_has_fpa; // + bool m_has_str; // has String-typed terms + bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // rational m_arith_k_sum; // sum of the numerals in arith atoms. unsigned m_num_arith_terms; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7060d79ad..f590725a7 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -249,6 +249,7 @@ protected: array_util m_arutil; fpa_util m_futil; seq_util m_sutil; + datalog::dl_decl_util m_dlutil; format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) { @@ -277,6 +278,7 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual seq_util & get_sutil() { return m_sutil; } + virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { return @@ -527,6 +529,9 @@ bool cmd_context::logic_has_fpa() const { return !has_logic() || smt_logics::logic_has_fpa(m_logic); } +bool cmd_context::logic_has_str() const { + return !has_logic() || m_logic == "QF_S"; +} bool cmd_context::logic_has_array() const { return !has_logic() || smt_logics::logic_has_array(m_logic); @@ -568,7 +573,6 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); - svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -616,7 +620,6 @@ void cmd_context::init_external_manager() { init_manager_core(false); } - bool cmd_context::set_logic(symbol const & s) { if (has_logic()) throw cmd_exception("the logic has already been set"); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 92943c71c..8885bc5d6 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -257,6 +257,7 @@ protected: bool logic_has_array() const; bool logic_has_datatype() const; bool logic_has_fpa() const; + bool logic_has_str() const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;} diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cd13ac7a4..df5aa6517 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3141,6 +3141,101 @@ namespace sat { // // ----------------------- +static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { + for (unsigned i = 0; i < lambda.size(); ++i) { + if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { + lambda[i] = lambda.back(); + lambda.pop_back(); + --i; + } + } +} + +// Algorithm 7: Corebased Algorithm with Chunking + +static void back_remove(sat::literal_vector& lits, sat::literal l) { + for (unsigned i = lits.size(); i > 0; ) { + --i; + if (lits[i] == l) { + lits[i] = lits.back(); + lits.pop_back(); + return; + } + } + std::cout << "UNREACHABLE\n"; +} + + static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector& conseq) { + for (unsigned i = 0; i < gamma.size(); ++i) { + sat::literal nlit = ~gamma[i]; + sat::literal_vector asms1(asms); + asms1.push_back(nlit); + lbool r = s.check(asms1.size(), asms1.c_ptr()); + if (r == l_false) { + conseq.push_back(s.get_core()); + } + } +} + + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { + sat::literal_vector lambda; + for (unsigned i = 0; i < vars.size(); i++) { + lambda.push_back(sat::literal(i, m[vars[i]] == l_false)); + } + while (!lambda.empty()) { + IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";); + unsigned k = std::min(K, lambda.size()); + sat::literal_vector gamma, omegaN; + for (unsigned i = 0; i < k; ++i) { + sat::literal l = lambda[lambda.size() - i - 1]; + gamma.push_back(l); + omegaN.push_back(~l); + } + while (true) { + sat::literal_vector asms1(asms); + asms1.append(omegaN); + lbool r = s.check(asms1.size(), asms1.c_ptr()); + if (r == l_true) { + IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";); + prune_unfixed(lambda, s.get_model()); + break; + } + sat::literal_vector const& core = s.get_core(); + sat::literal_vector occurs; + IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";); + for (unsigned i = 0; i < omegaN.size(); ++i) { + if (core.contains(omegaN[i])) { + occurs.push_back(omegaN[i]); + } + } + if (occurs.size() == 1) { + sat::literal lit = occurs.back(); + sat::literal nlit = ~lit; + conseq.push_back(core); + back_remove(lambda, ~lit); + back_remove(gamma, ~lit); + s.mk_clause(1, &nlit); + } + for (unsigned i = 0; i < omegaN.size(); ++i) { + if (occurs.contains(omegaN[i])) { + omegaN[i] = omegaN.back(); + omegaN.pop_back(); + --i; + } + } + if (omegaN.empty() && occurs.size() > 1) { + brute_force_consequences(s, asms, gamma, conseq); + for (unsigned i = 0; i < gamma.size(); ++i) { + back_remove(lambda, gamma[i]); + } + break; + } + } + } + return l_true; + } + + lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { literal_vector lits; lbool is_sat = l_true; @@ -3163,6 +3258,9 @@ namespace sat { default: break; } } + + // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); + is_sat = get_consequences(asms, lits, conseq); set_model(mdl); return is_sat; @@ -3310,7 +3408,7 @@ namespace sat { propagate(false); ++num_resolves; } - if (scope_lvl() == 1) { + if (false && scope_lvl() == 1) { break; } } diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index f63e07b57..e6551b8da 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -405,7 +405,6 @@ namespace smt { bool context::validate_justification(bool_var v, bool_var_data const& d, b_justification const& j) { if (j.get_kind() == b_justification::CLAUSE && v != true_bool_var) { clause* cls = j.get_clause(); - unsigned num_lits = cls->get_num_literals(); literal l = cls->get_literal(0); if (l.var() != v) { l = cls->get_literal(1); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 77882f186..439adbdff 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -552,6 +552,7 @@ namespace smt { bool is_int(theory_var v) const { return m_data[v].m_is_int; } bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); } bool is_real(theory_var v) const { return !is_int(v); } + bool is_real_src(theory_var v) const { return !is_int_src(v); } bool get_implied_old_value(theory_var v, inf_numeral & r) const; inf_numeral const & get_implied_value(theory_var v) const; inf_numeral const & get_quasi_base_value(theory_var v) const { return get_implied_value(v); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 785e0120f..5c652414a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -465,7 +465,7 @@ namespace smt { TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n"; tout << s_ante << "\n" << s_conseq << "\n";); - literal lits[2] = {l_ante, l_conseq}; + // literal lits[2] = {l_ante, l_conseq}; mk_clause(l_ante, l_conseq, 0, 0); if (ctx.relevancy()) { if (l_ante == false_literal) { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index c8729ea36..8a632cf48 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -444,7 +444,7 @@ namespace smt { m_asserted_bounds.push_back(new_bound); // copy justification to new bound dependency2new_bound(dep, *new_bound); - TRACE("buggy_bound", new_bound->display(*this, tout); tout << "\n";); + TRACE("non_linear", new_bound->display(*this, tout); tout << "\n";); } /** @@ -457,8 +457,19 @@ namespace smt { bool r = false; if (!i.minus_infinity()) { inf_numeral new_lower(i.get_lower_value()); - if (i.is_lower_open()) - new_lower += get_epsilon(v); + if (i.is_lower_open()) { + if (is_int(v)) { + if (new_lower.is_int()) { + new_lower += rational::one(); + } + else { + new_lower = ceil(new_lower.get_rational()); + } + } + else { + new_lower += get_epsilon(v); + } + } bound * old_lower = lower(v); if (old_lower == 0 || new_lower > old_lower->get_value()) { TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n"; @@ -469,8 +480,19 @@ namespace smt { } if (!i.plus_infinity()) { inf_numeral new_upper(i.get_upper_value()); - if (i.is_upper_open()) - new_upper -= get_epsilon(v); + if (i.is_upper_open()) { + if (is_int(v)) { + if (new_upper.is_int()) { + new_upper -= rational::one(); + } + else { + new_upper = floor(new_upper.get_rational()); + } + } + else { + new_upper -= get_epsilon(v); + } + } bound * old_upper = upper(v); if (old_upper == 0 || new_upper < old_upper->get_value()) { TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n"; @@ -819,6 +841,7 @@ namespace smt { if (is_fixed(_var)) r *= lower_bound(_var).get_rational(); } + TRACE("arith", tout << mk_pp(m, get_manager()) << " " << r << "\n";); return r; } @@ -896,7 +919,7 @@ namespace smt { // Assert the equality // (= (* x_1 ... x_n) k) - TRACE("non_linear", tout << "all variables are fixed.\n";); + TRACE("non_linear", tout << "all variables are fixed, and bound is: " << k << "\n";); new_lower = alloc(derived_bound, v, inf_numeral(k), B_LOWER); new_upper = alloc(derived_bound, v, inf_numeral(k), B_UPPER); } @@ -953,7 +976,8 @@ namespace smt { new_upper->m_eqs.append(new_lower->m_eqs); TRACE("non_linear", - tout << "lower: " << new_lower << " upper: " << new_upper << "\n"; + new_lower->display(*this, tout << "lower: "); tout << "\n"; + new_upper->display(*this, tout << "upper: "); tout << "\n"; for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) { ctx.display_detailed_literal(tout, new_upper->m_lits[j]); tout << " "; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9dd082de0..7a9369fd3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3874,8 +3874,8 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { } else if (n1 != n2 && m_util.is_re(n1->get_owner())) { warning_msg("equality between regular expressions is not yet supported"); - eautomaton* a1 = get_automaton(n1->get_owner()); - eautomaton* a2 = get_automaton(n2->get_owner()); + // eautomaton* a1 = get_automaton(n1->get_owner()); + // eautomaton* a2 = get_automaton(n2->get_owner()); // eautomaton* b1 = mk_difference(*a1, *a2); // eautomaton* b2 = mk_difference(*a2, *a1); // eautomaton* c = mk_union(*b1, *b2); diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index a4eaa4222..3387e1a8e 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -64,6 +64,56 @@ static void display_status(lbool r) { } } +static void track_clause(sat::solver& dst, + sat::literal_vector& lits, + sat::literal_vector& assumptions, + vector& tracking_clauses) { + sat::literal lit = sat::literal(dst.mk_var(true, false), false); + tracking_clauses.set(lit.var(), lits); + lits.push_back(~lit); + dst.mk_clause(lits.size(), lits.c_ptr()); + assumptions.push_back(lit); +} + + +static void track_clauses(sat::solver const& src, + sat::solver& dst, + sat::literal_vector& assumptions, + vector& tracking_clauses) { + for (sat::bool_var v = 0; v < src.num_vars(); ++v) { + dst.mk_var(false, true); + } + sat::literal_vector lits; + sat::literal lit; + sat::clause * const * it = src.begin_clauses(); + sat::clause * const * end = src.end_clauses(); + svector bin_clauses; + src.collect_bin_clauses(bin_clauses, false); + tracking_clauses.reserve(2*src.num_vars() + static_cast(end - it) + bin_clauses.size()); + + for (sat::bool_var v = 1; v < src.num_vars(); ++v) { + if (src.value(v) != l_undef) { + bool sign = src.value(v) == l_false; + lits.reset(); + lits.push_back(sat::literal(v, sign)); + track_clause(dst, lits, assumptions, tracking_clauses); + } + } + for (; it != end; ++it) { + lits.reset(); + sat::clause& cls = *(*it); + lits.append(static_cast(cls.end()-cls.begin()), cls.begin()); + track_clause(dst, lits, assumptions, tracking_clauses); + } + for (unsigned i = 0; i < bin_clauses.size(); ++i) { + lits.reset(); + lits.push_back(bin_clauses[i].first); + lits.push_back(bin_clauses[i].second); + track_clause(dst, lits, assumptions, tracking_clauses); + } +} + + static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { for (unsigned i = 0; i < lambda.size(); ++i) { if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { @@ -88,18 +138,20 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { std::cout << "UNREACHABLE\n"; } -static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) { +static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, sat::literal_vector& backbones) { for (unsigned i = 0; i < gamma.size(); ++i) { sat::literal nlit = ~gamma[i]; - lbool r = s.check(1, &nlit); + sat::literal_vector asms1(asms); + asms1.push_back(nlit); + lbool r = s.check(asms1.size(), asms1.c_ptr()); if (r == l_false) { backbones.push_back(gamma[i]); } } } -static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector& conseq, unsigned K) { - lbool r = s.check(); +static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { + lbool r = s.check(asms.size(), asms.c_ptr()); display_status(r); if (r != l_true) { return r; @@ -119,7 +171,9 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector 1) { - brute_force_consequences(s, gamma, backbones); + brute_force_consequences(s, asms, gamma, backbones); for (unsigned i = 0; i < gamma.size(); ++i) { back_remove(lambda, gamma[i]); } @@ -174,6 +228,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { p.set_bool("produce_models", true); reslimit limit; sat::solver solver(p, limit, 0); + sat::solver solver2(p, limit, 0); g_solver = &solver; if (file_name) { @@ -192,16 +247,22 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vector conseq; sat::bool_var_vector vars; sat::literal_vector assumptions; - for (unsigned i = 1; i < solver.num_vars(); ++i) { + if (p.get_bool("dimacs.core", false)) { + g_solver = &solver2; + vector tracking_clauses; + track_clauses(solver, solver2, assumptions, tracking_clauses); + } + + for (unsigned i = 1; i < g_solver->num_vars(); ++i) { vars.push_back(i); - solver.set_external(i); + g_solver->set_external(i); } lbool r; if (use_chunk) { - r = core_chunking(solver, vars, conseq, 100); + r = core_chunking(*g_solver, vars, assumptions, conseq, 100); } else { - r = solver.get_consequences(assumptions, vars, conseq); + r = g_solver->get_consequences(assumptions, vars, conseq); } std::cout << vars.size() << " " << conseq.size() << "\n"; display_status(r); diff --git a/src/test/main.cpp b/src/test/main.cpp index 4a54797ac..15f92b2f7 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -8,6 +8,7 @@ #include"timeit.h" #include"warning.h" #include "memory_manager.h" +#include"gparams.h" // // Unit tests fail by asserting. @@ -75,7 +76,7 @@ void display_usage() { void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) { int i = 1; while (i < argc) { - char * arg = argv[i]; + char * arg = argv[i], *eq_pos = 0; if (arg[0] == '-' || arg[0] == '/') { char * opt_name = arg + 1; @@ -118,6 +119,17 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t } #endif } + else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) { + char * key = arg; + *eq_pos = 0; + char * value = eq_pos+1; + try { + gparams::set(key, value); + } + catch (z3_exception& ex) { + std::cerr << ex.msg() << "\n"; + } + } i++; } }