use array interpretations whenever possible for #2378. Also strengthen equality test for lambda

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

src/ast/rewriter/array_rewriter.cpp

@@ -19,6 +19,7 @@ Notes:
 #include "ast/rewriter/array_rewriter.h"
 #include "ast/rewriter/array_rewriter_params.hpp"
 #include "ast/ast_lt.h"
+#include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "ast/rewriter/var_subst.h"
 
@@ -566,6 +567,15 @@ bool array_rewriter::has_index_set(expr* e, expr_ref& else_case, vector<expr_ref
             else_case = m().mk_false();
             return true;
         }
+        if (!is_ground(e) && m().is_and(e)) {
+            for (expr* arg : *to_app(e)) {
+                if (!add_store(args, num_idxs, arg, m().mk_true(), stores)) {
+                    return false;
+                }                            
+            }
+            else_case = m().mk_true();
+            return true;
+        }
         while (!is_ground(e) && m().is_ite(e, e1, store_val, e3) && is_ground(store_val)) {            
             if (!add_store(args, num_idxs, e1, store_val, stores)) {
                 return false;
@@ -584,13 +594,16 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
     ptr_vector<expr> eqs;    
     args.reset();
     args.resize(num_idxs + 1, nullptr);
+    bool is_not = m().is_bool(store_val) && m().is_not(e, e);
+
     eqs.push_back(e);
     for (unsigned i = 0; i < eqs.size(); ++i) {
         e = eqs[i];
         if (m().is_and(e)) {
             eqs.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            continue;
         }
-        else if (m().is_eq(e, e1, e2)) {
+        if (m().is_eq(e, e1, e2)) {
             if (is_var(e2)) {
                 std::swap(e1, e2);
             }
@@ -601,11 +614,16 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e
             else {
                 return false;
             }
-        }                
+            continue;
+        }    
+        return false;
     }
     for (unsigned i = 0; i < num_idxs; ++i) {
         if (!args.get(i)) return false;
     }
+    if (is_not) {
+        store_val = mk_not(m(), store_val);
+    }
     args[num_idxs] = store_val;
     stores.push_back(args);
     return true;

src/model/func_interp.cpp

@@ -75,7 +75,8 @@ func_interp::func_interp(ast_manager & m, unsigned arity):
     m_arity(arity),
     m_else(nullptr),
     m_args_are_values(true),
-    m_interp(nullptr) {
+    m_interp(nullptr),
+    m_array_interp(nullptr) {
 }
 
 func_interp::~func_interp() {
@@ -84,6 +85,7 @@ func_interp::~func_interp() {
     }
     m_manager.dec_ref(m_else);
     m_manager.dec_ref(m_interp);
+    m_manager.dec_ref(m_array_interp);
 }
 
 func_interp * func_interp::copy() const {
@@ -98,7 +100,9 @@ func_interp * func_interp::copy() const {
 
 void func_interp::reset_interp_cache() {
     m_manager.dec_ref(m_interp);
+    m_manager.dec_ref(m_array_interp);
     m_interp = nullptr;
+    m_array_interp = nullptr;
 }
 
 bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
@@ -317,36 +321,6 @@ bool func_interp::is_identity() const {
     return (sz.size() == m_entries.size() + 1);
 }
 
-expr_ref func_interp::get_array_interp(sort_ref_vector const& domain) const {
-    if (m_else == nullptr) 
-        return expr_ref(m_manager);
-    if (!is_ground(m_else)) {
-        return expr_ref(m_manager);
-    }
-    array_util autil(m_manager);
-    sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager);
-    expr_ref r(autil.mk_const_array(A, m_else), m_manager);
-    expr_ref_vector args(m_manager);
-    for (func_entry * curr : m_entries) {
-        expr * res = curr->get_result();
-
-        if (m_else == res) {
-            continue;
-        }
-        args.reset();
-        args.push_back(r);        
-        for (unsigned i = 0; i < m_arity; i++) {
-            expr* arg = curr->get_arg(i);
-            if (!is_ground(arg)) {
-                return expr_ref(m_manager);
-            }
-            args.push_back(arg);
-        }
-        args.push_back(res);
-        r = autil.mk_store(args.size(), args.c_ptr());
-    }
-    return r;    
-}
 
 expr * func_interp::get_interp_core() const {
     if (m_else == nullptr)
@@ -382,6 +356,57 @@ expr * func_interp::get_interp_core() const {
     return r;
 }
 
+expr* func_interp::get_array_interp_core(func_decl * f) const {
+    if (m_else == nullptr) 
+        return nullptr;
+    ptr_vector<sort> domain;
+    for (sort* s : *f) {
+        domain.push_back(s);
+    }
+    expr* r;
+
+    bool ground = is_ground(m_else);
+    for (func_entry * curr : m_entries) {
+        ground &= is_ground(curr->get_result());
+        for (unsigned i = 0; i < m_arity; i++) {
+            ground &= is_ground(curr->get_arg(i));
+        }
+    }
+    if (!ground) {
+        r = get_interp();
+        if (!r) return r;
+        sort_ref_vector vars(m_manager);
+        svector<symbol> var_names;
+        for (unsigned i = 0; i < m_arity; ++i) {
+            var_names.push_back(symbol(i));
+            vars.push_back(domain.get(m_arity - i - 1));
+        }
+        r = m_manager.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), r);        
+        return r;
+    }
+
+    expr_ref_vector args(m_manager);
+    array_util autil(m_manager);
+    sort_ref A(autil.mk_array_sort(domain.size(), domain.c_ptr(), m_manager.get_sort(m_else)), m_manager);
+    r = autil.mk_const_array(A, m_else);
+    for (func_entry * curr : m_entries) {
+        expr * res = curr->get_result();
+
+        if (m_else == res) {
+            continue;
+        }
+        args.reset();
+        args.push_back(r);        
+        for (unsigned i = 0; i < m_arity; i++) {
+            args.push_back(curr->get_arg(i));
+        }
+        args.push_back(res);
+        r = autil.mk_store(args.size(), args.c_ptr());
+    }
+    return r;    
+}
+
+   
 expr * func_interp::get_interp() const {
     if (m_interp != nullptr)
         return m_interp;
@@ -393,6 +418,17 @@ expr * func_interp::get_interp() const {
     return r;
 }
 
+expr * func_interp::get_array_interp(func_decl * f) const {
+    if (m_array_interp != nullptr)
+        return m_array_interp;
+    expr* r = get_array_interp_core(f);
+    if (r != nullptr) {
+        const_cast<func_interp*>(this)->m_array_interp = r;
+        m_manager.inc_ref(m_array_interp);
+    }
+    return r;
+}
+
 func_interp * func_interp::translate(ast_translation & translator) const {
     func_interp * new_fi = alloc(func_interp, translator.to(), m_arity);
 

src/model/func_interp.h

@@ -73,10 +73,14 @@ class func_interp {
 
     expr *                 m_interp; //!< cache for representing the whole interpretation as a single expression (it uses ite terms).
 
+    expr *                 m_array_interp; // <! interp with lambda abstraction
+
     void reset_interp_cache();
 
     expr * get_interp_core() const;
 
+    expr * get_array_interp_core(func_decl * f) const;
+
 public:
     func_interp(ast_manager & m, unsigned arity);
     ~func_interp();
@@ -112,7 +116,7 @@ public:
 
     expr * get_interp() const;
 
-    expr_ref get_array_interp(sort_ref_vector const& domain) const;
+    expr * get_array_interp(func_decl* f) const;
 
     func_interp * translate(ast_translation & translator) const;
 

src/model/model.cpp

@@ -418,10 +418,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
                 // only expand auxiliary definitions that occur once.
                 if (can_inline_def(ts, f)) {
                     fi = get_func_interp(f);
-                    for (sort* s : *f) {
+                    new_t = fi->get_array_interp(f);
-                        domain.push_back(s);
-                    }
-                    new_t = fi->get_array_interp(domain);
                     TRACE("model", tout << "array interpretation:" << new_t << "\n";);
                 }
             }
@@ -429,17 +426,6 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
             if (new_t) {
                 // noop
             }
-            else if (fi && fi->get_interp()) {
-                f = autil.get_as_array_func_decl(a);
-                expr_ref_vector sargs(m);
-                sort_ref_vector vars(m);
-                svector<symbol> var_names;
-                for (unsigned i = 0; i < f->get_arity(); ++i) {
-                    var_names.push_back(symbol(i));
-                    vars.push_back(f->get_domain(f->get_arity() - i - 1));
-                }
-                new_t = m.mk_lambda(vars.size(), vars.c_ptr(), var_names.c_ptr(), fi->get_interp());
-            }
             else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) && 
                      fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
                 var_subst vs(m, false);

src/model/model_evaluator.cpp

@@ -150,6 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
             expr * val = m_model.get_const_interp(f);
             if (val != nullptr) {
                 result = val;
+                // return BR_DONE;
                 return m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
             }
             else if (m_model_completion) {
@@ -243,19 +244,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 result = def;
                 return BR_DONE;
             }
-            if (get_macro(g, def, q, def_pr)) {
+            func_interp * fi = m_model.get_func_interp(g);
-                sort_ref_vector sorts(m);
+            if (fi && (result = fi->get_array_interp(g))) {
-                expr_ref_vector vars(m);
-                svector<symbol> var_names;
-                unsigned sz = g->get_arity();
-                for (unsigned i = 0; i < sz; ++i) {
-                    var_names.push_back(symbol(sz - i - 1));
-                    vars.push_back(m.mk_var(sz - i - 1, g->get_domain(i)));
-                    sorts.push_back(g->get_domain(i));
-                }
-                var_subst subst(m, false);
-                result = subst(def, sorts.size(), vars.c_ptr());
-                result = m.mk_lambda(sorts.size(), sorts.c_ptr(), var_names.c_ptr(), result);
                 model_evaluator ev(m_model, m_params);
                 result = ev(result);
                 m_pinned.push_back(result);
@@ -530,47 +520,34 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
         func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
         func_interp* g = m_model.get_func_interp(f);
-        if (!g) return false;
+        if (!g) return false;        
+        else_case = g->get_else();
+        if (!else_case) {
+            TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);
+            return false;
+        }
+        bool ground = is_ground(else_case);
         unsigned sz = g->num_entries();
-        unsigned arity = f->get_arity();
+        expr_ref_vector store(m);
-        unsigned base_sz = stores.size();
         for (unsigned i = 0; i < sz; ++i) {
-            expr_ref_vector store(m);
+            store.reset();
             func_entry const* fe = g->get_entry(i);
-            store.append(arity, fe->get_args());
+            expr* res = fe->get_result();
-            store.push_back(fe->get_result());
+            if (m.are_equal(else_case, res)) {
-            for (unsigned j = 0; j < store.size(); ++j) {
+                continue;
-                if (!is_ground(store[j].get())) {
+            }
-                    TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m) << "\n" << mk_pp(store[j].get(), m) << "\n";);
+            ground &= is_ground(res);
-                    return false;
+            store.append(g->get_arity(), fe->get_args());
-                }
+            store.push_back(res);
+            for (expr* arg : store) {
+                ground &= is_ground(arg);
             }
             stores.push_back(store);
         }
-        else_case = g->get_else();
+        if (!ground) {
-        if (!else_case) {
+            TRACE("model_evaluator", tout << "could not extract ground array interpretation: " << mk_pp(a, m) << "\n";);
-            TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";
-                  /*model_smt2_pp(tout, m, m_model, 0);*/
-                  );
             return false;
         }
-        if (!is_ground(else_case)) {
-            TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m) << "\n" << else_case << "\n";);
-            return false;
-        }
-        for (unsigned i = stores.size(); are_values && i > base_sz; ) {
-            --i;
-            if (m.are_equal(else_case, stores[i].back())) {
-                for (unsigned j = i + 1; j < stores.size(); ++j) {
-                    stores[j-1].reset();
-                    stores[j-1].append(stores[j]);
-                }
-                stores.pop_back();
-                continue;
-            }
-            are_values &= args_are_values(stores[i], are_unique);
-        }
-        TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
         return true;
     }
 };

src/qe/qe_arrays.cpp

@@ -515,9 +515,8 @@ namespace qe {
          * ...
          */
         unsigned get_nesting_depth(app* eq) {
-            SASSERT(m.is_eq(eq));
+            expr* lhs = nullptr, *rhs = nullptr;
-            expr* lhs = eq->get_arg (0);
+            VERIFY(m.is_eq(eq, lhs, rhs));
-            expr* rhs = eq->get_arg (1);
             bool lhs_has_v = (lhs == m_v || m_has_stores_v.is_marked (lhs));
             bool rhs_has_v = (rhs == m_v || m_has_stores_v.is_marked (rhs));
             app* store = nullptr;
@@ -537,9 +536,13 @@ namespace qe {
             }
 
             unsigned nd = 0; // nesting depth
-            for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0)))
+            for (nd = 1; m_arr_u.is_store (store); nd++, store = to_app (store->get_arg (0))) {
                 /* empty */ ;
-            SASSERT (store == m_v);
+            }
+            if (store != m_v) {
+                TRACE("qe", tout << "not a store " << mk_pp(eq, m) << " " << lhs_has_v << " " << rhs_has_v << " " << mk_pp(m_v, m) << "\n";);
+                return UINT_MAX;
+            }
             return nd;
         }