merge

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

.github/workflows/docker-image.yml

@@ -0,0 +1,61 @@
+name: Publish Docker image
+
+on:
+  schedule:
+    - cron: "0 1 * * 0" # every Sunday at 1 am
+  workflow_dispatch: # on button click
+
+jobs:
+  push_to_registry:
+    name: Push Docker image to GitHub Docker registry
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Check out the repo        
+        uses: actions/checkout@v2
+
+      - name: Log in to GitHub Docker registry
+        uses: docker/login-action@v1
+        with:
+          registry: ghcr.io
+          username: ${{ secrets.DOCKER_USERNAME }}
+          password: ${{ secrets.DOCKER_PASSWORD }}
+
+      # -------
+      # BARE Z3
+      # -------
+      - name: Extract metadata (tags, labels) for Bare Z3 Docker Image
+        id: meta
+        uses: docker/metadata-action@v3
+        with:
+          images: ghcr.io/z3prover/z3
+          flavor: |
+            latest=auto
+            prefix=ubuntu-20.04-bare-z3-
+          tags: |
+            type=schedule,pattern={{date 'YYYYMMDD'}}
+            type=ref,event=tag
+            type=edge
+            type=sha,prefix=ubuntu-20.04-bare-z3-sha-
+      - name: Build and push Bare Z3 Docker Image
+        uses: docker/build-push-action@v2.7.0
+        with:  
+          context: .
+          push: true
+          target: bare-z3
+          file: ./docker/ubuntu-20-04.Dockerfile
+          tags: ${{ steps.meta.outputs.tags }}
+          labels: ${{ steps.meta.outputs.labels }}
+
+      # ------------------------------
+      # Repo description on GHCR
+      # ------------------------------
+#      - name: Update repo description
+#        uses: peter-evans/dockerhub-description@v2
+#        with:
+#          registry: ghcr.io        
+#          repository: z3prover/z3
+#          username: ${{ secrets.DOCKER_USERNAME }}
+#          password: ${{ secrets.DOCKER_PASSWORD }}
+#          short-description: ${{ github.event.repository.description }}
+#          readme-filepath: ./docker/README.md

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.8.14.0 LANGUAGES CXX)
+project(Z3 VERSION 4.8.15.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version

README.md

@@ -18,6 +18,8 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 | --------------- | --------------|-----------|---------------|------------|
 | [![Build Status](https://dev.azure.com/Z3Public/Z3/_apis/build/status/Z3Prover.z3?branchName=master)](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [![CodeCoverage](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) |
 
+<a href="https://github.com/z3prover/z3/pkgs/container/z3">Docker image</a>.
+
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
 [3]: #building-z3-using-cmake

azure-pipelines.yml

@@ -288,6 +288,7 @@ jobs:
 
 - job: "MacOSOCaml"
   displayName: "MacOS build with OCaml"
+  condition: eq(0,1) 
   pool:
     vmImage: "macOS-latest"
   steps:
@@ -310,9 +311,9 @@ jobs:
         eval `opam config env`
         make -j3
         make -j3 _ex_ml_example_post_install
-        ./ml_example_shared.byte
+        # ./ml_example_shared.byte
-        ./ml_example_shared_custom.byte
+        # ./ml_example_shared_custom.byte
-        ./ml_example_shared
+        # ./ml_example_shared
         cd ..
 # Skip as dead-slow in debug mode:
 #  - template: scripts/test-z3.yml

docker/ubuntu-20-04.Dockerfile

@@ -0,0 +1,45 @@
+# -------------
+# OS Base image
+# -------------
+# >> Includes system-wide dependencies
+FROM ubuntu:20.04 as lib-base
+ARG DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && \
+    apt-get -y --no-install-recommends install \
+        cmake \
+        make \
+        clang \
+        g++ \
+        curl \
+        default-jdk \
+        python3 \
+        python3-setuptools \
+        python-is-python3 \
+        sudo
+
+# ----------------
+# Z3 Builder Image
+# ----------------
+# >> Includes build files and compiles the basic z3 sources
+FROM lib-base as builder
+COPY ./ /z3-source/
+WORKDIR /z3-source/
+RUN python scripts/mk_make.py
+WORKDIR /z3-source/build/
+RUN make
+RUN sudo make install
+WORKDIR /z3-source/
+
+# -------
+# Bare z3
+# -------
+# >> Includes only stnadard z3 installations.
+# >> Can be used as a standalone interface to z3.
+FROM builder as bare-z3
+ENTRYPOINT [ "z3" ]
+
+# TODO: introduce Python-binding stage
+# ...
+
+# TODO(optional): introduce C/C++ -binding stage
+# ...

scripts/mk_nuget_task.py

@@ -65,7 +65,7 @@ def unpack(packages, symbols):
             mk_dir(f"out/runtimes/{dst}/native")
             replace(f"{tmp}/{package_dir}/bin/libz3.{ext}", f"out/runtimes/{dst}/native/libz3.{ext}")            
             if "x64-win" in f:
-                mk_dir("out/lib/netstandard1.4/")
+                mk_dir("out/lib/netstandard2.0/")
                 if symbols:
                     zip_ref.extract(f"{package_dir}/bin/libz3.pdb", f"{tmp}")
                     replace(f"{tmp}/{package_dir}/bin/libz3.pdb", f"out/runtimes/{dst}/native/libz3.pdb") 
@@ -74,7 +74,7 @@ def unpack(packages, symbols):
                     files += ["Microsoft.Z3.pdb", "Microsoft.Z3.xml"]
                 for b in files:
                     zip_ref.extract(f"{package_dir}/bin/{b}", f"{tmp}")
-                    replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard1.4/{b}")
+                    replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard2.0/{b}")
 
 def mk_targets(source_root):
     mk_dir("out/build")
@@ -107,7 +107,7 @@ Linux Dependencies:
         <requireLicenseAcceptance>true</requireLicenseAcceptance>
         <language>en</language>
         <dependencies>
-            <group targetFramework=".NETStandard1.4" />
+            <group targetFramework=".netstandard2.0" />
         </dependencies>
     </metadata>
 </package>""".format(version, repo, branch, commit)

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 8, 14, 0)
+    set_version(4, 8, 15, 0)
     
 # Z3 Project definition
 def init_project_def():

scripts/mk_util.py

@@ -15,7 +15,7 @@ import shutil
 from mk_exception import *
 import mk_genfile_common
 from fnmatch import fnmatch
-import distutils.sysconfig
+import sysconfig
 import compileall
 import subprocess
 
@@ -48,7 +48,7 @@ CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
 JAVAC=None
 JAR=None
-PYTHON_PACKAGE_DIR=distutils.sysconfig.get_python_lib(prefix=getenv("PREFIX", None))
+PYTHON_PACKAGE_DIR=sysconfig.get_path('purelib')
 BUILD_DIR='build'
 REV_BUILD_DIR='..'
 SRC_DIR='src'
@@ -92,7 +92,6 @@ DOTNET_CORE_ENABLED=False
 DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
 JAVA_ENABLED=False
 ML_ENABLED=False
-JS_ENABLED=False
 PYTHON_INSTALL_ENABLED=False
 STATIC_LIB=False
 STATIC_BIN=False
@@ -681,7 +680,7 @@ def display_help(exit_code):
 # Parse configuration option for mk_make script
 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, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
+    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
     try:
@@ -749,8 +748,6 @@ def parse_options():
             GIT_DESCRIBE = True
         elif opt in ('', '--ml'):
             ML_ENABLED = True
-        elif opt == "--js":
-            JS_ENABLED = True
         elif opt in ('', '--log-sync'):
             LOG_SYNC = True
         elif opt == '--single-threaded':
@@ -813,16 +810,6 @@ def set_build_dir(d):
     BUILD_DIR = norm_path(d)
     REV_BUILD_DIR = reverse_path(d)
 
-def set_z3js_dir(p):
-    global SRC_DIR, Z3JS_SRC_DIR
-    p = norm_path(p)
-    full = os.path.join(SRC_DIR, p)
-    if not os.path.exists(full):
-        raise MKException("Python bindings directory '%s' does not exist" % full)
-    Z3JS_SRC_DIR = full
-    if VERBOSE:
-        print("Js bindings directory was detected.")
-
 def set_z3py_dir(p):
     global SRC_DIR, Z3PY_SRC_DIR
     p = norm_path(p)
@@ -858,9 +845,6 @@ def get_components():
 def get_z3py_dir():
     return Z3PY_SRC_DIR
 
-# Return directory where the js bindings are located
-def get_z3js_dir():
-    return Z3JS_SRC_DIR
 
 # Return true if in verbose mode
 def is_verbose():
@@ -872,9 +856,6 @@ def is_java_enabled():
 def is_ml_enabled():
     return ML_ENABLED
 
-def is_js_enabled():
-    return JS_ENABLED
-
 def is_dotnet_core_enabled():
     return DOTNET_CORE_ENABLED
 
@@ -1611,7 +1592,7 @@ class PythonInstallComponent(Component):
                                       os.path.join(self.pythonPkgDir,'z3'),
                                       in_prefix=self.in_prefix_install)
 
-        if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
+        if PYTHON_PACKAGE_DIR != sysconfig.get_path('purelib'):
             out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
 
     def mk_uninstall(self, out):
@@ -2692,7 +2673,7 @@ def mk_config():
             print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
             if GPROF:
                 print('gprof:          enabled')
-            print('Python version: %s' % distutils.sysconfig.get_python_version())
+            print('Python version: %s' % sysconfig.get_python_version())
             if is_java_enabled():
                 print('JNI Bindings:   %s' % JNI_HOME)
                 print('Java Compiler:  %s' % JAVAC)
@@ -3025,17 +3006,14 @@ def mk_bindings(api_files):
         ml_output_dir = None
         if is_ml_enabled():
           ml_output_dir = get_component('ml').src_dir
-        if is_js_enabled():
-          set_z3js_dir("api/js")
-          js_output_dir = get_component('js').src_dir
         # Get the update_api module to do the work for us
+        update_api.VERBOSE = is_verbose()
         update_api.generate_files(api_files=new_api_files,
           api_output_dir=get_component('api').src_dir,
           z3py_output_dir=get_z3py_dir(),
           dotnet_output_dir=dotnet_output_dir,
           java_output_dir=java_output_dir,
           java_package_name=java_package_name,
-          js_output_dir=get_z3js_dir(),
           ml_output_dir=ml_output_dir,
           ml_src_dir=ml_output_dir
         )

scripts/release.yml

@@ -171,6 +171,7 @@ stages:
       inputs:
         artifact: 'WindowsBuild-x64'
         path: $(Agent.TempDirectory)\package
+    - task: DownloadPipelineArtifact@2        
       displayName: 'Download Win32 Build'
       inputs:
         artifact: 'WindowsBuild-x86'
@@ -313,7 +314,7 @@ stages:
   jobs:
 
   - job: GitHubPublish
-    condition: eq(0,1)
+    condition: eq(1,1)
     displayName: "Publish to GitHub"
     pool:
       vmImage: "windows-latest"

scripts/update_api.py

@@ -15,7 +15,7 @@ several API header files. It can also optionally
 emit some of the files required for Z3's different
 language bindings.
 """
-import mk_util
+
 import mk_exception
 import argparse
 import logging
@@ -23,6 +23,10 @@ import re
 import os
 import sys
 
+VERBOSE = True
+def is_verbose():
+    return VERBOSE
+
 ##########################################################
 # TODO: rewrite this file without using global variables.
 # This file is a big HACK.
@@ -78,37 +82,39 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
                 FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr',
                 PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr' }
 
-# Mapping to Java types
-Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
-              FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
-              BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' }
-
-Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
-               FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
-               BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'}
 
 # Mapping to ML types
 Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
             FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
             BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string' }
 
-next_type_id = FIRST_OBJ_ID
+class APITypes:
+    def __init__(self):
+        self.next_type_id = FIRST_OBJ_ID
 
-def def_Type(var, c_type, py_type):
+    def def_Type(self, var, c_type, py_type):
-    global next_type_id
+        """Process type definitions of the form def_Type(var, c_type, py_type)
-    exec('%s = %s' % (var, next_type_id), globals())
+        The variable 'var' is set to a unique number and recorded globally using exec
-    Type2Str[next_type_id] = c_type
+        It is used by 'def_APIs' to that uses the unique numbers to access the
-    Type2PyStr[next_type_id] = py_type
+        corresponding C and Python types.
-    next_type_id    = next_type_id + 1
+        """
+        id = self.next_type_id
+        exec('%s = %s' % (var, id), globals())
+        Type2Str[id] = c_type
+        Type2PyStr[id] = py_type
+        self.next_type_id += 1
         
-def def_Types(api_files):
+    def def_Types(self, api_files):
         pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
         for api_file in api_files:
-        api = open(api_file, 'r')
+            with open(api_file, 'r') as api:
                 for line in api:
                     m = pat1.match(line)
                     if m:
-                def_Type(m.group(1), m.group(2), m.group(3))
+                        self.def_Type(m.group(1), m.group(2), m.group(3))
+        #
+        # Populate object type entries in dotnet and ML bindings.
+        # 
         for k in Type2Str:
             v = Type2Str[k]
             if is_obj(k):
@@ -127,20 +133,6 @@ def type2dotnet(ty):
     global Type2Dotnet
     return Type2Dotnet[ty]
 
-def type2java(ty):
-    global Type2Java
-    if (ty >= FIRST_OBJ_ID):
-        return 'long'
-    else:
-        return Type2Java[ty]
-
-def type2javaw(ty):
-    global Type2JavaW
-    if (ty >= FIRST_OBJ_ID):
-        return 'jlong'
-    else:
-        return Type2JavaW[ty]
-
 def type2ml(ty):
     global Type2ML
     q = Type2ML[ty]
@@ -214,42 +206,8 @@ def param2dotnet(p):
     else:
         return type2dotnet(param_type(p))
 
-def param2java(p):
-    k = param_kind(p)
-    if k == OUT:
-        if param_type(p) == INT or param_type(p) == UINT:
-            return "IntPtr"
-        elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID:
-            return "LongPtr"
-        elif param_type(p) == STRING:
-            return "StringPtr"
-        else:
-            print("ERROR: unreachable code")
-            assert(False)
-            exit(1)
-    elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
-        return "%s[]" % type2java(param_type(p))
-    elif k == OUT_MANAGED_ARRAY:
-        if param_type(p) == UINT:
-            return "UIntArrayPtr"
-        else:
-            return "ObjArrayPtr"
-    else:
-        return type2java(param_type(p))
 
-def param2javaw(p):
+# --------------
-    k = param_kind(p)
-    if k == OUT:
-        return "jobject"
-    elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
-        if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
-            return "jintArray"
-        else:
-            return "jlongArray"
-    elif k == OUT_MANAGED_ARRAY:
-        return "jlong"
-    else:
-        return type2javaw(param_type(p))
 
 def param2pystr(p):
     if param_kind(p) == IN_ARRAY or param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT:
@@ -257,6 +215,9 @@ def param2pystr(p):
     else:
         return type2pystr(param_type(p))
 
+# --------------
+# ML
+
 def param2ml(p):
     k = param_kind(p)
     if k == OUT:
@@ -507,6 +468,68 @@ def mk_dotnet_wrappers(dotnet):
     dotnet.write("    }\n\n")
     dotnet.write("}\n\n")
 
+# ----------------------
+# Java
+
+Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
+              FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
+              BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long' }
+
+Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
+               FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
+               BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong'}
+
+def type2java(ty):
+    global Type2Java
+    if (ty >= FIRST_OBJ_ID):
+        return 'long'
+    else:
+        return Type2Java[ty]
+
+def type2javaw(ty):
+    global Type2JavaW
+    if (ty >= FIRST_OBJ_ID):
+        return 'jlong'
+    else:
+        return Type2JavaW[ty]
+
+def param2java(p):
+    k = param_kind(p)
+    if k == OUT:
+        if param_type(p) == INT or param_type(p) == UINT:
+            return "IntPtr"
+        elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID:
+            return "LongPtr"
+        elif param_type(p) == STRING:
+            return "StringPtr"
+        else:
+            print("ERROR: unreachable code")
+            assert(False)
+            exit(1)
+    elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
+        return "%s[]" % type2java(param_type(p))
+    elif k == OUT_MANAGED_ARRAY:
+        if param_type(p) == UINT:
+            return "UIntArrayPtr"
+        else:
+            return "ObjArrayPtr"
+    else:
+        return type2java(param_type(p))
+
+def param2javaw(p):
+    k = param_kind(p)
+    if k == OUT:
+        return "jobject"
+    elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
+        if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
+            return "jintArray"
+        else:
+            return "jlongArray"
+    elif k == OUT_MANAGED_ARRAY:
+        return "jlong"
+    else:
+        return type2javaw(param_type(p))
+
 def java_method_name(name):
     result = ''
     name = name[3:] # Remove Z3_
@@ -776,62 +799,9 @@ def mk_java(java_dir, package_name):
     java_wrapper.write('#ifdef __cplusplus\n')
     java_wrapper.write('}\n')
     java_wrapper.write('#endif\n')
-    if mk_util.is_verbose():
+    if is_verbose():
         print("Generated '%s'" % java_nativef)
 
-
-Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number',
-            FLOAT : 'number', STRING : 'string', STRING_PTR : 'array',
-            BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number', CHAR : 'number' }
-
-def type2napi(t):
-    try:
-       return Type2Napi[t]
-    except:
-       return "external"
-
-Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double',
-            FLOAT : 'float', STRING : 'string', STRING_PTR : 'array',
-            BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32', CHAR : 'char' }
-
-def type2napibuilder(t):
-    try:
-       return Type2NapiBuilder[t]
-    except:
-       return "external"
-
-
-def mk_js(js_output_dir):
-    with open(os.path.join(js_output_dir, "z3.json"), 'w') as ous:
-       ous.write("{\n")
-       ous.write("  \"api\": [\n")
-       for name, result, params in _dotnet_decls:
-           ous.write("    {\n")
-           ous.write("       \"name\": \"%s\",\n" % name)
-           ous.write("       \"c_type\": \"%s\",\n" % Type2Str[result])
-           ous.write("       \"napi_type\": \"%s\",\n" % type2napi(result))
-           ous.write("       \"arg_list\": [")
-           first = True
-           for p in params:
-               if first:
-                  first = False
-                  ous.write("\n         {\n")
-               else:
-                  ous.write(",\n         {\n")
-               t = param_type(p)
-               k = t
-               ous.write("            \"name\": \"%s\",\n" % "")                        # TBD
-               ous.write("            \"c_type\": \"%s\",\n" % type2str(t))
-               ous.write("            \"napi_type\": \"%s\",\n" % type2napi(t))
-               ous.write("            \"napi_builder\": \"%s\"\n" % type2napibuilder(t))
-               ous.write(  "         }")
-           ous.write("],\n")
-           ous.write("       \"napi_builder\": \"%s\"\n" % type2napibuilder(result))
-           ous.write("    },\n")
-       ous.write("  ]\n")
-       ous.write("}\n")
-
-
 def mk_log_header(file, name, params):
     file.write("void log_%s(" % name)
     i = 0
@@ -842,6 +812,10 @@ def mk_log_header(file, name, params):
         i = i + 1
     file.write(")")
 
+# ---------------------------------
+# Logging
+
+
 def log_param(p):
     kind = param_kind(p)
     ty   = param_type(p)
@@ -1364,7 +1338,7 @@ def mk_ml(ml_src_dir, ml_output_dir):
     ml_native.write('(**/**)\n')
     ml_native.close()
 
-    if mk_util.is_verbose():
+    if is_verbose():
         print ('Generated "%s"' % ml_nativef)
 
     mk_z3native_stubs_c(ml_src_dir, ml_output_dir)
@@ -1689,7 +1663,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
     ml_wrapper.write('}\n')
     ml_wrapper.write('#endif\n')
 
-    if mk_util.is_verbose():
+    if is_verbose():
         print ('Generated "%s"' % ml_wrapperf)
 
 # Collect API(...) commands from
@@ -1889,7 +1863,6 @@ def generate_files(api_files,
                    dotnet_output_dir=None,
                    java_output_dir=None,
                    java_package_name=None,
-                   js_output_dir=None,
                    ml_output_dir=None,
                    ml_src_dir=None):
   """
@@ -1933,6 +1906,7 @@ def generate_files(api_files,
       import tempfile
       return tempfile.TemporaryFile(mode=mode)
 
+  apiTypes = APITypes()
   with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h:
     with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c:
       with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c:
@@ -1944,13 +1918,13 @@ def generate_files(api_files,
           write_core_py_preamble(core_py)
 
           # FIXME: these functions are awful
-          def_Types(api_files)
+          apiTypes.def_Types(api_files)
           def_APIs(api_files)
           mk_bindings(exe_c)
           mk_py_wrappers()
           write_core_py_post(core_py)
 
-          if mk_util.is_verbose():
+          if is_verbose():
             print("Generated '{}'".format(log_h.name))
             print("Generated '{}'".format(log_c.name))
             print("Generated '{}'".format(exe_c.name))
@@ -1960,7 +1934,7 @@ def generate_files(api_files,
     with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file:
       mk_dotnet(dotnet_file)
       mk_dotnet_wrappers(dotnet_file)
-      if mk_util.is_verbose():
+      if is_verbose():
         print("Generated '{}'".format(dotnet_file.name))
 
   if java_output_dir:
@@ -1970,8 +1944,6 @@ def generate_files(api_files,
     assert not ml_src_dir is None
     mk_ml(ml_src_dir, ml_output_dir)
 
-  if js_output_dir:
-    mk_js(js_output_dir)
 
 def main(args):
   logging.basicConfig(level=logging.INFO)
@@ -2006,10 +1978,6 @@ def main(args):
                       dest="ml_output_dir",
                       default=None,
                       help="Directory to emit OCaml files. If not specified no files are emitted.")
-  parser.add_argument("--js_output_dir",
-                      dest="js_output_dir",
-                      default=None,
-                      help="Directory to emit js bindings. If not specified no files are emitted.")
   pargs = parser.parse_args(args)
 
   if pargs.java_output_dir:
@@ -2033,7 +2001,6 @@ def main(args):
                  dotnet_output_dir=pargs.dotnet_output_dir,
                  java_output_dir=pargs.java_output_dir,
                  java_package_name=pargs.java_package_name,
-                 js_output_dir=pargs.js_output_dir,
                  ml_output_dir=pargs.ml_output_dir,
                  ml_src_dir=pargs.ml_src_dir)
   return 0

src/api/api_config_params.cpp

@@ -47,7 +47,7 @@ extern "C" {
         env_params::updt_params();
     }
     
-    Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
+    Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
         memory::initialize(UINT_MAX);
         LOG_Z3_global_param_get(param_id, param_value);
         *param_value = nullptr;

src/api/api_datalog.cpp

@@ -585,7 +585,7 @@ extern "C" {
         to_fixedpoint_ref(d)->collect_param_descrs(descrs);
         to_params(p)->m_params.validate(descrs);
         to_fixedpoint_ref(d)->updt_params(to_param_ref(p));
-        to_fixedpoint(d)->m_params = to_param_ref(p);
+        to_fixedpoint(d)->m_params.append(to_param_ref(p));
         Z3_CATCH;
     }
 

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

@@ -701,6 +701,9 @@ namespace z3 {
         sort array_range() const { assert(is_array()); Z3_sort s = Z3_get_array_sort_range(ctx(), *this); check_error(); return sort(ctx(), s); }
 
         friend std::ostream & operator<<(std::ostream & out, sort const & s) { return out << Z3_sort_to_string(s.ctx(), Z3_sort(s.m_ast)); }
+
+        func_decl_vector constructors();
+        func_decl_vector recognizers();
     };
 
     /**
@@ -741,6 +744,9 @@ namespace z3 {
         expr operator()(expr const & a1, expr const & a2, expr const & a3) const;
         expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4) const;
         expr operator()(expr const & a1, expr const & a2, expr const & a3, expr const & a4, expr const & a5) const;
+
+        func_decl_vector accessors();
+
     };
 
     /**
@@ -3863,6 +3869,42 @@ namespace z3 {
         return expr_vector(*this, r);
     }
 
+    inline func_decl_vector sort::constructors() {
+        assert(is_datatype()); 
+        func_decl_vector cs(ctx());
+        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
+        for (unsigned i = 0; i < n; ++i) 
+            cs.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor(ctx(), *this, i)));
+        return cs;
+    }
+
+    inline func_decl_vector sort::recognizers() {
+        assert(is_datatype()); 
+        func_decl_vector rs(ctx());
+        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), *this);
+        for (unsigned i = 0; i < n; ++i) 
+            rs.push_back(func_decl(ctx(), Z3_get_datatype_sort_recognizer(ctx(), *this, i)));
+        return rs;
+    }
+
+    inline func_decl_vector func_decl::accessors() {
+        sort s = range();
+        assert(s.is_datatype());
+        unsigned n = Z3_get_datatype_sort_num_constructors(ctx(), s);
+        unsigned idx = 0;
+        for (; idx < n; ++idx) {
+            func_decl f(ctx(), Z3_get_datatype_sort_constructor(ctx(), s, idx));
+            if (id() == f.id())
+                break;
+        }
+        assert(idx < n);
+        n = arity();
+        func_decl_vector as(ctx());
+        for (unsigned i = 0; i < n; ++i) 
+            as.push_back(func_decl(ctx(), Z3_get_datatype_sort_constructor_accessor(ctx(), s, idx, i)));
+        return as;
+    }
+
 
     inline expr expr::substitute(expr_vector const& src, expr_vector const& dst) {
         assert(src.size() == dst.size());

src/api/dotnet/CMakeLists.txt

@@ -18,8 +18,6 @@ add_custom_command(OUTPUT "${Z3_DOTNET_NATIVE_FILE}"
     ${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 ${Z3_DOTNET_NATIVE_FILE}"
   ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG}
 )

src/api/ml/z3.ml

@@ -203,7 +203,7 @@ end = struct
   let equal = (=)
 
   (* The standard comparison uses the custom operations of the C layer *)
-  let compare = Pervasives.compare
+  let compare = Stdlib.compare
 
   let translate (x:ast) (to_ctx:context) =
     if gc x = to_ctx then

src/api/python/CMakeLists.txt

@@ -99,7 +99,7 @@ if (Z3_INSTALL_PYTHON_BINDINGS)
     message(STATUS "CMAKE_INSTALL_PYTHON_PKG_DIR not set. Trying to guess")
     execute_process(
       COMMAND "${PYTHON_EXECUTABLE}" "-c"
-        "import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())"
+        "import sysconfig; print(sysconfig.get_path('purelib'))"
       RESULT_VARIABLE exit_code
       OUTPUT_VARIABLE CMAKE_INSTALL_PYTHON_PKG_DIR
       OUTPUT_STRIP_TRAILING_WHITESPACE

src/api/python/z3/z3.py

@@ -8789,6 +8789,10 @@ def Product(*args):
         _args, sz = _to_ast_array(args)
         return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
 
+def Abs(arg):
+    """Create the absolute value of an arithmetic expression"""
+    return If(arg > 0, arg, -arg)
+    
 
 def AtMost(*args):
     """Create an at-most Pseudo-Boolean k constraint.

src/api/z3_api.h

@@ -1516,7 +1516,7 @@ extern "C" {
 
        def_API('Z3_global_param_get', BOOL, (_in(STRING), _out(STRING)))
     */
-    Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
+    Z3_bool Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value);
 
     /**@}*/
 
@@ -4325,7 +4325,7 @@ extern "C" {
 
         def_API('Z3_get_finite_domain_sort_size', BOOL, (_in(CONTEXT), _in(SORT), _out(UINT64)))
     */
-    Z3_bool_opt Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
+    Z3_bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t* r);
 
     /**
        \brief Return the domain of the given array sort.
@@ -5264,7 +5264,7 @@ extern "C" {
 
        def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST)))
     */
-    Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
+    Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, bool model_completion, Z3_ast * v);
 
     /**
        \brief Return the interpretation (i.e., assignment) of constant \c a in the model \c m.

src/api/z3_macros.h

@@ -4,9 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#ifndef Z3_bool_opt
-#define Z3_bool_opt Z3_bool
-#endif
 
 #ifndef Z3_API
 # ifdef __GNUC__

src/ast/arith_decl_plugin.h

@@ -273,6 +273,17 @@ public:
     bool is_rem0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_REM0); }
     bool is_mod0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_MOD0); }
     bool is_power0(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER0); }
+    bool is_power(func_decl const * n) const { return is_decl_of(n, arith_family_id, OP_POWER); }
+    bool is_add(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_ADD); }
+    bool is_mul(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MUL); }
+    bool is_sub(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_SUB); }
+    bool is_uminus(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_UMINUS); }
+    bool is_div(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_DIV); }
+    bool is_rem(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_REM); }
+    bool is_mod(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_MOD); }
+    bool is_to_real(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_REAL); }
+    bool is_to_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_TO_INT); }
+    bool is_is_int(func_decl const* f) const { return is_decl_of(f, arith_family_id, OP_IS_INT); }
 
     bool is_add(expr const * n) const { return is_app_of(n, arith_family_id, OP_ADD); }
     bool is_sub(expr const * n) const { return is_app_of(n, arith_family_id, OP_SUB); }

src/ast/array_decl_plugin.h

@@ -150,6 +150,10 @@ public:
     bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
     bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); }
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
+    bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_SET_UNION); }
+    bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_SET_INTERSECT); }
+    bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_SET_DIFFERENCE); }
+    bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
     bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
     bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
@@ -158,11 +162,14 @@ public:
     bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
     bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
+    bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); }
+    bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); }
     bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
     bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
     bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
     bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
     bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
+    bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
@@ -172,6 +179,8 @@ public:
     bool is_const(expr* e, expr*& v) const;
 
     bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
+
+    MATCH_BINARY(is_subset);
 };
 
 class array_util : public array_recognizers {

src/ast/ast_util.cpp

@@ -264,8 +264,12 @@ void flatten_and(expr_ref_vector& result) {
     expr_fast_mark1 seen;
     for (unsigned i = 0; i < result.size(); ++i) {
         expr* e = result.get(i);
-        if (seen.is_marked(e))
+        if (seen.is_marked(e)) {
+            result[i] = result.back();
+            result.pop_back();
+            --i;
             continue;
+        }
         seen.mark(e);
         pin.push_back(e);
         if (m.is_and(e)) {
@@ -330,8 +334,12 @@ void flatten_or(expr_ref_vector& result) {
     expr_fast_mark1 seen;
     for (unsigned i = 0; i < result.size(); ++i) {
         expr* e = result.get(i);
-        if (seen.is_marked(e))
+        if (seen.is_marked(e)) {
+            result[i] = result.back();
+            result.pop_back();
+            --i;
             continue;
+        }
         seen.mark(e);
         pin.push_back(e);
         if (m.is_or(e)) {

src/ast/euf/euf_egraph.cpp

@@ -25,6 +25,8 @@ namespace euf {
 
     enode* egraph::mk_enode(expr* f, unsigned generation, unsigned num_args, enode * const* args) {
         enode* n = enode::mk(m_region, f, generation, num_args, args);
+        if (m_default_relevant)
+            n->set_relevant(true);
         m_nodes.push_back(n);
         m_exprs.push_back(f);
         if (is_app(f) && num_args > 0) {
@@ -187,10 +189,10 @@ namespace euf {
             add_th_diseq(id, v1, v2, n->get_expr());
             return;
         }
-        for (auto p : euf::enode_th_vars(r1)) {
+        for (auto const& p : euf::enode_th_vars(r1)) {
             if (!th_propagates_diseqs(p.get_id()))
                 continue;
-            for (auto q : euf::enode_th_vars(r2))
+            for (auto const& q : euf::enode_th_vars(r2))
                 if (p.get_id() == q.get_id()) 
                     add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n->get_expr());
         }
@@ -269,6 +271,13 @@ namespace euf {
         }
     }
 
+    void egraph::set_relevant(enode* n) {
+        if (n->is_relevant())
+            return;
+        n->set_relevant(true);
+        m_updates.push_back(update_record(n, update_record::set_relevant()));
+    }
+
     void egraph::toggle_merge_enabled(enode* n, bool backtracking) {
        bool enable_merge = !n->merge_enabled();
        n->set_merge_enabled(enable_merge);         
@@ -380,6 +389,10 @@ namespace euf {
             case update_record::tag_t::is_lbl_set:
                 p.r1->m_lbls.set(p.m_lbls);
                 break;
+            case update_record::tag_t::is_set_relevant:
+                SASSERT(p.r1->is_relevant());
+                p.r1->set_relevant(false);
+                break;
             case update_record::tag_t::is_update_children:
                 for (unsigned i = 0; i < p.r1->num_args(); ++i) {
                     SASSERT(p.r1->m_args[i]->get_root()->m_parents.back() == p.r1);
@@ -446,8 +459,8 @@ namespace euf {
         r2->inc_class_size(r1->class_size());   
         merge_th_eq(r1, r2);
         reinsert_parents(r1, r2);
-        if (m_on_merge)
+        for (auto& cb : m_on_merge)
-            m_on_merge(r2, r1);
+            cb(r2, r1);
     }
 
     void egraph::remove_parents(enode* r1, enode* r2) {
@@ -493,7 +506,7 @@ namespace euf {
 
     void egraph::merge_th_eq(enode* n, enode* root) {
         SASSERT(n != root);
-        for (auto iv : enode_th_vars(n)) {
+        for (auto const& iv : enode_th_vars(n)) {
             theory_id id = iv.get_id();
             theory_var v = root->get_th_var(id);
             if (v == null_theory_var) {                
@@ -754,6 +767,8 @@ namespace euf {
     }
 
     std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
+        if (!n->is_relevant())
+            out << "n";
         out << "#" << n->get_expr_id() << " := ";
         expr* f = n->get_expr();
         if (is_app(f))
@@ -770,11 +785,18 @@ namespace euf {
                 out << " " << p->get_expr_id();
             out << "] ";
         }
-        if (n->value() != l_undef) 
+        auto value_of = [&]() {
-            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
+            switch (n->value()) {
+            case l_true: return "T";
+            case l_false: return "F";
+            default: return "?";
+            }
+        };
+        if (n->bool_var() != sat::null_bool_var) 
+            out << "[b" << n->bool_var() << " := " << value_of() << (n->merge_tf() ? "" : " no merge") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
-            for (auto v : enode_th_vars(n))
+            for (auto const& v : enode_th_vars(n))
                 out << " " << v.get_id() << ":" << v.get_var();
             out << "] ";
         }

src/ast/euf/euf_egraph.h

@@ -32,6 +32,7 @@ Notes:
 #include "ast/euf/euf_enode.h"
 #include "ast/euf/euf_etable.h"
 #include "ast/ast_ll_pp.h"
+#include <vector>
 
 namespace euf {
 
@@ -105,10 +106,11 @@ namespace euf {
             struct lbl_hash {};
             struct lbl_set {};
             struct update_children {};
+            struct set_relevant {};
             enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, is_update_children,
                     is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
                     is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead, 
-                    is_inconsistent, is_value_assignment, is_lbl_set };
+                    is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant };
             tag_t  tag;
             enode* r1;
             enode* n1;
@@ -151,6 +153,8 @@ namespace euf {
                 tag(tag_t::is_lbl_set), r1(n), n1(nullptr), m_lbls(n->m_lbls.get()) {}    
             update_record(enode* n, update_children) :
                 tag(tag_t::is_update_children), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {}
+            update_record(enode* n, set_relevant) :
+                tag(tag_t::is_set_relevant), r1(n), n1(nullptr), r2_num_parents(UINT_MAX) {}
         };
         ast_manager&           m;
         svector<to_merge>      m_to_merge;
@@ -181,7 +185,8 @@ namespace euf {
         enode_vector           m_todo;
         stats                  m_stats;
         bool                   m_uses_congruence = false;
-        std::function<void(enode*,enode*)>     m_on_merge;
+        bool                   m_default_relevant = true;
+        std::vector<std::function<void(enode*,enode*)>>     m_on_merge;
         std::function<void(enode*)>            m_on_make;
         std::function<void(expr*,expr*,expr*)> m_used_eq;
         std::function<void(app*,app*)>         m_used_cc;  
@@ -292,8 +297,10 @@ namespace euf {
         void set_merge_enabled(enode* n, bool enable_merge);
         void set_value(enode* n, lbool value);
         void set_bool_var(enode* n, unsigned v) { n->set_bool_var(v); }
+        void set_relevant(enode* n);
+        void set_default_relevant(bool b) { m_default_relevant = b; }
 
-        void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge = on_merge; }
+        void set_on_merge(std::function<void(enode* root,enode* other)>& on_merge) { m_on_merge.push_back(on_merge); }
         void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make = on_make; }
         void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) { m_used_eq = used_eq; }
         void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc = used_cc; }

src/ast/euf/euf_enode.h

@@ -49,6 +49,7 @@ namespace euf {
         bool          m_interpreted = false;
         bool          m_merge_enabled = true; 
         bool          m_is_equality = false;    // Does the expression represent an equality
+        bool          m_is_relevant = false;
         lbool         m_value = l_undef;        // Assignment by SAT solver for Boolean node
         sat::bool_var m_bool_var = sat::null_bool_var;    // SAT solver variable associated with Boolean node
         unsigned      m_class_size = 1;         // Size of the equivalence class if the enode is the root.
@@ -145,6 +146,8 @@ namespace euf {
         unsigned num_parents() const { return m_parents.size(); }
         bool interpreted() const { return m_interpreted; }
         bool is_equality() const { return m_is_equality; }
+        bool is_relevant() const { return m_is_relevant; }
+        void set_relevant(bool b) { m_is_relevant = b; }
         lbool value() const { return m_value;  }
         bool value_conflict() const { return value() != l_undef && get_root()->value() != l_undef && value() != get_root()->value(); }
         sat::bool_var bool_var() const { return m_bool_var; }

src/ast/rewriter/seq_axioms.cpp

@@ -21,8 +21,11 @@ Revision History:
 
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/recfun_decl_plugin.h"
+#include "ast/rewriter/recfun_replace.h"
 #include "ast/rewriter/seq_axioms.h"
 
+
 namespace seq {
 
     axioms::axioms(th_rewriter& r):
@@ -1052,6 +1055,79 @@ namespace seq {
         NOT_IMPLEMENTED_YET();
     }
 
+    // A basic strategy for supporting replace_all and other
+    // similar functions is to use recursive relations.
+    // Then the features for recursive functions that allow expanding definitions
+    // using iterative deepening can be re-used.
+    //
+    // create recursive relation 'ra' with properties:
+    // ra(i, j, s, p, t, r) <- len(s) = i && len(r) = j
+    // ra(i, j, s, p, t, r) <- len(s) > i = 0 && p = "" && r = t + s
+    // ra(i, j, s, p, t, r) <- len(s) > i && p != "" && s = extract(s, 0, i) + p + extract(s, i + len(p), len(s)) && r = extract(r, 0, i) + t + extract(r, i + len(p), len(r)) && ra(i + len(p), j + len(t), s, p, t, r)
+    // ra(i, s, p, t, r) <- ~prefix(p, extract(s, i, len(s)) && at(s,i) = at(r,j) && ra(i + 1, j + 1, s, p, t, r)
+    // which amounts to:
+    //
+    //
+    // Then assert
+    // ra(s, p, t, replace_all(s, p, t))
+    //
+    void axioms::replace_all_axiom(expr* r) {
+        expr* s = nullptr, *p = nullptr, *t = nullptr;
+        VERIFY(seq.str.is_replace_all(r, s, p, t)); 
+        recfun::util rec(m);
+        recfun::decl::plugin& plugin = rec.get_plugin();
+        recfun_replace replace(m);
+        sort* srt = s->get_sort();
+        sort* domain[4] = { srt, srt, srt, srt };
+        auto d = plugin.ensure_def(symbol("ra"), 4, domain, m.mk_bool_sort(), true);
+        func_decl* ra = d.get_def()->get_decl();
+        sort* isrt = a.mk_int();
+        var_ref vi(m.mk_var(5, isrt), m);
+        var_ref vj(m.mk_var(4, isrt), m);
+        var_ref vs(m.mk_var(3, srt), m);
+        var_ref vp(m.mk_var(2, srt), m);
+        var_ref vt(m.mk_var(1, srt), m);
+        var_ref vr(m.mk_var(0, srt), m);
+        var* vars[6] = { vi, vj, vs, vp, vt, vr };
+        expr_ref len_s(seq.str.mk_length(vs), m);
+        expr_ref len_r(seq.str.mk_length(vr), m);
+        expr_ref test1(m.mk_eq(len_s, vi), m);
+        expr_ref branch1(m.mk_eq(len_r, vj), m);
+        expr_ref test2(m.mk_and(a.mk_gt(len_s, vi), m.mk_eq(vi, a.mk_int(0)), seq.str.mk_is_empty(vp)), m);
+        expr_ref branch2(m.mk_eq(vr, seq.str.mk_concat(vt, vs)), m);
+        NOT_IMPLEMENTED_YET();
+#if 0
+        expr_ref test3(, m);
+        expr_ref s1(m_sk.mk_prefix_inv(vp, vs), m);
+        expr_ref r1(m_sk.mk_prefix_inv(vp, vr), m);
+        expr* args1[4] = { s1, vp, vt, r1 };
+        expr_ref branch3(m.mk_and(m.mk_eq(seq.str.mk_concat(vp, s1), vs), 
+                                  m.mk_eq(seq.str.mk_concat(vr, r1), vr),
+                                  m.mk_app(ra, 4, args1)
+                                  ), m);
+        expr_ref s0(m), r0(m);
+        m_sk.decompose(vs, s0, s1);
+        m_sk.decompose(vr, r0, r1);
+        expr* args2[4] = { s1, vp, vt, r1 };
+        expr_ref branch4(m.mk_and(m.mk_eq(vs, seq.str.mk_concat(s0, s1)), 
+                                  m.mk_eq(vr, seq.str.mk_concat(s0, r1)),
+                                  m.mk_app(ra, 4, args2)), m);
+        // s = [s0] + s' && r = [s0] + r' && ra(s', p, t, r')
+
+        expr_ref body(m.mk_ite(test1, branch1, m.mk_ite(test2, branch2, m.mk_ite(test3, branch3, branch4))), m);        
+        plugin.set_definition(replace, d, true, 4, vars, body);
+        expr* args3[4] = { s, p, t, r };
+        expr_ref lit(m.mk_app(ra, 4, args3), m);
+        add_clause(lit);
+#endif
+    }
+
+    void axioms::replace_re_all_axiom(expr* e) {
+        expr* s = nullptr, *p = nullptr, *t = nullptr;
+        VERIFY(seq.str.is_replace_re_all(e, s, p, t)); 
+        NOT_IMPLEMENTED_YET();
+    }
+
 
 
     /**

src/ast/rewriter/seq_axioms.h

@@ -107,6 +107,8 @@ namespace seq {
         void length_axiom(expr* n);
         void unroll_not_contains(expr* e);
         void replace_re_axiom(expr* e);
+        void replace_all_axiom(expr* e);
+        void replace_re_all_axiom(expr* e);
 
         expr_ref length_limit(expr* s, unsigned k);
         expr_ref is_digit(expr* ch);

src/ast/rewriter/seq_rewriter.cpp

@@ -3112,7 +3112,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
         else
             // D(e,r1)r2|(ite (r1nullable) (D(e,r2)) [])
             // observe that (mk_ite_simplify(true, D(e,r2), []) = D(e,r2)
-            result = mk_regex_union_normalize(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
+            result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
     }
     else if (m().is_ite(r, c, r1, r2)) {
         c1 = simplify_path(e, m().mk_and(c, path));
@@ -3171,7 +3171,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
             result = re().mk_ite_simplify(range, epsilon(), nothing());
     }
     else if (re().is_union(r, r1, r2))
-        result = mk_regex_union_normalize(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));
+        result = mk_antimirov_deriv_union(mk_antimirov_deriv(e, r1, path), mk_antimirov_deriv(e, r2, path));
     else if (re().is_intersection(r, r1, r2))
         result = mk_antimirov_deriv_intersection(e, 
             mk_antimirov_deriv(e, r1, path),
@@ -3237,11 +3237,11 @@ expr_ref seq_rewriter::mk_antimirov_deriv_intersection(expr* e, expr* d1, expr*
         result = mk_antimirov_deriv_restrict(e, d2, path);
     else if (re().is_union(d1, a, b))
         // distribute intersection over the union in d1
-        result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, a, d2, path),
+        result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, a, d2, path),
             mk_antimirov_deriv_intersection(e, b, d2, path));
     else if (re().is_union(d2, a, b))
         // distribute intersection over the union in d2
-        result = mk_regex_union_normalize(mk_antimirov_deriv_intersection(e, d1, a, path),
+        result = mk_antimirov_deriv_union(mk_antimirov_deriv_intersection(e, d1, a, path),
             mk_antimirov_deriv_intersection(e, d1, b, path));
     else
         result = mk_regex_inter_normalize(d1, d2);
@@ -3256,7 +3256,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_concat(expr* d, expr* r) {
     if (m().is_ite(d, c, t, e))
         result = m().mk_ite(c, mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
     else if (re().is_union(d, t, e))
-        result = mk_regex_union_normalize(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
+        result = mk_antimirov_deriv_union(mk_antimirov_deriv_concat(t, r), mk_antimirov_deriv_concat(e, r));
     else
         result = mk_re_append(d, r);
     return result;
@@ -3284,7 +3284,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) {
     else if (re().is_union(d, t, e))
         result = mk_antimirov_deriv_intersection(elem, mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e), m().mk_true());
     else if (re().is_intersection(d, t, e))
-        result = mk_regex_union_normalize(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
+        result = mk_antimirov_deriv_union(mk_antimirov_deriv_negate(elem, t), mk_antimirov_deriv_negate(elem, e));
     else if (re().is_complement(d, t))
         result = t;
     else
@@ -3292,6 +3292,20 @@ expr_ref seq_rewriter::mk_antimirov_deriv_negate(expr* elem, expr* d) {
     return result;
 }
 
+expr_ref seq_rewriter::mk_antimirov_deriv_union(expr* d1, expr* d2) {
+    sort* seq_sort = nullptr, * ele_sort = nullptr;
+    VERIFY(m_util.is_re(d1, seq_sort));
+    VERIFY(m_util.is_seq(seq_sort, ele_sort));
+    expr_ref result(m());
+    expr* c1, * t1, * e1, * c2, * t2, * e2;
+    if (m().is_ite(d1, c1, t1, e1) && m().is_ite(d2, c2, t2, e2)  && c1 == c2)
+        // eliminate duplicate branching on exactly the same condition
+        result = m().mk_ite(c1, mk_antimirov_deriv_union(t1, t2), mk_antimirov_deriv_union(e1, e2));
+    else
+        result = mk_regex_union_normalize(d1, d2);
+    return result;
+}
+
 // restrict the guards of all conditionals id d and simplify the resulting derivative
 // restrict(if(c, a, b), cond) = if(c, restrict(a, cond & c), restrict(b, cond & ~c))
 // restrict(a U b, cond) = restrict(a, cond) U restrict(b, cond)
@@ -3320,7 +3334,7 @@ expr_ref seq_rewriter::mk_antimirov_deriv_restrict(expr* e, expr* d, expr* cond)
     else if (re().is_union(d, a, b)) {
         expr_ref a1(mk_antimirov_deriv_restrict(e, a, cond), m());
         expr_ref b1(mk_antimirov_deriv_restrict(e, b, cond), m());
-        result = mk_regex_union_normalize(a1, b1);
+        result = mk_antimirov_deriv_union(a1, b1);
     }
     return result;
 }
@@ -3331,7 +3345,7 @@ expr_ref seq_rewriter::mk_regex_union_normalize(expr* r1, expr* r2) {
     SASSERT(m_util.is_re(r2));
     expr_ref result(m());
     std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_union(t, a, b); };
-    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_union(r1, r2); };
+    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r2 : (is_subset(r2, r1) ? r1 : re().mk_union(r1, r2))); };
     if (r1 == r2 || re().is_empty(r2) || re().is_full_seq(r1))
         result = r1;
     else if (re().is_empty(r1) || re().is_full_seq(r2))
@@ -3353,7 +3367,7 @@ expr_ref seq_rewriter::mk_regex_inter_normalize(expr* r1, expr* r2) {
     if (re().is_epsilon(r2))
         std::swap(r1, r2);
     std::function<bool(expr*, expr*&, expr*&)> test = [&](expr* t, expr*& a, expr*& b) { return re().is_intersection(t, a, b); };
-    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return re().mk_inter(r1, r2); };
+    std::function<expr* (expr*, expr*)> compose = [&](expr* r1, expr* r2) { return (is_subset(r1, r2) ? r1 : (is_subset(r2, r1) ? r2 : re().mk_inter(r1, r2))); };
     if (r1 == r2 || re().is_empty(r1) || re().is_full_seq(r2))
         result = r1;
     else if (re().is_empty(r2) || re().is_full_seq(r1))
@@ -4586,6 +4600,7 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
     // return false;
     expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
     expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
+    unsigned la, ua, lb, ub;
     if (re().is_complement(r1, ra1) && 
         re().is_complement(r2, rb1)) {
         return is_subset(rb1, ra1);
@@ -4598,6 +4613,8 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
             return true;
         if (re().is_full_seq(r2))
             return true;
+        if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
+            return true;
         if (is_concat(r1, ra1, ra2, ra3) &&
             is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
             r1 = ra3;
@@ -4609,6 +4626,20 @@ bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
             r1 = ra2;
             continue;
         }
+        // r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub
+        if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) &&
+            re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) &&
+            ra3 == rb3 && lb <= la && ua <= ub) {
+            r1 = ra2;
+            r2 = rb2;
+            continue;
+        }
+        // ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub
+        if (re().is_loop(r1, ra3, la, ua) &&
+            re().is_loop(r2, rb3, lb, ub) &&
+            ra3 == rb3 && lb <= la && ua <= ub) {
+            return true;
+        }
         return false;
     }
 }

src/ast/rewriter/seq_rewriter.h

@@ -217,6 +217,7 @@ class seq_rewriter {
     expr_ref mk_antimirov_deriv_intersection(expr* elem, expr* d1, expr* d2, expr* path);
     expr_ref mk_antimirov_deriv_concat(expr* d, expr* r);
     expr_ref mk_antimirov_deriv_negate(expr* elem, expr* d);
+    expr_ref mk_antimirov_deriv_union(expr* d1, expr* d2);
     expr_ref mk_antimirov_deriv_restrict(expr* elem, expr* d1, expr* cond);
     expr_ref mk_regex_reverse(expr* r);
     expr_ref mk_regex_concat(expr* r1, expr* r2);

src/ast/rewriter/th_rewriter.cpp

@@ -627,7 +627,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 count_down_subterm_references(result, reference_map);
 
                 // Any term that was newly introduced by the rewrite step is only referenced within / reachable from the result term.
-                for (auto kv : reference_map) {
+                for (auto const& kv : reference_map) {
                     if (kv.m_value == 0) {
                         m().trace_stream() << "[attach-enode] #" << kv.m_key->get_id() << " 0\n";
                     }
@@ -691,7 +691,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return;
         if (m_new_subst) {
             m_rep.reset();
-            for (auto kv : m_subst->sub())
+            for (auto const& kv : m_subst->sub())
                 m_rep.insert(kv.m_key, kv.m_value);
             m_new_subst = false;
         }
@@ -859,8 +859,8 @@ ast_manager & th_rewriter::m() const {
 }
 
 void th_rewriter::updt_params(params_ref const & p) {
-    m_params = p;
+    m_params.append(p);
-    m_imp->cfg().updt_params(p);
+    m_imp->cfg().updt_params(m_params);
 }
 
 void th_rewriter::get_param_descrs(param_descrs & r) {

src/cmd_context/basic_cmds.cpp

@@ -301,10 +301,23 @@ UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr
     ctx.regular_stream() << std::endl;
 });
 
+static std::string escape_string(char const* arg) {
+    std::string result;
+    while (*arg) {
+        auto ch = *arg++;
+        if (ch == '"')
+            result.push_back(ch);
+        result.push_back(ch);
+    }
+    return result;
+}
+
 UNARY_CMD(echo_cmd, "echo", "<string>", "display the given string", CPK_STRING, char const *,
           bool smt2c = ctx.params().m_smtlib2_compliant;
-    ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;);
+          if (smt2c) 
-
+              ctx.regular_stream() << "\"" << escape_string(arg) << "\"" << std::endl;
+          else
+              ctx.regular_stream() << arg << std::endl;);
 
 class set_get_option_cmd : public cmd {
 protected:

src/cmd_context/cmd_context.cpp

@@ -2107,6 +2107,21 @@ void cmd_context::analyze_failure(expr_mark& seen, model_evaluator& ev, expr* a,
                << (expected_value?"true":"false") << "\n";);                
 
     IF_VERBOSE(11, display_detailed_analysis(verbose_stream(), ev, a));
+
+    if (m().is_iff(a)) {
+        ptr_vector<expr> todo;
+        todo.push_back(a);
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            e = todo[i];
+            if (m().is_and(e) || m().is_or(e) || m().is_iff(e) || m().is_implies(e) || m().is_not(e)) 
+                for (expr* arg : *to_app(e))
+                    todo.push_back(arg);
+            else
+                IF_VERBOSE(10, verbose_stream() << "#" << e->get_id() << " " << mk_bounded_pp(e, m()) << " " << (ev.is_true(e)?"true":"false") << "\n");
+        }
+        return;
+    }
+
 }
 
 void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e) {

src/cmd_context/extra_cmds/dbg_cmds.cpp

@@ -199,12 +199,12 @@ void tst_params(cmd_context & ctx) {
     params_ref p1;
     params_ref p2;
     p1.set_uint("val", 100);
-    p2 = p1;
+    p2.append(p1);
     SASSERT(p2.get_uint("val", 0) == 100);
     p2.set_uint("val", 200);
     SASSERT(p2.get_uint("val", 0) == 200);
     SASSERT(p1.get_uint("val", 0) == 100);
-    p2 = p1;
+    p2.append(p1);
     SASSERT(p2.get_uint("val", 0) == 100);
     SASSERT(p1.get_uint("val", 0) == 100);
     ctx.regular_stream() << "worked" << std::endl;

src/math/subpaving/tactic/subpaving_tactic.cpp

@@ -227,8 +227,8 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
-        m_imp->updt_params(p);
+        m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {

src/model/model_core.cpp

@@ -111,6 +111,7 @@ void model_core::unregister_decl(func_decl * d) {
         m_interp[m_const_decls.back()].first = v.first;
         m_const_decls.pop_back();
         m_interp.remove(d);
+        m_decls.erase(d);
         m.dec_ref(k);
         m.dec_ref(v.second);
         return;
@@ -122,6 +123,7 @@ void model_core::unregister_decl(func_decl * d) {
         auto v = ef->get_data().m_value;
         m_finterp.remove(d);
         m_func_decls.erase(d);
+        m_decls.erase(d);
         m.dec_ref(k);
         dealloc(v);
     }

src/muz/fp/horn_tactic.cpp

@@ -395,8 +395,8 @@ public:
     char const* name() const override { return "horn"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
-        m_imp->updt_params(p);
+        m_imp->updt_params(m_params);
     }
 
 

src/nlsat/tactic/nlsat_tactic.cpp

@@ -55,8 +55,8 @@ class nlsat_tactic : public tactic {
         }
         
         void updt_params(params_ref const & p) {
-            m_params = p;
+            m_params.append(p);
-            m_solver.updt_params(p);
+            m_solver.updt_params(m_params);
         }
         
         bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) {
@@ -226,7 +226,7 @@ public:
     char const* name() const override { return "nlsat"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
     }
 
     void collect_param_descrs(param_descrs & r) override {

src/opt/opt_solver.cpp

@@ -259,6 +259,12 @@ namespace opt {
         if (!m_models[i]) 
             m_models.set(i, m_last_model.get());
 
+        if (val > m_objective_values[i])
+            m_objective_values[i] = val;    
+
+        if (!m_last_model)
+            return true;
+
         //
         // retrieve value of objective from current model and update 
         // current optimal.

src/opt/optsmt.cpp

@@ -49,14 +49,14 @@ namespace opt {
                 dst[i] = src[i];
                 m_models.set(i, m_s->get_model_idx(i));
                 m_s->get_labels(m_labels);
-                m_lower_fmls[i] = fmls[i].get();
+                m_lower_fmls[i] = fmls.get(i);
                 if (dst[i].is_pos() && !dst[i].is_finite()) { // review: likely done already.
                     m_lower_fmls[i] = m.mk_false();
                     fmls[i] = m.mk_false();
                 }
             }
-            else if (src[i] < dst[i] && !m.is_true(m_lower_fmls[i].get())) {
+            else if (src[i] < dst[i] && !m.is_true(m_lower_fmls.get(i))) {
-                fmls[i] = m_lower_fmls[i].get();                
+                fmls[i] = m_lower_fmls.get(i);                
             }
         }
     }
@@ -202,6 +202,9 @@ namespace opt {
         for (unsigned i = 0; i < obj_index; ++i) 
             commit_assignment(i);
 
+//        m_s->maximize_objective(obj_index, bound);
+//        m_s->assert_expr(bound);
+
         unsigned steps = 0;
         unsigned step_incs = 0;
         rational delta_per_step(1);
@@ -282,7 +285,7 @@ namespace opt {
     bool optsmt::can_increment_delta(vector<inf_eps> const& lower, unsigned i) {
         arith_util arith(m);
         inf_eps max_delta;
-        if (m_lower[i] < m_upper[i] && arith.is_int(m_objs[i].get())) {
+        if (m_lower[i] < m_upper[i] && arith.is_int(m_objs.get(i))) {
             inf_eps delta = m_lower[i] - lower[i];  
             if (m_lower[i].is_finite() && delta > max_delta) {
                 return true;
@@ -435,7 +438,7 @@ namespace opt {
         bool progress = false;
         for (unsigned i = 0; i < m_lower.size() && m.inc(); ++i) {
             if (m_lower[i] <= mid[i] && mid[i] <= m_upper[i] && m_lower[i] < m_upper[i]) {
-                th.enable_record_conflict(bounds[i].get());
+                th.enable_record_conflict(bounds.get(i));
                 lbool is_sat = m_s->check_sat(1, bounds.data() + i);
                 switch(is_sat) {
                 case l_true:
@@ -484,10 +487,10 @@ namespace opt {
         }
 
         for (unsigned i = 0; i < m_objs.size(); ++i) {
-            smt::theory_var v = solver.add_objective(m_objs[i].get());
+            smt::theory_var v = solver.add_objective(m_objs.get(i));
             if (v == smt::null_theory_var) {
                 std::ostringstream out;
-                out << "Objective function '" << mk_pp(m_objs[i].get(), m) << "' is not supported";
+                out << "Objective function '" << mk_pp(m_objs.get(i), m) << "' is not supported";
                 throw default_exception(out.str());
             }
             m_vars.push_back(v);
@@ -547,7 +550,7 @@ namespace opt {
     // force lower_bound(i) <= objective_value(i)    
     void optsmt::commit_assignment(unsigned i) {
         inf_eps lo = m_lower[i];
-        TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs[i].get(), m) << " to: " << lo << "\n";
+        TRACE("opt", tout << "set lower bound of " << mk_pp(m_objs.get(i), m) << " to: " << lo << "\n";
               tout << get_lower(i) << ":" << get_upper(i) << "\n";);    
         // Only assert bounds for bounded objectives
         if (lo.is_finite()) {

src/params/context_params.cpp

@@ -190,7 +190,8 @@ void context_params::get_solver_params(params_ref & p, bool & proofs_enabled, bo
     proofs_enabled     &= p.get_bool("proof", m_proof);
     models_enabled     &= p.get_bool("model", m_model);
     unsat_core_enabled = m_unsat_core || p.get_bool("unsat_core", false);
-    p = merge_default_params(p);
+    if (!m_auto_config && !p.contains("auto_config"))
+        p.set_bool("auto_config", false);
 }
 
 

src/qe/mbp/mbp_arith.cpp

@@ -249,8 +249,8 @@ namespace mbp {
         bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) {
             app_ref_vector vs(m);
             vs.push_back(v);
-            project(model, vs, lits, false);
+            vector<def> defs;
-            return vs.empty();
+            return project(model, vs, lits, defs, false) && vs.empty();            
         }
 
         typedef opt::model_based_opt::var var;
@@ -265,12 +265,12 @@ namespace mbp {
             return t;
         }
 
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, bool compute_def) {
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& fmls, vector<def>& result, bool compute_def) {
             bool has_arith = false;
             for (expr* v : vars) 
                 has_arith |= is_arith(v);            
             if (!has_arith) 
-                return vector<def>();            
+                return true;            
             model_evaluator eval(model);
             TRACE("qe", tout << model;);
             eval.set_model_completion(true);
@@ -294,7 +294,7 @@ namespace mbp {
             }
             fmls.shrink(j);
             TRACE("qe", tout << "formulas\n" << fmls << "\n";
-		                for (auto [e, id] : tids)
+		                for (auto const& [e, id] : tids)
 		                    tout << mk_pp(e, m) << " -> " << id << "\n";);
 
             // fmls holds residue,
@@ -312,7 +312,7 @@ namespace mbp {
                     rational r;
                     expr_ref val = eval(v);
                     if (!m.inc())
-                        return vector<def>();
+                        return false;
                     if (!a.is_numeral(val, r))
                         throw default_exception("evaluation did not produce a numeral");
                     TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
@@ -326,17 +326,15 @@ namespace mbp {
                 if (is_arith(e) && !var_mark.is_marked(e)) 
                     mark_rec(fmls_mark, e);                
             }
-
             if (m_check_purified) {
                 for (expr* fml : fmls) 
                     mark_rec(fmls_mark, fml);                
                 for (auto& kv : tids) {
                     expr* e = kv.m_key;
-                    if (!var_mark.is_marked(e)) {
+                    if (!var_mark.is_marked(e)) 
                         mark_rec(fmls_mark, e);                    
                 }
             }
-            }
 
             ptr_vector<expr> index2expr;
             for (auto& kv : tids) 
@@ -364,16 +362,18 @@ namespace mbp {
                   for (auto const& d : defs) tout << "def: " << d << "\n";
                   tout << fmls << "\n";);
             
-            vector<def> result;
             if (compute_def) 
                 optdefs2mbpdef(defs, index2expr, real_vars, result);     
-            if (m_apply_projection)
+            if (m_apply_projection && !apply_projection(eval, result, fmls))
-                apply_projection(result, fmls);
+                return false;
+
             TRACE("qe",
-                for (auto [v, t] : result)
+                for (auto const& [v, t] : result)
                     tout << v << " := " << t << "\n";
+                for (auto* f : fmls)
+                    tout << mk_pp(f, m) << " := " << eval(f) << "\n";
                 tout << "fmls:" << fmls << "\n";);
-            return result;
+            return true;
         }        
 
         void optdefs2mbpdef(vector<opt::model_based_opt::def> const& defs, ptr_vector<expr> const& index2expr, unsigned_vector const& real_vars, vector<def>& result) {
@@ -548,10 +548,11 @@ namespace mbp {
             }
         }
 
-        void apply_projection(vector<def>& defs, expr_ref_vector& fmls) {
+        bool apply_projection(model_evaluator& eval, vector<def> const& defs, expr_ref_vector& fmls) {
             if (fmls.empty() || defs.empty())
-                return;
+                return true;
             expr_safe_replace subst(m);
+            expr_ref_vector fmls_tmp(m);
             expr_ref tmp(m);
             for (unsigned i = defs.size(); i-- > 0; ) {
                 auto const& d = defs[i];
@@ -561,8 +562,11 @@ namespace mbp {
             unsigned j = 0;
             for (expr* fml : fmls) {
                 subst(fml, tmp);
+                if (m.is_false(eval(tmp)))
+                    return false;
                 fmls[j++] = tmp;
             }
+            return true;
         }
 
     };
@@ -579,12 +583,13 @@ namespace mbp {
         return (*m_imp)(model, var, vars, lits);
     }
 
-    void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
-        m_imp->project(model, vars, lits, false);
+        vector<def> defs;
+        return m_imp->project(model, vars, lits, defs, false);
     }
 
-    vector<def> arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return m_imp->project(model, vars, lits, true);
+        return m_imp->project(model, vars, lits, defs, true);
     }
 
     void arith_project_plugin::set_check_purified(bool check_purified) {

src/qe/mbp/mbp_arith.h

@@ -29,8 +29,8 @@ namespace mbp {
         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; }
         family_id get_family_id() override;
-        void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); }
 
         opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt);

src/qe/mbp/mbp_arrays.cpp

@@ -1624,8 +1624,8 @@ namespace mbp {
               );
     }
 
-    vector<def> array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool array_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return vector<def>();
+        return true;
     }
 
     void array_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {

src/qe/mbp/mbp_arrays.h

@@ -35,7 +35,7 @@ namespace mbp {
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects);
         family_id get_family_id() override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
 
     };

src/qe/mbp/mbp_datatypes.cpp

@@ -300,8 +300,8 @@ namespace mbp {
         return m_imp->solve(model, vars, lits);
     }
 
-    vector<def> datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) {
+    bool datatype_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) {
-        return vector<def>();
+        return true;
     }
 
     void datatype_project_plugin::saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) {

src/qe/mbp/mbp_datatypes.h

@@ -34,7 +34,7 @@ namespace mbp {
         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
         family_id get_family_id() override;
-        vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
+        bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) override;
         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
 
     };

src/qe/mbp/mbp_plugin.h

@@ -67,7 +67,7 @@ namespace mbp {
         virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }
         virtual family_id get_family_id() { return null_family_id; }
 
-        virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { };
+        virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; };
 
         /**
            \brief project vars modulo model, return set of definitions for eliminated variables.
@@ -76,7 +76,7 @@ namespace mbp {
            - returns set of definitions
              (TBD: in triangular form, the last definition can be substituted into definitions that come before)
         */
-        virtual vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return vector<def>(); }
+        virtual bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector<def>& defs) { return true; }
 
         /**
            \brief model based saturation. Saturates theory axioms to equi-satisfiable literals over EUF,

src/qe/qe_lite.cpp

@@ -2466,7 +2466,7 @@ public:
     }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
         // m_imp->updt_params(p);
     }
 

src/qe/qe_mbi.cpp

@@ -266,7 +266,10 @@ namespace qe {
     vector<mbp::def> uflia_mbi::arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits) {
         mbp::arith_project_plugin ap(m);
         ap.set_check_purified(false);
-        return ap.project(*mdl.get(), avars, lits);
+        vector<mbp::def> defs;
+        bool ok = ap.project(*mdl.get(), avars, lits, defs);
+        CTRACE("qe", !ok, tout << "projection failure ignored!!!!\n");
+        return defs;
     }
 
     mbi_result uflia_mbi::operator()(expr_ref_vector& lits, model_ref& mdl) {

src/qe/qe_tactic.cpp

@@ -103,8 +103,8 @@ public:
     char const* name() const override { return "qe"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
-        m_imp->updt_params(p);
+        m_imp->updt_params(m_params);
     }
 
    

src/sat/sat_solver.cpp

@@ -288,6 +288,7 @@ namespace sat {
             m_free_vars.pop_back();
             m_active_vars.push_back(v);
             reset_var(v, ext, dvar);
+            SASSERT(v < m_justification.size());
             return v;
         }
         m_active_vars.push_back(v);
@@ -3008,7 +3009,7 @@ namespace sat {
         svector<double> logits(vars.size(), 0.0);
         double itau = m_config.m_reorder_itau;
         double lse = 0;
-        double mid = m_rand.max_value()/2;
+        double mid = (double)(m_rand.max_value()/2);
         double max = 0;
         for (double& f : logits) {
             f = itau * (m_rand() - mid)/mid;
@@ -3508,7 +3509,6 @@ namespace sat {
         unsigned old_num_vars = m_vars_lim.pop(num_scopes);
         if (old_num_vars == m_active_vars.size())
             return;
-        unsigned free_vars_head = m_free_vars.size();
         unsigned sz = m_active_vars.size(), j = old_num_vars;
         unsigned new_lvl = m_scopes.size() - num_scopes;
 
@@ -3538,9 +3538,7 @@ namespace sat {
             }
             else {
                 set_eliminated(v, true);
-                if (!is_external(v) || true) {
+                m_vars_to_free.push_back(v);                                   
-                    m_free_vars.push_back(v);                   
-                }
             }
         }
         m_active_vars.shrink(j);
@@ -3550,8 +3548,7 @@ namespace sat {
                 IF_VERBOSE(0, verbose_stream() << "cleanup: " << lit << " " << w.is_binary_clause() << "\n");
             }
         };
-        for (unsigned i = m_free_vars.size(); i-- > free_vars_head; ) {
+        for (bool_var v : m_vars_to_free) {
-            bool_var v = m_free_vars[i];
             cleanup_watch(literal(v, false));
             cleanup_watch(literal(v, true));
             
@@ -3560,7 +3557,7 @@ namespace sat {
             tout << "clauses to reinit: " << (m_clauses_to_reinit.size() - old_sz) << "\n";
             tout << "new level:         " << new_lvl << "\n";
             tout << "vars to reinit:    " << m_vars_to_reinit << "\n";
-            tout << "free vars:         " << bool_var_vector(m_free_vars.size() - free_vars_head, m_free_vars.data() + free_vars_head) << "\n";
+            tout << "free vars:         " << bool_var_vector(m_vars_to_free) << "\n";
             for (unsigned i = m_clauses_to_reinit.size(); i-- > old_sz; )
                 tout << "reinit:           " << m_clauses_to_reinit[i] << "\n";
             display(tout););        
@@ -3599,7 +3596,6 @@ namespace sat {
     void solver::pop(unsigned num_scopes) {
         if (num_scopes == 0)
             return;
-        unsigned free_vars_head = m_free_vars.size();
         if (m_ext) {
             pop_vars(num_scopes);
             m_ext->pop(num_scopes);
@@ -3609,13 +3605,16 @@ namespace sat {
         scope & s        = m_scopes[new_lvl];
         m_inconsistent   = false; // TBD: use model seems to make this redundant: s.m_inconsistent;
         unassign_vars(s.m_trail_lim, new_lvl);
-        for (unsigned i = m_free_vars.size(); i-- > free_vars_head; )
+        for (bool_var v : m_vars_to_free)
-            m_case_split_queue.del_var_eh(m_free_vars[i]);
+            m_case_split_queue.del_var_eh(v);
         m_scope_lvl -= num_scopes;
         reinit_clauses(s.m_clauses_to_reinit_lim);
         m_scopes.shrink(new_lvl);
-        if (m_ext) 
+        if (m_ext) {
             m_ext->pop_reinit();
+            m_free_vars.append(m_vars_to_free);
+            m_vars_to_free.reset();
+        }
     }
 
     void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) {
@@ -3692,6 +3691,7 @@ namespace sat {
     //
 
     void solver::user_push() {
+
         pop_to_base_level();
         m_free_var_freeze.push_back(m_free_vars);
         m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v

src/sat/sat_solver.h

@@ -124,7 +124,7 @@ namespace sat {
         clause_vector           m_clauses;
         clause_vector           m_learned;
         unsigned                m_num_frozen;
-        unsigned_vector         m_active_vars, m_free_vars, m_vars_to_reinit;
+        unsigned_vector         m_active_vars, m_free_vars, m_vars_to_free, m_vars_to_reinit;
         vector<watch_list>      m_watches;
         svector<lbool>          m_assignment;
         svector<justification>  m_justification; 
@@ -266,6 +266,11 @@ namespace sat {
         //
         // -----------------------
         void add_clause(unsigned num_lits, literal * lits, sat::status st) override { mk_clause(num_lits, lits, st); }
+        void add_clause(literal l1, literal l2, status st) {
+            literal lits[2] = { l1, l2 };
+            add_clause(2, lits, st);
+        }
+        void add_clause(literal lit, status st) { literal lits[1] = { lit }; add_clause(1, lits, st); }
         bool_var add_var(bool ext) override { return mk_var(ext, true); }
 
         bool_var mk_var(bool ext = false, bool dvar = true);
@@ -444,9 +449,10 @@ namespace sat {
         void       flush_roots();
         typedef std::pair<literal, literal> bin_clause;
         struct bin_clause_hash { unsigned operator()(bin_clause const& b) const { return b.first.hash() + 2*b.second.hash(); } };
-    protected:
+
-        watch_list & get_wlist(literal l) { return m_watches[l.index()]; }
         watch_list const& get_wlist(literal l) const { return m_watches[l.index()]; }
+        watch_list& get_wlist(literal l) { return m_watches[l.index()]; }
+    protected:            
         watch_list & get_wlist(unsigned l_idx) { return m_watches[l_idx]; }
         bool is_marked(bool_var v) const { return m_mark[v]; }
         void mark(bool_var v) { SASSERT(!is_marked(v)); m_mark[v] = true; }

src/sat/sat_solver_core.h

@@ -35,10 +35,7 @@ namespace sat {
 
         // add clauses
         virtual void add_clause(unsigned n, literal* lits, status st) = 0;
-        void add_clause(literal l1, literal l2, status st) {
+        
-            literal lits[2] = {l1, l2};
-            add_clause(2, lits, st);
-        }
         void add_clause(literal l1, literal l2, literal l3, status st) {
             literal lits[3] = {l1, l2, l3};
             add_clause(3, lits, st);

src/sat/smt/CMakeLists.txt

@@ -38,7 +38,6 @@ z3_add_component(sat_smt
     q_queue.cpp
     q_solver.cpp
     recfun_solver.cpp
-    sat_dual_solver.cpp
     sat_th.cpp
     user_solver.cpp
   COMPONENT_DEPENDENCIES

src/sat/smt/arith_internalize.cpp

@@ -545,11 +545,13 @@ namespace arith {
         }
         m_left_side.clear();
         // reset the coefficients after they have been used.
-        for (unsigned i = 0; i < vars.size(); ++i) {
+        for (theory_var var : vars) {
-            theory_var var = vars[i];
             rational const& r = m_columns[var];
             if (!r.is_zero()) {
-                m_left_side.push_back(std::make_pair(r, register_theory_var_in_lar_solver(var)));
+                auto vi = register_theory_var_in_lar_solver(var);
+                if (lp::tv::is_term(vi))
+                    vi = lp().map_term_index_to_column_index(vi);
+                m_left_side.push_back(std::make_pair(r, vi));
                 m_columns[var].reset();
             }
         }

src/sat/smt/arith_solver.cpp

@@ -953,6 +953,7 @@ namespace arith {
             if (n1->get_root() == n2->get_root())
                 continue;
             literal eq = eq_internalize(n1, n2);
+            ctx.mark_relevant(eq);
             if (s().value(eq) != l_true)
                 return true;
         }
@@ -1446,21 +1447,19 @@ namespace arith {
             TRACE("arith", tout << "canceled\n";);
             return l_undef;
         }
-        if (!m_nla) {
+        CTRACE("arith", !m_nla, tout << "no nla\n";);
-            TRACE("arith", tout << "no nla\n";);
+        if (!m_nla) 
             return l_true;
-        }
         if (!m_nla->need_check())
             return l_true;
 
         m_a1 = nullptr; m_a2 = nullptr;
         lbool r = m_nla->check(m_nla_lemma_vector);
         switch (r) {
-        case l_false: {
+        case l_false: 
             for (const nla::lemma& l : m_nla_lemma_vector)
                 false_case_of_check_nla(l);
             break;
-        }
         case l_true:
             if (assume_eqs())
                 return l_false;
@@ -1477,11 +1476,27 @@ namespace arith {
     }
 
     bool solver::include_func_interp(func_decl* f) const {
-        return 
+        SASSERT(f->get_family_id() == get_id());
-            a.is_div0(f) ||
+        switch (f->get_decl_kind()) {
-            a.is_idiv0(f) ||
+        case OP_ADD:
-            a.is_power0(f) ||
+        case OP_SUB:
-            a.is_rem0(f) ||
+        case OP_UMINUS:
-            a.is_mod0(f);        
+        case OP_MUL:
+        case OP_LE:
+        case OP_LT:
+        case OP_GE:
+        case OP_GT:
+        case OP_MOD:
+        case OP_REM:
+        case OP_DIV:
+        case OP_IDIV:
+        case OP_POWER:
+        case OP_IS_INT:
+        case OP_TO_INT:
+        case OP_TO_REAL:
+            return false;
+        default:
+            return true;            
+        }
     }
 }

src/sat/smt/arith_solver.h

@@ -445,6 +445,7 @@ namespace arith {
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
         bool include_func_interp(func_decl* f) const override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_add(n->get_expr()); }
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }

src/sat/smt/array_axioms.cpp

@@ -57,8 +57,6 @@ namespace array {
 
     bool solver::assert_axiom(unsigned idx) {
         axiom_record& r = m_axiom_trail[idx];
-        if (!is_relevant(r))
-            return false;
         switch (r.m_kind) {
         case axiom_record::kind_t::is_store:
             return assert_store_axiom(to_app(r.n->get_expr()));
@@ -86,35 +84,12 @@ namespace array {
             return assert_default_const_axiom(to_app(child));
         else if (a.is_store(child))
             return assert_default_store_axiom(to_app(child));
-        else if (a.is_map(child))
+        else if (is_map_combinator(child))
             return assert_default_map_axiom(to_app(child));
         else
             return false;                
     }
 
-
-    bool solver::is_relevant(axiom_record const& r) const {
-        return true;
-#if 0
-        // relevancy propagation is currently incomplete on terms
-
-        expr* child = r.n->get_expr();
-        switch (r.m_kind) {
-        case axiom_record::kind_t::is_select: {
-            app* select = r.select->get_app();
-            for (unsigned i = 1; i < select->get_num_args(); ++i)
-                if (!ctx.is_relevant(select->get_arg(i)))
-                    return false;
-            return ctx.is_relevant(child);            
-        }
-        case axiom_record::kind_t::is_default:
-            return ctx.is_relevant(child);            
-        default:
-            return true;
-        }
-#endif
-    }
-
     bool solver::assert_select(unsigned idx, axiom_record& r) {
         expr* child = r.n->get_expr();
         app* select = r.select->get_app();
@@ -140,7 +115,7 @@ namespace array {
             return assert_select_as_array_axiom(select, to_app(child));
         else if (a.is_store(child))
             return assert_select_store_axiom(select, to_app(child));
-        else if (a.is_map(child))
+        else if (is_map_combinator(child))
             return assert_select_map_axiom(select, to_app(child));
         else if (is_lambda(child))
             return assert_select_lambda_axiom(select, child);
@@ -215,10 +190,17 @@ namespace array {
             return new_prop;
         
         sat::literal sel_eq = sat::null_literal;
+        auto ensure_relevant = [&](sat::literal lit) {
+            if (ctx.is_relevant(lit))
+                return;
+            new_prop = true;
+            ctx.mark_relevant(lit);            
+        };
         auto init_sel_eq = [&]() {
             if (sel_eq != sat::null_literal) 
                 return true;
             sel_eq = mk_literal(sel_eq_e);
+            ensure_relevant(sel_eq);
             return s().value(sel_eq) != l_true;
         };
 
@@ -235,6 +217,7 @@ namespace array {
                 break;
             }
             sat::literal idx_eq = eq_internalize(idx1, idx2);
+            ensure_relevant(idx_eq);
             if (s().value(idx_eq) == l_true)
                 continue;
             if (s().value(idx_eq) == l_undef)
@@ -254,7 +237,6 @@ namespace array {
      *    select(const(v), i) = v
      */
     bool solver::assert_select_const_axiom(app* select, app* cnst) {        
-        
         ++m_stats.m_num_select_const_axiom;
         expr* val = nullptr;
         VERIFY(a.is_const(cnst, val));
@@ -291,16 +273,19 @@ namespace array {
         return add_clause(lit1, ~lit2);
     }
 
+    bool solver::is_map_combinator(expr* map) const {
+        return a.is_map(map) || a.is_union(map) || a.is_intersect(map) || a.is_difference(map) || a.is_complement(map);
+    }
+
     /**
     * Assert axiom:
     * select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i))
     */
     bool solver::assert_select_map_axiom(app* select, app* map) {
         ++m_stats.m_num_select_map_axiom;
-        SASSERT(a.is_map(map));
         SASSERT(a.is_select(select));
+        SASSERT(is_map_combinator(map));
         SASSERT(map->get_num_args() > 0);
-        func_decl* f = a.get_map_func_decl(map);
         unsigned num_args = select->get_num_args();
         ptr_buffer<expr> args1, args2;
         vector<ptr_vector<expr> > args2l;
@@ -321,7 +306,8 @@ namespace array {
 
         expr_ref sel1(m), sel2(m);
         sel1 = a.mk_select(args1);
-        sel2 = m.mk_app(f, args2);
+        sel2 = apply_map(map, args2.size(), args2.data());
+
         rewrite(sel2); 
         euf::enode* n1 = e_internalize(sel1);
         euf::enode* n2 = e_internalize(sel2);
@@ -348,21 +334,44 @@ namespace array {
         return ctx.propagate(n1, n2, array_axiom());
     }
 
+    expr_ref solver::apply_map(app* map, unsigned n, expr* const* args) {
+        expr_ref result(m);
+        if (a.is_map(map)) 
+            result = m.mk_app(a.get_map_func_decl(map), n, args);
+        else if (a.is_union(map)) 
+            result = m.mk_or(n, args);
+        else if (a.is_intersect(map)) 
+            result = m.mk_and(n, args);
+        else if (a.is_difference(map)) {
+            SASSERT(n > 0);
+            result = args[0];
+            for (unsigned i = 1; i < n; ++i)
+                result = m.mk_and(result, m.mk_not(args[i]));
+        }
+        else if (a.is_complement(map)) {
+            SASSERT(n == 1);
+            result = m.mk_not(args[0]);
+        }
+        else {            
+            UNREACHABLE();
+        }
+        rewrite(result);
+        return result;
+    }
+
+
     /**
      * Assert:
      *    default(map[f](a,..,d)) = f(default(a),..,default(d))
      */
     bool solver::assert_default_map_axiom(app* map) {
         ++m_stats.m_num_default_map_axiom;
-        SASSERT(a.is_map(map));
+        SASSERT(is_map_combinator(map));
-        func_decl* f = a.get_map_func_decl(map);
-        SASSERT(map->get_num_args() == f->get_arity());
         expr_ref_vector args2(m);
         for (expr* arg : *map)
             args2.push_back(a.mk_default(arg));
         expr_ref def1(a.mk_default(map), m);
-        expr_ref def2(m.mk_app(f, args2), m);
+        expr_ref def2 = apply_map(map, args2.size(), args2.data());
-        rewrite(def2);
         return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom());
     }
 
@@ -534,11 +543,14 @@ namespace array {
         unsigned num_vars = get_num_vars();
         bool change = false;
         for (unsigned v = 0; v < num_vars; v++) {
-            propagate_parent_select_axioms(v);
             auto& d = get_var_data(v);
             if (!d.m_prop_upward)
                 continue;
             euf::enode* n = var2enode(v);
+            if (!ctx.is_relevant(n))
+                continue;
+            for (euf::enode* lambda : d.m_parent_lambdas)
+                propagate_select_axioms(d, lambda);
             if (add_as_array_eqs(n))
                 change = true;
             bool has_default = false;
@@ -567,6 +579,8 @@ namespace array {
             return false;
         for (unsigned i = 0; i < ctx.get_egraph().enodes_of(f).size(); ++i) {
             euf::enode* p = ctx.get_egraph().enodes_of(f)[i];
+            if (!ctx.is_relevant(p))
+                continue;
             expr_ref_vector select(m);
             select.push_back(n->get_expr());
             for (expr* arg : *to_app(p->get_expr()))
@@ -574,7 +588,8 @@ namespace array {
             expr_ref _e(a.mk_select(select.size(), select.data()), m);
             euf::enode* e = e_internalize(_e);
             if (e->get_root() != p->get_root()) {
-                add_unit(eq_internalize(_e, p->get_expr()));
+                sat::literal eq = eq_internalize(_e, p->get_expr());
+                add_unit(eq);
                 change = true;
             }
         }
@@ -594,13 +609,12 @@ namespace array {
                 expr* e2 = var2expr(v2);
                 if (e1->get_sort() != e2->get_sort())
                     continue;
-                if (must_have_different_model_values(v1, v2)) {
+                if (must_have_different_model_values(v1, v2)) 
                     continue;                
-                }
+                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) 
-                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) {
                     continue;                
-                }
                 sat::literal lit = eq_internalize(e1, e2);
+                ctx.mark_relevant(lit);
                 if (s().value(lit) == l_undef) 
                     prop = true;
             }
@@ -613,9 +627,10 @@ namespace array {
         unsigned num_vars = get_num_vars();
         for (unsigned i = 0; i < num_vars; i++) {
             euf::enode * n = var2enode(i);            
-            
             if (!is_array(n)) 
                 continue;
+            if (!ctx.is_relevant(n))
+                continue;
             euf::enode * r = n->get_root();
             if (r->is_marked1()) 
                 continue;            

src/sat/smt/array_internalize.cpp

@@ -49,7 +49,7 @@ namespace array {
         if (v == euf::null_theory_var) {
             mk_var(n);
             if (is_lambda(n->get_expr()))
-                internalize_lambda(n);
+                internalize_lambda_eh(n);
         }
     }
 
@@ -57,45 +57,6 @@ namespace array {
         ensure_var(n);
     }
 
-    void solver::internalize_store(euf::enode* n) {
-        add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);   
-        push_axiom(store_axiom(n));
-        add_lambda(n->get_th_var(get_id()), n);
-        SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
-    }
-
-    void solver::internalize_map(euf::enode* n) {
-        for (auto* arg : euf::enode_args(n)) {
-            add_parent_lambda(arg->get_th_var(get_id()), n);
-            set_prop_upward(arg);
-        }
-        push_axiom(default_axiom(n));
-        add_lambda(n->get_th_var(get_id()), n);
-        SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
-    }
-
-    void solver::internalize_lambda(euf::enode* n) {
-        SASSERT(is_lambda(n->get_expr()) || a.is_const(n->get_expr()) || a.is_as_array(n->get_expr()));
-        theory_var v = n->get_th_var(get_id());
-        push_axiom(default_axiom(n));
-        add_lambda(v, n);
-        set_prop_upward(v);
-    }
-
-    void solver::internalize_select(euf::enode* n) {
-        add_parent_select(n->get_arg(0)->get_th_var(get_id()), n);
-    }
-
-    void solver::internalize_ext(euf::enode* n) {
-        SASSERT(is_array(n->get_arg(0)));
-        push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
-    }
-
-    void solver::internalize_default(euf::enode* n) {
-        add_parent_default(n->get_arg(0)->get_th_var(get_id()), n);
-        set_prop_upward(n);
-    }
-
     bool solver::visited(expr* e) {
         euf::enode* n = expr2enode(e);
         return n && n->is_attached_to(get_id());        
@@ -124,40 +85,111 @@ namespace array {
             mk_var(n);
         for (auto* arg : euf::enode_args(n))
             ensure_var(arg);  
-        switch (a->get_decl_kind()) {
+        internalize_eh(n);
+        if (ctx.is_relevant(n))
+            relevant_eh(n);
+        return true;
+    }
+
+    void solver::internalize_lambda_eh(euf::enode* n) {
+        push_axiom(default_axiom(n));
+        auto& d = get_var_data(find(n));
+        ctx.push_vec(d.m_lambdas, n);
+    }
+
+    void solver::internalize_eh(euf::enode* n) {
+        switch (n->get_decl()->get_decl_kind()) {
         case OP_STORE:          
-            internalize_store(n); 
+            ctx.push_vec(get_var_data(find(n)).m_lambdas, n);
+            push_axiom(store_axiom(n));
             break;
         case OP_SELECT:
-            internalize_select(n); 
             break;
         case OP_AS_ARRAY:
         case OP_CONST_ARRAY:
-            internalize_lambda(n); 
+            internalize_lambda_eh(n);
             break;
         case OP_ARRAY_EXT:
-            internalize_ext(n); 
+            SASSERT(is_array(n->get_arg(0)));
+            push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
             break;
         case OP_ARRAY_DEFAULT:
-            internalize_default(n); 
+            add_parent_default(find(n->get_arg(0)), n);
             break;
         case OP_ARRAY_MAP:
-            internalize_map(n); 
-            break;
         case OP_SET_UNION:
         case OP_SET_INTERSECT:
         case OP_SET_DIFFERENCE:
         case OP_SET_COMPLEMENT:
-        case OP_SET_SUBSET:      
+            for (auto* arg : euf::enode_args(n)) 
+                add_parent_lambda(find(arg), n);
+            internalize_lambda_eh(n);
+            break;
+        case OP_SET_SUBSET: {
+            expr* x, *y;
+            VERIFY(a.is_subset(n->get_expr(), x, y));
+            expr_ref diff(a.mk_setminus(x, y), m);
+            expr_ref emp(a.mk_empty_set(x->get_sort()), m);
+            sat::literal eq = eq_internalize(diff, emp);
+            sat::literal sub = expr2literal(n->get_expr());
+            add_equiv(eq, sub);
+            break;
+        }            
         case OP_SET_HAS_SIZE:
         case OP_SET_CARD:
-            ctx.unhandled_function(a->get_decl()); 
+            ctx.unhandled_function(n->get_decl());
+            break;
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+
+    void solver::relevant_eh(euf::enode* n) {
+        if (is_lambda(n->get_expr())) {
+            set_prop_upward(find(n));
+            return;
+        }
+        if (!is_app(n->get_expr()))
+            return;
+        if (n->get_decl()->get_family_id() != a.get_family_id())
+            return;
+        switch (n->get_decl()->get_decl_kind()) {
+        case OP_STORE:
+            add_parent_lambda(find(n->get_arg(0)), n);   
+            break;
+        case OP_SELECT:
+            add_parent_select(find(n->get_arg(0)), n);
+            break;
+        case OP_CONST_ARRAY:
+        case OP_AS_ARRAY:
+            set_prop_upward(find(n));            
+            propagate_parent_default(find(n));
+            break;
+        case OP_ARRAY_EXT:
+            break;
+        case OP_ARRAY_DEFAULT:
+            set_prop_upward(find(n->get_arg(0)));
+            break;
+        case OP_ARRAY_MAP:
+        case OP_SET_UNION:
+        case OP_SET_INTERSECT:
+        case OP_SET_DIFFERENCE:
+        case OP_SET_COMPLEMENT:
+            for (auto* arg : euf::enode_args(n)) 
+                set_prop_upward_store(arg);
+            set_prop_upward(find(n));
+            break;
+        case OP_SET_SUBSET:
+            break;
+        case OP_SET_HAS_SIZE:
+        case OP_SET_CARD:
+            ctx.unhandled_function(n->get_decl());
             break;
         default:
             UNREACHABLE();
             break;
         }
-        return true;
     }
 
     /**

src/sat/smt/array_solver.cpp

@@ -186,17 +186,16 @@ namespace array {
         if (should_set_prop_upward(d))
             set_prop_upward(d);
         ctx.push_vec(d.m_lambdas, lambda);
-        if (should_set_prop_upward(d)) {
-            set_prop_upward(lambda);
         propagate_select_axioms(d, lambda);
-        }
+        if (should_set_prop_upward(d)) 
+            set_prop_upward_store(lambda);                    
     }
 
     void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
         SASSERT(can_beta_reduce(lambda));
         auto& d = get_var_data(find(v_child));
         ctx.push_vec(d.m_parent_lambdas, lambda);
-        if (should_set_prop_upward(d))
+        if (should_prop_upward(d))        
             propagate_select_axioms(d, lambda);
     }
 
@@ -231,6 +230,9 @@ namespace array {
         for (euf::enode* lambda : d.m_lambdas) 
             propagate_select_axioms(d, lambda);        
         
+        if (!should_prop_upward(d))
+            return;
+
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);
     }
@@ -246,14 +248,14 @@ namespace array {
         set_prop_upward(d);
     }
 
-    void solver::set_prop_upward(euf::enode* n) {
+    void solver::set_prop_upward_store(euf::enode* n) {
         if (a.is_store(n->get_expr()))
             set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
     }
 
     void solver::set_prop_upward(var_data& d) {
         for (auto* p : d.m_lambdas)
-            set_prop_upward(p);
+            set_prop_upward_store(p);
     }
 
     /**
@@ -273,6 +275,6 @@ namespace array {
     }
 
     bool solver::can_beta_reduce(expr* c) const {
-        return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c);
+        return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || is_map_combinator(c);
     }
 }

src/sat/smt/array_solver.h

@@ -66,6 +66,7 @@ namespace array {
         array_union_find                     m_find;
 
         theory_var find(theory_var v) { return m_find.find(v); }
+        theory_var find(euf::enode* n) { return find(n->get_th_var(get_id())); }
         func_decl_ref_vector const& sort2diff(sort* s);
 
         // internalize
@@ -73,12 +74,8 @@ namespace array {
         bool visited(expr* e) override;
         bool post_visit(expr* e, bool sign, bool root) override;
         void ensure_var(euf::enode* n);
-        void internalize_store(euf::enode* n);
+        void internalize_eh(euf::enode* n);
-        void internalize_select(euf::enode* n);
+        void internalize_lambda_eh(euf::enode* n);
-        void internalize_lambda(euf::enode* n);
-        void internalize_ext(euf::enode* n);
-        void internalize_default(euf::enode* n);
-        void internalize_map(euf::enode* n);
 
         // axioms
         struct axiom_record {
@@ -157,7 +154,6 @@ namespace array {
         bool assert_axiom(unsigned idx);
         bool assert_select(unsigned idx, axiom_record & r);
         bool assert_default(axiom_record & r);
-        bool is_relevant(axiom_record const& r) const;
         void set_applied(unsigned idx) { m_axiom_trail[idx].set_applied(); }
         bool is_applied(unsigned idx) const { return m_axiom_trail[idx].is_applied(); }
         bool is_delayed(unsigned idx) const { return m_axiom_trail[idx].is_delayed(); }
@@ -185,6 +181,8 @@ namespace array {
         bool assert_congruent_axiom(expr* e1, expr* e2);
         bool add_delayed_axioms();
         bool add_as_array_eqs(euf::enode* n);
+        expr_ref apply_map(app* map, unsigned n, expr* const* args);
+        bool is_map_combinator(expr* e) const;
 
         bool has_unitary_domain(app* array_term);
         bool has_large_domain(expr* array_term);
@@ -206,7 +204,7 @@ namespace array {
 
         void set_prop_upward(theory_var v);
         void set_prop_upward(var_data& d);
-        void set_prop_upward(euf::enode* n);
+        void set_prop_upward_store(euf::enode* n);
         unsigned get_lambda_equiv_size(var_data const& d) const;
         bool should_set_prop_upward(var_data const& d) const;
         bool should_prop_upward(var_data const& d) const;
@@ -264,6 +262,8 @@ namespace array {
         void apply_sort_cnstr(euf::enode* n, sort* s) override;
         bool is_shared(theory_var v) const override;
         bool enable_self_propagate() const override { return true; }
+        void relevant_eh(euf::enode* n) override;
+        bool enable_ackerman_axioms(euf::enode* n) const override { return !a.is_array(n->get_sort()); }
  
         void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2);
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}

src/sat/smt/bv_delay_internalize.cpp

@@ -21,7 +21,10 @@ Author:
 namespace bv {
 
     bool solver::check_delay_internalized(expr* e) {
-        if (!ctx.is_relevant(e))
+        euf::enode* n = expr2enode(e);
+        if (!n)
+            return true;
+        if (!ctx.is_relevant(n))
             return true;
         if (get_internalize_mode(e) != internalize_mode::delay_i)
             return true;
@@ -247,7 +250,7 @@ namespace bv {
             return;
         expr_ref tmp = literal2expr(bits.back());
         for (unsigned i = bits.size() - 1; i-- > 0; ) {
-            auto b = bits[i];
+            sat::literal b = bits[i];
             tmp = m.mk_or(literal2expr(b), tmp);
             xs.push_back(tmp);
         }

src/sat/smt/bv_internalize.cpp

@@ -166,6 +166,7 @@ namespace bv {
 #define internalize_pun(F) pun = [&](unsigned sz, expr* const* xs, unsigned p, expr_ref_vector& bits) { m_bb.F(sz, xs, p, bits);}; internalize_par_unary(a, pun);
 #define internalize_nfl(F) ebin = [&](unsigned sz, expr* const* xs, expr* const* ys, expr_ref& out) { m_bb.F(sz, xs, ys, out);}; internalize_novfl(a, ebin);
 #define internalize_int(B, U) ibin = [&](expr* x, expr* y) { return B(x, y); }; iun = [&](expr* x) { return U(x); }; internalize_interp(a, ibin, iun);
+#define if_unary(F) if (a->get_num_args() == 1) { internalize_un(F); break; }
 
         switch (a->get_decl_kind()) {
         case OP_BV_NUM:           internalize_num(a); break;
@@ -190,7 +191,7 @@ namespace bv {
         case OP_BXOR:             internalize_ac(mk_xor); break;
         case OP_BNAND:            internalize_bin(mk_nand); break;
         case OP_BNOR:             internalize_bin(mk_nor); break;
-        case OP_BXNOR:            internalize_bin(mk_xnor); break;
+        case OP_BXNOR:            if_unary(mk_not); internalize_bin(mk_xnor); break;
         case OP_BCOMP:            internalize_bin(mk_comp); break;        
         case OP_SIGN_EXT:         internalize_pun(mk_sign_extend); break;
         case OP_ZERO_EXT:         internalize_pun(mk_zero_extend); break;
@@ -426,7 +427,6 @@ namespace bv {
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
         sat::literal lit = eq_internalize(n, sum);
 	add_unit(lit);
-	ctx.add_root(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -456,7 +456,6 @@ namespace bv {
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
 	sat::literal eq_lit = eq_internalize(lhs, rhs);
 	add_unit(eq_lit);
-	ctx.add_root(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -469,7 +468,6 @@ namespace bv {
             lhs = n_bits.get(i);
 	    eq_lit = eq_internalize(lhs, rhs);
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
         }
     }
 
@@ -535,7 +533,6 @@ namespace bv {
         if (p.hi_div0()) {
             eq_lit = eq_internalize(n, ibin(arg1, arg2));
 	    add_unit(eq_lit);
-	    ctx.add_root(eq_lit);
 	}
 	else {
 	    unsigned sz = bv.get_bv_size(n);
@@ -653,7 +650,6 @@ namespace bv {
         mk_bits(get_th_var(e));
 	sat::literal eq_lit = eq_internalize(e, r);
         add_unit(eq_lit);
-	ctx.add_root(eq_lit);
     }
 
     void solver::internalize_bit2bool(app* n) {

src/sat/smt/euf_ackerman.cpp

@@ -99,14 +99,38 @@ namespace euf {
         m_tmp_inference->init(m_tmp_inference);
     }
 
+    bool ackerman::enable_cc(app* a, app* b) {
+        if (!s.enable_ackerman_axioms(a))
+            return false;
+        if (!s.enable_ackerman_axioms(b))
+            return false;
+        for (expr* arg : *a)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        for (expr* arg : *b)
+            if (!s.enable_ackerman_axioms(arg))
+                return false;
+        return true;
+    }
+
+    bool ackerman::enable_eq(expr* a, expr* b, expr* c) {
+        return s.enable_ackerman_axioms(a) && 
+            s.enable_ackerman_axioms(b) && 
+            s.enable_ackerman_axioms(c);           
+    }
+
     void ackerman::cg_conflict_eh(expr * n1, expr * n2) {
         if (!is_app(n1) || !is_app(n2))
             return;
+        if (!s.enable_ackerman_axioms(n1))
+            return;
         SASSERT(!s.m_drating);
         app* a = to_app(n1);
         app* b = to_app(n2);
         if (a->get_decl() != b->get_decl() || a->get_num_args() != b->get_num_args())
             return;
+        if (!enable_cc(a, b))
+            return;
         TRACE("ack", tout << "conflict eh: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         insert(a, b);
         gc();
@@ -117,6 +141,8 @@ namespace euf {
             return;
         if (s.m_drating)
             return;
+        if (!enable_eq(a, b, c))
+            return;
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
         insert(a, b, c);
         gc();
@@ -128,6 +154,8 @@ namespace euf {
         TRACE("ack", tout << "used cc: " << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n";);
         SASSERT(a->get_decl() == b->get_decl());
         SASSERT(a->get_num_args() == b->get_num_args());
+        if (!enable_cc(a, b))
+            return;
         insert(a, b);
         gc();
     }
@@ -176,10 +204,10 @@ namespace euf {
         unsigned sz = a->get_num_args();        
         
         for (unsigned i = 0; i < sz; ++i) {
-            expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m);
+            expr_ref eq = s.mk_eq(a->get_arg(i), b->get_arg(i));
             lits.push_back(~s.mk_literal(eq));
         }
-        expr_ref eq(m.mk_eq(a, b), m);
+        expr_ref eq = s.mk_eq(a, b);
         lits.push_back(s.mk_literal(eq));
         s.s().mk_clause(lits, sat::status::th(true, m.get_basic_family_id()));
     }
@@ -187,9 +215,9 @@ namespace euf {
     void ackerman::add_eq(expr* a, expr* b, expr* c) {
         flet<bool> _is_redundant(s.m_is_redundant, true);
         sat::literal lits[3];
-        expr_ref eq1(m.mk_eq(a, c), m);
+        expr_ref eq1(s.mk_eq(a, c), m);
-        expr_ref eq2(m.mk_eq(b, c), m);
+        expr_ref eq2(s.mk_eq(b, c), m);
-        expr_ref eq3(m.mk_eq(a, b), m);
+        expr_ref eq3(s.mk_eq(a, b), m);
         TRACE("ack", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << "\n";);
         lits[0] = ~s.mk_literal(eq1);
         lits[1] = ~s.mk_literal(eq2);

src/sat/smt/euf_ackerman.h

@@ -70,6 +70,9 @@ namespace euf {
         void add_cc(expr* a, expr* b);
         void add_eq(expr* a, expr* b, expr* c);        
         void gc();
+        bool enable_cc(app* a, app* b);
+        bool enable_eq(expr* a, expr* b, expr* c);
+
 
     public:
         ackerman(solver& s, ast_manager& m);

src/sat/smt/euf_internalize.cpp

@@ -162,10 +162,8 @@ namespace euf {
             sat::literal lit2 = literal(v, false);
             s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
             s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
-            if (relevancy_enabled()) {
             add_aux(~lit, lit2);
             add_aux(lit, ~lit2);
-            }
             lit = lit2;
         }
 
@@ -185,8 +183,6 @@ namespace euf {
         m_egraph.set_bool_var(n, v);
         if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
             m_egraph.set_merge_enabled(n, false);
-        if (!si.is_bool_op(e))
-            track_relevancy(lit.var());
         if (s().value(lit) != l_undef) 
             m_egraph.set_value(n, s().value(lit));
         return lit;
@@ -224,9 +220,8 @@ namespace euf {
                     lits.push_back(lit);
                 }
             }
-            s().mk_clause(lits, st);
-            if (relevancy_enabled())
             add_root(lits);
+            s().mk_clause(lits, st);
         }
         else {
             // g(f(x_i)) = x_i
@@ -244,15 +239,13 @@ namespace euf {
                 expr_ref gapp(m.mk_app(g, fapp.get()), m);
                 expr_ref eq = mk_eq(gapp, arg);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
+                s().add_clause(lit, st);
                 eqs.push_back(mk_eq(fapp, a));
             }
             pb_util pb(m);
             expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
             sat::literal lit = si.internalize(at_least2, m_is_redundant);
-            s().mk_clause(1, &lit, st);
+            s().add_clause(lit, st);
-            if (relevancy_enabled())
-                add_root(1, &lit);
         }
     }
 
@@ -268,9 +261,7 @@ namespace euf {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
                     sat::literal lit = ~mk_literal(eq);
-                    s().add_clause(1, &lit, st);
+                    s().add_clause(lit, st);
-                    if (relevancy_enabled())
-                        add_root(1, &lit);
                 }
             }
         }
@@ -287,9 +278,7 @@ namespace euf {
                 n->mark_interpreted();
                 expr_ref eq = mk_eq(fapp, fresh);
                 sat::literal lit = mk_literal(eq);
-                s().add_clause(1, &lit, st);
+                s().add_clause(lit, st);
-                if (relevancy_enabled())
-                    add_root(1, &lit);
             }
         }
     }
@@ -302,16 +291,16 @@ namespace euf {
             expr_ref eq_th = mk_eq(e, th);
             sat::literal lit_th = mk_literal(eq_th);
             if (th == el) {
-                s().add_clause(1, &lit_th, st);
+                s().add_clause(lit_th, st);
             }
             else {
                 sat::literal lit_c = mk_literal(c);
                 expr_ref eq_el = mk_eq(e, el);
                 sat::literal lit_el = mk_literal(eq_el);
-                literal lits1[2] = { ~lit_c,  lit_th };
+                add_root(~lit_c, lit_th);
-                literal lits2[2] = { lit_c, lit_el };
+                add_root(lit_c, lit_el);
-                s().add_clause(2, lits1, st);
+                s().add_clause(~lit_c, lit_th, st);
-                s().add_clause(2, lits2, st);
+                s().add_clause(lit_c, lit_el, st);
             }
         }
         else if (m.is_distinct(e)) {
@@ -326,10 +315,10 @@ namespace euf {
             expr_ref fml(m.mk_or(eqs), m);
             sat::literal dist(si.to_bool_var(e), false);
             sat::literal some_eq = si.internalize(fml, m_is_redundant);
-            sat::literal lits1[2] = { ~dist, ~some_eq };
+            add_root(~dist, ~some_eq);
-            sat::literal lits2[2] = { dist, some_eq };
+            add_root(dist, some_eq);
-            s().add_clause(2, lits1, st);
+            s().add_clause(~dist, ~some_eq, st);
-            s().add_clause(2, lits2, st);
+            s().add_clause(dist, some_eq, st);
         }
         else if (m.is_eq(e, th, el) && !m.is_iff(e)) {
             sat::literal lit1 = expr2literal(e);
@@ -338,10 +327,10 @@ namespace euf {
             enode* n2 = m_egraph.find(e2);
             if (n2) {
                 sat::literal lit2 = expr2literal(e2);
-                sat::literal lits1[2] = { ~lit1, lit2 };
+                add_root(~lit1, lit2);
-                sat::literal lits2[2] = { lit1, ~lit2 };
+                add_root(lit1, ~lit2);
-                s().add_clause(2, lits1, st);
+                s().add_clause(~lit1, lit2, st);
-                s().add_clause(2, lits2, st);
+                s().add_clause(lit1, ~lit2, st);
             }
         }
     }
@@ -357,7 +346,7 @@ namespace euf {
         // contains a parent application.
         
         family_id th_id = m.get_basic_family_id();
-        for (auto p : euf::enode_th_vars(n)) {
+        for (auto const& p : euf::enode_th_vars(n)) {
             family_id id = p.get_id();
             if (m.get_basic_family_id() != id) {
                 if (th_id != m.get_basic_family_id())
@@ -402,7 +391,7 @@ namespace euf {
         // Remark: The inconsistency is not going to be detected if they are
         // not marked as shared.
 
-        for (auto p : euf::enode_th_vars(n)) 
+        for (auto const& p : euf::enode_th_vars(n)) 
             if (fid2solver(p.get_id())->is_shared(p.get_var()))
                 return true;
 

src/sat/smt/euf_model.cpp

@@ -35,7 +35,7 @@ namespace euf {
             s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
 
         ~user_sort() {
-            for (auto kv : sort2values)
+            for (auto const& kv : sort2values)
                 mdl->register_usort(kv.m_key, kv.m_value->size(), kv.m_value->data());
         }
 
@@ -161,10 +161,9 @@ namespace euf {
                 default:
                     break;
                 }
-                if (is_app(e) && to_app(e)->get_family_id() == m.get_basic_family_id())
-                    continue;
                 sat::bool_var v = get_enode(e)->bool_var();
-                SASSERT(v != sat::null_bool_var);
+                if (v == sat::null_bool_var)
+                    continue;
                 switch (s().value(v)) {
                 case l_true:
                     m_values.set(id, m.mk_true());
@@ -200,6 +199,8 @@ namespace euf {
             expr* e = n->get_expr();
             if (!is_app(e))
                 continue;
+            if (!is_relevant(n))
+                continue;
             app* a = to_app(e);
             func_decl* f = a->get_decl();       
             if (!include_func_interp(f))
@@ -224,7 +225,7 @@ namespace euf {
                     enode* earg = get_enode(arg); 
                     expr* val = m_values.get(earg->get_root_id());
                     args.push_back(val);                
-                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
+                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n" << bpp(n) << "\n"; display(tout););
                     SASSERT(val);
                 }
                 SASSERT(args.size() == arity);
@@ -259,7 +260,7 @@ namespace euf {
             if (n->is_root() && m_values.get(n->get_expr_id()))
                 m_values2root.insert(m_values.get(n->get_expr_id()), n);
         TRACE("model", 
-              for (auto kv : m_values2root) 
+              for (auto const& kv : m_values2root) 
                   tout << mk_bounded_pp(kv.m_key, m) << "\n    -> " << bpp(kv.m_value) << "\n";);
         
         return m_values2root;
@@ -271,6 +272,8 @@ namespace euf {
 
     void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
         out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
+        s().display(out);
+        return;
         euf::enode_vector nodes;
         nodes.push_back(n);
         for (unsigned i = 0; i < nodes.size(); ++i) {
@@ -289,7 +292,6 @@ namespace euf {
         for (euf::enode* r : nodes)
             r->unmark1();
         out << mdl << "\n";
-        s().display(out);
     }
 
     void solver::validate_model(model& mdl) {
@@ -297,6 +299,8 @@ namespace euf {
         ev.set_model_completion(true);
         TRACE("model",
             for (enode* n : m_egraph.nodes()) {
+                if (!is_relevant(n))
+                    continue;
                 unsigned id = n->get_root_id();
                 expr* val = m_values.get(id, nullptr);
                 if (!val)
@@ -322,6 +326,8 @@ namespace euf {
             IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
             CTRACE("euf", first, display_validation_failure(tout, mdl, n););
             (void)first;
+            first = false;
+            return;
             exit(1);
             first = false;
         }        

src/sat/smt/euf_relevancy.cpp

@@ -3,157 +3,326 @@ Copyright (c) 2020 Microsoft Corporation
 
 Module Name:
 
-    euf_relevancy.cpp
+    smt_relevant.cpp
 
 Abstract:
 
-    Features for relevancy tracking.
+    Relevancy propagation
-    A reduced (minimal) implicant is extracted by running a dual solver.
-    Then the literals in the implicant are used as a basis for marking
-    subterms relevant.
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2020-09-22
+    Nikolaj Bjorner (nbjorner) 2021-12-27
 
 --*/
-
+#include "sat/sat_solver.h"
 #include "sat/smt/euf_solver.h"
+#include "sat/smt/euf_relevancy.h"
+
 
 namespace euf {
     
-    void solver::add_auto_relevant(expr* e) {
+    void relevancy::pop(unsigned n) {
-        if (!relevancy_enabled())
+        if (!m_enabled)
             return;
-        for (; m_auto_relevant_scopes > 0; --m_auto_relevant_scopes) 
+        if (n <= m_num_scopes) {
-            m_auto_relevant_lim.push_back(m_auto_relevant.size());
+            m_num_scopes -= n;
-        // std::cout << "add-auto " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
-        m_auto_relevant.push_back(e);
-    }
-    
-    void solver::pop_relevant(unsigned n) {
-        if (m_auto_relevant_scopes >= n) {
-            m_auto_relevant_scopes -= n;
             return;
         }
-        n -= m_auto_relevant_scopes;
+        else if (m_num_scopes > 0) {
-        m_auto_relevant_scopes = 0;
+            n -= m_num_scopes;
-        unsigned top = m_auto_relevant_lim.size() - n;
+            m_num_scopes = 0;
-        unsigned lim = m_auto_relevant_lim[top];
+        }
-        m_auto_relevant_lim.shrink(top);
+        SASSERT(n > 0);
-        m_auto_relevant.shrink(lim);        
+        unsigned sz = m_lim[m_lim.size() - n];
+        for (unsigned i = m_trail.size(); i-- > sz; ) {
+            auto const& [u, idx] = m_trail[i];
+            switch (u) {
+            case update::relevant_var:
+                m_relevant_var_ids[idx] = false;
+                break;
+            case update::add_queue:
+                m_queue.pop_back();
+                break;
+            case update::add_clause: {
+                sat::clause* c = m_clauses.back();
+                for (sat::literal lit : *c) {
+                    SASSERT(m_occurs[lit.index()].back() == m_clauses.size() - 1);
+                    m_occurs[lit.index()].pop_back();
+                }
+                m_clauses.pop_back();
+                m_roots.pop_back();
+                m_alloc.del_clause(c);
+                break;
+            }
+            case update::set_root:
+                m_roots[idx] = false;
+                break;
+            case update::set_qhead:
+                m_qhead = idx;
+                break;
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        m_trail.shrink(sz);
+        m_lim.shrink(m_lim.size() - n);
     }
     
-    void solver::push_relevant() {
+    void relevancy::add_root(unsigned n, sat::literal const* lits) {
-        ++m_auto_relevant_scopes;
+        if (!m_enabled)
-    }
-
-    bool solver::is_relevant(expr* e) const { 
-        return m_relevant_expr_ids.get(e->get_id(), true); 
-    }
-
-    bool solver::is_relevant(enode* n) const { 
-        return m_relevant_expr_ids.get(n->get_expr_id(), true); 
-    }
-
-    void solver::ensure_dual_solver() {
-        if (m_dual_solver)
             return;
-        m_dual_solver = alloc(sat::dual_solver, s().rlimit());
+        flush();
-        for (unsigned i = s().num_user_scopes(); i-- > 0; )
+        TRACE("relevancy", tout << "root " << sat::literal_vector(n, lits) << "\n");
-            m_dual_solver->push();        
+        sat::literal true_lit = sat::null_literal;
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_true) {
+                if (is_relevant(lits[i]))
+                    return;
+                true_lit = lits[i];                
+            }
+        }
+        if (true_lit != sat::null_literal) {
+            mark_relevant(true_lit);
+            return;
+        }
+
+        sat::clause* cl = m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(cl);
+        m_roots.push_back(true);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : *cl) {
+            ctx.s().set_external(lit.var());
+            occurs(lit).push_back(sz);
+        }
+    }
+    
+    void relevancy::add_def(unsigned n, sat::literal const* lits) {        
+        if (!m_enabled)
+            return;
+        flush();
+        TRACE("relevancy", tout << "def " << sat::literal_vector(n, lits) << "\n");
+        for (unsigned i = 0; i < n; ++i) {
+            if (ctx.s().value(lits[i]) == l_false && is_relevant(lits[i])) {
+                add_root(n, lits);
+                return;
+            }
+        }
+        sat::clause* cl = m_alloc.mk_clause(n, lits, false);
+        unsigned sz = m_clauses.size();
+        m_clauses.push_back(cl);
+        m_roots.push_back(false);
+        m_trail.push_back(std::make_pair(update::add_clause, 0));
+        for (sat::literal lit : *cl) {
+            ctx.s().set_external(lit.var());
+            occurs(lit).push_back(sz);
+        }
+    }
+
+    void relevancy::add_to_propagation_queue(sat::literal lit) {
+        m_trail.push_back(std::make_pair(update::add_queue, lit.var()));
+        m_queue.push_back(std::make_pair(lit, nullptr));
+    }
+
+    void relevancy::set_relevant(sat::literal lit) {
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n)
+            mark_relevant(n);        
+        m_relevant_var_ids.setx(lit.var(), true, false);
+        m_trail.push_back(std::make_pair(update::relevant_var, lit.var()));
+    }
+
+    void relevancy::set_asserted(sat::literal lit) {
+        SASSERT(!is_relevant(lit));
+        SASSERT(ctx.s().value(lit) == l_true);
+        set_relevant(lit);
+        add_to_propagation_queue(lit);
+        ctx.asserted(lit);
     }
 
     /**
-     * Add a root clause. Root clauses must all be satisfied by the 
+    * Boolean variable is set relevant because an E-node is relevant.
-     * final assignment. If a clause is added above search level it
+    * 
-     * is subject to removal on backtracking. These clauses are therefore
-     * not tracked.
     */
-    void solver::add_root(unsigned n, sat::literal const* lits) {
+    void relevancy::relevant_eh(sat::bool_var v) {
-        if (!relevancy_enabled())
+        if (is_relevant(v))
             return;
-        ensure_dual_solver();
+        sat::literal lit(v);
-        m_dual_solver->add_root(n, lits);
+        switch (ctx.s().value(lit)) {
-    }
+        case l_undef:
-
+            set_relevant(lit);
-    void solver::add_aux(unsigned n, sat::literal const* lits) {
+            break;
-        if (!relevancy_enabled())
-            return;
-        ensure_dual_solver();
-        m_dual_solver->add_aux(n, lits);
-    }
-
-    void solver::track_relevancy(sat::bool_var v) {
-        ensure_dual_solver();
-        m_dual_solver->track_relevancy(v);
-    }
-
-    bool solver::init_relevancy() {
-        m_relevant_expr_ids.reset();
-        if (!relevancy_enabled())
-            return true;
-        if (!m_dual_solver)
-            return true;
-        if (!(*m_dual_solver)(s()))
-            return false;
-        unsigned max_id = 0;
-        for (enode* n : m_egraph.nodes())
-            max_id = std::max(max_id, n->get_expr_id());
-        m_relevant_expr_ids.resize(max_id + 1, false);
-        ptr_vector<expr>& todo = m_relevant_todo;
-        bool_vector& visited = m_relevant_visited;
-        auto const& core = m_dual_solver->core();
-        todo.reset();
-        for (auto lit : core) {
-            expr* e = m_bool_var2expr.get(lit.var(), nullptr);
-            if (e)
-                todo.push_back(e);
-        }
-#if 0
-        std::cout << "init-relevant\n";
-        for (expr* e : m_auto_relevant)
-            std::cout << "auto-relevant " << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
-#endif
-        todo.append(m_auto_relevant);
-        for (unsigned i = 0; i < todo.size(); ++i) {
-            expr* e = todo[i];
-            if (visited.get(e->get_id(), false))
-                continue;
-            visited.setx(e->get_id(), true, false);
-            if (!si.is_bool_op(e)) 
-                m_relevant_expr_ids.setx(e->get_id(), true, false);
-            if (!is_app(e))
-                continue;
-            expr* c = nullptr, *th = nullptr, *el = nullptr;
-            if (m.is_ite(e, c, th, el) && get_enode(c)) {
-                sat::literal lit = expr2literal(c);
-                todo.push_back(c);
-                switch (s().value(lit)) {
         case l_true:
-                    todo.push_back(th);
+            set_asserted(lit);
             break;
         case l_false:
-                    todo.push_back(el);
+            set_asserted(~lit);
+            break;
+        }
+    }
+
+    void relevancy::asserted(sat::literal lit) {
+        TRACE("relevancy", tout << "asserted " << lit << " relevant " << is_relevant(lit) << "\n");
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(lit)) {
+            add_to_propagation_queue(lit);
+            return;
+        }
+        if (ctx.s().lvl(lit) <= ctx.s().search_lvl()) {
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
+            return;
+        }
+
+        for (auto idx : occurs(lit)) {
+            if (!m_roots[idx])
+                continue;
+            for (sat::literal lit2 : *m_clauses[idx]) 
+                if (lit2 != lit && ctx.s().value(lit2) == l_true && is_relevant(lit2))
+                    goto next;  
+            set_relevant(lit);
+            add_to_propagation_queue(lit);
+            return;
+        next:
+            ;
+        }
+    }
+
+    void relevancy::propagate() {
+        if (!m_enabled)
+            return;
+        flush();
+        if (m_qhead == m_queue.size())
+            return;
+        m_trail.push_back(std::make_pair(update::set_qhead, m_qhead));
+        while (m_qhead < m_queue.size() && !ctx.s().inconsistent() && ctx.get_manager().inc()) {
+            auto const& [lit, n] = m_queue[m_qhead++];
+            SASSERT(n || lit != sat::null_literal);
+            SASSERT(!n || lit == sat::null_literal);
+            if (n)
+                propagate_relevant(n);
+            else 
+                propagate_relevant(lit);            
+        }
+    }
+
+    void relevancy::merge(euf::enode* root, euf::enode* other) {
+        TRACE("relevancy", tout << "merge #" << ctx.bpp(root) << " " << is_relevant(root) << " #" << ctx.bpp(other) << " " << is_relevant(other) << "\n");
+        if (is_relevant(root))
+            mark_relevant(other);
+        else if (is_relevant(other))
+            mark_relevant(root);
+    }
+    
+    void relevancy::mark_relevant(euf::enode* n) {
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(n))
+            return;
+        TRACE("relevancy", tout << "mark #" << ctx.bpp(n) << "\n");
+        m_trail.push_back(std::make_pair(update::add_queue, 0));
+        m_queue.push_back(std::make_pair(sat::null_literal, n));
+    }
+
+    void relevancy::mark_relevant(sat::literal lit) {
+        TRACE("relevancy", tout << "mark " << lit << " " << is_relevant(lit) << " " << ctx.s().value(lit) << " lim: " << m_lim.size() << "\n");
+        if (!m_enabled)
+            return;
+        flush();
+        if (is_relevant(lit))
+            return;        
+        set_relevant(lit);
+        switch (ctx.s().value(lit)) {
+        case l_true:
+            break;
+        case l_false:
+            lit.neg();
             break;
         default:
-                    todo.push_back(th);
+            return;               
-                    todo.push_back(el);
-                    break;
         }
+        add_to_propagation_queue(lit);
+    }
+
+    void relevancy::propagate_relevant(sat::literal lit) {
+        SASSERT(m_num_scopes == 0);
+        TRACE("relevancy", tout << "propagate " << lit << " lim: " << m_lim.size() << "\n");
+        SASSERT(ctx.s().value(lit) == l_true);
+        SASSERT(is_relevant(lit));
+        euf::enode* n = ctx.bool_var2enode(lit.var());
+        if (n && !ctx.get_si().is_bool_op(n->get_expr()))
+            return;
+        for (auto idx : occurs(~lit)) {
+            if (m_roots[idx])
                 continue;
+            sat::clause* cl = m_clauses[idx];
+            sat::literal true_lit = sat::null_literal;
+            for (sat::literal lit2 : *cl) {
+                if (ctx.s().value(lit2) == l_true) {
+                    if (is_relevant(lit2))
+                        goto next;
+                    true_lit = lit2;
                 }
-            for (expr* arg : *to_app(e))
-                todo.push_back(arg);
             }
 
-        for (auto * e : todo)
+            if (true_lit != sat::null_literal) 
-            visited[e->get_id()] = false;
+                set_asserted(true_lit);            
+            else {
+                m_trail.push_back(std::make_pair(update::set_root, idx));
+                m_roots[idx] = true;
+            }
+        next:
+            TRACE("relevancy", tout << "propagate " << lit << " " << true_lit << " " << m_roots[idx] << "\n");
+            ;
+        }
+    }
 
-        TRACE("euf",
+    void relevancy::propagate_relevant(euf::enode* n) {
-            for (enode* n : m_egraph.nodes())
+        m_todo.push_back(n);
-                if (is_relevant(n)) 
+        while (!m_todo.empty()) {
-                    tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";);
+            n = m_todo.back();
-              return true;
+            m_todo.pop_back();
+            TRACE("relevancy", tout << "propagate #" << ctx.bpp(n) << " lim: " << m_lim.size() << "\n");
+            if (n->is_relevant())
+                continue;
+            m_stack.push_back(n);
+            while (!m_stack.empty()) {
+                n = m_stack.back();
+                unsigned sz = m_stack.size();
+                bool is_bool_op = ctx.get_si().is_bool_op(n->get_expr());
+                if (!is_bool_op)
+                    for (euf::enode* arg : euf::enode_args(n))
+                        if (!arg->is_relevant())
+                            m_stack.push_back(arg);
+                if (sz != m_stack.size())
+                    continue;
+                if (!n->is_relevant()) {
+                    ctx.get_egraph().set_relevant(n);
+                    ctx.relevant_eh(n);
+                    sat::bool_var v = n->bool_var();                    
+                    if (v != sat::null_bool_var)
+                        relevant_eh(v);
+                    for (euf::enode* sib : euf::enode_class(n))
+                        if (!sib->is_relevant())
+                            m_todo.push_back(sib);
+                }
+                if (!ctx.get_manager().inc()) {
+                    m_todo.reset();
+                    m_stack.reset();
+                    return;
+                }
+                m_stack.pop_back();
             }
         }
+    }
+
+    void relevancy::set_enabled(bool e) {
+        m_enabled = e;
+        ctx.get_egraph().set_default_relevant(!e);
+    }
+
+}

src/sat/smt/euf_relevancy.h

@@ -0,0 +1,173 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    smt_relevant.h
+
+Abstract:
+
+    Relevancy propagation
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-12-27
+
+
+Clauses are split into two parts:
+
+- Roots
+- Defs
+
+The goal is to establish a labeling of literals as "relevant" such that
+- the set of relevant literals satisfies Roots
+- there is a set of blocked literals that can be used to satisfy the clauses in Defs
+  independent of their real assignment.
+
+The idea is that the Defs clauses are obtained from Tseitin transformation so they can be
+grouped by the blocked literal that was used to introduce them.
+For example, when clausifying (and a b) we have the clauses
+(=> (and a b) a)
+(=> (and a b) b)
+(or (not a) (not b) (and a b))
+then the literal for "(and a b)" is blocked.
+And recursively for clauses introduced for a, b if they use a Boolean connectives
+at top level.
+
+The state transitions are:
+
+- A literal lit is assigned:
+  lit appears positively in a Root clause R and no other literal in R are relevant.
+  ->
+  lit is set relevant
+
+  lit is justified at search level
+  -> 
+  lit is set relevant
+
+- An equality n1 = n2 is assigned:
+  n1 is relevant
+  -> 
+  n2 is marked as relevant
+
+- A lit is set relevant:
+  -> 
+  all clauses D in Defs where lit appears negatively are added to Roots
+
+- When a clause R is added to Roots:
+  R contains a positive literal lit that is relevant
+  ->
+  skip adding R to Roots
+
+- When a clause R is added to Roots:
+  R contains a positive literal lit, no positive literal in R are relevant
+  ->
+  lit is set relevant 
+
+- When a clause D is added to Defs:
+  D contains a negative literal that is relevant
+  -> 
+  Add D to Roots
+
+- When an expression is set relevant:
+  All non-relevant children above Boolean connectives are set relevant
+  If nodes are treated as Boolean connectives because they are clausified
+  to (=> cond (= n then)) and (=> (not cond) (= n else))
+
+Replay:
+  - literals that are replayed in clauses that are marked relevant are 
+    marked relevant again.
+
+  - expressions corresponding to auxiliary clauses are added as auxiliary clauses.
+  
+  - TBD: Are root clauses added under a scope discarded?
+    The SAT solver re-initializes clauses on its own, should we just use this mechanism?
+
+Can a literal that is not in a root be set relevant?
+ - yes, if we propagate over expressions
+
+Do we need full watch lists instead of 2-watch lists?
+ - probably, but unclear. The dual SAT solver only uses 2-watch lists, but uses a large clause for tracking 
+   roots.
+
+
+   State machine for literals: relevant(lit), assigned(lit)
+
+relevant(lit) transitions false -> true
+   if assigned(lit):     add to propagation queue
+   if not assigned(lit): no-op (or mark enodes as relevant)
+
+assigned(lit) transitions false -> true
+   if relevant(lit):      add to propagation queue
+   if not relevant(lit):  set relevant if member of root, add to propagation queue
+
+
+--*/
+#pragma once
+#include "sat/sat_solver.h"
+#include "sat/smt/sat_th.h"
+
+
+namespace euf {
+
+    class solver;
+
+    class relevancy {
+        euf::solver&         ctx;
+
+        enum class update { relevant_var, add_queue, add_clause, set_root, set_qhead };
+       
+        bool                                 m_enabled = false;
+        svector<std::pair<update, unsigned>> m_trail;
+        unsigned_vector                      m_lim;
+        unsigned                             m_num_scopes = 0;
+        bool_vector                          m_relevant_var_ids;  // identifiers of relevant Boolean variables
+        sat::clause_allocator                m_alloc;
+        sat::clause_vector                   m_clauses;           // clauses
+        bool_vector                          m_roots;             // indicate if clause is a root
+        vector<unsigned_vector>              m_occurs;            // where do literals occur
+        unsigned                             m_qhead = 0;         // queue head for relevancy
+        svector<std::pair<sat::literal, euf::enode*>> m_queue;    // propagation queue for relevancy
+        euf::enode_vector                    m_stack, m_todo;
+
+        void push_core() { m_lim.push_back(m_trail.size()); }
+        void flush() { for (; m_num_scopes > 0; --m_num_scopes) push_core(); }
+
+        unsigned_vector& occurs(sat::literal lit) { m_occurs.reserve(lit.index() + 1); return m_occurs[lit.index()]; }
+
+        void propagate_relevant(sat::literal lit);
+
+        void add_to_propagation_queue(sat::literal lit);        
+
+        void set_relevant(sat::literal lit);
+
+        void set_asserted(sat::literal lit);
+
+        void relevant_eh(sat::bool_var v);
+
+        void propagate_relevant(euf::enode* n);
+
+    public:
+        relevancy(euf::solver& ctx): ctx(ctx) {}
+
+        void push() { if (m_enabled) ++m_num_scopes; }
+        void pop(unsigned n);
+
+        void add_root(unsigned n, sat::literal const* lits);
+        void add_def(unsigned n, sat::literal const* lits);
+        void asserted(sat::literal lit);
+        void propagate();
+        bool can_propagate() const { return m_qhead < m_queue.size(); }
+
+        void mark_relevant(euf::enode* n);
+        void mark_relevant(sat::literal lit);
+        void merge(euf::enode* n1, euf::enode* n2);
+
+        bool is_relevant(sat::bool_var v) const { return !m_enabled || m_relevant_var_ids.get(v, false); }
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
+        bool is_relevant(euf::enode* n) const { return !m_enabled || n->is_relevant(); }
+        
+        bool enabled() const { return m_enabled; }
+        void set_enabled(bool e);
+    };
+}

src/sat/smt/euf_solver.cpp

@@ -41,6 +41,7 @@ namespace euf {
         extension(symbol("euf"), m.mk_family_id("euf")),
         m(m),
         si(si),
+        m_relevancy(*this),
         m_egraph(m),
         m_trail(),
         m_rewriter(m),
@@ -51,12 +52,21 @@ namespace euf {
         m_values(m)
     {
         updt_params(p);
+        m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);
 
         std::function<void(std::ostream&, void*)> disp =
             [&](std::ostream& out, void* j) { 
             display_justification_ptr(out, reinterpret_cast<size_t*>(j)); 
         };
         m_egraph.set_display_justification(disp);
+
+        if (m_relevancy.enabled()) {
+            std::function<void(euf::enode* root, euf::enode* other)> on_merge =
+                [&](enode* root, enode* other) {
+                m_relevancy.merge(root, other);
+            };
+            m_egraph.set_on_merge(on_merge);
+        }
     }
 
     void solver::updt_params(params_ref const& p) {
@@ -183,7 +193,7 @@ namespace euf {
     }
 
     void solver::propagate(literal lit, ext_justification_idx idx) {
-        add_auto_relevant(bool_var2expr(lit.var()));
+        mark_relevant(lit);
         s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
     }
 
@@ -286,6 +296,11 @@ namespace euf {
     }
 
     void solver::asserted(literal l) {
+
+        m_relevancy.asserted(l);
+        if (!m_relevancy.is_relevant(l))
+            return;        
+
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
         TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
         if (!e) 
@@ -329,6 +344,8 @@ namespace euf {
     bool solver::unit_propagate() {
         bool propagated = false;
         while (!s().inconsistent()) {
+            if (m_relevancy.enabled())
+                m_relevancy.propagate();
             if (m_egraph.inconsistent()) {  
                 unsigned lvl = s().scope_lvl();
                 s().set_conflict(sat::justification::mk_ext_justification(lvl, conflict_constraint().to_index()));
@@ -345,9 +362,13 @@ namespace euf {
                 if (m_solvers[i]->unit_propagate())
                     propagated1 = true;
             
-            if (!propagated1)
+            if (propagated1) {
-                break;
                 propagated = true;
+                continue;
+            }
+            if (m_relevancy.enabled() && m_relevancy.can_propagate())
+                continue;
+            break;                  
         }
         DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation(););
         return propagated;
@@ -422,12 +443,10 @@ namespace euf {
     void solver::propagate_th_eqs() {
         for (; m_egraph.has_th_eq() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_th_eq()) {
             th_eq eq = m_egraph.get_th_eq();
-            if (eq.is_eq()) {
+            if (!eq.is_eq())
-                if (!is_self_propagated(eq))
-                    m_id2solver[eq.id()]->new_eq_eh(eq);    
-            }
-            else
                 m_id2solver[eq.id()]->new_diseq_eh(eq);
+            else if (!is_self_propagated(eq))
+                m_id2solver[eq.id()]->new_eq_eh(eq);                                
         }
     }
 
@@ -459,9 +478,6 @@ namespace euf {
         if (unit_propagate())
             return sat::check_result::CR_CONTINUE;
         
-        if (!init_relevancy())
-            give_up = true;
-        
         unsigned num_nodes = m_egraph.num_nodes();
         auto apply_solver = [&](th_solver* e) {
             switch (e->check()) {
@@ -525,9 +541,7 @@ namespace euf {
         for (auto* e : m_solvers)
             e->push();
         m_egraph.push();
-        if (m_dual_solver)
+        m_relevancy.push();
-            m_dual_solver->push();
-        push_relevant();
     }
 
     void solver::pop(unsigned n) {
@@ -537,7 +551,7 @@ namespace euf {
             e->pop(n);
         si.pop(n);
         m_egraph.pop(n);
-        pop_relevant(n);
+        m_relevancy.pop(n);
         scope const & sc = m_scopes[m_scopes.size() - n];
         for (unsigned i = m_var_trail.size(); i-- > sc.m_var_lim; ) {
             bool_var v = m_var_trail[i];
@@ -546,8 +560,6 @@ namespace euf {
         }
         m_var_trail.shrink(sc.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
-        if (m_dual_solver)
-            m_dual_solver->pop(n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
         TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
     }
@@ -720,6 +732,35 @@ namespace euf {
         }
     }
 
+    bool solver::is_relevant(bool_var v) const {
+        if (m_relevancy.enabled())
+            return m_relevancy.is_relevant(v);
+        auto* e = bool_var2enode(v);
+        return !e || is_relevant(e);
+    }
+
+    void solver::relevant_eh(euf::enode* n) {
+        if (m_qsolver)
+            m_qsolver->relevant_eh(n);
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && th != m_qsolver)
+                th->relevant_eh(n);
+        }       
+    }
+
+    bool solver::enable_ackerman_axioms(expr* e) const {
+        euf::enode* n = get_enode(e);
+        if (!n)
+            return false;
+        for (auto const& thv : enode_th_vars(n)) {
+            auto* th = m_id2solver.get(thv.get_id(), nullptr);
+            if (th && !th->enable_ackerman_axioms(n))
+                return false;
+        }
+        return true;
+    }
+
     void solver::pre_simplify() {
         for (auto* e : m_solvers)
             e->pre_simplify();
@@ -765,6 +806,8 @@ namespace euf {
     }
 
     bool solver::set_root(literal l, literal r) {
+        if (m_relevancy.enabled())
+            return false;
         expr* e = bool_var2expr(l.var());
         if (!e)
             return true;
@@ -794,7 +837,7 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             expr* e = m_bool_var2expr[v];
-            out << v << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
+            out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);

src/sat/smt/euf_solver.h

@@ -25,11 +25,12 @@ Author:
 #include "sat/sat_extension.h"
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_th.h"
-#include "sat/smt/sat_dual_solver.h"
 #include "sat/smt/euf_ackerman.h"
 #include "sat/smt/user_solver.h"
+#include "sat/smt/euf_relevancy.h"
 #include "smt/params/smt_params.h"
 
+
 namespace euf {
     typedef sat::literal literal;
     typedef sat::ext_constraint_idx ext_constraint_idx;
@@ -91,6 +92,7 @@ namespace euf {
         std::function<::solver*(void)>   m_mk_solver;
         ast_manager&                     m;
         sat::sat_internalizer& si;
+        relevancy              m_relevancy;
         smt_params             m_config;
         euf::egraph            m_egraph;
         trail_stack            m_trail;
@@ -181,18 +183,18 @@ namespace euf {
         void init_drat();
 
         // relevancy
-        bool_vector m_relevant_expr_ids;
+        //bool_vector m_relevant_expr_ids;
-        bool_vector m_relevant_visited;
+        //bool_vector m_relevant_visited;
-        ptr_vector<expr> m_relevant_todo;
+        //ptr_vector<expr> m_relevant_todo;
-        void ensure_dual_solver();
+        //void init_relevant_expr_ids();
-        bool init_relevancy();
+        //void push_relevant(sat::bool_var v);
-
+        bool is_propagated(sat::literal lit);
-
         // invariant
         void check_eqc_bool_assignment() const;
         void check_missing_bool_enode_propagation() const;
         void check_missing_eq_propagation() const;
         
+
         // diagnosis
         std::ostream& display_justification_ptr(std::ostream& out, size_t* j) const;
 
@@ -250,6 +252,10 @@ namespace euf {
         sat::sat_internalizer& get_si() { return si; }
         ast_manager& get_manager() { return m; }
         enode* get_enode(expr* e) const { return m_egraph.find(e); }
+        enode* bool_var2enode(sat::bool_var b) const {
+            expr* e = m_bool_var2expr.get(b, nullptr);
+            return e ? get_enode(e) : nullptr;
+        }
         sat::literal expr2literal(expr* e) const { return enode2literal(get_enode(e)); }
         sat::literal enode2literal(enode* n) const { return sat::literal(n->bool_var(), false); }
         lbool value(enode* n) const { return s().value(enode2literal(n)); }
@@ -362,32 +368,28 @@ namespace euf {
         th_rewriter& get_rewriter() { return m_rewriter; }
         void rewrite(expr_ref& e) { m_rewriter(e); }
         bool is_shared(euf::enode* n) const;
+        bool enable_ackerman_axioms(expr* n) const;
 
         // relevancy
-        bool m_relevancy = true;
-        scoped_ptr<sat::dual_solver>  m_dual_solver;
-        ptr_vector<expr>              m_auto_relevant;
-        unsigned_vector               m_auto_relevant_lim;
-        unsigned                      m_auto_relevant_scopes = 0;
 
-        bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; }
+        bool relevancy_enabled() const { return m_relevancy.enabled(); }
-        void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false;  }
+        void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy.set_enabled(false); }
-        void add_root(unsigned n, sat::literal const* lits);
+        void add_root(unsigned n, sat::literal const* lits) { m_relevancy.add_root(n, lits); }
         void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
         void add_root(sat::literal lit) { add_root(1, &lit); }
-        void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
+        void add_root(sat::literal lit1, sat::literal lit2) { sat::literal lits[2] = { lit1, lit2, }; add_root(2, lits); }
         void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
-        void add_aux(unsigned n, sat::literal const* lits);
+        void add_aux(unsigned n, sat::literal const* lits) { m_relevancy.add_def(n, lits); }
         void add_aux(sat::literal a) { sat::literal lits[1] = { a }; add_aux(1, lits); }
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
         void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
-        void track_relevancy(sat::bool_var v);
+        void mark_relevant(sat::literal lit) { m_relevancy.mark_relevant(lit); }
-        bool is_relevant(expr* e) const;
+        bool is_relevant(enode* n) const { return m_relevancy.is_relevant(n); }
-        bool is_relevant(enode* n) const;
+        bool is_relevant(bool_var v) const;
-        void add_auto_relevant(expr* e);
+        bool is_relevant(sat::literal lit) const { return is_relevant(lit.var()); }
-        void pop_relevant(unsigned n);
+        void relevant_eh(euf::enode* n);
-        void push_relevant();
 
+        relevancy& get_relevancy() { return m_relevancy; }
 
         // model construction
         void update_model(model_ref& mdl);

src/sat/smt/fpa_solver.cpp

@@ -269,7 +269,7 @@ namespace fpa {
         expr* xe = e_x->get_expr();
         expr* ye = e_y->get_expr();
 
-        if (m_fpa_util.is_bvwrap(xe) || m_fpa_util.is_bvwrap(ye))
+        if (fu.is_bvwrap(xe) || fu.is_bvwrap(ye))
             return;
 
         expr_ref xc = convert(xe);

src/sat/smt/pb_solver.cpp

@@ -2006,7 +2006,7 @@ namespace pb {
             s().pop_to_base_level();
         if (s().inconsistent())
             return;
-        unsigned trail_sz, count = 0;
+        unsigned trail_sz = 0, count = 0;
         do {
             trail_sz = s().init_trail_size();
             m_simplify_change = false;

src/sat/smt/q_ematch.cpp

@@ -69,10 +69,16 @@ namespace q {
             m_mam->add_node(n, false);
         };
         ctx.get_egraph().set_on_merge(_on_merge);
+        if (!ctx.relevancy_enabled())
             ctx.get_egraph().set_on_make(_on_make);
         m_mam = mam::mk(ctx, *this);
     }
 
+    void ematch::relevant_eh(euf::enode* n) {
+        if (ctx.relevancy_enabled())
+            m_mam->add_node(n, false);
+    }
+
     void ematch::ensure_ground_enodes(expr* e) {
         mam::ground_subterms(e, m_ground);
         for (expr* g : m_ground) 
@@ -352,7 +358,7 @@ namespace q {
         if (m_prop_queue.empty())
             return false;
         for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
-            auto [is_conflict, idx, j_idx] = m_prop_queue[i];
+            auto const& [is_conflict, idx, j_idx] = m_prop_queue[i];
             propagate(is_conflict, idx, j_idx);
         }
         m_prop_queue.reset();
@@ -581,7 +587,7 @@ namespace q {
             return m_inst_queue.propagate() || propagated;
         ctx.push(value_trail<unsigned>(m_qhead));
         ptr_buffer<binding> to_remove;
-        for (; m_qhead < m_clause_queue.size(); ++m_qhead) {
+        for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) {
             unsigned idx = m_clause_queue[m_qhead];
             clause& c = *m_clauses[idx];
             binding* b = c.m_bindings;

src/sat/smt/q_ematch.h

@@ -135,9 +135,10 @@ namespace q {
 
         bool unit_propagate();        
 
-
         void add(quantifier* q);
 
+        void relevant_eh(euf::enode* n);
+
         void collect_statistics(statistics& st) const;
 
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing);

src/sat/smt/q_mam.cpp

@@ -424,15 +424,19 @@ namespace q {
         friend class compiler;
         friend class code_tree_manager;
 
-        void display_seq(std::ostream & out, instruction * head, unsigned indent) const {
+        void spaces(std::ostream& out, unsigned indent) const {
-            for (unsigned i = 0; i < indent; i++) {
+            for (unsigned i = 0; i < indent; i++) 
                 out << "    ";
         }
+
+        void display_seq(std::ostream & out, instruction * head, unsigned indent) const {
+            spaces(out, indent);
             instruction * curr = head;
             out << *curr;
             curr = curr->m_next;
             while (curr != nullptr && curr->m_opcode != CHOOSE && curr->m_opcode != NOOP) {
                 out << "\n";
+                spaces(out, indent);
                 out << *curr;
                 curr = curr->m_next;
             }
@@ -598,7 +602,7 @@ namespace q {
                 ast_manager & m = m_egraph->get_manager();
                 out << "patterns:\n";
                 for (auto [q, a] : m_patterns) 
-                    out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
+                    out << q->get_id() << ": " << mk_pp(q, m) << " " << mk_pp(a, m) << "\n";
             }
 #endif
             out << "function: " << m_root_lbl->get_name();
@@ -2878,8 +2882,10 @@ namespace q {
                 if (tree->expected_num_args() == p->get_num_args()) 
                     m_compiler.insert(tree, qa, mp, first_idx, false);
             }
-            DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
+            DEBUG_CODE(if (first_idx == 0) {
-                       ctx.push(push_back_trail<std::pair<quantifier*,app*>, false>(m_trees[lbl_id]->get_patterns())););
+                m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp));
+                ctx.push(push_back_trail<std::pair<quantifier*, app*>, false>(m_trees[lbl_id]->get_patterns()));
+            });
             TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
         }
 

src/sat/smt/q_mbi.cpp

@@ -51,7 +51,7 @@ namespace q {
         m_instantiations.reset();
         for (sat::literal lit : m_qs.m_universal) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
-            if (!ctx.is_relevant(q))
+            if (!ctx.is_relevant(lit.var()))
                 continue;
             init_model();
             switch (check_forall(q)) {
@@ -67,11 +67,10 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto [qlit, fml, generation] : m_instantiations) {
+        for (auto const& [qlit, fml, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
             sat::literal lit = ctx.mk_literal(fml);
             m_qs.add_clause(~qlit, ~lit);
-            ctx.add_root(~qlit, ~lit);
         }
         m_instantiations.reset();
         return result;
@@ -130,7 +129,7 @@ namespace q {
                 r = n;
             }
             else if (n->generation() == gen) {
-                if ((++count) % m_qs.random() == 0)
+                if ((m_qs.random() % ++count) == 0)
                     r = n;
             }
             if (count > m_max_choose_candidates)
@@ -309,8 +308,10 @@ namespace q {
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;
             }
-            if (p)
+            if (!p)
-                (*p)(*m_model, vars, fmls);
+                continue;
+            if (!(*p)(*m_model, vars, fmls))
+                return expr_ref(nullptr, m);
         }
         for (app* v : vars) {
             expr_ref term(m);

src/sat/smt/q_model_fixer.cpp

@@ -66,7 +66,7 @@ namespace q {
         ptr_vector<quantifier> univ;
         for (sat::literal lit : m_qs.universal()) {
             quantifier* q = to_quantifier(ctx.bool_var2expr(lit.var()));
-            if (ctx.is_relevant(q))
+            if (ctx.is_relevant(lit.var()))
                 univ.push_back(q);
         }
         if (univ.empty())
@@ -256,7 +256,7 @@ namespace q {
               tout << "invert-app " << mk_pp(t, m) << " = " << mk_pp(value, m) << "\n";
               if (v2r.find(value, r)) 
                   tout << "inverse " << mk_pp(r->get_expr(), m) << "\n";
-              ctx.display(tout);              
+              /*ctx.display(tout); */
               );
         if (v2r.find(value, r)) 
             return r->get_expr();

src/sat/smt/q_queue.cpp

@@ -149,12 +149,7 @@ namespace q {
         if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
             return;
 
-#if 0
+
-        std::cout << mk_pp(q, m) << "\n";
-        std::cout << num_bindings << "\n";
-        for (unsigned i = 0; i < num_bindings; ++i)
-            std::cout << mk_pp(f[i]->get_expr(), m) << " " << mk_pp(f[i]->get_sort(), m) << "\n";
-#endif
         auto* ebindings = m_subst(q, num_bindings);
         for (unsigned i = 0; i < num_bindings; ++i)
             ebindings[i] = f[i]->get_expr();
@@ -168,6 +163,14 @@ namespace q {
 
         m_stats.m_num_instances++;
 
+#if 0
+        std::cout << "instantiate\n";
+        for (unsigned i = 0; i < num_bindings; ++i)
+            std::cout << ctx.bpp(f[i]) << " ";
+        std::cout << "\n";
+        std::cout << mk_pp(q, m) << "\n";
+#endif
+
 //        f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") <<  "\n";
 
         

src/sat/smt/q_solver.cpp

@@ -44,19 +44,16 @@ namespace q {
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
         }
         else if (expand(q)) {
             for (expr* e : m_expanded) {
                 sat::literal lit = ctx.internalize(e, l.sign(), false, false);
                 add_clause(~l, lit);
-                ctx.add_root(~l, lit);
             }
         }
         else if (is_ground(q->get_expr())) {
             auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
             add_clause(~l, lit);
-            ctx.add_root(~l, lit);
         }
         else {
             ctx.push_vec(m_universal, l);

src/sat/smt/q_solver.h

@@ -83,6 +83,7 @@ namespace q {
         void init_search() override;
         void finalize_model(model& mdl) override;
         bool is_shared(euf::theory_var v) const override { return true; }
+        void relevant_eh(euf::enode* n) override { m_ematch.relevant_eh(n); }
 
         ast_manager& get_manager() { return m; }
         sat::literal_vector const& universal() const { return m_universal; }

src/sat/smt/recfun_solver.cpp

@@ -68,8 +68,8 @@ namespace recfun {
         TRACEFN("case expansion " << e);
         SASSERT(e.m_def->is_fun_macro());
         auto & vars = e.m_def->get_vars();
-        auto lhs = e.m_lhs;
+        app_ref lhs = e.m_lhs;
-        auto rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
+        expr_ref rhs = apply_args(vars, e.m_args, e.m_def->get_rhs());
         unsigned generation = std::max(ctx.get_max_generation(lhs), ctx.get_max_generation(rhs));
         euf::solver::scoped_generation _sgen(ctx, generation + 1);
         auto eq = eq_internalize(lhs, rhs);

src/sat/smt/sat_dual_solver.cpp

@@ -1,185 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    sat_dual_solver.cpp
-
-Abstract:
-
-    Solver for obtaining implicant.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-#include "sat/smt/sat_dual_solver.h"
-
-namespace sat {
-
-    dual_solver::dual_solver(reslimit& l):
-        m_solver(m_params, l)
-    {
-        SASSERT(!m_solver.get_config().m_drat);
-        m_solver.set_incremental(true);
-    }
-
-    void dual_solver::flush() {
-        while (m_num_scopes > 0) {
-            m_solver.user_push();
-            m_roots.push_scope();
-            m_tracked_vars.push_scope();
-            m_units.push_scope();
-            m_vars.push_scope();
-            --m_num_scopes;
-        }
-    }
-
-    void dual_solver::push() {
-        ++m_num_scopes;
-    }
-
-    void dual_solver::pop(unsigned num_scopes) {        
-        if (m_num_scopes >= num_scopes) {
-            m_num_scopes -= num_scopes;
-            return;
-        }
-        num_scopes -= m_num_scopes;
-        m_num_scopes = 0;
-        m_solver.user_pop(num_scopes);
-        unsigned old_sz = m_tracked_vars.old_size(num_scopes);
-        for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
-            m_is_tracked[m_tracked_vars[i]] = false; 
-        old_sz = m_vars.old_size(num_scopes);
-        for (unsigned i = m_vars.size(); i-- > old_sz; ) {
-            unsigned v = m_vars[i];
-            unsigned w = m_ext2var[v];
-            m_ext2var[v] = null_bool_var;
-            m_var2ext[w] = null_bool_var;
-        }
-        m_vars.pop_scope(num_scopes);
-        m_units.pop_scope(num_scopes);
-        m_roots.pop_scope(num_scopes);
-        m_tracked_vars.pop_scope(num_scopes);
-    }
-
-    bool_var dual_solver::ext2var(bool_var v) {
-        bool_var w = m_ext2var.get(v, null_bool_var);
-        if (null_bool_var == w) {
-            w = m_solver.mk_var();
-            m_solver.set_external(w);
-            m_ext2var.setx(v, w, null_bool_var);
-            m_var2ext.setx(w, v, null_bool_var);
-            m_vars.push_back(v);
-        }
-        return w;
-    }
-
-    void dual_solver::track_relevancy(bool_var w) {
-        flush();
-        bool_var v = ext2var(w);
-        if (!m_is_tracked.get(v, false)) {
-            m_is_tracked.setx(v, true, false);
-            m_tracked_vars.push_back(v);
-        }
-    }
-
-    literal dual_solver::ext2lit(literal lit) {
-        return literal(ext2var(lit.var()), lit.sign());
-    }
-
-    literal dual_solver::lit2ext(literal lit) {
-        return literal(m_var2ext[lit.var()], lit.sign());
-    }
-
-    void dual_solver::add_root(unsigned sz, literal const* clause) {      
-        flush();
-        if (false && sz == 1) {
-            TRACE("dual", tout << "unit: " << clause[0] << "\n";);
-            m_units.push_back(clause[0]);
-            return;
-        }
-        literal root;
-        if (sz == 1) 
-            root = ext2lit(clause[0]);
-        else {
-            root = literal(m_solver.mk_var(), false);
-            for (unsigned i = 0; i < sz; ++i)
-                m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
-        }        
-        m_solver.set_external(root.var());
-        m_roots.push_back(~root);
-        TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
-    }
-
-    void dual_solver::add_aux(unsigned sz, literal const* clause) {
-        flush();        
-        m_lits.reset();
-        for (unsigned i = 0; i < sz; ++i) 
-            m_lits.push_back(ext2lit(clause[i]));
-        TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";);
-        m_solver.mk_clause(sz, m_lits.data(), status::input());
-    }
-
-    void dual_solver::add_assumptions(solver const& s) {
-        flush();
-        m_lits.reset();
-        for (bool_var v : m_tracked_vars)
-            m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
-        for (auto lit : m_units) {
-            bool_var w = m_ext2var.get(lit.var(), null_bool_var);
-            if (w != null_bool_var)
-                m_lits.push_back(ext2lit(lit));            
-        }
-    }
-
-    bool dual_solver::operator()(solver const& s) {        
-        m_core.reset();
-        m_core.append(m_units);
-        if (m_roots.empty())
-            return true;
-        m_solver.user_push();
-        m_solver.add_clause(m_roots.size(), m_roots.data(), status::input());
-        add_assumptions(s);
-        lbool is_sat = m_solver.check(m_lits.size(), m_lits.data());
-        if (is_sat == l_false) 
-            for (literal lit : m_solver.get_core())
-                m_core.push_back(lit2ext(lit));        
-        if (is_sat == l_true) {
-            TRACE("dual", display(s, tout); s.display(tout););
-            IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
-            UNREACHABLE();
-            return false;
-        }
-        TRACE("dual", m_solver.display(tout << "is-sat: " << is_sat << " core: " << m_core << "\n"););
-        m_solver.user_pop(1);
-        return is_sat == l_false;
-    }
-
-    std::ostream& dual_solver::display(solver const& s, std::ostream& out) const {        
-        for (unsigned v = 0; v < m_solver.num_vars(); ++v) {
-            bool_var w = m_var2ext.get(v, null_bool_var);
-            if (w == null_bool_var)
-                continue;
-            lbool v1 = m_solver.value(v);
-            lbool v2 = s.value(w);
-            if (v1 == v2 || v2 == l_undef)
-                continue;
-            out << "ext: " << w << " " << v2 << "\n";
-            out << "int: " << v << " " << v1 << "\n";
-        }
-        literal_vector lits;
-        for (bool_var v : m_tracked_vars) 
-            lits.push_back(literal(m_var2ext[v], l_false == s.value(m_var2ext[v])));
-        out << "tracked: " << lits << "\n";  
-        lits.reset();
-        for (literal r : m_roots) 
-            if (m_solver.value(r) == l_true)
-                lits.push_back(r);
-        out << "roots: " << lits << "\n";
-        m_solver.display(out);
-
-        return out;
-    }
-}

src/sat/smt/sat_dual_solver.h

@@ -1,83 +0,0 @@
-/*++
-Copyright (c) 2020 Microsoft Corporation
-
-Module Name:
-
-    sat_dual_solver.h
-
-Abstract:
-
-    Solver for obtaining implicant.
-    Based on an idea by Armin Biere to use dual propagation 
-    for representation of negated goal.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2020-08-25
-
---*/
-#pragma once
-#include "util/lim_vector.h"
-#include "sat/sat_solver.h"
-
-namespace sat {
-
-    class dual_solver {
-        class dual_params : public no_drat_params {
-        public:
-            dual_params() {
-                set_bool("core.minimize", false);
-            }
-        };
-        dual_params     m_params;
-        solver          m_solver;
-        lim_svector<literal> m_units, m_roots;
-        lim_svector<bool_var> m_tracked_vars;
-        literal_vector  m_lits, m_core;
-        bool_var_vector m_is_tracked;
-        unsigned_vector m_ext2var;
-        unsigned_vector m_var2ext;
-        lim_svector<unsigned> m_vars;
-        unsigned        m_num_scopes = 0;
-        void add_literal(literal lit);
-
-        bool_var ext2var(bool_var v);
-        bool_var var2ext(bool_var v);
-        literal  ext2lit(literal lit);
-        literal  lit2ext(literal lit);
-
-        void add_assumptions(solver const& s);
-
-        std::ostream& display(solver const& s, std::ostream& out) const;
-
-        void flush();
-
-    public:
-        dual_solver(reslimit& l);
-        void push();
-        void pop(unsigned num_scopes);
-
-        /*
-        * track model relevancy for variable 
-        */
-        void track_relevancy(bool_var v);
-
-        /*
-        * Add a root clause from the input problem.
-        * At least one literal has to be satisfied in every root.
-        */
-        void add_root(unsigned sz, literal const* clause);
-
-        /*
-        * Add auxiliary clauses that originate from compiling definitions.
-        */
-        void add_aux(unsigned sz, literal const* clause);
-
-        /*
-        * Extract a minimized subset of relevant literals from a model for s.
-        */
-        bool operator()(solver const& s);
-
-        literal_vector const& core() const { return m_core; }
-    };
-}

src/sat/smt/sat_th.cpp

@@ -132,6 +132,7 @@ namespace euf {
     bool th_euf_solver::add_unit(sat::literal lit) {
         bool was_true = is_true(lit);
         ctx.s().add_clause(1, &lit, mk_status());
+        ctx.add_root(lit);
         return !was_true;
     }
 
@@ -144,31 +145,26 @@ namespace euf {
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {      
-        bool was_true = is_true(a, b);
         sat::literal lits[2] = { a, b };
-        ctx.s().add_clause(2, lits, mk_status());
+        return add_clause(2, lits);
-        return !was_true;
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {      
-        bool was_true = is_true(a, b, c);
         sat::literal lits[3] = { a, b, c };
-        ctx.s().add_clause(3, lits, mk_status());
+        return add_clause(3, lits);
-        return !was_true;
     }
 
     bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
-        bool was_true = is_true(a, b, c, d);
         sat::literal lits[4] = { a, b, c, d };
-        ctx.s().add_clause(4, lits, mk_status());
+        return add_clause(4, lits);
-        return !was_true;
     }
 
-    bool th_euf_solver::add_clause(sat::literal_vector const& lits) {
+    bool th_euf_solver::add_clause(unsigned n, sat::literal* lits) {
         bool was_true = false;
-        for (auto lit : lits)
+        for (unsigned i = 0; i < n; ++i)       
-            was_true |= is_true(lit);
+            was_true |= is_true(lits[i]);
-        s().add_clause(lits.size(), lits.data(), mk_status());
+        ctx.add_root(n, lits);
+        s().add_clause(n, lits, mk_status());
         return !was_true;
     }
 

src/sat/smt/sat_th.h

@@ -111,6 +111,10 @@ namespace euf {
 
         virtual void new_diseq_eh(euf::th_eq const& eq) {}
 
+        virtual bool enable_ackerman_axioms(euf::enode* n) const { return true; }
+
+        virtual void relevant_eh(euf::enode* n) {}
+
         /**
            \brief Parametric theories (e.g. Arrays) should implement this method.
         */
@@ -139,7 +143,8 @@ namespace euf {
         bool add_clause(sat::literal a, sat::literal b);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c);
         bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
-        bool add_clause(sat::literal_vector const& lits);
+        bool add_clause(sat::literal_vector const& lits) { return add_clause(lits.size(), lits.data()); }
+        bool add_clause(unsigned n, sat::literal* lits);
         void add_equiv(sat::literal a, sat::literal b);
         void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
 

src/sat/tactic/goal2sat.cpp

@@ -126,20 +126,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         return m_top_level && relevancy_enabled();
     }
     
-    void add_dual_def(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_aux(n, lits);        
-    }
-
-    void add_dual_root(unsigned n, sat::literal const* lits) {
-        if (relevancy_enabled())
-            ensure_euf()->add_root(n, lits);
-    }
-
-    void add_dual_root(sat::literal lit) {
-        add_dual_root(1, &lit);
-    }
-    
     void mk_clause(sat::literal l) {
         mk_clause(1, &l);
     }
@@ -156,7 +142,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_def(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_aux(n, lits);
         m_solver.add_clause(n, lits, mk_status());
     }
 
@@ -176,7 +163,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
 
     void mk_root_clause(unsigned n, sat::literal * lits) {
         TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
-        add_dual_root(n, lits);
+        if (relevancy_enabled())
+            ensure_euf()->add_root(n, lits);
         m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
     }
 
@@ -186,8 +174,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
             return v;
         v = m_solver.add_var(is_ext);
         log_def(v, n);
-        if (top_level_relevant() && !is_bool_op(n))
-            ensure_euf()->track_relevancy(v);
         return v;
     }
 
@@ -216,14 +202,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))  
             v = add_var(true, t);
         m_map.insert(t, v);
-        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) {
-            add_dual_root(sat::literal(v, m.is_false(t)));
-            ensure_euf()->track_relevancy(v);
-        }
         return v;
     }
 
     sat::bool_var add_bool_var(expr* t) override {
+        force_push();
         sat::bool_var v = m_map.to_bool_var(t);
         if (v == sat::null_bool_var) 
             v = mk_bool_var(t);
@@ -677,8 +660,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
         if (lit == sat::null_literal) 
             return;
-        if (top_level_relevant())
-            euf->track_relevancy(lit.var());
         if (root)
             mk_root_clause(lit);
         else

src/sat/tactic/sat_tactic.cpp

@@ -201,8 +201,8 @@ public:
     char const* name() const override { return "sat"; }
 
     void updt_params(params_ref const & p) override {
-        m_params = p;
+        m_params.append(p);
-        if (m_imp) m_imp->updt_params(p);
+        if (m_imp) m_imp->updt_params(m_params);
     }
 
     void collect_param_descrs(param_descrs & r) override {

src/smt/qi_queue.cpp

@@ -226,6 +226,7 @@ namespace smt {
             ebindings[i] = bindings[i]->get_expr();
         expr_ref instance = m_subst();
 
+
         TRACE("qi_queue", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
         TRACE("qi_queue_instance", tout << "new instance:\n" << mk_pp(instance, m) << "\n";);
         expr_ref  s_instance(m);
@@ -244,6 +245,15 @@ namespace smt {
 
             return;
         }
+#if 0
+        std::cout << "instantiate\n";
+        enode_vector _bindings(num_bindings, bindings);
+        for (auto * b : _bindings)
+            std::cout << enode_pp(b, m_context) << " ";
+        std::cout << "\n";
+        std::cout << mk_pp(q, m) << "\n";
+#endif
+   
         TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
         stat->inc_num_instances();
         if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {

src/smt/seq_axioms.h

@@ -73,6 +73,7 @@ namespace smt {
         void add_indexof_axiom(expr* n) { m_ax.indexof_axiom(n); }
         void add_last_indexof_axiom(expr* n) { m_ax.last_indexof_axiom(n); }
         void add_replace_axiom(expr* n) { m_ax.replace_axiom(n); }
+        void add_replace_all_axiom(expr* n) { m_ax.replace_all_axiom(n); }
         void add_at_axiom(expr* n) { m_ax.at_axiom(n); }
         void add_nth_axiom(expr* n) { m_ax.nth_axiom(n); }
         void add_itos_axiom(expr* n) { m_ax.itos_axiom(n); }

src/smt/smt_enode.h

@@ -158,7 +158,6 @@ namespace smt {
 
         void mark_as_interpreted() {
             SASSERT(!m_interpreted);
-            SASSERT(m_owner->get_num_args() == 0);
             SASSERT(m_class_size == 1);
             m_interpreted = true;
         }

src/smt/smt_internalizer.cpp

@@ -974,7 +974,7 @@ namespace smt {
         }
         enode * e           = enode::mk(m, m_region, m_app2enode, n, generation, suppress_args, merge_tf, m_scope_lvl, cgc_enabled, true);
         TRACE("mk_enode_detail", tout << "e.get_num_args() = " << e->get_num_args() << "\n";);
-        if (n->get_num_args() == 0 && m.is_unique_value(n))
+        if (m.is_unique_value(n))
             e->mark_as_interpreted();
         TRACE("mk_var_bug", tout << "mk_enode: " << id << "\n";);
         TRACE("generation", tout << "mk_enode: " << id << " " << generation << "\n";);

src/smt/smt_kernel.h

@@ -307,13 +307,13 @@ namespace smt {
 
         /**
            \brief Return a reference to smt::context.
-           This is a temporary hack to support user theories.
+           This breaks abstractions. 
-           TODO: remove this hack.
-           We need to revamp user theories too.
            
-           This method breaks the abstraction barrier.
+           It is currently used by the opt-solver
+           to access optimization services from arithmetic solvers
+           and to ensure that the solver has registered PB theory solver.
 
-           \warning We should not use this method
+           \warning This method should not be used in new code.
         */
         context & get_context();
     };

src/smt/smt_relevancy.cpp

@@ -134,11 +134,11 @@ namespace smt {
         obj_map<expr, relevancy_ehs *> m_relevant_ehs;
         obj_map<expr, relevancy_ehs *> m_watches[2];
         struct eh_trail {
-            enum kind { POS_WATCH, NEG_WATCH, HANDLER };
+            enum class kind { POS_WATCH, NEG_WATCH, HANDLER };
             kind   m_kind;
             expr * m_node;
-            eh_trail(expr * n):m_kind(HANDLER), m_node(n) {}
+            eh_trail(expr * n):m_kind(kind::HANDLER), m_node(n) {}
-            eh_trail(expr * n, bool val):m_kind(val ? POS_WATCH : NEG_WATCH), m_node(n) {}
+            eh_trail(expr * n, bool val):m_kind(val ? kind::POS_WATCH : kind::NEG_WATCH), m_node(n) {}
             kind get_kind() const { return m_kind; }
             expr * get_node() const { return m_node; }
         };
@@ -292,9 +292,9 @@ namespace smt {
                 expr * n = t.get_node();
                 relevancy_ehs * ehs;
                 switch (t.get_kind()) {
-                case eh_trail::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break;
+                case eh_trail::kind::POS_WATCH: ehs = get_watches(n, true); SASSERT(ehs); set_watches(n, true, ehs->tail()); break;
-                case eh_trail::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break;
+                case eh_trail::kind::NEG_WATCH: ehs = get_watches(n, false); SASSERT(ehs); set_watches(n, false, ehs->tail()); break;
-                case eh_trail::HANDLER:   ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break;
+                case eh_trail::kind::HANDLER:   ehs = get_handlers(n); SASSERT(ehs); set_handlers(n, ehs->tail()); break;
                 default: UNREACHABLE(); break;
                 }
                 m.dec_ref(n);
@@ -378,9 +378,7 @@ namespace smt {
                 break;
             case l_true: {
                 expr * true_arg = nullptr;
-                unsigned num_args = n->get_num_args();
+                for (expr* arg : *n) {
-                for (unsigned i = 0; i < num_args; i++) {
-                    expr * arg  = n->get_arg(i);
                     if (m_context.find_assignment(arg) == l_true) {
                         if (is_relevant_core(arg))
                             return;
@@ -402,9 +400,7 @@ namespace smt {
             switch (val) {
             case l_false: {
                 expr * false_arg = nullptr;
-                unsigned num_args = n->get_num_args();
+                for (expr* arg : *n) {
-                for (unsigned i = 0; i < num_args; i++) {
-                    expr * arg  = n->get_arg(i);
                     if (m_context.find_assignment(arg) == l_false) {
                         if (is_relevant_core(arg))
                             return; 

src/smt/smt_solver.cpp

@@ -125,7 +125,7 @@ namespace {
         smt_params m_smt_params_save;
 
         void push_params() override {
-            m_params_save = params_ref();
+            m_params_save.reset();           
             m_params_save.copy(solver::get_params());
             m_smt_params_save = m_smt_params;
         }

src/smt/tactic/smt_tactic_core.cpp

@@ -127,7 +127,8 @@ public:
 
         scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
             m_params = o.fparams();
-            m_params_ref = o.params();
+            m_params_ref.reset();
+            m_params_ref.append(o.params());
             smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
             TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
             new_ctx->set_logic(o.m_logic);

src/smt/tactic/unit_subsumption_tactic.cpp

@@ -50,7 +50,7 @@ struct unit_subsumption_tactic : public tactic {
     }
 
     void updt_params(params_ref const& p) override {
-        m_params = p;
+        m_params.append(p);
         // m_context.updt_params(p); does not exist.
     }
     

src/smt/theory_seq.cpp

@@ -2646,6 +2646,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_replace(n)) {
         m_ax.add_replace_axiom(n);
     }
+    else if (m_util.str.is_replace_all(n)) {
+        m_ax.add_replace_all_axiom(n);
+    }
     else if (m_util.str.is_extract(n)) {
         m_ax.add_extract_axiom(n);
     }
@@ -3190,6 +3193,7 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_to_code(n) ||
         m_util.str.is_unit(n) ||
         m_util.str.is_length(n) || 
+        /* m_util.str.is_replace_all(n) || uncomment to enable axiomatization */
         m_util.str.is_le(n)) {
         enque_axiom(n);
     }

src/solver/check_sat_result.cpp

@@ -20,7 +20,10 @@ Notes:
 
 void check_sat_result::set_reason_unknown(event_handler& eh) {
     switch (eh.caller_id()) {
-    case UNSET_EH_CALLER: break;
+    case UNSET_EH_CALLER: 
+        if (reason_unknown() == "")
+            set_reason_unknown("unclassifed exception");
+        break;
     case CTRL_C_EH_CALLER:
         set_reason_unknown("interrupted from keyboard");
         break;

src/solver/solver.cpp

@@ -226,7 +226,7 @@ void solver::collect_param_descrs(param_descrs & r) {
 }
 
 void solver::reset_params(params_ref const & p) {
-    m_params = p;
+    m_params.append(p);
     solver_params sp(m_params);
     m_cancel_backup_file = sp.cancel_backup_file();
 }