Merge branch 'master' of https://github.com/Z3Prover/z3 into jfleisher/devIntellitest

CMakeLists.txt

@@ -198,7 +198,9 @@ elseif (CMAKE_SYSTEM_NAME MATCHES "GNU")
   message(STATUS "Platform: GNU/Hurd")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_")
 elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-  # Does macOS really not need any special flags?
+  if (TARGET_ARCHITECTURE STREQUAL "arm64")
+    set(CMAKE_OSX_ARCHITECTURES "arm64")
+  endif()
   message(STATUS "Platform: Darwin")
 elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
   message(STATUS "Platform: FreeBSD")

cmake/target_arch_detect.cpp

@@ -5,6 +5,8 @@
 #error CMAKE_TARGET_ARCH_i686
 #elif defined(__x86_64__) || defined(_M_X64)
 #error CMAKE_TARGET_ARCH_x86_64
+#elif defined(__ARM_ARCH_ISA_A64)
+#error CMAKE_TARGET_ARCH_arm64
 #elif defined(__ARM_ARCH)
 #error CMAKE_TARGET_ARCH_arm
 #else

doc/website.dox.in

@@ -4,7 +4,7 @@
    Z3 is a high-performance theorem prover being developed at <a class="el"
    href="http://research.microsoft.com">Microsoft Research</a>. 
    
-   <b>The Z3 website is at <a class="el" href="http://github.com/z3prover">http://github.com/z3prover.</a>.</b>
+   <b>The Z3 website is at <a class="el" href="http://github.com/z3prover">http://github.com/z3prover</a>.</b>
 
    This website hosts the automatically generated documentation for the Z3 APIs.
 

scripts/mk_unix_dist.py

@@ -56,6 +56,7 @@ def display_help():
     print("  -f, --force                   force script to regenerate Makefiles.")
     print("  --nodotnet                    do not include .NET bindings in the binary distribution files.")
     print("  --dotnet-key=<file>           sign the .NET assembly with the private key in <file>.")
+    print("  --arch=<arch>                 set architecture (to arm64) to force arm64 build")
     print("  --nojava                      do not include Java bindings in the binary distribution files.")
     print("  --nopython                    do not include Python bindings in the binary distribution files.")
     print("  --githash                     include git hash in the Zip file.")
@@ -72,6 +73,7 @@ def parse_options():
                                                                    'nojava',
                                                                    'nodotnet',
                                                                    'dotnet-key=',
+                                                                   'arch=',
                                                                    'githash',
                                                                    'nopython'
                                                                    ])
@@ -96,6 +98,11 @@ def parse_options():
             JAVA_ENABLED = False
         elif opt == '--githash':
             GIT_HASH = True
+        elif opt == '--arch':
+            if arg == "arm64":
+                mk_util.IS_ARCH_ARM64 = True
+            else:
+                raise MKException("Invalid architecture directive '%s'. Legal directives: arm64" % arg)
         else:
             raise MKException("Invalid command line option '%s'" % opt)
     set_build_dir(path)
@@ -119,6 +126,8 @@ def mk_build_dir(path):
             opts.append('--git-describe')
         if PYTHON_ENABLED:
             opts.append('--python')
+        if mk_util.IS_ARCH_ARM64:
+            opts.append('--arm64=true')
         if subprocess.call(opts) != 0:
             raise MKException("Failed to generate build directory at '%s'" % path)
 
@@ -172,7 +181,9 @@ def get_os_name():
 
 def get_z3_name():
     major, minor, build, revision = get_version()
-    if sys.maxsize >= 2**32:
+    if mk_util.IS_ARCH_ARM64:
+        platform = "arm64"    
+    elif sys.maxsize >= 2**32:
         platform = "x64"
     else:
         platform = "x86"

scripts/mk_util.py

@@ -69,6 +69,7 @@ IS_WINDOWS=False
 IS_LINUX=False
 IS_HURD=False
 IS_OSX=False
+IS_ARCH_ARM64=False
 IS_FREEBSD=False
 IS_NETBSD=False
 IS_OPENBSD=False
@@ -278,10 +279,13 @@ def test_gmp(cc):
 
 
 def test_fpmath(cc):
-    global FPMATH_FLAGS
+    global FPMATH_FLAGS, IS_ARCH_ARM64, IS_OSX
     if FPMATH_ENABLED == "False":
         FPMATH_FLAGS=""
         return "Disabled"
+    if IS_ARCH_ARM64 and IS_OSX:
+        FPMATH_FLAGS = ""
+        return "Disabled-ARM64"
     if is_verbose():
         print("Testing floating point support...")
     t = TempFile('tstsse.cpp')
@@ -620,8 +624,12 @@ elif os.name == 'posix':
             LINUX_X64=True
         else:
             LINUX_X64=False
-            
 
+            
+if os.name == 'posix' and os.uname()[4] == 'arm64':
+    IS_ARCH_ARM64 = True
+
+            
 def display_help(exit_code):
     print("mk_make.py: Z3 Makefile generator\n")
     print("This script generates the Makefile for the Z3 theorem prover.")
@@ -644,6 +652,7 @@ def display_help(exit_code):
         print("  -x, --x64                     create 64 binary when using Visual Studio.")
     else:
         print("  --x86                         force 32-bit x86 build on x64 systems.")
+    print("  --arm64=<bool>                    forcearm64 bit build  on/off (supported for Darwin).")
     print("  -m, --makefiles               generate only makefiles.")
     if IS_WINDOWS:
         print("  -v, --vsproj                  generate Visual Studio Project Files.")
@@ -686,11 +695,11 @@ def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
     global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
-    global GUARD_CF, ALWAYS_DYNAMIC_BASE
+    global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
-                                               'b:df:sxhmcvtnp:gj',
+                                               'b:df:sxa:hmcvtnp:gj',
-                                               ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
+                                               ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf',
                                                 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js',
                                                 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded'])
     except:
@@ -713,6 +722,8 @@ def parse_options():
             VS_X64 = True
         elif opt in ('--x86'):
             LINUX_X64=False
+        elif opt in ('--arm64'):
+            IS_ARCH_ARM64 = arg in ('true','on','True','TRUE')
         elif opt in ('-h', '--help'):
             display_help(0)
         elif opt in ('-m', '--makefiles'):
@@ -2431,7 +2442,7 @@ def mk_config():
     if ONLY_MAKEFILES:
         return
     config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w')
-    global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED
+    global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64
     if IS_WINDOWS:
         CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++17'
         config.write(
@@ -2636,6 +2647,11 @@ def mk_config():
             LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS
         if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'):
             CXXFLAGS = '%s -fpic' % CXXFLAGS
+        if IS_OSX and IS_ARCH_ARM64:
+            print("Setting arm64")
+            CXXFLAGS = '%s -arch arm64' % CXXFLAGS
+            LDFLAGS = '%s -arch arm64' % LDFLAGS
+            SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS
 
         config.write('PREFIX=%s\n' % PREFIX)
         config.write('CC=%s\n' % CC)

scripts/nightly.yaml

@@ -4,7 +4,6 @@ variables:
   Minor: '8'
   Patch: '16'
   NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
-  MacFlags: 'CXXFLAGS="-arch x86_64" LINK_EXTRA_FLAGS="-arch x86_64" SLINK_EXTRA_FLAGS="-arch x86_64"'
 
 stages:
 - stage: Build
@@ -15,7 +14,7 @@ stages:
     pool:
       vmImage: "macOS-latest"
     steps:
-    - script: $(MacFlags) python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
+    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
     - script: git clone https://github.com/z3prover/z3test z3test
     - script: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2    
     - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
@@ -25,6 +24,20 @@ stages:
         targetPath: $(Build.ArtifactStagingDirectory)
 
 
+  - job: MacArm64
+    displayName: "Mac ARM64 Build"
+    pool:
+      vmImage: "macOS-latest"
+    steps:
+    - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
+    - script: git clone https://github.com/z3prover/z3test z3test
+    - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/.
+    - task: PublishPipelineArtifact@1
+      inputs:
+        artifactName: 'MacArm64'
+        targetPath: $(Build.ArtifactStagingDirectory)
+
+
   - job: Ubuntu
     displayName: "Ubuntu build"
     pool:
@@ -166,6 +179,11 @@ stages:
       inputs:
         artifact: 'Mac'
         path: $(Agent.TempDirectory)\package
+    - task: DownloadPipelineArtifact@2
+      displayName: 'Download macOS Arm64 Build'
+      inputs:
+        artifact: 'MacArm64'
+        path: $(Agent.TempDirectory)\package	
     - task: NuGetToolInstaller@0
       inputs:
         versionSpec: 5.x
@@ -381,7 +399,12 @@ stages:
       inputs:
         artifactName: 'Mac'
         targetPath: $(Agent.TempDirectory)
-    - script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip
+    - task: DownloadPipelineArtifact@2
+      inputs:
+        artifactName: 'MacArm64'
+        targetPath: $(Agent.TempDirectory)
+    - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip
+    - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip
     - script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip
     - script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip
     - script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip
@@ -391,7 +414,8 @@ stages:
     - script: cd src/api/python; echo $(Agent.TempDirectory)/linux-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
-    - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
+    - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
+    - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel
     - task: PublishPipelineArtifact@0
       inputs:
         artifactName: 'Python packages'
@@ -421,6 +445,11 @@ stages:
       inputs:
         artifactName: 'Mac'
         targetPath: tmp
+    - task: DownloadPipelineArtifact@2
+      displayName: "Download MacArm64"
+      inputs:
+        artifactName: 'MacArm64'
+        targetPath: tmp
     - task: DownloadPipelineArtifact@2
       displayName: "Download Ubuntu"
       inputs:

scripts/update_api.py

@@ -1820,8 +1820,8 @@ _error_handler_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
 _lib.Z3_set_error_handler.restype  = None
 _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
 
-push_eh_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
+push_eh_type  = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
-pop_eh_type   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
+pop_eh_type   = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
 fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 
 fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)

src/api/api_ast.cpp

@@ -164,7 +164,7 @@ extern "C" {
             return;
         }
         recfun_replace replace(m);
-        p.set_definition(replace, pd, true, n, _vars.data(), abs_body);
+        p.set_definition(replace, pd, false, n, _vars.data(), abs_body);
         Z3_CATCH;
     }
 
@@ -355,7 +355,7 @@ extern "C" {
             return mk_c(c)->mk_external_string(buffer.str());
         }
         else {
-            return mk_c(c)->mk_external_string(_s.bare_str());
+            return mk_c(c)->mk_external_string(_s.str());
         }
         Z3_CATCH_RETURN("");
     }
@@ -1329,6 +1329,9 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
+            return Z3_OP_RECURSIVE;
+
         return Z3_OP_UNINTERPRETED;
         Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
     }

src/api/api_log.cpp

@@ -88,7 +88,7 @@ void Sy(Z3_symbol sym) {
         *g_z3_log << "# " << s.get_num();
     }
     else {
-        *g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|';
+        *g_z3_log << "$ |" << ll_escaped{s.str().c_str()} << '|';
     }
     *g_z3_log << std::endl;
 }

src/api/api_solver.cpp

@@ -883,8 +883,8 @@ extern "C" {
         Z3_TRY;
         RESET_ERROR_CODE();
         init_solver(c, s);
-        user_propagator::push_eh_t _push = push_eh;
+        user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh;
-        user_propagator::pop_eh_t _pop = pop_eh;
+        user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh;
         user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) {
             ast_context_params params;
             params.set_foreign_manager(&m);

src/api/api_tactic.cpp

@@ -331,8 +331,8 @@ extern "C" {
         if (idx >= mk_c(c)->num_tactics()) {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
-        }
+        }        
-        return mk_c(c)->get_tactic(idx)->get_name().bare_str();
+        return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str());
         Z3_CATCH_RETURN("");
     }
 
@@ -352,7 +352,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
         }
-        return mk_c(c)->get_probe(idx)->get_name().bare_str();
+        return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str());
         Z3_CATCH_RETURN("");
     }
 

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

@@ -3964,18 +3964,23 @@ namespace z3 {
             }
         };
 
-        static void push_eh(void* p) {
+        static void push_eh(void* _p, Z3_solver_callback cb) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
+            scoped_cb _cb(p, cb);
             static_cast<user_propagator_base*>(p)->push();
         }
 
-        static void pop_eh(void* p, unsigned num_scopes) {
+        static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) {
-            static_cast<user_propagator_base*>(p)->pop(num_scopes);
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
+            scoped_cb _cb(p, cb);
+            static_cast<user_propagator_base*>(_p)->pop(num_scopes);
         }
 
-        static void* fresh_eh(void* p, Z3_context ctx) {
+        static void* fresh_eh(void* _p, Z3_context ctx) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
             context* c = new context(ctx);
-            static_cast<user_propagator_base*>(p)->subcontexts.push_back(c);
+            p->subcontexts.push_back(c);
-            return static_cast<user_propagator_base*>(p)->fresh(*c);
+            return p->fresh(*c);
         }
 
         static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) {

src/api/python/CMakeLists.txt

@@ -42,8 +42,6 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py"
     ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
     "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
     ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
-    # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency
-    "${PROJECT_SOURCE_DIR}/scripts/mk_util.py"
   COMMENT "Generating z3core.py"
   ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
 )

src/api/python/pyproject.toml

@@ -0,0 +1,3 @@
+[build-system]
+requires = ["setuptools>=46.4.0", "wheel", "cmake"]
+build-backend = "setuptools.build_meta"

src/api/python/setup.py

@@ -154,16 +154,10 @@ def _copy_bins():
 
     _clean_bins()
 
-    python_dir = None
+    py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3')
-    if RELEASE_DIR is not None:
+    root_z3_dir = os.path.join(ROOT_DIR, 'z3')
-        python_dir = os.path.join(RELEASE_DIR, 'bin', 'python')
+    shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir)
-    elif SRC_DIR == SRC_DIR_LOCAL:
+    shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir)
-        python_dir = os.path.join(SRC_DIR, 'src', 'api', 'python')
-    if python_dir is not None:
-        py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3')
-        root_z3_dir = os.path.join(ROOT_DIR, 'z3')
-        shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir)
-        shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir)
 
     # STEP 2: Copy the shared library, the executable and the headers
 
@@ -279,8 +273,10 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
             osver = RELEASE_METADATA[3]
             if osver.count('.') > 1:
                 osver = '.'.join(osver.split('.')[:2])
-            if arch == 'x64':
+            if arch == 'x64':                
                 plat_name ='macosx_%s_x86_64' % osver.replace('.', '_')
+            elif arch == 'arm64':
+                plat_name ='macosx_%s_arm64' % osver.replace('.', '_')                
             else:
                 raise Exception(f"idk how os {distos} {osver} works. what goes here?")
         else:

src/api/python/z3/z3.py

@@ -2279,6 +2279,9 @@ class ArithSortRef(SortRef):
         """
         return self.kind() == Z3_INT_SORT
 
+    def is_bool(self):
+        return False
+
     def subsort(self, other):
         """Return `True` if `self` is a subsort of `other`."""
         return self.is_int() and is_arith_sort(other) and other.is_real()
@@ -11237,12 +11240,16 @@ def ensure_prop_closures():
         _prop_closures = PropClosures()
 
 
-def user_prop_push(ctx):
+def user_prop_push(ctx, cb):
-    _prop_closures.get(ctx).push()
+    prop = _prop_closures.get(ctx)
+    prop.cb = cb
+    prop.push()
 
 
-def user_prop_pop(ctx, num_scopes):
+def user_prop_pop(ctx, cb, num_scopes):
-    _prop_closures.get(ctx).pop(num_scopes)
+    prop = _prop_closures.get(ctx)
+    prop.cb = cb
+    pop(num_scopes)
 
 
 def user_prop_fresh(id, ctx):

src/api/z3_api.h

@@ -996,6 +996,8 @@ typedef enum
         information is exposed. Tools may use the string representation of the
         function declaration to obtain more information.
 
+   - Z3_OP_RECURSIVE: function declared as recursive
+
    - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
 */
 typedef enum {
@@ -1320,6 +1322,7 @@ typedef enum {
     Z3_OP_FPA_BV2RM,
 
     Z3_OP_INTERNAL,
+    Z3_OP_RECURSIVE,
 
     Z3_OP_UNINTERPRETED
 } Z3_decl_kind;
@@ -1434,8 +1437,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e));
 /**
    \brief callback functions for user propagator.
 */
-Z3_DECLARE_CLOSURE(Z3_push_eh,    void, (void* ctx));
+Z3_DECLARE_CLOSURE(Z3_push_eh,    void, (void* ctx, Z3_solver_callback cb));
-Z3_DECLARE_CLOSURE(Z3_pop_eh,     void, (void* ctx, unsigned num_scopes));
+Z3_DECLARE_CLOSURE(Z3_pop_eh,     void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes));
 Z3_DECLARE_CLOSURE(Z3_fresh_eh,   void*, (void* ctx, Z3_context new_context));
 Z3_DECLARE_CLOSURE(Z3_fixed_eh,   void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value));
 Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t));

src/ast/ast_smt2_pp.cpp

@@ -47,18 +47,14 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo
         len = static_cast<unsigned>(str.length());
         return mk_string(m, str);
     }
-    else if (s.is_numerical()) {
+    else if (s.is_null()) {
-        std::string str = s.str();
-        len = static_cast<unsigned>(str.length());
-        return mk_string(m, str);
-    }
-    else if (!s.bare_str()) {
         len = 4;
         return mk_string(m, "null");
     }
     else {
-        len = static_cast<unsigned>(strlen(s.bare_str()));
+        std::string str = s.str();
-        return mk_string(m, s.bare_str());
+        len = static_cast<unsigned>(str.length());
+        return mk_string(m, str);
     }
 }
 

src/ast/pb_decl_plugin.cpp

@@ -90,11 +90,11 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
 
 void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") {
-        op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
+        op_names.push_back(builtin_name(m_at_most_sym.str(), OP_AT_MOST_K));
-        op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
+        op_names.push_back(builtin_name(m_at_least_sym.str(), OP_AT_LEAST_K));
-        op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));
+        op_names.push_back(builtin_name(m_pble_sym.str(), OP_PB_LE));
-        op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE));
+        op_names.push_back(builtin_name(m_pbge_sym.str(), OP_PB_GE));
-        op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ));
+        op_names.push_back(builtin_name(m_pbeq_sym.str(), OP_PB_EQ));
     }
 }
 

src/ast/rewriter/bv_rewriter.cpp

@@ -2803,6 +2803,21 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu
     return BR_FAILED;
 }
 
+br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (num_args <= 1) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    unsigned sz = get_bv_size(args[0]);
+    // check if num_args > 2^sz
+    if (sz >= 32) 
+        return BR_FAILED;
+    if (num_args <= 1u << sz)
+        return BR_FAILED;
+    result = m().mk_false();
+    return BR_DONE;     
+}
+
 br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) {
     SASSERT(num == 2);
     unsigned bv_sz;

src/ast/rewriter/bv_rewriter.h

@@ -180,7 +180,8 @@ public:
 
     bool is_urem_any(expr * e, expr * & dividend,  expr * & divisor);
     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
-    br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul);
+    br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
+    br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result);
 
     bool hi_div0() const { return m_hi_div0; }
 

src/ast/rewriter/th_rewriter.cpp

@@ -60,7 +60,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     expr_substitution * m_subst = nullptr;
     unsigned long long  m_max_memory; // in bytes
     bool                m_new_subst = false;
-    unsigned            m_max_steps = UINT_MAX;    
+    unsigned            m_max_steps = UINT_MAX;
     bool                m_pull_cheap_ite = true;
     bool                m_flat = true;
     bool                m_cache_all = false;
@@ -180,7 +180,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 // theory dispatch for =
                 SASSERT(num == 2);
                 family_id s_fid = args[0]->get_sort()->get_family_id();
-                if (s_fid == m_a_rw.get_fid()) 
+                if (s_fid == m_a_rw.get_fid())
                     st = m_a_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_bv_rw.get_fid())
                     st = m_bv_rw.mk_eq_core(args[0], args[1], result);
@@ -193,10 +193,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
                 if (st != BR_FAILED)
-                    return st;     
+                    return st;
-            }
-            if (k == OP_EQ) {
-                SASSERT(num == 2);
                 st = apply_tamagotchi(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
@@ -210,16 +207,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                     return st;
             }
             if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) {
-                st = m_seq_rw.mk_bool_app(f, num, args, result); 
+                st = m_seq_rw.mk_bool_app(f, num, args, result);
                 if (st != BR_FAILED)
                     return st;
             }
-            if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) && 
+            if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
                 to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
                 st = m_seq_rw.mk_eq_core(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
             }
+            if (k == OP_DISTINCT && num > 0 && m_bv_rw.is_bv(args[0])) {
+               st = m_bv_rw.mk_distinct(num, args, result);
+               if (st != BR_FAILED)
+                    return st;
+            }
 
             return m_b_rw.mk_app_core(f, num, args, result);
         }
@@ -250,7 +252,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         if (fid == m_seq_rw.get_fid())
             return m_seq_rw.mk_app_core(f, num, args, result);
         if (fid == m_char_rw.get_fid())
-            return m_char_rw.mk_app_core(f, num, args, result);        
+            return m_char_rw.mk_app_core(f, num, args, result);
         if (fid == m_rec_rw.get_fid())
             return m_rec_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;

src/ast/special_relations_decl_plugin.cpp

@@ -61,11 +61,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl(
 
 void special_relations_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     if (logic == symbol::null) {
-        op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO));
+        op_names.push_back(builtin_name(m_po.str(), OP_SPECIAL_RELATION_PO));
-        op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO));
+        op_names.push_back(builtin_name(m_lo.str(), OP_SPECIAL_RELATION_LO));
-        op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO));
+        op_names.push_back(builtin_name(m_plo.str(), OP_SPECIAL_RELATION_PLO));
-        op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO));
+        op_names.push_back(builtin_name(m_to.str(), OP_SPECIAL_RELATION_TO));
-        op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC));
+        op_names.push_back(builtin_name(m_tc.str(), OP_SPECIAL_RELATION_TC));
     }
 }
 

src/cmd_context/basic_cmds.cpp

@@ -58,7 +58,7 @@ public:
         cmd * c = ctx.find_cmd(s);
         if (c == nullptr) {
             std::string err_msg("unknown command '");
-            err_msg = err_msg + s.bare_str() + "'";
+            err_msg = err_msg + s.str() + "'";
             throw cmd_exception(std::move(err_msg));
         }
         m_cmds.push_back(s);

src/cmd_context/cmd_context.cpp

@@ -1636,6 +1636,7 @@ void cmd_context::pop(unsigned n) {
     restore_aux_pdecls(s.m_aux_pdecls_lim);
     restore_assertions(s.m_assertions_lim);
     restore_psort_inst(s.m_psort_inst_stack_lim);
+    m_dt_eh.get()->reset();
     m_mcs.shrink(m_mcs.size() - n);
     m_scopes.shrink(new_lvl);
     if (!m_global_decls)

src/cmd_context/cmd_context.h

@@ -267,6 +267,7 @@ protected:
         cmd_context &             m_owner;
         datatype_util             m_dt_util;
     public:
+        void reset() { m_dt_util.reset(); }
         dt_eh(cmd_context & owner);
         ~dt_eh() override;
         void operator()(sort * dt, pdecl* pd) override;

src/cmd_context/pdecl.cpp

@@ -156,8 +156,8 @@ public:
             return false;
         return m_sort == static_cast<psort_sort const *>(other)->m_sort;
     }
-    void display(std::ostream & out) const override {
+    std::ostream& display(std::ostream & out) const override {
-        out << m_sort->get_name();
+        return out << m_sort->get_name();
     }
 };
 
@@ -180,8 +180,8 @@ public:
             get_num_params() == other->get_num_params() && 
             m_idx == static_cast<psort_var const *>(other)->m_idx;
     }
-    void display(std::ostream & out) const override {
+    std::ostream& display(std::ostream & out) const override {
-        out << "s_" << m_idx;
+        return out << "s_" << m_idx;
     }
     unsigned idx() const { return m_idx; }
 };
@@ -254,7 +254,7 @@ public:
         }
         return true;
     }
-    void display(std::ostream & out) const override {
+    std::ostream& display(std::ostream & out) const override {
         if (m_args.empty()) {
             out << m_decl->get_name();
         }
@@ -267,6 +267,7 @@ public:
             }
             out << ")";
         }
+        return out;
     }
 };
 
@@ -342,12 +343,12 @@ void display_sort_args(std::ostream & out, unsigned num_params) {
         out << ") ";
 }
 
-void psort_user_decl::display(std::ostream & out) const {
+std::ostream& psort_user_decl::display(std::ostream & out) const {
     out << "(declare-sort " << m_name;
     display_sort_args(out, m_num_params);
     if (m_def)
         m_def->display(out);
-    out << ")";
+    return out << ")";
 }
 
 // -------------------
@@ -364,8 +365,8 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
     return m.instantiate_datatype(this, m_name, n, s);
 }
 
-void psort_dt_decl::display(std::ostream & out) const {
+std::ostream& psort_dt_decl::display(std::ostream & out) const {
-    out << "(datatype-sort " << m_name << ")";
+    return out << "(datatype-sort " << m_name << ")";
 }
 
 // -------------------
@@ -410,8 +411,8 @@ sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned c
     }
 }
 
-void psort_builtin_decl::display(std::ostream & out) const {
+std::ostream& psort_builtin_decl::display(std::ostream & out) const {
-    out << "(declare-builtin-sort " << m_name << ")";
+    return out << "(declare-builtin-sort " << m_name << ")";
 }
 
 void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const {
@@ -615,7 +616,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
 }
 
 
-void pdatatype_decl::display(std::ostream & out) const {
+std::ostream& pdatatype_decl::display(std::ostream & out) const {
     out << "(declare-datatype " << m_name;
     display_sort_args(out, m_num_params);
     bool first = true;
@@ -631,7 +632,7 @@ void pdatatype_decl::display(std::ostream & out) const {
         }
         first = false;
     }
-    out << ")";
+    return out << ")";
 }
 
 bool pdatatype_decl::commit(pdecl_manager& m) {
@@ -645,9 +646,11 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
     datatype_decl * d_ptr = dts.m_buffer[0];
     sort_ref_vector sorts(m.m());
     bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.data(), sorts);
+    m.notify_mk_datatype(m_name);
     if (is_ok && m_num_params == 0) {
         m.notify_new_dt(sorts.get(0), this);        
     }
+
     return is_ok;
 }
 
@@ -722,6 +725,7 @@ void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* co
 
 void pdecl_manager::push() {
     m_notified_lim.push_back(m_notified_trail.size());
+    m_datatypes_lim.push_back(m_datatypes_trail.size());
 }
 
 void pdecl_manager::pop(unsigned n) {
@@ -732,6 +736,16 @@ void pdecl_manager::pop(unsigned n) {
     }
     m_notified_trail.shrink(new_sz);
     m_notified_lim.shrink(m_notified_lim.size() - n);
+    
+    new_sz = m_datatypes_lim[m_datatypes_lim.size() - n];
+    if (new_sz != m_datatypes_trail.size()) {
+        datatype_util util(m());
+        for (unsigned i = m_datatypes_trail.size(); i-- > new_sz; )
+            util.plugin().remove(m_datatypes_trail[i]);
+    }
+    m_datatypes_trail.shrink(new_sz);
+    m_datatypes_lim.shrink(m_datatypes_lim.size() - n);
+        
 }
 
 bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
@@ -751,16 +765,24 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
     sort_ref_vector sorts(m.m());
     bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.data(), 0, nullptr, sorts);
     if (is_ok) {
+        for (pdatatype_decl* d : m_datatypes) {
+            m.notify_mk_datatype(d->get_name());
+        }
         for (unsigned i = 0; i < m_datatypes.size(); ++i) {
             pdatatype_decl* d = m_datatypes[i];
-            if (d->get_num_params() == 0) {
+            if (d->get_num_params() == 0) 
                 m.notify_new_dt(sorts.get(i), this);        
-            }
         }
     }
+    
     return is_ok;
 }
 
+void pdecl_manager::notify_mk_datatype(symbol const& name) {
+    m_datatypes_trail.push_back(name);
+}
+
+
 struct pdecl_manager::sort_info {
     psort_decl * m_decl;
 
@@ -985,16 +1007,19 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
-    TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);   
+    TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
         if (_p->is_sort_wrapper()) {
-            m_sort2psort.erase(static_cast<psort_sort*>(_p)->get_sort());
+            sort* s = static_cast<psort_sort*>(_p)->get_sort();
+            m_sort2psort.erase(s);
         }
         else {
             m_table.erase(_p);
         }
+
     }
+
     del_decl_core(p);
 }
 

src/cmd_context/pdecl.h

@@ -45,7 +45,7 @@ public:
     unsigned get_id() const { return m_id; }
     unsigned get_ref_count() const { return m_ref_count; }
     unsigned hash() const { return m_id; }
-    virtual void display(std::ostream & out) const {}
+    virtual std::ostream& display(std::ostream & out) const { return out;}
     virtual void reset_cache(pdecl_manager& m) {}
 };
 
@@ -123,7 +123,7 @@ protected:
     ~psort_user_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
-    void display(std::ostream & out) const override;
+    std::ostream& display(std::ostream & out) const override;
 };
  
 class psort_builtin_decl : public psort_decl {
@@ -137,7 +137,7 @@ protected:
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
     sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override;
-    void display(std::ostream & out) const override;
+    std::ostream& display(std::ostream & out) const override;
 };
 
 class psort_dt_decl : public psort_decl {
@@ -148,7 +148,7 @@ protected:
     ~psort_dt_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
-    void display(std::ostream & out) const override;
+    std::ostream& display(std::ostream & out) const override;
 };
 
 
@@ -198,7 +198,7 @@ class paccessor_decl : public pdecl {
     ptype const & get_type() const { return m_type; }
     ~paccessor_decl() override {}
 public:
-    void display(std::ostream & out) const override { pdecl::display(out); }
+    std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
 };
 
@@ -219,7 +219,7 @@ class pconstructor_decl : public pdecl {
     constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
     ~pconstructor_decl() override {}
 public:
-    void display(std::ostream & out) const override { pdecl::display(out); }
+    std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
     void display(std::ostream & out, pdatatype_decl const * const * dts) const;
 };
 
@@ -237,7 +237,7 @@ class pdatatype_decl : public psort_decl {
     ~pdatatype_decl() override {}
 public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
-    void display(std::ostream & out) const override;
+    std::ostream& display(std::ostream & out) const override;
     bool has_missing_refs(symbol & missing) const;
     bool has_duplicate_accessors(symbol & repeated) const;
     bool commit(pdecl_manager& m);
@@ -289,6 +289,8 @@ class pdecl_manager {
     obj_hashtable<sort>          m_notified;
     ptr_vector<sort>             m_notified_trail;
     unsigned_vector              m_notified_lim;
+    svector<symbol>              m_datatypes_trail;
+    unsigned_vector              m_datatypes_lim;
 
     void init_list();
     void del_decl_core(pdecl * p);
@@ -319,6 +321,7 @@ public:
     sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s);
     sort * instantiate(psort * s, unsigned num, sort * const * args);
     void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s);
+    void notify_mk_datatype(symbol const& name);
     void push();
     void pop(unsigned n);
 

src/muz/fp/datalog_parser.cpp

@@ -777,6 +777,7 @@ protected:
     // Sym ::= String | NUM | Var
     // 
     dtoken parse_infix(dtoken tok1, char const* td, app_ref& pred) {
+        std::string td1_(td);
         symbol td1(td);
         expr_ref v1(m), v2(m);
         sort* s = nullptr;
@@ -793,12 +794,12 @@ protected:
 
         if (tok1 == TK_ID) {
             expr* _v1 = nullptr;
-            m_vars.find(td1.bare_str(), _v1);
+            m_vars.find(td1_, _v1);
             v1 = _v1;
         }
         if (tok3 == TK_ID) {
             expr* _v2 = nullptr;
-            m_vars.find(td2.bare_str(), _v2);
+            m_vars.find(td, _v2);
             v2 = _v2;
         }
         if (!v1 && !v2) {
@@ -950,18 +951,19 @@ protected:
             break;
         }
         case TK_ID: {
-            symbol data (m_lexer->get_token_data());
+            char const* d = m_lexer->get_token_data();
-            if (is_var(data.bare_str())) {
+            symbol data (d);
+            if (is_var(d)) {
                 unsigned idx = 0;
                 expr* v = nullptr;
-                if (!m_vars.find(data.bare_str(), v)) {
+                if (!m_vars.find(d, v)) {
                     idx = m_num_vars++;
                     v = m.mk_var(idx, s);
-                    m_vars.insert(data.bare_str(), v);
+                    m_vars.insert(d, v);
                 }
                 else if (s != v->get_sort()) {
                     throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n",
-                        s->get_name().bare_str(), v->get_sort()->get_name().bare_str());
+                                            s->get_name().str().c_str(), v->get_sort()->get_name().str().c_str());
                 }
                 args.push_back(v);
             }
@@ -1075,21 +1077,21 @@ protected:
     }
 
     sort * register_finite_sort(symbol name, uint64_t domain_size, context::sort_kind k) {
-        if(m_sort_dict.contains(name.bare_str())) {
+        if(m_sort_dict.contains(name.str().c_str())) {
-            throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
+            throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str());
         }
         sort * s = m_decl_util.mk_sort(name, domain_size);
         m_context.register_finite_sort(s, k);
-        m_sort_dict.insert(name.bare_str(), s);
+        m_sort_dict.insert(name.str(), s);
         return s;
     }
 
     sort * register_int_sort(symbol name) {
-        if(m_sort_dict.contains(name.bare_str())) {
+        if(m_sort_dict.contains(name.str().c_str())) {
-            throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str());
+            throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str());
         }
         sort * s = m_arith.mk_int();
-        m_sort_dict.insert(name.bare_str(), s);
+        m_sort_dict.insert(name.str(), s);
         return s;
     }
 
@@ -1105,8 +1107,8 @@ protected:
         app * res;
         if(m_arith.is_int(s)) {
             uint64_t val;
-            if (!string_to_uint64(name.bare_str(), val)) {
+            if (!string_to_uint64(name.str().c_str(), val)) {
-                throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.bare_str());
+                throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.str().c_str());
             }
             res = m_arith.mk_numeral(rational(val, rational::ui64()), s);
         }
@@ -1288,7 +1290,7 @@ private:
         uint64_set & sort_content = *e->get_data().m_value;
         if(!sort_content.contains(num)) {
             warning_msg("symbol number %I64u on line %d in file %s does not belong to sort %s", 
-                num, m_current_line, m_current_file.c_str(), s->get_name().bare_str());
+                        num, m_current_line, m_current_file.c_str(), s->get_name().str().c_str());
             return false;
         }
         if(!m_use_map_names) {
@@ -1366,7 +1368,7 @@ private:
         func_decl * pred = m_context.try_get_predicate_decl(predicate_name);
         if(!pred) {
             throw default_exception(default_exception::fmt(), "tuple file %s for undeclared predicate %s", 
-                m_current_file.c_str(), predicate_name.bare_str());
+                                    m_current_file.c_str(), predicate_name.str().c_str());
         }
         unsigned pred_arity = pred->get_arity();
         sort * const * arg_sorts = pred->get_domain();
@@ -1531,9 +1533,9 @@ private:
             
             if(m_use_map_names) {
                 auto const & value = m_number_names.insert_if_not_there(num, el_name);
-                if (value!=el_name) {
+                if (value != el_name) {
                     warning_msg("mismatch of number names on line %d in file %s. old: \"%s\" new: \"%s\"", 
-                        m_current_line, fname.c_str(), value.bare_str(), el_name.bare_str());
+                                m_current_line, fname.c_str(), value.str().c_str(), el_name.str().c_str());
                 }
             }
         }

src/muz/rel/dl_finite_product_relation.cpp

@@ -64,7 +64,7 @@ namespace datalog {
     }
 
     symbol finite_product_relation_plugin::get_name(relation_plugin & inner_plugin) {
-        std::string str = std::string("fpr_")+inner_plugin.get_name().bare_str();
+        std::string str = std::string("fpr_")+inner_plugin.get_name().str();
         return symbol(str.c_str());
     }
 

src/muz/rel/dl_instruction.cpp

@@ -213,10 +213,10 @@ namespace datalog {
             return true;
         }
         void make_annotations(execution_context & ctx) override {
-            ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str());
+            ctx.set_register_annotation(m_reg, m_pred->get_name().str().c_str());
         }
         std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            const char * rel_name = m_pred->get_name().bare_str();
+            auto rel_name = m_pred->get_name();            
             if (m_store) {
                 return out << "store " << m_reg << " into " << rel_name;
             }
@@ -378,7 +378,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                                             "trying to perform unsupported join operation on relations of kinds %s and %s",
-                                            r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
+                                            r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r1, r2, fn);
             }
@@ -441,7 +441,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_equal operation on a relation of kind %s",
-                        r.get_plugin().get_name().bare_str());
+                        r.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r, fn);
             }
@@ -490,7 +490,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_identical operation on a relation of kind %s",
-                        r.get_plugin().get_name().bare_str());
+                        r.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r, fn);
             }
@@ -537,7 +537,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_interpreted operation on a relation of kind %s",
-                        r.get_plugin().get_name().bare_str());
+                        r.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r, fn);
             }
@@ -594,7 +594,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s",
-                        reg.get_plugin().get_name().bare_str());
+                        reg.get_plugin().get_name().str().c_str());
                 }
                 store_fn(reg, fn);
             }
@@ -837,7 +837,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                                             "trying to perform unsupported join-project operation on relations of kinds %s and %s",
-                        r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str());
+                        r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r1, r2, fn);
             }
@@ -910,7 +910,7 @@ namespace datalog {
                 if (!fn) {
                     throw default_exception(default_exception::fmt(), 
                         "trying to perform unsupported select_equal_and_project operation on a relation of kind %s",
-                        r.get_plugin().get_name().bare_str());
+                        r.get_plugin().get_name().str().c_str());
                 }
                 store_fn(r, fn);
             }
@@ -1076,7 +1076,7 @@ namespace datalog {
             return true;
         }
         std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override {
-            return out << "mark_saturated " << m_pred->get_name().bare_str();
+            return out << "mark_saturated " << m_pred->get_name();
         }
         void make_annotations(execution_context & ctx) override {
         }

src/muz/rel/dl_table_relation.cpp

@@ -33,7 +33,7 @@ namespace datalog {
     // -----------------------------------
 
     symbol table_relation_plugin::create_plugin_name(const table_plugin &p) {
-        std::string name = std::string("tr_") + p.get_name().bare_str();
+        std::string name = std::string("tr_") + p.get_name().str();
         return symbol(name.c_str());
     }
 

src/muz/rel/rel_context.cpp

@@ -157,7 +157,7 @@ namespace datalog {
             //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream()););
 
             if (m_context.print_aig().is_non_empty_string()) {
-                const char *filename = m_context.print_aig().bare_str();
+                std::string filename = m_context.print_aig().str();
                 aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts);
                 std::ofstream strm(filename, std::ios_base::binary);
                 aig(strm);

src/opt/CMakeLists.txt

@@ -8,6 +8,7 @@ z3_add_component(opt
     opt_lns.cpp
     opt_pareto.cpp
     opt_parse.cpp
+    opt_preprocess.cpp
     optsmt.cpp
     opt_solver.cpp
     pb_sls.cpp

src/opt/maxlex.cpp

@@ -26,15 +26,15 @@ Author:
 
 namespace opt {
 
-    bool is_maxlex(weights_t & _ws) {
+    bool is_maxlex(vector<soft> const & _ws) {
-        vector<rational> ws(_ws);
+        vector<soft> ws(_ws);
-        std::sort(ws.begin(), ws.end());
+        std::sort(ws.begin(), ws.end(), [&](soft const& s1, soft const& s2) { return s1.weight < s2.weight; });
         ws.reverse();
         rational sum(0);
-        for (rational const& w : ws) {
+        for (auto const& [e, w, t] : ws) {
             sum += w;
         }
-        for (rational const& w : ws) {
+        for (auto const& [e, w, t] : ws) {
             if (sum > w + w) return false;
             sum -= w;
         }
@@ -185,8 +185,8 @@ namespace opt {
 
     public:
 
-        maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s):
+        maxlex(maxsat_context& c, unsigned id, vector<soft>& s):
-            maxsmt_solver_base(c, ws, s),
+            maxsmt_solver_base(c, s, id),
             m(c.get_manager()),
             m_c(c) {
             // ensure that soft constraints are sorted with largest soft constraints first.
@@ -210,8 +210,8 @@ namespace opt {
         }
     };
 
-    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) {
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector<soft>& soft) {
-        return alloc(maxlex, c, id, ws, soft);
+        return alloc(maxlex, c, id, soft);
     }
 
 }

src/opt/maxlex.h

@@ -21,9 +21,9 @@ Notes:
 
 namespace opt {
 
-    bool is_maxlex(weights_t & ws);
+    bool is_maxlex(vector<soft> const & ws);
 
-    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector<soft>& soft);
 
 
 };

src/opt/maxres.cpp

@@ -95,7 +95,6 @@ private:
         expr_ref_vector const& soft() override { return i.m_asms; }
     };
 
-    unsigned         m_index;
     stats            m_stats;
     expr_ref_vector  m_B;
     expr_ref_vector  m_asms;    
@@ -129,11 +128,10 @@ private:
     typedef ptr_vector<expr> exprs;
 
 public:
-    maxres(maxsat_context& c, unsigned index, 
+    maxres(maxsat_context& c, unsigned index,
-           weights_t& ws, expr_ref_vector const& soft, 
+           vector<soft>& soft,
            strategy_t st):
-        maxsmt_solver_base(c, ws, soft),
+        maxsmt_solver_base(c, soft, index),
-        m_index(index), 
         m_B(m), m_asms(m), m_defs(m),
         m_new_core(m),
         m_mus(c.get_solver()),
@@ -791,11 +789,10 @@ public:
         improve_model(mdl);
         mdl->set_model_completion(true);
         unsigned correction_set_size = 0;
-        for (expr* a : m_asms) {
+        for (expr* a : m_asms) 
-            if (mdl->is_false(a)) {
+            if (mdl->is_false(a)) 
                 ++correction_set_size;
-            }
+
-        }
         if (!m_csmodel.get() || correction_set_size < m_correction_set_size) {
             m_csmodel = mdl;
             m_correction_set_size = correction_set_size;
@@ -810,22 +807,22 @@ public:
             return;
         }
 
-        if (!m_c.verify_model(m_index, mdl.get(), upper)) {
+        if (!m_c.verify_model(m_index, mdl.get(), upper)) 
             return;
-        }
 
+        unsigned num_assertions = s().get_num_assertions();
         m_model = mdl;
         m_c.model_updated(mdl.get());
 
         TRACE("opt", tout << "updated upper: " << upper << "\n";);
 
-        for (soft& s : m_soft) {
+        for (soft& s : m_soft) 
             s.set_value(m_model->is_true(s.s));
-        }
        
         verify_assignment();
 
-        m_upper = upper;
+        if (num_assertions == s().get_num_assertions())
+            m_upper = upper;
         
         trace();
 
@@ -876,17 +873,10 @@ public:
     }
 
     lbool init_local() {
-        m_lower.reset();
         m_trail.reset();
         lbool is_sat = l_true;
-        obj_map<expr, rational> new_soft;
+        for (auto const& [e, w, t] : m_soft)
-        is_sat = find_mutexes(new_soft);
+            add_soft(e, w);
-        if (is_sat != l_true) {
-            return is_sat;
-        }
-        for (auto const& kv : new_soft) {
-            add_soft(kv.m_key, kv.m_value);
-        }
         m_max_upper = m_upper;
         m_found_feasible_optimum = false;
         m_last_index = 0;
@@ -954,12 +944,12 @@ public:
 };
 
 opt::maxsmt_solver_base* opt::mk_maxres(
-    maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
+    maxsat_context& c, unsigned id, vector<soft>& soft) {
-    return alloc(maxres, c, id, ws, soft, maxres::s_primal);
+    return alloc(maxres, c, id, soft, maxres::s_primal);
 }
 
 opt::maxsmt_solver_base* opt::mk_primal_dual_maxres(
-    maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) {
+    maxsat_context& c, unsigned id, vector<soft>& soft) {
-    return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual);
+    return alloc(maxres, c, id, soft, maxres::s_primal_dual);
 }
 

src/opt/maxres.h

@@ -21,9 +21,9 @@ Notes:
 
 namespace opt {
 
-    maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
-    maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
 
 };
 

src/opt/maxsmt.cpp

@@ -28,29 +28,34 @@ Notes:
 #include "opt/wmax.h"
 #include "opt/opt_params.hpp"
 #include "opt/opt_context.h"
+#include "opt/opt_preprocess.h"
 #include "smt/theory_wmaxsat.h"
 #include "smt/theory_pb.h"
 
 
 namespace opt {
 
-    maxsmt_solver_base::maxsmt_solver_base(
+    maxsmt_solver_base::maxsmt_solver_base(maxsat_context& c, vector<soft>& s, unsigned index):
-        maxsat_context& c, vector<rational> const& ws, expr_ref_vector const& softs):
         m(c.get_manager()), 
         m_c(c),
+        m_index(index),
+        m_soft(s),
         m_assertions(m),
         m_trail(m) {
         c.get_base_model(m_model);
         SASSERT(m_model);
         updt_params(c.params());
-        for (unsigned i = 0; i < ws.size(); ++i) {
-            m_soft.push_back(soft(expr_ref(softs.get(i), m), ws[i], false));
-        }
     }
     
     void maxsmt_solver_base::updt_params(params_ref& p) {
         m_params.copy(p);
-    }       
+    }
+
+    void maxsmt_solver_base::reset_upper() {
+        m_upper = m_lower;
+        for (soft& s : m_soft) 
+            m_upper += s.weight;
+    }
 
     solver& maxsmt_solver_base::s() {
         return m_c.get_solver(); 
@@ -82,14 +87,24 @@ namespace opt {
         m_upper.reset();
         for (soft& s : m_soft) {
             s.set_value(m.is_true(s.s));
-            if (!s.is_true()) m_upper += s.weight;
+            if (!s.is_true())
+                m_upper += s.weight;
         }
+
+        // return true;
+
+        preprocess pp(s());
+        rational lower(0);
+        bool r = pp(m_soft, lower);
+
+        m_c.add_offset(m_index, lower);
+        m_upper -= lower;
         
         TRACE("opt", 
-              tout << "upper: " << m_upper << " assignments: ";
+              tout << "lower " << lower << " upper: " << m_upper << " assignments: ";
               for (soft& s : m_soft) tout << (s.is_true()?"T":"F");              
               tout << "\n";);
-        return true;
+        return r;
     }
 
     void maxsmt_solver_base::set_mus(bool f) {
@@ -153,80 +168,15 @@ namespace opt {
 
     void maxsmt_solver_base::trace_bounds(char const * solver) {
         IF_VERBOSE(1, 
-                   rational l = m_adjust_value(m_lower);
+                   rational l = m_c.adjust(m_index, m_lower);
-                   rational u = m_adjust_value(m_upper);
+                   rational u = m_c.adjust(m_index, m_upper);
                    if (l > u) std::swap(l, u);
                    verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";);                
     }
 
-    lbool maxsmt_solver_base::find_mutexes(obj_map<expr, rational>& new_soft) {
-        m_lower.reset();
-        expr_ref_vector fmls(m);
-        for (soft& s : m_soft) {
-            new_soft.insert(s.s, s.weight);
-            fmls.push_back(s.s);
-        }
-        vector<expr_ref_vector> mutexes;
-        lbool is_sat = s().find_mutexes(fmls, mutexes);
-        if (is_sat != l_true) {
-            return is_sat;
-        }
-        for (auto& mux : mutexes) {
-            process_mutex(mux, new_soft);
-        }
-        return l_true;
-    }
-
-    struct maxsmt_compare_soft {
-        obj_map<expr, rational> const& m_soft;
-        maxsmt_compare_soft(obj_map<expr, rational> const& soft): m_soft(soft) {}
-        bool operator()(expr* a, expr* b) const {
-            return m_soft.find(a) > m_soft.find(b);
-        }
-    };
-
-    void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft) {
-        TRACE("opt", 
-              for (expr* e : mutex) {
-                  tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
-              });
-        if (mutex.size() <= 1) {
-            return;
-        }
-        maxsmt_compare_soft cmp(new_soft);
-        ptr_vector<expr> _mutex(mutex.size(), mutex.data());
-        std::sort(_mutex.begin(), _mutex.end(), cmp);
-        mutex.reset();
-        mutex.append(_mutex.size(), _mutex.data());
-
-        rational weight(0), sum1(0), sum2(0);
-        vector<rational> weights;
-        for (expr* e : mutex) {
-            rational w = new_soft.find(e);
-            weights.push_back(w);
-            sum1 += w;
-            new_soft.remove(e);
-        }
-        for (unsigned i = mutex.size(); i-- > 0; ) {
-            expr_ref soft(m.mk_or(i+1, mutex.data()), m);
-            m_trail.push_back(soft);
-            rational w = weights[i];
-            weight = w - weight;
-            m_lower += weight*rational(i);
-            IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
-            sum2 += weight*rational(i+1);
-            new_soft.insert(soft, weight);
-            for (; i > 0 && weights[i-1] == w; --i) {} 
-            weight = w;
-        }        
-        SASSERT(sum1 == sum2);        
-    }
-
-
 
     maxsmt::maxsmt(maxsat_context& c, unsigned index):
-        m(c.get_manager()), m_c(c), m_index(index), 
+        m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {}
-        m_soft_constraints(m), m_answer(m) {}
 
     lbool maxsmt::operator()() {
         lbool is_sat = l_undef;
@@ -235,30 +185,29 @@ namespace opt {
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
-        if (optp.maxlex_enable() && is_maxlex(m_weights)) {
+        if (optp.maxlex_enable() && is_maxlex(m_soft)) {
-            m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_maxlex(m_c, m_index, m_soft);            
         }
-        else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
+        else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
-            m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_maxres(m_c, m_index, m_soft);            
         }
         else if (maxsat_engine == symbol("pd-maxres")) {            
-            m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft);
         }
         else if (maxsat_engine == symbol("wmax")) {
-            m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
+            m_msolver = mk_wmax(m_c, m_soft, m_index);
         }
         else if (maxsat_engine == symbol("sortmax")) {
-            m_msolver = mk_sortmax(m_c, m_weights, m_soft_constraints);
+            m_msolver = mk_sortmax(m_c, m_soft, m_index);
         }
         else {
             auto str = maxsat_engine.str();
             warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str());
-            m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+            m_msolver = mk_maxres(m_c, m_index, m_soft);
         }
 
         if (m_msolver) {
             m_msolver->updt_params(m_params);
-            m_msolver->set_adjust_value(m_adjust_value);
             is_sat = l_undef;
             try {
                 is_sat = (*m_msolver)();
@@ -282,14 +231,13 @@ namespace opt {
         return is_sat;
     }
 
-    void maxsmt::set_adjust_value(adjust_value& adj) { 
+    void maxsmt::reset_upper() {
-        m_adjust_value = adj; 
         if (m_msolver) {
-            m_msolver->set_adjust_value(m_adjust_value);
+            m_msolver->reset_upper();
+            m_upper = m_msolver->get_upper();
         }
     }
 
-
     void maxsmt::verify_assignment() {
         // TBD: have to use a different solver 
         // because we don't push local scope any longer.
@@ -311,7 +259,7 @@ namespace opt {
             rational q = m_msolver->get_lower();
             if (q > r) r = q;
         }
-        return m_adjust_value(r);
+        return m_c.adjust(m_index, r);
     }
 
     rational maxsmt::get_upper() const {
@@ -320,7 +268,7 @@ namespace opt {
             rational q = m_msolver->get_upper();
             if (q < r) r = q; 
         }
-        return m_adjust_value(r);
+        return m_c.adjust(m_index, r);
     }
 
     void maxsmt::update_lower(rational const& r) {
@@ -348,39 +296,32 @@ namespace opt {
         SASSERT(w.is_pos());
         unsigned index = 0;
         if (m_soft_constraint_index.find(f, index)) {
-            m_weights[index] += w;
+            m_soft[index].weight += w;
         }
         else {
-            m_soft_constraint_index.insert(f, m_weights.size());
+            m_soft_constraint_index.insert(f, m_soft.size());
-            m_soft_constraints.push_back(f);
+            m_soft.push_back(soft(expr_ref(f, m), w, false));
-            m_weights.push_back(w);
         }
         m_upper += w;
     }
 
     struct cmp_first {
         bool operator()(std::pair<unsigned, rational> const& x, std::pair<unsigned, rational> const& y) const {
-            return x.first < y.first;
+            return x.second < y.second;
         }
     };
 
     void maxsmt::display_answer(std::ostream& out) const {
-        vector<std::pair<unsigned, rational>> sorted_weights;
+
-        unsigned n = m_weights.size();
+        unsigned idx = 0;
-        for (unsigned i = 0; i < n; ++i) {
+        for (auto const & [_e, w, t] : m_soft) {
-            sorted_weights.push_back(std::make_pair(i, m_weights[i]));
+            expr* e = _e.get();
-        }
-        std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first());
-        sorted_weights.reverse();
-        for (unsigned i = 0; i < n; ++i) {
-            unsigned idx = sorted_weights[i].first;
-            expr* e = m_soft_constraints[idx];
             bool is_not = m.is_not(e, e);
-            out << m_weights[idx] << ": " << mk_pp(e, m)
+            out << w << ": " << mk_pp(e, m)
                 << ((is_not != get_assignment(idx))?" |-> true ":" |-> false ")
                 << "\n";
-            
+            ++idx;
-        }
+        }       
     }
     
     
@@ -420,6 +361,7 @@ namespace opt {
         model_ref  m_model;
         ref<generic_model_converter> m_fm; 
         symbol m_maxsat_engine;
+        vector<rational> m_offsets;
     public:
         solver_maxsat_context(params_ref& p, solver* s, model * m): 
             m_params(p), 
@@ -444,6 +386,14 @@ namespace opt {
         bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; };
         void set_model(model_ref& _m) override { m_model = _m; }
         void model_updated(model* mdl) override { } // no-op
+        rational adjust(unsigned id, rational const& r) override {
+            m_offsets.reserve(id+1);
+            return r + m_offsets[id];
+        }
+        void add_offset(unsigned id, rational const& r) override {
+            m_offsets.reserve(id+1);
+            m_offsets[id] += r;
+        }
     };
 
     lbool maxsmt_wrapper::operator()(vector<std::pair<expr*,rational>>& soft) {

src/opt/maxsmt.h

@@ -34,8 +34,6 @@ namespace opt {
     class maxsat_context;
 
     class maxsmt_solver {
-    protected:
-        adjust_value m_adjust_value;
     public:        
         virtual ~maxsmt_solver() {}
         virtual lbool operator()() = 0;
@@ -45,28 +43,30 @@ namespace opt {
         virtual void collect_statistics(statistics& st) const = 0;
         virtual void get_model(model_ref& mdl, svector<symbol>& labels) = 0;
         virtual void updt_params(params_ref& p) = 0;
-        void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; }
 
     };
 
     // ---------------------------------------------
     // base class with common utilities used
     // by maxsmt solvers
-    // 
+    //
+
+    struct soft { 
+        expr_ref  s; 
+        rational  weight; 
+        lbool     value;
+        void set_value(bool t) { value = t?l_true:l_undef; }
+        void set_value(lbool t) { value = t; }
+        bool is_true() const { return value == l_true; }
+        soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
+    };
+
     class maxsmt_solver_base : public maxsmt_solver {
     protected:
-        struct soft { 
-            expr_ref  s; 
-            rational  weight; 
-            lbool     value;
-            void set_value(bool t) { value = t?l_true:l_undef; }
-            void set_value(lbool t) { value = t; }
-            bool is_true() const { return value == l_true; }
-            soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {}
-        };
         ast_manager&     m;
-        maxsat_context&  m_c;        
+        maxsat_context&  m_c;
-        vector<soft>     m_soft;
+        unsigned         m_index;
+        vector<soft>&    m_soft;
         expr_ref_vector  m_assertions;
         expr_ref_vector  m_trail;
         rational         m_lower;
@@ -76,8 +76,8 @@ namespace opt {
         params_ref       m_params;           // config
 
     public:
-        maxsmt_solver_base(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft); 
+        maxsmt_solver_base(maxsat_context& c, vector<soft>& soft, unsigned index);
-
+        
         ~maxsmt_solver_base() override {}
         rational get_lower() const override { return m_lower; }
         rational get_upper() const override { return m_upper; }
@@ -102,16 +102,13 @@ namespace opt {
             smt::theory_wmaxsat& operator()();
         };
 
-        lbool find_mutexes(obj_map<expr, rational>& new_soft);
+        void reset_upper();
         
 
     protected:
         void enable_sls(bool force);
         void trace_bounds(char const* solver);
 
-        void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft);
-
-
     };
 
     /**
@@ -124,13 +121,11 @@ namespace opt {
         maxsat_context&           m_c;
         unsigned                  m_index;
         scoped_ptr<maxsmt_solver_base> m_msolver;
-        expr_ref_vector  m_soft_constraints;
+        vector<soft>     m_soft;
         obj_map<expr, unsigned> m_soft_constraint_index;
         expr_ref_vector  m_answer;
-        vector<rational> m_weights;
         rational         m_lower;
         rational         m_upper;
-        adjust_value     m_adjust_value;
         model_ref        m_model;
         svector<symbol>  m_labels;
         params_ref       m_params;
@@ -139,10 +134,9 @@ namespace opt {
         lbool operator()();
         void updt_params(params_ref& p);
         void add(expr* f, rational const& w); 
-        void set_adjust_value(adjust_value& adj);
+        unsigned size() const { return m_soft.size(); }
-        unsigned size() const { return m_soft_constraints.size(); }
+        expr* operator[](unsigned idx) const { return m_soft[idx].s; }
-        expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; }
+        rational weight(unsigned idx) const { return m_soft[idx].weight; }
-        rational weight(unsigned idx) const { return m_weights[idx]; }
         void commit_assignment();
         rational get_lower() const;
         rational get_upper() const;        
@@ -153,6 +147,7 @@ namespace opt {
         void display_answer(std::ostream& out) const;        
         void collect_statistics(statistics& st) const;
         void model_updated(model* mdl);
+        void reset_upper();
     private:
         bool is_maxsat_problem(weights_t& ws) const;        
         void verify_assignment();

src/opt/opt_context.cpp

@@ -185,17 +185,36 @@ namespace opt {
     }
 
     void context::set_hard_constraints(expr_ref_vector const& fmls) {
-        if (m_scoped_state.set(fmls)) {
+        if (m_calling_on_model) {
+            for (expr* f : fmls)
+                add_hard_constraint(f);
+            return;
+        }
+        if (m_scoped_state.set(fmls)) 
+            clear_state();
+    }
+
+    void context::add_hard_constraint(expr* f) {
+        if (m_calling_on_model) {
+            get_solver().assert_expr(f);
+            for (auto const& [k, v] : m_maxsmts)
+                v->reset_upper();
+            for (unsigned i = 0; i < num_objectives(); ++i) {
+                auto const& o = m_scoped_state.m_objectives[i]; 
+                if (o.m_type != O_MAXSMT)
+                    m_optsmt.update_upper(o.m_index, inf_eps::infinity());
+            }
+        }
+        else {
+            m_scoped_state.add(f);
             clear_state();
         }
     }
-
+    
-    void context::add_hard_constraint(expr* f) { 
-        m_scoped_state.add(f);
-        clear_state();
-    }
 
     void context::add_hard_constraint(expr* f, expr* t) {
+        if (m_calling_on_model) 
+            throw default_exception("adding soft constraints is not supported during callbacks");
         m_scoped_state.m_asms.push_back(t);
         m_scoped_state.add(m.mk_implies(t, f));
         clear_state();
@@ -379,7 +398,7 @@ namespace opt {
     }
 
     void context::set_model(model_ref& m) { 
-        m_model = m; 
+        m_model = m;
         opt_params optp(m_params);
         if (optp.dump_models() && m) {
             model_ref md = m->copy();
@@ -389,6 +408,7 @@ namespace opt {
             model_ref md = m->copy();
             if (!m_model_fixed.contains(md.get()))
                 fix_model(md);
+            flet<bool> _calling(m_calling_on_model, true);
             m_on_model_eh(m_on_model_ctx, md);
             m_model_fixed.pop_back();
         }
@@ -910,7 +930,8 @@ namespace opt {
     bool context::is_maxsat(expr* fml, expr_ref_vector& terms, 
                             vector<rational>& weights, rational& offset, 
                             bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) {
-        if (!is_app(fml)) return false;
+        if (!is_app(fml))
+            return false;
         neg = false;
         orig_term = nullptr;
         index = 0;
@@ -1085,8 +1106,7 @@ namespace opt {
                 obj.m_weights.append(weights);
                 obj.m_adjust_value.set_offset(offset);
                 obj.m_adjust_value.set_negate(neg);
-                m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value);
+                TRACE("opt", tout << "maxsat: " << neg << " " << id << " offset: " << offset << "\n";
-                TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";
                       tout << terms << "\n";);
             }
             else if (is_maximize(fml, tr, orig_term, index)) {
@@ -1138,7 +1158,14 @@ namespace opt {
 #endif
     }
 
+    rational context::adjust(unsigned id, rational const& v) {
+        return m_objectives[id].m_adjust_value(v);
+    }
 
+    void context::add_offset(unsigned id, rational const& o) {
+        m_objectives[id].m_adjust_value.add_offset(o);
+    }
+    
     bool context::verify_model(unsigned index, model* md, rational const& _v) {
         rational r;
         app_ref term = m_objectives[index].m_term;
@@ -1321,24 +1348,21 @@ namespace opt {
                 break;
             }
             case O_MAXSMT: {
-                bool ok = true;
+                for (unsigned j = 0; j < obj.m_terms.size(); ++j) {
-                for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) {
                     val = (*m_model)(obj.m_terms[j]);
                     TRACE("opt", tout << mk_pp(obj.m_terms[j], m) << " " << val << "\n";);
-                    if (!m.is_true(val)) {
+                    if (!m.is_true(val)) 
                         r += obj.m_weights[j];
-                    }
                 }
-                if (ok) {
+
-                    maxsmt& ms = *m_maxsmts.find(obj.m_id);
+                maxsmt& ms = *m_maxsmts.find(obj.m_id);
-                    if (is_lower) {
+                if (is_lower) {
-                        ms.update_upper(r);
+                    ms.update_upper(r);
-                        TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";);                        
+                    TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";);           
-                    }
+                }
-                    else {
+                else {
-                        ms.update_lower(r);
+                    ms.update_lower(r);
-                        TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";);                        
+                    TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";);           
-                    }
                 }
                 break;
             }

src/opt/opt_context.h

@@ -57,6 +57,8 @@ namespace opt {
         virtual smt::context& smt_context() = 0;    // access SMT context for SMT based MaxSMT solver (wmax requires SMT core)
         virtual unsigned num_objectives() = 0;
         virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0;
+        virtual rational adjust(unsigned id, rational const& v) = 0;
+        virtual void add_offset(unsigned id, rational const& o) = 0;
         virtual void set_model(model_ref& _m) = 0;
         virtual void model_updated(model* mdl) = 0;
     };
@@ -93,7 +95,7 @@ namespace opt {
             app_ref     m_term;          // for maximize, minimize term
             expr_ref_vector   m_terms;   // for maxsmt
             vector<rational>  m_weights; // for maxsmt
-            adjust_value  m_adjust_value;
+            adjust_value      m_adjust_value;
             symbol      m_id;            // for maxsmt
             unsigned    m_index;         // for maximize/minimize index
 
@@ -165,6 +167,7 @@ namespace opt {
         ast_manager&        m;
         on_model_t          m_on_model_ctx;
         std::function<void(on_model_t&, model_ref&)> m_on_model_eh;
+        bool                m_calling_on_model = false;
         arith_util          m_arith;
         bv_util             m_bv;
         expr_ref_vector     m_hard_constraints;
@@ -268,11 +271,14 @@ namespace opt {
         
         void model_updated(model* mdl) override;
 
+        rational adjust(unsigned id, rational const& v) override;
+
+        void add_offset(unsigned id, rational const& o) override;
+
         void register_on_model(on_model_t& ctx, std::function<void(on_model_t&, model_ref&)>& on_model) { 
             m_on_model_ctx = ctx; 
             m_on_model_eh  = on_model; 
         }
-
       
         void collect_timer_stats(statistics& st) const {
 	  if (m_time != 0) 

src/opt/opt_mux.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_mux.h
+
+Abstract:
+   
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+    class mux {
+        ast_manager&     m;
+        solver&          s;
+
+    public:
+        mux(solver& s);
+        lbool operator()(vector<soft>& soft, rational& bound);
+    };
+};

src/opt/opt_preprocess.cpp

@@ -0,0 +1,102 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_preprocess.cpp
+
+Abstract:
+   
+    Pre-processing for MaxSMT
+
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/opt_preprocess.h"
+
+namespace opt {
+
+    bool preprocess::find_mutexes(vector<soft>& softs, rational& lower) {
+        expr_ref_vector fmls(m);
+        obj_map<expr, rational> new_soft;
+        for (soft& sf : softs) {
+            m_trail.push_back(sf.s);
+            if (new_soft.contains(sf.s))
+                new_soft[sf.s] += sf.weight;
+            else
+                new_soft.insert(sf.s, sf.weight);
+            fmls.push_back(sf.s);
+        }
+        vector<expr_ref_vector> mutexes;
+        lbool is_sat = s.find_mutexes(fmls, mutexes);
+        if (is_sat == l_false)
+            return true;
+        if (is_sat == l_undef)
+            return false;
+        for (auto& mux : mutexes) 
+            process_mutex(mux, new_soft, lower);
+        softs.reset();
+        for (auto const& [k, v] : new_soft)
+            softs.push_back(soft(expr_ref(k, m), v, false));
+        m_trail.reset();
+        return true;
+    }
+
+    struct maxsmt_compare_soft {
+        obj_map<expr, rational> const& m_soft;
+        maxsmt_compare_soft(obj_map<expr, rational> const& soft): m_soft(soft) {}
+        bool operator()(expr* a, expr* b) const {
+            return m_soft.find(a) > m_soft.find(b);
+        }
+    };
+
+    void preprocess::process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower) {
+        TRACE("opt", 
+              for (expr* e : mutex) {
+                  tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
+              });
+        if (mutex.size() <= 1) 
+            return;
+
+        maxsmt_compare_soft cmp(new_soft);
+        ptr_vector<expr> _mutex(mutex.size(), mutex.data());
+        std::sort(_mutex.begin(), _mutex.end(), cmp);
+        mutex.reset();
+        mutex.append(_mutex.size(), _mutex.data());
+
+        rational weight(0), sum1(0), sum2(0);
+        vector<rational> weights;
+        for (expr* e : mutex) {
+            rational w = new_soft.find(e);
+            weights.push_back(w);
+            sum1 += w;
+            new_soft.remove(e);
+        }
+        for (unsigned i = mutex.size(); i-- > 0; ) {
+            expr_ref soft(m.mk_or(i+1, mutex.data()), m);
+            m_trail.push_back(soft);
+            rational w = weights[i];
+            weight = w - weight;
+            lower += weight*rational(i);
+            IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";);
+            sum2 += weight*rational(i+1);
+            new_soft.insert(soft, weight);
+            for (; i > 0 && weights[i-1] == w; --i) {} 
+            weight = w;
+        }        
+        SASSERT(sum1 == sum2);        
+    }
+
+    preprocess::preprocess(solver& s):  m(s.get_manager()), s(s), m_trail(m) {}
+    
+    bool preprocess::operator()(vector<soft>& soft, rational& lower) {
+        return find_mutexes(soft, lower);
+    }
+};

src/opt/opt_preprocess.h

@@ -0,0 +1,38 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    opt_preprocess.h
+
+Abstract:
+   
+    Pre-processing for MaxSMT
+
+    Find mutexes - at most 1 constraints and modify soft constraints and bounds.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-04-11
+
+--*/
+
+#pragma once
+
+#include "opt/maxsmt.h"
+
+namespace opt {
+
+    class preprocess {
+        ast_manager&     m;
+        solver&          s;
+        expr_ref_vector  m_trail;
+
+        bool find_mutexes(vector<soft>& softs, rational& lower);
+        void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
+
+    public:
+        preprocess(solver& s);
+        bool operator()(vector<soft>& soft, rational& lower);
+    };
+};

src/opt/opt_solver.h

@@ -48,6 +48,7 @@ namespace opt {
         void set_offset(rational const& o) { m_offset = o; }
         void set_negate(bool neg) { m_negate = neg; }
         rational const& get_offset() const { return m_offset; }
+        void add_offset(rational const& o) { if (m_negate) m_offset -= o; else m_offset += o; }
         bool get_negate() { return m_negate; }
         inf_eps operator()(inf_eps const& r) const {
             inf_eps result = r;

src/opt/sortmax.cpp

@@ -36,34 +36,27 @@ namespace opt {
         expr_ref_vector   m_trail;
         func_decl_ref_vector m_fresh;
         ref<generic_model_converter> m_filter;
-        sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
+        sortmax(maxsat_context& c, vector<soft>& s, unsigned index): 
-            maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {}
+            maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {}
 
         ~sortmax() override {}
 
         lbool operator()() override {
-            obj_map<expr, rational> soft;            
+            if (!init()) 
-            if (!init()) {
+                return l_undef;
-                return l_false;
+
-            }
+            lbool is_sat = l_true;
-            lbool is_sat = find_mutexes(soft);
-            if (is_sat != l_true) {
-                return is_sat;
-            }
             m_filter = alloc(generic_model_converter, m, "sortmax");
-            rational offset = m_lower;
-            m_upper = offset;
             expr_ref_vector in(m);
             expr_ref tmp(m);
             ptr_vector<expr> out;
-            obj_map<expr, rational>::iterator it = soft.begin(), end = soft.end();
+            for (auto const & [e, w, t] : m_soft) {
-            for (; it != end; ++it) {
+                if (!w.is_unsigned()) {
-                if (!it->m_value.is_unsigned()) {
                     throw default_exception("sortmax can only handle unsigned weights. Use a different heuristic.");
                 }
-                unsigned n = it->m_value.get_unsigned();
+                unsigned n = w.get_unsigned();
                 while (n > 0) {
-                    in.push_back(it->m_key);
+                    in.push_back(e);
                     --n;
                 }
             }
@@ -71,19 +64,15 @@ namespace opt {
 
             // initialize sorting network outputs using the initial assignment.
             unsigned first = 0;
-            it = soft.begin();
+            for (auto const & [e, w, t] : m_soft) {
-            for (; it != end; ++it) {
+                if (t == l_true) {
-                if (m_model->is_true(it->m_key)) {
+                    unsigned n = w.get_unsigned();
-                    unsigned n = it->m_value.get_unsigned();
                     while (n > 0) {
                         s().assert_expr(out[first]);
                         ++first;
                         --n;
                     }
                 }
-                else {
-                    m_upper += it->m_value;
-                }
             }
             while (l_true == is_sat && first < out.size() && m_lower < m_upper) {
                 trace_bounds("sortmax");
@@ -149,8 +138,8 @@ namespace opt {
     };
     
     
-    maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
+    maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector<soft>& s, unsigned index) {
-        return alloc(sortmax, c, ws, soft);
+        return alloc(sortmax, c, s, index);
     }
 
 }

src/opt/wmax.cpp

@@ -44,8 +44,8 @@ namespace opt {
         }
 
     public:
-        wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): 
+        wmax(maxsat_context& c, vector<soft>& s, unsigned index): 
-            maxsmt_solver_base(c, ws, soft),
+            maxsmt_solver_base(c, s, index),
             m_trail(m),
             m_defs(m) {}
 
@@ -54,22 +54,18 @@ namespace opt {
         lbool operator()() override {
             TRACE("opt", tout << "weighted maxsat\n";);
             scoped_ensure_theory wth(*this);
-            obj_map<expr, rational> soft;
             reset();
-            lbool is_sat = find_mutexes(soft);
+            if (init())
-            if (is_sat != l_true) {
+                return l_undef;
-                return is_sat;
+            
-            }
+            lbool is_sat = l_true;
-            m_upper = m_lower;
+            
             expr_ref_vector asms(m);
             vector<expr_ref_vector> cores;
 
-            for (auto const& kv : soft) {
+            for (auto const& [k, w, t] : m_soft) 
-                assert_weighted(wth(), kv.m_key, kv.m_value);
+                assert_weighted(wth(), k, w);
-                if (!is_true(kv.m_key)) {
+            
-                    m_upper += kv.m_value;
-                }
-            }
             wth().init_min_cost(m_upper - m_lower);
             trace_bounds("wmax");
 
@@ -308,8 +304,8 @@ namespace opt {
                 
     };
 
-    maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) {
+    maxsmt_solver_base* mk_wmax(maxsat_context& c, vector<soft> & s, unsigned index) {
-        return alloc(wmax, c, ws, soft);
+        return alloc(wmax, c, s, index);
     }
 
 }

src/opt/wmax.h

@@ -22,8 +22,8 @@ Notes:
 #include "opt/maxsmt.h"
 
 namespace opt {
-    maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_wmax(maxsat_context& c, vector<soft>& s, unsigned index);
 
-    maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft);
+    maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector<soft>& s, unsigned index);
 
 }

src/sat/sat_solver.cpp

@@ -3818,6 +3818,8 @@ namespace sat {
     void solver::move_to_front(bool_var b) {
         if (b >= num_vars())
             return;
+        if (m_case_split_queue.empty())
+            return;
         bool_var next = m_case_split_queue.min_var();
         auto next_act = m_activity[next];
         set_activity(b, next_act + 1);

src/sat/smt/arith_solver.cpp

@@ -549,13 +549,14 @@ namespace arith {
         found_compatible = false;
         for (; it != end; ++it) {
             api_bound* a2 = *it;
-            if (a1 == a2) continue;
+            if (a1 == a2)
-            if (a2->get_bound_kind() != kind) continue;
+                continue;
+            if (a2->get_bound_kind() != kind)
+                continue;
             rational const& k2(a2->get_value());
             found_compatible = true;
-            if (k1 < k2) {
+            if (k1 < k2) 
                 return it;
-            }
         }
         return end;
     }

src/sat/smt/euf_internalize.cpp

@@ -312,6 +312,7 @@ namespace euf {
             }
         }
         else if (m.is_distinct(e)) {
+            // TODO - add lazy case for large values of sz.
             expr_ref_vector eqs(m);
             unsigned sz = n->num_args();
             for (unsigned i = 0; i < sz; ++i) {

src/sat/smt/q_model_fixer.cpp

@@ -184,6 +184,8 @@ namespace q {
         for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
             expr* t = n->get_arg(idx)->get_expr();
             values.push_back(mdl(t));
+            if (!m.is_value(values.back())) 
+                return expr_ref(m.mk_var(idx, srt), m);
             md->v2t.insert(values.back(), t);
             md->t2v.insert(t, values.back());
         }
@@ -299,6 +301,10 @@ namespace q {
         auto term = [&](unsigned j) {
             return md->v2t[md->values[j]];
         };
+        
+        for (unsigned j = 0; j < sz; ++j)
+            std::cout << mk_pp(md->values[j], m) << "\n";
+
 
         expr* arg = t->get_arg(i);
 

src/sat/smt/user_solver.cpp

@@ -88,7 +88,7 @@ namespace user_solver {
     void solver::push_core() {
         th_euf_solver::push_core();
         m_prop_lim.push_back(m_prop.size());
-        m_push_eh(m_user_context);
+        m_push_eh(m_user_context, this);
     }
 
     void solver::pop_core(unsigned num_scopes) {
@@ -96,7 +96,7 @@ namespace user_solver {
         unsigned old_sz = m_prop_lim.size() - num_scopes;
         m_prop.shrink(m_prop_lim[old_sz]);
         m_prop_lim.shrink(old_sz);
-        m_pop_eh(m_user_context, num_scopes);
+        m_pop_eh(m_user_context, this, num_scopes);
     }
 
     void solver::propagate_consequence(prop_info const& prop) {

src/smt/theory_user_propagator.cpp

@@ -25,6 +25,7 @@ using namespace smt;
 theory_user_propagator::theory_user_propagator(context& ctx):
     theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())),
     m_var2expr(ctx.get_manager()),
+    m_push_popping(false),
     m_to_add(ctx.get_manager())
 {}
 
@@ -38,7 +39,7 @@ void theory_user_propagator::force_push() {
         theory::push_scope_eh();
         m_prop_lim.push_back(m_prop.size());
         m_to_add_lim.push_back(m_to_add.size());
-        m_push_eh(m_user_context);
+        m_push_eh(m_user_context, this);
     }
 }
 
@@ -122,7 +123,8 @@ final_check_status theory_user_propagator::final_check_eh() {
     if (!(bool)m_final_eh)
         return FC_DONE;
     force_push();
-    unsigned sz = m_prop.size();
+    unsigned sz1 = m_prop.size();
+    unsigned sz2 = m_expr2var.size();
     try {
         m_final_eh(m_user_context, this);
     }
@@ -130,7 +132,8 @@ final_check_status theory_user_propagator::final_check_eh() {
       throw default_exception("Exception thrown in \"final\"-callback");
     }
     propagate();
-    bool done = (sz == m_prop.size()) && !ctx.inconsistent();
+    // check if it became inconsistent or something new was propagated/registered
+    bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }
 
@@ -169,11 +172,11 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) {
     old_sz = m_to_add_lim.size() - num_scopes;
     m_to_add.shrink(m_to_add_lim[old_sz]);
     m_to_add_lim.shrink(old_sz);
-    m_pop_eh(m_user_context, num_scopes);
+    m_pop_eh(m_user_context, this, num_scopes);
 }
 
 bool theory_user_propagator::can_propagate() {
-    return m_qhead < m_prop.size() || !m_to_add.empty();
+    return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size();
 }
 
 void theory_user_propagator::propagate_consequence(prop_info const& prop) {

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -143,10 +143,9 @@ public:
         tactic_ref t;
         if (tp.default_tactic() != symbol::null &&
             !tp.default_tactic().is_numerical() && 
-            tp.default_tactic().bare_str() && 
+            tp.default_tactic().str()[0]) {
-            tp.default_tactic().bare_str()[0]) {
             cmd_context ctx(false, &m, l);
-            std::istringstream is(tp.default_tactic().bare_str());
+            std::istringstream is(tp.default_tactic().str());
             char const* file_name = "";
             sexpr_ref se = parse_sexpr(ctx, is, p, file_name);
             if (se) {

src/tactic/user_propagator_base.h

@@ -17,13 +17,13 @@ namespace user_propagator {
         virtual ~context_obj() = default;
     };
     
-    typedef std::function<void(void*, callback*)> final_eh_t;
+    typedef std::function<void(void*, callback*)>                    final_eh_t;
-    typedef std::function<void(void*, callback*, expr*, expr*)> fixed_eh_t;
+    typedef std::function<void(void*, callback*, expr*, expr*)>      fixed_eh_t;
-    typedef std::function<void(void*, callback*, expr*, expr*)> eq_eh_t;
+    typedef std::function<void(void*, callback*, expr*, expr*)>      eq_eh_t;
     typedef std::function<void*(void*, ast_manager&, context_obj*&)> fresh_eh_t;
-    typedef std::function<void(void*)>                 push_eh_t;
+    typedef std::function<void(void*, callback*)>                    push_eh_t;
-    typedef std::function<void(void*,unsigned)>        pop_eh_t;
+    typedef std::function<void(void*, callback*, unsigned)>          pop_eh_t;
-    typedef std::function<void(void*, callback*, expr*)> created_eh_t;
+    typedef std::function<void(void*, callback*, expr*)>             created_eh_t;
 
 
     class plugin : public decl_plugin {

src/util/params.cpp

@@ -24,15 +24,14 @@ Notes:
 
 params_ref params_ref::g_empty_params_ref;
 
-std::string norm_param_name(char const * n) {
+std::string norm_param_name(char const* n) {
-    if (n == nullptr)
-        return "_";
     if (*n == ':')
         n++;
     std::string r = n;
     unsigned sz = static_cast<unsigned>(r.size());
     if (sz == 0)
         return "_";
+        
     for (unsigned i = 0; i < sz; i++) {
         char curr = r[i];
         if ('A' <= curr && curr <= 'Z')
@@ -44,6 +43,8 @@ std::string norm_param_name(char const * n) {
 }
 
 std::string norm_param_name(symbol const & n) {
+    if (n.is_null())
+        return "_";
     return norm_param_name(n.bare_str());
 }
 
@@ -156,8 +157,8 @@ struct param_descrs::imp {
         return m_names[idx];
     }
 
-    struct lt {
+    struct symlt {
-        bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; }
+        bool operator()(symbol const & s1, symbol const & s2) const { return ::lt(s1, s2); }        
     };
 
     void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
@@ -165,13 +166,13 @@ struct param_descrs::imp {
         for (auto const& kv : m_info) {
             names.push_back(kv.m_key);
         }
-        std::sort(names.begin(), names.end(), lt());
+        std::sort(names.begin(), names.end(), symlt());
         for (symbol const& name : names) {
             for (unsigned i = 0; i < indent; i++) out << " ";
             if (smt2_style)
                 out << ':';
-            char const * s = name.bare_str();
+            std::string s = name.str();
-            unsigned n = static_cast<unsigned>(strlen(s));
+            unsigned n = static_cast<unsigned>(s.length());
             for (unsigned i = 0; i < n; i++) {
                 if (smt2_style && s[i] == '_')
                     out << '-';