fix #3860 fix #3861

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

src/ast/rewriter/array_rewriter.cpp

@@ -644,6 +644,8 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
 bool array_rewriter::is_expandable_store(expr* s) {
     unsigned count = 0;
     unsigned depth = 0;
+    if (false && !is_ground(s))
+        return false;
     while (m_util.is_store(s)) {
         s = to_app(s)->get_arg(0);
         count += s->get_ref_count();
@@ -653,8 +655,11 @@ bool array_rewriter::is_expandable_store(expr* s) {
 }
 
 expr_ref array_rewriter::expand_store(expr* s) {
+    sort* srt = m().get_sort(s);    
+    unsigned arity = get_array_arity(srt);
     ptr_vector<app> stores;
-    expr_ref result(m());
+    expr_ref result(m()), tmp(m());
+    var_shifter sh(m());
     while (m_util.is_store(s)) {
         stores.push_back(to_app(s));
         s = to_app(s)->get_arg(0);
@@ -663,9 +668,9 @@ expr_ref array_rewriter::expand_store(expr* s) {
     expr_ref_vector args(m()), eqs(m());
     ptr_vector<sort> sorts;
     svector<symbol> names;
-    sort* srt = m().get_sort(s);    
+    sh(s, arity, tmp);
-    args.push_back(s);
+    args.push_back(tmp);
-    for (unsigned i = get_array_arity(srt); i-- > 0; ) {
+    for (unsigned i = arity; i-- > 0; ) {
         args.push_back(m().mk_var(i, get_array_domain(srt, i)));
         sorts.push_back(get_array_domain(srt, i));
         names.push_back(symbol(i));
@@ -676,9 +681,11 @@ expr_ref array_rewriter::expand_store(expr* s) {
     for (app* st : stores) {
         eqs.reset();
         for (unsigned i = 1; i < args.size(); ++i) {
-            eqs.push_back(m().mk_eq(args.get(i), st->get_arg(i)));
+            sh(st->get_arg(i), arity, tmp);
+            eqs.push_back(m().mk_eq(args.get(i), tmp));
         }
-        result = m().mk_ite(mk_and(eqs), st->get_arg(args.size()), result);
+        sh(st->get_arg(args.size()), arity, tmp);
+        result = m().mk_ite(mk_and(eqs), tmp, result);
     }
     result = m().mk_lambda(sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
     return result;

src/ast/rewriter/bv_trailing.cpp

@@ -17,6 +17,7 @@
 #include "ast/rewriter/bv_trailing.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 
 // The analyzer gives up analysis after going TRAILING_DEPTH deep.
 // This number shouldn't be too big.
@@ -69,6 +70,7 @@ struct bv_trailing::imp {
         }
         expr_ref out1(m);
         expr_ref out2(m);
+        TRACE("bv-trailing", tout << min << "\n";);
         VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH));
         VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH));
         const bool are_eq = m.are_equal(out1, out2);
@@ -152,13 +154,11 @@ struct bv_trailing::imp {
         if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one())
             new_args.push_back(std::move(tmp));
 
-
         if (new_sz == 0) {
             result = nullptr;
             return retv;
         }
 
-
         for (unsigned i = 1; i < num; i++) {
             expr * const curr = a->get_arg(i);
             new_args.push_back(m_mk_extract(new_sz - 1, 0, curr));
@@ -168,6 +168,7 @@ struct bv_trailing::imp {
         case 1: result = new_args.get(0); break;
         default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr());
         }
+        SASSERT(retv == m_util.get_bv_size(result));
         return retv;
     }
 
@@ -179,22 +180,28 @@ struct bv_trailing::imp {
         }
         const unsigned num  = a->get_num_args();
         unsigned retv = 0;
-        unsigned i = num;
+        unsigned i;
         expr_ref new_last(nullptr, m);
-        while (i && retv < n) {
+        for (i = num; retv < n && i-- > 0; ) {  
-            i--;
+            new_last = nullptr;
             expr * const curr = a->get_arg(i);
-            const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
+            unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1);
-            const unsigned curr_sz = m_util.get_bv_size(curr);
+            unsigned curr_sz = m_util.get_bv_size(curr);
             retv += cur_rm;
-            if (cur_rm < curr_sz) break;
+            if (cur_rm < curr_sz) {
+                break;
+            }            
         }
+
         if (retv == 0) {
             result = a;
             return 0;
         }
 
-        if (!i && !new_last) {// all args eaten completely
+        if (i == 0 && retv != m_util.get_bv_size(a))
+            new_last = a->get_arg(0);
+
+        if (i == 0 && !new_last) { // all args eaten completely
             SASSERT(retv == m_util.get_bv_size(a));
             result = nullptr;
             return retv;
@@ -222,7 +229,10 @@ struct bv_trailing::imp {
 
     unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) {
         SASSERT(m_util.is_bv(e));
-        if (!depth || !n) {
+        if (depth == 0) {            
+            return 0;
+        }
+        if (n == 0) {
             return 0;
         }
         unsigned sz;

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -54,6 +54,7 @@ struct enum2bv_rewriter::imp {
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
             expr_ref a0(m), a1(m);
             expr_ref_vector _args(m);
+            result_pr = nullptr;
             if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) {
                 result = m.mk_eq(a0, a1);
                 return BR_DONE;
@@ -201,7 +202,8 @@ struct enum2bv_rewriter::imp {
                                      q->get_weight(), q->get_qid(), q->get_skid(), 
                                      q->get_num_patterns(), new_patterns,
                                      q->get_num_no_patterns(), new_no_patterns);
-            result_pr = nullptr;
+            if (m.proofs_enabled())
+                result_pr = m.mk_rewrite(q, result);
             return true;
         }
 

src/ast/rewriter/rewriter_def.h

@@ -47,8 +47,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
                tout << "index " << index << " bindings " << m_bindings.size() << "\n";
                display_bindings(tout););
         SASSERT(v->get_sort() == m().get_sort(r));
-        if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {
+        if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {            
-            
             unsigned shift_amount = m_bindings.size() - m_shifts[index];
             expr* c = get_cached(r, shift_amount);
             if (c) {
@@ -58,8 +57,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
                 expr_ref tmp(m());
                 m_shifter(r, shift_amount, tmp);
                 result_stack().push_back(tmp);
-                TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n";
+                TRACE("rewriter", display_bindings(tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n"););
-                      display_bindings(tout););
                 cache_shifted_result(r, shift_amount, tmp);                    
             }
         }
@@ -514,14 +512,12 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     SASSERT(fr.m_state == PROCESS_CHILDREN);
     unsigned num_decls = q->get_num_decls();
     if (fr.m_i == 0) {
-        if (!ProofGen) {
+        begin_scope();
-            begin_scope();
+        m_root       = q->get_expr();
-            m_root       = q->get_expr();
+        unsigned sz = m_bindings.size();
-            unsigned sz = m_bindings.size();
+        for (unsigned i = 0; i < num_decls; i++) {
-            for (unsigned i = 0; i < num_decls; i++) {
+            m_bindings.push_back(nullptr);
-                m_bindings.push_back(nullptr);
+            m_shifts.push_back(sz);
-                m_shifts.push_back(sz);
-            }
         }
         m_num_qvars += num_decls;
     }
@@ -595,17 +591,11 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     result_stack().shrink(fr.m_spos);
     result_stack().push_back(m_r.get());
     SASSERT(m().get_sort(q) == m().get_sort(m_r));
-    if (!ProofGen) {
+    SASSERT(num_decls <= m_bindings.size());
-        SASSERT(num_decls <= m_bindings.size());
+    m_bindings.shrink(m_bindings.size() - num_decls);
-        m_bindings.shrink(m_bindings.size() - num_decls);
+    m_shifts.shrink(m_shifts.size() - num_decls);
-        m_shifts.shrink(m_shifts.size() - num_decls);
+    end_scope();
-        end_scope();
+    cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
-        cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
-    }
-    else {
-        cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
-        m_pr = nullptr;
-    }
     m_r = nullptr;
     frame_stack().pop_back();
     set_new_child_flag(q, m_r);

src/ast/rewriter/var_subst.cpp

@@ -41,7 +41,7 @@ expr_ref var_subst::operator()(expr * n, unsigned num_args, expr * const * args)
           tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m_reducer.m()) << "\nusing\n";
           for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m_reducer.m()) << "\n";
           tout << "\n------>\n";
-          tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
+          tout << result << "\n";);
     return result;
 }
 
@@ -119,7 +119,6 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
             var_mapping.push_back(nullptr);
     }
 
-
     // Remark:
     // (VAR 0) should be in the last position of var_mapping.
     // ...
@@ -215,10 +214,8 @@ static void get_free_vars_offset(expr_sparse_mark& mark, ptr_vector<expr>& todo,
             break;
         }
         case AST_APP: {
-            app* a = to_app(e);
+            for (expr* arg : *to_app(e))  
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                todo.push_back(arg);            
-                todo.push_back(a->get_arg(i));
-            }
             break;
         }
         default:

src/smt/theory_array_base.cpp

@@ -401,8 +401,21 @@ namespace smt {
         quantifier * q = m.is_lambda_def(e->get_decl());
         expr_ref f(e, m);
         if (q) {
-            var_subst sub(m);
+            // the variables in q are maybe not consecutive.
-            f = sub(q, e->get_num_args(), e->get_args());
+            var_subst sub(m, false);
+            expr_free_vars fv;
+            fv(q);
+            expr_ref_vector es(m);
+            es.resize(fv.size());
+            for (unsigned i = 0, j = 0; i < e->get_num_args(); ++i) {
+                SASSERT(j < es.size());
+                while (!fv[j]) {
+                    ++j; 
+                    SASSERT(j < es.size());
+                }
+                es[j++] = e->get_arg(i);
+            }
+            f = sub(q, es.size(), es.c_ptr());
         }
         return f;
     }