diff --git a/CMakeLists.txt b/CMakeLists.txt index 47a081e75..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 @@ -155,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}") @@ -326,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 ################################################################################ @@ -376,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 ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 4bbbd36a8..9289d40f1 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -292,6 +292,7 @@ The following useful options can be passed to CMake whilst configuring. 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. 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/src/ast/simplifier/poly_simplifier_plugin.h b/src/ast/simplifier/poly_simplifier_plugin.h index 4e6ae9c15..ed6d506c5 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.h +++ b/src/ast/simplifier/poly_simplifier_plugin.h @@ -37,7 +37,7 @@ protected: expr * mk_add(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_add(2, args); } expr * mk_mul(unsigned num_args, expr * const * args); expr * mk_mul(expr * arg1, expr * arg2) { expr * args[2] = { arg1, arg2 }; return mk_mul(2, args); } - expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); } + // expr * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_fid, m_SUB, num_args, args); } expr * mk_uminus(expr * arg) { return m_manager.mk_app(m_fid, m_UMINUS, arg); } void process_monomial(unsigned num_args, expr * const * args, numeral & k, ptr_buffer & result); diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index c75c12689..0faddce73 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -187,6 +187,7 @@ struct check_logic::imp { m_bvs = true; m_uf = true; m_ints = true; + m_nonlinear = true; // non-linear 0-1 variables may get eliminated } else { m_unknown_logic = true; diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h index b1719577b..a4e9f192e 100644 --- a/src/muz/base/dl_util.h +++ b/src/muz/base/dl_util.h @@ -29,6 +29,7 @@ Revision History: #include"substitution.h" #include"ast_counter.h" #include"statistics.h" +#include"stopwatch.h" #include"lbool.h" namespace datalog { diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 160eb7b94..196f5268c 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -30,7 +30,6 @@ Revision History: namespace datalog { - class execution_context; class instruction_block; class rel_context; diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index cbfcbf1fe..491aca8ba 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2219,11 +2219,27 @@ namespace smt2 { if (m_cached_strings.empty()) throw cmd_exception("invalid get-value command, empty list of terms"); next(); + unsigned index = 0; + if (curr_is_keyword() && (curr_id() == ":model-index" || curr_id() == ":model_index")) { + next(); + check_int("integer index expected to indexed model evaluation"); + if (!curr_numeral().is_unsigned()) + throw parser_exception("expected unsigned integer index to model evaluation"); + index = curr_numeral().get_unsigned(); + next(); + } + check_rparen("invalid get-value command, ')' expected"); if (!m_ctx.is_model_available() || m_ctx.get_check_sat_result() == 0) throw cmd_exception("model is not available"); model_ref md; - m_ctx.get_check_sat_result()->get_model(md); + if (index == 0) { + m_ctx.get_check_sat_result()->get_model(md); + } + else { + m_ctx.get_opt()->get_box_model(md, index); + + } m_ctx.regular_stream() << "("; expr ** expr_it = expr_stack().c_ptr() + spos; expr ** expr_end = expr_it + m_cached_strings.size(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 739a591e7..dc5aa2964 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(vars[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; @@ -3273,13 +3371,14 @@ namespace sat { propagate(false); if (check_inconsistent()) return l_false; - unsigned num_units = 0, num_iterations = 0; - extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); + unsigned num_iterations = 0; + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); while (!unfixed_lits.empty()) { if (scope_lvl() > 1) { pop(scope_lvl() - 1); } + propagate(false); ++num_iterations; checkpoint(); literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); @@ -3291,6 +3390,10 @@ namespace sat { literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; + if (lvl(lit) <= 1) { + SASSERT(value(lit) == l_true); + extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); + } continue; } push(); @@ -3307,19 +3410,14 @@ namespace sat { propagate(false); ++num_resolves; } - if (scope_lvl() == 1) { + if (false && scope_lvl() == 1) { + is_sat = l_undef; break; } } - if (scope_lvl() == 1) { - it = unfixed_lits.begin(); - for (; it != end; ++it) { - literal lit = *it; - if (value(lit) == l_true) { - VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq)); - } - } - } + + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); + if (is_sat == l_true) { if (scope_lvl() == 1 && num_resolves > 0) { IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";); @@ -3330,6 +3428,7 @@ namespace sat { if (is_sat == l_undef) { restart(); } + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); } } if (is_sat == l_false) { @@ -3339,7 +3438,6 @@ namespace sat { if (is_sat == l_true) { delete_unfixed(unfixed_lits, unfixed_vars); } - extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations @@ -3391,32 +3489,47 @@ namespace sat { SASSERT(!inconsistent()); unsigned sz = m_trail.size(); for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) { - if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) { - for (i = 0; i < sz && lvl(m_trail[i]) <= 1; ++i) { - VERIFY(extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)); - } - break; - } + extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq); } start = sz; } + void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector& conseq) { + literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); + for (; it != end; ++it) { + literal lit = *it; + if (lvl(lit) <= 1) { + SASSERT(value(lit) == l_true); + extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); + } + } + } + bool solver::check_domain(literal lit, literal lit2) { - return m_antecedents.contains(lit2.var()); + if (!m_antecedents.contains(lit2.var())) { + SASSERT(value(lit2) == l_true); + m_todo_antecedents.push_back(lit2); + TRACE("sat", tout << "todo: " << lit2 << " " << value(lit2) << "\n";); + return false; + } + else { + return true; + } } bool solver::extract_assumptions(literal lit, index_set& s) { justification js = m_justification[lit.var()]; + TRACE("sat", tout << lit << " " << js << "\n";); switch (js.get_kind()) { case justification::NONE: break; case justification::BINARY: - if (!check_domain(lit, js.get_literal())) return false; + if (!check_domain(lit, ~js.get_literal())) return false; s |= m_antecedents.find(js.get_literal().var()); break; case justification::TERNARY: - if (!check_domain(lit, js.get_literal1())) return false; - if (!check_domain(lit, js.get_literal2())) return false; + if (!check_domain(lit, ~js.get_literal1()) || + !check_domain(lit, ~js.get_literal2())) return false; s |= m_antecedents.find(js.get_literal1().var()); s |= m_antecedents.find(js.get_literal2().var()); break; @@ -3424,7 +3537,7 @@ namespace sat { clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset())); for (unsigned i = 0; i < c.size(); ++i) { if (c[i] != lit) { - if (!check_domain(lit, c[i])) return false; + if (!check_domain(lit, ~c[i])) return false; s |= m_antecedents.find(c[i].var()); } } @@ -3458,7 +3571,7 @@ namespace sat { } - bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { + bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { index_set s; if (m_antecedents.contains(lit.var())) { return true; @@ -3468,6 +3581,7 @@ namespace sat { } else { if (!extract_assumptions(lit, s)) { + SASSERT(!m_todo_antecedents.empty()); return false; } add_assumption(lit); @@ -3486,6 +3600,16 @@ namespace sat { return true; } + void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq) { + SASSERT(m_todo_antecedents.empty()); + m_todo_antecedents.push_back(lit); + while (!m_todo_antecedents.empty()) { + if (extract_fixed_consequences1(m_todo_antecedents.back(), assumptions, unfixed, conseq)) { + m_todo_antecedents.pop_back(); + } + } + } + void solver::asymmetric_branching() { if (scope_lvl() > 0 || inconsistent()) return; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c7f472a60..a26abe1e0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -481,6 +481,7 @@ namespace sat { typedef hashtable index_set; u_map m_antecedents; + literal_vector m_todo_antecedents; vector m_binary_clause_graph; bool extract_assumptions(literal lit, index_set& s); @@ -497,7 +498,11 @@ namespace sat { void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); - bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + + void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); + + bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector& conseq); void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars); diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 760fdcf54..278dad287 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -20,12 +20,12 @@ static opt::context* g_opt = 0; static double g_start_time = 0; static unsigned_vector g_handles; -class stream_buffer { +class opt_stream_buffer { std::istream & m_stream; int m_val; unsigned m_line; public: - stream_buffer(std::istream & s): + opt_stream_buffer(std::istream & s): m_stream(s), m_line(0) { m_val = m_stream.get(); @@ -111,7 +111,7 @@ public: class wcnf { opt::context& opt; ast_manager& m; - stream_buffer& in; + opt_stream_buffer& in; app_ref read_clause(unsigned& weight) { int parsed_lit; @@ -141,7 +141,7 @@ class wcnf { public: - wcnf(opt::context& opt, stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) { + wcnf(opt::context& opt, opt_stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) { opt.set_clausal(true); } @@ -180,7 +180,7 @@ public: class opb { opt::context& opt; ast_manager& m; - stream_buffer& in; + opt_stream_buffer& in; arith_util arith; app_ref parse_id() { @@ -254,7 +254,7 @@ class opb { opt.add_hard_constraint(t); } public: - opb(opt::context& opt, stream_buffer& in): + opb(opt::context& opt, opt_stream_buffer& in): opt(opt), m(opt.get_manager()), in(in), arith(m) {} @@ -335,7 +335,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) { g_opt = &opt; params_ref p = gparams::get_module("opt"); opt.updt_params(p); - stream_buffer _in(in); + opt_stream_buffer _in(in); if (is_wcnf) { wcnf wcnf(opt, _in); wcnf.parse(); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f003dfa37..68a9f980d 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -63,7 +63,6 @@ namespace smt { m_is_diseq_tmp(0), m_units_to_reassert(m_manager), m_qhead(0), - m_th_case_split_qhead(0), m_simp_qhead(0), m_simp_counter(0), m_bvar_inc(1.0), @@ -341,7 +340,6 @@ namespace smt { bool context::bcp() { SASSERT(!inconsistent()); - m_th_case_split_qhead = m_qhead; while (m_qhead < m_assigned_literals.size()) { if (get_cancel_flag()) { return true; @@ -1777,7 +1775,7 @@ namespace smt { unsigned qhead = m_qhead; if (!bcp()) return false; - if (!propagate_th_case_split()) + if (!propagate_th_case_split(qhead)) return false; if (get_cancel_flag()) { m_qhead = qhead; @@ -2977,7 +2975,6 @@ namespace smt { public: case_split_insert_trail(literal l): l(l) { - } virtual void undo(context & ctx) { ctx.undo_th_case_split(l); @@ -2988,23 +2985,19 @@ namespace smt { TRACE("theory_case_split", display_literals_verbose(tout << "theory case split: ", num_lits, lits); tout << std::endl;); // If we don't use the theory case split heuristic, // for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2) - // to enforce the condition that more than one literal can't be - // assigned 'true' simultaneously. + // to enforce the condition that at most one literal can be assigned 'true'. if (!m_fparams.m_theory_case_split) { for (unsigned i = 0; i < num_lits; ++i) { for (unsigned j = i+1; j < num_lits; ++j) { literal l1 = lits[i]; literal l2 = lits[j]; - literal excl[2] = {~l1, ~l2}; - justification * j_excl = 0; - mk_clause(2, excl, j_excl); + mk_clause(~l1, ~l2, (justification*) 0); } } } else { - literal_vector new_case_split; // TODO is it okay to allocate this on the stack? + literal_vector new_case_split; for (unsigned i = 0; i < num_lits; ++i) { literal l = lits[i]; - // TODO do we need to enforce this invariant? can we make undo information work without it? SASSERT(!m_all_th_case_split_literals.contains(l.index())); m_all_th_case_split_literals.insert(l.index()); push_trail(case_split_insert_trail(l)); @@ -3020,11 +3013,11 @@ namespace smt { m_literal2casesplitsets[l.index()].push_back(new_case_split); } TRACE("theory_case_split", tout << "tracking case split literal set { "; - for (unsigned i = 0; i < num_lits; ++i) { - tout << lits[i].index() << " "; - } - tout << "}" << std::endl; - ); + for (unsigned i = 0; i < num_lits; ++i) { + tout << lits[i].index() << " "; + } + tout << "}" << std::endl; + ); } } @@ -3041,7 +3034,7 @@ namespace smt { } } - bool context::propagate_th_case_split() { + bool context::propagate_th_case_split(unsigned qhead) { if (m_all_th_case_split_literals.empty()) return true; @@ -3049,46 +3042,33 @@ namespace smt { // not counting any literals that get assigned by this method // this relies on bcp() to give us its old m_qhead and therefore // bcp() should always be called before this method - unsigned assigned_literal_idx = m_th_case_split_qhead; unsigned assigned_literal_end = m_assigned_literals.size(); - while(assigned_literal_idx < assigned_literal_end) { - literal l = m_assigned_literals[assigned_literal_idx]; + for (; qhead < assigned_literal_end; ++qhead) { + literal l = m_assigned_literals[qhead]; TRACE("theory_case_split", tout << "check literal " << l.index() << std::endl; display_literal_verbose(tout, l); tout << std::endl;); - ++assigned_literal_idx; // check if this literal participates in any theory case split - if (m_all_th_case_split_literals.contains(l.index())) { - TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); - // now find the sets of literals which contain l - vector case_split_sets = m_literal2casesplitsets.get(l.index(), vector()); - for (vector::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { - literal_vector case_split_set = *it; - TRACE("theory_case_split", tout << "found case split set { "; - for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { - tout << set_it->index() << " "; - } - tout << "}" << std::endl;); - for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { - literal l2 = *set_it; - if (l2 != l) { - b_justification js(l); - switch (get_assignment(l2)) { - case l_false: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned False" << std::endl;); - break; - // TODO these next two cases can be combined. I'm doing this for debugging purposes - case l_undef: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is not assigned" << std::endl;); - assign(~l2, js); - break; - case l_true: - TRACE("theory_case_split", tout << "case split literal " << l2.index() << " is already assigned True" << std::endl;); - assign(~l2, js); - break; - } - if (inconsistent()) { - TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); - return false; - } + if (!m_all_th_case_split_literals.contains(l.index())) { + continue; + } + TRACE("theory_case_split", tout << "assigned literal " << l.index() << " is a theory case split literal" << std::endl;); + // now find the sets of literals which contain l + vector const& case_split_sets = m_literal2casesplitsets[l.index()]; + for (vector::const_iterator it = case_split_sets.begin(); it != case_split_sets.end(); ++it) { + literal_vector case_split_set = *it; + TRACE("theory_case_split", tout << "found case split set { "; + for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { + tout << set_it->index() << " "; + } + tout << "}" << std::endl;); + for(literal_vector::iterator set_it = case_split_set.begin(); set_it != case_split_set.end(); ++set_it) { + literal l2 = *set_it; + if (l2 != l) { + b_justification js(l); + TRACE("theory_case_split", tout << "case split literal "; l2.display(tout, m_manager, m_bool_var2expr.c_ptr());); + assign(~l2, js); + if (inconsistent()) { + TRACE("theory_case_split", tout << "conflict detected!" << std::endl;); + return false; } } } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3f8f9b1f1..f6837307a 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -234,7 +234,6 @@ namespace smt { uint_set m_all_th_case_split_literals; vector m_th_case_split_sets; u_map< vector > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in - unsigned m_th_case_split_qhead; // ----------------------------------- // @@ -851,7 +850,7 @@ namespace smt { // helper function for trail void undo_th_case_split(literal l); - bool propagate_th_case_split(); + bool propagate_th_case_split(unsigned qhead); bool_var mk_bool_var(expr * n); 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 7a5d46e7d..eb36a92fb 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 7864955a4..7fed094da 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_bv.cpp b/src/smt/theory_bv.cpp index ae2aa95e2..255e2044f 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -762,6 +762,21 @@ namespace smt { TRACE("bv", tout << mk_pp(cond, get_manager()) << "\n"; tout << l << "\n";); \ } + void theory_bv::internalize_sub(app *n) { + SASSERT(!get_context().e_internalized(n)); + SASSERT(n->get_num_args() == 2); + process_args(n); + ast_manager & m = get_manager(); + enode * e = mk_enode(n); + expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m); + get_arg_bits(e, 0, arg1_bits); + get_arg_bits(e, 1, arg2_bits); + SASSERT(arg1_bits.size() == arg2_bits.size()); + expr_ref carry(m); + m_bb.mk_subtracter(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits, carry); + init_bits(e, bits); + } + MK_UNARY(internalize_not, mk_not); MK_UNARY(internalize_redand, mk_redand); MK_UNARY(internalize_redor, mk_redor); @@ -848,6 +863,7 @@ namespace smt { switch (term->get_decl_kind()) { case OP_BV_NUM: internalize_num(term); return true; case OP_BADD: internalize_add(term); return true; + case OP_BSUB: internalize_sub(term); return true; case OP_BMUL: internalize_mul(term); return true; case OP_BSDIV_I: internalize_sdiv(term); return true; case OP_BUDIV_I: internalize_udiv(term); return true; diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 17d03b412..50e4f9c30 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -172,6 +172,7 @@ namespace smt { bool get_fixed_value(theory_var v, numeral & result) const; void internalize_num(app * n); void internalize_add(app * n); + void internalize_sub(app * n); void internalize_mul(app * n); void internalize_udiv(app * n); void internalize_sdiv(app * n); 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/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 9afd97de5..35601f374 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -137,8 +137,10 @@ public: SASSERT(num.is_unsigned()); expr_ref head(m); ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); - consequences[i] = m.mk_implies(a, head); + if (enums.size() > num.get_unsigned()) { + head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + consequences[i] = m.mk_implies(a, head); + } } } return r; diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index a4eaa4222..b95977a46 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,26 +138,27 @@ 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(); - display_status(r); +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()); if (r != l_true) { return r; } sat::model const & m = s.get_model(); sat::literal_vector lambda, backbones; - for (unsigned i = 1; i < m.size(); i++) { - lambda.push_back(sat::literal(i, m[i] == l_false)); + for (unsigned i = 0; i < vars.size(); i++) { + lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false)); } while (!lambda.empty()) { IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << backbones.size() << ")\n";); @@ -119,7 +170,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 +227,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 +246,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); @@ -209,10 +269,15 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { } void tst_cnf_backbones(char ** argv, int argc, int& i) { + bool use_chunk = i + 1 < argc && argv[i + 1] == std::string("chunk"); + if (use_chunk) ++i; + char const* file = ""; if (i + 1 < argc) { - bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk")); - cnf_backbones(use_chunk, argv[i + 1]); - ++i; - if (use_chunk) ++i; + file = argv[i + 1]; } + else { + file = argv[1]; + } + cnf_backbones(use_chunk, file); + ++i; } 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++; } }