From 88147f7047f85b64c26660717871e0d6be8c3eeb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 28 Apr 2017 14:14:28 -0400 Subject: [PATCH 01/32] theory_str static features and cmd_context --- src/ast/static_features.cpp | 8 ++++++++ src/ast/static_features.h | 4 ++++ src/cmd_context/cmd_context.cpp | 7 +++++-- src/cmd_context/cmd_context.h | 1 + 4 files changed, 18 insertions(+), 2 deletions(-) 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;} From 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 17:59:04 +0100 Subject: [PATCH 02/32] [CMake] Remove compiler flag overrides and support for C language. The setting of overrides was broken (the CXX flags were not set but the C flags were) and we aren't even using the C compiler any more. The C compiler is used by the example C project but that is built as an external project now so we don't need C support anymore. The setting of defaults was also very fragile. CMake has quite complicated support here (e.g. MSVC with a clang based tool chain) which would likely not work properly with the override approach as it existed. This means we loose some of the custom linker flags we were setting for MSVC but we were never doing a great job of replicating the exact set of flags used in the old build system anyway. Subsequent commits will gradually fix this. --- CMakeLists.txt | 4 +- .../cmake/cmake/compiler_flags_override.cmake | 43 ------------------- 2 files changed, 1 insertion(+), 46 deletions(-) delete mode 100644 contrib/cmake/cmake/compiler_flags_override.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 47a081e75..ab3976aea 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,9 +24,7 @@ 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) +project(Z3 CXX) ################################################################################ # Project version 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) From f568b2478ff743b735f5e1ab03325040ea320cc9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 21:30:36 +0100 Subject: [PATCH 03/32] [CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_, CMAKE__LINKER_FLAGS, and CMAKE__LINKER_FLAGS_. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake. --- CMakeLists.txt | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index ab3976aea..795a23320 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -153,13 +153,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}") @@ -374,6 +374,28 @@ if (BUILD_LIBZ3_SHARED) endif() 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 ################################################################################ From fe1af4bcdb7c4f4d85874e449fae3db8cf0a49ad Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 23:28:04 +0100 Subject: [PATCH 04/32] [CMake] Teach build system to pass `/fp:precise` to compiler when using MSVC. This is set by the old build system but we weren't setting it. This actually MSVC's default but in an effort to try to behave more like the old build system we will set it anyway. --- CMakeLists.txt | 9 +++++++++ contrib/cmake/cmake/z3_add_cxx_flag.cmake | 1 + 2 files changed, 10 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 795a23320..6e858a421 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -324,6 +324,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 ################################################################################ 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}) From fb403229bd7a2bc422afe574c98dd858035c42aa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 00:29:26 +0100 Subject: [PATCH 05/32] [CMake] CMake's default value for CMAKE_CXX_FLAGS includes `/W3` remove this so we can have fine grained control of warnings. --- contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake index c214e4464..e49e43947 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() From 0e1343e78db9d396240151af436a1a2028cc40fa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 01:21:49 +0100 Subject: [PATCH 06/32] [CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default. --- CMakeLists.txt | 5 +++ README-CMake.md | 1 + contrib/cmake/cmake/compiler_lto.cmake | 52 ++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) create mode 100644 contrib/cmake/cmake/compiler_lto.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 6e858a421..8afc6339b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -383,6 +383,11 @@ if (BUILD_LIBZ3_SHARED) endif() endif() +################################################################################ +# Link time optimization +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake) + ################################################################################ # Report default CMake 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_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() From 870be706e958f37d6bc7a0ca0347704b56a9c08d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 11:00:27 +0100 Subject: [PATCH 07/32] [CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices. --- CMakeLists.txt | 8 ++ contrib/cmake/cmake/msvc_legacy_quirks.cmake | 112 +++++++++++++++++++ 2 files changed, 120 insertions(+) create mode 100644 contrib/cmake/cmake/msvc_legacy_quirks.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 8afc6339b..aa347ae66 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -388,6 +388,14 @@ endif() ################################################################################ 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 ################################################################################ diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake new file mode 100644 index 000000000..050d34553 --- /dev/null +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -0,0 +1,112 @@ +# 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) From 5893aea60250c0e55475fd53326a0929a8028c8a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 12:12:54 +0100 Subject: [PATCH 08/32] [CMake] When building with MSVC and without `WARNINGS_AS_ERRORS` pass `/WX-` to MSVC. Although this is not necessary this duplicates the behaviour of the old build system. --- contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake index e49e43947..e02b28b2c 100644 --- a/contrib/cmake/cmake/compiler_warnings.cmake +++ b/contrib/cmake/cmake/compiler_warnings.cmake @@ -44,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() From c9aac0ba7787b98b3f2dd4268d252f434d3e2c1a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 12:48:49 +0100 Subject: [PATCH 09/32] [CMake] When building with MSVC try to disable incremental linking for all builds. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 31 ++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index 050d34553..9411d112b 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -110,3 +110,34 @@ endif() # 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() From 364bcde6c1daa9efa4db30cad5fc179cc304d287 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 13:28:44 +0100 Subject: [PATCH 10/32] [CMake] When building with MSVC pass the `/STACK:` argument to the linker like the old build system does. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index 9411d112b..d0ca00c83 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -118,7 +118,6 @@ z3_add_cxx_flag("/analyze-" REQUIRED) # 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) @@ -141,3 +140,12 @@ foreach (_build_type ${_build_types_as_upper}) 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}") From d032dbcbb238e9be365d9b8057190d9f3f375def Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 13:49:53 +0100 Subject: [PATCH 11/32] [CMake] When using MSVC set the `/SUBSYSTEM:` argument given to the linker. This mimics the behaviour of the old build system. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index d0ca00c83..f36a5bfb0 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -149,3 +149,13 @@ set(STACK_SIZE_MSVC_LINKER 8388608) # 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") From 2a919cf16e7d6807a76fa2806d37486c7e7e04e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 15:02:01 +0100 Subject: [PATCH 12/32] [CMake] Duplicate the remaining linker flags from the old build system. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 33 ++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index f36a5bfb0..2ca20277c 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -159,3 +159,36 @@ string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}") # 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() From 6e07d6dd2d11c7c779640f7cdb9c234875454e88 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 17:45:02 +0100 Subject: [PATCH 13/32] [CMake] Override CMake's default flags for GCC/Clang as we were doing before 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01. It's useful to be able to control the defaults and CMake's internal logic for GCC/Clang is simple enough that doing this makes sense. It would be nice to do the same for MSVC but CMake's internal logic is more complicated so for now it's better that we just use CMake's default. --- CMakeLists.txt | 1 + .../cmake/cmake/cxx_compiler_flags_overrides.cmake | 14 ++++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index aa347ae66..19c56a413 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,6 +24,7 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) "``python contrib/cmake/bootstrap.py create``") endif() +set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) ################################################################################ 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() From fa868e058efa853cceff50e4ae925a8381a91cfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 17:39:02 -0700 Subject: [PATCH 14/32] fix bound bug #991 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 100 ++++++++++++++++++++++++++++++++++++- src/smt/theory_arith.h | 1 + src/smt/theory_arith_nl.h | 38 +++++++++++--- src/test/cnf_backbones.cpp | 81 ++++++++++++++++++++++++++---- src/test/main.cpp | 14 +++++- 5 files changed, 215 insertions(+), 19 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 739a591e7..bc28221a9 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; @@ -3307,7 +3405,7 @@ namespace sat { propagate(false); ++num_resolves; } - if (scope_lvl() == 1) { + if (false && scope_lvl() == 1) { break; } } 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_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/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++; } } From 3152833893ece622174d1b8e6fab443da1e409cf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 18:55:47 -0700 Subject: [PATCH 15/32] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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); From b3f720c2bf0ba2326f5c1513c27c3e142683d068 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 18:58:34 -0700 Subject: [PATCH 16/32] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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) { From 4468816d3223ff8efa604388c5967e34cf7fe354 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 19:00:15 -0700 Subject: [PATCH 17/32] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context_inv.cpp | 1 - 1 file changed, 1 deletion(-) 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); From 2c208e1d1002c25593ad2e1a637fdfe96628fda3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 10:23:00 -0700 Subject: [PATCH 18/32] Sat update Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 739a591e7..cd13ac7a4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3291,6 +3291,9 @@ namespace sat { literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; + if (value(lit) == l_true && lvl(lit) == 1) { + VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq)); + } continue; } push(); From bd1b930d7a1735da6de575a4c57784f720690c8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 11:00:03 -0700 Subject: [PATCH 19/32] swap argument order of chunk with file Signed-off-by: Nikolaj Bjorner --- src/test/cnf_backbones.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index 3387e1a8e..c34e109d3 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -271,9 +271,9 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { void tst_cnf_backbones(char ** argv, int argc, int& i) { if (i + 1 < argc) { - bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk")); + bool use_chunk = (i + 2 < argc && argv[i + 1] == std::string("chunk")); + if (use_chunk) ++i; cnf_backbones(use_chunk, argv[i + 1]); ++i; - if (use_chunk) ++i; } } From aff02ca9056f299b0b460d408e1425e4dec050f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 11:26:54 -0700 Subject: [PATCH 20/32] include 'stopwatch.h' to avoid ODR warnings, #994 --- src/muz/base/dl_util.h | 1 + src/muz/rel/dl_instruction.h | 1 - src/sat/sat_solver.cpp | 18 ++++++++++++++++-- src/sat/sat_solver.h | 1 + 4 files changed, 18 insertions(+), 3 deletions(-) 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/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bc28221a9..c80b75ba6 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3500,7 +3500,13 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { } bool solver::check_domain(literal lit, literal lit2) { - return m_antecedents.contains(lit2.var()); + if (!m_antecedents.contains(lit2.var())) { + m_todo_antecedents.push_back(lit2); + return false; + } + else { + return true; + } } bool solver::extract_assumptions(literal lit, index_set& s) { @@ -3565,8 +3571,16 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { s.insert(lit.index()); } else { + SASSERT(m_todo_antecedents.empty()); if (!extract_assumptions(lit, s)) { - return false; + SASSERT(!m_todo_antecedents.empty()); + while (!m_todo_antecedents.empty()) { + index_set s1; + if (extract_assumptions(m_todo_antecedents.back(), s1)) { + m_todo_antecedents.pop_back(); + } + } + VERIFY (extract_assumptions(lit, s)); } add_assumption(lit); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c7f472a60..091162f23 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); From 86f3526110de9ca8c4d92696744c07d9dbad4e72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 11:48:06 -0700 Subject: [PATCH 21/32] update get-value to also respect parameter model_index, #955 Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index d2b55af1d..b7f33d333 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2218,11 +2218,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") { + 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(); From 0693a413b6dc9facb8ae9ee484dc7d85d4fe89ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 12:50:56 -0700 Subject: [PATCH 22/32] augment #955 to handle hyphen Signed-off-by: Nikolaj Bjorner --- src/parsers/smt2/smt2parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index b7f33d333..8e72e50db 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2219,7 +2219,7 @@ namespace smt2 { throw cmd_exception("invalid get-value command, empty list of terms"); next(); unsigned index = 0; - if (curr_is_keyword() && curr_id() == ":model_index") { + 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()) From aceee3fac8912629e0d1e3568bb0788f184138d6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Apr 2017 12:54:29 -0700 Subject: [PATCH 23/32] renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. #994 Signed-off-by: Nikolaj Bjorner --- src/shell/opt_frontend.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) 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(); From f655e1976eca91d1aaa06d1551367910e63ec03c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:18:38 -0400 Subject: [PATCH 24/32] add params for theory case split --- src/smt/params/smt_params.cpp | 3 ++- src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + 3 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 8a9188e2b..4b7920596 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -31,6 +31,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_restart_strategy = static_cast(p.restart_strategy()); m_restart_factor = p.restart_factor(); m_case_split_strategy = static_cast(p.case_split()); + m_theory_case_split = p.theory_case_split(); m_delay_units = p.delay_units(); m_delay_units_threshold = p.delay_units_threshold(); m_preprocess = _p.get_bool("preprocess", true); // hidden parameter @@ -155,4 +156,4 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_check_at_labels); DISPLAY_PARAM(m_dump_goal_as_smt); DISPLAY_PARAM(m_auto_config); -} \ No newline at end of file +} diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 366570365..c03eaeaef 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -109,6 +109,7 @@ struct smt_params : public preprocessor_params, case_split_strategy m_case_split_strategy; unsigned m_rel_case_split_order; bool m_lookahead_diseq; + bool m_theory_case_split; // ----------------------------------- // diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 6ac4aab04..faa48400d 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -61,6 +61,7 @@ def_module_params(module_name='smt', ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), + ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.'), ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), From 2f56d128b0531829d8354c52d1059e368747c33e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:34:43 -0400 Subject: [PATCH 25/32] add theory case split support to smt_context --- src/smt/smt_context.cpp | 123 ++++++++++++++++++++++++++++++++++++++++ src/smt/smt_context.h | 25 ++++++++ 2 files changed, 148 insertions(+) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6a3c036ca..af1e94e62 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -62,6 +62,7 @@ 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), @@ -339,6 +340,7 @@ 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; @@ -1768,6 +1770,8 @@ namespace smt { unsigned qhead = m_qhead; if (!bcp()) return false; + if (!propagate_th_case_split()) + return false; if (get_cancel_flag()) { m_qhead = qhead; return true; @@ -2960,6 +2964,125 @@ namespace smt { assert_expr_core(e, pr); } + class case_split_insert_trail : public trail { + literal l; + public: + case_split_insert_trail(literal l): + l(l) { + } + virtual void undo(context & ctx) { + ctx.undo_th_case_split(l); + } + }; + + void context::mk_th_case_split(unsigned num_lits, literal * lits) { + 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. + 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); + } + } + } else { + literal_vector new_case_split; + for (unsigned i = 0; i < num_lits; ++i) { + literal l = lits[i]; + 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)); + new_case_split.push_back(l); + } + m_th_case_split_sets.push_back(new_case_split); + push_trail(push_back_vector >(m_th_case_split_sets)); + for (unsigned i = 0; i < num_lits; ++i) { + literal l = lits[i]; + if (!m_literal2casesplitsets.contains(l.index())) { + m_literal2casesplitsets.insert(l.index(), vector()); + } + 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; + ); + } + } + + void context::undo_th_case_split(literal l) { + m_all_th_case_split_literals.remove(l.index()); + if (m_literal2casesplitsets.contains(l.index())) { + if (!m_literal2casesplitsets[l.index()].empty()) { + m_literal2casesplitsets[l.index()].pop_back(); + } + } + } + + bool context::propagate_th_case_split() { + if (m_all_th_case_split_literals.empty()) + return true; + + // iterate over all literals assigned since the last time this method was called, + // 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]; + 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; + 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 we get here without detecting a conflict, we're fine + return true; + } + bool context::reduce_assertions() { if (!m_asserted_formulas.inconsistent()) { SASSERT(at_base_level()); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b3cfb4639..d9817236e 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -226,6 +226,16 @@ namespace smt { literal2assumption m_literal2assumption; // maps an expression associated with a literal to the original assumption expr_ref_vector m_unsat_core; + // ----------------------------------- + // + // Theory case split + // + // ----------------------------------- + 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; + // ----------------------------------- // // Accessors @@ -820,6 +830,21 @@ namespace smt { void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = 0); + /* + * Provide a hint to the core solver that the specified literals form a "theory case split". + * The core solver will enforce the condition that exactly one of these literals can be + * assigned 'true' at any time. + * We assume that the theory solver has already asserted the disjunction of these literals + * or some other axiom that means at least one of them must be assigned 'true'. + */ + void mk_th_case_split(unsigned num_lits, literal * lits); + + public: + + // helper function for trail + void undo_th_case_split(literal l); + + bool propagate_th_case_split(); bool_var mk_bool_var(expr * n); From 3bce61e0d432261ae173ac77659c773aa148940e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 10:43:33 -0400 Subject: [PATCH 26/32] fix warning --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index af1e94e62..9a841ea26 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -62,7 +62,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), @@ -75,6 +74,7 @@ namespace smt { m_unsat_proof(m), m_unknown("unknown"), m_unsat_core(m), + m_th_case_split_qhead(0), #ifdef Z3DEBUG m_trail_enabled(true), #endif From d14f2af5ae5844d62be2a4408ffb22ef948e02d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 May 2017 15:22:06 -0700 Subject: [PATCH 27/32] deal with subtraction that manages to sneak in. Issue #996 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifier/poly_simplifier_plugin.h | 2 +- src/cmd_context/check_logic.cpp | 1 + src/sat/sat_solver.cpp | 81 ++++++++++++--------- src/sat/sat_solver.h | 6 +- src/smt/theory_bv.cpp | 16 ++++ src/smt/theory_bv.h | 1 + src/tactic/portfolio/enum2bv_solver.cpp | 6 +- src/test/cnf_backbones.cpp | 18 +++-- 8 files changed, 84 insertions(+), 47 deletions(-) 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/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d6b39c394..22418ed28 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3180,7 +3180,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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)); + 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";); @@ -3259,9 +3259,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { } } - // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); + is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); - is_sat = get_consequences(asms, lits, conseq); + // is_sat = get_consequences(asms, lits, conseq); set_model(mdl); return is_sat; } @@ -3371,13 +3371,14 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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(); @@ -3389,8 +3390,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { literal lit = *it; if (value(lit) != l_undef) { ++num_fixed; - if (value(lit) == l_true && lvl(lit) == 1) { - VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq)); + if (lvl(lit) <= 1) { + SASSERT(value(lit) == l_true); + extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq); } continue; } @@ -3409,18 +3411,13 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { ++num_resolves; } 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";); @@ -3431,6 +3428,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { if (is_sat == l_undef) { restart(); } + extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); } } if (is_sat == l_false) { @@ -3440,7 +3438,6 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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 @@ -3492,19 +3489,27 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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) { 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 { @@ -3514,16 +3519,17 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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; @@ -3531,7 +3537,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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()); } } @@ -3565,7 +3571,7 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { } - 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; @@ -3574,16 +3580,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { s.insert(lit.index()); } else { - SASSERT(m_todo_antecedents.empty()); if (!extract_assumptions(lit, s)) { SASSERT(!m_todo_antecedents.empty()); - while (!m_todo_antecedents.empty()) { - index_set s1; - if (extract_assumptions(m_todo_antecedents.back(), s1)) { - m_todo_antecedents.pop_back(); - } - } - VERIFY (extract_assumptions(lit, s)); + return false; } add_assumption(lit); } @@ -3601,6 +3600,16 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { 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 091162f23..a26abe1e0 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -498,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/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/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 c34e109d3..b95977a46 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -152,14 +152,13 @@ static void brute_force_consequences(sat::solver& s, sat::literal_vector const& 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; } 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";); @@ -270,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 + 1] == std::string("chunk")); - if (use_chunk) ++i; - cnf_backbones(use_chunk, argv[i + 1]); - ++i; + file = argv[i + 1]; } + else { + file = argv[1]; + } + cnf_backbones(use_chunk, file); + ++i; } From b86d472eaf5767cc2d870a08d0c22b70b2262f47 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 18:22:49 -0400 Subject: [PATCH 28/32] simplify theory case split handling --- src/smt/smt_context.cpp | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9a841ea26..af45f0fcc 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3057,19 +3057,8 @@ namespace smt { 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; - 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; - } + 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; From f9105edb14c6d6aca605bc61ce206c57f95a28f4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 May 2017 15:22:52 -0700 Subject: [PATCH 29/32] revert to native chunker Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 22418ed28..dc5aa2964 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3259,9 +3259,9 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { } } - is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); + // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); - // is_sat = get_consequences(asms, lits, conseq); + is_sat = get_consequences(asms, lits, conseq); set_model(mdl); return is_sat; } From 16a5e944d78aae384f2acb17e1bd60c6499f965e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 1 May 2017 18:25:54 -0400 Subject: [PATCH 30/32] use reference for case split sets --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index af45f0fcc..602ff5160 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3045,7 +3045,7 @@ namespace smt { 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()); + 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 { "; From 8ba78081ecc8057eb03d8447e9778157d9d20bba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 May 2017 16:41:17 -0700 Subject: [PATCH 31/32] fix build break Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 602ff5160..03eb38043 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3045,7 +3045,7 @@ namespace smt { 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()); + 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 { "; From 48e37b0e160313a58fe946d84baa7445bb721a06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 May 2017 16:54:22 -0700 Subject: [PATCH 32/32] pass qhead Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 73 +++++++++++++++++++---------------------- src/smt/smt_context.h | 3 +- 2 files changed, 35 insertions(+), 41 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 03eb38043..abac9ef82 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -74,7 +74,6 @@ namespace smt { m_unsat_proof(m), m_unknown("unknown"), m_unsat_core(m), - m_th_case_split_qhead(0), #ifdef Z3DEBUG m_trail_enabled(true), #endif @@ -340,7 +339,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; @@ -1770,7 +1768,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; @@ -2979,16 +2977,13 @@ 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 { @@ -3010,11 +3005,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; + ); } } @@ -3027,7 +3022,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; @@ -3035,34 +3030,34 @@ 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 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; - } + 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 d9817236e..ca2429be8 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; // ----------------------------------- // @@ -844,7 +843,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);