From 185f125f7a3d356192df272bfb2339ad36d3cdf9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2013 17:48:43 -0700
Subject: [PATCH] Fix problem reported at
 http://stackoverflow.com/questions/17215640/getting-concrete-values-from-a-model-containing-array-ext

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/smt/smt_model_finder.cpp | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index f3d0ca3bb..c4a48d9f8 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -94,7 +94,7 @@ namespace smt {
             }
 
             obj_map<expr, unsigned> const & get_elems() const { return m_elems; }
-            
+
             void insert(expr * n, unsigned generation) {
                 if (m_elems.contains(n))
                     return;
@@ -102,6 +102,14 @@ namespace smt {
                 m_elems.insert(n, generation);
                 SASSERT(!m_manager.is_model_value(n));
             }
+
+            void remove(expr * n) {
+                // We can only remove n if it is in m_elems, AND m_inv was not initialized yet.
+                SASSERT(m_elems.contains(n));
+                SASSERT(m_inv.empty());
+                m_elems.erase(n);
+                m_manager.dec_ref(n);
+            }
             
             void display(std::ostream & out) const {
                 obj_map<expr, unsigned>::iterator it  = m_elems.begin();
@@ -525,6 +533,30 @@ namespace smt {
                 }
             }
 
+            // For each instantiation_set, reemove entries that do not evaluate to values.
+            void cleanup_instantiation_sets() {
+                ptr_vector<expr> to_delete;
+                ptr_vector<node>::const_iterator it  = m_nodes.begin();
+                ptr_vector<node>::const_iterator end = m_nodes.end();
+                for (; it != end; ++it) {
+                    node * curr = *it;
+                    if (curr->is_root()) {
+                        instantiation_set * s = curr->get_instantiation_set();
+                        to_delete.reset();
+                        obj_map<expr, unsigned> const & elems = s->get_elems();
+                        for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
+                            expr * n     = it->m_key;
+                            expr * n_val = eval(n, true);
+                            if (!m_manager.is_value(n_val))
+                                to_delete.push_back(n);
+                        }
+                        for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
+                            s->remove(*it);
+                        }
+                    }
+                }
+            }
+
             void display_nodes(std::ostream & out) const {
                 display_key2node(out, m_uvars);
                 display_A_f_is(out);                
@@ -545,6 +577,7 @@ namespace smt {
                     r = 0;
                 else
                     r = tmp;
+                TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
                 m_eval_cache.insert(n, r);
                 m_eval_cache_range.push_back(r);
                 return r;
@@ -1047,6 +1080,7 @@ namespace smt {
 
         public:
             void fix_model(expr_ref_vector & new_constraints) {
+                cleanup_instantiation_sets();
                 m_new_constraints = &new_constraints;
                 func_decl_set partial_funcs;
                 collect_partial_funcs(partial_funcs);