merge with master

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

CMakeLists.txt

@@ -24,9 +24,8 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt"))
           "``python contrib/cmake/bootstrap.py create``")
 endif()
 
-# This overrides the default flags for the different CMAKE_BUILD_TYPEs
+set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake")
+project(Z3 CXX)
-project(Z3 C CXX)
 
 ################################################################################
 # Project version
@@ -155,13 +154,13 @@ set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "")
 # Build type
 ################################################################################
 message(STATUS "CMake generator: ${CMAKE_GENERATOR}")
+set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
 if (DEFINED CMAKE_CONFIGURATION_TYPES)
   # Multi-configuration build (e.g. Visual Studio and Xcode). Here
   # CMAKE_BUILD_TYPE doesn't matter
   message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}")
 else()
   # Single configuration generator (e.g. Unix Makefiles, Ninja)
-  set(available_build_types Debug Release RelWithDebInfo MinSizeRel)
   if(NOT CMAKE_BUILD_TYPE)
     message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default")
     message(STATUS "The available build types are: ${available_build_types}")
@@ -326,6 +325,15 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
   unset(SSE_FLAGS)
 endif()
 
+# FIXME: Remove "x.." when CMP0054 is set to NEW
+if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  # This is the default for MSVC already but to replicate the
+  # python/Makefile build system behaviour this flag is set
+  # explicitly.
+  z3_add_cxx_flag("/fp:precise" REQUIRED)
+endif()
+# There doesn't seem to be an equivalent for clang/gcc
+
 ################################################################################
 # Threading support
 ################################################################################
@@ -376,6 +384,41 @@ if (BUILD_LIBZ3_SHARED)
   endif()
 endif()
 
+################################################################################
+# Link time optimization
+################################################################################
+include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake)
+
+################################################################################
+# MSVC specific flags inherited from old build system
+################################################################################
+# FIXME: Remove "x.." when CMP0054 is set to NEW
+if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
+endif()
+
+################################################################################
+# Report default CMake flags
+################################################################################
+# This is mainly for debugging.
+message(STATUS "CMAKE_CXX_FLAGS: \"${CMAKE_CXX_FLAGS}\"")
+message(STATUS "CMAKE_EXE_LINKER_FLAGS: \"${CMAKE_EXE_LINKER_FLAGS}\"")
+message(STATUS "CMAKE_STATIC_LINKER_FLAGS: \"${CMAKE_STATIC_LINKER_FLAGS}\"")
+message(STATUS "CMAKE_SHARED_LINKER_FLAGS: \"${CMAKE_SHARED_LINKER_FLAGS}\"")
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi configuration generator
+  string(TOUPPER "${available_build_types}" build_types_to_report)
+else()
+  # Single configuration generator
+  string(TOUPPER "${CMAKE_BUILD_TYPE}" build_types_to_report)
+endif()
+foreach (_build_type ${build_types_to_report})
+  message(STATUS "CMAKE_CXX_FLAGS_${_build_type}: \"${CMAKE_CXX_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_EXE_LINKER_FLAGS_${_build_type}: \"${CMAKE_EXE_LINKER_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_SHARED_LINKER_FLAGS_${_build_type}: \"${CMAKE_SHARED_LINKER_FLAGS_${_build_type}}\"")
+  message(STATUS "CMAKE_STATIC_LINKER_FLAGS_${_build_type}: \"${CMAKE_STATIC_LINKER_FLAGS_${_build_type}}\"")
+endforeach()
+
 ################################################################################
 # Report Z3_COMPONENT flags
 ################################################################################

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.
 

contrib/cmake/cmake/compiler_flags_override.cmake

@@ -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)

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 `$<$<CONFIG:Release>:${_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()

contrib/cmake/cmake/compiler_warnings.cmake

@@ -15,6 +15,13 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
   # FIXME: Remove "x.." when CMP0054 is set to NEW
 elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
   list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
+
+  # CMake's default flags include /W3 already so remove them if
+  # they already exist.
+  if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3")
+    string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}")
+    set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE)
+  endif()
 else()
   message(AUTHOR_WARNING "Unknown compiler")
 endif()
@@ -37,4 +44,11 @@ if (WARNINGS_AS_ERRORS)
   message(STATUS "Treating compiler warnings as errors")
 else()
   message(STATUS "Not treating compiler warnings as errors")
+  # FIXME: Remove "x.." when CMP0054 is set to NEW
+  if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+    # Warnings as errors is off by default for MSVC so setting this
+    # is not necessary but this duplicates the behaviour of the old
+    # build system.
+    list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-")
+  endif()
 endif()

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()

contrib/cmake/cmake/msvc_legacy_quirks.cmake

@@ -0,0 +1,194 @@
+# This file ether sets or notes various compiler and linker flags for MSVC that
+# were defined by the old python/Makefile based build system but
+# don't obviously belong in the other sections in the CMake build system.
+
+################################################################################
+# Compiler definitions
+################################################################################
+# FIXME: All the commented out defines should be removed once
+# we are confident it is correct to not set them.
+set(Z3_MSVC_LEGACY_DEFINES
+  # Don't set `_DEBUG`. The old build sytem sets this but this
+  # is wrong. MSVC will set this depending on which runtime is being used.
+  # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx
+  # _DEBUG
+
+  # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release.
+  # That seems completly wrong so set it for all configurations.
+  # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/
+  # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files.
+  # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx
+  UNICODE
+  _UNICODE
+)
+
+if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  list(APPEND Z3_MSVC_LEGACY_DEFINES ""
+    # Don't set `_LIB`. The old build system sets this for x86_64 release
+    # build. This flag doesn't seem to be documented but a stackoverflow
+    # post hints that this is usually set when building a static library.
+    # See http://stackoverflow.com/questions/35034683/how-to-tell-if-current-project-is-dll-or-static-lib
+    # This seems wrong give that the old build system set this regardless
+    # whether or not libz3 was static or shared so its probably best
+    # to not set for now.
+    #$<$<CONFIG:Release>:_LIB>
+    #$<$<CONFIG:RelWithDebInfo>:_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.
+    #$<$<CONFIG:Debug:_CONSOLE>
+    #$<$<CONFIG:MinSizeRel:_CONSOLE>
+
+    # 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.
+    #$<$<CONFIG:Release>:ASYNC_COMMANDS>
+    #$<$<CONFIG:RelWithDebInfo>: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
+    $<$<CONFIG:Debug>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
+    $<$<CONFIG:MinSizeRel>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
+  )
+else()
+  list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG})
+endif()
+
+if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686"))
+  # Use __cdecl calling convention. Apparently this is MSVC's default
+  # but the old build system set it so for completeness set it too.
+  # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx
+  z3_add_cxx_flag("/Gd" REQUIRED)
+endif()
+
+# FIXME: The old build system explicitly disables code analysis.
+# I don't know why. Duplicate this behaviour for now.
+# See https://msdn.microsoft.com/en-us/library/ms173498.aspx
+z3_add_cxx_flag("/analyze-" REQUIRED)
+
+################################################################################
+# Linker flags
+################################################################################
+
+# By default CMake enables incremental linking for Debug and RelWithDebInfo
+# builds. The old build sytem disables it for all builds so try to do the same
+# by changing all configurations if necessary
+string(TOUPPER "${available_build_types}" _build_types_as_upper)
+foreach (_build_type ${_build_types_as_upper})
+  foreach (t EXE SHARED STATIC)
+    set(_replacement "/INCREMENTAL:NO")
+    # Remove any existing incremental flags
+    string(REGEX REPLACE
+      "/INCREMENTAL:YES"
+      "${_replacement}"
+      _replaced_linker_flags
+      "${CMAKE_${t}_LINKER_FLAGS_${_build_type}}")
+    string(REGEX REPLACE
+      "(/INCREMENTAL$)|(/INCREMENTAL )"
+      "${_replacement} "
+      _replaced_linker_flags
+      "${_replaced_linker_flags}")
+    if (NOT "${_replaced_linker_flags}" MATCHES "${_replacement}")
+      # Flag not present. Add it
+      string(APPEND _replaced_linker_flags " ${_replacement}")
+    endif()
+    set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}")
+  endforeach()
+endforeach()
+
+# The original build system passes `/STACK:` to the linker.
+# This size comes from the original build system.
+# FIXME: What is the rationale behind this?
+set(STACK_SIZE_MSVC_LINKER 8388608)
+# MSVC documentation (https://msdn.microsoft.com/en-us/library/35yc2tc3.aspx)
+# says this only matters for executables which is why this is not being
+# set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS.
+string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}")
+
+# The original build system passes `/SUBSYSTEM:<X>` to the linker where `<X>`
+# depends on what is being linked. Where `<X>` is `CONSOLE` for executables
+# and `WINDOWS` for shard libraries.
+# We don't need to pass `/SUBSYSTEM:CONSOLE` because CMake will do this for
+# us when building executables because we don't pass the `WIN32` argument to
+# `add_executable()`.
+# FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx
+# suggests that `/SUBSYSTEM:` only matters for executables.
+string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS")
+
+# FIXME: The following linker flags are weird. They are set in all configurations
+# in the old build system except release x86_64. We try to emulate this here but
+# this is likely the wrong thing to do.
+foreach (_build_type ${_build_types_as_upper})
+  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND
+      ("${_build_type}" STREQUAL "RELEASE" OR
+      "${_build_type}"  STREQUAL "RELWITHDEBINFO")
+      )
+    message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}")
+  else()
+    # Linker optimizations.
+    # See https://msdn.microsoft.com/en-us/library/bxwfs976.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # See https://msdn.microsoft.com/en-us/library/b1kw34cb.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /TLBID:1")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /TLBID:1")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # Address space layout randomization
+    # See https://msdn.microsoft.com/en-us/library/bb384887.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /DYNAMICBASE")
+    string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO")
+
+    # FIXME: This is not necessary. This is MSVC's default.
+    # Indicate that the executable is compatible with DEP
+    # See https://msdn.microsoft.com/en-us/library/ms235442.aspx
+    string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT")
+  endif()
+endforeach()

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})

contrib/cmake/doc/CMakeLists.txt

@@ -67,7 +67,6 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
   ${JAVA_API_OPTIONS}
   DEPENDS
     ${DOC_EXTRA_DEPENDS}
-  BYPRODUCTS "${DOC_DEST_DIR}"
   COMMENT "Generating documentation"
   ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG}
 )

contrib/cmake/src/smt/CMakeLists.txt

@@ -58,6 +58,7 @@ z3_add_component(smt
     theory_opt.cpp
     theory_pb.cpp
     theory_seq.cpp
+    theory_str.cpp
     theory_utvpi.cpp
     theory_wmaxsat.cpp
     uses_theory.cpp

contrib/cmake/src/smt/params/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(smt_params
     theory_array_params.cpp
     theory_bv_params.cpp
     theory_pb_params.cpp
+    theory_str_params.cpp
   COMPONENT_DEPENDENCIES
     ast
     bit_blaster

doc/mk_api_doc.py

@@ -103,15 +103,17 @@ def parse_options():
     TEMP_DIR = pargs.temp_dir
     OUTPUT_DIRECTORY = pargs.output_dir
     Z3PY_PACKAGE_PATH = pargs.z3py_package_path
-    if not os.path.exists(Z3PY_PACKAGE_PATH):
-        raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH))
-    if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3':
-        raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH))
     Z3PY_ENABLED = not pargs.no_z3py
     DOTNET_ENABLED = not pargs.no_dotnet
     JAVA_ENABLED = not pargs.no_java
     DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths
     JAVA_API_SEARCH_PATHS = pargs.java_search_paths
+
+    if Z3PY_ENABLED:
+        if not os.path.exists(Z3PY_PACKAGE_PATH):
+            raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH))
+        if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3':
+            raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH))
     return
 
 def mk_dir(d):

scripts/mk_util.py

@@ -1633,6 +1633,8 @@ class DotNetDLLComponent(Component):
 
         if not self.key_file is None:
             print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
+            if (self.key_file.find(' ') != -1):
+                self.key_file = '"' + self.key_file + '"'
             cscCmdLine.append('/keyfile:{}'.format(self.key_file))
 
         cscCmdLine.extend( ['/unsafe+',
@@ -2419,6 +2421,7 @@ def mk_config():
                 FOCI2 = False
         if GIT_HASH:
             CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
+        CXXFLAGS = '%s -std=c++11' % CXXFLAGS
         CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
         FPMATH = test_fpmath(CXX)
         CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS)

src/ast/ast.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<cstring>
 #include"ast.h"
 #include"ast_pp.h"
 #include"ast_ll_pp.h"

src/ast/ast.h

@@ -117,6 +117,9 @@ public:
     explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
     explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
     explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
+    explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
+        new (m_symbol) symbol(s);
+    }
     explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
     parameter(parameter const&);
 

src/ast/rewriter/rewriter.txt

@@ -7,6 +7,7 @@ The following classes implement theory specific rewriting rules:
   - array_rewriter
   - datatype_rewriter
   - fpa_rewriter
+  - seq_rewriter
 
 Each of them provide the method
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)

src/ast/rewriter/seq_rewriter.cpp

@@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     switch(f->get_decl_kind()) {
 
     case OP_SEQ_UNIT:
-        return BR_FAILED;
+        SASSERT(num_args == 1);
+        return mk_seq_unit(args[0], result);
     case OP_SEQ_EMPTY:
         return BR_FAILED;
     case OP_RE_PLUS:
@@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         return mk_re_union(args[0], args[1], result);
     case OP_RE_RANGE:
-        return BR_FAILED;    
+        SASSERT(num_args == 2);
+        return mk_re_range(args[0], args[1], result);
     case OP_RE_INTERSECT:
         SASSERT(num_args == 2);
         return mk_re_inter(args[0], args[1], result);
@@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     return BR_FAILED;
 }
 
+/*
+ * (seq.unit (_ BitVector 8)) ==> String constant
+ */
+br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
+    sort * s = m().get_sort(e);
+    bv_util bvu(m());
+
+    if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) {
+        // specifically we want (_ BitVector 8)
+        rational n_val;
+        unsigned int n_size;
+        if (bvu.is_numeral(e, n_val, n_size)) {
+            if (n_size == 8) {
+                // convert to string constant
+                char ch = (char)n_val.get_int32();
+                TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;);
+                char s_tmp[2] = {ch, '\0'};
+                symbol s(s_tmp);
+                result = m_util.str.mk_string(s);
+                return BR_DONE;
+            }
+        }
+    }
+
+    return BR_FAILED;
+}
+
 /*
    string + string = string
    a + (b + c) = (a + b) + c
@@ -1401,6 +1430,40 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+/*
+ * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
+ */
+br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
+    return BR_FAILED;
+    TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
+    zstring str_lo, str_hi;
+    if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {
+        if (str_lo.length() == 1 && str_hi.length() == 1) {
+            unsigned int c1 = str_lo[0];
+            unsigned int c2 = str_hi[0];
+            if (c1 > c2) {
+                // exchange c1 and c2
+                unsigned int tmp = c1;
+                c2 = c1;
+                c1 = tmp;
+            }
+            zstring s(c1);
+            expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m());
+            for (unsigned int ch = c1 + 1; ch <= c2; ++ch) {
+                zstring s_ch(ch);
+                expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m());
+                acc = m_util.re.mk_union(acc, acc2);
+            }
+            result = acc;
+            return BR_REWRITE2;
+        } else {
+            m().raise_exception("string constants in re.range must have length 1");
+        }
+    }
+
+    return BR_FAILED;
+}
+
 /*
    emp+ = emp
    all+ = all
@@ -1430,9 +1493,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
         return BR_DONE;
     }
 
-    return BR_FAILED;
+    //return BR_FAILED;
-//  result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
+    result = m_util.re.mk_concat(a, m_util.re.mk_star(a));
-//  return BR_REWRITE2;
+    return BR_REWRITE2;
 }
 
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {

src/ast/rewriter/seq_rewriter.h

@@ -98,6 +98,7 @@ class seq_rewriter {
     re2automaton   m_re2aut;
     expr_ref_vector m_es, m_lhs, m_rhs;
 
+    br_status mk_seq_unit(expr* e, expr_ref& result);
     br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_seq_length(expr* a, expr_ref& result);
     br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
@@ -119,6 +120,7 @@ class seq_rewriter {
     br_status mk_re_plus(expr* a, expr_ref& result);
     br_status mk_re_opt(expr* a, expr_ref& result);
     br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
+    br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
 
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 

src/ast/seq_decl_plugin.cpp

@@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     init();
     sort_names.push_back(builtin_name("Seq",   SEQ_SORT));
     sort_names.push_back(builtin_name("RegEx", RE_SORT));
+    // SMT-LIB 2.5 compatibility
     sort_names.push_back(builtin_name("String", _STRING_SORT));
+    sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
 }
 
 app* seq_decl_plugin::mk_string(symbol const& s) {

src/ast/seq_decl_plugin.h

@@ -273,6 +273,15 @@ public:
         bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
 
+        bool is_string_term(expr const * n) const {
+            sort * s = get_sort(n);
+            return u.is_string(s);
+        }
+
+        bool is_non_string_sequence(expr const * n) const {
+            sort * s = get_sort(n);
+            return (u.is_seq(s) && !u.is_string(s));
+        }
 
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);

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<expr> & result);

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);

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;

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;

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<family_id>::iterator it  = fids.begin();
         svector<family_id>::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");

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;}

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 {

src/muz/rel/dl_instruction.h

@@ -30,7 +30,6 @@ Revision History:
 
 namespace datalog {
 
-    class execution_context;
     class instruction_block;
     class rel_context;
 

src/opt/wmax.cpp

@@ -61,13 +61,12 @@ namespace opt {
                 return is_sat;
             }
             m_upper = m_lower;
-            bool was_sat = false;
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
 
             obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
             for (; it != end; ++it) {
-                expr* c = assert_weighted(wth(), it->m_key, it->m_value);
+                assert_weighted(wth(), it->m_key, it->m_value);
                 if (!is_true(it->m_key)) {
                     m_upper += it->m_value;
                 }
@@ -97,7 +96,6 @@ namespace opt {
                     expr_ref fml = wth().mk_block();
                     //DEBUG_CODE(verify_cores(cores););
                     s().assert_expr(fml);
-                    was_sat = true;
                 }
                 else {
                     //DEBUG_CODE(verify_cores(cores););

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" || 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;
+            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();

src/sat/sat_solver.cpp

@@ -3202,6 +3202,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;
+            }
+        }
+        UNREACHABLE();
+    }
+
+    static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector<sat::literal_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<sat::literal_vector>& conseq, unsigned K) {
+        sat::literal_vector lambda;
+        for (unsigned i = 0; i < vars.size(); i++) {
+            lambda.push_back(sat::literal(vars[i], m[vars[i]] == l_false));
+        }
+        while (!lambda.empty()) {
+            IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";);
+            unsigned k = std::min(K, lambda.size());
+            sat::literal_vector gamma, omegaN;
+            for (unsigned i = 0; i < k; ++i) {
+                sat::literal l = lambda[lambda.size() - i - 1];
+                gamma.push_back(l);
+                omegaN.push_back(~l);
+            }
+            while (true) {
+                sat::literal_vector asms1(asms);
+                asms1.append(omegaN);
+                lbool r = s.check(asms1.size(), asms1.c_ptr());
+                if (r == l_true) {
+                    IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";);
+                    prune_unfixed(lambda, s.get_model());
+                    break;
+                }
+                sat::literal_vector const& core = s.get_core();
+                sat::literal_vector occurs;
+                IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";);
+                for (unsigned i = 0; i < omegaN.size(); ++i) {
+                    if (core.contains(omegaN[i])) {
+                        occurs.push_back(omegaN[i]);
+                    }
+                }
+                if (occurs.size() == 1) {
+                    sat::literal lit = occurs.back();
+                    sat::literal nlit = ~lit;
+                    conseq.push_back(core);
+                    back_remove(lambda, ~lit);
+                    back_remove(gamma, ~lit);
+                    s.mk_clause(1, &nlit);
+                }
+                for (unsigned i = 0; i < omegaN.size(); ++i) {
+                    if (occurs.contains(omegaN[i])) {
+                        omegaN[i] = omegaN.back();
+                        omegaN.pop_back();
+                        --i;
+                    }
+                }
+                if (omegaN.empty() && occurs.size() > 1) {
+                    brute_force_consequences(s, asms, gamma, conseq);
+                    for (unsigned i = 0; i < gamma.size(); ++i) {
+                        back_remove(lambda, gamma[i]);
+                    }
+                    break;
+                }
+            }
+        }
+        return l_true;
+    }
+
+
     lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
         literal_vector lits;
         lbool is_sat = l_true;
@@ -3224,7 +3319,13 @@ namespace sat {
             default: break;
             }
         }
+
+        if (false && asms.empty()) {
+            is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100);
+        }
+        else {
             is_sat = get_consequences(asms, lits, conseq);
+        }
         set_model(mdl);
         return is_sat;
     }
@@ -3335,13 +3436,14 @@ namespace sat {
         if (check_inconsistent()) return l_false;
         SASSERT(search_lvl() == 1);
 
-        unsigned num_units = 0, num_iterations = 0;
+        unsigned num_iterations = 0;
-        extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
+        extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq); 
         update_unfixed_literals(unfixed_lits, unfixed_vars);
         while (!unfixed_lits.empty()) {
             if (scope_lvl() > search_lvl()) {
                 pop(scope_lvl() - search_lvl());
             }
+            propagate(false);
             ++num_iterations;
             checkpoint();
             literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
@@ -3353,6 +3455,9 @@ namespace sat {
                 literal lit = *it;                
                 if (value(lit) != l_undef) {
                     ++num_fixed;
+                    if (lvl(lit) <= 1 && value(lit) == l_true) {
+                        extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
+                    }
                     continue;
                 }
                 push();
@@ -3369,19 +3474,14 @@ namespace sat {
                     propagate(false);
                     ++num_resolves;
                 }
-                if (scope_lvl() == search_lvl()) { 
+                if (false && scope_lvl() == search_lvl()) {
+                    is_sat = l_undef;
                     break;
                 }
             }
-            if (scope_lvl() == 1) {
+
-                it = unfixed_lits.begin();
+            extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
-                for (; it != end; ++it) {
+
-                    literal lit = *it;
-                    if (value(lit) == l_true) {
-                        VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
-                    }
-                }
-            }
             if (is_sat == l_true) {
                 if (scope_lvl() == search_lvl() && num_resolves > 0) {
                     IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
@@ -3392,6 +3492,7 @@ namespace sat {
                     if (is_sat == l_undef) {
                         restart();
                     }
+                    extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
                 }
             }
             if (is_sat == l_false) {
@@ -3401,7 +3502,6 @@ namespace sat {
             if (is_sat == l_true) {
                 delete_unfixed(unfixed_lits, unfixed_vars);
             }
-            extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); 
             update_unfixed_literals(unfixed_lits, unfixed_vars);
             IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
                        << " iterations: " << num_iterations
@@ -3453,32 +3553,49 @@ namespace sat {
         SASSERT(!inconsistent());
         unsigned sz = m_trail.size();
         for (unsigned i = start; i < sz && lvl(m_trail[i]) <= 1; ++i) {
-            if (!extract_fixed_consequences(m_trail[i], assumptions, unfixed, conseq)) {
+            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;
-            }
         }
         start = sz;
     }
 
+    void solver::extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed_vars, vector<literal_vector>& conseq) {
+        literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
+        for (; it != end; ++it) {
+            literal lit = *it;
+            TRACE("sat", tout << "extract: " << lit << " " << value(lit) << " " << lvl(lit) << "\n";);
+
+            if (lvl(lit) <= 1 && value(lit) == l_true) {
+                extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq);
+            }
+        }
+    }
+
     bool solver::check_domain(literal lit, literal lit2) {
-        return m_antecedents.contains(lit2.var());
+        if (!m_antecedents.contains(lit2.var())) {
+            SASSERT(value(lit2) == l_true);
+            SASSERT(m_todo_antecedents.empty() || m_todo_antecedents.back() != lit2);
+            m_todo_antecedents.push_back(lit2);
+            return false;
+        }
+        else {
+            return true;
+        }
     }
 
     bool solver::extract_assumptions(literal lit, index_set& s) {
         justification js = m_justification[lit.var()];
+        TRACE("sat", tout << lit << " " << js << "\n";);
+        bool all_found = true;
         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_literal1()) ||
-            if (!check_domain(lit, js.get_literal2())) return false;
+                !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;
@@ -3486,9 +3603,13 @@ namespace sat {
             clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
             for (unsigned i = 0; i < c.size(); ++i) {
                 if (c[i] != lit) {
-                    if (!check_domain(lit, c[i])) return false;
+                    if (check_domain(lit, ~c[i]) && all_found) {
                         s |= m_antecedents.find(c[i].var());
                     }
+                    else {
+                        all_found = false;
+                    }
+                }
             }
             break;
         }
@@ -3497,9 +3618,13 @@ namespace sat {
             literal_vector::iterator it  = m_ext_antecedents.begin();
             literal_vector::iterator end = m_ext_antecedents.end();
             for (; it != end; ++it) {
-                if (!check_domain(lit, *it)) return false;
+                if (check_domain(lit, *it) && all_found) {
                     s |= m_antecedents.find(it->var());
                 }
+                else {
+                    all_found = false;
+                }
+            }
             break;
         }
         default:
@@ -3507,7 +3632,7 @@ namespace sat {
             break;
         }
         TRACE("sat", display_index_set(tout << lit << ": " , s) << "\n";);
-        return true;
+        return all_found;
     }
 
     std::ostream& solver::display_index_set(std::ostream& out, index_set const& s) const {
@@ -3520,7 +3645,7 @@ namespace sat {
     }
 
 
-    bool solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
+    bool solver::extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq) {
         index_set s;
         if (m_antecedents.contains(lit.var())) {
             return true;
@@ -3530,6 +3655,7 @@ namespace sat {
         }
         else {
             if (!extract_assumptions(lit, s)) {
+                SASSERT(!m_todo_antecedents.empty());
                 return false;
             }
             add_assumption(lit);
@@ -3548,6 +3674,16 @@ namespace sat {
         return true;
     }
 
+    void solver::extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_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 (!at_base_lvl() || inconsistent())
             return;

src/sat/sat_solver.h

@@ -506,6 +506,7 @@ namespace sat {
         typedef hashtable<unsigned, u_hash, u_eq> index_set;
 
         u_map<index_set>       m_antecedents;
+        literal_vector         m_todo_antecedents;
         vector<literal_vector> m_binary_clause_graph;
 
         bool extract_assumptions(literal lit, index_set& s);
@@ -522,7 +523,11 @@ namespace sat {
 
         void extract_fixed_consequences(unsigned& start, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
 
-        bool extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+        void extract_fixed_consequences(literal_set const& unfixed_lits, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+
+        void extract_fixed_consequences(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
+
+        bool extract_fixed_consequences1(literal lit, literal_set const& assumptions, bool_var_set& unfixed, vector<literal_vector>& conseq);
 
         void update_unfixed_literals(literal_set& unfixed_lits, bool_var_set& unfixed_vars);
 

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() {
@@ -264,7 +264,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) {}
 
@@ -348,7 +348,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();

src/smt/params/smt_params.cpp

@@ -31,6 +31,8 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_restart_strategy = static_cast<restart_strategy>(p.restart_strategy());
     m_restart_factor = p.restart_factor();
     m_case_split_strategy = static_cast<case_split_strategy>(p.case_split());
+    m_theory_case_split = p.theory_case_split();
+    m_theory_aware_branching = p.theory_aware_branching();
     m_delay_units = p.delay_units();
     m_delay_units_threshold = p.delay_units_threshold();
     m_preprocess = _p.get_bool("preprocess", true); // hidden parameter
@@ -39,6 +41,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_max_conflicts = p.max_conflicts();
     m_core_validate = p.core_validate();
     m_logic = _p.get_sym("logic", m_logic);
+    m_string_solver = p.string_solver();
     model_params mp(_p);
     m_model_compact = mp.compact();
     if (_p.get_bool("arith.greatest_error_pivot", false))

src/smt/params/smt_params.h

@@ -25,6 +25,7 @@ Revision History:
 #include"theory_arith_params.h"
 #include"theory_array_params.h"
 #include"theory_bv_params.h"
+#include"theory_str_params.h"
 #include"theory_pb_params.h"
 #include"theory_datatype_params.h"
 #include"preprocessor_params.h"
@@ -66,7 +67,8 @@ enum case_split_strategy {
     CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
     CS_RELEVANCY, // case split based on relevancy
     CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
-    CS_RELEVANCY_GOAL // based on relevancy and the current goal
+    CS_RELEVANCY_GOAL, // based on relevancy and the current goal
+    CS_ACTIVITY_THEORY_AWARE_BRANCHING // activity-based case split, but theory solvers can manipulate activity
 };
 
 struct smt_params : public preprocessor_params, 
@@ -75,6 +77,7 @@ struct smt_params : public preprocessor_params,
                     public theory_arith_params, 
                     public theory_array_params, 
                     public theory_bv_params,
+                    public theory_str_params,
                     public theory_pb_params,
                     public theory_datatype_params {
     bool             m_display_proof;
@@ -109,6 +112,8 @@ 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;
+    bool                m_theory_aware_branching;
 
     // -----------------------------------
     //
@@ -212,6 +217,13 @@ struct smt_params : public preprocessor_params,
     bool                m_dump_goal_as_smt;
     bool                m_auto_config;
 
+    // -----------------------------------
+    //
+    // Solver selection
+    //
+    // -----------------------------------
+    symbol m_string_solver;
+
     smt_params(params_ref const & p = params_ref()):
         m_display_proof(false),
         m_display_dot_proof(false),
@@ -239,6 +251,8 @@ struct smt_params : public preprocessor_params,
         m_case_split_strategy(CS_ACTIVITY_DELAY_NEW),
         m_rel_case_split_order(0),
         m_lookahead_diseq(false),
+        m_theory_case_split(false),
+        m_theory_aware_branching(false),
         m_delay_units(false),
         m_delay_units_threshold(32),
         m_theory_resolve(false),
@@ -280,7 +294,8 @@ struct smt_params : public preprocessor_params,
         m_at_labels_cex(false),
         m_check_at_labels(false),
         m_dump_goal_as_smt(false),
-        m_auto_config(true) {
+        m_auto_config(true),
+        m_string_solver(symbol("auto")){
         updt_local_params(p);
     }
 

src/smt/params/smt_params_helper.pyg

@@ -11,7 +11,7 @@ def_module_params(module_name='smt',
                           ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
-                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal'),
+                          ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
@@ -61,7 +61,21 @@ 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.'),
+                          ('string_solver', SYMBOL, 'seq', 'solver for string/sequence theories. options are: \'z3str3\' (specialized string solver), \'seq\' (sequence solver), \'auto\' (use static features to choose best solver)'),
                           ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
+                          ('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
+                          ('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
+                          ('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),
+                          ('str.aggressive_unroll_testing', BOOL, True, 'prioritize testing concrete regex unroll counts over generating more options'),
+                          ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
+                          ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
+                          ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
+                          ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
+                          ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
+                          ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
+                          ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
+                          ('str.overlap_priority', DOUBLE, -0.1, 'theory-aware priority for overlapping variable cases; use smt.theory_aware_branching=true'),
                           ('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'),
                           ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),

src/smt/params/theory_str_params.cpp

@@ -0,0 +1,34 @@
+/*++
+Module Name:
+
+    theory_str_params.cpp
+
+Abstract:
+
+    Parameters for string theory plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2016-12-13
+
+Revision History:
+
+--*/
+
+#include"theory_str_params.h"
+#include"smt_params_helper.hpp"
+
+void theory_str_params::updt_params(params_ref const & _p) {
+    smt_params_helper p(_p);
+    m_StrongArrangements = p.str_strong_arrangements();
+    m_AggressiveLengthTesting = p.str_aggressive_length_testing();
+    m_AggressiveValueTesting = p.str_aggressive_value_testing();
+    m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
+    m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
+    m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
+    m_StringConstantCache = p.str_string_constant_cache();
+    m_FiniteOverlapModels = p.str_finite_overlap_models();
+    m_UseBinarySearch = p.str_use_binary_search();
+    m_BinarySearchInitialUpperBound = p.str_binary_search_start();
+    m_OverlapTheoryAwarePriority = p.str_overlap_priority();
+}

src/smt/params/theory_str_params.h

@@ -0,0 +1,102 @@
+/*++
+Module Name:
+
+    theory_str_params.h
+
+Abstract:
+
+    Parameters for string theory plugin
+
+Author:
+
+    Murphy Berzish (mtrberzi) 2016-12-13
+
+Revision History:
+
+--*/
+
+#ifndef THEORY_STR_PARAMS_H
+#define THEORY_STR_PARAMS_H
+
+#include"params.h"
+
+struct theory_str_params {
+    /*
+     * If AssertStrongerArrangements is set to true,
+     * the implications that would normally be asserted during arrangement generation
+     * will instead be asserted as equivalences.
+     * This is a stronger version of the standard axiom.
+     * The Z3str2 axioms can be simulated by setting this to false.
+     */
+    bool m_StrongArrangements;
+
+    /*
+     * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
+     * to prioritize trying concrete length options over choosing the "more" option.
+     */
+    bool m_AggressiveLengthTesting;
+
+    /*
+     * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
+     * to prioritize trying concrete value options over choosing the "more" option.
+     */
+    bool m_AggressiveValueTesting;
+
+    /*
+     * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
+     * to prioritize trying concrete unroll counts over choosing the "more" option.
+     */
+    bool m_AggressiveUnrollTesting;
+
+    /*
+     * If UseFastLengthTesterCache is set to true,
+     * length tester terms will not be generated from scratch each time they are needed,
+     * but will be saved in a map and looked up.
+     */
+    bool m_UseFastLengthTesterCache;
+
+    /*
+     * If UseFastValueTesterCache is set to true,
+     * value tester terms will not be generated from scratch each time they are needed,
+     * but will be saved in a map and looked up.
+     */
+    bool m_UseFastValueTesterCache;
+
+    /*
+     * If StringConstantCache is set to true,
+     * all string constants in theory_str generated from anywhere will be cached and saved.
+     */
+    bool m_StringConstantCache;
+
+    /*
+     * If FiniteOverlapModels is set to true,
+     * arrangements that result in overlapping variables will generate a small number of models
+     * to test instead of completely giving up on the case.
+     */
+    bool m_FiniteOverlapModels;
+
+    bool m_UseBinarySearch;
+    unsigned m_BinarySearchInitialUpperBound;
+
+    double m_OverlapTheoryAwarePriority;
+
+    theory_str_params(params_ref const & p = params_ref()):
+        m_StrongArrangements(true),
+        m_AggressiveLengthTesting(false),
+        m_AggressiveValueTesting(false),
+        m_AggressiveUnrollTesting(true),
+        m_UseFastLengthTesterCache(false),
+        m_UseFastValueTesterCache(true),
+        m_StringConstantCache(true),
+        m_FiniteOverlapModels(false),
+        m_UseBinarySearch(false),
+        m_BinarySearchInitialUpperBound(64),
+        m_OverlapTheoryAwarePriority(-0.1)
+    {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+};
+
+#endif /* THEORY_STR_PARAMS_H */

src/smt/smt_case_split_queue.cpp

@@ -22,9 +22,13 @@ Revision History:
 #include"stopwatch.h"
 #include"for_each_expr.h"
 #include"ast_pp.h"
+#include"map.h"
+#include"hashtable.h"
 
 namespace smt {
 
+    typedef map<bool_var, double, int_hash, default_eq<bool_var> > theory_var_priority_map;
+
     struct bool_var_act_lt {
         svector<double> const & m_activity;
         bool_var_act_lt(svector<double> const & a):m_activity(a) {}
@@ -35,6 +39,27 @@ namespace smt {
 
     typedef heap<bool_var_act_lt> bool_var_act_queue;
 
+    struct theory_aware_act_lt {
+        svector<double> const & m_activity;
+        theory_var_priority_map const & m_theory_var_priority;
+        theory_aware_act_lt(svector<double> const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {}
+        bool operator()(bool_var v1, bool_var v2) const {
+            double p_v1, p_v2;
+            if (!m_theory_var_priority.find(v1, p_v1)) {
+                p_v1 = 0.0;
+            }
+            if (!m_theory_var_priority.find(v2, p_v2)) {
+                p_v2 = 0.0;
+            }
+	    // add clause activity
+	    p_v1 += m_activity[v1];
+	    p_v2 += m_activity[v2];
+            return p_v1 > p_v2;
+        }
+    };
+
+    typedef heap<theory_aware_act_lt> theory_aware_act_queue;
+
     /**
        \brief Case split queue based on activity and random splits.
     */
@@ -1087,6 +1112,120 @@ namespace smt {
         }
     };
 
+    class theory_aware_branching_queue : public case_split_queue {
+    protected:
+        context &          m_context;
+        smt_params &       m_params;
+        theory_var_priority_map m_theory_var_priority;
+        theory_aware_act_queue m_queue;
+
+        int_hashtable<int_hash, default_eq<bool_var> > m_theory_vars;
+        map<bool_var, lbool, int_hash, default_eq<bool_var> > m_theory_var_phase;
+    public:
+        theory_aware_branching_queue(context & ctx, smt_params & p):
+            m_context(ctx),
+            m_params(p),
+            m_theory_var_priority(),
+            m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) {
+        }
+
+        virtual void activity_increased_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.decreased(v);
+        }
+
+        virtual void mk_var_eh(bool_var v) {
+            m_queue.reserve(v+1);
+            m_queue.insert(v);
+        }
+
+        virtual void del_var_eh(bool_var v) {
+            if (m_queue.contains(v))
+                m_queue.erase(v);
+        }
+
+        virtual void unassign_var_eh(bool_var v) {
+            if (!m_queue.contains(v))
+                m_queue.insert(v);
+        }
+
+        virtual void relevant_eh(expr * n) {}
+
+        virtual void init_search_eh() {}
+
+        virtual void end_search_eh() {}
+
+        virtual void reset() {
+            m_queue.reset();
+        }
+
+        virtual void push_scope() {}
+
+        virtual void pop_scope(unsigned num_scopes) {}
+
+        virtual void next_case_split(bool_var & next, lbool & phase) {
+            int threshold = static_cast<int>(m_params.m_random_var_freq * random_gen::max_value());
+            SASSERT(threshold >= 0);
+            if (m_context.get_random_value() < threshold) {
+                SASSERT(m_context.get_num_b_internalized() > 0);
+                next = m_context.get_random_value() % m_context.get_num_b_internalized(); 
+                TRACE("random_split", tout << "next: " << next << " get_assignment(next): " << m_context.get_assignment(next) << "\n";);
+                if (m_context.get_assignment(next) == l_undef)
+                    return;
+            }
+
+            while (!m_queue.empty()) {
+                next = m_queue.erase_min();
+                if (m_context.get_assignment(next) == l_undef)
+                    return;
+            }
+
+            next = null_bool_var;
+            if (m_theory_vars.contains(next)) {
+                if (!m_theory_var_phase.find(next, phase)) {
+                    phase = l_undef;
+                }
+            }
+        }
+
+        virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
+            TRACE("theory_aware_branching", tout << "Add theory-aware branching information for l#" << v << ": priority=" << priority << std::endl;);
+            m_theory_vars.insert(v);
+            m_theory_var_phase.insert(v, phase);
+            m_theory_var_priority.insert(v, priority);
+            if (m_queue.contains(v)) {
+                if (priority > 0.0) {
+                    m_queue.decreased(v);
+                } else {
+                    m_queue.increased(v);
+                }
+            }
+            // m_theory_queue.reserve(v+1);
+            // m_theory_queue.insert(v);
+        }
+
+        virtual void display(std::ostream & out) {
+            bool first = true;
+            bool_var_act_queue::const_iterator it  = m_queue.begin();
+            bool_var_act_queue::const_iterator end = m_queue.end();
+            for (; it != end ; ++it) {
+                unsigned v = *it;
+                if (m_context.get_assignment(v) == l_undef) {
+                    if (first) {
+                        out << "remaining case-splits:\n";
+                        first = false;
+                    }
+                    out << "#" << m_context.bool_var2expr(v)->get_id() << " ";
+                }
+            }
+            if (!first)
+                out << "\n";
+
+        }
+
+        virtual ~theory_aware_branching_queue() {};
+    };
+
 
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
         if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
@@ -1110,6 +1249,8 @@ namespace smt {
             return alloc(rel_act_case_split_queue, ctx, p);
         case CS_RELEVANCY_GOAL:
             return alloc(rel_goal_case_split_queue, ctx, p);
+        case CS_ACTIVITY_THEORY_AWARE_BRANCHING:
+            return alloc(theory_aware_branching_queue, ctx, p);
         default:
             return alloc(act_case_split_queue, ctx, p);
         }

src/smt/smt_case_split_queue.h

@@ -46,6 +46,9 @@ namespace smt {
         virtual void next_case_split(bool_var & next, lbool & phase) = 0;
         virtual void display(std::ostream & out) = 0;
         virtual ~case_split_queue() {}
+
+        // theory-aware branching hint
+        virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {}
     };
 
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p);

src/smt/smt_context.cpp

@@ -1768,6 +1768,8 @@ namespace smt {
             unsigned qhead = m_qhead;
             if (!bcp())
                 return false;
+            if (!propagate_th_case_split(qhead))
+                return false;
             if (get_cancel_flag()) {
                 m_qhead = qhead;
                 return true;
@@ -2455,8 +2457,9 @@ namespace smt {
         
         ptr_vector<theory>::iterator it  = m_theory_set.begin();
         ptr_vector<theory>::iterator end = m_theory_set.end();
-        for (; it != end; ++it)
+        for (; it != end; ++it) {
             (*it)->pop_scope_eh(num_scopes);
+        }
 
         del_justifications(m_justifications, s.m_justifications_lim);
 
@@ -2969,6 +2972,115 @@ namespace smt {
         assert_expr_core(e, pr);
     }
 
+    class case_split_insert_trail : public trail<context> {
+        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 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];
+                    mk_clause(~l1, ~l2, (justification*) 0);
+                }
+            }
+        } 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<context, vector<literal_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<literal_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::add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
+        m_case_split_queue->add_theory_aware_branching_info(v, priority, phase);
+    }
+
+    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(unsigned qhead) {
+        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_end = m_assigned_literals.size();
+        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;);
+            // check if this literal participates in any theory case split
+            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<literal_vector> const& case_split_sets = m_literal2casesplitsets[l.index()];
+            for (vector<literal_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 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());
@@ -3012,11 +3124,18 @@ namespace smt {
     }
 
     bool is_valid_assumption(ast_manager & m, expr * assumption) {
+        expr* arg;
         if (!m.is_bool(assumption))
             return false;
         if (is_uninterp_const(assumption))
             return true;
-        if (m.is_not(assumption) && is_uninterp_const(to_app(assumption)->get_arg(0)))
+        if (m.is_not(assumption, arg) && is_uninterp_const(arg))
+            return true;
+        if (!is_app(assumption)) 
+            return false;
+        if (to_app(assumption)->get_num_args() == 0)
+            return true;
+        if (m.is_not(assumption, arg) && is_app(arg) && to_app(arg)->get_num_args() == 0)
             return true;
         return false;
     }

src/smt/smt_context.h

@@ -226,6 +226,15 @@ 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<literal_vector> m_th_case_split_sets;
+        u_map< vector<literal_vector> > m_literal2casesplitsets; // returns the case split literal sets that a literal participates in
+
         // -----------------------------------
         //
         // Accessors
@@ -827,6 +836,29 @@ 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);
+
+
+        /*
+         * Provide a hint to the branching heuristic about the priority of a "theory-aware literal".
+         * Literals marked in this way will always be branched on before unmarked literals,
+         * starting with the literal having the highest priority.
+         */
+        void add_theory_aware_branching_info(bool_var v, double priority, lbool phase);
+
+    public:
+
+        // helper function for trail
+        void undo_th_case_split(literal l);
+
+        bool propagate_th_case_split(unsigned qhead);
 
         bool_var mk_bool_var(expr * n);
 

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);

src/smt/smt_setup.cpp

@@ -33,6 +33,7 @@ Revision History:
 #include"theory_seq.h"
 #include"theory_pb.h"
 #include"theory_fpa.h"
+#include"theory_str.h"
 
 namespace smt {
 
@@ -120,6 +121,8 @@ namespace smt {
             setup_QF_FP();
         else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
             setup_QF_FPBV();
+        else if (m_logic == "QF_S")
+            setup_QF_S();
         else
             setup_unknown();
     }
@@ -161,6 +164,8 @@ namespace smt {
                  setup_QF_BVRE();
             else if (m_logic == "QF_AUFLIA")
                 setup_QF_AUFLIA(st);
+            else if (m_logic == "QF_S")
+                setup_QF_S();
             else if (m_logic == "AUFLIA")
                 setup_AUFLIA(st);
             else if (m_logic == "AUFLIRA")
@@ -201,7 +206,7 @@ namespace smt {
     void setup::setup_QF_BVRE() {
         setup_QF_BV();
         setup_QF_LIA();
-        setup_seq();
+        m_context.register_plugin(alloc(theory_seq, m_manager));
     }
 
     void setup::setup_QF_UF(static_features const & st) {
@@ -700,6 +705,11 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_fpa, m_manager));
     }
 
+    void setup::setup_QF_S() {
+        m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
+        m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
+    }
+
     bool is_arith(static_features const & st) {
         return st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0;
     }
@@ -814,8 +824,25 @@ namespace smt {
         m_context.register_plugin(mk_theory_dl(m_manager));
     }
 
-    void setup::setup_seq() {
+    void setup::setup_seq_str(static_features const & st) {
-        m_context.register_plugin(alloc(theory_seq, m_manager));
+        // check params for what to do here when it's ambiguous
+        if (m_params.m_string_solver == "z3str3") {
+            setup_str();
+        } 
+        else if (m_params.m_string_solver == "seq") {
+            setup_seq();
+        } 
+        else if (m_params.m_string_solver == "auto") {
+            if (st.m_has_seq_non_str) {
+                setup_seq();
+            } 
+            else {
+                setup_str();
+            }
+        } 
+        else {
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+        }
     }
 
     void setup::setup_card() {
@@ -827,13 +854,25 @@ namespace smt {
         m_context.register_plugin(alloc(theory_fpa, m_manager));
     }
 
+    void setup::setup_str() {
+        setup_arith();
+        m_context.register_plugin(alloc(theory_str, m_manager, m_params));
+    }
+
+    void setup::setup_seq() {
+        m_context.register_plugin(alloc(smt::theory_seq, m_manager));
+    }
+
     void setup::setup_unknown() {
+        static_features st(m_manager);
+        st.collect(m_context.get_num_asserted_formulas(), m_context.get_asserted_formulas());
+
         setup_arith();
         setup_arrays();
         setup_bv();
         setup_datatypes();
         setup_dl();
-        setup_seq();
+        setup_seq_str(st);
         setup_card();
         setup_fpa();
     }
@@ -848,7 +887,7 @@ namespace smt {
             setup_datatypes();
             setup_bv();
             setup_dl();
-            setup_seq();
+            setup_seq_str(st);
             setup_card();
             setup_fpa();
             return;

src/smt/smt_setup.h

@@ -77,6 +77,7 @@ namespace smt {
         void setup_QF_AUFLIA(static_features const & st);
         void setup_QF_FP();
         void setup_QF_FPBV();
+        void setup_QF_S();
         void setup_LRA();
         void setup_AUFLIA(bool simple_array = true);
         void setup_AUFLIA(static_features const & st);
@@ -93,11 +94,13 @@ namespace smt {
         void setup_bv();
         void setup_arith();
         void setup_dl();
+        void setup_seq_str(static_features const & st);
         void setup_seq();
         void setup_card();
         void setup_i_arith();
         void setup_mi_arith();
         void setup_fpa();
+        void setup_str();
 
     public:
         setup(context & c, smt_params & params);

src/smt/smt_theory.h

@@ -186,7 +186,7 @@ namespace smt {
         }
 
         /**
-           \brief This method is called from smt_context when an unsat core is generated.
+           \brief This method is called from the smt_context when an unsat core is generated.
            The theory may change the answer to UNKNOWN by returning l_undef from this method.
         */
         virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {

src/smt/theory_arith.h

@@ -505,7 +505,7 @@ namespace smt {
         struct var_value_eq {
             theory_arith & m_th;
             var_value_eq(theory_arith & th):m_th(th) {}
-            bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int(v1) == m_th.is_int(v2); }
+            bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int_src(v1) == m_th.is_int_src(v2); }
         };
 
         typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
@@ -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); }

src/smt/theory_arith_aux.h

@@ -2201,16 +2201,19 @@ namespace smt {
         int num       = get_num_vars();
         for (theory_var v = 0; v < num; v++) {
             enode * n        = get_enode(v);
-            TRACE("func_interp_bug", tout << "#" << n->get_owner_id() << " -> " << m_value[v] << "\n";);
+            TRACE("func_interp_bug", tout << mk_pp(n->get_owner(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";);
-            if (!is_relevant_and_shared(n))
+            if (!is_relevant_and_shared(n)) {
                 continue;
+            }
             theory_var other = null_theory_var;
             other = m_var_value_table.insert_if_not_there(v);
-            if (other == v)
+            if (other == v) {
                 continue;
+            }
             enode * n2 = get_enode(other);
-            if (n->get_root() == n2->get_root())
+            if (n->get_root() == n2->get_root()) {
                 continue;
+            }
             TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
             m_assume_eq_candidates.push_back(std::make_pair(other, v));
             result = true;

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) {

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())
+            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())
+            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 << " ";

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;

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);

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* a1 = get_automaton(n1->get_owner());
-        eautomaton* a2 = get_automaton(n2->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);

src/smt/theory_str.h

@@ -0,0 +1,653 @@
+/*++
+  Module Name:
+
+  theory_str.h
+
+  Abstract:
+
+  String Theory Plugin
+
+  Author:
+
+  Murphy Berzish and Yunhui Zheng
+
+  Revision History:
+
+  --*/
+#ifndef _THEORY_STR_H_
+#define _THEORY_STR_H_
+
+#include"smt_theory.h"
+#include"theory_str_params.h"
+#include"trail.h"
+#include"th_rewriter.h"
+#include"value_factory.h"
+#include"smt_model_generator.h"
+#include"arith_decl_plugin.h"
+#include<set>
+#include<stack>
+#include<vector>
+#include<map>
+#include"seq_decl_plugin.h"
+#include"union_find.h"
+
+namespace smt {
+
+typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
+
+class str_value_factory : public value_factory {
+    seq_util u;
+    symbol_set m_strings;
+    std::string delim;
+    unsigned m_next;
+public:
+    str_value_factory(ast_manager & m, family_id fid) :
+        value_factory(m, fid),
+        u(m), delim("!"), m_next(0) {}
+    virtual ~str_value_factory() {}
+    virtual expr * get_some_value(sort * s) {
+        return u.str.mk_string(symbol("some value"));
+    }
+    virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
+        v1 = u.str.mk_string(symbol("value 1"));
+        v2 = u.str.mk_string(symbol("value 2"));
+        return true;
+    }
+    virtual expr * get_fresh_value(sort * s) {
+        if (u.is_string(s)) {
+            while (true) {
+                std::ostringstream strm;
+                strm << delim << std::hex << (m_next++) << std::dec << delim;
+                symbol sym(strm.str().c_str());
+                if (m_strings.contains(sym)) continue;
+                m_strings.insert(sym);
+                return u.str.mk_string(sym);
+            }
+        }
+        sort* seq = 0;
+        if (u.is_re(s, seq)) {
+            expr* v0 = get_fresh_value(seq);
+            return u.re.mk_to_re(v0);
+        }
+        TRACE("t_str", tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
+        UNREACHABLE(); return NULL;
+    }
+    virtual void register_value(expr * n) { /* Ignore */ }
+};
+
+// rather than modify obj_pair_map I inherit from it and add my own helper methods
+class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
+public:
+    expr * operator[](std::pair<expr*, expr*> key) const {
+        expr * value;
+        bool found = this->find(key.first, key.second, value);
+        if (found) {
+            return value;
+        } else {
+            TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
+            return NULL;
+        }
+    }
+
+    bool contains(std::pair<expr*, expr*> key) const {
+        expr * unused;
+        return this->find(key.first, key.second, unused);
+    }
+};
+
+template<typename Ctx>
+class binary_search_trail : public trail<Ctx> {
+    obj_map<expr, ptr_vector<expr> > & target;
+    expr * entry;
+public:
+    binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
+        target(target), entry(entry) {}
+    virtual ~binary_search_trail() {}
+    virtual void undo(Ctx & ctx) {
+        TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
+        if (target.contains(entry)) {
+            if (!target[entry].empty()) {
+                target[entry].pop_back();
+            } else {
+                TRACE("t_str_binary_search", tout << "WARNING: attempt to remove length tester from an empty stack" << std::endl;);
+            }
+        } else {
+            TRACE("t_str_binary_search", tout << "WARNING: attempt to access length tester map via invalid key" << std::endl;);
+        }
+    }
+};
+
+
+class nfa {
+protected:
+    bool m_valid;
+    unsigned m_next_id;
+
+    unsigned next_id() {
+        unsigned retval = m_next_id;
+        ++m_next_id;
+        return retval;
+    }
+
+    unsigned m_start_state;
+    unsigned m_end_state;
+
+    std::map<unsigned, std::map<char, unsigned> > transition_map;
+    std::map<unsigned, std::set<unsigned> > epsilon_map;
+
+    void make_transition(unsigned start, char symbol, unsigned end) {
+        transition_map[start][symbol] = end;
+    }
+
+    void make_epsilon_move(unsigned start, unsigned end) {
+        epsilon_map[start].insert(end);
+    }
+
+    // Convert a regular expression to an e-NFA using Thompson's construction
+    void convert_re(expr * e, unsigned & start, unsigned & end, seq_util & u);
+
+public:
+    nfa(seq_util & u, expr * e)
+: m_valid(true), m_next_id(0), m_start_state(0), m_end_state(0) {
+        convert_re(e, m_start_state, m_end_state, u);
+    }
+
+    nfa() : m_valid(false), m_next_id(0), m_start_state(0), m_end_state(0) {}
+
+    bool is_valid() const {
+        return m_valid;
+    }
+
+    void epsilon_closure(unsigned start, std::set<unsigned> & closure);
+
+    bool matches(zstring input);
+};
+
+class theory_str : public theory {
+    struct T_cut
+    {
+        int level;
+        std::map<expr*, int> vars;
+
+        T_cut() {
+            level = -100;
+        }
+    };
+
+    typedef trail_stack<theory_str> th_trail_stack;
+    typedef union_find<theory_str> th_union_find;
+
+    typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
+    struct zstring_hash_proc {
+        unsigned operator()(zstring const & s) const {
+            return string_hash(s.encode().c_str(), static_cast<unsigned>(s.length()), 17);
+        }
+    };
+    typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
+
+protected:
+    theory_str_params const & m_params;
+
+    /*
+     * Setting EagerStringConstantLengthAssertions to true allows some methods,
+     * in particular internalize_term(), to add
+     * length assertions about relevant string constants.
+     * Note that currently this should always be set to 'true', or else *no* length assertions
+     * will be made about string constants.
+     */
+    bool opt_EagerStringConstantLengthAssertions;
+
+    /*
+     * If VerifyFinalCheckProgress is set to true, continuing after final check is invoked
+     * without asserting any new axioms is considered a bug and will throw an exception.
+     */
+    bool opt_VerifyFinalCheckProgress;
+
+    /*
+     * This constant controls how eagerly we expand unrolls in unbounded regex membership tests.
+     */
+    int opt_LCMUnrollStep;
+
+    /*
+     * If NoQuickReturn_IntegerTheory is set to true,
+     * integer theory integration checks that assert axioms
+     * will not return from the function after asserting their axioms.
+     * The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect.
+     */
+    bool opt_NoQuickReturn_IntegerTheory;
+
+    /*
+     * If DisableIntegerTheoryIntegration is set to true,
+     * ALL calls to the integer theory integration methods
+     * (get_value, get_len_value, lower_bound, upper_bound)
+     * will ignore what the arithmetic solver believes about length terms,
+     * and will return no information.
+     *
+     * This reduces performance significantly, but can be useful to enable
+     * if it is suspected that string-integer integration, or the arithmetic solver itself,
+     * might have a bug.
+     *
+     * The default behaviour of Z3str2 is to set this to 'false'.
+     */
+    bool opt_DisableIntegerTheoryIntegration;
+
+    /*
+     * If DeferEQCConsistencyCheck is set to true,
+     * expensive calls to new_eq_check() will be deferred until final check,
+     * at which time the consistency of *all* string equivalence classes will be validated.
+     */
+    bool opt_DeferEQCConsistencyCheck;
+
+    /*
+     * If CheckVariableScope is set to true,
+     * pop_scope_eh() and final_check_eh() will run extra checks
+     * to determine whether the current assignment
+     * contains references to any internal variables that are no longer in scope.
+     */
+    bool opt_CheckVariableScope;
+
+    /*
+     * If ConcatOverlapAvoid is set to true,
+     * the check to simplify Concat = Concat in handle_equality() will
+     * avoid simplifying wrt. pairs of Concat terms that will immediately
+     * result in an overlap. (false = Z3str2 behaviour)
+     */
+    bool opt_ConcatOverlapAvoid;
+
+    bool search_started;
+    arith_util m_autil;
+    seq_util u;
+    int sLevel;
+
+    bool finalCheckProgressIndicator;
+
+    expr_ref_vector m_trail; // trail for generated terms
+
+    str_value_factory * m_factory;
+
+    // terms we couldn't go through set_up_axioms() with because they weren't internalized
+    expr_ref_vector m_delayed_axiom_setup_terms;
+
+    ptr_vector<enode> m_basicstr_axiom_todo;
+    svector<std::pair<enode*,enode*> > m_str_eq_todo;
+    ptr_vector<enode> m_concat_axiom_todo;
+    ptr_vector<enode> m_string_constant_length_todo;
+    ptr_vector<enode> m_concat_eval_todo;
+
+    // enode lists for library-aware/high-level string terms (e.g. substr, contains)
+    ptr_vector<enode> m_library_aware_axiom_todo;
+
+    // hashtable of all exprs for which we've already set up term-specific axioms --
+    // this prevents infinite recursive descent with respect to axioms that
+    // include an occurrence of the term for which axioms are being generated
+    obj_hashtable<expr> axiomatized_terms;
+
+    int tmpStringVarCount;
+    int tmpXorVarCount;
+    int tmpLenTestVarCount;
+    int tmpValTestVarCount;
+    std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
+
+    bool avoidLoopCut;
+    bool loopDetected;
+    obj_map<expr, std::stack<T_cut*> > cut_var_map;
+    expr_ref m_theoryStrOverlapAssumption_term;
+
+    obj_hashtable<expr> variable_set;
+    obj_hashtable<expr> internal_variable_set;
+    obj_hashtable<expr> regex_variable_set;
+    std::map<int, std::set<expr*> > internal_variable_scope_levels;
+
+    obj_hashtable<expr> internal_lenTest_vars;
+    obj_hashtable<expr> internal_valTest_vars;
+    obj_hashtable<expr> internal_unrollTest_vars;
+
+    obj_hashtable<expr> input_var_in_len;
+
+    obj_map<expr, unsigned int> fvar_len_count_map;
+    std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+    obj_map<expr, expr*> lenTester_fvar_map;
+
+    std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
+    std::map<expr*, expr*> valueTester_fvar_map;
+
+    std::map<expr*, int_vector> val_range_map;
+
+    // This can't be an expr_ref_vector because the constructor is wrong,
+    // we would need to modify the allocator so we pass in ast_manager
+    std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
+    std::map<expr*, expr*> unroll_var_map;
+    std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
+
+    expr_ref_vector contains_map;
+
+    theory_str_contain_pair_bool_map_t contain_pair_bool_map;
+    //obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
+    std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
+
+    std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
+    std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
+
+    std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+
+    char * char_set;
+    std::map<char, int> charSetLookupTable;
+    int charSetSize;
+
+    obj_pair_map<expr, expr, expr*> concat_astNode_map;
+
+    // all (str.to-int) and (int.to-str) terms
+    expr_ref_vector string_int_conversion_terms;
+    obj_hashtable<expr> string_int_axioms;
+
+    // used when opt_FastLengthTesterCache is true
+    rational_map lengthTesterCache;
+    // used when opt_FastValueTesterCache is true
+    string_map valueTesterCache;
+
+    string_map stringConstantCache;
+    unsigned long totalCacheAccessCount;
+    unsigned long cacheHitCount;
+    unsigned long cacheMissCount;
+
+    // cache mapping each string S to Length(S)
+    obj_map<expr, app*> length_ast_map;
+
+    th_union_find m_find;
+    th_trail_stack m_trail_stack;
+    theory_var get_var(expr * n) const;
+    expr * get_eqc_next(expr * n);
+    app * get_ast(theory_var i);
+
+    // binary search heuristic data
+    struct binary_search_info {
+        rational lowerBound;
+        rational midPoint;
+        rational upperBound;
+        rational windowSize;
+
+        binary_search_info() : lowerBound(rational::zero()), midPoint(rational::zero()),
+                upperBound(rational::zero()), windowSize(rational::zero()) {}
+        binary_search_info(rational lower, rational mid, rational upper, rational windowSize) :
+            lowerBound(lower), midPoint(mid), upperBound(upper), windowSize(windowSize) {}
+
+        void calculate_midpoint() {
+            midPoint = floor(lowerBound + ((upperBound - lowerBound) / rational(2)) );
+        }
+    };
+    // maps a free string var to a stack of active length testers.
+    // can use binary_search_trail to record changes to this object
+    obj_map<expr, ptr_vector<expr> > binary_search_len_tester_stack;
+    // maps a length tester var to the *active* search window
+    obj_map<expr, binary_search_info> binary_search_len_tester_info;
+    // maps a free string var to the first length tester to be (re)used
+    obj_map<expr, expr*> binary_search_starting_len_tester;
+    // maps a length tester to the next length tester to be (re)used if the split is "low"
+    obj_map<expr, expr*> binary_search_next_var_low;
+    // maps a length tester to the next length tester to be (re)used if the split is "high"
+    obj_map<expr, expr*> binary_search_next_var_high;
+
+    // finite model finding data
+    // maps a finite model tester var to a list of variables that will be tested
+    obj_map<expr, ptr_vector<expr> > finite_model_test_varlists;
+protected:
+    void assert_axiom(expr * e);
+    void assert_implication(expr * premise, expr * conclusion);
+    expr * rewrite_implication(expr * premise, expr * conclusion);
+
+    expr * mk_string(zstring const& str);
+    expr * mk_string(const char * str);
+
+    app * mk_strlen(expr * e);
+    expr * mk_concat(expr * n1, expr * n2);
+    expr * mk_concat_const_str(expr * n1, expr * n2);
+    app * mk_contains(expr * haystack, expr * needle);
+    app * mk_indexof(expr * haystack, expr * needle);
+    app * mk_fresh_const(char const* name, sort* s);
+
+    literal mk_literal(expr* _e);
+    app * mk_int(int n);
+    app * mk_int(rational & q);
+
+    void check_and_init_cut_var(expr * node);
+    void add_cut_info_one_node(expr * baseNode, int slevel, expr * node);
+    void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode);
+    bool has_self_cut(expr * n1, expr * n2);
+
+    // for ConcatOverlapAvoid
+    bool will_result_in_overlap(expr * lhs, expr * rhs);
+
+    void track_variable_scope(expr * var);
+    app * mk_str_var(std::string name);
+    app * mk_int_var(std::string name);
+    app * mk_nonempty_str_var();
+    app * mk_internal_xor_var();
+    expr * mk_internal_valTest_var(expr * node, int len, int vTries);
+    app * mk_regex_rep_var();
+    app * mk_unroll_bound_var();
+    app * mk_unroll_test_var();
+    void add_nonempty_constraint(expr * s);
+
+    void instantiate_concat_axiom(enode * cat);
+    void try_eval_concat(enode * cat);
+    void instantiate_basic_string_axioms(enode * str);
+    void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
+
+    void instantiate_axiom_CharAt(enode * e);
+    void instantiate_axiom_prefixof(enode * e);
+    void instantiate_axiom_suffixof(enode * e);
+    void instantiate_axiom_Contains(enode * e);
+    void instantiate_axiom_Indexof(enode * e);
+    void instantiate_axiom_Indexof2(enode * e);
+    void instantiate_axiom_LastIndexof(enode * e);
+    void instantiate_axiom_Substr(enode * e);
+    void instantiate_axiom_Replace(enode * e);
+    void instantiate_axiom_str_to_int(enode * e);
+    void instantiate_axiom_int_to_str(enode * e);
+
+    expr * mk_RegexIn(expr * str, expr * regexp);
+    void instantiate_axiom_RegexIn(enode * e);
+    app * mk_unroll(expr * n, expr * bound);
+
+    void process_unroll_eq_const_str(expr * unrollFunc, expr * constStr);
+    void unroll_str2reg_constStr(expr * unrollFunc, expr * eqConstStr);
+    void process_concat_eq_unroll(expr * concat, expr * unroll);
+
+    void set_up_axioms(expr * ex);
+    void handle_equality(expr * lhs, expr * rhs);
+
+    app * mk_value_helper(app * n);
+    expr * get_eqc_value(expr * n, bool & hasEqcValue);
+    expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
+    bool in_same_eqc(expr * n1, expr * n2);
+    expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
+
+    bool get_value(expr* e, rational& val) const;
+    bool get_len_value(expr* e, rational& val);
+    bool lower_bound(expr* _e, rational& lo);
+    bool upper_bound(expr* _e, rational& hi);
+
+    bool can_two_nodes_eq(expr * n1, expr * n2);
+    bool can_concat_eq_str(expr * concat, zstring& str);
+    bool can_concat_eq_concat(expr * concat1, expr * concat2);
+    bool check_concat_len_in_eqc(expr * concat);
+    bool check_length_consistency(expr * n1, expr * n2);
+    bool check_length_const_string(expr * n1, expr * constStr);
+    bool check_length_eq_var_concat(expr * n1, expr * n2);
+    bool check_length_concat_concat(expr * n1, expr * n2);
+    bool check_length_concat_var(expr * concat, expr * var);
+    bool check_length_var_var(expr * var1, expr * var2);
+    void check_contain_in_new_eq(expr * n1, expr * n2);
+    void check_contain_by_eqc_val(expr * varNode, expr * constNode);
+    void check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass);
+    void check_contain_by_eq_nodes(expr * n1, expr * n2);
+    bool in_contain_idx_map(expr * n);
+    void compute_contains(std::map<expr*, expr*> & varAliasMap,
+            std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
+            std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
+    expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
+    void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
+            std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
+            std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
+            std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+    void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+    void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
+            std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
+    bool is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec);
+
+    void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
+    expr * simplify_concat(expr * node);
+
+    void simplify_parent(expr * nn, expr * eq_str);
+
+    void simplify_concat_equality(expr * lhs, expr * rhs);
+    void solve_concat_eq_str(expr * concat, expr * str);
+
+    void infer_len_concat_equality(expr * nn1, expr * nn2);
+    bool infer_len_concat(expr * n, rational & nLen);
+    void infer_len_concat_arg(expr * n, rational len);
+
+    bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
+    bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
+    bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);
+    bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2);
+    bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2);
+    bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2);
+
+    void process_concat_eq_type1(expr * concatAst1, expr * concatAst2);
+    void process_concat_eq_type2(expr * concatAst1, expr * concatAst2);
+    void process_concat_eq_type3(expr * concatAst1, expr * concatAst2);
+    void process_concat_eq_type4(expr * concatAst1, expr * concatAst2);
+    void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
+    void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
+
+    void print_cut_var(expr * node, std::ofstream & xout);
+
+    void generate_mutual_exclusion(expr_ref_vector & exprs);
+    void add_theory_aware_branching_info(expr * term, double priority, lbool phase);
+
+    bool new_eq_check(expr * lhs, expr * rhs);
+    void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
+
+    int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
+            std::map<expr*, std::set<expr*> > & unrollGroupMap, std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
+    void trace_ctx_dep(std::ofstream & tout,
+            std::map<expr*, expr*> & aliasIndexMap,
+            std::map<expr*, expr*> & var_eq_constStr_map,
+            std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
+            std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
+            std::map<expr*, expr*> & concat_eq_constStr_map,
+            std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map,
+            std::map<expr*, std::set<expr*> > & unrollGroupMap);
+
+    void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,
+            std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
+    void classify_ast_by_type_in_positive_context(std::map<expr*, int> & varMap,
+            std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
+
+    expr * mk_internal_lenTest_var(expr * node, int lTries);
+    expr * gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue);
+    void process_free_var(std::map<expr*, int> & freeVar_map);
+    expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries);
+    expr * gen_free_var_options(expr * freeVar, expr * len_indicator,
+            zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr);
+    expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
+            zstring lenStr, int tries);
+    void print_value_tester_list(svector<std::pair<int, expr*> > & testerList);
+    bool get_next_val_encode(int_vector & base, int_vector & next);
+    zstring gen_val_string(int len, int_vector & encoding);
+
+    // binary search heuristic
+    expr * binary_search_length_test(expr * freeVar, expr * previousLenTester, zstring previousLenTesterValue);
+    expr_ref binary_search_case_split(expr * freeVar, expr * tester, binary_search_info & bounds, literal_vector & case_split_lits);
+
+    bool free_var_attempt(expr * nn1, expr * nn2);
+    void more_len_tests(expr * lenTester, zstring lenTesterValue);
+    void more_value_tests(expr * valTester, zstring valTesterValue);
+
+    expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node);
+    expr * getMostLeftNodeInConcat(expr * node);
+    expr * getMostRightNodeInConcat(expr * node);
+    void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
+    void get_concats_in_eqc(expr * n, std::set<expr*> & concats);
+    void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
+    expr * eval_concat(expr * n1, expr * n2);
+
+    bool finalcheck_str2int(app * a);
+    bool finalcheck_int2str(app * a);
+
+    // strRegex
+
+    void get_eqc_allUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
+    void get_eqc_simpleUnroll(expr * n, expr * &constStr, std::set<expr*> & unrollFuncSet);
+    void gen_assign_unroll_reg(std::set<expr*> & unrolls);
+    expr * gen_assign_unroll_Str2Reg(expr * n, std::set<expr*> & unrolls);
+    expr * gen_unroll_conditional_options(expr * var, std::set<expr*> & unrolls, zstring lcmStr);
+    expr * gen_unroll_assign(expr * var, zstring lcmStr, expr * testerVar, int l, int h);
+    void reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items);
+    void check_regex_in(expr * nn1, expr * nn2);
+    zstring get_std_regex_str(expr * r);
+
+    void dump_assignments();
+    void initialize_charset();
+
+    void check_variable_scope();
+    void recursive_check_variable_scope(expr * ex);
+
+    void collect_var_concat(expr * node, std::set<expr*> & varSet, std::set<expr*> & concatSet);
+    bool propagate_length(std::set<expr*> & varSet, std::set<expr*> & concatSet, std::map<expr*, int> & exprLenMap);
+    void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
+    bool propagate_length_within_eqc(expr * var);
+
+    // TESTING
+    void refresh_theory_var(expr * e);
+
+    expr_ref set_up_finite_model_test(expr * lhs, expr * rhs);
+    void finite_model_test(expr * v, expr * c);
+
+public:
+    theory_str(ast_manager & m, theory_str_params const & params);
+    virtual ~theory_str();
+
+    virtual char const * get_name() const { return "seq"; }
+    virtual void display(std::ostream & out) const;
+
+    bool overlapping_variables_detected() const { return loopDetected; }
+
+    th_trail_stack& get_trail_stack() { return m_trail_stack; }
+    void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
+    void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
+    void unmerge_eh(theory_var v1, theory_var v2) {}
+protected:
+    virtual bool internalize_atom(app * atom, bool gate_ctx);
+    virtual bool internalize_term(app * term);
+    virtual enode* ensure_enode(expr* e);
+    virtual theory_var mk_var(enode * n);
+
+    virtual void new_eq_eh(theory_var, theory_var);
+    virtual void new_diseq_eh(theory_var, theory_var);
+
+    virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager(), m_params); }
+    virtual void init_search_eh();
+    virtual void add_theory_assumptions(expr_ref_vector & assumptions);
+    virtual lbool validate_unsat_core(expr_ref_vector & unsat_core);
+    virtual void relevant_eh(app * n);
+    virtual void assign_eh(bool_var v, bool is_true);
+    virtual void push_scope_eh();
+    virtual void pop_scope_eh(unsigned num_scopes);
+    virtual void reset_eh();
+
+    virtual bool can_propagate();
+    virtual void propagate();
+
+    virtual final_check_status final_check_eh();
+    virtual void attach_new_th_var(enode * n);
+
+    virtual void init_model(model_generator & m);
+    virtual model_value_proc * mk_value(enode * n, model_generator & mg);
+    virtual void finalize_model(model_generator & mg);
+};
+
+};
+
+#endif /* _THEORY_STR_H_ */

src/solver/smt_logics.cpp

@@ -24,7 +24,7 @@ Revision History:
 bool smt_logics::supported_logic(symbol const & s) {
     return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || 
         logic_has_arith(s) || logic_has_bv(s) ||
-        logic_has_array(s) || logic_has_seq(s) ||
+        logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
         logic_has_horn(s) || logic_has_fpa(s);
 }
 
@@ -132,6 +132,10 @@ bool smt_logics::logic_has_seq(symbol const & s) {
     return s == "QF_BVRE" || s == "QF_S" || s == "ALL";
 }
 
+bool smt_logics::logic_has_str(symbol const & s) {
+    return s == "QF_S" || s == "ALL";
+}
+
 bool smt_logics::logic_has_fpa(symbol const & s) {
     return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL";
 }

src/solver/smt_logics.h

@@ -30,6 +30,7 @@ public:
     static bool logic_has_bv(symbol const & s);
     static bool logic_has_array(symbol const & s);
     static bool logic_has_seq(symbol const & s);
+    static bool logic_has_str(symbol const & s);
     static bool logic_has_fpa(symbol const & s);
     static bool logic_has_horn(symbol const& s);
     static bool logic_has_pb(symbol const& s);

src/tactic/portfolio/enum2bv_solver.cpp

@@ -137,10 +137,12 @@ public:
                 SASSERT(num.is_unsigned());
                 expr_ref head(m);
                 ptr_vector<func_decl> const& enums = *dt.get_datatype_constructors(f->get_range());
+                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;
     }
 

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<sat::literal_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<sat::literal_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<sat::solver::bin_clause> bin_clauses;
+    src.collect_bin_clauses(bin_clauses, false);
+    tracking_clauses.reserve(2*src.num_vars() + static_cast<unsigned>(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<unsigned>(cls.end()-cls.begin()), cls.begin());
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+    for (unsigned i = 0; i < bin_clauses.size(); ++i) {
+        lits.reset();
+        lits.push_back(bin_clauses[i].first);
+        lits.push_back(bin_clauses[i].second);        
+        track_clause(dst, lits, assumptions, tracking_clauses);
+    }
+}
+
+
 static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) {
     for (unsigned i = 0; i < lambda.size(); ++i) {
         if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) {
@@ -88,26 +138,27 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) {
     std::cout << "UNREACHABLE\n";
 }
 
-static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
+static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, sat::literal_vector& backbones) {
     for (unsigned i = 0; i < gamma.size(); ++i) {
         sat::literal nlit = ~gamma[i];
-        lbool r = s.check(1, &nlit);
+        sat::literal_vector asms1(asms);
+        asms1.push_back(nlit);
+        lbool r = s.check(asms1.size(), asms1.c_ptr());
         if (r == l_false) {
             backbones.push_back(gamma[i]);
         }
     }
 }
 
-static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sat::literal_vector>& conseq, unsigned K) {
+static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector<sat::literal_vector>& conseq, unsigned K) {
-    lbool r = s.check();
+    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++) {
+    for (unsigned i = 0; i < vars.size(); i++) {
-        lambda.push_back(sat::literal(i, m[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() << " " << backbones.size() << ")\n";);
@@ -119,7 +170,9 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
             omegaN.push_back(~l);
         }
         while (true) {
-            r = s.check(omegaN.size(), omegaN.c_ptr());
+            sat::literal_vector asms1(asms);
+            asms1.append(omegaN);
+            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());
@@ -149,7 +202,7 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector<sa
                 }
             }
             if (omegaN.empty() && occurs.size() > 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]);
                 }
@@ -173,7 +226,8 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
     params_ref p = gparams::get_module("sat");
     p.set_bool("produce_models", true);
     reslimit limit;
-    sat::solver solver(p, limit, 0);
+    sat::solver solver(p, limit);
+    sat::solver solver2(p, limit);
     g_solver = &solver;
 
     if (file_name) {
@@ -192,16 +246,24 @@ static void cnf_backbones(bool use_chunk, char const* file_name) {
     vector<sat::literal_vector> conseq;
     sat::bool_var_vector vars;
     sat::literal_vector assumptions;
-    for (unsigned i = 1; i < solver.num_vars(); ++i) {
+    unsigned num_vars = solver.num_vars();
+    if (p.get_bool("dimacs.core", false)) {
+        g_solver = &solver2;        
+        vector<sat::literal_vector> tracking_clauses;
+        track_clauses(solver, solver2, assumptions, tracking_clauses);
+    }
+    // remove this line to limit variables to exclude assumptions
+    num_vars = g_solver->num_vars();
+    for (unsigned i = 1; i < num_vars; ++i) {
         vars.push_back(i);        
-        solver.set_external(i);
+        g_solver->set_external(i);
     }
     lbool r;
     if (use_chunk) {
-        r = core_chunking(solver, vars, conseq, 100);
+        r = core_chunking(*g_solver, vars, assumptions, conseq, 100);
     }
     else {
-        r = solver.get_consequences(assumptions, vars, conseq);
+        r = g_solver->get_consequences(assumptions, vars, conseq);
     }
     std::cout << vars.size() << " " << conseq.size() << "\n";
     display_status(r);
@@ -209,10 +271,15 @@ 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 + 1 < argc && argv[i + 1] == std::string("chunk");
-        bool use_chunk = (i + 2 < argc && argv[i + 2] == std::string("chunk"));
-        cnf_backbones(use_chunk, argv[i + 1]);
-        ++i;
     if (use_chunk) ++i;     
+    char const* file = "";
+    if (i + 1 < argc) {
+        file = argv[i + 1];
     }
+    else {
+        file = argv[1];
+    }
+    cnf_backbones(use_chunk, file);
+    ++i;
 }

src/test/main.cpp

@@ -131,7 +131,6 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t
                 std::cerr << ex.msg() << "\n";
             }
         }            
-
 	i++;
     }
 }
@@ -243,12 +242,9 @@ int main(int argc, char ** argv) {
     TST(model_evaluator);
     TST(get_consequences);
     TST(pb2bv);
-<<<<<<< HEAD
     TST_ARGV(sat_lookahead);
     TST_ARGV(sat_local_search);
-=======
     TST_ARGV(cnf_backbones);
->>>>>>> 69aa5ca877f5de0a2c00515d0fe86a797b95701a
     //TST_ARGV(hs);
 }
 

src/test/smt2print_parse.cpp

@@ -13,8 +13,9 @@ Copyright (c) 2015 Microsoft Corporation
 void test_print(Z3_context ctx, Z3_ast a) {
     Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
     char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a);
-    std::cout << spec1 << "\n";
+    std::cout << "spec1: benchmark->string\n" << spec1 << "\n";
 
+    std::cout << "attempting to parse spec1...\n";
     Z3_ast b = 
         Z3_parse_smtlib2_string(ctx, 
                                 spec1,
@@ -24,14 +25,14 @@ void test_print(Z3_context ctx, Z3_ast a) {
                                 0,
                                 0,
                                 0);
-
+    std::cout << "parse successful, converting ast->string\n";
     char const* spec2 = Z3_ast_to_string(ctx, b);
-    std::cout << spec2 << "\n";    
+    std::cout << "spec2: string->ast->string\n" << spec2 << "\n";
 }
 
 void test_parseprint(char const* spec) {
     Z3_context ctx = Z3_mk_context(0);
-    std::cout << spec << "\n";
+    std::cout << "spec:\n" << spec << "\n";
 
     Z3_ast a = 
         Z3_parse_smtlib2_string(ctx, 
@@ -43,8 +44,12 @@ void test_parseprint(char const* spec) {
                                 0,
                                 0);
     
+    std::cout << "done parsing\n";
+
     test_print(ctx, a);
 
+    std::cout << "done printing\n";
+
     Z3_del_context(ctx);
 }
 
@@ -104,6 +109,12 @@ void tst_smt2print_parse() {
 
     test_parseprint(spec5);
 
+    // Test strings
+    char const* spec6 =
+        "(assert (= \"abc\" \"abc\"))";
+
+    test_parseprint(spec6);
+
     // Test ?     
 
 }

src/util/obj_pair_set.h

@@ -46,6 +46,11 @@ public:
     bool contains(obj_pair const & p) const { return m_set.contains(p); }
     void reset() { m_set.reset(); }
     bool empty() const { return m_set.empty(); }
+
+    typedef typename chashtable<obj_pair, hash_proc, eq_proc>::iterator iterator;
+
+    iterator begin() { return m_set.begin(); }
+    iterator end() { return m_set.end(); }
 };
 
 #endif