Merge branch 'master' of https://github.com/z3prover/z3 into polysat

.github/workflows/coverage.yml

@@ -6,10 +6,6 @@ on:
   schedule:
     - cron: "0 11 * * *"
 
-env:
-  BUILD_TYPE: Debug
-  CMAKE_GENERATOR: Ninja
-
 jobs:
   build:
     runs-on: ubuntu-latest
@@ -17,6 +13,9 @@ jobs:
     env:
       CC: clang
       CXX: clang++
+      BUILD_TYPE: Debug
+      CMAKE_GENERATOR: Ninja
+      COV_DETAILS_PATH: ${{github.workspace}}/cov-details
 
     steps:
     - uses: actions/checkout@v2
@@ -25,14 +24,13 @@ jobs:
       run: |
         sudo apt-get remove -y --purge man-db
         sudo apt-get update -y
-        sudo apt-get install -y gcovr ninja-build
+        sudo apt-get install -y gcovr ninja-build llvm clang
 
     ## Building
     - name: Configure CMake Z3
       run: CFLAGS=="--coverage" CXXFLAGS="--coverage" LDFLAGS="-lgcov" cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCMAKE_INSTALL_PREFIX=./install
 
     - name: Build Z3
-      # Build your program with the given configuration
       run: cmake --build ${{github.workspace}}/build --target install --config ${{env.BUILD_TYPE}}
 
     - name: Build test-z3
@@ -75,8 +73,14 @@ jobs:
     - name: Gather coverage
       run: |
         cd ${{github.workspace}}
-        gcovr
+        gcovr --html coverage.html --gcov-executable "llvm-cov gcov" .
-        #gcovr --html -o coverage.html .
+        cd -
+
+    - name: Gather detailed coverage
+      run: |
+        cd ${{github.workspace}}
+        mkdir cov-details
+        gcovr --html-details ${{env.COV_DETAILS_PATH}}/coverage.html --gcov-executable "llvm-cov gcov" -r `pwd`/src --object-directory `pwd`/build
         cd -
 
     - name: Get date
@@ -86,5 +90,11 @@ jobs:
     - uses: actions/upload-artifact@v2
       with:
         name: coverage-${{steps.date.outputs.date}}
-        path: coverage.html
+        path: ${{github.workspace}}/coverage.html
-        retention-days: 10
+        retention-days: 4
+
+    - uses: actions/upload-artifact@v2
+      with:
+        name: coverage-details-${{steps.date.outputs.date}}
+        path: ${{env.COV_DETAILS_PATH}}
+        retention-days: 4

azure-pipelines.yml

@@ -200,8 +200,6 @@ jobs:
          examples\cpp_example_build_dir\cpp_example.exe
          nmake c_example
          examples\c_example_build_dir\c_example.exe
-         nmake java_example
-         nmake dotnet_example
          nmake test-z3
          test-z3.exe -a
          popd
@@ -226,6 +224,7 @@ jobs:
         make -j3 test-z3
         ./cpp_example
         ./c_example
+        # java -cp api/java/classes; JavaExample
         cd ..
 # Skip as dead-slow in debug mode:
 #  - template: scripts/test-z3.yml

examples/java/README

@@ -12,3 +12,9 @@ On Linux and FreeBSD, we must use
    LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
 On macOS, the corresponding option is DYLD_LIBRARY_PATH:
    DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample  
+
+By default, Z3 Java bindings are automatically loading the required native library for Z3 from the default library path.
+In certain environments, depending on the developing process, the Z3 library is not available in the given library path.
+To disable the automated loading process, the user can set the environment variable "z3.skipLibraryLoad=true".
+In that case, the calling application should directly load the corresponding libraries before any interaction with Z3.
+

scripts/mk_util.py

@@ -1735,7 +1735,7 @@ class DotNetDLLComponent(Component):
             dotnetCmdLine.extend(['Release'])
 
         path = os.path.join(os.path.abspath(BUILD_DIR), ".")
-        dotnetCmdLine.extend(['-o', path])
+        dotnetCmdLine.extend(['-o', "\"%s\"" % path])
             
         MakeRuleCmd.write_cmd(out, ' '.join(dotnetCmdLine))
         out.write('\n')        

scripts/update_api.py

@@ -545,7 +545,7 @@ def mk_java(java_dir, package_name):
     java_native.write('  public static native void setInternalErrorHandler(long ctx);\n\n')
 
     java_native.write('  static {\n')
-    java_native.write('    if (null == System.getProperty("z3.skipLibraryLoad")) {\n')
+    java_native.write('    if (!Boolean.parseBoolean(System.getProperty("z3.skipLibraryLoad"))) {\n')
     java_native.write('      try {\n')
     java_native.write('        System.loadLibrary("z3java");\n')
     java_native.write('      } catch (UnsatisfiedLinkError ex) {\n')
@@ -1719,14 +1719,12 @@ def write_log_h_preamble(log_h):
   log_h.write('#define _Z3_UNUSED\n')
   log_h.write('#endif\n')
   #
-  log_h.write('#include<iostream>\n')
+  log_h.write('#include "util/mutex.h"\n')
-  log_h.write('#include<atomic>\n')
+  log_h.write('extern atomic<bool> g_z3_log_enabled;\n')
-  log_h.write('extern std::ostream * g_z3_log;\n')
+  log_h.write('void ctx_enable_logging();\n')
-  log_h.write('extern std::atomic<bool>      g_z3_log_enabled;\n')
+  log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n')
-  log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { m_prev = g_z3_log && g_z3_log_enabled.exchange(false); } ~z3_log_ctx() { if (g_z3_log) g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n')
+  log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
-  log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n')
+  log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n')
-  log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
-  log_h.write('void _Z3_append_log(char const * msg);\n')
 
 
 def write_log_c_preamble(log_c):

src/api/api_ast.cpp

@@ -137,6 +137,11 @@ extern "C" {
         func_decl* d = to_func_decl(f);
         ast_manager& m = mk_c(c)->m();
         recfun::decl::plugin& p = mk_c(c)->recfun().get_plugin();
+        if (!p.has_def(d)) {
+            std::string msg = "function " + mk_pp(d, m) + " needs to be defined using rec_func_decl";
+            SET_ERROR_CODE(Z3_INVALID_ARG, msg.c_str());
+            return;
+        }
         expr_ref abs_body(m);
         expr_ref_vector _args(m);
         var_ref_vector _vars(m);
@@ -714,6 +719,9 @@ extern "C" {
         else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
             return Z3_RE_SORT;
         }
+	else if (fid == mk_c(c)->get_char_fid() && k == CHAR_SORT) {
+            return Z3_CHAR_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }

src/api/api_context.cpp

@@ -98,6 +98,7 @@ namespace api {
         m_datalog_fid = m().mk_family_id("datalog_relation");
         m_fpa_fid   = m().mk_family_id("fpa");
         m_seq_fid   = m().mk_family_id("seq");
+	m_char_fid   = m().mk_family_id("char");
         m_special_relations_fid   = m().mk_family_id("specrels");
         m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
     
@@ -269,10 +270,8 @@ namespace api {
     
     void context::invoke_error_handler(Z3_error_code c) {
         if (m_error_handler) {
-            if (g_z3_log) {
             // error handler can do crazy stuff such as longjmp
-                g_z3_log_enabled = true;
+            ctx_enable_logging();
-            }
             m_error_handler(reinterpret_cast<Z3_context>(this), c);
         }
     }

src/api/api_context.h

@@ -104,6 +104,7 @@ namespace api {
         family_id                  m_pb_fid;
         family_id                  m_fpa_fid;
         family_id                  m_seq_fid;
+        family_id                  m_char_fid;
         family_id                  m_special_relations_fid;
         datatype_decl_plugin *     m_dt_plugin;
         
@@ -159,6 +160,7 @@ namespace api {
         family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
         family_id get_seq_fid() const { return m_seq_fid; }
+        family_id get_char_fid() const { return m_char_fid; }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
         family_id get_special_relations_fid() const { return m_special_relations_fid; }
 

src/api/api_fpa.cpp

@@ -877,7 +877,7 @@ extern "C" {
         CHECK_VALID_AST(s, 0);
         if (!is_fp_sort(c, s)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");
-            RETURN_Z3(0);
+            return 0;
         }
         return mk_c(c)->fpautil().get_ebits(to_sort(s));
         Z3_CATCH_RETURN(0);
@@ -891,7 +891,7 @@ extern "C" {
         CHECK_VALID_AST(s, 0);
         if (!is_fp_sort(c, s)) {
             SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");
-            RETURN_Z3(0);
+            return 0;
         }
         return mk_c(c)->fpautil().get_sbits(to_sort(s));
         Z3_CATCH_RETURN(0);

src/api/api_log.cpp

@@ -18,12 +18,13 @@ Revision History:
 #include<fstream>
 #include "api/z3.h"
 #include "api/api_log_macros.h"
+#include "api/z3_logger.h"
 #include "util/util.h"
 #include "util/z3_version.h"
 #include "util/mutex.h"
 
-std::ostream * g_z3_log = nullptr;
+static std::ostream * g_z3_log = nullptr;
-std::atomic<bool> g_z3_log_enabled;
+atomic<bool> g_z3_log_enabled;
 
 #ifdef Z3_LOG_SYNC
 static mutex g_log_mux;
@@ -32,6 +33,78 @@ static mutex g_log_mux;
 #define SCOPED_LOCK() {}
 #endif
 
+// functions called from api_log_macros.*
+void SetR(void * obj) {
+    *g_z3_log << "= " << obj << '\n';
+}
+
+void SetO(void * obj, unsigned pos) {
+    *g_z3_log << "* " << obj << ' ' << pos << '\n';
+}
+
+void SetAO(void * obj, unsigned pos, unsigned idx) {
+    *g_z3_log << "@ " << obj << ' ' << pos << ' ' << idx << '\n';
+}
+
+namespace {
+struct ll_escaped { char const * m_str; };
+std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
+    char const * s = d.m_str;
+    while (*s) {
+        unsigned char c = *s;
+        if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') ||
+            c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' ||
+            c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' ||
+            c == '<' || c == '>') {
+            out << c;
+        }
+        else {
+            unsigned char str[4] = {'0', '0', '0', 0};
+            str[2] = '0' + (c % 10);
+            c /= 10;
+            str[1] = '0' + (c % 10);
+            c /= 10;
+            str[0] = '0' + c;
+            out << '\\' << str;
+        }
+        s++;
+    }
+    return out;
+}
+}
+
+void R()              { *g_z3_log << 'R' << std::endl; }
+void P(void * obj)    { *g_z3_log << "P " << obj <<std::endl; }
+void I(int64_t i)     { *g_z3_log << "I " << i << std::endl; }
+void U(uint64_t u)    { *g_z3_log << "U " << u << std::endl; }
+void D(double d)      { *g_z3_log << "D " << d << std::endl; }
+void S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped{str} << '"' << std::endl; }
+void Sy(Z3_symbol sym) {
+    symbol s = symbol::c_api_ext2symbol(sym);
+    if (s.is_null()) {
+        *g_z3_log << 'N';
+    }
+    else if (s.is_numerical()) {
+        *g_z3_log << "# " << s.get_num();
+    }
+    else {
+        *g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|';
+    }
+    *g_z3_log << std::endl;
+}
+void Ap(unsigned sz)  { *g_z3_log << "p " << sz << std::endl; }
+void Au(unsigned sz)  { *g_z3_log << "u " << sz << std::endl; }
+void Ai(unsigned sz)  { *g_z3_log << "i " << sz << std::endl; }
+void Asy(unsigned sz) { *g_z3_log << "s " << sz << std::endl; }
+void C(unsigned id)   { *g_z3_log << "C " << id << std::endl; }
+static void _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped{msg} << '"' << std::endl; }
+
+void ctx_enable_logging() {
+    SCOPED_LOCK();
+    if (g_z3_log != nullptr)
+        g_z3_log_enabled = true;
+}
+
 static void Z3_close_log_unsafe(void) {
     if (g_z3_log != nullptr) {
         g_z3_log_enabled = false;
@@ -42,11 +115,11 @@ static void Z3_close_log_unsafe(void) {
 
 extern "C" {
     bool Z3_API Z3_open_log(Z3_string filename) {
-        bool res = true;
+        bool res;
 
         SCOPED_LOCK();
-        if (g_z3_log != nullptr)
         Z3_close_log_unsafe();
+
         g_z3_log = alloc(std::ofstream, filename);
         if (g_z3_log->bad() || g_z3_log->fail()) {
             dealloc(g_z3_log);
@@ -54,16 +127,16 @@ extern "C" {
             res = false;
         }
         else {
-            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n";
+            *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << '"' << std::endl;
-            g_z3_log->flush();
+            res = true;
-            g_z3_log_enabled = true;
         }
 
+        g_z3_log_enabled = res;
         return res;
     }
 
     void Z3_API Z3_append_log(Z3_string str) {
-        if (g_z3_log == nullptr)
+        if (!g_z3_log_enabled)
             return;
         SCOPED_LOCK();
         if (g_z3_log != nullptr)
@@ -71,9 +144,7 @@ extern "C" {
     }
 
     void Z3_API Z3_close_log(void) {
-        if (g_z3_log != nullptr) {
         SCOPED_LOCK();
         Z3_close_log_unsafe();
     }
-    }
 }

src/api/api_opt.cpp

@@ -325,6 +325,7 @@ extern "C" {
         RESET_ERROR_CODE();
         Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
         to_optimize_ptr(d)->collect_statistics(st->m_stats);
+        to_optimize_ptr(d)->collect_timer_stats(st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
         RETURN_Z3(r);

src/api/api_quant.cpp

@@ -162,7 +162,7 @@ extern "C" {
         }
         result = mk_c(c)->m().mk_lambda(names.size(), ts, names.data(), to_expr(body));
         mk_c(c)->save_ast_trail(result.get());
-        return of_ast(result.get());
+        RETURN_Z3(of_ast(result.get()));
         Z3_CATCH_RETURN(nullptr);
     }
 
@@ -192,7 +192,7 @@ extern "C" {
         
         result = mk_c(c)->m().mk_lambda(_vars.size(), _vars.data(), _names.data(), result);
         mk_c(c)->save_ast_trail(result.get());
-        return of_ast(result.get());
+        RETURN_Z3(of_ast(result.get()));
         Z3_CATCH_RETURN(nullptr);
     }
 

src/api/api_seq.cpp

@@ -267,6 +267,7 @@ extern "C" {
     MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
     MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP);
   
+    MK_SORTED(Z3_mk_re_allchar, mk_c(c)->sutil().re.mk_full_char);
     MK_SORTED(Z3_mk_re_empty, mk_c(c)->sutil().re.mk_empty);
     MK_SORTED(Z3_mk_re_full, mk_c(c)->sutil().re.mk_full_seq);
 

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

@@ -507,7 +507,6 @@ namespace z3 {
         ast(context & c):object(c), m_ast(0) {}
         ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
         ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
-        ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
         ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
         operator Z3_ast() const { return m_ast; }
         operator bool() const { return m_ast != 0; }
@@ -1210,6 +1209,7 @@ namespace z3 {
         friend expr implies(bool a, expr const & b);
 
         friend expr mk_or(expr_vector const& args);
+        friend expr mk_xor(expr_vector const& args);
         friend expr mk_and(expr_vector const& args);
 
         friend expr ite(expr const & c, expr const & t, expr const & e);
@@ -2384,6 +2384,14 @@ namespace z3 {
         args.check_error();
         return expr(args.ctx(), r);
     }
+    inline expr mk_xor(expr_vector const& args) {
+        if (args.empty())
+            return args.ctx().bool_val(false);
+        expr r = args[0];
+        for (unsigned i = 1; i < args.size(); ++i)
+            r = r ^ args[i];
+        return r;
+    }
 
 
     class func_entry : public object {
@@ -3874,8 +3882,11 @@ namespace z3 {
 
 
     public:
-        user_propagator_base(solver* s): s(s), c(nullptr) {}
+        user_propagator_base(Z3_context c) : s(nullptr), c(c) {}
-        user_propagator_base(Z3_context c): s(nullptr), c(c) {}
+        
+        user_propagator_base(solver* s): s(s), c(nullptr) {
+              Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
+	    }
 
         virtual void push() = 0;
         virtual void pop(unsigned num_scopes) = 0;

src/api/java/Optimize.java

@@ -173,10 +173,21 @@ public class Optimize extends Z3Object {
      *
      **/
     public Handle<?> AssertSoft(Expr<BoolSort> constraint, int weight, String group)
+    {
+        return AssertSoft(constraint, Integer.toString(weight), group);
+    }
+    
+    /**
+     * Assert soft constraint
+     *
+     * Return an objective which associates with the group of constraints.
+     *
+     **/
+    public Handle<?> AssertSoft(Expr<BoolSort> constraint, String weight, String group)
     {
         getContext().checkContextMatch(constraint);
         Symbol s = getContext().mkSymbol(group);
-        return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
+        return new Handle<>(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), weight, s.getNativeObject()));
     }
 
     /**

src/api/python/setup.py

@@ -296,9 +296,9 @@ setup(
     name='z3-solver',
     version=_z3_version(),
     description='an efficient SMT solver library',
-    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/angr/angr-z3',
+    long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compilation, or installation, please submit issues to https://github.com/z3prover/z3.git',
     author="The Z3 Theorem Prover Project",
-    maintainer="Audrey Dutcher",
+    maintainer="Audrey Dutcher and Nikolaj Bjorner",
     maintainer_email="audrey@rhelmot.io",
     url='https://github.com/Z3Prover/z3',
     license='MIT License',

src/api/python/z3/z3.py

@@ -680,6 +680,8 @@ def _to_sort_ref(s, ctx):
         return ReSortRef(s, ctx)
     elif k == Z3_SEQ_SORT:
         return SeqSortRef(s, ctx)
+    elif k == Z3_CHAR_SORT:
+        return CharSortRef(s, ctx)
     return SortRef(s, ctx)
 
 
@@ -6561,6 +6563,15 @@ class ModelRef(Z3PPObject):
             r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
         return r
 
+    def update_value(self, x, value):
+        """Update the interpretation of a constant"""
+        if is_expr(x):
+            x = x.decl()
+        if not is_func_decl(x) or x.arity() != 0:
+            raise Z3Exception("Expecting 0-ary function or constant expression")
+        value = _py2expr(value)
+        Z3_add_const_interp(x.ctx_ref(), self.model, x.ast, value.ast)
+
     def translate(self, target):
         """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
         """
@@ -9572,7 +9583,7 @@ class FPNumRef(FPRef):
 
     def sign(self):
         num = (ctypes.c_int)()
-        nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l))
+        nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
         if nsign is False:
             raise Z3Exception("error retrieving the sign of a numeral.")
         return num.value != 0
@@ -10565,6 +10576,10 @@ class SeqSortRef(SortRef):
     def basis(self):
         return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx)
 
+class CharSortRef(SortRef):
+    """Character sort."""
+    
+
 
 def StringSort(ctx=None):
     """Create a string sort
@@ -10575,6 +10590,15 @@ def StringSort(ctx=None):
     ctx = _get_ctx(ctx)
     return SeqSortRef(Z3_mk_string_sort(ctx.ref()), ctx)
 
+def CharSort(ctx=None):
+    """Create a character sort
+    >>> ch = CharSort()
+    >>> print(ch)
+    Char
+    """
+    ctx = _get_ctx(ctx)
+    return CharSortRef(Z3_mk_char_sort(ctx.ref()), ctx)
+
 
 def SeqSort(s):
     """Create a sequence sort over elements provided in the argument
@@ -11042,6 +11066,11 @@ def Range(lo, hi, ctx=None):
     hi = _coerce_seq(hi, ctx)
     return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx)
 
+def AllChar(regex_sort, ctx=None):
+    """Create a regular expression that accepts all single character strings
+    """
+    return ReRef(Z3_mk_re_allchar(regex_sort.ctx_ref(), regex_sort.ast), regex_sort.ctx)
+
 # Special Relations
 
 

src/api/python/z3/z3printer.py

@@ -757,6 +757,8 @@ class Formatter:
             if s.is_string():
                 return to_format("String")
             return seq1("Seq", (self.pp_sort(s.basis()), ))
+        elif isinstance(s, z3.CharSortRef):
+            return to_format("Char")
         else:
             return to_format(s.name())
 

src/api/z3_api.h

@@ -161,6 +161,7 @@ typedef enum
     Z3_ROUNDING_MODE_SORT,
     Z3_SEQ_SORT,
     Z3_RE_SORT,
+    Z3_CHAR_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -3724,6 +3725,14 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_re_range(Z3_context c, Z3_ast lo, Z3_ast hi);
 
+
+    /**
+       \brief Create a regular expression that accepts all singleton sequences of the regular expression sort
+
+      def_API('Z3_mk_re_allchar', AST, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_re_allchar(Z3_context c, Z3_sort regex_sort);
+  
     /**
        \brief Create a regular expression loop. The supplied regular expression \c r is repeated
        between \c lo and \c hi times. The \c lo should be below \c hi with one exception: when

src/api/z3_logger.h

@@ -16,57 +16,17 @@ Author:
 Notes:
     
 --*/
-#include<iostream>
 #include "util/symbol.h"
-struct ll_escaped { char const * m_str; ll_escaped(char const * str):m_str(str) {} };
-static std::ostream & operator<<(std::ostream & out, ll_escaped const & d);
 
-static void __declspec(noinline) R()  { *g_z3_log << "R\n"; g_z3_log->flush(); }
+void R();
-static void __declspec(noinline) P(void * obj)  { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); }
+void P(void * obj);
-static void __declspec(noinline) I(int64_t i)   { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); }
+void I(int64_t i);
-static void __declspec(noinline) U(uint64_t u)   { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); }
+void U(uint64_t u);
-static void __declspec(noinline) D(double d)   { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); }
+void D(double d);
-static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); }
+void S(Z3_string str);
-static void __declspec(noinline) Sy(Z3_symbol sym) { 
+void Sy(Z3_symbol sym);
-    symbol s = symbol::c_api_ext2symbol(sym);
+void Ap(unsigned sz);
-    if (s.is_null()) {
+void Au(unsigned sz);
-        *g_z3_log << "N\n";
+void Ai(unsigned sz);
-    }
+void Asy(unsigned sz);
-    else if (s.is_numerical()) {
+void C(unsigned id);
-        *g_z3_log << "# " << s.get_num() << "\n";
-    }
-    else {
-        *g_z3_log << "$ |" << ll_escaped(s.bare_str()) << "|\n";
-    }
-    g_z3_log->flush();
-}
-static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); }
-static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); }
-static void __declspec(noinline) Ai(unsigned sz) { *g_z3_log << "i " << sz << "\n"; g_z3_log->flush(); }
-static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); }
-static void __declspec(noinline) C(unsigned id)   { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); }
-void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); }
-
-static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) {
-    char const * s = d.m_str;
-    while (*s) {
-        unsigned char c = *s;
-        if (('0' <= c && c <= '9') || ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z') ||
-            c == '~' || c == '!' || c == '@' || c == '#' || c == '$' || c == '%' || c == '^' || c == '&' ||
-            c == '*' || c == '-' || c == '_' || c == '+' || c == '.' || c == '?' || c == '/' || c == ' ' ||
-            c == '<' || c == '>') {
-            out << c;
-        }
-        else {
-            unsigned char str[4] = {'0', '0', '0', 0};
-            str[2] = '0' + (c % 10);
-            c /= 10;
-            str[1] = '0' + (c % 10);
-            c /= 10;
-            str[0] = '0' + c;
-            out << '\\' << str;
-        }
-        s++;
-    }
-    return out;
-}

src/ast/ast_pp.h

@@ -67,4 +67,7 @@ inline std::string operator+(std::string const& s, mk_pp const& pp) {
     return strm.str();
 }
 
+inline std::string& operator+=(std::string& s, mk_pp const& pp) {
+    return s = s + pp;
+}
 

src/ast/datatype_decl_plugin.cpp

@@ -367,6 +367,25 @@ namespace datatype {
             return m.mk_func_decl(name, arity, domain, range, info);
         }
 
+        ptr_vector<constructor> plugin::get_constructors(symbol const& s) const {
+            ptr_vector<constructor> result;
+            for (auto [k, d] : m_defs) 
+                for (auto* c : *d)
+                    if (c->name() == s)
+                        result.push_back(c);
+            return result;
+        }
+
+        ptr_vector<accessor> plugin::get_accessors(symbol const& s) const {
+            ptr_vector<accessor> result;
+            for (auto [k, d] : m_defs) 
+                for (auto* c : *d)
+                    for (auto* a : *c)
+                        if (a->name() == s)
+                            result.push_back(a);
+            return result;
+        }
+
         func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, 
                                                 unsigned arity, sort * const * domain, sort *) {
             ast_manager& m = *m_manager;
@@ -556,9 +575,8 @@ namespace datatype {
 
         void plugin::remove(symbol const& s) {
             def* d = nullptr;
-            if (m_defs.find(s, d)) {
+            if (m_defs.find(s, d)) 
                 dealloc(d);
-            }
             m_defs.remove(s);
         }
 
@@ -688,18 +706,18 @@ namespace datatype {
        \brief Return true if the inductive datatype is recursive.
     */
     bool util::is_recursive_core(sort* s) const {
-        obj_map<sort, status> already_found;
+        map<symbol, status, symbol_hash_proc, symbol_eq_proc> already_found;
         ptr_vector<sort> todo, subsorts;
         sort* s0 = s;
         todo.push_back(s);
         status st;        
         while (!todo.empty()) {
             s = todo.back();
-            if (already_found.find(s, st) && st == BLACK) {
+            if (already_found.find(datatype_name(s), st) && st == BLACK) {
                 todo.pop_back();
                 continue;
             }
-            already_found.insert(s, GRAY);
+            already_found.insert(datatype_name(s), GRAY);
             def const& d = get_def(s);
             bool can_process       = true;
             for (constructor const* c : d) {
@@ -710,9 +728,9 @@ namespace datatype {
                     get_subsorts(d, subsorts);
                     for (sort * s2 : subsorts) {
                         if (is_datatype(s2)) {
-                            if (already_found.find(s2, st)) {
+                            if (already_found.find(datatype_name(s2), st)) {
                                 // type is recursive
-                                if (st == GRAY && s0 == s2) 
+                                if (st == GRAY && datatype_name(s0) == datatype_name(s2)) 
                                     return true;
                             }
                             else {
@@ -724,7 +742,7 @@ namespace datatype {
                 }
             }
             if (can_process) {
-                already_found.insert(s, BLACK);
+                already_found.insert(datatype_name(s), BLACK);
                 todo.pop_back();
             }
         }

src/ast/datatype_decl_plugin.h

@@ -248,6 +248,8 @@ namespace datatype {
 
             def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); }
             def& get_def(symbol const& s) { return *(m_defs[s]); }
+            ptr_vector<constructor> get_constructors(symbol const& s) const;
+            ptr_vector<accessor> get_accessors(symbol const& s) const;
             bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); }
             unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
             util & u() const;
@@ -321,6 +323,7 @@ namespace datatype {
         bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
         def& get_def(symbol const& s) { return plugin().get_def(s); }        
         void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;        
+        symbol datatype_name(sort* s) const { return s->get_parameter(0).get_symbol(); }
 
     public:
         util(ast_manager & m);

src/ast/euf/euf_egraph.cpp

@@ -99,7 +99,7 @@ namespace euf {
     void egraph::update_children(enode* n) {
         for (enode* child : enode_args(n)) 
             child->get_root()->add_parent(n);
-        n->set_update_children();            
+        m_updates.push_back(update_record(n, update_record::update_children()));
     }
 
     enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) {
@@ -118,14 +118,14 @@ namespace euf {
             n->set_is_equality();
             update_children(n);
             reinsert_equality(n);
-            return n;
         }
-        enode_bool_pair p = insert_table(n);
+        else {
-        enode* n2 = p.first;
+            auto [n2, comm] = insert_table(n);
             if (n2 == n) 
                 update_children(n);        
             else 
-            merge(n, n2, justification::congruence(p.second));        
+                merge(n, n2, justification::congruence(comm));
+        }
         return n;
     }
 
@@ -264,18 +264,21 @@ namespace euf {
 
     void egraph::set_merge_enabled(enode* n, bool enable_merge) {
         if (enable_merge != n->merge_enabled()) {
-            toggle_merge_enabled(n);
+            toggle_merge_enabled(n, false);
             m_updates.push_back(update_record(n, update_record::toggle_merge()));
         }
     }
 
-    void egraph::toggle_merge_enabled(enode* n) {
+    void egraph::toggle_merge_enabled(enode* n, bool backtracking) {
        bool enable_merge = !n->merge_enabled();
        n->set_merge_enabled(enable_merge);         
        if (n->num_args() > 0) {
-           if (enable_merge)
+           if (enable_merge) {
-               insert_table(n);
+               auto [n2, comm] = insert_table(n);
-           else if (m_table.contains_ptr(n))
+               if (n2 != n && !backtracking)
+                   m_to_merge.push_back(to_merge(n, n2, comm));
+           }
+           else if (n->is_cgr())
                erase_from_table(n);
        }
        VERIFY(n->num_args() == 0 || !n->merge_enabled() || m_table.contains(n));
@@ -332,14 +335,15 @@ namespace euf {
             m_nodes.pop_back();
             m_exprs.pop_back();
         };
-        for (unsigned i = m_updates.size(); i-- > num_updates; ) {
+        unsigned sz = m_updates.size();
+        for (unsigned i = sz; i-- > num_updates; ) {
             auto const& p = m_updates[i];
             switch (p.tag) {
             case update_record::tag_t::is_add_node:
                 undo_node();
                 break;
             case update_record::tag_t::is_toggle_merge:
-                toggle_merge_enabled(p.r1);
+                toggle_merge_enabled(p.r1, true);
                 break;
             case update_record::tag_t::is_set_parent:
                 undo_eq(p.r1, p.n1, p.r2_num_parents);
@@ -376,12 +380,18 @@ 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_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);
+                    p.r1->m_args[i]->get_root()->m_parents.pop_back();
+                }
+                break;
             default:
                 UNREACHABLE();
                 break;
             }                    
         }        
-       
+        SASSERT(m_updates.size() == sz);
         m_updates.shrink(num_updates);
         m_scopes.shrink(old_lim);        
         m_region.pop_scope(num_scopes);  
@@ -403,7 +413,7 @@ namespace euf {
         if (r1 == r2)
             return;
 
-        TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
+        TRACE("euf", j.display(tout << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n" << bpp(r1) << " " << bpp(r2) << "\n";);
         IF_VERBOSE(20, j.display(verbose_stream() << "merge: " << bpp(n1) << " == " << bpp(n2) << " ", m_display_justification) << "\n";);
         force_push();
         SASSERT(m_num_scopes == 0);
@@ -457,12 +467,13 @@ namespace euf {
             if (!p->is_marked1())
                 continue;
             p->unmark1();
+            TRACE("euf", tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->merge_enabled() << "\n";);
             if (p->merge_enabled()) {
-                auto rc = insert_table(p);
+                auto [p_other, comm] = insert_table(p);
-                enode* p_other = rc.first;
                 SASSERT(m_table.contains_ptr(p) == (p_other == p));
+                TRACE("euf", tout << "other " << bpp(p_other) << "\n";);
                 if (p_other != p) 
-                    m_to_merge.push_back(to_merge(p_other, p, rc.second));                
+                    m_to_merge.push_back(to_merge(p_other, p, comm));                
                 else
                     r2->m_parents.push_back(p);
                 if (p->is_equality())
@@ -752,7 +763,7 @@ namespace euf {
             out << "] ";
         }
         if (n->value() != l_undef) 
-            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << "] ";
+            out << "[b" << n->bool_var() << " := " << (n->value() == l_true ? "T":"F") << (n->merge_tf()?"":" no merge") << "] ";
         if (n->has_th_vars()) {
             out << "[t";
             for (auto v : enode_th_vars(n))

src/ast/euf/euf_egraph.h

@@ -104,7 +104,8 @@ namespace euf {
             struct value_assignment {};
             struct lbl_hash {};
             struct lbl_set {};
-            enum class tag_t { is_set_parent, is_add_node, is_toggle_merge, 
+            struct update_children {};
+            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 };
@@ -148,6 +149,8 @@ namespace euf {
                 tag(tag_t::is_lbl_hash), r1(n), n1(nullptr), m_lbl_hash(n->m_lbl_hash) {}
             update_record(enode* n, lbl_set):
                 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) {}
         };
         ast_manager&           m;
         svector<to_merge>      m_to_merge;
@@ -211,7 +214,7 @@ namespace euf {
         void push_to_lca(enode* a, enode* lca);
         void push_congruence(enode* n1, enode* n2, bool commutative);
         void push_todo(enode* n);
-        void toggle_merge_enabled(enode* n);
+        void toggle_merge_enabled(enode* n, bool backtracking);
 
         enode_bool_pair insert_table(enode* p);
         void erase_from_table(enode* p);
@@ -235,7 +238,7 @@ namespace euf {
         enode* find(expr* f, unsigned n, enode* const* args);
         enode* mk(expr* f, unsigned generation, unsigned n, enode *const* args);
         enode_vector const& enodes_of(func_decl* f);
-        void push() { ++m_num_scopes; }
+        void push() { if (!m_to_merge.empty()) propagate(); ++m_num_scopes; }
         void pop(unsigned num_scopes);
 
         /**

src/ast/euf/euf_enode.h

@@ -46,7 +46,6 @@ namespace euf {
         bool          m_mark1 = false;
         bool          m_mark2 = false;
         bool          m_commutative = false;
-        bool          m_update_children = false;
         bool          m_interpreted = false;
         bool          m_merge_enabled = true; 
         bool          m_is_equality = false;    // Does the expression represent an equality
@@ -125,9 +124,6 @@ namespace euf {
             return n;
         }    
        
-        void set_update_children() { m_update_children = true; }
-
-
         friend class add_th_var_trail;
         friend class replace_th_var_trail;
         void add_th_var(theory_var v, theory_id id, region & r) { m_th_vars.add_var(v, id, r); }
@@ -142,12 +138,6 @@ namespace euf {
         ~enode() { 
             SASSERT(m_root == this); 
             SASSERT(class_size() == 1); 
-            if (m_update_children) {
-                for (unsigned i = 0; i < num_args(); ++i) {
-                    SASSERT(m_args[i]->get_root()->m_parents.back() == this);
-                    m_args[i]->get_root()->m_parents.pop_back();
-                }
-            }
         }
 
         enode* const* args() const { return m_args; }

src/ast/fpa/fpa2bv_converter.cpp

@@ -19,6 +19,7 @@ Notes:
 #include<math.h>
 
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "ast/well_sorted.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/used_vars.h"
@@ -4430,7 +4431,7 @@ expr* fpa2bv_converter_wrapped::bv2fpa_value(sort* s, expr* a, expr* b, expr* c)
     mpfm.set(f, ebits, sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
     result = m_util.mk_value(f);
 
-    TRACE("t_fpa", tout << "result: [" <<
+    TRACE("t_fpa", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << " result: [" <<
           mpzm.to_string(sgn_z) << "," <<
           mpzm.to_string(exp_z) << "," <<
           mpzm.to_string(sig_z) << "] --> " <<

src/ast/macros/macro_manager.cpp

@@ -126,7 +126,7 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
     }
 
     app * head;
-    expr * definition;
+    expr_ref definition(m);
     bool revert = false;
     get_head_def(q, f, head, definition, revert);
 
@@ -190,21 +190,23 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
 }
 
 
-void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const {
+void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const {
-    app * body = to_app(q->get_expr());
+    expr * body = q->get_expr();
     expr * lhs = nullptr, *rhs = nullptr;
+    bool is_not = m.is_not(body, body);
     VERIFY(m.is_eq(body, lhs, rhs));
     SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d));
     SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d));
+    SASSERT(!is_not || m.is_bool(lhs));     
     if (is_app_of(lhs, d)) {
         revert = false;
         head = to_app(lhs);
-        def  = rhs;
+        def  = is_not ? m.mk_not(rhs) : rhs;
     }
     else {
         revert = true;
         head = to_app(rhs);
-        def  = lhs;
+        def  = is_not ? m.mk_not(lhs) : lhs;
     }
 }
 
@@ -215,7 +217,7 @@ void macro_manager::display(std::ostream & out) {
         quantifier * q = nullptr;
         m_decl2macro.find(f, q);
         app * head;
-        expr * def;
+        expr_ref def(m);
         bool r;
         get_head_def(q, f, head, def, r);
         SASSERT(q);
@@ -227,7 +229,7 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
     func_decl * f  = m_decls.get(i);
     quantifier * q = m_macros.get(i);
     app * head;
-    expr * def;
+    expr_ref def(m);
     bool r;
     get_head_def(q, f, head, def, r);
     TRACE("macro_bug",
@@ -298,7 +300,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
         TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
         if (mm.m_decl2macro.find(d, q)) {            
             app * head = nullptr;
-            expr * def = nullptr;
+            expr_ref def(m);
             bool revert = false;
             mm.get_head_def(q, d, head, def, revert);
             unsigned num = n->get_num_args();
@@ -320,6 +322,14 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             r = rr;
             if (m.proofs_enabled()) {
                 expr_ref instance = s(q->get_expr(), num, subst_args.data());
+                expr* eq, * lhs, * rhs;
+                if (m.is_not(instance, eq) && m.is_eq(eq, lhs, rhs)) {
+                    if (revert)
+                        instance = m.mk_eq(m.mk_not(lhs), rhs);
+                    else
+                        instance = m.mk_eq(lhs, m.mk_not(rhs));
+                }
+                SASSERT(m.is_eq(instance));
                 proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.data());
                 proof * q_pr  = mm.m_decl2macro_pr.find(d);
                 proof * prs[2] = { qi_pr, q_pr };

src/ast/macros/macro_manager.h

@@ -84,7 +84,7 @@ public:
     func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); }
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
-    void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const;
+    void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const;
     void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
 
 

src/ast/macros/macro_util.cpp

@@ -184,6 +184,15 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
         def  = rhs;
         return true;
     }
+    if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) &&
+        m_manager.is_bool(lhs) &&
+        is_macro_head(lhs, num_decls) &&
+        !is_forbidden(to_app(lhs)->get_decl()) &&
+        !occurs(to_app(lhs)->get_decl(), rhs)) {
+        head = to_app(lhs);
+        def  = m_manager.mk_not(rhs);
+        return true;
+    }
     return false;
 }
 
@@ -215,6 +224,15 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
         def  = lhs;
         return true;
     }
+    if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) &&
+        m_manager.is_bool(lhs) &&
+        is_macro_head(rhs, num_decls) &&
+        !is_forbidden(to_app(rhs)->get_decl()) &&
+        !occurs(to_app(rhs)->get_decl(), lhs)) {
+        head = to_app(rhs);
+        def  = m_manager.mk_not(lhs);
+        return true;
+    }
     return false;
 }
 

src/ast/macros/quasi_macros.cpp

@@ -148,6 +148,15 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
     return false;
 }
 
+bool quasi_macros::is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const {
+  return
+    is_non_ground_uninterp(lhs) &&
+    is_unique(to_app(lhs)->get_decl()) &&
+    !depends_on(rhs, to_app(lhs)->get_decl()) &&
+    fully_depends_on(to_app(lhs), q);
+}
+
+
 bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
     // Our definition of a quasi-macro:
     // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
@@ -158,27 +167,39 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
         quantifier * q = to_quantifier(e);
         expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
         if (m.is_eq(qe, lhs, rhs)) {
-            if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
+	  if (is_quasi_def(q, lhs, rhs)) {
-                !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
 	        a = to_app(lhs);
                 t = rhs;
                 return true;
-            } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
+	  } else if (is_quasi_def(q, rhs, lhs)) {
-                !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
 	        a = to_app(rhs);
                 t = lhs;
                 return true;
             }
-        } else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
+        }
+	else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
                    is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
             a = to_app(lhs);
             t = m.mk_false();
             return true;
-        } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
+        }
+	else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
             a = to_app(qe);
             t = m.mk_true();
             return true;
         }
+	else if (m.is_not(qe, lhs) && m.is_eq(lhs, lhs, rhs) && m.is_bool(lhs)) {
+	  if (is_quasi_def(q, lhs, rhs)) {
+	        a = to_app(lhs);
+                t = m.mk_not(rhs);
+                return true;
+            } else if (is_quasi_def(q, rhs, lhs)) {
+	        a = to_app(rhs);
+                t = m.mk_not(lhs);
+                return true;
+            }
+	}
+
     }
 
     return false;

src/ast/macros/quasi_macros.h

@@ -49,6 +49,7 @@ class quasi_macros {
     bool depends_on(expr * e, func_decl * f) const;
 
     bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const;
+    bool is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const;
     bool quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro);
 
     void find_occurrences(expr * e);

src/ast/rewriter/array_rewriter.cpp

@@ -695,6 +695,12 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     if (m_util.is_const(rhs) && m_util.is_store(lhs)) {
         std::swap(lhs, rhs);
     }
+    if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
+        unsigned n = to_app(rhs)->get_num_args();
+        result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)),
+ 			  m().mk_eq(v, to_app(rhs)->get_arg(n - 1)));
+        return BR_REWRITE2;
+    }
     if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {
         result = m().mk_eq(v, w);
         return BR_REWRITE1;

src/ast/rewriter/bit_blaster/bit_blaster_tpl.h

@@ -35,16 +35,12 @@ protected:
     void mk_ext_rotate_left_right(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     unsigned long long m_max_memory;
-    bool               m_use_wtm; /* Wallace Tree Multiplier */
-    bool               m_use_bcm; /* Booth Multiplier for constants */
     void checkpoint();
 
 public:
-    bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX, bool use_wtm = false, bool use_bcm=false):
+    bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX):
         Cfg(cfg),
-        m_max_memory(max_memory),
+        m_max_memory(max_memory) {
-        m_use_wtm(use_wtm),
-        m_use_bcm(use_bcm) {
     }
 
     void set_max_memory(unsigned long long max_memory) {
@@ -121,7 +117,6 @@ public:
     void mk_comp(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
-    bool mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
     bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
     void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
 

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -195,16 +195,11 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
         return;
     }
    
-    if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
+    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
-        SASSERT(sz == out_bits.size());
-        return;
-    }
-    if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
         SASSERT(sz == out_bits.size());
         return;
     }
     out_bits.reset();
-    if (!m_use_wtm) {
 #if 0
     static unsigned counter = 0;
     counter++;
@@ -245,7 +240,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
         couts.reset();
         expr_ref i1(m()), i2(m());
         mk_and(a_bits[0], b_bits[i], i1);
-            mk_and(a_bits[1], b_bits[i-1], i2);
+        mk_and(a_bits[1], b_bits[i - 1], i2);
         if (i < sz - 1) {
             mk_half_adder(i1, i2, out, cout);
             couts.push_back(cout);
@@ -253,8 +248,8 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
                 expr_ref prev_out(m());
                 prev_out = out;
                 expr_ref i3(m());
-                    mk_and(a_bits[j], b_bits[i-j], i3);
+                mk_and(a_bits[j], b_bits[i - j], i3);
-                    mk_full_adder(i3, prev_out, cins.get(j-2), out, cout);
+                mk_full_adder(i3, prev_out, cins.get(j - 2), out, cout);
                 couts.push_back(cout);
             }
             out_bits.push_back(out);
@@ -265,98 +260,23 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
             mk_xor(i1, i2, out);
             for (unsigned j = 2; j <= i; j++) {
                 expr_ref i3(m());
-                    mk_and(a_bits[j], b_bits[i-j], i3);
+                mk_and(a_bits[j], b_bits[i - j], i3);
-                    mk_xor3(i3, out, cins.get(j-2), out);
+                mk_xor3(i3, out, cins.get(j - 2), out);
             }
             out_bits.push_back(out);
         }
     }
-    }
-    else { 
-        // WALLACE TREE MULTIPLIER        
 
-        if (sz == 1) {
-            expr_ref t(m());
-            mk_and(a_bits[0], b_bits[0], t);
-            out_bits.push_back(t);
-            return;
-        }
-
-        // There are sz numbers to add and we use a Wallace tree to reduce that to two. 
-        // In this tree, we reduce as early as possible, as opposed to the Dada tree where some 
-        // additions may be delayed if they don't increase the propagation delay [which may be 
-        // a little bit more efficient, but it's tricky to find out which additions create 
-        // additional delays].
-                
-        expr_ref zero(m());
-        zero = m().mk_false();
-
-        vector< expr_ref_vector > pps;
-        pps.resize(sz, expr_ref_vector(m()));
-               
-        for (unsigned i = 0; i < sz; i++) {
-            checkpoint();
-            // The partial product is a_bits AND b_bits[i] 
-            // [or alternatively ITE(b_bits[i], a_bits, bv0[sz])]
-
-            expr_ref_vector & pp = pps[i];
-            expr_ref t(m());
-            for (unsigned j = 0; j < i; j++)
-                pp.push_back(zero); // left shift by i bits
-            for (unsigned j = 0; j < (sz - i); j++) {
-                mk_and(a_bits[j], b_bits[i], t);
-                pp.push_back(t);
-            }
-
-            SASSERT(pps[i].size() == sz);            
-        }        
-        
-        while (pps.size() != 2) {            
-            unsigned save_inx = 0;
-            unsigned i = 0;
-            unsigned end = pps.size() - 3;
-            for ( ; i <= end; i += 3) {
-                checkpoint();
-                expr_ref_vector pp1(m()), pp2(m()), pp3(m());
-                pp1.swap(pps[i]);
-                pp2.swap(pps[i+1]);
-                pp3.swap(pps[i+2]);
-                expr_ref_vector & sum_bits = pps[save_inx];
-                expr_ref_vector & carry_bits = pps[save_inx+1];
-                SASSERT(sum_bits.empty() && carry_bits.empty());
-                carry_bits.push_back(zero);                
-                mk_carry_save_adder(pp1.size(), pp1.data(), pp2.data(), pp3.data(), sum_bits, carry_bits);
-                carry_bits.pop_back();
-                save_inx += 2;                
-            }
-
-            if (i == pps.size()-2) {
-                pps[save_inx++].swap(pps[i++]);
-                pps[save_inx++].swap(pps[i++]);
-            }
-            else if (i == pps.size()-1) {
-                pps[save_inx++].swap(pps[i++]);
-            }
-
-            SASSERT (save_inx < pps.size() && i == pps.size());            
-            pps.shrink(save_inx);
-        }        
-
-        SASSERT(pps.size() == 2);
-
-        // Now there are only two numbers to add, we can use a ripple carry adder here.
-        mk_adder(sz, pps[0].data(), pps[1].data(), out_bits);
-    }
 }
 
 
 template<typename Cfg>
-void bit_blaster_tpl<Cfg>::mk_umul_no_overflow(unsigned sz, expr * const * a_bits,  expr * const * b_bits, expr_ref & result) {
+void bit_blaster_tpl<Cfg>::mk_umul_no_overflow(unsigned sz, expr* const* a_bits, expr* const* b_bits, expr_ref& result) {
     SASSERT(sz > 0);
     expr_ref zero(m());
     zero = m().mk_false();
-    ptr_buffer<expr,128> ext_a_bits;
+    ptr_buffer<expr, 128> ext_a_bits;
-    ptr_buffer<expr,128> ext_b_bits;
+    ptr_buffer<expr, 128> ext_b_bits;
     ext_a_bits.append(sz, a_bits);
     ext_b_bits.append(sz, b_bits);
     ext_a_bits.push_back(zero);
@@ -1196,30 +1116,32 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
     unsigned case_size = 1;
     unsigned circuit_size = sz*sz*5;
     for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
-        if (!is_bool_const(a_bits[i])) {
+        if (!is_bool_const(a_bits[i])) 
+            case_size *= 2;        
+        if (!is_bool_const(b_bits[i])) 
             case_size *= 2;        
     }
-        if (!is_bool_const(b_bits[i])) {
+    if (case_size >= circuit_size) 
-            case_size *= 2;
-        }
-    }
-    if (case_size >= circuit_size) {
         return false;
-    }
+    
     SASSERT(out_bits.empty());
     ptr_buffer<expr, 128> na_bits;
     na_bits.append(sz, a_bits);
     ptr_buffer<expr, 128> nb_bits;
     nb_bits.append(sz, b_bits);
     mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); 
-    return false;
+    return true;
 }
  
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
     while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;
-    if (is_a && i == sz) { is_a = false; i = 0; }
+    if (is_a && i == sz) { 
-    while (!is_a && i < sz && is_bool_const(b_bits[i])) ++i;
+        is_a = false; 
+        i = 0; 
+    }
+    while (!is_a && i < sz && is_bool_const(b_bits[i])) 
+        ++i;
     if (i < sz) {
         expr_ref_vector out1(m()), out2(m());
         expr_ref x(m());
@@ -1230,8 +1152,10 @@ void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsig
         mk_const_case_multiplier(is_a, i+1, sz, a_bits, b_bits, out2);
         if (is_a) a_bits[i] = x; else b_bits[i] = x;
         SASSERT(out_bits.empty());
+        expr_ref bit(m());
         for (unsigned j = 0; j < sz; ++j) {
-            out_bits.push_back(m().mk_ite(x, out1[j].get(), out2[j].get()));
+            mk_ite(x, out1.get(j), out2.get(j), bit);
+            out_bits.push_back(bit);
         }       
     }
     else {
@@ -1244,101 +1168,3 @@ void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsig
     }
     SASSERT(out_bits.size() == sz);
 }
-
-template<typename Cfg>
-bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
-    numeral n_a;
-    if (!is_numeral(sz, a_bits, n_a)) {
-        return false;
-    }
-    SASSERT(out_bits.empty());
-    
-    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
-        SASSERT(sz == out_bits.size());
-        return true;
-    }    
-    out_bits.reset();
-    if (!m_use_bcm) {
-        return false;
-    }
-    expr_ref_vector minus_b_bits(m()), tmp(m());
-    mk_neg(sz, b_bits, minus_b_bits);
-        
-    out_bits.resize(sz, m().mk_false());
-    
-#if 1
-    bool last = false, now;
-    for (unsigned i = 0; i < sz; i++) {
-        now = m().is_true(a_bits[i]);
-        SASSERT(now || m().is_false(a_bits[i]));
-        tmp.reset();
-
-        if (now && !last) {            
-            mk_adder(sz - i, out_bits.data() + i, minus_b_bits.data(), tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j)); // do not use [], it does not work on Linux.
-        }
-        else if (!now && last) {
-            mk_adder(sz - i, out_bits.data() + i, b_bits, tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j)); // do not use [], it does not work on Linux.
-        }
-        
-        last = now; 
-    }
-#else
-    // Radix 4 Booth encoder
-    // B = b_bits, -B = minus_b_bits
-    // 2B = b2_bits, -2B = minus_b2_bits
-
-    expr_ref_vector b2_bits(m());
-    expr_ref_vector minus_b2_bits(m());
-
-    b2_bits.push_back(m().mk_false());
-    minus_b2_bits.push_back(m().mk_false());
-    for (unsigned i = 0; i < sz-1; i++) {
-        b2_bits.push_back(b_bits[i]);
-        minus_b2_bits.push_back(minus_b_bits.get(i));
-    }
-
-    bool last=false, now1, now2;
-    for (unsigned i = 0; i < sz; i += 2) {
-        now1 = m().is_true(a_bits[i]);
-        now2 = m().is_true(a_bits[i+1]);
-        SASSERT(now1 || m().is_false(a_bits[i]));
-        SASSERT(now2 || m().is_false(a_bits[i+1]));
-        tmp.reset();
-
-        if ((!now2 && !now1 && last) ||
-            (!now2 && now1 && !last)) { // Add B
-            mk_adder(sz - i, out_bits.c_ptr() + i, b_bits, tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j));
-        }
-        else if (!now2 && now1 && last) { // Add 2B
-            mk_adder(sz - i, out_bits.c_ptr() + i, b2_bits.c_ptr(), tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j));
-        }
-        else if (now2 && !now1 && !last) { // Add -2B
-            mk_adder(sz - i, out_bits.c_ptr() + i, minus_b2_bits.c_ptr(), tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j));
-        }
-        else if ((now2 && !now1 && last) ||
-                 (now2 && now1 && !last)) { // Add -B        
-            mk_adder(sz - i, out_bits.c_ptr() + i, minus_b_bits.c_ptr(), tmp);
-            for (unsigned j = 0; j < (sz - i); j++)
-                out_bits.set(i+j, tmp.get(j));
-        }
-        
-        last = now2; 
-    }
-#endif
-
-    TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
-                                     tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
-
-    SASSERT(out_bits.size() == sz);
-    return true;
-}

src/ast/rewriter/bool_rewriter.cpp

@@ -721,9 +721,18 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
             result = m().mk_false();
             return BR_DONE;
         }
+
+	    if (m().is_not(rhs))
+            std::swap(lhs, rhs);
+	
+	    if (m().is_not(lhs, lhs)) {
+	        result = m().mk_not(m().mk_eq(lhs, rhs));
+	        return BR_REWRITE2;
+        }
+	    
         if (unfolded) {
             result = mk_eq(lhs, rhs);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
 
         expr *la, *lb, *ra, *rb;

src/ast/rewriter/bool_rewriter.h

@@ -137,6 +137,11 @@ public:
         mk_eq(lhs, rhs, r);
         return r;
     }
+    expr_ref mk_xor(expr* a, expr* b) {
+       expr_ref result(m());
+       mk_xor(a, b, result);
+       return result;
+    }
     void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
     void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
     void mk_and(unsigned num_args, expr * const * args, expr_ref & result) {
@@ -169,6 +174,16 @@ public:
         mk_and(args.size(), args.data(), result);
         return result;
     }
+    expr_ref mk_and(expr* a, expr* b) {
+        expr_ref result(m());
+        mk_and(a, b, result);
+        return result;     
+    }
+    expr_ref mk_or(expr* a, expr* b) {
+        expr_ref result(m());
+        mk_or(a, b, result);
+        return result;     
+    }
 
     void mk_and(expr * arg1, expr * arg2, expr_ref & result) {
         expr * args[2] = {arg1, arg2};

src/ast/rewriter/der.cpp

@@ -136,8 +136,12 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
     var * v = nullptr;
     expr_ref t(m);
 
-    if (m.is_or(e)) {
+    if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) 
-        unsigned num_args = to_app(e)->get_num_args();
+        r = m.mk_false();
+    else {
+        expr_ref_vector ors(m);
+        flatten_or(e, ors);
+        unsigned num_args = ors.size();
         unsigned diseq_count = 0;
         unsigned largest_vinx = 0;
 
@@ -149,7 +153,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
 
         // Find all disequalities
         for (unsigned i = 0; i < num_args; i++) {
-            if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) {
+            if (is_var_diseq(ors.get(i), num_decls, v, t)) {
                 unsigned idx = v->get_idx();
                 if (m_map.get(idx, nullptr) == nullptr) {
                     m_map.reserve(idx + 1);
@@ -170,7 +174,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
 
             if (!m_order.empty()) {
                 create_substitution(largest_vinx + 1);
-                apply_substitution(q, r);
+                apply_substitution(q, ors, r);
             }
         }
         else {
@@ -180,11 +184,6 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
     }
     // Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
     // So, we must perform a occurs check here.
-    else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) {
-        r = m.mk_false();
-    }
-    else
-        r = q;
 
     if (m.proofs_enabled()) {
         pr = r == q ? nullptr : m.mk_der(q, r);
@@ -327,9 +326,8 @@ void der::create_substitution(unsigned sz) {
     }
 }
 
-void der::apply_substitution(quantifier * q, expr_ref & r) {
+void der::apply_substitution(quantifier * q, expr_ref_vector& ors, expr_ref & r) {
-    expr * e = q->get_expr();
+    unsigned num_args = ors.size();
-    unsigned num_args=to_app(e)->get_num_args();
 
     // get a new expression
     m_new_args.reset();
@@ -338,13 +336,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
         if (x != -1 && m_map.get(x) != nullptr)
             continue; // this is a disequality with definition (vanishes)
 
-        m_new_args.push_back(to_app(e)->get_arg(i));
+        m_new_args.push_back(ors.get(i));
     }
 
-    unsigned sz = m_new_args.size();
+    expr_ref t(mk_or(m, m_new_args.size(), m_new_args.data()), m);
-    expr_ref t(m);
+    expr_ref new_e = m_subst(t, m_subst_map);
-    t = (sz == 1) ? m_new_args[0] : m.mk_or(sz, m_new_args.data());
-    expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.data());
 
     // don't forget to update the quantifier patterns
     expr_ref_buffer  new_patterns(m);

src/ast/rewriter/der.h

@@ -147,7 +147,7 @@ class der {
 
     void get_elimination_order();
     void create_substitution(unsigned sz);
-    void apply_substitution(quantifier * q, expr_ref & r);
+    void apply_substitution(quantifier * q, expr_ref_vector& ors, expr_ref & r);
 
     void reduce1(quantifier * q, expr_ref & r, proof_ref & pr);
 

src/ast/rewriter/th_rewriter.cpp

@@ -52,21 +52,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     arith_util          m_a_util;
     bv_util             m_bv_util;
     expr_safe_replace   m_rep;
-    bool                m_new_subst { false };
     expr_ref_vector     m_pinned;
-    unsigned long long  m_max_memory; // in bytes
-    unsigned            m_max_steps;    
-    bool                m_pull_cheap_ite;
-    bool                m_flat;
-    bool                m_cache_all;
-    bool                m_push_ite_arith;
-    bool                m_push_ite_bv;
-    bool                m_ignore_patterns_on_ground_qbody;
-    bool                m_rewrite_patterns;
-
       // substitution support
     expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
-    expr_substitution * m_subst;
+    expr_substitution * m_subst = nullptr;
+    unsigned long long  m_max_memory; // in bytes
+    bool                m_new_subst = false;
+    unsigned            m_max_steps = UINT_MAX;    
+    bool                m_pull_cheap_ite = true;
+    bool                m_flat = true;
+    bool                m_cache_all = false;
+    bool                m_push_ite_arith = true;
+    bool                m_push_ite_bv = true;
+    bool                m_ignore_patterns_on_ground_qbody = true;
+    bool                m_rewrite_patterns = true;
+
 
     ast_manager & m() const { return m_b_rw.m(); }
 
@@ -805,8 +805,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_bv_util(m),
         m_rep(m),
         m_pinned(m),
-        m_used_dependencies(m),
+        m_used_dependencies(m) {
-        m_subst(nullptr) {
         updt_local_params(p);
     }
 

src/cmd_context/cmd_context.cpp

@@ -1194,6 +1194,59 @@ bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * c
     return false;
 }
 
+bool cmd_context::try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const {
+    sort_ref_vector binding(m());
+    auto match = [&](sort* s, sort* ps) {
+        if (ps == s)
+            return true;
+        if (m().is_uninterp(ps) && ps->get_name().is_numerical()) {
+            int index = ps->get_name().get_num();
+            if (index < 0)
+                return false;
+            binding.reserve(index + 1);
+            if (binding.get(index) && binding.get(index) != s)
+                return false;
+            binding[index] = s;
+            return true;
+        }
+        // Other matching is TBD
+        return false;
+    };
+    datatype::util dt(m());
+    func_decl_ref fn(m());
+    for (auto* c : dt.plugin().get_constructors(s)) {
+        if (c->accessors().size() != num_args)
+            continue;
+        binding.reset();
+        unsigned i = 0;
+        for (auto* a : *c) 
+            if (!match(args[i++]->get_sort(), a->range()))
+                goto match_failure;
+        if (binding.size() != c->get_def().params().size())
+            goto match_failure;
+        for (auto* b : binding)
+            if (!b)
+                goto match_failure;
+        
+        fn = c->instantiate(binding);
+        r = m().mk_app(fn, num_args, args);
+        return true;
+    match_failure:
+        ;
+    }    
+    if (num_args != 1)
+        return false;
+
+    for (auto* a : dt.plugin().get_accessors(s)) {        
+        fn = a->instantiate(args[0]->get_sort());
+        r = m().mk_app(fn, num_args, args);
+        return true;
+    }
+    
+    return false;
+}
+
+
 void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * args, 
                          unsigned num_indices, parameter const * indices, sort * range,
                          expr_ref & result) const {
@@ -1206,6 +1259,8 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
         return;    
     if (try_mk_builtin_app(s, num_args, args, num_indices, indices, range, result)) 
         return;
+    if (!range && try_mk_pdecl_app(s, num_args, args, num_indices, indices, result))
+        return;
     
     std::ostringstream buffer;
     buffer << "unknown constant " << s;
@@ -1899,7 +1954,7 @@ void cmd_context::complete_model(model_ref& md) const {
             SASSERT(!v->has_var_params());
             IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
             ptr_vector<sort> param_sorts(v->get_num_params(), m().mk_bool_sort());
-            sort * srt = v->instantiate(*m_pmanager, param_sorts.size(), param_sorts.data());
+            sort * srt = v->instantiate(pm(), param_sorts.size(), param_sorts.data());
             if (!md->has_uninterpreted_sort(srt)) {
                 expr * singleton = m().get_some_value(srt);
                 md->register_usort(srt, 1, &singleton);

src/cmd_context/cmd_context.h

@@ -425,6 +425,7 @@ public:
     bool try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args, 
                              unsigned num_indices, parameter const * indices, sort * range,
                              func_decls& fs, expr_ref & result) const;
+    bool try_mk_pdecl_app(symbol const & s, unsigned num_args, expr * const * args, unsigned num_indices, parameter const * indices, expr_ref & r) const;
     void erase_cmd(symbol const & s);
     void erase_func_decl(symbol const & s);
     void erase_func_decl(symbol const & s, func_decl * f);

src/model/datatype_factory.cpp

@@ -35,9 +35,8 @@ expr * datatype_factory::get_some_value(sort * s) {
     func_decl * c = m_util.get_non_rec_constructor(s);
     ptr_vector<expr> args;
     unsigned num  = c->get_arity();
-    for (unsigned i = 0; i < num; i++) {
+    for (unsigned i = 0; i < num; i++) 
         args.push_back(m_model.get_some_value(c->get_domain(i)));    
-    }
     expr * r = m_manager.mk_app(c, args);
     register_value(r);
     TRACE("datatype", tout << mk_pp(r, m_util.get_manager()) << "\n";);

src/model/model_core.cpp

@@ -125,3 +125,20 @@ void model_core::unregister_decl(func_decl * d) {
         dealloc(v);
     }
 }
+
+void model_core::add_lambda_defs() {
+    unsigned sz = get_num_decls();
+    for (unsigned i = sz; i-- > 0; ) {
+        func_decl* f = get_decl(i);
+        quantifier* q = m.is_lambda_def(f);
+        if (!q)
+            continue;
+        if (f->get_arity() > 0) {
+            func_interp* fi = alloc(func_interp, m, f->get_arity());
+            fi->set_else(q);
+            register_decl(f, fi);
+        }
+        else
+            register_decl(f, q);
+    }
+}

src/model/model_core.h

@@ -72,6 +72,8 @@ public:
     void unregister_decl(func_decl * d);
     func_interp* update_func_interp(func_decl* f, func_interp* fi);
 
+    void add_lambda_defs();
+
     virtual expr * get_some_value(sort * s) = 0;
     virtual expr * get_fresh_value(sort * s) = 0;
     virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;

src/opt/opt_context.cpp

@@ -266,6 +266,7 @@ namespace opt {
     }
 
     lbool context::optimize(expr_ref_vector const& _asms) {
+        scoped_time _st(*this);
         if (m_pareto) {
             return execute_pareto();
         }

src/opt/opt_context.h

@@ -117,6 +117,17 @@ namespace opt {
             {}
         };
 
+      double m_time = 0;      
+      class scoped_time {
+        context& c;
+        timer t;
+      public:
+        scoped_time(context& c):c(c) { c.m_time = 0; }
+        ~scoped_time() { c.m_time = t.get_seconds(); }
+      };
+
+
+
         class scoped_state {
             ast_manager& m;
             arith_util   m_arith;
@@ -261,6 +272,13 @@ namespace opt {
             m_on_model_eh  = on_model; 
         }
 
+      
+        void collect_timer_stats(statistics& st) const {
+	  if (m_time != 0) 
+	    st.update("time", m_time);
+	}
+
+
     private:
         lbool execute(objective const& obj, bool committed, bool scoped);
         lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);        
@@ -340,6 +358,8 @@ namespace opt {
         // quantifiers
         bool is_qsat_opt();
         lbool run_qsat_opt();
+
+      
     };
 
 }

src/qe/mbp/mbp_arith.cpp

@@ -552,10 +552,13 @@ namespace mbp {
             if (fmls.empty() || defs.empty())
                 return;
             expr_safe_replace subst(m);
-            for (auto const& d : defs) 
-                subst.insert(d.var, d.term);            
-            unsigned j = 0;
             expr_ref tmp(m);
+            for (unsigned i = defs.size(); i-- > 0; ) {
+                auto const& d = defs[i];
+                subst(d.term, tmp);
+                subst.insert(d.var, tmp);
+            }
+            unsigned j = 0;
             for (expr* fml : fmls) {
                 subst(fml, tmp);
                 fmls[j++] = tmp;

src/sat/sat_extension.h

@@ -120,7 +120,7 @@ namespace sat {
         virtual bool check_model(model const& m) const { return true; }
         virtual void gc_vars(unsigned num_vars) {}
         virtual bool should_research(sat::literal_vector const& core) { return false;}
-        virtual void add_assumptions() {}
+        virtual void add_assumptions(literal_set& ext_assumptions) {}
         virtual bool tracking_assumptions() { return false; }
         virtual bool enable_self_propagate() const { return false; }
 

src/sat/sat_solver.cpp

@@ -1895,9 +1895,7 @@ namespace sat {
             m_ext_assumption_set.reset();
             unsigned trail_size = m_trail.size();
             if (!inconsistent())
-                m_ext->add_assumptions();
+                m_ext->add_assumptions(m_ext_assumption_set);
-            for (unsigned i = trail_size; i < m_trail.size(); ++i)
-                m_ext_assumption_set.insert(m_trail[i]);
         }
     }
 
@@ -2225,6 +2223,7 @@ namespace sat {
     bool solver::should_restart() const {
         if (m_conflicts_since_restart <= m_restart_threshold) return false;
         if (scope_lvl() < 2 + search_lvl()) return false;
+        if (m_case_split_queue.empty()) return false;
         if (m_config.m_restart != RS_EMA) return true;
         return 
             m_fast_glue_avg + search_lvl() <= scope_lvl() && 
@@ -2315,9 +2314,9 @@ namespace sat {
     }
 
     unsigned solver::restart_level(bool to_base) {
-        if (to_base || scope_lvl() == search_lvl()) {
+        SASSERT(!m_case_split_queue.empty());
+        if (to_base || scope_lvl() == search_lvl()) 
             return scope_lvl() - search_lvl();        
-        }
         else {
             bool_var next = m_case_split_queue.min_var();
 

src/sat/smt/arith_solver.cpp

@@ -964,7 +964,7 @@ namespace arith {
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         SASSERT(lp().ax_is_correct());
 
-        if (lp().get_status() != lp::lp_status::OPTIMAL) {
+        if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
             switch (make_feasible()) {
             case l_false:
                 get_infeasibility_explanation_and_set_conflict();

src/sat/smt/array_axioms.cpp

@@ -120,9 +120,15 @@ namespace array {
         app* select = r.select->get_app();
         SASSERT(a.is_select(select));
         SASSERT(can_beta_reduce(r.n));
-        TRACE("array", display(tout << "select-axiom: ", r) << "\n";);
 
-        if (get_config().m_array_delay_exp_axiom && r.select->get_arg(0)->get_root() != r.n->get_root() && !r.is_delayed() && m_enable_delay) {
+        bool should_delay = 
+            get_config().m_array_delay_exp_axiom && 
+            r.select->get_arg(0)->get_root() != r.n->get_root() && 
+            !r.is_delayed() && m_enable_delay;
+
+        TRACE("array", display(tout << "select-axiom: " << (should_delay ? "delay " : ""), r) << "\n";);
+
+        if (should_delay) {
             IF_VERBOSE(11, verbose_stream() << "delay: " << mk_bounded_pp(child, m) << " " << mk_bounded_pp(select, m) << "\n");
             ctx.push(reset_new(*this, idx));
             r.set_delayed();
@@ -175,19 +181,15 @@ namespace array {
         ptr_buffer<expr> sel1_args, sel2_args;
         unsigned num_args = select->get_num_args();
 
-        if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) 
-            return false;
         bool has_diff = false;
         for (unsigned i = 1; i < num_args; i++) 
             has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
         if (!has_diff)
             return false;
 
-
         sel1_args.push_back(store);
         sel2_args.push_back(store->get_arg(0));       
         
-        
         for (unsigned i = 1; i < num_args; i++) {
             sel1_args.push_back(select->get_arg(i));
             sel2_args.push_back(select->get_arg(i));
@@ -209,7 +211,6 @@ namespace array {
               tout << "select-store " << ctx.bpp(s1) << " " << ctx.bpp(s1->get_root()) << "\n";
               tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";);
 
-
         if (s1->get_root() == s2->get_root())
             return new_prop;
         
@@ -272,7 +273,6 @@ namespace array {
      * e1 = e2 or select(e1, diff(e1,e2)) != select(e2, diff(e1, e2))
      */
     bool solver::assert_extensionality(expr* e1, expr* e2) {
-        TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n";);
         ++m_stats.m_num_extensionality_axiom;
         func_decl_ref_vector const& funcs = sort2diff(e1->get_sort());
         expr_ref_vector args1(m), args2(m);
@@ -287,6 +287,7 @@ namespace array {
         expr_ref sel2(a.mk_select(args2), m);
         literal lit1 = eq_internalize(e1, e2);
         literal lit2 = eq_internalize(sel1, sel2);
+        TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n" << lit1 << " " << ~lit2 << "\n";);
         return add_clause(lit1, ~lit2);
     }
 

src/sat/smt/array_model.cpp

@@ -22,6 +22,10 @@ Author:
 namespace array {
 
 
+    void solver::init_model() {
+        collect_defaults();
+    }
+    
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { 
         if (!a.is_array(n->get_expr())) {
             dep.insert(n, nullptr);
@@ -41,6 +45,10 @@ namespace array {
         for (euf::enode* k : euf::enode_class(n)) 
             if (a.is_const(k->get_expr())) 
                 dep.add(n, k->get_arg(0)); 
+        theory_var v = get_th_var(n);
+        euf::enode* d = get_default(v);
+        if (d)
+            dep.add(n, d);
         if (!dep.deps().contains(n))
             dep.insert(n, nullptr);
         return true;
@@ -57,6 +65,17 @@ namespace array {
         func_interp * fi = alloc(func_interp, m, arity);
         mdl.register_decl(f, fi);
 
+        theory_var v = get_th_var(n);
+        euf::enode* d = get_default(v);
+        if (d && !fi->get_else())
+            fi->set_else(values.get(d->get_root_id()));
+
+        if (!fi->get_else() && get_else(v))
+            fi->set_else(get_else(v));
+        
+#if 0
+        // this functionality is already taken care of by model_init.
+
         if (!fi->get_else())
             for (euf::enode* k : euf::enode_class(n))
                 if (a.is_const(k->get_expr()))
@@ -66,6 +85,7 @@ namespace array {
             for (euf::enode* p : euf::enode_parents(n))
                 if (a.is_default(p->get_expr()))
                     fi->set_else(values.get(p->get_root_id()));
+#endif
     
         if (!fi->get_else()) {
             expr* else_value = nullptr;
@@ -90,6 +110,9 @@ namespace array {
                 fi->set_else(else_value);
         }
 
+        if (!get_else(v) && fi->get_else())
+            set_else(v, fi->get_else());
+        
         for (euf::enode* p : euf::enode_parents(n)) {
             if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
                 expr* value = values.get(p->get_root_id(), nullptr);
@@ -175,4 +198,104 @@ namespace array {
         return table_diff(r1, r2, else1) || table_diff(r2, r1, else2);
     }
 
+    void solver::collect_defaults() {
+        unsigned num_vars = get_num_vars();
+        m_defaults.reset();
+        m_else_values.reset();
+        m_parents.reset();
+        m_parents.resize(num_vars, -1);
+        m_defaults.resize(num_vars);
+        m_else_values.resize(num_vars);
+    
+        //
+        // Create equivalence classes for defaults.
+        //
+        for (unsigned v = 0; v < num_vars; ++v) {
+            euf::enode * n  = var2enode(v);
+            expr* e = n->get_expr();
+                       
+            theory_var r = get_representative(v);
+
+            mg_merge(v, r);
+
+            if (a.is_const(e)) 
+                set_default(v, n->get_arg(0));
+            else if (a.is_store(e)) {
+                theory_var w = get_th_var(n->get_arg(0));
+                SASSERT(w != euf::null_theory_var);
+                mg_merge(v, get_representative(w));                                
+                TRACE("array", tout << "merge: " << ctx.bpp(n) << " " << v << " " << w << "\n";);
+            }
+            else if (a.is_default(e)) {
+                theory_var w = get_th_var(n->get_arg(0));
+                SASSERT(w != euf::null_theory_var);
+                set_default(w, n);
+            }
+        }
+    }
+
+    void solver::set_default(theory_var v, euf::enode* n) {
+        TRACE("array", tout << "set default: " << v << " " << ctx.bpp(n) << "\n";);
+        v = mg_find(v);
+        if (!m_defaults[v]) 
+            m_defaults[v] = n;
+    }
+
+    euf::enode* solver::get_default(theory_var v) {
+        return m_defaults[mg_find(v)];
+    }
+
+    void solver::set_else(theory_var v, expr* e) {
+        m_else_values[mg_find(v)] = e;
+    }
+
+    expr* solver::get_else(theory_var v) {
+        return m_else_values[mg_find(v)];
+    }
+
+    euf::theory_var solver::mg_find(theory_var n) {
+        if (m_parents[n] < 0) 
+            return n;
+        theory_var n0 = n;
+        n = m_parents[n0];
+        if (m_parents[n] < -1) 
+            return n;
+        while (m_parents[n] >= 0) 
+            n = m_parents[n];        
+        // compress path.
+        while (m_parents[n0] >= 0) {
+            theory_var n1 = m_parents[n0];
+            m_parents[n0] = n;
+            n0 = n1;
+        }
+        return n;
+    }
+
+    void solver::mg_merge(theory_var u, theory_var v) {
+        u = mg_find(u);
+        v = mg_find(v);
+        if (u != v) {
+            SASSERT(m_parents[u] < 0);
+            SASSERT(m_parents[v] < 0);
+            if (m_parents[u] > m_parents[v]) 
+                std::swap(u, v);
+            m_parents[u] += m_parents[v];
+            m_parents[v] = u;
+
+            if (!m_defaults[u]) 
+                m_defaults[u] = m_defaults[v];
+
+            CTRACE("array", m_defaults[v], 
+                   tout << ctx.bpp(m_defaults[v]->get_root()) << "\n";
+                   tout << ctx.bpp(m_defaults[u]->get_root()) << "\n";
+                  );
+
+            // NB. it may be the case that m_defaults[u] != m_defaults[v]
+            //     when m and n are finite arrays.
+
+        }
+    }
+
+
+
 }

src/sat/smt/array_solver.cpp

@@ -228,11 +228,8 @@ namespace array {
         
         auto& d = get_var_data(v);
 
-        for (euf::enode* lambda : d.m_lambdas) {
+        for (euf::enode* lambda : d.m_lambdas) 
-            expr* e = lambda->get_expr();
-            if (a.is_const(e) || a.is_map(e)) 
             propagate_select_axioms(d, lambda);        
-        }
         
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);
@@ -275,8 +272,7 @@ namespace array {
         return !get_config().m_array_delay_exp_axiom && d.m_prop_upward;
     }
 
-    bool solver::can_beta_reduce(euf::enode* n) const {
+    bool solver::can_beta_reduce(expr* c) const {
-        expr* c = n->get_expr();
         return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c);
     }
 }

src/sat/smt/array_solver.h

@@ -209,7 +209,8 @@ namespace array {
         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;
-        bool can_beta_reduce(euf::enode* n) const;
+        bool can_beta_reduce(euf::enode* n) const { return can_beta_reduce(n->get_expr()); }
+        bool can_beta_reduce(expr* e) const;
 
         var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
         var_data& get_var_data(theory_var v) { return *m_var_data[v]; }
@@ -218,7 +219,17 @@ namespace array {
         void pop_core(unsigned n) override;
         
         // models
+        euf::enode_vector   m_defaults;       // temporary field for model construction
+        ptr_vector<expr>    m_else_values;    // 
+        svector<int>        m_parents;        // temporary field for model construction
         bool have_different_model_values(theory_var v1, theory_var v2);
+        void collect_defaults();
+        void mg_merge(theory_var u, theory_var v);
+        theory_var mg_find(theory_var n);
+        void set_default(theory_var v, euf::enode* n);
+        euf::enode* get_default(theory_var v);
+        void set_else(theory_var v, expr* e);
+        expr* get_else(theory_var v);
 
         // diagnostics
         std::ostream& display_info(std::ostream& out, char const* id, euf::enode_vector const& v) const; 
@@ -243,6 +254,7 @@ namespace array {
         bool use_diseqs() const override { return true; }
         void new_diseq_eh(euf::th_eq const& eq) override;
         bool unit_propagate() override;
+        void init_model() override;
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;

src/sat/smt/bv_internalize.cpp

@@ -423,9 +423,9 @@ namespace bv {
         for (expr* b : k_bits) 
             args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero));        
         expr_ref sum(m_autil.mk_add(sz, args.data()), m);
-        expr_ref eq = mk_eq(n, sum);
+        sat::literal lit = eq_internalize(n, sum);
-        sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant);
 	add_unit(lit);
+	ctx.add_root(lit);
     }
 
     void solver::internalize_int2bv(app* n) {
@@ -453,9 +453,9 @@ namespace bv {
         unsigned sz = bv.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
         rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
-        expr_ref eq = mk_eq(lhs, rhs);
+	sat::literal eq_lit = eq_internalize(lhs, rhs);
-        TRACE("bv", tout << eq << "\n";);
+	add_unit(eq_lit);
-        add_unit(ctx.internalize(eq, false, false, m_is_redundant));
+	ctx.add_root(eq_lit);
        
         expr_ref_vector n_bits(m);
         get_bits(n_enode, n_bits);
@@ -466,9 +466,9 @@ namespace bv {
             rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
             rhs = mk_eq(rhs, m_autil.mk_int(1));
             lhs = n_bits.get(i);
-            expr_ref eq = mk_eq(lhs, rhs);
+	    eq_lit = eq_internalize(lhs, rhs);
-            TRACE("bv", tout << eq << "\n";);
+	    add_unit(eq_lit);
-            add_unit(ctx.internalize(eq, false, false, m_is_redundant));
+	    ctx.add_root(eq_lit);
         }
     }
 
@@ -530,15 +530,23 @@ namespace bv {
         expr* arg1 = n->get_arg(0);
         expr* arg2 = n->get_arg(1);
         mk_bits(get_th_var(n));
+	sat::literal eq_lit;
         if (p.hi_div0()) {
-            add_unit(eq_internalize(n, ibin(arg1, arg2)));
+            eq_lit = eq_internalize(n, ibin(arg1, arg2));
-            return;
+	    add_unit(eq_lit);
+	    ctx.add_root(eq_lit);
 	}
+	else {
 	    unsigned sz = bv.get_bv_size(n);
 	    expr_ref zero(bv.mk_numeral(0, sz), m);
-        expr_ref eq(m.mk_eq(arg2, zero), m);
+	    sat::literal eqZ = eq_internalize(arg2, zero);
-        expr_ref ite(m.mk_ite(eq, iun(arg1), ibin(arg1, arg2)), m);
+	    sat::literal eqU = mk_literal(iun(arg1));
-        add_unit(eq_internalize(n, ite));
+	    sat::literal eqI = mk_literal(ibin(arg1, arg2));
+	    add_clause(~eqZ, eqU);
+	    add_clause(eqZ, eqI);
+	    ctx.add_aux(~eqZ, eqU);
+	    ctx.add_aux(eqZ, eqI);
+	}
     }
 
     void solver::internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn) {
@@ -642,7 +650,9 @@ namespace bv {
             conc.push_back(arg);
         expr_ref r(bv.mk_concat(conc), m);
         mk_bits(get_th_var(e));
-        add_unit(eq_internalize(e, r));
+	sat::literal eq_lit = eq_internalize(e, r);
+        add_unit(eq_lit);
+	ctx.add_root(eq_lit);
     }
 
     void solver::internalize_bit2bool(app* n) {
@@ -752,8 +762,7 @@ namespace bv {
             expr_ref e1(m), e2(m);
             e1 = bv.mk_bit2bool(o1, i);
             e2 = bv.mk_bit2bool(o2, i);
-            expr_ref e = mk_eq(e1, e2);
+            literal eq = eq_internalize(e1, e2);
-            literal eq = ctx.internalize(e, false, false, m_is_redundant);
 	    add_clause(eq, ~oeq);
             eqs.push_back(~eq);
         }

src/sat/smt/euf_model.cpp

@@ -23,6 +23,7 @@ Author:
 namespace euf {
 
     class solver::user_sort {
+        solver& s;
         ast_manager& m;
         model_ref& mdl;
         expr_ref_vector& values;
@@ -31,7 +32,7 @@ namespace euf {
         obj_map<sort, expr_ref_vector*>    sort2values;
     public:
         user_sort(solver& s, expr_ref_vector& values, model_ref& mdl) :
-            m(s.m), mdl(mdl), values(values), factory(m) {}
+            s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
 
         ~user_sort() {
             for (auto kv : sort2values)
@@ -45,6 +46,7 @@ namespace euf {
                 value = r->get_expr();
             else
                 value = factory.get_fresh_value(srt);
+            TRACE("model", tout << s.bpp(r) << " := " << value << "\n";);
             values.set(id, value);
             expr_ref_vector* vals = nullptr;
             if (!sort2values.find(srt, vals)) {
@@ -261,6 +263,18 @@ namespace euf {
         return m_values.get(n->get_root_id(), nullptr);
     }
 
+    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";
+        for (auto* arg : euf::enode_args(n)) {
+            expr_ref val = mdl(arg->get_expr());
+            expr_ref sval(m);
+            th_rewriter rw(m);
+            rw(val, sval);
+            out << bpp(arg) << "\n" << sval << "\n";
+        }
+        out << mdl << "\n";
+    }
+
     void solver::validate_model(model& mdl) {
         bool first = true;
         for (enode* n : m_egraph.nodes()) {
@@ -276,18 +290,12 @@ namespace euf {
                 continue;
             if (!tt && !mdl.is_true(e))
                 continue;
-            IF_VERBOSE(0, 
+            IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
-                       verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
+            CTRACE("euf", first, display_validation_failure(tout, mdl, n););
-                       for (auto* arg : euf::enode_args(n))
-                           verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
-            CTRACE("euf", first, 
-                   tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
-                   s().display(tout);
-                   tout << mdl << "\n";);
             (void)first;
+            exit(1);
             first = false;
         }        
-        
     }
 
 

src/sat/smt/euf_solver.cpp

@@ -699,9 +699,9 @@ namespace euf {
         return result;
     }
 
-    void solver::add_assumptions() {
+    void solver::add_assumptions(sat::literal_set& assumptions) {
         for (auto* e : m_solvers)
-            e->add_assumptions();
+            e->add_assumptions(assumptions);
     }
 
     bool solver::tracking_assumptions() {

src/sat/smt/euf_solver.h

@@ -157,6 +157,7 @@ namespace euf {
         void collect_dependencies(user_sort& us, deps_t& deps);
         void values2model(deps_t const& deps, model_ref& mdl);
         void validate_model(model& mdl);
+        void display_validation_failure(std::ostream& out, model& mdl, enode* n);
 
         // solving
         void propagate_literals();
@@ -276,7 +277,7 @@ namespace euf {
         bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override;
         bool should_research(sat::literal_vector const& core) override;
-        void add_assumptions() override;
+        void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override;
 
         void propagate(literal lit, ext_justification_idx idx);

src/sat/smt/fpa_solver.cpp

@@ -83,6 +83,14 @@ namespace fpa {
         return conds;
     }
 
+    sat::check_result solver::check() {
+        SASSERT(m_converter.m_extra_assertions.empty());
+        if (unit_propagate())
+            return sat::check_result::CR_CONTINUE;
+        SASSERT(m_nodes.size() <= m_nodes_qhead);
+        return sat::check_result::CR_DONE;
+    }
+
     void solver::attach_new_th_var(enode* n) {
         theory_var v = mk_var(n);
         ctx.attach_th_var(n, this, v);
@@ -141,6 +149,8 @@ namespace fpa {
 
         if (is_attached_to_var(n))
             return;
+        if (m.is_ite(n->get_expr()))
+            return;
         attach_new_th_var(n);
 
         expr* owner = n->get_expr();
@@ -157,7 +167,6 @@ namespace fpa {
     }
 
     bool solver::unit_propagate() {
-
         if (m_nodes.size() <= m_nodes_qhead)
             return false;
         ctx.push(value_trail<unsigned>(m_nodes_qhead));
@@ -199,7 +208,7 @@ namespace fpa {
                 break;
             }
         }
-
+        activate(e);
     }
 
     void solver::activate(expr* n) {
@@ -207,7 +216,10 @@ namespace fpa {
 
         mpf_manager& mpfm = m_fpa_util.fm();
 
-        if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
+        if (m.is_ite(n)) {
+            // skip
+        }
+        else if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) {
             expr* a = nullptr, * b = nullptr, * c = nullptr;
             if (!m_fpa_util.is_fp(n)) {
                 app_ref wrapped = m_converter.wrap(n);
@@ -223,12 +235,13 @@ namespace fpa {
                     VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c));
                     expr* args[] = { a, b, c };
                     expr_ref cc_args(m_bv_util.mk_concat(3, args), m);
+                    // Require
+                    // wrap(n) = bvK
+                    // fp(extract(wrap(n)) = n
                     add_unit(eq_internalize(wrapped, cc_args));
+                    add_unit(eq_internalize(bv_val_e, n));
                     add_units(mk_side_conditions());
                 }
-                else if (m.is_ite(n)) {
-                    // pass
-                }
                 else 
                     add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n));                
             }
@@ -313,6 +326,7 @@ namespace fpa {
         expr* e = n->get_expr();
         app_ref wrapped(m);
         expr_ref value(m);
+        
         auto is_wrapped = [&]() {
             if (!wrapped) wrapped = m_converter.wrap(e);
             return expr2enode(wrapped) != nullptr;
@@ -345,6 +359,7 @@ namespace fpa {
             value = m_fpa_util.mk_pzero(ebits, sbits);
         }
         values.set(n->get_root_id(), value);
+        TRACE("t_fpa", tout << ctx.bpp(n) << " := " << value << "\n";);
     }
 
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {

src/sat/smt/fpa_solver.h

@@ -72,7 +72,7 @@ namespace fpa {
 
         bool unit_propagate() override;
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
-        sat::check_result check() override { return sat::check_result::CR_DONE; }
+      sat::check_result check() override;
 
         euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
 

src/sat/smt/q_eval.cpp

@@ -105,13 +105,19 @@ namespace q {
             return l_undef;
         if (!sn && !tn) 
             return compare_rec(n, binding, s, t, evidence);
+
+        // in recursive calls we ensure the first argument is decomposed
+        if (!tn && sn && m_freeze_swap)
+            return l_undef;
+        flet<bool> _freeze_swap(m_freeze_swap, true);
         if (!tn && sn) {
             std::swap(tn, sn);
             std::swap(t, s);
         }        
         unsigned sz = evidence.size();
         for (euf::enode* t1 : euf::enode_class(tn)) {      
-            if (c = compare_rec(n, binding, s, t1->get_expr(), evidence), c != l_undef) {
+            expr* t2 = t1->get_expr();
+            if ((c = compare_rec(n, binding, s, t2, evidence), c != l_undef)) {
                 evidence.push_back(euf::enode_pair(t1, tn));
                 return c;
             }

src/sat/smt/q_eval.h

@@ -30,6 +30,7 @@ namespace q {
         expr_fast_mark1    m_mark;
         euf::enode_vector  m_eval;
         euf::enode_vector  m_indirect_nodes;
+        bool               m_freeze_swap = false;
 
         struct scoped_mark_reset;
 

src/sat/smt/q_mam.cpp

@@ -3413,7 +3413,7 @@ namespace q {
             unsigned num_vars = qa->get_num_decls();
             if (num_vars >= m_var_paths.size())
                 m_var_paths.resize(num_vars+1);
-            for (unsigned i = 0; i < num_vars; i++)
+            for (unsigned i = 0; i <= num_vars; i++)
                 m_var_paths[i].reset();
             m_tmp_region.reset();
             // Given a multi-pattern (p_1, ..., p_n)

src/sat/smt/q_mbi.cpp

@@ -321,7 +321,7 @@ namespace q {
             eqs.push_back(m.mk_eq(v, val));
         }
         rep(fmls);
-        TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs;);
+        TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs << "\n";);
         return mk_and(fmls);
     }
 

src/sat/smt/recfun_solver.cpp

@@ -279,13 +279,18 @@ namespace recfun {
         return true;
     }
 
-    void solver::add_assumptions() {
+    void solver::add_assumptions(sat::literal_set& assumptions) {
         if (u().has_defs() || m_disabled_guards.empty()) {
             app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
             TRACEFN("add_theory_assumption " << dlimit);
-            s().assign_scoped(mk_literal(dlimit));
+            sat::literal assumption = mk_literal(dlimit); 
-            for (auto g : m_disabled_guards)
+            assumptions.insert(assumption);
-                s().assign_scoped(~mk_literal(g));
+            s().assign_scoped(assumption);
+            for (auto g : m_disabled_guards) {
+                assumption = ~mk_literal(g);
+                assumptions.insert(assumption);
+                s().assign_scoped(assumption);
+            }
         }
     }
     

src/sat/smt/recfun_solver.h

@@ -108,7 +108,7 @@ namespace recfun {
         bool is_shared(euf::theory_var v) const override { return true; }
         void init_search() override {}
         bool should_research(sat::literal_vector const& core) override;
-        void add_assumptions() override;
+        void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override { return true; }
     };
 }

src/sat/smt/sat_th.cpp

@@ -102,6 +102,11 @@ namespace euf {
         return get_th_var(ctx.get_enode(e));
     }
 
+    theory_var th_euf_solver::get_representative(theory_var v) const {
+        euf::enode* r = var2enode(v)->get_root();
+        return get_th_var(r);
+    }
+    
     void th_euf_solver::push_core() {
         m_var2enode_lim.push_back(m_var2enode.size());
     }

src/sat/smt/sat_th.h

@@ -182,6 +182,7 @@ namespace euf {
         sat::literal mk_literal(expr* e) const;
         theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
         theory_var get_th_var(expr* e) const;
+        theory_var get_representative(theory_var v) const;
         trail_stack& get_trail_stack();
         bool is_attached_to_var(enode* n) const;
         bool is_root(theory_var v) const { return var2enode(v)->is_root(); }

src/smt/CMakeLists.txt

@@ -30,7 +30,6 @@ z3_add_component(smt
     smt_farkas_util.cpp
     smt_for_each_relevant_expr.cpp
     smt_implied_equalities.cpp
-    smt_induction.cpp
     smt_internalizer.cpp
     smt_justification.cpp
     smt_kernel.cpp

src/smt/smt_context.cpp

@@ -137,6 +137,8 @@ namespace smt {
         for (unsigned i = 0; i < src_af.get_num_formulas(); ++i) {
             expr_ref fml(dst_m);
             proof_ref pr(dst_m);
+            if (src_m.is_true(src_af.get_formula(i)))
+               continue;
             proof* pr_src = src_af.get_formula_proof(i);
             fml = tr(src_af.get_formula(i));
             if (pr_src) {
@@ -159,6 +161,8 @@ namespace smt {
             }
             expr_ref fml0(src_m), fml1(dst_m);
             src_ctx.literal2expr(lit, fml0);
+            if (src_m.is_true(fml0))
+                continue;
             fml1 = tr(fml0.get());
             dst_ctx.assert_expr(fml1);
         }
@@ -1667,16 +1671,6 @@ namespace smt {
             !m_th_diseq_propagation_queue.empty();
     }
 
-    /**
-       \brief retrieve facilities for creating induction lemmas.
-     */
-    induction& context::get_induction() {
-        if (!m_induction) {
-            m_induction = alloc(induction, *this, get_manager());
-        }
-        return *m_induction;
-    }
-
     /**
        \brief unit propagation.
        Cancelation is not safe during propagation at base level because
@@ -2886,7 +2880,7 @@ namespace smt {
         solver::push_eh_t&       push_eh,
         solver::pop_eh_t&        pop_eh,
         solver::fresh_eh_t&      fresh_eh) {
-        setup_context(m_fparams.m_auto_config);
+        setup_context(false);
         m_user_propagator = alloc(user_propagator, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; ) 

src/smt/smt_context.h

@@ -33,7 +33,6 @@ Revision History:
 #include "smt/smt_statistics.h"
 #include "smt/smt_conflict_resolution.h"
 #include "smt/smt_relevancy.h"
-#include "smt/smt_induction.h"
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
@@ -184,7 +183,6 @@ namespace smt {
         unsigned                    m_simp_qhead { 0 };
         int                         m_simp_counter { 0 }; //!< can become negative
         scoped_ptr<case_split_queue> m_case_split_queue;
-        scoped_ptr<induction>       m_induction;
         double                      m_bvar_inc { 1.0 };
         bool                        m_phase_cache_on { true };
         unsigned                    m_phase_counter { 0 }; //!< auxiliary variable used to decide when to turn on/off phase caching
@@ -1323,7 +1321,6 @@ namespace smt {
     public:
         bool can_propagate() const;
 
-        induction& get_induction(); 
 
         // Retrieve arithmetic values. 
         bool get_arith_lo(expr* e, rational& lo, bool& strict);

src/smt/smt_model_checker.cpp

@@ -425,6 +425,12 @@ namespace smt {
         TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
         tout << "model:\n"; model_pp(tout, *m_curr_model););
 
+        for (quantifier* q : *m_qm)
+            if (m.is_lambda_def(q)) {
+                md->add_lambda_defs();
+                break;
+            }
+	
         md->compress();
 
         TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";

src/smt/theory_fpa.cpp

@@ -454,6 +454,11 @@ namespace smt {
                     expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
                     cc_args = m_bv_util.mk_concat(3, args);
                     c = m.mk_eq(wrapped, cc_args);
+		    // NB code review: #5454 exposes a bug in fpa_solver that
+		    // could be latent here as well. It needs also the equality
+		    // n == bv_val_e to be asserted such that whenever something is assigned th
+		    // bit-vector value cc_args it is equated with n
+		    // I don't see another way this constraint would be enforced.
                     assert_cnstr(c);
                     assert_cnstr(mk_side_conditions());
                 }

src/smt/theory_recfun.h

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include "util/scoped_ptr_vector.h"
 #include "smt/smt_theory.h"
 #include "smt/smt_context.h"
 #include "ast/ast_pp.h"

src/smt/theory_seq.cpp

@@ -3191,10 +3191,8 @@ void theory_seq::relevant_eh(app* n) {
 
     if (m_util.str.is_replace_all(n) ||
         m_util.str.is_replace_re(n) ||
-        m_util.str.is_replace_re_all(n) ||
+        m_util.str.is_replace_re_all(n)
-        // m_util.str.is_from_code(n) ||
+        ) {
-        // m_util.str.is_to_code(n) ||
-        m_util.str.is_is_digit(n)) {
         add_unhandled_expr(n);
     }
 }

src/tactic/core/reduce_invertible_tactic.cpp

@@ -238,6 +238,8 @@ private:
             }
         }
         else {            
+            if (!is_uninterp_const(fst_arg))
+                return false;
             bool first = true;
             for (expr* arg : *a) {
                 if (!is_app(arg))

src/test/bit_blaster.cpp

@@ -17,9 +17,12 @@ Revision History:
 
 --*/
 
-#include "ast/rewriter/bit_blaster/bit_blaster.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/reg_decl_plugins.h"
+#include "ast/rewriter/bit_blaster/bit_blaster.h"
+#include "model/model.h"
+#include "model/model_evaluator.h"
 
 void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) {
     sort_ref b(m);
@@ -36,38 +39,153 @@ void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector
 }
 
 void display(std::ostream & out, expr_ref_vector & r, bool ll=true) {
-    ast_mark v;
     for (unsigned i = 0; i < r.size(); i++) {
+        out << "bit " << i << ":\n";
         if (ll)
-            ast_ll_pp(out, r.get_manager(), r.get(i), v);
+            ast_ll_pp(out, r.get_manager(), r.get(i));
         else
-            out << mk_pp(r.get(i), r.get_manager());
+            out << mk_pp(r.get(i), r.get_manager()) << "\n";
-        out << "\n";
     }
 }
 
-void tst_adder(ast_manager & m, unsigned sz) {
+static unsigned to_int(model_core & mdl, expr_ref_vector & out) {
-//     expr_ref_vector a(m);
+    SASSERT(out.size() <= sizeof(unsigned) * 8);
-//     expr_ref_vector b(m);
+    ast_manager & m = mdl.get_manager();
-//     expr_ref_vector c(m);
+    model_evaluator eval(mdl);
-//     mk_bits(m, "a", sz, a);
+    expr_ref bit(m);
-//     mk_bits(m, "b", sz, b);
+    unsigned actual = 0;
-//     bool t = true;
+    for (unsigned i = 0; i < out.size(); i++) {
-//     bit_blaster blaster(m, t);
+        eval(out.get(i), bit);
-//     blaster.mk_adder(sz, a.c_ptr(), b.c_ptr(), c);
+        if (m.is_true(bit))
-//     TRACE("bit_blaster", display(tout, c););
+            actual |= 1 << i;
+        else
+            ENSURE(m.is_false(bit));
+    }
+    return actual;
 }
 
-void tst_multiplier(ast_manager & m, unsigned sz) {
+#define ENSURE_INT(mdl, out, expected) \
-//     expr_ref_vector a(m);
+    do { \
-//     expr_ref_vector b(m);
+        unsigned actual = to_int(mdl, out); \
-//     expr_ref_vector c(m);
+        TRACE("bit_blaster", \
-//     mk_bits(m, "a", sz, a);
+            display(tout, out); \
-//     mk_bits(m, "b", sz, b);
+            tout << "expected=" << (expected) << ", actual=" << actual << "\n"; \
-//     bool t = true;
+        ); \
-//     bit_blaster blaster(m, t);
+        ENSURE(actual == (expected)); \
-//     blaster.mk_multiplier(sz, a.c_ptr(), b.c_ptr(), c);
+    } while (0)
-//     TRACE("bit_blaster", display(tout, c););
+
+void tst_adder(ast_manager & m, bit_blaster & blaster) {
+    model mdl(m);
+    expr_ref_vector c(m);
+    app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m);
+    app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m);
+    expr_ref not_b1(m.mk_not(b1), m);
+
+    {
+        expr * const a[] = { b1, b1, b1 };
+        expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() };
+        c.reset();
+        blaster.mk_adder(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 6); // b000 + b110
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 5); // b111 + b110
+
+    {
+        expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() };
+        expr * const b[] = { b1, not_b1, m.mk_false() };
+        c.reset();
+        blaster.mk_adder(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 0); // b110 + b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 7); // b110 + b001
+
+    {
+        expr * const a[] = { b1, b2, m.mk_true() };
+        expr * const b[] = { b1, not_b1, m.mk_false() };
+        c.reset();
+        blaster.mk_adder(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    mdl.register_decl(b2->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 6); // b100 + b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    mdl.register_decl(b2->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 0); // b110 + b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    mdl.register_decl(b2->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 6); // b101 + b001
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    mdl.register_decl(b2->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 0); // b111 + b001
+}
+
+void tst_multiplier(ast_manager & m, bit_blaster & blaster) {
+    model mdl(m);
+    expr_ref_vector c(m);
+    app_ref b1(m.mk_const("b1", m.mk_bool_sort()), m);
+    app_ref b2(m.mk_const("b2", m.mk_bool_sort()), m);
+    expr_ref not_b1(m.mk_not(b1), m);
+
+    {
+        expr * const a[] = { b1, b1, b1 };
+        expr * const b[] = { m.mk_false(), m.mk_true(), m.mk_true() };
+        c.reset();
+        blaster.mk_multiplier(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 0); // b000 * b110
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 2); // b111 * b110
+
+    {
+        expr * const a[] = { m.mk_false(), m.mk_true(), m.mk_true() };
+        expr * const b[] = { b1, not_b1, m.mk_false() };
+        c.reset();
+        blaster.mk_multiplier(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 4); // b110 * b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 6); // b110 * b001
+
+    {
+        expr * const a[] = { b1, b2, m.mk_true() };
+        expr * const b[] = { b1, not_b1, m.mk_false() };
+        c.reset();
+        blaster.mk_multiplier(3, a, b, c);
+    }
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    mdl.register_decl(b2->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 0); // b100 * b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_false());
+    mdl.register_decl(b2->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 4); // b110 * b010
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    mdl.register_decl(b2->get_decl(), m.mk_false());
+    ENSURE_INT(mdl, c, 5); // b101 * b001
+
+    mdl.register_decl(b1->get_decl(), m.mk_true());
+    mdl.register_decl(b2->get_decl(), m.mk_true());
+    ENSURE_INT(mdl, c, 7); // b111 * b001
 }
 
 void tst_le(ast_manager & m, unsigned sz) {
@@ -115,8 +233,12 @@ void tst_sh(ast_manager & m, unsigned sz) {
 
 void tst_bit_blaster() {
     ast_manager m;
-    tst_adder(m, 4);
+    reg_decl_plugins(m);
-    tst_multiplier(m, 4);
+    bit_blaster_params params;
+    bit_blaster blaster(m, params);
+
+    tst_adder(m, blaster);
+    tst_multiplier(m, blaster);
     tst_le(m, 4);
     tst_eqs(m, 8);
     tst_sh(m, 4);

src/util/mpz.cpp

@@ -566,12 +566,13 @@ void mpz_manager<SYNCH>::machine_div_rem(mpz const & a, mpz const & b, mpz & q,
 template<bool SYNCH>
 void mpz_manager<SYNCH>::machine_div(mpz const & a, mpz const & b, mpz & c) {
     STRACE("mpz", tout << "[mpz-ext] machine-div(" << to_string(a) << ",  " << to_string(b) << ") == ";); 
-    if (is_small(a) && is_small(b)) {
+    if (is_small(b) && i64(b) == 0)
+        throw default_exception("division by 0"); 
+
+    if (is_small(a) && is_small(b)) 
         set_i64(c, i64(a) / i64(b));
-    }
+    else 
-    else {
         big_div(a, b, c);
-    }
     STRACE("mpz", tout << to_string(c) << "\n";);
 }
 

src/util/mutex.h

@@ -16,6 +16,8 @@ Abstract:
 
 template<typename T> using atomic = T;
 
+#define ATOMIC_EXCHANGE(ret, var, val) ret = var; var = val
+
 struct mutex {
   void lock() {}
   void unlock() {}
@@ -38,6 +40,7 @@ template<typename T> using atomic = std::atomic<T>;
 typedef std::mutex mutex;
 typedef std::lock_guard<std::mutex> lock_guard;
 
+#define ATOMIC_EXCHANGE(ret, var, val) ret = var.exchange(val)
 #define DECLARE_MUTEX(name) mutex *name = nullptr
 #define DECLARE_INIT_MUTEX(name) mutex *name = new mutex
 #define ALLOC_MUTEX(name) name = alloc(mutex)