fix evaluator for array store expressions

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

src/ast/rewriter/array_rewriter.cpp

@@ -26,6 +26,7 @@ void array_rewriter::updt_params(params_ref const & _p) {
     m_sort_store = p.sort_store();
     m_expand_select_store = p.expand_select_store();
     m_expand_store_eq = p.expand_store_eq();
+    m_expand_select_ite = false;
 }
 
 void array_rewriter::get_param_descrs(param_descrs & r) {
@@ -201,6 +202,17 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         result = m().mk_app(f, num_args - 1, args + 1);
         return BR_REWRITE1;
     }
+
+    expr* c, *th, *el;
+    if (m_expand_select_ite && m().is_ite(args[0], c, th, el)) {
+        ptr_vector<expr> args1, args2;
+        args1.push_back(th);
+        args1.append(num_args-1, args + 1);
+        args2.push_back(el);
+        args2.append(num_args-1, args + 1);
+        result = m().mk_ite(c, m_util.mk_select(num_args, args1.c_ptr()), m_util.mk_select(num_args, args2.c_ptr()));
+        return BR_REWRITE2;
+    }
     
     return BR_FAILED;
 }

src/ast/rewriter/array_rewriter.h

@@ -32,6 +32,7 @@ class array_rewriter {
     bool          m_sort_store;
     bool          m_expand_select_store;
     bool          m_expand_store_eq;
+    bool          m_expand_select_ite;
     template<bool CHECK_DISEQ>
     lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
 public:    
@@ -43,6 +44,8 @@ public:
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }
 
+    void set_expand_select_store(bool f) { m_expand_select_store = f; }
+    void set_expand_select_ite(bool f) { m_expand_select_ite = f; }
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
 

src/model/model_evaluator.cpp

@@ -32,6 +32,7 @@ Revision History:
 #include"cooperate.h"
 #include"ast_pp.h"
 #include"ast_util.h"
+#include"model_smt2_pp.h"
 
 
 struct evaluator_cfg : public default_rewriter_cfg {
@@ -69,6 +70,8 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_a_rw.set_flat(flat);
         m_bv_rw.set_flat(flat);
         m_bv_rw.set_mkbv2num(true);
+        m_ar_rw.set_expand_select_store(true);
+        m_ar_rw.set_expand_select_ite(true);
         updt_params(p);
     }
 
@@ -400,6 +403,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         SASSERT(m_ar.is_array(a));
         bool are_values = true;
         are_unique = true;
+        TRACE("model_evaluator", tout << mk_pp(a, m()) << "\n";);
 
         while (m_ar.is_store(a)) {
             expr_ref_vector store(m());
@@ -438,13 +442,28 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }        
         else_case = g->get_else();
         if (!else_case) {
-            TRACE("model_evaluator", tout << "no else case " << 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;
         }
+        if (m_ar.is_as_array(else_case)) {
+            bool are_unique1 = true;
+            expr_ref tmp(m());
+            unsigned num_stores = stores.size();
+            if (!extract_array_func_interp(else_case, stores, tmp, are_unique1)) {
+                stores.shrink(num_stores);
+            }
+            else {
+                sort* srt = m().get_sort(else_case);
+                else_case = m_ar.mk_const_array(srt, tmp);
+                are_unique &= are_unique1;
+            }
+        }
         for (unsigned i = stores.size(); are_values && i > 0; ) {
             --i;
             if (m().are_equal(else_case, stores[i].back())) {

src/smt/theory_array.cpp

@@ -404,7 +404,7 @@ namespace smt {
                     r = assert_delayed_axioms();
             }
         }
-        TRACE("as_array", tout << "m_found_unsupported_op: " << m_found_unsupported_op << " " << r << "\n";);
+        TRACE("array", tout << "m_found_unsupported_op: " << m_found_unsupported_op << " " << r << "\n";);
         if (r == FC_DONE && m_found_unsupported_op) 
             r = FC_GIVEUP;
         return r;

src/smt/theory_array_base.cpp

@@ -33,7 +33,7 @@ namespace smt {
     }
 
     void theory_array_base::found_unsupported_op(expr * n) {
-        TRACE("theory_array_unsup", tout << mk_ll_pp(n, get_manager()) << "\n";);
+        TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);
         if (!m_found_unsupported_op) {
             get_context().push_trail(value_trail<context, bool>(m_found_unsupported_op));
             m_found_unsupported_op = true;