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

src/api/python/z3/z3.py

@@ -6470,7 +6470,25 @@ class ModelRef(Z3PPObject):
                     return None
                 r = _to_expr_ref(_r, self.ctx)
                 if is_as_array(r):
-                    return self.get_interp(get_as_array_func(r))
+                    fi = self.get_interp(get_as_array_func(r))
+                    if fi is None:
+                        return fi                    
+                    e = fi.else_value()
+                    if e is None:
+                        return fi
+                    if fi.arity() != 1:
+                        return fi
+                    srt = decl.range()
+                    dom =  srt.domain()
+                    e = K(dom, e)
+                    i = 0
+                    sz = fi.num_entries()
+                    n = fi.arity()
+                    while i < sz:
+                        fe = fi.entry(i)
+                        e = Store(e, fe.arg_value(0), fe.value())
+                        i += 1
+                    return e
                 else:
                     return r
             else:

src/ast/ast.h

@@ -272,6 +272,7 @@ public:
 
     family_id get_family_id() const { return m_family_id; }
     decl_kind get_decl_kind() const { return m_kind; }
+    bool is_decl_of(family_id fid, decl_kind k) const { return m_family_id == fid && k == m_kind; }
     unsigned get_num_parameters() const { return m_parameters.size(); }
     parameter const & get_parameter(unsigned idx) const { return m_parameters[idx]; }
     parameter const * get_parameters() const { return m_parameters.begin(); }
@@ -577,6 +578,7 @@ public:
     decl_info * get_info() const { return m_info; }
     family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
     decl_kind get_decl_kind() const { return m_info == nullptr ? null_decl_kind : m_info->get_decl_kind(); }
+    bool is_decl_of(family_id fid, decl_kind k) const { return m_info && m_info->is_decl_of(fid, k); }
     unsigned get_num_parameters() const { return m_info == nullptr ? 0 : m_info->get_num_parameters(); }
     parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
     parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
@@ -718,7 +720,7 @@ public:
     unsigned get_num_parameters() const { return get_decl()->get_num_parameters(); }
     parameter const& get_parameter(unsigned idx) const { return get_decl()->get_parameter(idx); }
     parameter const* get_parameters() const { return get_decl()->get_parameters(); }
-    bool is_app_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
+    bool is_app_of(family_id fid, decl_kind k) const { return m_decl->is_decl_of(fid, k); }
     unsigned get_num_args() const { return m_num_args; }
     expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
     expr * const * get_args() const { return m_args; }

src/ast/bv_decl_plugin.cpp

@@ -423,7 +423,8 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
     // This cannot be enforced now, since some Z3 modules try to generate these invalid numerals.
     // After SMT-COMP, I should find all offending modules.
     // For now, I will just simplify the numeral here.
-    parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
+    rational v = parameters[0].get_rational();
+    parameter p0(mod2k(v, bv_size));
     parameter ps[2] = { std::move(p0), parameters[1] };
     sort * bv = get_bv_sort(bv_size);
     return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
@@ -641,16 +642,18 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
         offset = decl->get_parameter(0).get_rational();
         sz     = decl->get_parameter(1).get_int();
         t      = a->get_arg(1);
-        offset = mod(offset, rational::power_of_two(sz));
+        offset = mod2k(offset, sz);
     }
     else {
         t      = a;
-        offset = rational(0);
+        offset.reset();
     }
 }
 
 bool bv_decl_plugin::are_distinct(app * a, app * b) const {
-#if 1
+    if (decl_plugin::are_distinct(a, b))
+        return true;
+    
     // Check for a + k1 != a + k2   when k1 != k2
     rational a_offset;
     expr *   a_term;
@@ -665,8 +668,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const {
           tout << "b: " << b_offset << " + " << mk_ismt2_pp(b_term, *m_manager) << "\n";);
     if (a_term == b_term && a_offset != b_offset)
         return true;
-#endif
+    return false;    
-    return decl_plugin::are_distinct(a, b);
 }
 
 void bv_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
@@ -752,7 +754,7 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
 }
 
 rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
-    rational r = mod(val, rational::power_of_two(bv_size));
+    rational r = mod2k(val, bv_size);
     SASSERT(!r.is_neg());
     if (is_signed) {        
         if (r >= rational::power_of_two(bv_size - 1)) {

src/ast/rewriter/array_rewriter.cpp

@@ -23,6 +23,7 @@ Notes:
 #include "ast/ast_ll_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "params/array_rewriter_params.hpp"
+#include "util/util.h"
 
 void array_rewriter::updt_params(params_ref const & _p) {
     array_rewriter_params p(_p);
@@ -162,6 +163,7 @@ br_status array_rewriter::mk_store_core(unsigned num_args, expr * const * args,
     return BR_FAILED;
 }
 
+
 br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(num_args >= 2);
     if (m_util.is_store(args[0])) {
@@ -172,9 +174,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
             result = to_app(args[0])->get_arg(num_args);
             return BR_DONE;
         case l_false: {
+            expr* arg0 = to_app(args[0])->get_arg(0);
+            while (m_util.is_store(arg0) && compare_args<true>(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
+                arg0 = to_app(arg0)->get_arg(0);
+            }
+            
             // select(store(a, I, v), J) --> select(a, J) if I != J
             ptr_buffer<expr> new_args;
-            new_args.push_back(to_app(args[0])->get_arg(0));
+            new_args.push_back(arg0);
             new_args.append(num_args-1, args+1);
             result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.data());
             return BR_REWRITE1;

src/ast/rewriter/bv_rewriter.cpp

@@ -1736,7 +1736,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         unsigned low = 0;
         unsigned i = 0;
         while (i < sz) {
-            while (i < sz && mod(v1, two).is_one()) {
+            while (i < sz && v1.is_odd()) {
                 i++;
                 div(v1, two, v1);
             }
@@ -1745,7 +1745,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
                 exs.push_back(m_util.mk_numeral(rational::power_of_two(num_sz) - numeral(1), num_sz));
                 low = i;
             }
-            while (i < sz && mod(v1, two).is_zero()) {
+            while (i < sz && v1.is_even()) {
                 i++;
                 div(v1, two, v1);
             }

src/util/rational.h

@@ -237,6 +237,12 @@ public:
         rational::m().mod(r1.m_val, r2.m_val, r.m_val);
     }
 
+    friend inline rational mod2k(rational const & a, unsigned k) {
+        if (a.is_nonneg() && a.is_int() && a.bitsize() <= k) 
+            return a;
+        return mod(a, power_of_two(k));
+    }
+
     friend inline rational operator%(rational const & r1, rational const & r2) {
         rational r;
         rational::m().rem(r1.m_val, r2.m_val, r.m_val);

src/util/scoped_timer.cpp

@@ -80,27 +80,20 @@ scoped_timer::scoped_timer(unsigned ms, event_handler * eh) {
         return;
 
     workers.lock();
-    bool new_worker = false;
     if (available_workers.empty()) {
+        // start new thead
         workers.unlock();
         s = new scoped_timer_state;
-        new_worker = true;
         ++num_workers;
-        s->work = WORKING;
+        init_state(ms, eh);
-    }
-    else {
-        s = available_workers.back();
-        available_workers.pop_back();
-        s->work = WORKING;
-        workers.unlock();
-    }
-    s->ms = ms;
-    s->eh = eh;
-    s->m_mutex.lock();
-    if (new_worker) {
         s->m_thread = std::thread(thread_func, s);
     }
     else {
+        // re-use existing thread
+        s = available_workers.back();
+        available_workers.pop_back();
+        init_state(ms, eh);
+        workers.unlock();
         s->cv.notify_one();
     }
 }
@@ -148,3 +141,10 @@ void scoped_timer::finalize() {
     num_workers = 0;
     available_workers.clear();
 }
+
+void scoped_timer::init_state(unsigned ms, event_handler * eh) {
+    s->ms = ms;
+    s->eh = eh;
+    s->m_mutex.lock();
+    s->work = WORKING;
+}

src/util/scoped_timer.h

@@ -29,6 +29,8 @@ public:
     ~scoped_timer();
     static void initialize();
     static void finalize();
+private:
+    void init_state(unsigned ms, event_handler * eh);
 };
 
 /*