Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api

README-CMake.md

@@ -279,6 +279,10 @@ The following useful options can be passed to CMake whilst configuring.
 * ``INSTALL_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOTNET_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's .NET bindings.
 * ``DOTNET_CSC_EXECUTABLE`` - STRING. The path to the C# compiler to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``.
 * ``DOTNET_GACUTIL_EXECUTABLE`` - STRING. The path to the gacutil program to use. Only relevant if ``BUILD_DOTNET_BINDINGS`` is set to ``TRUE``.
+* ``BUILD_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Java bindings will be built.
+* ``INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
+* ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
+* ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
 
 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.
 
@@ -286,8 +290,29 @@ Example
 
 ```
 cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../
+
 ```
 
+## Z3 API Bindings
+
+Z3 exposes various language bindings for its API. Below are some notes on building
+and/or installing these bindings when building Z3 with CMake.
+
+### Java bindings
+
+The CMake build uses the ``FindJava`` and ``FindJNI`` cmake modules to detect the
+installation of Java. If CMake fails to find your installation of Java set the
+``JAVA_HOME`` environment variable when invoking CMake so that it points at the
+correct location. For example
+
+```
+JAVA_HOME=/usr/lib/jvm/default cmake -DBUILD_JAVA_BINDINGS=ON ../
+```
+Note that the built ``.jar`` file is named ``com.microsoft.z3-VERSION.jar``
+where ``VERSION`` is the Z3 version. Under non Windows systems a
+symbolic link named ``com.microsoft.z3.jar`` is provided. This symbolic
+link is not created when building under Windows.
+
 ## Developer/packager notes
 
 These notes are help developers and packagers of Z3.

contrib/cmake/src/CMakeLists.txt

@@ -166,7 +166,8 @@ endforeach()
 
 install(TARGETS libz3
   LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}"
-  ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}"
+  ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed?
+  RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake
   PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}"
 )
 
@@ -234,4 +235,16 @@ if (BUILD_DOTNET_BINDINGS)
   add_subdirectory(api/dotnet)
 endif()
 
+################################################################################
+# Java bindings
+################################################################################
+option(BUILD_JAVA_BINDINGS "Build Java bindings for Z3" OFF)
+if (BUILD_JAVA_BINDINGS)
+  if (NOT BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The Java bindings will not work with a static libz3. "
+      "You either need to disable BUILD_JAVA_BINDINGS or enable BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/java)
+endif()
+
 # TODO: Implement support for other bindigns

contrib/cmake/src/api/dotnet/CMakeLists.txt

@@ -203,12 +203,24 @@ if (DOTNET_TOOLCHAIN_IS_WINDOWS)
   endif()
 endif()
 
-# FIXME: The get_property() command only works correctly for single configuration generators
+# FIXME: Ideally we should emit files into a configuration specific directory
-# so we can't use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
+# when using multi-configuration generators so that the files generated by each
-# argument to ``add_custom_commands()`` won't accept it. For now just output file to the
+# configuration don't clobber each other. Unfortunately the ``get_property()``
-# current binary directory.
+# command only works correctly for single configuration generators so we can't
-# get_property(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR TARGET libz3 PROPERTY LIBRARY_OUTPUT_DIRECTORY)
+# use it. We also can't use ``$<TARGET_FILE_DIR:libz3>`` because the ``OUTPUT``
-set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}")
+# argument to ``add_custom_commands()`` won't accept it.
+# See http://public.kitware.com/pipermail/cmake/2016-March/063101.html
+#
+# For now just output file to the root binary directory like the Python build
+# system does and emit a warning when appropriate.
+if (DEFINED CMAKE_CONFIGURATION_TYPES)
+  # Multi-configuration build (e.g. Visual Studio and Xcode).
+  message(WARNING "You are using a multi-configuration generator. The build rules for"
+    " the \".NET\" bindings currently do not emit files per configuration so previously"
+    " generated files for other configurations will be overwritten.")
+endif()
+
+set(Z3_DOTNET_ASSEMBLY_OUTPUT_DIR "${CMAKE_BINARY_DIR}")
 set(Z3_DOTNET_ASSEMBLY_NAME "Microsoft.Z3.dll")
 set(Z3_DOTNET_ASSEMBLY_DLL "${Z3_DOTNET_ASSEMBLY_OUTPUT_DIR}/${Z3_DOTNET_ASSEMBLY_NAME}")
 # csc.exe doesn't work with UNIX style paths so convert to native path
@@ -252,7 +264,9 @@ if (DOTNET_TOOLCHAIN_IS_MONO)
   # to find the assembly
   install(FILES "${Z3_DOTNET_PKGCONFIG_FILE}" DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}")
 
-  # Configure the install and uninstall scripts
+  # Configure the install and uninstall scripts.
+  # Note: If multi-configuration generator support is ever fixed then these
+  # scripts will be broken.
   configure_file(cmake_install_gac.cmake.in cmake_install_gac.cmake @ONLY)
   configure_file(cmake_uninstall_gac.cmake.in cmake_uninstall_gac.cmake @ONLY)
 
@@ -268,9 +282,10 @@ if (DOTNET_TOOLCHAIN_IS_MONO)
   add_dependencies(uninstall remove_dotnet_dll_from_gac)
 
 elseif(DOTNET_TOOLCHAIN_IS_WINDOWS)
-  # FIXME: This isn't implemented because I'm not sure how/if the assembly should
+  # Don't install Z3_DOTNET_ASSEMBLY_DLL into the gac. Instead just copy into
-  # be installed to the GAC.
+  # installation directory.
-  message(WARNING "Install of .NET bindings is not implemented for Windows")
+  install(FILES "${Z3_DOTNET_ASSEMBLY_DLL}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
+  install(FILES "${Z3_DOTNET_ASSEMBLY_DLL_DOC}" DESTINATION "${CMAKE_INSTALL_LIBDIR}")
 else()
   message(FATAL_ERROR "Unknown .NET toolchain")
 endif()

contrib/cmake/src/api/java/CMakeLists.txt

@@ -0,0 +1,236 @@
+find_package(Java REQUIRED)
+find_package(JNI REQUIRED)
+include(UseJava)
+
+# Sanity check for dirty source tree
+foreach (file_name "enumerations" "Native.cpp" "Native.java")
+  if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${file_name}")
+    message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${file_name}\""
+            ${z3_polluted_tree_msg})
+  endif()
+endforeach()
+
+set(Z3_JAVA_PACKAGE_NAME "com.microsoft.z3")
+
+# Rule to generate ``Native.java`` and ``Native.cpp``
+set(Z3_JAVA_NATIVE_JAVA "${CMAKE_CURRENT_BINARY_DIR}/Native.java")
+set(Z3_JAVA_NATIVE_CPP "${CMAKE_CURRENT_BINARY_DIR}/Native.cpp")
+add_custom_command(OUTPUT "${Z3_JAVA_NATIVE_JAVA}" "${Z3_JAVA_NATIVE_CPP}"
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--java-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    "--java-package-name"
+    ${Z3_JAVA_PACKAGE_NAME}
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
+    "${CMAKE_SOURCE_DIR}/scripts/mk_util.py"
+  COMMENT "Generating \"${Z3_JAVA_NATIVE_JAVA}\" and \"${Z3_JAVA_NATIVE_CPP}\""
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+# Add rule to build native code that provides a bridge between
+# ``Native.java`` and libz3's interfac3.
+add_library(z3java SHARED ${Z3_JAVA_NATIVE_CPP})
+target_link_libraries(z3java PRIVATE libz3)
+# FIXME:
+# Not sure if using all the flags used by the Z3 components is really necessary
+# here.  At the bare minimum setting _AMD64_ depending on the target is
+# necessary but seeing as the Python build system uses all the flags used for building
+# Z3's components to build ``Native.cpp`` lets do the same for now.
+target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES})
+z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS})
+target_include_directories(z3java PRIVATE
+  "${CMAKE_SOURCE_DIR}/src/api"
+  "${CMAKE_BINARY_DIR}/src/api"
+  ${JNI_INCLUDE_DIRS}
+)
+# FIXME: Should this library have SONAME and VERSION set?
+
+# This prevents CMake from automatically defining ``z3java_EXPORTS``
+set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
+
+# Rule to generate the ``com.microsoft.z3.enumerations`` package
+# FIXME: This list of files is fragile
+set(Z3_JAVA_ENUMERATION_PACKAGE_FILES
+  Z3_ast_kind.java
+  Z3_ast_print_mode.java
+  Z3_decl_kind.java
+  Z3_error_code.java
+  Z3_goal_prec.java
+  Z3_lbool.java
+  Z3_param_kind.java
+  Z3_parameter_kind.java
+  Z3_sort_kind.java
+  Z3_symbol_kind.java
+)
+set(Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH "")
+foreach (enum_file ${Z3_JAVA_ENUMERATION_PACKAGE_FILES})
+  list(APPEND Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH
+    "${CMAKE_CURRENT_BINARY_DIR}/enumerations/${enum_file}"
+  )
+endforeach()
+add_custom_command(OUTPUT ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
+  COMMAND "${PYTHON_EXECUTABLE}"
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--java-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+    "--java-package-name"
+    ${Z3_JAVA_PACKAGE_NAME}
+  DEPENDS
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generating ${Z3_JAVA_PACKAGE_NAME}.enumerations package"
+  ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
+)
+
+set(Z3_JAVA_JAR_SOURCE_FILES
+  AlgebraicNum.java
+  ApplyResultDecRefQueue.java
+  ApplyResult.java
+  ArithExpr.java
+  ArithSort.java
+  ArrayExpr.java
+  ArraySort.java
+  ASTDecRefQueue.java
+  AST.java
+  AstMapDecRefQueue.java
+  ASTMap.java
+  AstVectorDecRefQueue.java
+  ASTVector.java
+  BitVecExpr.java
+  BitVecNum.java
+  BitVecSort.java
+  BoolExpr.java
+  BoolSort.java
+  Constructor.java
+  ConstructorList.java
+  Context.java
+  DatatypeExpr.java
+  DatatypeSort.java
+  EnumSort.java
+  Expr.java
+  FiniteDomainExpr.java
+  FiniteDomainNum.java
+  FiniteDomainSort.java
+  FixedpointDecRefQueue.java
+  Fixedpoint.java
+  FPExpr.java
+  FPNum.java
+  FPRMExpr.java
+  FPRMNum.java
+  FPRMSort.java
+  FPSort.java
+  FuncDecl.java
+  FuncInterpDecRefQueue.java
+  FuncInterpEntryDecRefQueue.java
+  FuncInterp.java
+  Global.java
+  GoalDecRefQueue.java
+  Goal.java
+  IDecRefQueue.java
+  IDisposable.java
+  InterpolationContext.java
+  IntExpr.java
+  IntNum.java
+  IntSort.java
+  IntSymbol.java
+  ListSort.java
+  Log.java
+  ModelDecRefQueue.java
+  Model.java
+  OptimizeDecRefQueue.java
+  Optimize.java
+  ParamDescrsDecRefQueue.java
+  ParamDescrs.java
+  ParamsDecRefQueue.java
+  Params.java
+  Pattern.java
+  ProbeDecRefQueue.java
+  Probe.java
+  Quantifier.java
+  RatNum.java
+  RealExpr.java
+  RealSort.java
+  ReExpr.java
+  RelationSort.java
+  ReSort.java
+  SeqExpr.java
+  SeqSort.java
+  SetSort.java
+  SolverDecRefQueue.java
+  Solver.java
+  Sort.java
+  StatisticsDecRefQueue.java
+  Statistics.java
+  Status.java
+  StringSymbol.java
+  Symbol.java
+  TacticDecRefQueue.java
+  Tactic.java
+  TupleSort.java
+  UninterpretedSort.java
+  Version.java
+  Z3Exception.java
+  Z3Object.java
+)
+set(Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "")
+foreach (java_src_file ${Z3_JAVA_JAR_SOURCE_FILES})
+  list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH "${CMAKE_CURRENT_SOURCE_DIR}/${java_src_file}")
+endforeach()
+# Add generated files to list
+list(APPEND Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH
+  ${Z3_JAVA_NATIVE_JAVA}
+  ${Z3_JAVA_ENUMERATION_PACKAGE_FILES_FULL_PATH}
+)
+
+# Convenient top-level target
+add_custom_target(build_z3_java_bindings
+  ALL
+  DEPENDS
+    z3java
+    z3JavaJar
+)
+
+# Rule to build ``com.microsoft.z3.jar``
+# TODO: Should we set ``CMAKE_JNI_TARGET`` to ``TRUE``?
+add_jar(z3JavaJar
+  SOURCES ${Z3_JAVA_JAR_SOURCE_FILES_FULL_PATH}
+  OUTPUT_NAME ${Z3_JAVA_PACKAGE_NAME}
+  OUTPUT_DIR "${CMAKE_BINARY_DIR}"
+  VERSION "${Z3_VERSION}"
+)
+
+###############################################################################
+# Install
+###############################################################################
+option(INSTALL_JAVA_BINDINGS "Install Java bindings when invoking install target" ON)
+if (INSTALL_JAVA_BINDINGS)
+  # Provide cache variables for the install locations that the user can change.
+  # This defaults to ``/usr/local/java`` which seems to be the location for ``.jar``
+  # files on Linux distributions
+  set(Z3_JAVA_JAR_INSTALLDIR
+    "${CMAKE_INSTALL_DATAROOTDIR}/java"
+    CACHE
+    PATH
+    "Directory to install Z3 Java jar file relative to install prefix"
+  )
+  # FIXME: I don't think this the right installation location
+  set(Z3_JAVA_JNI_LIB_INSTALLDIR
+    "${CMAKE_INSTALL_LIBDIR}"
+    CACHE
+    PATH
+    "Directory to install Z3 Java JNI bridge library relative to install prefix"
+  )
+  install(TARGETS z3java DESTINATION "${Z3_JAVA_JNI_LIB_INSTALLDIR}")
+  # Note: Don't use ``DESTINATION`` here as the version of ``UseJava.cmake`` shipped
+  # with CMake 2.8.12.2 handles that incorrectly.
+  install_jar(z3JavaJar "${Z3_JAVA_JAR_INSTALLDIR}")
+endif()

contrib/cmake/src/math/simplex/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(simplex
   SOURCES
     simplex.cpp
+    model_based_opt.cpp
   COMPONENT_DEPENDENCIES
     util
 )

contrib/cmake/src/test/CMakeLists.txt

@@ -61,6 +61,7 @@ add_executable(test-z3
   "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp"
   memory.cpp
   model2expr.cpp
+  model_based_opt.cpp
   model_evaluator.cpp
   model_retrieval.cpp
   mpbq.cpp

scripts/mk_consts_files.py

@@ -17,6 +17,11 @@ def main(args):
     parser.add_argument("api_files", nargs="+")
     parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
     parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None)
+    parser.add_argument("--java-output-dir", dest="java_output_dir", default=None)
+    parser.add_argument("--java-package-name",
+                        dest="java_package_name",
+                        default=None,
+                        help="Name to give the Java package (e.g. ``com.microsoft.z3``).")
     pargs = parser.parse_args(args)
 
     if not mk_genfile_common.check_files_exist(pargs.api_files):
@@ -41,6 +46,20 @@ def main(args):
         logging.info('Generated "{}"'.format(output))
         count += 1
 
+    if pargs.java_output_dir:
+        if pargs.java_package_name == None:
+            logging.error('Java package name must be specified')
+            return 1
+        if not mk_genfile_common.check_dir_exists(pargs.java_output_dir):
+            return 1
+        outputs = mk_genfile_common.mk_z3consts_java_internal(
+            pargs.api_files,
+            pargs.java_package_name,
+            pargs.java_output_dir)
+        for generated_file in outputs:
+            logging.info('Generated "{}"'.format(generated_file))
+        count += 1
+
     if count == 0:
         logging.info('No files generated. You need to specific an output directory'
                      ' for the relevant langauge bindings')

scripts/mk_genfile_common.py

@@ -255,6 +255,116 @@ def mk_z3consts_dotnet_internal(api_files, output_dir):
     z3consts.close()
     return z3consts_output_path
 
+
+def mk_z3consts_java_internal(api_files, package_name, output_dir):
+    """
+        Generate "com.microsoft.z3.enumerations" package from the list of API
+        header files in ``api_files`` and write the package directory into
+        the ``output_dir`` directory
+
+        Returns a list of the generated java source files.
+    """
+    blank_pat      = re.compile("^ *$")
+    comment_pat    = re.compile("^ *//.*$")
+    typedef_pat    = re.compile("typedef enum *")
+    typedef2_pat   = re.compile("typedef enum { *")
+    openbrace_pat  = re.compile("{ *")
+    closebrace_pat = re.compile("}.*;")
+
+    DeprecatedEnums = [ 'Z3_search_failure' ]
+    gendir = os.path.join(output_dir, "enumerations")
+    if not os.path.exists(gendir):
+        os.mkdir(gendir)
+
+    generated_enumeration_files = []
+    for api_file in api_files:
+        api = open(api_file, 'r')
+
+        SEARCHING  = 0
+        FOUND_ENUM = 1
+        IN_ENUM    = 2
+
+        mode    = SEARCHING
+        decls   = {}
+        idx     = 0
+
+        linenum = 1
+        for line in api:
+            m1 = blank_pat.match(line)
+            m2 = comment_pat.match(line)
+            if m1 or m2:
+                # skip blank lines and comments
+                linenum = linenum + 1
+            elif mode == SEARCHING:
+                m = typedef_pat.match(line)
+                if m:
+                    mode = FOUND_ENUM
+                m = typedef2_pat.match(line)
+                if m:
+                    mode = IN_ENUM
+                    decls = {}
+                    idx   = 0
+            elif mode == FOUND_ENUM:
+                m = openbrace_pat.match(line)
+                if m:
+                    mode  = IN_ENUM
+                    decls = {}
+                    idx   = 0
+                else:
+                    assert False, "Invalid %s, line: %s" % (api_file, linenum)
+            else:
+                assert mode == IN_ENUM
+                words = re.split('[^\-a-zA-Z0-9_]+', line)
+                m = closebrace_pat.match(line)
+                if m:
+                    name = words[1]
+                    if name not in DeprecatedEnums:
+                        efile  = open('%s.java' % os.path.join(gendir, name), 'w')
+                        generated_enumeration_files.append(efile.name)
+                        efile.write('/**\n *  Automatically generated file\n **/\n\n')
+                        efile.write('package %s.enumerations;\n\n' % package_name)
+
+                        efile.write('/**\n')
+                        efile.write(' * %s\n' % name)
+                        efile.write(' **/\n')
+                        efile.write('public enum %s {\n' % name)
+                        efile.write
+                        first = True
+                        # Iterate over key-value pairs ordered by value
+                        for k, v in sorted(decls.items(), key=lambda pair: pair[1]):
+                            if first:
+                                first = False
+                            else:
+                                efile.write(',\n')
+                            efile.write('    %s (%s)' % (k, v))
+                        efile.write(";\n")
+                        efile.write('\n    private final int intValue;\n\n')
+                        efile.write('    %s(int v) {\n' % name)
+                        efile.write('        this.intValue = v;\n')
+                        efile.write('    }\n\n')
+                        efile.write('    public static final %s fromInt(int v) {\n' % name)
+                        efile.write('        for (%s k: values()) \n' % name)
+                        efile.write('            if (k.intValue == v) return k;\n')
+                        efile.write('        return values()[0];\n')
+                        efile.write('    }\n\n')
+                        efile.write('    public final int toInt() { return this.intValue; }\n')
+                        #  efile.write(';\n  %s(int v) {}\n' % name)
+                        efile.write('}\n\n')
+                        efile.close()
+                    mode = SEARCHING
+                else:
+                    if words[2] != '':
+                        if len(words[2]) > 1 and words[2][1] == 'x':
+                            idx = int(words[2], 16)
+                        else:
+                            idx = int(words[2])
+                    decls[words[1]] = idx
+                    idx = idx + 1
+            linenum = linenum + 1
+        api.close()
+    return generated_enumeration_files
+
+
 ###############################################################################
 # Functions for generating a "module definition file" for MSVC
 ###############################################################################

scripts/mk_util.py

@@ -2776,109 +2776,19 @@ def mk_z3consts_dotnet(api_files):
 
 # Extract enumeration types from z3_api.h, and add Java definitions
 def mk_z3consts_java(api_files):
-    blank_pat      = re.compile("^ *$")
-    comment_pat    = re.compile("^ *//.*$")
-    typedef_pat    = re.compile("typedef enum *")
-    typedef2_pat   = re.compile("typedef enum { *")
-    openbrace_pat  = re.compile("{ *")
-    closebrace_pat = re.compile("}.*;")
-
     java = get_component(JAVA_COMPONENT)
-
+    full_path_api_files = []
-    DeprecatedEnums = [ 'Z3_search_failure' ]
-    gendir = os.path.join(java.src_dir, "enumerations")
-    if not os.path.exists(gendir):
-        os.mkdir(gendir)
-
     for api_file in api_files:
         api_file_c = java.find_file(api_file, java.name)
         api_file   = os.path.join(api_file_c.src_dir, api_file)
-
+        full_path_api_files.append(api_file)
-        api = open(api_file, 'r')
+    generated_files = mk_genfile_common.mk_z3consts_java_internal(
-
+        full_path_api_files,
-        SEARCHING  = 0
+        java.package_name,
-        FOUND_ENUM = 1
+        java.src_dir)
-        IN_ENUM    = 2
-
-        mode    = SEARCHING
-        decls   = {}
-        idx     = 0
-
-        linenum = 1
-        for line in api:
-            m1 = blank_pat.match(line)
-            m2 = comment_pat.match(line)
-            if m1 or m2:
-                # skip blank lines and comments
-                linenum = linenum + 1
-            elif mode == SEARCHING:
-                m = typedef_pat.match(line)
-                if m:
-                    mode = FOUND_ENUM
-                m = typedef2_pat.match(line)
-                if m:
-                    mode = IN_ENUM
-                    decls = {}
-                    idx   = 0
-            elif mode == FOUND_ENUM:
-                m = openbrace_pat.match(line)
-                if m:
-                    mode  = IN_ENUM
-                    decls = {}
-                    idx   = 0
-                else:
-                    assert False, "Invalid %s, line: %s" % (api_file, linenum)
-            else:
-                assert mode == IN_ENUM
-                words = re.split('[^\-a-zA-Z0-9_]+', line)
-                m = closebrace_pat.match(line)
-                if m:
-                    name = words[1]
-                    if name not in DeprecatedEnums:
-                        efile  = open('%s.java' % os.path.join(gendir, name), 'w')
-                        efile.write('/**\n *  Automatically generated file\n **/\n\n')
-                        efile.write('package %s.enumerations;\n\n' % java.package_name)
-
-                        efile.write('/**\n')
-                        efile.write(' * %s\n' % name)
-                        efile.write(' **/\n')
-                        efile.write('public enum %s {\n' % name)
-                        efile.write
-                        first = True
-                        for k in decls:
-                            i = decls[k]
-                            if first:
-                                first = False
-                            else:
-                                efile.write(',\n')
-                            efile.write('    %s (%s)' % (k, i))
-                        efile.write(";\n")
-                        efile.write('\n    private final int intValue;\n\n')
-                        efile.write('    %s(int v) {\n' % name)
-                        efile.write('        this.intValue = v;\n')
-                        efile.write('    }\n\n')
-                        efile.write('    public static final %s fromInt(int v) {\n' % name)
-                        efile.write('        for (%s k: values()) \n' % name)
-                        efile.write('            if (k.intValue == v) return k;\n')
-                        efile.write('        return values()[0];\n')
-                        efile.write('    }\n\n')
-                        efile.write('    public final int toInt() { return this.intValue; }\n')
-                        #  efile.write(';\n  %s(int v) {}\n' % name)
-                        efile.write('}\n\n')
-                        efile.close()
-                    mode = SEARCHING
-                else:
-                    if words[2] != '':
-                        if len(words[2]) > 1 and words[2][1] == 'x':
-                            idx = int(words[2], 16)
-                        else:
-                            idx = int(words[2])
-                    decls[words[1]] = idx
-                    idx = idx + 1
-            linenum = linenum + 1
-        api.close()
     if VERBOSE:
-        print("Generated '%s'" % ('%s' % gendir))
+        for generated_file in generated_files:
+            print("Generated '{}'".format(generated_file))
 
 # Extract enumeration types from z3_api.h, and add ML definitions
 def mk_z3consts_ml(api_files):

src/ackermannization/ackr_helper.h

@@ -33,20 +33,13 @@ class ackr_helper {
          which are not marked as uninterpreted but effectively are.
         */
         inline bool should_ackermannize(app const * a) const {
-            if (a->get_family_id() == m_bvutil.get_family_id()) {
+            if (is_uninterp(a))
-                switch (a->get_decl_kind()) {
-                    case OP_BSDIV0:
-                    case OP_BUDIV0:
-                    case OP_BSREM0:
-                    case OP_BUREM0:
-                    case OP_BSMOD0:
                 return true;
-                    default:
+            else {
-                        return is_uninterp(a);
+                decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
+                return p->is_considered_uninterpreted(a->get_decl());
             }
         }
-            return (is_uninterp(a));
-        }
 
         inline bv_util& bvutil() { return m_bvutil; }
 

src/api/api_context.cpp

@@ -131,7 +131,7 @@ namespace api {
     }
 
     char * context::mk_external_string(char const * str) {
-        m_string_buffer = str;
+        m_string_buffer = str?str:"";
         return const_cast<char *>(m_string_buffer.c_str());
     }
     

src/api/c++/z3++.h

@@ -1275,6 +1275,51 @@ namespace z3 {
     inline expr udiv(expr const & a, int b) { return udiv(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr udiv(int a, expr const & b) { return udiv(b.ctx().num_val(a, b.get_sort()), b); }
 
+	/**
+		\brief signed reminder operator for bitvectors
+	*/
+	inline expr srem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsrem(a.ctx(), a, b)); }
+	inline expr srem(expr const & a, int b) { return srem(a, a.ctx().num_val(b, a.get_sort())); }
+	inline expr srem(int a, expr const & b) { return srem(b.ctx().num_val(a, b.get_sort()), b); }
+
+	/**
+	\brief unsigned reminder operator for bitvectors
+	*/
+	inline expr urem(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvurem(a.ctx(), a, b)); }
+	inline expr urem(expr const & a, int b) { return urem(a, a.ctx().num_val(b, a.get_sort())); }
+	inline expr urem(int a, expr const & b) { return urem(b.ctx().num_val(a, b.get_sort()), b); }
+
+	/**
+	\brief shift left operator for bitvectors
+	*/
+	inline expr shl(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvshl(a.ctx(), a, b)); }
+	inline expr shl(expr const & a, int b) { return shl(a, a.ctx().num_val(b, a.get_sort())); }
+	inline expr shl(int a, expr const & b) { return shl(b.ctx().num_val(a, b.get_sort()), b); }
+
+	/**
+	\brief logic shift right operator for bitvectors
+	*/
+	inline expr lshr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvlshr(a.ctx(), a, b)); }
+	inline expr lshr(expr const & a, int b) { return lshr(a, a.ctx().num_val(b, a.get_sort())); }
+	inline expr lshr(int a, expr const & b) { return lshr(b.ctx().num_val(a, b.get_sort()), b); }
+
+	/**
+	\brief arithmetic shift right operator for bitvectors
+	*/
+	inline expr ashr(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvashr(a.ctx(), a, b)); }
+	inline expr ashr(expr const & a, int b) { return ashr(a, a.ctx().num_val(b, a.get_sort())); }
+	inline expr ashr(int a, expr const & b) { return ashr(b.ctx().num_val(a, b.get_sort()), b); }
+
+	/**
+	\brief Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
+	*/
+	inline expr zext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_zero_ext(a.ctx(), i, a)); }
+
+	/**
+	\brief Sign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m is the size of the given bit-vector.
+	*/
+	inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); }
+
     template<typename T> class cast_ast;
 
     template<> class cast_ast<ast> {

src/api/dotnet/ArithExpr.cs

@@ -38,5 +38,136 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
         #endregion
+
+        #region Operators
+
+        private static ArithExpr MkNum(ArithExpr e, int i) { return (ArithExpr)e.Context.MkNumeral(i, e.Context.MkIntSort()); }        
+
+        private static ArithExpr MkNum(ArithExpr e, double d) { return (ArithExpr)e.Context.MkNumeral(d.ToString(), e.Context.MkRealSort()); }        
+
+        /// <summary> Operator overloading for arithmetical divsion operator (over reals) </summary>
+        public static ArithExpr operator /(ArithExpr a, ArithExpr b) { return a.Context.MkDiv(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator /(ArithExpr a, int b) { return a / MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator /(ArithExpr a, double b) { return a / MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator /(int a, ArithExpr b) { return MkNum(b, a) / b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator /(double a, ArithExpr b) { return MkNum(b, a) / b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(ArithExpr a) { return a.Context.MkUnaryMinus(a); }        
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(ArithExpr a, ArithExpr b) { return a.Context.MkSub(a, b); }        
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(ArithExpr a, int b) { return a - MkNum(a, b); }        
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(ArithExpr a, double b) { return a - MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(int a, ArithExpr b) { return MkNum(b, a) - b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator -(double a, ArithExpr b) { return MkNum(b, a) - b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(ArithExpr a, ArithExpr b) { return a.Context.MkAdd(a, b); }        
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(ArithExpr a, int b) { return a + MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(ArithExpr a, double b) { return a + MkNum(a, b); }
+ 
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(int a, ArithExpr b) { return MkNum(b, a) + b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator +(double a, ArithExpr b) { return MkNum(b, a) + b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, ArithExpr b) { return a.Context.MkMul(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, int b) { return a * MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(ArithExpr a, double b) { return a * MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(int a, ArithExpr b) { return MkNum(b, a) * b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static ArithExpr operator *(double a, ArithExpr b) { return MkNum(b, a) * b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, ArithExpr b) { return a.Context.MkLe(a, b); }         
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, int b) { return a <= MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(ArithExpr a, double b) { return a <= MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(int a, ArithExpr b) { return MkNum(b, a) <= b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <=(double a, ArithExpr b) { return MkNum(b, a) <= b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, ArithExpr b) { return a.Context.MkLt(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, int b) { return a < MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(ArithExpr a, double b) { return a < MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(int a, ArithExpr b) { return MkNum(b, a) < b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator <(double a, ArithExpr b) { return MkNum(b, a) < b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, ArithExpr b) { return a.Context.MkGt(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, int b) { return a > MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(ArithExpr a, double b) { return a > MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(int a, ArithExpr b) { return MkNum(b, a) > b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >(double a, ArithExpr b) { return MkNum(b, a) > b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, ArithExpr b) { return a.Context.MkGe(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, int b) { return a >= MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(ArithExpr a, double b) { return a >= MkNum(a, b); }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(int a, ArithExpr b) { return MkNum(b, a) >= b; }
+
+        /// <summary> Operator overloading for arithmetical operator </summary>
+        public static BoolExpr operator >=(double a, ArithExpr b) { return MkNum(b, a) >= b; }
+
+        #endregion
     }
 }

src/api/dotnet/BoolExpr.cs

@@ -34,5 +34,20 @@ namespace Microsoft.Z3
         /// <summary> Constructor for BoolExpr </summary>
         internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         #endregion
+
+        #region Operators
+        /// <summary> Disjunction of Boolean expressions </summary>
+        public static BoolExpr operator|(BoolExpr a, BoolExpr b) { return a.Context.MkOr(a, b); }
+
+        /// <summary> Conjunction of Boolean expressions </summary>
+        public static BoolExpr operator &(BoolExpr a, BoolExpr b) { return a.Context.MkAnd(a, b); }
+       
+        /// <summary> Xor of Boolean expressions </summary>
+        public static BoolExpr operator ^(BoolExpr a, BoolExpr b) { return a.Context.MkXor(a, b); }
+       
+        /// <summary> Negation </summary>
+        public static BoolExpr operator !(BoolExpr a) { return a.Context.MkNot(a); }
+
+        #endregion
     }
 }

src/api/dotnet/Context.cs

@@ -21,6 +21,7 @@ using System;
 using System.Collections.Generic;
 using System.Runtime.InteropServices;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Z3
 {
@@ -814,6 +815,20 @@ namespace Microsoft.Z3
             return Expr.Create(this, f, args);
         }
 
+        /// <summary>
+        /// Create a new function application.
+        /// </summary>
+        public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
+        {
+            Contract.Requires(f != null);
+            Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
+            Contract.Ensures(Contract.Result<Expr>() != null);
+
+            CheckContextMatch(f);
+            CheckContextMatch(args);
+            return Expr.Create(this, f, args.ToArray());
+        }
+
         #region Propositional
         /// <summary>
         /// The true Term.
@@ -959,6 +974,18 @@ namespace Microsoft.Z3
             return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t[0] and t[1] and ...</c>.
+        /// </summary>
+        public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+            CheckContextMatch(t);
+            return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
+        }
+
         /// <summary>
         /// Create an expression representing <c>t[0] or t[1] or ...</c>.
         /// </summary>
@@ -973,6 +1000,19 @@ namespace Microsoft.Z3
         }
 
 
+        /// <summary>
+        /// Create an expression representing <c>t[0] or t[1] or ...</c>.
+        /// </summary>
+        public BoolExpr MkOr(IEnumerable<BoolExpr> t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<BoolExpr>() != null);
+
+            CheckContextMatch(t);
+            return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
+        }
+
         #endregion
 
         #region Arithmetic
@@ -989,6 +1029,19 @@ namespace Microsoft.Z3
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
+        /// <summary>
+        /// Create an expression representing <c>t[0] + t[1] + ...</c>.
+        /// </summary>
+        public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
+        {
+            Contract.Requires(t != null);
+            Contract.Requires(Contract.ForAll(t, a => a != null));
+            Contract.Ensures(Contract.Result<ArithExpr>() != null);
+
+            CheckContextMatch(t);
+            return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
+        }
+
         /// <summary>
         /// Create an expression representing <c>t[0] * t[1] * ...</c>.
         /// </summary>
@@ -4743,6 +4796,21 @@ namespace Microsoft.Z3
             }
         }
 
+        [Pure]
+        internal void CheckContextMatch(IEnumerable<Z3Object> arr)
+        {
+            Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
+
+            if (arr != null)
+            {
+                foreach (Z3Object a in arr)
+                {
+                    Contract.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
+                    CheckContextMatch(a);
+                }
+            }
+        }
+
         [ContractInvariantMethod]
         private void ObjectInvariant()
         {

src/api/dotnet/Optimize.cs

@@ -66,6 +66,38 @@ namespace Microsoft.Z3
         /// Assert a constraint (or multiple) into the optimize solver.
         /// </summary>        
         public void Assert(params BoolExpr[] constraints)
+        {
+            AddConstraints(constraints);
+        }
+
+        /// <summary>
+        /// Assert a constraint (or multiple) into the optimize solver.
+        /// </summary>        
+        public void Assert(IEnumerable<BoolExpr> constraints)
+        {
+            AddConstraints(constraints);
+        }
+
+        /// <summary>
+        /// Alias for Assert.
+        /// </summary>        
+        public void Add(params BoolExpr[] constraints)
+        {
+            AddConstraints(constraints);
+        }
+
+        /// <summary>
+        /// Alias for Assert.
+        /// </summary>        
+        public void Add(IEnumerable<BoolExpr> constraints)
+        {
+            AddConstraints(constraints);
+        }
+
+        /// <summary>
+        /// Assert a constraint (or multiple) into the optimize solver.
+        /// </summary>   
+        private void AddConstraints(IEnumerable<BoolExpr> constraints)
         {
             Contract.Requires(constraints != null);
             Contract.Requires(Contract.ForAll(constraints, c => c != null));
@@ -76,15 +108,6 @@ namespace Microsoft.Z3
                 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
             }
         }
-
-        /// <summary>
-        /// Alias for Assert.
-        /// </summary>        
-        public void Add(params BoolExpr[] constraints)
-        {
-            Assert(constraints);
-        }
-
         /// <summary>
         /// Handle to objectives returned by objective functions.
         /// </summary>

src/api/dotnet/Z3Object.cs

@@ -20,6 +20,8 @@ Notes:
 using System;
 using System.Diagnostics.Contracts;
 using System.Threading;
+using System.Collections.Generic;
+using System.Linq;
 
 namespace Microsoft.Z3
 {
@@ -135,6 +137,23 @@ namespace Microsoft.Z3
             return an;
         }
 
+        [Pure]
+        internal static IntPtr[] EnumToNative(IEnumerable<Z3Object> a)
+        {
+            Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
+            Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Count());
+
+            if (a == null) return null;
+            IntPtr[] an = new IntPtr[a.Count()];
+            int i = 0;
+            foreach (var ai in a)
+            {
+                if (ai != null) an[i] = ai.NativeObject;
+                ++i;
+            }
+            return an;
+        }
+
         [Pure]
         internal static uint ArrayLength(Z3Object[] a)
         {

src/api/python/z3.py

@@ -52,7 +52,7 @@ import math
 
 if sys.version < '3':
     def _is_int(v):
-        return isinstance(v, int) or isinstance(v, long)
+        return isinstance(v, (int, long))    
 else:
     def _is_int(v):
         return isinstance(v, int)
@@ -95,7 +95,7 @@ def append_log(s):
 
 def to_symbol(s, ctx=None):
     """Convert an integer or string into a Z3 symbol."""
-    if isinstance(s, int):
+    if _is_int(s):
         return Z3_mk_int_symbol(_get_ctx(ctx).ref(), s)
     else:
         return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
@@ -3627,7 +3627,7 @@ def Extract(high, low, a):
             return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
     if __debug__:
         _z3_assert(low <= high, "First argument must be greater than or equal to second argument")
-        _z3_assert(isinstance(high, int) and high >= 0 and isinstance(low, int) and low >= 0, "First and second arguments must be non negative integers")
+        _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
         _z3_assert(is_bv(a), "Third argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
 
@@ -3849,7 +3849,7 @@ def SignExt(n, a):
     fe
     """
     if __debug__:
-        _z3_assert(isinstance(n, int), "First argument must be an integer")
+        _z3_assert(_is_int(n), "First argument must be an integer")
         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
 
@@ -3876,7 +3876,7 @@ def ZeroExt(n, a):
     8
     """
     if __debug__:
-        _z3_assert(isinstance(n, int), "First argument must be an integer")
+        _z3_assert(_is_int(n), "First argument must be an integer")
         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
 
@@ -3899,7 +3899,7 @@ def RepeatBitVec(n, a):
     aaaa
     """
     if __debug__:
-        _z3_assert(isinstance(n, int), "First argument must be an integer")
+        _z3_assert(_is_int(n), "First argument must be an integer")
         _z3_assert(is_bv(a), "Second argument must be a Z3 Bitvector expression")
     return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
 
@@ -4580,7 +4580,7 @@ class ParamsRef:
         name_sym = to_symbol(name, self.ctx)
         if isinstance(val, bool):
             Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
-        elif isinstance(val, int):
+        elif _is_int(val):
             Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
         elif isinstance(val, float):
             Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
@@ -5627,7 +5627,7 @@ class ModelRef(Z3PPObject):
         x -> 1
         f -> [1 -> 0, else -> 0]
         """
-        if isinstance(idx, int):
+        if _is_int(idx):
             if idx >= len(self):
                 raise IndexError
             num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
@@ -9310,7 +9310,7 @@ def IndexOf(s, substr, offset):
     ctx = _get_ctx2(s, substr, ctx)
     s = _coerce_seq(s, ctx)
     substr = _coerce_seq(substr, ctx)
-    if isinstance(offset, int):
+    if _is_int(offset):
         offset = IntVal(offset, ctx)
     return SeqRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
 

src/api/z3_replayer.cpp

@@ -23,6 +23,7 @@ Notes:
 #include"symbol.h"
 #include"trace.h"
 #include<sstream>
+#include<vector>
 
 void register_z3_replayer_cmds(z3_replayer & in);
 
@@ -46,7 +47,7 @@ struct z3_replayer::imp {
     size_t                   m_ptr;
     size_t_map<void *>       m_heap;
     svector<z3_replayer_cmd> m_cmds;
-    vector<std::string>      m_cmds_names;
+    std::vector<std::string>      m_cmds_names;
 
     enum value_kind { INT64, UINT64, DOUBLE, STRING, SYMBOL, OBJECT, UINT_ARRAY, INT_ARRAY, SYMBOL_ARRAY, OBJECT_ARRAY, FLOAT };
 
@@ -676,7 +677,9 @@ struct z3_replayer::imp {
 
     void register_cmd(unsigned id, z3_replayer_cmd cmd, char const* name) {
         m_cmds.reserve(id+1, 0);
-        m_cmds_names.reserve(id+1, "");
+        while (static_cast<unsigned>(m_cmds_names.size()) <= id+1) {
+            m_cmds_names.push_back("");
+        }
         m_cmds[id] = cmd;
         m_cmds_names[id] = name;
     }

src/ast/fpa/fpa2bv_converter.h

@@ -145,7 +145,7 @@ public:
     expr_ref_vector m_extra_assertions;
 
 protected:
-    void mk_one(func_decl *f, expr_ref sign, expr_ref & result);
+    void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);
 
     void mk_is_nan(expr * e, expr_ref & result);
     void mk_is_inf(expr * e, expr_ref & result);
@@ -184,6 +184,23 @@ protected:
     void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result);
 
     void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result);
+
+private:
+    void mk_nan(sort * s, expr_ref & result);
+    void mk_nzero(sort * s, expr_ref & result);
+    void mk_pzero(sort * s, expr_ref & result);
+    void mk_zero(sort * s, expr_ref & sgn, expr_ref & result);
+    void mk_ninf(sort * s, expr_ref & result);
+    void mk_pinf(sort * s, expr_ref & result);
+
+    void mk_one(sort * s, expr_ref & sign, expr_ref & result);
+    void mk_neg(sort * s, expr_ref & x, expr_ref & result);
+    void mk_add(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
+    void mk_sub(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
+    void mk_mul(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
+    void mk_div(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
+    void mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result);
+    void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
 };
 
 #endif

src/ast/rewriter/bv_trailing.cpp

@@ -194,8 +194,7 @@ struct bv_trailing::imp {
             return 0;
         }
 
-        if (!i) {// all args eaten completely
+        if (!i && !new_last) {// all args eaten completely
-            SASSERT(new_last.get() == NULL);
             SASSERT(retv == m_util.get_bv_size(a));
             result = NULL;
             return retv;
@@ -204,7 +203,7 @@ struct bv_trailing::imp {
         expr_ref_vector new_args(m);
         for (unsigned j = 0; j < i; ++j)
             new_args.push_back(a->get_arg(j));
-        if (new_last.get()) new_args.push_back(new_last);
+        if (new_last) new_args.push_back(new_last);
         result = new_args.size() == 1 ? new_args.get(0)
                                       : m_util.mk_concat(new_args.size(), new_args.c_ptr());
         return retv;
@@ -228,7 +227,7 @@ struct bv_trailing::imp {
         unsigned retv = 0;
         numeral e_val;
         if (m_util.is_numeral(e, e_val, sz)) {
-            retv = remove_trailing(n, e_val);
+            retv = remove_trailing(std::min(n, sz), e_val);
             const unsigned new_sz = sz - retv;
             result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
             return retv;

src/ast/seq_decl_plugin.h

@@ -240,6 +240,8 @@ public:
         app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
         app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); }
         app* mk_char(zstring const& s, unsigned idx);
+        app* mk_itos(expr* i) { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
+        app* mk_stoi(expr* s) { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); }
 
         bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
 

src/cmd_context/cmd_context.cpp

@@ -1322,7 +1322,7 @@ void cmd_context::restore_func_decls(unsigned old_sz) {
         sf_pair const & p = *it;
         erase_func_decl_core(p.first, p.second);
     }
-    m_func_decls_stack.shrink(old_sz);
+    m_func_decls_stack.resize(old_sz);
 }
 
 void cmd_context::restore_psort_decls(unsigned old_sz) {
@@ -1389,7 +1389,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
     if (produce_unsat_cores())
         restore(m(), m_assertion_names, old_sz);
     if (m_interactive_mode)
-        m_assertion_strings.shrink(old_sz);
+        m_assertion_strings.resize(old_sz);
 }
 
 void cmd_context::pop(unsigned n) {
@@ -1724,8 +1724,8 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
 void cmd_context::display_assertions() {
     if (!m_interactive_mode)
         throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
-    vector<std::string>::const_iterator it  = m_assertion_strings.begin();
+    std::vector<std::string>::const_iterator it  = m_assertion_strings.begin();
-    vector<std::string>::const_iterator end = m_assertion_strings.end();
+    std::vector<std::string>::const_iterator end = m_assertion_strings.end();
     regular_stream() << "(";
     for (bool first = true; it != end; ++it) {
         std::string const & s = *it;

src/cmd_context/cmd_context.h

@@ -22,6 +22,7 @@ Notes:
 #define CMD_CONTEXT_H_
 
 #include<sstream>
+#include<vector>
 #include"ast.h"
 #include"ast_printer.h"
 #include"pdecl.h"
@@ -38,6 +39,7 @@ Notes:
 #include"scoped_ptr_vector.h"
 #include"context_params.h"
 
+
 class func_decls {
     func_decl * m_decls;
 public:
@@ -189,7 +191,7 @@ protected:
     // 
     ptr_vector<pdecl>            m_aux_pdecls;
     ptr_vector<expr>             m_assertions;
-    vector<std::string>          m_assertion_strings;
+    std::vector<std::string>     m_assertion_strings;
     ptr_vector<expr>             m_assertion_names; // named assertions are represented using boolean variables.
 
     struct scope {
@@ -270,8 +272,6 @@ public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
     void set_cancel(bool f);
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     context_params  & params() { return m_params; }
     solver_factory &get_solver_factory() { return *m_solver_factory; }
     solver_factory &get_interpolating_solver_factory() { return *m_interpolating_solver_factory; }

src/math/simplex/model_based_opt.cpp

@@ -0,0 +1,452 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    model_based_opt.cpp
+
+Abstract:
+
+    Model-based optimization for linear real arithmetic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-27-4
+
+Revision History:
+
+
+--*/
+
+#include "model_based_opt.h"
+#include "uint_set.h"
+
+std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
+    switch (ie) {
+    case opt::t_eq: return out << " = ";
+    case opt::t_lt: return out << " < ";
+    case opt::t_le: return out << " <= ";        
+    }
+    return out;
+}
+
+
+namespace opt {
+    
+
+    model_based_opt::model_based_opt():
+        m_objective_id(0)
+    {
+        m_rows.push_back(row());
+    }
+
+        
+    bool model_based_opt::invariant() {
+        // variables in each row are sorted.
+        for (unsigned i = 0; i < m_rows.size(); ++i) {
+            if (!invariant(i, m_rows[i])) {
+                return false;
+            }
+        }
+        return true;
+    }
+
+    bool model_based_opt::invariant(unsigned index, row const& r) {
+        rational val = r.m_coeff;
+        vector<var> const& vars = r.m_vars;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            var const& v = vars[i];
+            SASSERT(i + 1 == vars.size() || v.m_id < vars[i+1].m_id);
+            SASSERT(!v.m_coeff.is_zero());
+            val += v.m_coeff * m_var2value[v.m_id];
+        }
+        SASSERT(val == r.m_value);
+        SASSERT(r.m_type != t_eq ||  val.is_zero());
+        SASSERT(index == 0 || r.m_type != t_lt ||  val.is_neg());
+        SASSERT(index == 0 || r.m_type != t_le || !val.is_pos());        
+        return true;
+    }
+        
+    // a1*x + obj 
+    // a2*x + t2 <= 0
+    // a3*x + t3 <= 0
+    // a4*x + t4 <= 0
+    // a1 > 0, a2 > 0, a3 > 0, a4 < 0
+    // x <= -t2/a2
+    // x <= -t2/a3
+    // determine lub among these.
+    // then resolve lub with others
+    // e.g., -t2/a2 <= -t3/a3, then 
+    // replace inequality a3*x + t3 <= 0 by -t2/a2 + t3/a3 <= 0
+    // mark a4 as invalid.
+    // 
+
+    // a1 < 0, a2 < 0, a3 < 0, a4 > 0
+    // x >= t2/a2
+    // x >= t3/a3
+    // determine glb among these
+    // the resolve glb with others.
+    // e.g. t2/a2 >= t3/a3
+    // then replace a3*x + t3 by t3/a3 - t2/a2 <= 0
+    // 
+    inf_eps model_based_opt::maximize() {
+        SASSERT(invariant());
+        unsigned_vector other;
+        unsigned_vector bound_trail, bound_vars;
+        while (!objective().m_vars.empty()) {
+            TRACE("opt", display(tout << "tableau\n"););
+            var v = objective().m_vars.back();
+            unsigned x = v.m_id;
+            rational const& coeff = v.m_coeff;
+            unsigned bound_row_index;
+            rational bound_coeff;
+            other.reset();
+            if (find_bound(x, bound_row_index, bound_coeff, other, coeff.is_pos())) {
+                SASSERT(!bound_coeff.is_zero());
+                for (unsigned i = 0; i < other.size(); ++i) {
+                    resolve(bound_row_index, bound_coeff, other[i], x);
+                }
+                // coeff*x + objective <= ub
+                // a2*x + t2 <= 0
+                // => coeff*x <= -t2*coeff/a2
+                // objective + t2*coeff/a2 <= ub
+
+                mul_add(false, m_objective_id, - coeff/bound_coeff, bound_row_index);
+                m_rows[bound_row_index].m_alive = false;
+                bound_trail.push_back(bound_row_index);
+                bound_vars.push_back(x);
+            }
+            else {
+                return inf_eps::infinity();
+            }
+        }
+
+        //
+        // update the evaluation of variables to satisfy the bound.
+        //
+
+        update_values(bound_vars, bound_trail);
+
+        rational value = objective().m_value;
+        if (objective().m_type == t_lt) {            
+            return inf_eps(inf_rational(value, rational(-1)));
+        }
+        else {
+            return inf_eps(inf_rational(value));
+        }
+    }
+
+
+    void model_based_opt::update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail) {
+        rational eps(0);
+        for (unsigned i = bound_trail.size(); i > 0; ) {
+            --i;
+            unsigned x = bound_vars[i];
+            row& r = m_rows[bound_trail[i]];
+            rational val = r.m_coeff;
+            rational x_val;
+            rational x_coeff;
+            vector<var> const& vars = r.m_vars;
+            for (unsigned j = 0; j < vars.size(); ++j) {
+                var const& v = vars[j];
+                if (x == v.m_id) {
+                    x_coeff = v.m_coeff;
+                }
+                else {
+                    val += m_var2value[v.m_id]*v.m_coeff;
+                }
+            }
+            TRACE("opt", display(tout << "v" << x << " val: " << val 
+                                 << " coeff_x: " << x_coeff << " val_x: " << m_var2value[x] << " ", r); );
+            SASSERT(!x_coeff.is_zero());
+            x_val = -val/x_coeff;
+            //
+            //
+            //     ax + t < 0
+            // <=> x < -t/a
+            // <=> x := -t/a - epsilon
+            // 
+            if (r.m_type == t_lt) {
+                // Adjust epsilon to be 
+                if (!x_val.is_zero() && (eps.is_zero() || eps >= abs(x_val))) {
+                    eps = abs(x_val)/rational(2);
+                }
+                if (!r.m_value.is_zero() && (eps.is_zero() || eps >= abs(r.m_value))) {
+                    eps = abs(r.m_value)/rational(2);
+                }
+
+                SASSERT(!eps.is_zero());
+                if (x_coeff.is_pos()) {
+                    x_val -= eps;
+                }
+                //
+                //     -ax + t < 0 
+                // <=> -ax < -t
+                // <=> -x < -t/a
+                // <=> x > t/a
+                // <=> x := t/a + epsilon
+                //
+                else if (x_coeff.is_neg()) {
+                    x_val += eps;
+                }
+            }
+            m_var2value[x] = x_val;
+            r.m_value = (x_val * x_coeff) + val;
+            
+            TRACE("opt", display(tout << "v" << x << " val: " << val << " coeff_x: " 
+                                 << x_coeff << " val_x: " << m_var2value[x] << " ", r); );
+            SASSERT(invariant(bound_trail[i], r));
+        }        
+    }
+
+    bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, unsigned_vector& other, bool is_pos) {
+        bound_row_index = UINT_MAX;
+        rational lub_val;
+        rational const& x_val = m_var2value[x];
+        unsigned_vector const& row_ids = m_var2row_ids[x];
+        uint_set visited;
+        for (unsigned i = 0; i < row_ids.size(); ++i) {
+            unsigned row_id = row_ids[i];
+            if (visited.contains(row_id)) {
+                continue;
+            }
+            visited.insert(row_id);
+            row& r = m_rows[row_id];
+            if (r.m_alive) {
+                rational a = get_coefficient(row_id, x);
+                if (a.is_zero()) {
+                    // skip
+                }
+                else if (a.is_pos() == is_pos || r.m_type == t_eq) {
+                    rational value = x_val - (r.m_value/a);
+                    if (bound_row_index == UINT_MAX) {
+                        lub_val = value;
+                        bound_row_index = row_id;
+                        bound_coeff = a;
+                    }
+                    else if ((value == lub_val && r.m_type == opt::t_lt) ||
+                             (is_pos && value < lub_val) || 
+                             (!is_pos && value > lub_val)) {
+                        other.push_back(bound_row_index);
+                        lub_val = value;
+                        bound_row_index = row_id;                            
+                        bound_coeff = a;
+                    }
+                    else {
+                        other.push_back(row_id);
+                    }
+                }
+                else {
+                    r.m_alive = false;
+                }
+            }
+        }
+        return bound_row_index != UINT_MAX;
+    }
+        
+    rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) {
+        row const& r = m_rows[row_id];
+        if (r.m_vars.empty()) {
+            return rational::zero();
+        }
+        unsigned lo = 0, hi = r.m_vars.size();
+        while (lo < hi) {
+            unsigned mid = lo + (hi - lo)/2;
+            SASSERT(mid < hi);
+            unsigned id = r.m_vars[mid].m_id;
+            if (id == var_id) {
+                lo = mid;
+                break;
+            }
+            if (id < var_id) {
+                lo = mid + 1;
+            }			
+            else {
+                hi = mid;
+            }
+        }
+        if (lo == r.m_vars.size()) {
+            return rational::zero();
+        }
+        unsigned id = r.m_vars[lo].m_id;
+        if (id == var_id) {
+            return r.m_vars[lo].m_coeff;
+        }
+        else {
+            return rational::zero();
+        }
+    }
+
+    // 
+    // Let
+    //   row1: t1 + a1*x <= 0
+    //   row2: t2 + a2*x <= 0
+    //
+    // assume a1, a2 have the same signs:
+    //       (t2 + a2*x) <= (t1 + a1*x)*a2/a1 
+    //   <=> t2*a1/a2 - t1 <= 0
+    //   <=> t2 - t1*a2/a1 <= 0
+    //
+    // assume a1 > 0, -a2 < 0:
+    //       t1 + a1*x <= 0,  t2 - a2*x <= 0
+    //       t2/a2 <= -t1/a1
+    //       t2 + t1*a2/a1 <= 0
+    // assume -a1 < 0, a2 > 0:
+    //       t1 - a1*x <= 0,  t2 + a2*x <= 0
+    //       t1/a1 <= -t2/a2
+    //       t2 + t1*a2/a1 <= 0
+    // 
+    // the resolvent is the same in all cases (simpler proof should exist)
+    // 
+
+    void model_based_opt::resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) {
+
+        SASSERT(a1 == get_coefficient(row_src, x));
+        SASSERT(!a1.is_zero());
+        SASSERT(row_src != row_dst);
+                
+        if (m_rows[row_dst].m_alive) {
+            rational a2 = get_coefficient(row_dst, x);
+            mul_add(row_dst != m_objective_id && a1.is_pos() == a2.is_pos(), row_dst, -a2/a1, row_src);            
+        }
+    }
+    
+    //
+    // set row1 <- row1 + c*row2
+    //
+    void model_based_opt::mul_add(bool same_sign, unsigned row_id1, rational const& c, unsigned row_id2) {
+        if (c.is_zero()) {
+            return;
+        }
+        m_new_vars.reset();
+        row& r1 = m_rows[row_id1];
+        row const& r2 = m_rows[row_id2];
+        unsigned i = 0, j = 0;
+        for(; i < r1.m_vars.size() || j < r2.m_vars.size(); ) {
+            if (j == r2.m_vars.size()) {
+                m_new_vars.append(r1.m_vars.size() - i, r1.m_vars.c_ptr() + i);
+                break;
+            }
+            if (i == r1.m_vars.size()) {
+                for (; j < r2.m_vars.size(); ++j) {
+                    m_new_vars.push_back(r2.m_vars[j]);
+                    m_new_vars.back().m_coeff *= c;
+                    if (row_id1 != m_objective_id) {
+                        m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1);
+                    }
+                }
+                break;
+            }
+
+            unsigned v1 = r1.m_vars[i].m_id;
+            unsigned v2 = r2.m_vars[j].m_id;
+            if (v1 == v2) {
+                m_new_vars.push_back(r1.m_vars[i]);
+                m_new_vars.back().m_coeff += c*r2.m_vars[j].m_coeff;
+                ++i;
+                ++j;
+                if (m_new_vars.back().m_coeff.is_zero()) {
+                    m_new_vars.pop_back();
+                }
+            }
+            else if (v1 < v2) {
+                m_new_vars.push_back(r1.m_vars[i]);
+                ++i;                        
+            }
+            else {
+                m_new_vars.push_back(r2.m_vars[j]);
+                m_new_vars.back().m_coeff *= c;
+                if (row_id1 != m_objective_id) {
+                    m_var2row_ids[r2.m_vars[j].m_id].push_back(row_id1);
+                }
+                ++j;                        
+            }
+        }
+        r1.m_coeff += c*r2.m_coeff;
+        r1.m_vars.swap(m_new_vars);
+        r1.m_value += c*r2.m_value;
+
+        if (!same_sign && r2.m_type == t_lt) {
+            r1.m_type = t_lt;
+        }
+        else if (same_sign && r1.m_type == t_lt && r2.m_type == t_lt) {
+            r1.m_type = t_le;        
+        }
+        SASSERT(invariant(row_id1, r1));
+    }
+    
+    void model_based_opt::display(std::ostream& out) const {
+        for (unsigned i = 0; i < m_rows.size(); ++i) {
+            display(out, m_rows[i]);
+        }
+        for (unsigned i = 0; i < m_var2row_ids.size(); ++i) {
+            unsigned_vector const& rows = m_var2row_ids[i];
+            out << i << ": ";
+            for (unsigned j = 0; j < rows.size(); ++j) {
+                out << rows[j] << " ";
+            }
+            out << "\n";
+        }
+    }        
+
+    void model_based_opt::display(std::ostream& out, row const& r) const {
+        vector<var> const& vars = r.m_vars;
+        out << (r.m_alive?"+":"-") << " ";
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            if (i > 0 && vars[i].m_coeff.is_pos()) {
+                out << "+ ";
+            }
+            out << vars[i].m_coeff << "* v" << vars[i].m_id << " ";                
+        }
+        if (r.m_coeff.is_pos()) {
+            out << " + " << r.m_coeff << " ";
+        }
+        else if (r.m_coeff.is_neg()) {
+            out << r.m_coeff << " ";
+        }        
+        out << r.m_type << " 0; value: " << r.m_value  << "\n";
+    }
+
+    unsigned model_based_opt::add_var(rational const& value) {
+        unsigned v = m_var2value.size();
+        m_var2value.push_back(value);
+        m_var2row_ids.push_back(unsigned_vector());
+        return v;
+    }
+
+    rational model_based_opt::get_value(unsigned var) {
+        return m_var2value[var];
+    }
+
+    void model_based_opt::set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, ineq_type rel) {
+        row& r = m_rows[row_id];
+        rational val(c);
+        SASSERT(r.m_vars.empty());
+        r.m_vars.append(coeffs.size(), coeffs.c_ptr());
+        std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare());
+        for (unsigned i = 0; i < coeffs.size(); ++i) {
+            val += m_var2value[coeffs[i].m_id] * coeffs[i].m_coeff;
+        }
+        r.m_alive = true;
+        r.m_coeff = c;
+        r.m_value = val;
+        r.m_type = rel;
+        SASSERT(invariant(row_id, r));
+    }
+
+    void model_based_opt::add_constraint(vector<var> const& coeffs, rational const& c, ineq_type rel) {
+        rational val(c);        
+        unsigned row_id = m_rows.size();
+        m_rows.push_back(row());
+        set_row(row_id, coeffs, c, rel);
+        for (unsigned i = 0; i < coeffs.size(); ++i) {
+            m_var2row_ids[coeffs[i].m_id].push_back(row_id); 
+        }
+    }
+
+    void model_based_opt::set_objective(vector<var> const& coeffs, rational const& c) {
+        set_row(m_objective_id, coeffs, c, t_le);
+    }
+
+}
+

src/math/simplex/model_based_opt.h

@@ -0,0 +1,119 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    model_based_opt.h
+
+Abstract:
+
+    Model-based optimization for linear real arithmetic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-27-4
+
+Revision History:
+
+
+--*/
+
+#ifndef __MODEL_BASED_OPT_H__
+#define __MODEL_BASED_OPT_H__
+
+#include "util.h"
+#include "rational.h"
+#include"inf_eps_rational.h"
+
+namespace opt {
+   
+    enum ineq_type {
+        t_eq,
+        t_lt,
+        t_le
+    };
+
+
+    typedef inf_eps_rational<inf_rational> inf_eps;
+    
+    class model_based_opt {
+    public:
+        struct var {
+            unsigned m_id;
+            rational m_coeff;
+            var(unsigned id, rational const& c): m_id(id), m_coeff(c) {}
+            struct compare {
+                bool operator()(var x, var y) {
+                    return x.m_id < y.m_id;
+                }
+            };
+        };
+    private:
+        struct row {
+            row(): m_type(t_le), m_value(0), m_alive(false) {}
+            vector<var> m_vars;         // variables with coefficients
+            rational    m_coeff;        // constant in inequality
+            ineq_type   m_type;         // inequality type
+            rational    m_value;        // value of m_vars + m_coeff under interpretation of m_var2value.
+            bool        m_alive;        // rows can be marked dead if they have been processed.
+        };
+
+        vector<row>             m_rows;
+        unsigned                m_objective_id;
+        vector<unsigned_vector> m_var2row_ids;
+        vector<rational>        m_var2value;
+        vector<var>             m_new_vars;
+        
+        bool invariant();
+        bool invariant(unsigned index, row const& r);
+
+        row& objective() { return m_rows[0]; }        
+
+        bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, unsigned_vector& other, bool is_pos);
+        
+        rational get_coefficient(unsigned row_id, unsigned var_id);
+
+        void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);
+
+        void mul_add(bool same_sign, unsigned row_id1, rational const& c, unsigned row_id2);
+
+        void set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, ineq_type rel);
+        
+        void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);
+
+    public:
+
+        model_based_opt();
+
+        // add a fresh variable with value 'value'.
+        unsigned add_var(rational const& value);
+
+        // retrieve updated value of variable.
+        rational get_value(unsigned var_id);
+
+        // add a constraint. We assume that the constraint is 
+        // satisfied under the values provided to the variables.
+        void add_constraint(vector<var> const& coeffs, rational const& c, ineq_type r);
+
+        // Set the objective function (linear).
+        void set_objective(vector<var> const& coeffs, rational const& c);
+
+        //
+        // find a maximal value for the objective function over the current values.
+        // in other words, the returned maximal value may not be globally optimal,
+        // but the current evaluation of variables are used to select a local
+        // optimal.
+        //
+        inf_eps maximize();
+
+        void display(std::ostream& out) const;
+        void display(std::ostream& out, row const& r) const;
+
+    };
+
+}
+
+std::ostream& operator<<(std::ostream& out, opt::ineq_type ie);
+
+
+#endif 

src/model/func_interp.cpp

@@ -105,8 +105,49 @@ void func_interp::reset_interp_cache() {
     m_interp = 0;
 }
 
+bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
+    args.reset();
+    expr* c, *t, *f, *a0, *a1;
+    if (!m().is_ite(e, c, t, f)) {
+        return false;
+    }
+
+    if ((m_arity == 0) ||
+        (m_arity == 1 && !m().is_eq(c, a0, a1)) ||
+        (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
+        return false;
+
+    args.resize(m_arity, 0);
+    for (unsigned i = 0; i < m_arity; i++) {
+        expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);
+
+        if (!m().is_eq(ci, a0, a1)) 
+            return false;
+
+        if (is_var(a0) && to_var(a0)->get_idx() == i)
+            args[i] = a1;
+        else if (is_var(a1) && to_var(a1)->get_idx() == i)
+            args[i] = a0;
+        else
+            return false;
+    }
+
+    return true;
+}
+
 void func_interp::set_else(expr * e) {
+    if (e == m_else)
+        return;
+
     reset_interp_cache();
+
+    ptr_vector<expr> args;
+    while (e && is_fi_entry_expr(e, args)) {
+        TRACE("func_interp", tout << "fi entry expr: " << mk_ismt2_pp(e, m()) << std::endl;);
+        insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
+        e = to_app(e)->get_arg(2);
+    }
+
     m_manager.inc_ref(e);
     m_manager.dec_ref(m_else);
     m_else = e;

src/model/func_interp.h

@@ -110,6 +110,9 @@ public:
     expr * get_interp() const;
 
     func_interp * translate(ast_translation & translator) const;
+
+private:
+    bool is_fi_entry_expr(expr * e, ptr_vector<expr> & args);
 };
 
 #endif

src/model/model_evaluator.cpp

@@ -118,8 +118,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr * val = m_model.get_const_interp(f);
             if (val != 0) {
                 result = val;
+                expand_value(result);
                 return BR_DONE;
-//                return m().is_value(val)?BR_DONE:BR_REWRITE_FULL;
             }
 
             if (m_model_completion) {
@@ -172,6 +172,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
             st = m_f_rw.mk_app_core(f, num, args, result);
         else if (fid == m_seq_rw.get_fid())
             st = m_seq_rw.mk_app_core(f, num, args, result);
+        else if (fid == m().get_label_family_id() && num == 1) {
+            result = args[0];
+            st = BR_DONE;
+        }
         else if (evaluate(f, num, args, result)) {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
@@ -188,6 +192,21 @@ struct evaluator_cfg : public default_rewriter_cfg {
         return st;
     }
 
+    void expand_value(expr_ref& val) {
+        vector<expr_ref_vector> stores;
+        expr_ref else_case(m());
+        if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case)) {
+            sort* srt = m().get_sort(val);
+            val = m_ar.mk_const_array(srt, else_case);
+            for (unsigned i = stores.size(); i > 0; ) {
+                --i;
+                expr_ref_vector args(m());
+                args.push_back(val);
+                args.append(stores[i].size(), stores[i].c_ptr());
+                val = m_ar.mk_store(args.size(), args.c_ptr());
+            }
+        }        
+    }
 
     bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
 
@@ -306,6 +325,21 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";);
                 return false;
             }
+            bool is_value = true;
+            for (unsigned i = stores.size(); is_value && i > 0; ) {
+                --i;
+                if (else_case == stores[i].back()) {
+                    for (unsigned j = i + 1; j < stores.size(); ++j) {
+                        stores[j-1].reset();
+                        stores[j-1].append(stores[j]);
+                    }
+                    stores.pop_back();
+                    continue;
+                }
+                for (unsigned j = 0; is_value && j + 1 < stores[i].size(); ++j) {
+                    is_value = m().is_value(stores[i][j].get());
+                }
+            }
             TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";);
             return true;
         }
@@ -358,14 +392,10 @@ unsigned model_evaluator::get_num_steps() const {
     return m_imp->get_num_steps();
 }
 
-
 void model_evaluator::cleanup(params_ref const & p) {
     model_core & md = m_imp->cfg().m_model;
-    #pragma omp critical (model_evaluator)
-    {
     dealloc(m_imp);
     m_imp = alloc(imp, md, p);    
-    }
 }
 
 void model_evaluator::reset(params_ref const & p) {

src/muz/base/dl_util.h

@@ -19,6 +19,7 @@ Revision History:
 #ifndef DL_UTIL_H_
 #define DL_UTIL_H_
 
+#include<vector>
 #include"ast.h"
 #include"hashtable.h"
 #include"obj_hashtable.h"
@@ -67,7 +68,7 @@ namespace datalog {
     typedef idx_set var_idx_set;
     typedef u_map<var *> varidx2var_map;
     typedef obj_hashtable<func_decl> func_decl_set; //!< Rule dependencies.
-    typedef vector<std::string> string_vector;
+    typedef std::vector<std::string> string_vector;
     
     bool contains_var(expr * trm, unsigned var_idx);
 

src/opt/opt_context.cpp

@@ -42,6 +42,7 @@ Notes:
 #include "filter_model_converter.h"
 #include "ast_pp_util.h"
 #include "inc_sat_solver.h"
+#include "qsat.h"
 
 namespace opt {
 
@@ -237,6 +238,11 @@ namespace opt {
         import_scoped_state(); 
         normalize();
         internalize();
+#if 0
+        if (is_qsat_opt()) {
+            return run_qsat_opt();
+        }
+#endif
         update_solver();
         solver& s = get_solver();
         s.assert_expr(m_hard_constraints);
@@ -1205,7 +1211,7 @@ namespace opt {
     }
 
     inf_eps context::get_lower_as_num(unsigned idx) {
-        if (idx > m_objectives.size()) {
+        if (idx >= m_objectives.size()) {
             throw default_exception("index out of bounds"); 
         }
         objective const& obj = m_objectives[idx];
@@ -1223,7 +1229,7 @@ namespace opt {
     }
 
     inf_eps context::get_upper_as_num(unsigned idx) {
-        if (idx > m_objectives.size()) {
+        if (idx >= m_objectives.size()) {
             throw default_exception("index out of bounds"); 
         }
         objective const& obj = m_objectives[idx];
@@ -1439,4 +1445,39 @@ namespace opt {
             }       
         } 
     }
+
+    bool context::is_qsat_opt() {
+        if (m_objectives.size() != 1) {
+            return false;
+        }
+        if (m_objectives[0].m_type != O_MAXIMIZE && 
+            m_objectives[0].m_type != O_MINIMIZE) {
+            return false;
+        }
+        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+            if (has_quantifiers(m_hard_constraints[i].get())) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    lbool context::run_qsat_opt() {
+        SASSERT(is_qsat_opt());
+        objective const& obj = m_objectives[0];
+        app_ref term(obj.m_term);
+        if (obj.m_type == O_MINIMIZE) {
+            term = m_arith.mk_uminus(term);
+        }
+        inf_eps value;
+        lbool result = qe::maximize(m_hard_constraints, term, value, m_model, m_params);
+        if (result != l_undef && obj.m_type == O_MINIMIZE) {
+            value.neg();
+        }
+        if (result != l_undef) {
+            m_optsmt.update_lower(obj.m_index, value);
+            m_optsmt.update_upper(obj.m_index, value);
+        }
+        return result;
+    }
 }

src/opt/opt_context.h

@@ -289,12 +289,15 @@ namespace opt {
 
         void display_benchmark();
 
-
         // pareto
         void yield();
         expr_ref mk_ge(expr* t, expr* s);
         expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj);
 
+
+        // quantifiers
+        bool is_qsat_opt();
+        lbool run_qsat_opt();
     };
 
 }

src/opt/optsmt.h

@@ -61,7 +61,9 @@ namespace opt {
         void    get_model(model_ref& mdl, svector<symbol>& labels);
         model*  get_model(unsigned index) const { return m_models[index]; }
 
+
         void update_lower(unsigned idx, inf_eps const& r);
+
         void update_upper(unsigned idx, inf_eps const& r);
 
         void reset();
@@ -82,6 +84,7 @@ namespace opt {
 
         lbool update_upper();
 
+
     };
 
 };

src/parsers/smt2/smt2parser.cpp

@@ -298,7 +298,7 @@ namespace smt2 {
         }
 
         unsigned            m_cache_end;
-        vector<std::string> m_cached_strings;
+        std::vector<std::string> m_cached_strings;
 
         int m_num_open_paren;
 
@@ -403,7 +403,7 @@ namespace smt2 {
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
         void error(unsigned line, unsigned pos, char const * msg) {
-            m_ctx.reset_cancel();
+            m_ctx.set_cancel(false);
             if (use_vs_format()) {
                 m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
                 if (msg[strlen(msg)-1] != '\n')
@@ -2197,7 +2197,7 @@ namespace smt2 {
 
             m_scanner.start_caching();
             m_cache_end = 0;
-            m_cached_strings.reset();
+            m_cached_strings.resize(0);
             
             check_lparen_next("invalid get-value command, '(' expected");
             while (!curr_is_rparen()) {

src/qe/qe_arith.cpp

@@ -20,6 +20,7 @@ Revision History:
 --*/
 
 #include "qe_arith.h"
+#include "qe_mbp.h"
 #include "ast_util.h"
 #include "arith_decl_plugin.h"
 #include "ast_pp.h"
@@ -27,12 +28,12 @@ Revision History:
 #include "expr_functors.h"
 #include "model_v2_pp.h"
 #include "expr_safe_replace.h"
+#include "model_based_opt.h"
 
 namespace qe {
 
     bool is_divides(arith_util& a, expr* e1, expr* e2, rational& k, expr_ref& p) {  
         expr* t1, *t2;
-        ast_manager& m = a.get_manager();
         if (a.is_mod(e2, t1, t2) && 
             a.is_numeral(e1, k) && 
             k.is_zero() &&
@@ -51,19 +52,21 @@ namespace qe {
         return is_divides(a, e1, e2, k, t) || is_divides(a, e2, e1, k, t);
     }
 
+
+#if 0
+        obj_map<expr, unsigned> m_expr2var;
+        ptr_vector<expr>        m_var2expr;
+
+#endif
+    
     struct arith_project_plugin::imp {
 
-        enum ineq_type {
-            t_eq,
-            t_lt,
-            t_le
-        };
         ast_manager&      m;
         arith_util        a;
         th_rewriter       m_rw;
         expr_ref_vector   m_ineq_terms;
         vector<rational>  m_ineq_coeffs;
-        svector<ineq_type>  m_ineq_types;
+        svector<opt::ineq_type>  m_ineq_types;
         expr_ref_vector   m_div_terms;
         vector<rational>  m_div_divisors, m_div_coeffs;
         expr_ref_vector   m_new_lits;
@@ -85,6 +88,111 @@ namespace qe {
             }            
         }
 
+        void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts)
+        {
+            rational w;
+            if (ts.find(x, w)) {
+                ts.insert(x, w + v);
+            }
+            else {
+                ts.insert(x, v); 
+            }
+        }
+
+        void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map<expr, unsigned>& tids) {
+            obj_map<expr, rational> ts;
+            rational c(0), mul(1);
+            expr_ref t(m);
+            opt::ineq_type ty = opt::t_le;
+            expr* e1, *e2;
+            bool is_not = m.is_not(lit, lit);
+            if (is_not) {
+                mul.neg();
+            }
+            SASSERT(!m.is_not(lit));
+            if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
+                if (is_not) mul.neg();
+                linearize(model, mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = is_not ? opt::t_lt : opt::t_le;
+            }
+            else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
+                if (is_not) mul.neg();
+                linearize(model,  mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = is_not ? opt::t_le: opt::t_lt;
+            }
+            else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
+                linearize(model,  mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = opt::t_eq;
+            }  
+            else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
+                UNREACHABLE();
+            }
+            else if (m.is_distinct(lit) && is_not && is_arith(to_app(lit)->get_arg(0))) {
+                UNREACHABLE();
+            }
+            else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) {
+                UNREACHABLE();
+            }            
+            else {
+                return;
+            }
+            if (ty == opt::t_lt && is_int()) {
+                c += rational(1);
+                ty = opt::t_le;
+            }            
+            vars coeffs;
+            extract_coefficients(ts, tids, coeffs);
+            mbo.add_constraint(coeffs, c, ty);
+        }
+
+        void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map<expr, rational>& ts) {
+            expr* t1, *t2, *t3;
+            rational mul1;
+            expr_ref val(m);
+            if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) {
+                linearize(model, mul* mul1, t2, c, ts);
+            }
+            else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) {
+                linearize(model, mul* mul1, t1, c, ts);
+            }
+            else if (a.is_add(t)) {
+                app* ap = to_app(t);
+                for (unsigned i = 0; i < ap->get_num_args(); ++i) {
+                    linearize(model, mul, ap->get_arg(i), c, ts);
+                }
+            }
+            else if (a.is_sub(t, t1, t2)) {
+                linearize(model, mul, t1, c, ts);
+                linearize(model, -mul, t2, c, ts);
+            }
+            else if (a.is_uminus(t, t1)) {
+                linearize(model, -mul, t1, c, ts);
+            }
+            else if (a.is_numeral(t, mul1)) {
+                c += mul*mul1;
+            }
+            else if (extract_mod(model, t, val)) {
+                insert_mul(val, mul, ts);
+            }
+            else if (m.is_ite(t, t1, t2, t3)) {
+                VERIFY(model.eval(t1, val));
+                SASSERT(m.is_true(val) || m.is_false(val));
+                TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
+                if (m.is_true(val)) {
+                    linearize(model, mul, t2, c, ts);
+                }
+                else {
+                    linearize(model, mul, t3, c, ts);
+                }
+            }
+            else {
+                insert_mul(t, mul, ts);
+            }
+        }
+
         void is_linear(model& model, rational const& mul, expr* t, rational& c, expr_ref_vector& ts) {
             expr* t1, *t2, *t3;
             rational mul1;
@@ -120,6 +228,7 @@ namespace qe {
             else if (m.is_ite(t, t1, t2, t3)) {                
                 VERIFY(model.eval(t1, val));
                 SASSERT(m.is_true(val) || m.is_false(val));
+                TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
                 if (m.is_true(val)) {
                     is_linear(model, mul, t2, c, ts); 
                 }
@@ -140,7 +249,7 @@ namespace qe {
         bool is_linear(model& model, expr* lit, bool& found_eq) {
             rational c(0), mul(1);
             expr_ref t(m);
-            ineq_type ty = t_le;
+            opt::ineq_type ty = opt::t_le;
             expr* e1, *e2;
             expr_ref_vector ts(m);            
             bool is_not = m.is_not(lit, lit);
@@ -151,17 +260,17 @@ namespace qe {
             if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
                 is_linear(model,  mul, e1, c, ts);
                 is_linear(model, -mul, e2, c, ts);
-                ty = is_not?t_lt:t_le;
+                ty = is_not? opt::t_lt : opt::t_le;
             }
             else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
                 is_linear(model,  mul, e1, c, ts);
                 is_linear(model, -mul, e2, c, ts);
-                ty = is_not?t_le:t_lt;
+                ty = is_not? opt::t_le: opt::t_lt;
             }
             else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
                 is_linear(model,  mul, e1, c, ts);
                 is_linear(model, -mul, e2, c, ts);
-                ty = t_eq;
+                ty = opt::t_eq;
             }  
             else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
                 expr_ref val(m);
@@ -180,7 +289,7 @@ namespace qe {
                     is_linear(model,  mul, nums[i+1].first, c, ts);
                     is_linear(model, -mul, nums[i].first,   c, ts);  
                     t = add(ts);
-                    accumulate_linear(model, c, t, t_lt);
+                    accumulate_linear(model, c, t, opt::t_lt);
                 }
                 t = mk_num(0);
                 c.reset();
@@ -199,7 +308,7 @@ namespace qe {
                 if (r1 < r2) {
                     std::swap(e1, e2);
                 }                
-                ty = t_lt;
+                ty = opt::t_lt;
                 is_linear(model,  mul, e1, c, ts);
                 is_linear(model, -mul, e2, c, ts);    
             }
@@ -207,24 +316,24 @@ namespace qe {
                 TRACE("qe", tout << "can't project:" << mk_pp(lit, m) << "\n";);
                 throw cant_project();
             }
-            if (ty == t_lt && is_int()) {
+            if (ty == opt::t_lt && is_int()) {
                 ts.push_back(mk_num(1));
-                ty = t_le;
+                ty = opt::t_le;
             }
             t = add(ts);
-            if (ty == t_eq && c.is_neg()) {
+            if (ty == opt::t_eq && c.is_neg()) {
                 t = mk_uminus(t);
                 c.neg();
             }
-            if (ty == t_eq && c > rational(1)) {
+            if (ty == opt::t_eq && c > rational(1)) {
                 m_ineq_coeffs.push_back(-c);
                 m_ineq_terms.push_back(mk_uminus(t));
-                m_ineq_types.push_back(t_le);
+                m_ineq_types.push_back(opt::t_le);
                 m_num_neg++;
-                ty = t_le;
+                ty = opt::t_le;
             }
             accumulate_linear(model, c, t, ty);
-            found_eq = !c.is_zero() && ty == t_eq;
+            found_eq = !c.is_zero() && ty == opt::t_eq;
             return true;
         }
 
@@ -275,16 +384,16 @@ namespace qe {
             }
         };
 
-        void accumulate_linear(model& model, rational const& c, expr_ref& t, ineq_type ty) {
+        void accumulate_linear(model& model, rational const& c, expr_ref& t, opt::ineq_type ty) {
             if (c.is_zero()) {
                 switch (ty) {
-                case t_eq:
+                case opt::t_eq:
                     t = a.mk_eq(t, mk_num(0));
                     break;
-                case t_lt:
+                case opt::t_lt:
                     t = a.mk_lt(t, mk_num(0));
                     break;
-                case t_le:
+                case opt::t_le:
                     t = a.mk_le(t, mk_num(0));
                     break;
                 }
@@ -294,7 +403,7 @@ namespace qe {
                 m_ineq_coeffs.push_back(c);
                 m_ineq_terms.push_back(t);
                 m_ineq_types.push_back(ty);
-                if (ty == t_eq) {
+                if (ty == opt::t_eq) {
                     // skip
                 }
                 else if (c.is_pos()) {
@@ -404,18 +513,18 @@ namespace qe {
 
         expr* ineq_term(unsigned i) const { return m_ineq_terms[i]; }
         rational const& ineq_coeff(unsigned i) const { return m_ineq_coeffs[i]; }
-        ineq_type ineq_ty(unsigned i) const { return m_ineq_types[i]; }
+        opt::ineq_type ineq_ty(unsigned i) const { return m_ineq_types[i]; }
         app_ref mk_ineq_pred(unsigned i) { 
             app_ref result(m);
             result = to_app(mk_add(mk_mul(ineq_coeff(i), m_var->x()), ineq_term(i)));
             switch (ineq_ty(i)) {
-            case t_lt:
+            case opt::t_lt:
                 result = a.mk_lt(result, mk_num(0));
                 break;
-            case t_le:
+            case opt::t_le:
                 result = a.mk_le(result, mk_num(0));
                 break;
-            case t_eq:
+            case opt::t_eq:
                 result = m.mk_eq(result, mk_num(0));
                 break;
             }
@@ -424,9 +533,9 @@ namespace qe {
         void display_ineq(std::ostream& out, unsigned i) const {
             out << mk_pp(ineq_term(i), m) << " " << ineq_coeff(i) << "*" << mk_pp(m_var->x(), m);
             switch (ineq_ty(i)) {
-            case t_eq: out <<  " = 0\n"; break;
+            case opt::t_eq: out <<  " = 0\n"; break;
-            case t_le: out << " <= 0\n"; break;
+            case opt::t_le: out << " <= 0\n"; break;
-            case t_lt: out <<  " < 0\n"; break;
+            case opt::t_lt: out <<  " < 0\n"; break;
             }
         }
         unsigned num_ineqs() const { return m_ineq_terms.size(); }
@@ -541,7 +650,7 @@ namespace qe {
             bool is_int = a.is_int(m_var->x());
             for (unsigned i = 0; i < num_ineqs(); ++i) {
                 rational const& ac = m_ineq_coeffs[i];
-                SASSERT(!is_int || t_le == ineq_ty(i));
+                SASSERT(!is_int || opt::t_le == ineq_ty(i));
 
                 //
                 // ac*x + t < 0
@@ -555,7 +664,7 @@ namespace qe {
                     new_max =
                         new_max || 
                         (r > max_r) || 
-                        (r == max_r && t_lt == ineq_ty(i)) ||
+                        (r == max_r && opt::t_lt == ineq_ty(i)) ||
                         (r == max_r && is_int && ac.is_one());
                     TRACE("qe", tout << "max: "  << mk_pp(ineq_term(i), m) << "/" << abs(ac) << " := " << r << " " 
                           << (new_max?"":"not ") << "new max\n";);
@@ -593,7 +702,7 @@ namespace qe {
             expr_ref ts = mk_add(bt, as);
             expr_ref  z = mk_num(0);
             expr_ref  fml(m);
-            if (t_lt == ineq_ty(i) || t_lt == ineq_ty(j)) {
+            if (opt::t_lt == ineq_ty(i) || opt::t_lt == ineq_ty(j)) {
                 fml = a.mk_lt(ts, z);
             }
             else {
@@ -610,7 +719,7 @@ namespace qe {
             rational ac = ineq_coeff(i);
             rational bc = ineq_coeff(j);
             expr_ref tmp(m);
-            SASSERT(t_le == ineq_ty(i) && t_le == ineq_ty(j));
+            SASSERT(opt::t_le == ineq_ty(i) && opt::t_le == ineq_ty(j));
             SASSERT(ac.is_pos() == bc.is_neg());
             rational abs_a = abs(ac);
             rational abs_b = abs(bc);
@@ -689,7 +798,7 @@ namespace qe {
             expr* s = ineq_term(j);
             expr_ref bt = mk_mul(abs(bc), t);
             expr_ref as = mk_mul(abs(ac), s);
-            if (t_lt == ineq_ty(i) && t_le == ineq_ty(j)) {
+            if (opt::t_lt == ineq_ty(i) && opt::t_le == ineq_ty(j)) {
                 return expr_ref(a.mk_lt(bt, as), m);
             }
             else {
@@ -760,9 +869,9 @@ namespace qe {
                     expr_ref lhs(m), val(m);
                     lhs = mk_sub(mk_mul(c, ineq_term(i)), mk_mul(ineq_coeff(i), t));
                     switch (ineq_ty(i)) {
-                    case t_lt: lhs = a.mk_lt(lhs, mk_num(0)); break;
+                    case opt::t_lt: lhs = a.mk_lt(lhs, mk_num(0)); break;
-                    case t_le: lhs = a.mk_le(lhs, mk_num(0)); break;
+                    case opt::t_le: lhs = a.mk_le(lhs, mk_num(0)); break;
-                    case t_eq: lhs = m.mk_eq(lhs, mk_num(0)); break;
+                    case opt::t_eq: lhs = m.mk_eq(lhs, mk_num(0)); break;
                     }
                     TRACE("qe", tout << lhs << "\n";);
                     SASSERT (model.eval(lhs, val) && m.is_true(val));
@@ -853,6 +962,78 @@ namespace qe {
             }
             return true;
         }
+
+        typedef opt::model_based_opt::var var;
+        typedef vector<var> vars;
+        
+
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+            SASSERT(a.is_real(t));
+            opt::model_based_opt mbo;
+            opt::inf_eps value;
+            obj_map<expr, rational> ts;
+            obj_map<expr, unsigned> tids;
+
+            // extract objective function.
+            vars coeffs;
+            rational c(0), mul(1);
+            linearize(mdl, mul, t, c, ts);
+            extract_coefficients(ts, tids, coeffs);
+            mbo.set_objective(coeffs, c);
+
+            // extract linear constraints
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                linearize(mdl, mbo, fmls[i], tids);
+            }
+            
+            // find optimal value
+            value = mbo.maximize();
+
+            expr_ref val(a.mk_numeral(value.get_rational(), false), m);
+            if (!value.is_finite()) {
+                bound = m.mk_false();
+                return value;
+            }
+
+            // update model to use new values that satisfy optimality
+            ptr_vector<expr> vars;
+            obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
+            for (; it != end; ++it) {
+                expr* e = it->m_key;
+                if (is_uninterp_const(e)) {
+                    unsigned id = it->m_value;
+                    func_decl* f = to_app(e)->get_decl();
+                    expr_ref val(a.mk_numeral(mbo.get_value(id), false), m);
+                    mdl.register_decl(f, val);
+                }
+                else {
+                    TRACE("qe", tout << "omitting model update for non-uninterpreted constant " << mk_pp(e, m) << "\n";);
+                }
+            }
+
+            // update the predicate 'bound' which forces larger values.
+            if (value.get_infinitesimal().is_neg()) {
+                bound = a.mk_le(val, t);
+            }
+            else {
+                bound = a.mk_lt(val, t);
+            }            
+            return value;
+        }
+
+        void extract_coefficients(obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
+            coeffs.reset();
+            obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
+            for (; it != end; ++it) {
+                unsigned id;
+                if (!tids.find(it->m_key, id)) {
+                    id = tids.size();
+                    tids.insert(it->m_key, id);
+                }
+                coeffs.push_back(var(id, it->m_value));                
+            }
+        }
+
     };
 
     arith_project_plugin::arith_project_plugin(ast_manager& m) {
@@ -875,6 +1056,10 @@ namespace qe {
         return m_imp->a.get_family_id();
     }
 
+    opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+        return m_imp->maximize(fmls, mdl, t, bound);
+    }
+
     bool arith_project(model& model, app* var, expr_ref_vector& lits) {
         ast_manager& m = lits.get_manager();
         arith_project_plugin ap(m);

src/qe/qe_arith.h

@@ -29,6 +29,8 @@ namespace qe {
         virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits);
         virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
         virtual family_id get_family_id();
+
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound);
     };
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits);

src/qe/qe_datatypes.cpp

@@ -87,7 +87,6 @@ namespace qe {
         }
 
         void project_rec(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-            func_decl* f = m_val->get_decl();
             expr_ref rhs(m);
             expr_ref_vector eqs(m);
             for (unsigned i = 0; i < lits.size(); ++i) {

src/qe/qe_mbp.cpp

@@ -107,6 +107,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
 class mbp::impl {
     ast_manager& m;
     ptr_vector<project_plugin> m_plugins;
+    expr_mark m_visited;
 
     void add_plugin(project_plugin* p) {
         family_id fid = p->get_family_id();
@@ -175,12 +176,53 @@ class mbp::impl {
         return false;
     }
 
+
+    void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) {
+        TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
+        ptr_vector<expr> todo;
+        if (is_app(fml)) {
+            todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
+        }
+        while (!todo.empty()) {
+            expr* e = todo.back();
+            todo.pop_back();
+            if (m_visited.is_marked(e)) {
+                continue;
+            }
+            m_visited.mark(e);
+            if (m.is_bool(e)) {
+                expr_ref val(m);
+                VERIFY(model.eval(e, val));
+                TRACE("qe", tout << "found: " << mk_pp(e, m) << "\n";);
+                if (m.is_true(val)) {
+                    fmls.push_back(e);
+                }
+                else {
+                    fmls.push_back(mk_not(m, e));
+                }
+            }
+            else if (is_app(e)) {
+                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            }
+            else {
+                TRACE("qe", tout << "expression not handled " << mk_pp(e, m) << "\n";);
+            }
+        }
+    }
+
 public:
 
+
+    opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+        arith_project_plugin arith(m);
+        return arith.maximize(fmls, mdl, t, bound);
+    }
+
     void extract_literals(model& model, expr_ref_vector& fmls) {
         expr_ref val(m);
         for (unsigned i = 0; i < fmls.size(); ++i) {
             expr* fml = fmls[i].get(), *nfml, *f1, *f2, *f3;
+            SASSERT(m.is_bool(fml));
             if (m.is_not(fml, nfml) && m.is_distinct(nfml)) {
                 fmls[i] = project_plugin::pick_equality(m, model, nfml);
                 --i;
@@ -205,26 +247,28 @@ public:
                     f1 = mk_not(m, f1);
                     f2 = mk_not(m, f2);
                 }
-                project_plugin::push_back(fmls, f1);
+                fmls[i] = f1;
                 project_plugin::push_back(fmls, f2);
-                project_plugin::erase(fmls, i);
+                --i;
             }
             else if (m.is_implies(fml, f1, f2)) {
                 VERIFY (model.eval(f2, val));
                 if (m.is_true(val)) {
-                    project_plugin::push_back(fmls, f2);
+                    fmls[i] = f2;
                 }
                 else {
-                    project_plugin::push_back(fmls, mk_not(m, f1));
+                    fmls[i] = mk_not(m, f1);
                 }
-                project_plugin::erase(fmls, i);
+                --i;
             }
             else if (m.is_ite(fml, f1, f2, f3)) {
                 VERIFY (model.eval(f1, val));                
                 if (m.is_true(val)) {
+                    project_plugin::push_back(fmls, f1);
                     project_plugin::push_back(fmls, f2);
                 }
                 else {
+                    project_plugin::push_back(fmls, mk_not(m, f1));
                     project_plugin::push_back(fmls, f3);
                 }
                 project_plugin::erase(fmls, i);
@@ -269,17 +313,24 @@ public:
             else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
                 VERIFY (model.eval(f1, val));                
                 if (m.is_true(val)) {
+                    project_plugin::push_back(fmls, f1);
                     project_plugin::push_back(fmls, mk_not(m, f2));
                 }
                 else {
+                    project_plugin::push_back(fmls, mk_not(m, f1));
                     project_plugin::push_back(fmls, mk_not(m, f3));
                 }
                 project_plugin::erase(fmls, i);
             }
+            else if (m.is_not(fml, nfml)) {
+                extract_bools(model, fmls, nfml);
+            }
             else {
+                extract_bools(model, fmls, fml);
                 // TBD other Boolean operations.
             }
         }
+        m_visited.reset();
     }
 
     impl(ast_manager& m):m(m) {
@@ -310,6 +361,7 @@ public:
         app_ref var(m);
         th_rewriter rw(m);
         bool progress = true;
+        TRACE("qe", tout << vars << " " << fmls << "\n";);
         while (progress && !vars.empty()) {
             preprocess_solve(model, vars, fmls);
             app_ref_vector new_vars(m);
@@ -345,6 +397,7 @@ public:
             }
             vars.append(new_vars);
         }
+        TRACE("qe", tout << vars << " " << fmls << "\n";);
     }
 };
     
@@ -367,3 +420,7 @@ void mbp::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
 void mbp::extract_literals(model& model, expr_ref_vector& lits) {
     m_impl->extract_literals(model, lits);
 }
+
+opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+    return m_impl->maximize(fmls, mdl, t, bound);
+}

src/qe/qe_mbp.h

@@ -24,6 +24,7 @@ Revision History:
 #include "ast.h"
 #include "params.h"
 #include "model.h"
+#include "model_based_opt.h"
 
 
 namespace qe {
@@ -70,6 +71,12 @@ namespace qe {
            Extract literals from formulas based on model.
          */
         void extract_literals(model& model, expr_ref_vector& lits);
+
+        /**
+           \brief 
+           Maximize objective t under current model for constraints in fmls.
+         */
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound);
     };
 }
 

src/qe/qsat.cpp

@@ -31,6 +31,8 @@ Notes:
 #include "expr_abstract.h"
 #include "qe.h"
 #include "label_rewriter.h"
+#include "expr_replacer.h"
+#include "th_rewriter.h"
 
 
 namespace qe {
@@ -535,6 +537,13 @@ namespace qe {
         }
     };
 
+    enum qsat_mode {
+        qsat_qe,
+        qsat_qe_rec,
+        qsat_sat,
+        qsat_maximize
+    };
+    
     class qsat : public tactic {
         
         struct stats {
@@ -557,8 +566,7 @@ namespace qe {
         vector<app_ref_vector>     m_vars;       // variables from alternating prefixes.
         unsigned                   m_level;
         model_ref                  m_model;
-        bool                       m_qelim;       // perform quantifier elimination
+        qsat_mode                  m_mode;
-        bool                       m_force_elim;  // force elimination of variables during projection.
         app_ref_vector             m_avars;       // variables to project
         app_ref_vector             m_free_vars;
 
@@ -587,7 +595,7 @@ namespace qe {
                     switch (m_level) {
                     case 0: return l_false;
                     case 1: 
-                        if (!m_qelim) return l_true; 
+                        if (m_mode == qsat_sat) return l_true; 
                         if (m_model.get()) {
                             project_qe(asms);
                         }
@@ -670,20 +678,23 @@ namespace qe {
             m_pred_abs.get_free_vars(fml, vars);
             m_vars.push_back(vars);
             vars.reset();
-            if (m_qelim) {
+            if (m_mode != qsat_sat) {
                 is_forall = true;
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.push_back(vars);
+                filter_vars(vars);
             }
             else {
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.back().append(vars);
+                filter_vars(vars);
             }
             do {
                 is_forall = !is_forall;
                 vars.reset();
                 hoist.pull_quantifier(is_forall, fml, vars);
                 m_vars.push_back(vars);
+                filter_vars(vars);
             }
             while (!vars.empty());
             SASSERT(m_vars.back().empty()); 
@@ -691,6 +702,101 @@ namespace qe {
             TRACE("qe", tout << fml << "\n";);
         }
 
+        void filter_vars(app_ref_vector const& vars) {
+            for (unsigned i = 0; i < vars.size(); ++i) {
+                m_pred_abs.fmc()->insert(vars[i]->get_decl());
+            }
+        }
+
+#if 0
+        void hoist_ite(expr_ref& fml) {
+            app* ite;
+            scoped_ptr<expr_replacer> replace = mk_default_expr_replacer(m);
+            th_rewriter rewriter(m);
+            while (find_ite(fml, ite)) {
+                expr* cond, *th, *el;
+                VERIFY(m.is_ite(ite, cond, th, el));
+                expr_ref tmp1(fml, m), tmp2(fml, m);
+                replace->apply_substitution(cond, m.mk_true(), tmp1);
+                replace->apply_substitution(cond, m.mk_false(), tmp2);
+                fml = m.mk_ite(cond, tmp1, tmp2);
+                rewriter(fml);
+            }
+        }
+
+        bool find_ite(expr* e, app*& ite) {
+            ptr_vector<expr> todo;
+            todo.push_back(e);
+            ast_mark visited;
+            while(!todo.empty()) {
+                e = todo.back();
+                todo.pop_back();
+                if (visited.is_marked(e)) {
+                    continue;
+                }        
+                visited.mark(e, true);
+                if (m.is_ite(e) && !m.is_bool(e)) {
+                    ite = to_app(e);
+                    return true;
+                }
+                if (is_app(e)) {
+                    app* a = to_app(e);
+                    todo.append(a->get_num_args(), a->get_args());
+                }
+            }
+            return false;
+        }
+
+        // slower
+        void hoist_ite2(expr_ref& fml) {
+            obj_map<expr,expr*> result;
+            expr_ref_vector trail(m);
+            ptr_vector<expr> todo, args;
+            todo.push_back(fml);
+            
+            while (!todo.empty()) {
+                expr* e = todo.back();
+                if (result.contains(e)) {
+                    todo.pop_back();
+                    continue;
+                }
+                if (!is_app(e)) {
+                    todo.pop_back();
+                    result.insert(e, e);
+                    continue;
+                }
+                app* a = to_app(e);
+                expr* r;
+                unsigned sz = a->get_num_args();
+                args.reset();
+                for (unsigned i = 0; i < sz; ++i) {
+                    if (result.find(a->get_arg(i), r)) {
+                        args.push_back(r);
+                    }
+                    else {
+                        todo.push_back(a->get_arg(i));
+                    }
+                }
+                if (sz == args.size()) {
+                    r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
+                    trail.push_back(r);
+                    if (m.is_bool(e) && m.get_basic_family_id() != a->get_family_id()) {
+                        expr_ref fml(r, m);
+                        hoist_ite(fml);
+                        trail.push_back(fml);
+                        r = fml;
+                    }
+                    result.insert(e, r);
+                    todo.pop_back();
+                }                               
+            }
+            fml = result.find(fml);
+        }
+#endif
+
+
+        
+
         void initialize_levels() {
             // initialize levels.
             for (unsigned i = 0; i < m_vars.size(); ++i) {
@@ -758,13 +864,19 @@ namespace qe {
             get_core(core, m_level);
             SASSERT(validate_core(core));
             get_vars(m_level);
-            m_mbp(m_force_elim, m_avars, mdl, core);
+            m_mbp(force_elim(), m_avars, mdl, core);
+            if (m_mode == qsat_maximize) {
+                maximize(core, mdl);
+                pop(1);
+            }
+            else {
                 fml = negate_core(core);
                 add_assumption(fml);
                 m_answer.push_back(fml);
                 m_free_vars.append(m_avars);
                 pop(1);
             }
+        }
                 
         void project(expr_ref_vector& core) {
             get_core(core, m_level);
@@ -778,7 +890,7 @@ namespace qe {
             
             get_vars(m_level-1);
             SASSERT(validate_project(mdl, core));
-            m_mbp(m_force_elim, m_avars, mdl, core);
+            m_mbp(force_elim(), m_avars, mdl, core);
             m_free_vars.append(m_avars);
             fml = negate_core(core);
             unsigned num_scopes = 0;
@@ -789,7 +901,7 @@ namespace qe {
             if (level.max() == UINT_MAX) {
                 num_scopes = 2*(m_level/2);
             }
-            else if (m_qelim && !m_force_elim) {
+            else if (m_mode == qsat_qe_rec) {
                 num_scopes = 2;
             }
             else {
@@ -803,7 +915,7 @@ namespace qe {
             
             pop(num_scopes); 
             TRACE("qe", tout << "backtrack: " << num_scopes << " new level: " << m_level << "\nproject:\n" << core << "\n|->\n" << fml << "\n";);
-            if (m_level == 0 && m_qelim) {
+            if (m_level == 0 && m_mode != qsat_sat) {
                 add_assumption(fml);
             }
             else {
@@ -819,10 +931,14 @@ namespace qe {
             }
         } 
         
-        expr_ref negate_core(expr_ref_vector& core) {
+        expr_ref negate_core(expr_ref_vector const& core) {
             return ::push_not(::mk_and(core));
         }
 
+        bool force_elim() const {
+            return m_mode != qsat_qe_rec;
+        }
+        
         expr_ref elim_rec(expr* fml) {
             expr_ref tmp(m);
             expr_ref_vector     trail(m);
@@ -941,7 +1057,7 @@ namespace qe {
             expr_ref_vector fmls(m);
             fmls.append(core.size(), core.c_ptr());
             fmls.append(k.size(), k.get_formulas());
-            return check_fmls(fmls);
+            return check_fmls(fmls) || m.canceled();
         }
 
         bool check_fmls(expr_ref_vector const& fmls) {
@@ -953,7 +1069,7 @@ namespace qe {
             lbool is_sat = solver.check();
             CTRACE("qe", is_sat != l_false, 
                    tout << fmls << "\nare not unsat\n";);
-            return (is_sat == l_false);
+            return (is_sat == l_false) || m.canceled();
         }
 
         bool validate_model(expr_ref_vector const& asms) {
@@ -967,7 +1083,7 @@ namespace qe {
         bool validate_model(model& mdl, unsigned sz, expr* const* fmls) {
             expr_ref val(m);
             for (unsigned i = 0; i < sz; ++i) {
-                if (!m_model->eval(fmls[i], val)) {
+                if (!m_model->eval(fmls[i], val) && !m.canceled()) {
                     TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";);
                     return false;
                 } 
@@ -1001,6 +1117,9 @@ namespace qe {
                 TRACE("qe", tout << "Projection is false in model\n";);
                 return false;
             }
+            if (m.canceled()) {
+                return true;
+            }
             for (unsigned i = 0; i < m_avars.size(); ++i) {
                 contains_app cont(m, m_avars[i].get());
                 if (cont(proj)) {
@@ -1029,9 +1148,10 @@ namespace qe {
             return true;
         }
 
+
     public:
         
-        qsat(ast_manager& m, params_ref const& p, bool qelim, bool force_elim):
+        qsat(ast_manager& m, params_ref const& p, qsat_mode mode):
             m(m),
             m_mbp(m),
             m_fa(m),
@@ -1040,8 +1160,7 @@ namespace qe {
             m_answer(m),
             m_asms(m),
             m_level(0),
-            m_qelim(qelim),
+            m_mode(mode),
-            m_force_elim(force_elim),
             m_avars(m),
             m_free_vars(m)
         {
@@ -1070,13 +1189,15 @@ namespace qe {
             expr_ref fml(m);
             mc = 0; pc = 0; core = 0;
             in->get_formulas(fmls);
+
+
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             
             // for now:
             // fail if cores.  (TBD)
             // fail if proofs. (TBD)
             
-            if (!m_force_elim) {
+            if (m_mode == qsat_qe_rec) {
                 fml = elim_rec(fml);
                 in->reset();
                 in->inc_depth();
@@ -1087,10 +1208,11 @@ namespace qe {
                 
             reset();
             TRACE("qe", tout << fml << "\n";);
-            if (m_qelim) {
+            if (m_mode != qsat_sat) {
                 fml = push_not(fml);
             }
             hoist(fml);
+//            hoist_ite(fml); redundant provided theories understand to deal with ite terms.
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
             m_ex.assert_expr(mk_and(defs));
@@ -1104,11 +1226,12 @@ namespace qe {
             case l_false:
                 in->reset();
                 in->inc_depth();
-                if (m_qelim) {
+                if (m_mode == qsat_qe) {
                     fml = ::mk_and(m_answer);
                     in->assert_expr(fml);
                 }
                 else {
+                    SASSERT(m_mode == qsat_sat);
                     in->assert_expr(m.mk_false());
                 }
                 result.push_back(in.get());
@@ -1155,13 +1278,93 @@ namespace qe {
         }
         
         tactic * translate(ast_manager & m) {
-            return alloc(qsat, m, m_params, m_qelim, m_force_elim);
+            return alloc(qsat, m, m_params, m_mode);
         }        
+
+        app*             m_objective;
+        opt::inf_eps     m_value;
+        bool             m_was_sat;
+
+        lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) {
+            expr_ref_vector defs(m);
+            expr_ref fml = negate_core(fmls);
+            hoist(fml);
+            m_objective = t;
+            m_value = opt::inf_eps();
+            m_was_sat = false;
+            m_pred_abs.abstract_atoms(fml, defs);
+            fml = m_pred_abs.mk_abstract(fml);
+            m_ex.assert_expr(mk_and(defs));
+            m_fa.assert_expr(mk_and(defs));
+            m_ex.assert_expr(fml);
+            m_fa.assert_expr(m.mk_not(fml));
+            lbool is_sat = check_sat();
+            mdl = m_model.get();
+            switch (is_sat) {
+            case l_false:
+                if (!m_was_sat) {
+                    return l_false;
+                }
+                break;
+            case l_true:
+                UNREACHABLE();
+                break;
+            case l_undef:
+                std::string s = m_ex.k().last_failure_as_string();
+                if (s == "ok") {
+                    s = m_fa.k().last_failure_as_string();
+                }
+                throw tactic_exception(s.c_str()); 
+            }        
+            value = m_value;
+            return l_true;
+        }
+
+        void maximize(expr_ref_vector const& core, model& mdl) {
+            TRACE("qe", tout << "maximize: " << core << "\n";);
+            m_was_sat |= !core.empty();
+            expr_ref bound(m);
+            m_value = m_mbp.maximize(core, mdl, m_objective, bound);
+            m_ex.assert_expr(bound);            
+        }
+
     };
 
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) {
+        ast_manager& m = fmls.get_manager();
+        qsat qs(m, p, qsat_maximize);
+        return qs.maximize(fmls, t, mdl, value);
+    }    
+};
+
+tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
+    return alloc(qe::qsat, m, p, qe::qsat_sat);
+}
+
+tactic * mk_qe2_tactic(ast_manager& m, params_ref const& p) {   
+    return alloc(qe::qsat, m, p, qe::qsat_qe);
+}
+
+tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) {   
+    return alloc(qe::qsat, m, p, qe::qsat_qe_rec);
+}
 
 
 
+
+#if 0
+
+    class min_max_opt {
+        struct imp;
+        imp* m_imp;
+    public:
+        min_max_opt(ast_manager& m);
+        ~min_max_opt();
+        void add(expr* e);
+        void add(expr_ref_vector const& fmls);
+        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
+    };
+
     struct min_max_opt::imp {
         ast_manager&    m;
         expr_ref_vector m_fmls;
@@ -1239,20 +1442,4 @@ namespace qe {
         return m_imp->check(is_max, vars, t);
     }
 
-
+#endif
-    
-};
-
-tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
-    return alloc(qe::qsat, m, p, false, true);
-}
-
-tactic * mk_qe2_tactic(ast_manager& m, params_ref const& p) {   
-    return alloc(qe::qsat, m, p, true, true);
-}
-
-tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) {   
-    return alloc(qe::qsat, m, p, true, false);
-}
-
-

src/qe/qsat.h

@@ -23,6 +23,7 @@ Revision History:
 
 #include "tactic.h"
 #include "filter_model_converter.h"
+#include "qe_mbp.h"
 
 namespace qe {
 
@@ -113,17 +114,7 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
-    class min_max_opt {
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
-        struct imp;
-        imp* m_imp;
-    public:
-        min_max_opt(ast_manager& m);
-        ~min_max_opt();
-        void add(expr* e);
-        void add(expr_ref_vector const& fmls);
-        lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
-    };
-
 
 }
 

src/sat/tactic/goal2sat.cpp

@@ -324,6 +324,7 @@ struct goal2sat::imp {
     }
     
     void process(expr * n) {
+        //SASSERT(m_result_stack.empty());
         TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
         if (visit(n, true, false)) {
             SASSERT(m_result_stack.empty());
@@ -342,8 +343,7 @@ struct goal2sat::imp {
             bool sign  = fr.m_sign;
             TRACE("goal2sat_bug", tout << "result stack\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             if (fr.m_idx == 0 && process_cached(t, root, sign)) {
                 m_frame_stack.pop_back();
                 continue;
@@ -362,11 +362,11 @@ struct goal2sat::imp {
             }
             TRACE("goal2sat_bug", tout << "converting\n";
                   tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
-                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << m_result_stack << "\n";);
-                  tout << "\n";);
             convert(t, root, sign);
             m_frame_stack.pop_back();
         }
+        CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
         SASSERT(m_result_stack.empty());
     }
 

src/smt/smt_model_finder.cpp

@@ -1756,16 +1756,16 @@ namespace smt {
 
             void insert_qinfo(qinfo * qi) {
                 // I'm assuming the number of qinfo's per quantifier is small. So, the linear search is not a big deal.
+                scoped_ptr<qinfo> q(qi);
                 ptr_vector<qinfo>::iterator it  = m_qinfo_vect.begin();            
                 ptr_vector<qinfo>::iterator end = m_qinfo_vect.end();            
                 for (; it != end; ++it) {
                     checkpoint();
                     if (qi->is_equal(*it)) {
-                        dealloc(qi);
                         return;
                     }
                 }
-                m_qinfo_vect.push_back(qi);
+                m_qinfo_vect.push_back(q.detach());
                 TRACE("model_finder", tout << "new quantifier qinfo: "; qi->display(tout); tout << "\n";);
             }
 

src/smt/theory_seq.cpp

@@ -202,6 +202,7 @@ theory_seq::theory_seq(ast_manager& m):
     m_exclude(m),
     m_axioms(m),
     m_axioms_head(0),
+    m_int_string(m),
     m_mg(0),
     m_rewrite(m),
     m_seq_rewrite(m),
@@ -257,6 +258,11 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>fixed_length\n";);
         return FC_CONTINUE;
     }
+    if (check_int_string()) {
+        ++m_stats.m_int_string;
+        TRACE("seq", tout << ">>int_string\n";);
+        return FC_CONTINUE;
+    }
     if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() ||  branch_variable()) {
         ++m_stats.m_branch_variable;
         TRACE("seq", tout << ">>branch_variable\n";);
@@ -292,7 +298,6 @@ final_check_status theory_seq::final_check_eh() {
 
 bool theory_seq::reduce_length_eq() {
     context& ctx = get_context();
-    unsigned sz = m_eqs.size();
     int start = ctx.get_random_value();
 
     for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) {
@@ -451,7 +456,6 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
 }
 
 bool theory_seq::branch_variable_mb() {
-    context& ctx = get_context();
     bool change = false;
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
         eq const& e = m_eqs[i];
@@ -2160,6 +2164,7 @@ void theory_seq::add_length(expr* e) {
     m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_length, e));
 }
 
+
 /*
   ensure that all elements in equivalence class occur under an applicatin of 'length'
 */
@@ -2177,6 +2182,48 @@ void theory_seq::enforce_length(enode* n) {
     while (n1 != n);
 }
 
+
+void theory_seq::add_int_string(expr* e) {
+    m_int_string.push_back(e);
+    m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_int_string));
+}
+
+bool theory_seq::check_int_string() {
+    bool change = false;
+    for (unsigned i = 0; i < m_int_string.size(); ++i) {
+        expr* e = m_int_string[i].get(), *n;
+        if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
+            change = true;
+        }
+        else if (m_util.str.is_stoi(e, n)) {
+            // not (yet) handled.
+            // we would check that in the current proto-model
+            // the string at 'n', when denoting integer would map to the
+            // proper integer.
+        }
+    }
+    return change;
+}
+
+bool theory_seq::add_itos_axiom(expr* e) {
+    rational val;
+    expr* n;
+    VERIFY(m_util.str.is_itos(e, n));
+    if (get_value(n, val)) {
+        if (!m_itos_axioms.contains(val)) {
+            m_itos_axioms.insert(val);
+
+            app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);            
+            expr_ref n1(arith_util(m).mk_numeral(val, true), m);
+            add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false));
+            m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
+            m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
+            return true;
+        }            
+    }
+    return false;
+}
+
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
     mk_var(n);
 }
@@ -2317,6 +2364,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq add axiom", m_stats.m_add_axiom);
     st.update("seq extensionality", m_stats.m_extensionality);
     st.update("seq fixed length", m_stats.m_fixed_length);
+    st.update("seq int.to.str", m_stats.m_int_string);
 }
 
 void theory_seq::init_model(expr_ref_vector const& es) {
@@ -2627,6 +2675,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_string(n)) {
         add_elim_string_axiom(n);
     }
+    else if (m_util.str.is_itos(n)) {
+        add_itos_axiom(n);
+    }
 }
 
 
@@ -2890,6 +2941,14 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
     }
 }
 
+bool theory_seq::get_value(expr* e, rational& val) const {
+    context& ctx = get_context();
+    theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
+    expr_ref _val(m);
+    if (!tha || !tha->get_value(ctx.get_enode(e), _val)) return false;
+    return m_autil.is_numeral(_val, val) && val.is_int();
+}
+
 bool theory_seq::lower_bound(expr* _e, rational& lo) const {
     context& ctx = get_context();
     expr_ref e(m_util.str.mk_length(_e), m);
@@ -3525,6 +3584,11 @@ void theory_seq::relevant_eh(app* n) {
         enque_axiom(n);
     }
 
+    if (m_util.str.is_itos(n) ||
+        m_util.str.is_stoi(n)) {
+        add_int_string(n);
+    }
+
     expr* arg;
     if (m_util.str.is_length(n, arg) && !has_length(arg)) {
         enforce_length(get_context().get_enode(arg));

src/smt/theory_seq.h

@@ -287,7 +287,10 @@ namespace smt {
             unsigned m_extensionality;
             unsigned m_fixed_length;
             unsigned m_propagate_contains;
+            unsigned m_int_string;
         };
+        typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
+
         ast_manager&               m;
         dependency_manager         m_dm;
         solution_map               m_rep;        // unification representative.
@@ -303,6 +306,8 @@ namespace smt {
         obj_hashtable<expr>        m_axiom_set;
         unsigned                   m_axioms_head; // index of first axiom to add.
         bool            m_incomplete;             // is the solver (clearly) incomplete for the fragment.
+        expr_ref_vector     m_int_string;
+        rational_set        m_itos_axioms;
         obj_hashtable<expr> m_length;             // is length applied
         scoped_ptr_vector<apply> m_replay;        // set of actions to replay
         model_generator* m_mg;
@@ -481,9 +486,14 @@ namespace smt {
         bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
         void enforce_length_coherence(enode* n1, enode* n2);
 
+        // model-check the functions that convert integers to strings and the other way.
+        void add_int_string(expr* e);
+        bool check_int_string();
+
         void add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
         void add_in_re_axiom(expr* n);
+        bool add_itos_axiom(expr* n);
         literal mk_literal(expr* n);
         literal mk_eq_empty(expr* n, bool phase = true);
         literal mk_seq_eq(expr* a, expr* b);
@@ -496,6 +506,7 @@ namespace smt {
 
 
         // arithmetic integration
+        bool get_value(expr* s, rational& val) const;
         bool lower_bound(expr* s, rational& lo) const;
         bool upper_bound(expr* s, rational& hi) const;
         bool get_length(expr* s, rational& val) const;

src/solver/combined_solver.cpp

@@ -83,9 +83,14 @@ private:
         solver *        m_solver;
         volatile bool   m_canceled;
         aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
+        ~aux_timeout_eh() {
+            if (m_canceled) {                
+                m_solver->get_manager().limit().dec_cancel();
+            }
+        }
         virtual void operator()() {
-            m_solver->get_manager().limit().cancel();
             m_canceled = true;
+            m_solver->get_manager().limit().inc_cancel();
         }
     };
 
@@ -225,9 +230,6 @@ public:
                 if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
                     return r;
                 }
-                if (eh.m_canceled) {
-                    m_solver1->get_manager().limit().reset_cancel();
-                }
             }
             IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
         }

src/tactic/arith/eq2bv_tactic.cpp

@@ -191,15 +191,18 @@ public:
             expr* c = it->m_key;
             bool strict;
             rational r;
-            if (m_bounds.has_lower(c, r, strict)) {
+            expr_ref fml(m);
+            if (m_bounds.has_lower(c, r, strict) && !r.is_neg()) {
                 SASSERT(!strict);
                 expr* d = m_fd.find(c);
-                g->assert_expr(bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d), m_bounds.lower_dep(c));
+                fml = bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d);
+                g->assert_expr(fml, m_bounds.lower_dep(c));
             }
-            if (m_bounds.has_upper(c, r, strict)) {
+            if (m_bounds.has_upper(c, r, strict) && !r.is_neg()) {
                 SASSERT(!strict);
                 expr* d = m_fd.find(c);
-                g->assert_expr(bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d))), m_bounds.upper_dep(c));
+                fml = bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d)));
+                g->assert_expr(fml, m_bounds.upper_dep(c));
             }
         }        
         g->inc_depth();
@@ -247,6 +250,7 @@ public:
             }
             unsigned p = next_power_of_two(it->m_value);            
             if (p <= 1) p = 2;
+            if (it->m_value == p) p *= 2;
             unsigned n = log2(p);
             app* z = m.mk_fresh_const("z", bv.mk_sort(n));
             m_trail.push_back(z);

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -25,6 +25,7 @@ Notes:
 #include"ast_pp.h"
 #include"bvarray2uf_rewriter.h"
 #include"rewriter_def.h"
+#include"ref_util.h"
 
 // [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
 //     Quantified Bit-Vector Formulas, in Formal Methods in System Design,
@@ -50,10 +51,7 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con
 }
 
 bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
-    for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
+    dec_ref_map_key_values(m_manager, m_arrays_fs);
-    it != m_arrays_fs.end();
-        it++)
-        m_manager.dec_ref(it->m_value);
 }
 
 void bvarray2uf_rewriter_cfg::reset() {}
@@ -110,12 +108,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
     if (m_array_util.is_as_array(e))
         return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
     else {
-        app * a = to_app(e);
         func_decl * bv_f = 0;
         if (!m_arrays_fs.find(e, bv_f)) {
-            sort * domain = get_index_sort(a);
+            sort * domain = get_index_sort(e);
-            sort * range = get_value_sort(a);
+            sort * range = get_value_sort(e);
             bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
+            TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " new func_decl is " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(to_app(e)->get_decl(),
@@ -124,8 +122,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
             else if (m_fmc)
                 m_fmc->insert(bv_f);
             m_arrays_fs.insert(e, bv_f);
+            m_manager.inc_ref(e);
             m_manager.inc_ref(bv_f);
         }
+        else {
+            TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " found " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
+        }
 
         return func_decl_ref(bv_f, m_manager);
     }
@@ -138,6 +140,11 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         SASSERT(num == 2);
         // From [1]: Finally, we replace equations of the form t = s,
         // where t and s are arrays, with \forall x . f_t(x) = f_s(x).
+        if (m_manager.are_equal(args[0], args[1])) {
+            result = m_manager.mk_true();
+            res = BR_DONE;
+        }
+        else {
             func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
             func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
 
@@ -151,6 +158,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
             result = m_manager.mk_forall(1, sorts, names, body);
             res = BR_DONE;
         }
+    }
     else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
         result = m_manager.mk_distinct_expanded(num, args);
         res = BR_REWRITE1;
@@ -310,7 +318,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         }
     }
 
-    CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
+    CTRACE("bvarray2uf_rw", res == BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
     return res;
 }
 

src/tactic/bv/bvarray2uf_tactic.cpp

@@ -62,7 +62,6 @@ class bvarray2uf_tactic : public tactic {
             SASSERT(g->is_well_sorted());
             tactic_report report("bvarray2uf", *g);
             mc = 0; pc = 0; core = 0; result.reset();
-            fail_if_proof_generation("bvarray2uf", g);
             fail_if_unsat_core_generation("bvarray2uf", g);
 
             TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
@@ -73,7 +72,6 @@ class bvarray2uf_tactic : public tactic {
                 filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
                 mc = concat(emc, fmc);
                 m_rw.set_mcs(emc, fmc);
-
             }
 
 
@@ -86,10 +84,10 @@ class bvarray2uf_tactic : public tactic {
                     break;
                 expr * curr = g->form(idx);
                 m_rw(curr, new_curr, new_pr);
-                //if (m_produce_proofs) {
+                if (m_produce_proofs) {
-                //    proof * pr = g->pr(idx);
+                    proof * pr = g->pr(idx);
-                //    new_pr = m.mk_modus_ponens(pr, new_pr);
+                    new_pr = m_manager.mk_modus_ponens(pr, new_pr);
-                //}
+                }
                 g->update(idx, new_curr, new_pr, g->dep(idx));
             }
 

src/tactic/extension_model_converter.cpp

@@ -43,41 +43,6 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
     }
 }
 
-bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args) {
-    args.reset();
-    if (!is_app(e) || !m().is_ite(to_app(e)))
-        return false;
-
-    app * a = to_app(e);
-    expr * c = a->get_arg(0);
-    expr * t = a->get_arg(1);
-    expr * f = a->get_arg(2);
-
-    if ((arity == 0) ||
-        (arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||
-        (arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity)))
-        return false;
-
-    args.resize(arity, 0);
-    for (unsigned i = 0; i < arity; i++) {
-        expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i);
-
-        if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2)
-            return false;
-
-        expr * a0 = to_app(ci)->get_arg(0);
-        expr * a1 = to_app(ci)->get_arg(1);
-        if (is_var(a0) && to_var(a0)->get_idx() == i)
-            args[i] = a1;
-        else if (is_var(a1) && to_var(a1)->get_idx() == i)
-            args[i] = a0;
-        else
-            return false;
-    }
-
-    return true;
-}
-
 void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
     SASSERT(goal_idx == 0);
     TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
@@ -97,14 +62,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
         }
         else {
             func_interp * new_fi = alloc(func_interp, m(), arity);
-            expr * e = val.get();
+            new_fi->set_else(val);
-            ptr_vector<expr> args;
-            while (is_fi_entry_expr(e, arity, args)) {
-                TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;);
-                new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
-                e = to_app(e)->get_arg(2);
-            }
-            new_fi->set_else(e);
             md->register_decl(f, new_fi);
         }
     }

src/tactic/extension_model_converter.h

@@ -43,9 +43,6 @@ public:
     void insert(func_decl * v, expr * def);
 
     virtual model_converter * translate(ast_translation & translator);
-
-private:
-    bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args);
 };
 
 

src/tactic/goal.cpp

@@ -136,7 +136,7 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
     }
 }
 
-void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
+void goal::quick_process(bool save_first, expr_ref& f, expr_dependency * d) {
     if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
         if (!save_first) {
             push_back(f, 0, d);
@@ -145,6 +145,7 @@ void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
     }
     typedef std::pair<expr *, bool> expr_pol;
     sbuffer<expr_pol, 64> todo;
+    expr_ref_vector tmp_exprs(m());
     todo.push_back(expr_pol(f, true));
     while (!todo.empty()) {
         if (m_inconsistent)
@@ -173,8 +174,10 @@ void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
             todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
         }
         else {
-            if (!pol) 
+            if (!pol) {
                 curr = m().mk_not(curr);                
+                tmp_exprs.push_back(curr);
+            }
             if (save_first) {
                 f = curr;
                 save_first = false;
@@ -239,8 +242,10 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
         return;
     if (proofs_enabled())
         slow_process(f, pr, d);
-    else
+    else {
-        quick_process(false, f, d);
+        expr_ref fr(f, m());
+        quick_process(false, fr, d);
+    }
 }
 
 void goal::assert_expr(expr * f, expr_dependency * d) {
@@ -276,13 +281,14 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
         }
     }
     else {
-        quick_process(true, f, d);
+        expr_ref fr(f, m());
+        quick_process(true, fr, d);
         if (!m_inconsistent) {
-            if (m().is_false(f)) {
+            if (m().is_false(fr)) {
                 push_back(f, 0, d);
             }
             else {
-                m().set(m_forms, i, f);
+                m().set(m_forms, i, fr);
                 if (unsat_core_enabled())
                     m().set(m_dependencies, i, d);
             }

src/tactic/goal.h

@@ -62,7 +62,7 @@ protected:
     unsigned              m_precision:2;       // PRECISE, UNDER, OVER.
 
     void push_back(expr * f, proof * pr, expr_dependency * d);
-    void quick_process(bool save_first, expr * & f, expr_dependency * d);
+    void quick_process(bool save_first, expr_ref & f, expr_dependency * d);
     void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
     void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
     void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);

src/tactic/smtlogics/quant_tactics.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
+#include"elim_term_ite_tactic.h"
 
 static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
     params_ref pull_ite_p;
@@ -112,6 +113,7 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
                                    ));
 #else
     tactic * st = and_then(mk_quant_preprocessor(m),
+                           mk_qe_lite_tactic(m, p),
                            or_else(mk_qsat_tactic(m, p),
                                    and_then(mk_qe_tactic(m), mk_smt_tactic())));
 #endif

src/test/main.cpp

@@ -186,6 +186,7 @@ int main(int argc, char ** argv) {
     TST(smt_context);
     TST(theory_dl);
     TST(model_retrieval);
+    TST(model_based_opt);
     TST(factor_rewriter);
     TST(smt2print_parse);
     TST(substitution);

src/test/model_based_opt.cpp

@@ -0,0 +1,227 @@
+#include "model_based_opt.h"
+#include "util.h"
+#include "uint_set.h"
+
+typedef opt::model_based_opt::var var;
+
+static void add_ineq(opt::model_based_opt& mbo, unsigned x, int a, int k, opt::ineq_type rel) {
+    vector<var> vars;
+    vars.push_back(var(x, rational(a)));
+    mbo.add_constraint(vars, rational(k), rel);
+}
+
+static void add_ineq(opt::model_based_opt& mbo, 
+                     unsigned x, int a, 
+                     unsigned y, int b, int k, 
+                     opt::ineq_type rel) {
+    vector<var> vars;
+    vars.push_back(var(x, rational(a)));
+    vars.push_back(var(y, rational(b)));
+    mbo.add_constraint(vars, rational(k), rel);
+}
+
+static void add_ineq(opt::model_based_opt& mbo, 
+                     unsigned x, int a, 
+                     unsigned y, int b, 
+                     unsigned z, int c, int k, 
+                     opt::ineq_type rel) {
+    vector<var> vars;
+    vars.push_back(var(x, rational(a)));
+    vars.push_back(var(y, rational(b)));
+    vars.push_back(var(z, rational(c)));
+    mbo.add_constraint(vars, rational(k), rel);
+}
+
+static void add_random_ineq(opt::model_based_opt& mbo,
+                            random_gen& r,
+                            svector<int>  const& values,
+                            unsigned max_vars,
+                            unsigned max_coeff) {
+    unsigned num_vars = values.size();
+    uint_set used_vars;
+    vector<var> vars;
+    int value = 0;
+    for (unsigned i = 0; i < max_vars; ++i) {
+        unsigned x = r(num_vars);
+        if (used_vars.contains(x)) {
+            continue;
+        }
+        used_vars.insert(x);
+        int coeff = r(max_coeff + 1);
+        if (coeff == 0) {
+            continue;
+        }
+        unsigned sign = r(2);
+		coeff = sign == 0 ? coeff : -coeff;
+        vars.push_back(var(x, rational(coeff)));
+        value += coeff*values[x];
+    }
+    unsigned abs_value = value < 0 ? - value : value;
+    // value + k <= 0
+    // k <= - value
+    // range for k is 2*|value|
+    // k <= - value - range
+    opt::ineq_type rel = opt::t_le;
+
+    int coeff = 0;
+    if (r(4) == 0) {
+        rel = opt::t_eq;
+        coeff = -value;
+    }
+    else {
+        if (abs_value > 0) {
+            coeff = -value - r(2*abs_value);
+        }
+        else {
+            coeff = 0;
+        }
+        if (coeff != -value && r(3) == 0) {
+            rel = opt::t_lt;
+        }   
+    }
+    mbo.add_constraint(vars, rational(coeff), rel);
+}
+                        
+static void check_random_ineqs(random_gen& r, unsigned num_vars, unsigned max_value, unsigned num_ineqs, unsigned max_vars, unsigned max_coeff) {
+    opt::model_based_opt mbo;
+    svector<int> values;
+    for (unsigned i = 0; i < num_vars; ++i) {
+        values.push_back(r(max_value + 1));
+        mbo.add_var(rational(values.back()));
+    }
+    for (unsigned i = 0; i < num_ineqs; ++i) {
+        add_random_ineq(mbo, r, values, max_vars, max_coeff);
+    }
+
+    vector<var> vars;
+    vars.reset();
+    vars.push_back(var(0, rational(2)));
+    vars.push_back(var(1, rational(-2)));
+    mbo.set_objective(vars, rational(0));
+
+    mbo.display(std::cout);
+    opt::inf_eps value = mbo.maximize();    
+    std::cout << "optimal: " << value << "\n";
+    mbo.display(std::cout);
+    for (unsigned i = 0; i < values.size(); ++i) {
+        std::cout << i << ": " << values[i] << " -> " << mbo.get_value(i) << "\n";
+    }
+}
+
+static void check_random_ineqs() {
+    random_gen r(1);
+
+    for (unsigned i = 0; i < 1009; ++i) {
+        check_random_ineqs(r, 4, 5, 5, 3, 6);
+    }
+}
+
+// test with upper bounds
+static void test1() {
+    opt::model_based_opt mbo;
+    vector<var> vars;
+    unsigned x = mbo.add_var(rational(2));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, x, 1, z, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, z, 1, u, -1, 1, opt::t_le);
+    add_ineq(mbo, u, 1, -6, opt::t_le);
+
+    vars.reset();
+    vars.push_back(var(x, rational(2)));
+    mbo.set_objective(vars, rational(0));
+
+    opt::inf_eps value = mbo.maximize();    
+    std::cout << value << "\n";
+    std::cout << "x: " << mbo.get_value(x) << "\n";
+    std::cout << "y: " << mbo.get_value(y) << "\n";
+    std::cout << "z: " << mbo.get_value(z) << "\n";
+    std::cout << "u: " << mbo.get_value(u) << "\n";
+}
+
+// test with lower bounds
+static void test2() {
+    opt::model_based_opt mbo;
+    vector<var> vars;
+    unsigned x = mbo.add_var(rational(5));
+    unsigned y = mbo.add_var(rational(4));
+    unsigned z = mbo.add_var(rational(3));
+    unsigned u = mbo.add_var(rational(2));
+
+    add_ineq(mbo, x, -1, y, 1, 0, opt::t_le);
+    add_ineq(mbo, x, -1, z, 1, 0, opt::t_le);
+    add_ineq(mbo, y, -1, u, 1, 0, opt::t_le);
+    add_ineq(mbo, z, -1, u, 1, 1, opt::t_le);
+    add_ineq(mbo, u, -1, -6, opt::t_le);
+
+    vars.reset();
+    vars.push_back(var(x, rational(-2)));
+    mbo.set_objective(vars, rational(0));
+
+    opt::inf_eps value = mbo.maximize();    
+    std::cout << value << "\n";
+}
+
+// test unbounded
+static void test3() {
+    opt::model_based_opt mbo;
+    vector<var> vars;
+    unsigned x = mbo.add_var(rational(2));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, x, 1, z, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, z, 1, u, -1, 1, opt::t_le);
+
+    vars.reset();
+    vars.push_back(var(x, rational(2)));
+    mbo.set_objective(vars, rational(0));
+
+    opt::inf_eps value = mbo.maximize();    
+    std::cout << value << "\n";
+
+}
+
+// test strict
+static void test4() {
+    opt::model_based_opt mbo;
+    vector<var> vars;
+    unsigned x = mbo.add_var(rational(2));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt);
+    add_ineq(mbo, x, 1, z, -1, 0, opt::t_lt);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, z, 1, u, -1, 1, opt::t_le);
+    add_ineq(mbo, u, 1, -6, opt::t_le);
+
+    vars.reset();
+    vars.push_back(var(x, rational(2)));
+    mbo.set_objective(vars, rational(0));
+
+    opt::inf_eps value = mbo.maximize();    
+    std::cout << value << "\n";
+    std::cout << "x: " << mbo.get_value(x) << "\n";
+    std::cout << "y: " << mbo.get_value(y) << "\n";
+    std::cout << "z: " << mbo.get_value(z) << "\n";
+    std::cout << "u: " << mbo.get_value(u) << "\n";
+}
+
+// test with mix of upper and lower bounds
+
+void tst_model_based_opt() {
+    check_random_ineqs();
+    test1();
+    test2();
+    test3();
+    test4();
+}

src/util/cancel_eh.h

@@ -26,12 +26,14 @@ Revision History:
 */
 template<typename T>
 class cancel_eh : public event_handler {
+    bool m_canceled;
     T & m_obj;
 public:
-    cancel_eh(T & o):m_obj(o) {}
+    cancel_eh(T & o): m_canceled(false), m_obj(o) {}
-    ~cancel_eh() { m_obj.reset_cancel(); }
+    ~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); }
     virtual void operator()() { 
-        m_obj.cancel(); 
+        m_canceled = true;
+        m_obj.inc_cancel(); 
     }
 };
 

src/util/hwf.cpp

@@ -383,17 +383,16 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
 }
 
 void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {
-    // The built-in fmod() works, except for the special numbers.
+#if defined(_WINDOWS) && _MSC_VER <= 1700
-
-    if (is_inf(x) && is_inf(y))
-        o.value = x.value/y.value; // NaN
-    else if (is_inf(y))
-        o.value = x.value;
-    else 
     o.value = fmod(x.value, y.value);
+    if (o.value >= (y.value/2.0))
+        o.value -= y.value;
+#else
+    o.value = remainder(x.value, y.value);
+#endif
 
-    // Here is an x87 alternative if the above makes problems; this may also be faster.
 #if 0
+    // Here is an x87 alternative if the above makes problems; this may also be faster.
     double xv = x.value;
     double yv = y.value;
     double & ov = o.value;

src/util/inf_eps_rational.h

@@ -23,6 +23,7 @@ Revision History:
 #include"debug.h"
 #include"vector.h"
 #include"rational.h"
+#include"inf_rational.h"
 
 template<typename Numeral>
 class inf_eps_rational {

src/util/mpf.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 #include<sstream>
+#include<iomanip>
 #include"mpf.h"
 
 mpf::mpf() :
@@ -1077,21 +1078,20 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
 
         unsigned shift = (o.sbits - 1) - ((unsigned)o.exponent);
         const mpz & shift_p = m_powers2(shift);
+        const mpz & shiftm1_p = m_powers2(shift-1);
         TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;);
+        TRACE("mpf_dbg", tout << "shiftm1_p=" << m_mpz_manager.to_string(shiftm1_p) << std::endl;);
 
         scoped_mpz div(m_mpz_manager), rem(m_mpz_manager);
         m_mpz_manager.machine_div_rem(o.significand, shift_p, div, rem);
         TRACE("mpf_dbg", tout << "div=" << m_mpz_manager.to_string(div) << " rem=" << m_mpz_manager.to_string(rem) << std::endl;);
 
-        const mpz & shift_p1 = m_powers2(shift-1);
-        TRACE("mpf_dbg", tout << "shift_p1=" << m_mpz_manager.to_string(shift_p1) << std::endl;);
-
         switch (rm) {
         case MPF_ROUND_NEAREST_TEVEN:
         case MPF_ROUND_NEAREST_TAWAY: {
-            bool tie = m_mpz_manager.eq(rem, shift_p1);
+            bool tie = m_mpz_manager.eq(rem, shiftm1_p);
-            bool less_than_tie = m_mpz_manager.lt(rem, shift_p1);
+            bool less_than_tie = m_mpz_manager.lt(rem, shiftm1_p);
-            bool more_than_tie = m_mpz_manager.gt(rem, shift_p1);
+            bool more_than_tie = m_mpz_manager.gt(rem, shiftm1_p);
             TRACE("mpf_dbg", tout << "tie= " << tie << "; <tie = " << less_than_tie << "; >tie = " << more_than_tie << std::endl;);
             if (tie) {
                 if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
@@ -1231,43 +1231,56 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
     else if (is_zero(x))
         set(o, x);
     else {
-        o.ebits = x.ebits;
+        // This is a generalized version of the algorithm for FPREM1 in the `Intel
-        o.sbits = x.sbits;
+        // 64 and IA-32 Architectures Software Developer’s Manual',
+        // Section 3-402 Vol. 2A `FPREM1-Partial Remainder'.
+        scoped_mpf ST0(*this), ST1(*this);
+        set(ST0, x);
+        set(ST1, y);
+
+        const mpf_exp_t B = x.sbits-1; // max bits per iteration.
+        mpf_exp_t D;
+        do {
+            D = ST0.exponent() - ST1.exponent();
+            TRACE("mpf_dbg_rem", tout << "st0=" << to_string_hexfloat(ST0) << std::endl;
+                                 tout << "st1=" << to_string_hexfloat(ST1) << std::endl;
+                                 tout << "D=" << D << std::endl;);
+
+            if (D < B) {
+                scoped_mpf ST0_DIV_ST1(*this), Q(*this), ST1_MUL_Q(*this), ST0p(*this);
+                div(MPF_ROUND_NEAREST_TEVEN, ST0, ST1, ST0_DIV_ST1);
+                round_to_integral(MPF_ROUND_NEAREST_TEVEN, ST0_DIV_ST1, Q);
+                mul(MPF_ROUND_NEAREST_TEVEN, ST1, Q, ST1_MUL_Q);
+                sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_Q, ST0p);
+                TRACE("mpf_dbg_rem", tout << "ST0/ST1=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl;
+                                     tout << "Q=" << to_string_hexfloat(Q) << std::endl;
+                                     tout << "ST1*Q=" << to_string_hexfloat(ST1_MUL_Q) << std::endl;
+                                     tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;);
+                set(ST0, ST0p);
+            }
+            else {
+                const mpf_exp_t N = B;
+                scoped_mpf ST0_DIV_ST1(*this), QQ(*this), ST1_MUL_QQ(*this), ST0p(*this);
+                div(MPF_ROUND_TOWARD_ZERO, ST0, ST1, ST0_DIV_ST1);
+                ST0_DIV_ST1.get().exponent -= D - N;
+                round_to_integral(MPF_ROUND_TOWARD_ZERO, ST0_DIV_ST1, QQ);
+                mul(MPF_ROUND_NEAREST_TEVEN, ST1, QQ, ST1_MUL_QQ);
+                ST1_MUL_QQ.get().exponent += D - N;
+                sub(MPF_ROUND_NEAREST_TEVEN, ST0, ST1_MUL_QQ, ST0p);
+                TRACE("mpf_dbg_rem", tout << "ST0/ST1/2^{D-N}=" << to_string_hexfloat(ST0_DIV_ST1) << std::endl;
+                                     tout << "QQ=" << to_string_hexfloat(QQ) << std::endl;
+                                     tout << "ST1*QQ*2^{D-N}=" << to_string_hexfloat(ST1_MUL_QQ) << std::endl;
+                                     tout << "ST0'=" << to_string_hexfloat(ST0p) << std::endl;);
+                SASSERT(!eq(ST0, ST0p));
+                set(ST0, ST0p);
+            }
+
+            SASSERT(ST0.exponent() - ST1.exponent() <= D);
+        } while (D >= B);
+
+        set(o, ST0);
+        if (is_zero(o))
             o.sign = x.sign;
-
-        scoped_mpf a(*this), b(*this);
-        set(a, x);
-        set(b, y);
-        unpack(a, true);
-        unpack(b, true);
-
-        TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;);
-        TRACE("mpf_dbg", tout << "B = " << to_string(b) << std::endl;);
-
-        if (a.exponent() < b.exponent())
-            set(o, x);
-        else {
-            mpf_exp_t exp_diff = a.exponent() - b.exponent();
-            SASSERT(exp_diff >= 0);
-            TRACE("mpf_dbg", tout << "exp_diff = " << exp_diff << std::endl;);
-
-            SASSERT(exp_diff < INT_MAX);
-            // CMW: This requires rather a lot of memory. There are algorithms that trade space for time by
-            // computing only a small chunk of the remainder bits at a time.
-            unsigned extra_bits = (unsigned) exp_diff;
-            m_mpz_manager.mul2k(a.significand(), extra_bits);
-            m_mpz_manager.rem(a.significand(), b.significand(), o.significand);
-
-            TRACE("mpf_dbg", tout << "REM' = " << to_string(o) << std::endl;);
-
-            if (m_mpz_manager.is_zero(o.significand))
-                mk_zero(o.ebits, o.sbits, o.sign, o);
-            else {
-                o.exponent = b.exponent();
-                m_mpz_manager.mul2k(o.significand, 3); // rounding bits
-                round(MPF_ROUND_NEAREST_TEVEN, o);
-            }
-        }
     }
 
     TRACE("mpf_dbg", tout << "REMAINDER = " << to_string(o) << std::endl;);
@@ -1352,7 +1365,7 @@ std::string mpf_manager::to_string(mpf const & x) {
     }
 
     //DEBUG_CODE(
-    //   res += " " + to_string_raw(x);
+    //   res += " " + to_string_hexfloat(x);
     //);
 
     return res;
@@ -1394,6 +1407,20 @@ std::string mpf_manager::to_string_raw(mpf const & x) {
     return res;
 }
 
+std::string mpf_manager::to_string_hexfloat(mpf const & x) {
+    std::stringstream ss("");
+    std::ios::fmtflags ff = ss.setf(std::ios_base::hex | std::ios_base::uppercase |
+                                    std::ios_base::showpoint | std::ios_base::showpos);
+    ss.setf(ff);
+    ss.precision(13);
+#if defined(_WIN32) && _MSC_VER >= 1800
+    ss << std::hexfloat << to_double(x);
+#else
+    ss << std::hex << (*reinterpret_cast<const unsigned long long *>(&(x)));
+#endif
+    return ss.str();
+}
+
 void mpf_manager::to_rational(mpf const & x, unsynch_mpq_manager & qm, mpq & o) {
     scoped_mpf a(*this);
     scoped_mpz n(m_mpq_manager), d(m_mpq_manager);

src/util/mpf.h

@@ -186,6 +186,7 @@ public:
     void mk_ninf(unsigned ebits, unsigned sbits, mpf & o);
 
     std::string to_string_raw(mpf const & a);
+    std::string to_string_hexfloat(mpf const & a);
 
     unsynch_mpz_manager & mpz_manager(void) { return m_mpz_manager; }
     unsynch_mpq_manager & mpq_manager(void) { return m_mpq_manager; }

src/util/rlimit.cpp

@@ -31,7 +31,7 @@ uint64 reslimit::count() const {
 
 bool reslimit::inc() {
     ++m_count;
-    return !m_cancel && (m_limit == 0 || m_count <= m_limit);
+    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
 }
 
 bool reslimit::inc(unsigned offset) {
@@ -46,7 +46,7 @@ void reslimit::push(unsigned delta_limit) {
     }
     m_limits.push_back(m_limit);
     m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
-    m_cancel = false;
+    m_cancel = 0;
 }
 
 void reslimit::pop() {
@@ -55,11 +55,11 @@ void reslimit::pop() {
     }
     m_limit = m_limits.back();
     m_limits.pop_back();
-    m_cancel = false;
+    m_cancel = 0;
 }
 
 char const* reslimit::get_cancel_msg() const {
-    if (m_cancel) {
+    if (m_cancel > 0) {
         return Z3_CANCELED_MSG;
     }
     else {
@@ -84,7 +84,7 @@ void reslimit::pop_child() {
 void reslimit::cancel() {
     #pragma omp critical (reslimit_cancel)
     {
-        set_cancel(true);
+        set_cancel(m_cancel+1);
     }
 }
 
@@ -92,11 +92,28 @@ void reslimit::cancel() {
 void reslimit::reset_cancel() {
     #pragma omp critical (reslimit_cancel)
     {
-        set_cancel(false);
+        set_cancel(0);
     }
 }
 
-void reslimit::set_cancel(bool f) { 
+void reslimit::inc_cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {        
+        set_cancel(m_cancel+1);
+    }
+}
+
+
+void reslimit::dec_cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        if (m_cancel > 0) {
+            set_cancel(m_cancel-1);
+        }
+    }
+}
+
+void reslimit::set_cancel(unsigned f) { 
     m_cancel = f; 
     for (unsigned i = 0; i < m_children.size(); ++i) {
         m_children[i]->set_cancel(f);

src/util/rlimit.h

@@ -22,13 +22,13 @@ Revision History:
 #include "vector.h"
 
 class reslimit {
-    volatile bool   m_cancel;
+    volatile unsigned   m_cancel;
     uint64          m_count;
     uint64          m_limit;
     svector<uint64> m_limits;
     ptr_vector<reslimit> m_children;
 
-    void set_cancel(bool f);
+    void set_cancel(unsigned f);
     
 public:    
     reslimit();
@@ -42,10 +42,13 @@ public:
     uint64 count() const; 
 
 
-    bool get_cancel_flag() const { return m_cancel; }
+    bool get_cancel_flag() const { return m_cancel > 0; }
     char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();
+
+    void inc_cancel();
+    void dec_cancel();
 };
 
 class scoped_rlimit {

src/util/util.h

@@ -226,10 +226,8 @@ public:
     }
 
     ~scoped_ptr() {
-        if (m_ptr) {
         dealloc(m_ptr);
     }
-    }
 
     T * operator->() const { 
         return m_ptr; 
@@ -253,9 +251,7 @@ public:
 
     scoped_ptr & operator=(T * n) {
         if (m_ptr != n) {
-            if (m_ptr) {
             dealloc(m_ptr);
-            }
             m_ptr = n;
         }
         return *this;

src/util/vector.h

@@ -457,5 +457,15 @@ template<typename Hash>
 struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
 
 
+// Specialize vector<std::string> to be inaccessible.
+// This will catch any regression of issue #564 and #420.
+// Use std::vector<std::string> instead.
+template <>
+class vector<std::string, true, unsigned> {
+private:
+    vector<std::string, true, unsigned>();
+};
+
+
 #endif /* VECTOR_H_ */