From 357b4b20fd0ee83e38ba52328ca16b30bc2e5a0f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Nov 2017 11:17:41 -0800
Subject: [PATCH] fix #1365. Filter MBQI instantiations for as-array terms that
 lead the array theory to return unknown and therefore block further
 instantiations. as-array terms are at this point almost always created from
 internal model values so quantifier instantiations with these have little
 value, other than instantiations of other paraameters that may indepdendently
 help

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_model_checker.cpp |  5 +++--
 src/smt/smt_model_checker.h   |  2 ++
 src/smt/smt_model_finder.cpp  |  8 ++------
 src/smt/smt_quantifier.cpp    | 11 +++--------
 4 files changed, 10 insertions(+), 16 deletions(-)

diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index f72485d0e..cd59014aa 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -32,6 +32,7 @@ namespace smt {
     model_checker::model_checker(ast_manager & m, qi_params const & p, model_finder & mf):
         m(m),
         m_params(p),
+        m_autil(m),
         m_qm(0),
         m_context(0),
         m_root2value(0),
@@ -205,13 +206,13 @@ namespace smt {
     }
 
     void model_checker::operator()(expr *n) {
-        if (m.is_model_value(n)) {
+        if (m.is_model_value(n) || m_autil.is_as_array(n)) {
             throw is_model_value();
         }
     }
 
     bool model_checker::contains_model_value(expr* n) {
-        if (m.is_model_value(n)) {
+        if (m.is_model_value(n) || m_autil.is_as_array(n)) {
             return true;
         }
         if (is_app(n) && to_app(n)->get_num_args() == 0) {
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index 778f913c3..dd63940b7 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -22,6 +22,7 @@ Revision History:
 #define SMT_MODEL_CHECKER_H_
 
 #include "ast/ast.h"
+#include "ast/array_decl_plugin.h"
 #include "util/obj_hashtable.h"
 #include "smt/params/qi_params.h"
 #include "smt/params/smt_params.h"
@@ -39,6 +40,7 @@ namespace smt {
     class model_checker {
         ast_manager &                               m; // _manager;
         qi_params const &                           m_params;
+        array_util                                  m_autil;
         // copy of smt_params for auxiliary context.
         // the idea is to use a different configuration for the aux context (e.g., disable relevancy)
         scoped_ptr<smt_params>                      m_fparams;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 0536c200d..11202d58a 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -643,12 +643,8 @@ namespace smt {
                 return t_result;
             }
 
-            bool is_infinite(sort * s) const {
-                // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
-                return 
-                    !m.is_uninterp(s) &&
-                    s->is_infinite();
-            }
+            // we should not assume that uninterpreted sorts are infinite in benchmarks with quantifiers.
+            bool is_infinite(sort * s) const { return !m.is_uninterp(s) && s->is_infinite(); }
 
             /**
                \brief Return a fresh constant k that is used as a witness for elements that must be different from
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 1d58e2bb3..c6f83c611 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -127,10 +127,8 @@ namespace smt {
                         out << " #" << bindings[i]->get_owner_id();
                     }
                     out << " ;";
-                    ptr_vector<enode>::const_iterator it  = used_enodes.begin();
-                    ptr_vector<enode>::const_iterator end = used_enodes.end();
-                    for (; it != end; ++it)
-                        out << " #" << (*it)->get_owner_id();
+                    for (enode* n : used_enodes) 
+                        out << " #" << n->get_owner_id();
                     out << "\n";
                 }
                 m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
@@ -150,10 +148,7 @@ namespace smt {
 
         void init_search_eh() {
             m_num_instances = 0;
-            ptr_vector<quantifier>::iterator it2  = m_quantifiers.begin();
-            ptr_vector<quantifier>::iterator end2 = m_quantifiers.end();
-            for (; it2 != end2; ++it2) {
-                quantifier * q = *it2;
+            for (quantifier * q : m_quantifiers) {
                 get_stat(q)->reset_num_instances_curr_search();
             }
             m_qi_queue.init_search_eh();