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

@@ -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) {

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;

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.
-                // 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(); }
-                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

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();
+                    for (enode* n : used_enodes) 
-                    ptr_vector<enode>::const_iterator end = used_enodes.end();
+                        out << " #" << n->get_owner_id();
-                    for (; it != end; ++it)
-                        out << " #" << (*it)->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();
+            for (quantifier * q : m_quantifiers) {
-            ptr_vector<quantifier>::iterator end2 = m_quantifiers.end();
-            for (; it2 != end2; ++it2) {
-                quantifier * q = *it2;
                 get_stat(q)->reset_num_instances_curr_search();
             }
             m_qi_queue.init_search_eh();