Issue #354. Fix unsoundness in Array theory based on missing propagation of selects over ite expressions

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

src/smt/proto_model/proto_model.cpp

@@ -174,6 +174,13 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu
     return true;
 }
 
+bool proto_model::is_select_of_model_value(expr* e) const {
+    return 
+        is_app_of(e, m_afid, OP_SELECT) && 
+        is_as_array(to_app(e)->get_arg(0)) &&
+        has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0))));
+}
+
 /**
    \brief Evaluate the expression e in the current model, and store the result in \c result.
    It returns \c true if succeeded, and false otherwise. If the evaluation fails,
@@ -257,7 +264,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
                         m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
                         TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
                         trail.push_back(new_t);
-                        if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
+                        if (!is_app(new_t) || to_app(new_t)->get_decl() != f || is_select_of_model_value(new_t)) {
                             // if the result is not of the form (f ...), then assume we must simplify it.
                             expr * new_new_t = 0;
                             if (!eval_cache.find(new_t.get(), new_new_t)) {
@@ -588,7 +595,7 @@ void proto_model::register_value(expr * n) {
     }
 }
 
-bool proto_model::is_array_value(expr * v) const {
+bool proto_model::is_as_array(expr * v) const {
     return is_app_of(v, m_afid, OP_AS_ARRAY);
 }
 

src/smt/proto_model/proto_model.h

@@ -59,6 +59,7 @@ class proto_model : public model_core {
     void remove_aux_decls_not_in_set(ptr_vector<func_decl> & decls, func_decl_set const & s);
     void cleanup_func_interp(func_interp * fi, func_decl_set & found_aux_fs);
 
+    bool is_select_of_model_value(expr* e) const;
 
 public:
     proto_model(ast_manager & m, simplifier & s, params_ref const & p = params_ref());
@@ -68,7 +69,7 @@ public:
 
     bool eval(expr * e, expr_ref & result, bool model_completion = false);
 
-    bool is_array_value(expr * v) const;
+    bool is_as_array(expr * v) const;
     
     value_factory * get_factory(family_id fid);
 

src/smt/smt_context.cpp

@@ -4126,6 +4126,7 @@ namespace smt {
             if (m_fparams.m_model_compact)
                 m_proto_model->compress();
             TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
+            SASSERT(validate_model());
         }
     }
 

src/smt/smt_context.h

@@ -1415,6 +1415,8 @@ namespace smt {
         bool update_model(bool refinalize);
 
         void get_proto_model(proto_model_ref & m) const;
+
+        bool validate_model();
         
         unsigned get_num_asserted_formulas() const { return m_asserted_formulas.get_num_formulas(); }
 

src/smt/smt_context_inv.cpp

@@ -399,6 +399,45 @@ namespace smt {
 
 #endif
 
+    bool context::validate_model() {
+        if (!m_proto_model) {
+            return true;
+        }
+        ast_manager& m = m_manager;
+        literal_vector::const_iterator it  = m_assigned_literals.begin();
+        literal_vector::const_iterator end = m_assigned_literals.end();
+        for (; it != end; ++it) {
+            literal lit = *it;
+            if (!is_relevant(lit)) {
+                continue;
+            }
+            expr_ref n(m), res(m);
+            literal2expr(lit, n);
+            if (!is_ground(n)) {
+                continue;
+            }
+            switch (get_assignment(*it)) {
+            case l_undef:
+                break;
+            case l_true:
+                m_proto_model->eval(n, res, false);
+                CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
+                if (m.is_false(res)) {
+                    return false;
+                }
+                break;
+            case l_false:
+                m_proto_model->eval(n, res, false);
+                CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
+                if (m.is_true(res)) {
+                    return false;
+                }
+                break;
+            }
+        }
+        return true;
+    }
+
     /**
        \brief validate unsat core returned by 
      */

src/smt/smt_context_pp.cpp

@@ -239,6 +239,7 @@ namespace smt {
                     first = false;
                 }
                 out << "#" << n->get_id() << " -> #" << r->get_id() << "\n";
+                out << mk_pp(n, m_manager) << " -> " << mk_pp(r, m_manager) << "\n";
             }
         }
     }

src/smt/smt_model_checker.cpp

@@ -346,6 +346,10 @@ namespace smt {
         for (; it != end; ++it) {
             quantifier * q = *it;
 	    if(!m_qm->mbqi_enabled(q)) continue;
+            TRACE("model_checker", 
+                  tout << "Check: " << mk_pp(q, m_manager) << "\n";
+                  tout << m_context->get_assignment(q) << "\n";);
+
             if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
                 if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
                     verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
@@ -364,8 +368,12 @@ namespace smt {
             m_iteration_idx++;
 
         TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
-        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
+        TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);        
         m_max_cexs += m_params.m_mbqi_max_cexs;
+
+        if (num_failures == 0 && !m_context->validate_model()) {
+            num_failures = 1;
+        }
         if (num_failures == 0)
             m_curr_model->cleanup();
         if (m_params.m_mbqi_trace) {

src/smt/smt_model_finder.cpp

@@ -1418,7 +1418,7 @@ namespace smt {
 
             func_decl * get_array_func_decl(app * ground_array, auf_solver & s) {
                 expr * ground_array_interp = s.eval(ground_array, false);
-                if (ground_array_interp != 0 && s.get_model()->is_array_value(ground_array_interp))
+                if (ground_array_interp != 0 && s.get_model()->is_as_array(ground_array_interp))
                     return to_func_decl(to_app(ground_array_interp)->get_decl()->get_parameter(0).get_ast());
                 return 0;
             }

src/smt/theory_array.cpp

@@ -44,7 +44,9 @@ namespace smt {
 
     void theory_array::merge_eh(theory_var v1, theory_var v2, theory_var, theory_var) {
         // v1 is the new root
-        TRACE("array", tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1););
+        TRACE("array", 
+              tout << "merging v" << v1 << " v" << v2 << "\n"; display_var(tout, v1);
+              tout << mk_pp(get_enode(v1)->get_owner(), get_manager()) << " <- " << mk_pp(get_enode(v2)->get_owner(), get_manager()) << "\n";);
         SASSERT(v1 == find(v1));
         var_data * d1 = m_var_data[v1];
         var_data * d2 = m_var_data[v2];
@@ -70,21 +72,41 @@ namespace smt {
     }
 
     theory_var theory_array::mk_var(enode * n) {
+        ast_manager& m = get_manager();
+        context& ctx = get_context();
         theory_var r  = theory_array_base::mk_var(n);
         theory_var r2 = m_find.mk_var();
         SASSERT(r == r2);
         SASSERT(r == static_cast<int>(m_var_data.size()));
         m_var_data.push_back(alloc(var_data));
         var_data * d  = m_var_data[r];
-        TRACE("array", tout << mk_bounded_pp(n->get_owner(), get_manager()) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
+        TRACE("array", tout << mk_bounded_pp(n->get_owner(), m) << "\nis_array: " << is_array_sort(n) << ", is_select: " << is_select(n) <<
               ", is_store: " << is_store(n) << "\n";);
         d->m_is_array  = is_array_sort(n);
         if (d->m_is_array) 
-            register_sort(get_manager().get_sort(n->get_owner()));
+            register_sort(m.get_sort(n->get_owner()));
         d->m_is_select = is_select(n);
+        
+        expr* e1, *e2, *e3;
         if (is_store(n))
             d->m_stores.push_back(n);
-        get_context().attach_th_var(n, this, r);
+        else if (m.is_ite(n->get_owner(), e1, e2, e3)) {
+            ptr_vector<expr> todo;
+            todo.push_back(e2);
+            todo.push_back(e3);
+            while (!todo.empty()) {
+                e1 = todo.back();
+                todo.pop_back();
+                if (is_app(e1) && is_store(to_app(e1))) {
+                    d->m_stores.push_back(ctx.get_enode(e1));
+                }
+                else if (m.is_ite(e1, e1, e2, e3)) {
+                    todo.push_back(e2);
+                    todo.push_back(e3);
+                }
+            }
+        }
+        ctx.attach_th_var(n, this, r);
         if (m_params.m_array_laziness <= 1 && is_store(n))
             instantiate_axiom1(n);
         return r;
@@ -97,6 +119,7 @@ namespace smt {
         v                = find(v);
         var_data * d     = m_var_data[v];
         d->m_parent_selects.push_back(s);
+        TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
         ptr_vector<enode>::iterator it  = d->m_stores.begin();
         ptr_vector<enode>::iterator end = d->m_stores.end();
@@ -109,8 +132,13 @@ namespace smt {
             for (; it != end; ++it) {
                 enode * store = *it;
                 SASSERT(is_store(store));
-                if (!m_params.m_array_cg || store->is_cgr())
+                std::cout << mk_pp(store->get_owner(), get_manager()) << " " << mk_pp(s->get_owner(), get_manager()) << "\n";
+                if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
+                }
+                else {
+                    std::cout << mk_pp(store->get_owner(), get_manager()) << "\n";
+                }
             }
         }
     }
@@ -331,6 +359,9 @@ namespace smt {
     void theory_array::relevant_eh(app * n) {
         if (m_params.m_array_laziness == 0)
             return;
+        if (get_manager().is_ite(n)) {
+            TRACE("array", tout << "relevant ite " << mk_pp(n, get_manager()) << "\n";);
+        }
         if (!is_store(n) && !is_select(n))
             return;
         context & ctx    = get_context();

src/smt/theory_array_base.cpp

@@ -943,6 +943,18 @@ namespace smt {
                 result->add_entry(args.size(), args.c_ptr(), select);
             }
         }
+        TRACE("array", 
+              tout << mk_pp(n->get_root()->get_owner(), get_manager()) << "\n";
+              if (sel_set) {
+                  select_set::iterator it  = sel_set->begin();
+                  select_set::iterator end = sel_set->end();
+                  for (; it != end; ++it) {
+                      tout << "#" << (*it)->get_root()->get_owner()->get_id() << " " << mk_pp((*it)->get_owner(), get_manager()) << "\n";
+                  }
+              }
+              if (else_val_n) {
+                  tout << "else: " << mk_pp(else_val_n->get_owner(), get_manager()) << "\n";
+              });
         return result;
     }