fix #2468, adding assignment phase heuristic

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

src/ast/array_decl_plugin.h

@@ -210,6 +210,10 @@ public:
         return r;
     }
 
+    app * mk_default(expr * a) {
+        return m_manager.mk_app(m_fid, OP_ARRAY_DEFAULT, 0, nullptr, 1, &a);
+    }
+
     app * mk_const_array(sort * s, expr * v) {
         parameter param(s);
         return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v);
@@ -251,6 +255,14 @@ public:
         parameter param(f);
         return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, nullptr, nullptr);
     }
+
+    sort* get_array_range_rec(sort* s) {
+        while (is_array(s)) {
+            s = get_array_range(s);
+        }
+        return s;
+    }
+
 };
 
 

src/ast/datatype_decl_plugin.cpp

@@ -450,6 +450,19 @@ namespace datatype {
                 m_manager->raise_exception("datatype is not co-variant");
             }
 
+            array_util autil(m);
+            for (sort* s : sorts) {
+                for (constructor const* c : get_def(s)) {
+                    for (accessor const* a : *c) {
+                        if (autil.is_array(a->range())) {
+                            if (sorts.contains(get_array_range(a->range()))) {
+                                m_has_nested_arrays = true;
+                            }
+                        }                    
+                    }
+                }
+            }
+            
             u().compute_datatype_size_functions(m_def_block);
             for (symbol const& s : m_def_block) {
                 sort_ref_vector ps(m);
@@ -892,10 +905,13 @@ namespace datatype {
         for (unsigned i = 0; i < n; ++i) {
             get_subsorts(get_array_domain(s, i), subsorts);
         }
+        if (!is_datatype(get_array_range(s))) {
+            get_subsorts(get_array_range(s), subsorts);
+        }
         for (sort* r : subsorts) {
             if (mark.is_marked(r)) return false;
         }
-        return is_covariant(mark, subsorts, get_array_range(s));
+        return true;
     }
 
     def const& util::get_def(sort* s) const {
@@ -1115,6 +1131,7 @@ namespace datatype {
 
         ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
         unsigned sz = constructors.size();
+        array_util autil(m);
         TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
               tout << "forbidden: ";
               for (sort* s : forbidden_set) tout << sort_ref(s, m) << " ";
@@ -1129,7 +1146,7 @@ namespace datatype {
             TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";);
             unsigned num_args = c->get_arity();
             unsigned i = 0;
-            for (; i < num_args && !is_datatype(c->get_domain(i)); i++);
+            for (; i < num_args && !is_datatype(autil.get_array_range_rec(c->get_domain(i))); i++);
             if (i == num_args) {
                 TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";);
                 return c;
@@ -1142,7 +1159,7 @@ namespace datatype {
             unsigned num_args = c->get_arity();
             unsigned i = 0;
             for (; i < num_args; i++) {
-                sort * T_i = c->get_domain(i);
+                sort * T_i = autil.get_array_range_rec(c->get_domain(i));
                 TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";);
                 if (!is_datatype(T_i)) {
                     TRACE("util_bug", tout << sort_ref(T_i, m) << " is not a datatype\n";);

src/ast/datatype_decl_plugin.h

@@ -210,13 +210,14 @@ namespace datatype {
             unsigned                 m_id_counter;
             svector<symbol>          m_def_block;
             unsigned                 m_class_id;
+            mutable bool             m_has_nested_arrays;
 
             void inherit(decl_plugin* other_p, ast_translation& tr) override;
 
             void log_axiom_definitions(symbol const& s, sort * new_sort);
 
         public:
-            plugin(): m_id_counter(0), m_class_id(0) {}
+            plugin(): m_id_counter(0), m_class_id(0), m_has_nested_arrays(false) {}
             ~plugin() override;
 
             void finalize() override;
@@ -254,6 +255,8 @@ namespace datatype {
             unsigned get_axiom_base_id(symbol const& s) { return m_axiom_bases[s]; }
             util & u() const;
 
+            bool has_nested_arrays() const { return m_has_nested_arrays; }
+
         private:
             bool is_value_visit(expr * arg, ptr_buffer<app> & todo) const;
         
@@ -353,6 +356,7 @@ namespace datatype {
         func_decl * get_accessor_constructor(func_decl * accessor);
         func_decl * get_recognizer_constructor(func_decl * recognizer) const;
         func_decl * get_update_accessor(func_decl * update) const;
+        bool has_nested_arrays() const { return m_plugin->has_nested_arrays(); }
         family_id get_family_id() const { return m_family_id; }
         bool are_siblings(sort * s1, sort * s2);
         bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);

src/smt/params/smt_params.h

@@ -39,7 +39,8 @@ enum phase_selection {
     PS_CACHING_CONSERVATIVE,
     PS_CACHING_CONSERVATIVE2, // similar to the previous one, but alternated default config from time to time.
     PS_RANDOM,
-    PS_OCCURRENCE
+    PS_OCCURRENCE,
+    PS_THEORY
 };
 
 enum restart_strategy {

src/smt/params/smt_params_helper.pyg

@@ -10,7 +10,7 @@ def_module_params(module_name='smt',
                           ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
                           ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
                           ('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
-                          ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
+                          ('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences, 7 - theory'),
                           ('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
                           ('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold'),
                           ('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),

src/smt/smt_arith_value.cpp

@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+#include "ast/ast_pp.h"
 #include "smt/smt_arith_value.h"
 
 namespace smt {
@@ -50,6 +51,7 @@ namespace smt {
             next = next->get_next();
         }
         while (n != next);
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return found;
     }
 
@@ -69,6 +71,7 @@ namespace smt {
             next = next->get_next();
         }
         while (n != next);
+        CTRACE("arith_value", !found, tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return found;
     }
 
@@ -79,6 +82,7 @@ namespace smt {
         if (m_tha) return m_tha->get_upper(n, up, is_strict);
         if (m_thi) return m_thi->get_upper(n, up, is_strict);
         if (m_thr) return m_thr->get_upper(n, up, is_strict);
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return false;
     }
 
@@ -89,6 +93,7 @@ namespace smt {
         if (m_tha) return m_tha->get_lower(n, up, is_strict);
         if (m_thi) return m_thi->get_lower(n, up, is_strict);
         if (m_thr) return m_thr->get_lower(n, up, is_strict);
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return false;
     }
 
@@ -99,6 +104,7 @@ namespace smt {
         if (m_tha && m_tha->get_value(n, _val) && a.is_numeral(_val, val)) return true;
         if (m_thi && m_thi->get_value(n, _val) && a.is_numeral(_val, val)) return true;
         if (m_thr && m_thr->get_value(n, val)) return true;
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return false;
     }
 
@@ -115,6 +121,7 @@ namespace smt {
             next = next->get_next();
         }
         while (next != n);
+        TRACE("arith_value", tout << "value not found for " << mk_pp(e, m_ctx->get_manager()) << "\n";);
         return false;
     }
 

src/smt/smt_context.cpp

@@ -1849,6 +1849,16 @@ namespace smt {
             }
             else {
                 switch (m_fparams.m_phase_selection) {
+                case PS_THEORY: 
+                    if (d.is_theory_atom()) {
+                        theory * th = m_theories.get_plugin(d.get_theory());
+                        lbool ph = th->get_phase(var);
+                        if (ph != l_undef) {
+                            is_pos = ph == l_true;
+                            break;
+                        }
+                    }
+                    Z3_fallthrough;
                 case PS_CACHING:
                 case PS_CACHING_CONSERVATIVE:
                 case PS_CACHING_CONSERVATIVE2:

src/smt/smt_model_generator.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/array_decl_plugin.h"
 #include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
 #include "smt/proto_model/proto_model.h"
@@ -38,15 +39,15 @@ namespace smt {
     }
 
     model_generator::model_generator(ast_manager & m):
-        m_manager(m),
+        m(m),
         m_context(nullptr),
         m_fresh_idx(1),
-        m_asts(m_manager),
+        m_asts(m),
         m_model(nullptr) {
     }
 
     model_generator::~model_generator() {
-        dec_ref_collection_values(m_manager, m_hidden_ufs);
+        dec_ref_collection_values(m, m_hidden_ufs);
     }
 
     void model_generator::reset() {
@@ -60,7 +61,7 @@ namespace smt {
     void model_generator::init_model() {
         SASSERT(!m_model);
         // PARAM-TODO smt_params ---> params_ref
-        m_model = alloc(proto_model, m_manager); // , m_context->get_fparams());
+        m_model = alloc(proto_model, m); // , m_context->get_fparams());
         for (theory* th : m_context->theories()) {
             TRACE("model_generator_bug", tout << "init_model for theory: " << th->get_name() << "\n";);
             th->init_model(*this);
@@ -75,10 +76,10 @@ namespace smt {
         for (unsigned i = 0; i < sz; i++) {
             expr * p = m_context->get_b_internalized(i);
             if (is_uninterp_const(p) && m_context->is_relevant(p)) {
-                SASSERT(m_manager.is_bool(p));
+                SASSERT(m.is_bool(p));
                 func_decl * d = to_app(p)->get_decl();
                 lbool val     = m_context->get_assignment(p);
-                expr * v      = val == l_true ? m_manager.mk_true() : m_manager.mk_false();
+                expr * v      = val == l_true ? m.mk_true() : m.mk_false();
                 m_model->register_decl(d, v);
             }
         }
@@ -93,16 +94,16 @@ namespace smt {
         for (enode * r : m_context->enodes()) {
             if (r == r->get_root() && m_context->is_relevant(r)) {
                 roots.push_back(r);
-                sort * s      = m_manager.get_sort(r->get_owner());
+                sort * s      = m.get_sort(r->get_owner());
                 model_value_proc * proc = nullptr;
-                if (m_manager.is_bool(s)) {
+                if (m.is_bool(s)) {
                     CTRACE("model", m_context->get_assignment(r) == l_undef, 
-                           tout << mk_pp(r->get_owner(), m_manager) << "\n";);
+                           tout << mk_pp(r->get_owner(), m) << "\n";);
                     SASSERT(m_context->get_assignment(r) != l_undef);
                     if (m_context->get_assignment(r) == l_true)
-                        proc = alloc(expr_wrapper_proc, m_manager.mk_true());
+                        proc = alloc(expr_wrapper_proc, m.mk_true());
                     else
-                        proc = alloc(expr_wrapper_proc, m_manager.mk_false());
+                        proc = alloc(expr_wrapper_proc, m.mk_false());
                 }
                 else {
                     family_id fid = s->get_family_id();
@@ -114,7 +115,7 @@ namespace smt {
                         }
                         else {
                             TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
-                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(m_manager.get_sort(r->get_owner())));
+                            proc = alloc(fresh_value_proc, mk_extra_fresh_value(m.get_sort(r->get_owner())));
                         }
                     }
                     else {
@@ -132,11 +133,11 @@ namespace smt {
     model_value_proc* model_generator::mk_model_value(enode* r) {
         SASSERT(r == r->get_root());
         expr * n = r->get_owner();
-        if (!m_manager.is_model_value(n)) {
+        if (!m.is_model_value(n)) {
-            sort * s = m_manager.get_sort(r->get_owner());
+            sort * s = m.get_sort(r->get_owner());
             n = m_model->get_fresh_value(s);
             CTRACE("model", n == 0, 
-                   tout << mk_pp(r->get_owner(), m_manager) << "\nsort:\n" << mk_pp(s, m_manager) << "\n";
+                   tout << mk_pp(r->get_owner(), m) << "\nsort:\n" << mk_pp(s, m) << "\n";
                    tout << "is_finite: " << m_model->is_finite(s) << "\n";);
         }
         return alloc(expr_wrapper_proc, to_app(n));
@@ -180,15 +181,12 @@ namespace smt {
                 return true;
             bool visited = true;
             for (enode * r : roots) {
-                if (m_manager.get_sort(r->get_owner()) != s)
+                if (m.get_sort(r->get_owner()) != s)
                     continue;
                 SASSERT(r == r->get_root());
-                model_value_proc * proc = root2proc[r];
+                if (root2proc[r]->is_fresh()) 
-                SASSERT(proc);
-                if (proc->is_fresh())
                     continue; // r is associated with a fresh value...
-                SASSERT(r == r->get_root());
+                TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(m.get_sort(r->get_owner()), m) << "\n";);
-                TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(m_manager.get_sort(r->get_owner()), m_manager) << "\n";);
                 visit_child(source(r), colors, todo, visited);
                 TRACE("mg_top_sort", tout << "visited: " << visited << ", todo.size(): " << todo.size() << "\n";);
             }
@@ -206,8 +204,14 @@ namespace smt {
         proc->get_dependencies(dependencies);
         for (model_value_dependency const& dep : dependencies) {
             visit_child(dep, colors, todo, visited);
-            TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";);
         }
+        TRACE("mg_top_sort",
+              tout << "src: " << src << " ";
+              tout << mk_pp(n->get_owner(), m) << "\n";
+              for (model_value_dependency const& dep : dependencies) {
+                  tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";
+              }
+        );
         return visited;
     }
 
@@ -273,12 +277,10 @@ namespace smt {
 
         // traverse all enodes that are associated with fresh values...
         for (enode* r : roots) {
-            model_value_proc * proc = root2proc[r];
+            if (root2proc[r]->is_fresh()) {
-            SASSERT(proc);
-            if (!proc->is_fresh())
-                continue;
                 process_source(source(r), roots, root2proc, colors, already_traversed, todo, sorted_sources);
             }
+        }
 
         for (enode * r : roots) {
             process_source(source(r), roots, root2proc, colors, already_traversed, todo, sorted_sources);
@@ -291,29 +293,32 @@ namespace smt {
         ptr_vector<model_value_proc> procs;
         svector<source> sources;
         buffer<model_value_dependency> dependencies;
-        expr_ref_vector dependency_values(m_manager);
+        expr_ref_vector dependency_values(m);
         mk_value_procs(root2proc, roots, procs);
         top_sort_sources(roots, root2proc, sources);
         TRACE("sorted_sources",
               for (source const& curr : sources) {
                   if (curr.is_fresh_value()) {
-                      tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n";
+                      tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m) << "\n";
                   }
                   else {
                       enode * n = curr.get_enode();
                       SASSERT(n->get_root() == n);
-                      sort * s = m_manager.get_sort(n->get_owner());
+                      tout << mk_pp(n->get_owner(), m) << "\n";
-                      tout << curr << " " << mk_pp(s, m_manager);
+                      sort * s = m.get_sort(n->get_owner());
+                      tout << curr << " " << mk_pp(s, m);
                       tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
                   }
-              });
+              }
+              m_context->display(tout);
+              );
 
         scoped_reset _scoped_reset(*this, procs);
 
         for (source const& curr : sources) {
             if (curr.is_fresh_value()) {
                 sort * s = curr.get_value()->get_sort();
-                TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";);
+                TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m) << "\n";);
                 expr * val = m_model->get_fresh_value(s);
                 TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";);
                 m_asts.push_back(val);
@@ -331,13 +336,14 @@ namespace smt {
                 for (model_value_dependency const& d : dependencies) {
                     if (d.is_fresh_value()) {
                         CTRACE("mg_top_sort", !d.get_value()->get_value(), 
-                               tout << "#" << n->get_owner_id() << " -> " << d << "\n";);
+                               tout << "#" << n->get_owner_id() << " " << mk_pp(n->get_owner(), m) << " -> " << d << "\n";);
                         SASSERT(d.get_value()->get_value());
                         dependency_values.push_back(d.get_value()->get_value());
                     }
                     else {
                         enode * child = d.get_enode();
-                        TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m_manager) << "): " << mk_pp(child->get_owner(), m_manager) << " " << mk_pp(child->get_root()->get_owner(), m_manager) << "\n";);
+                        TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " (" << mk_pp(n->get_owner(), m) << "): " 
+                              << mk_pp(child->get_owner(), m) << " " << mk_pp(child->get_root()->get_owner(), m) << "\n";);
                         child = child->get_root();
                         dependency_values.push_back(m_root2value[child]);
                     }
@@ -379,7 +385,7 @@ namespace smt {
     bool model_generator::include_func_interp(func_decl * f) const {
         family_id fid = f->get_family_id();
         if (fid == null_family_id) return !m_hidden_ufs.contains(f); 
-        if (fid == m_manager.get_basic_family_id()) return false;
+        if (fid == m.get_basic_family_id()) return false;
         theory * th = m_context->get_theory(fid);
         if (!th) return true;
         return th->include_func_interp(f);
@@ -412,19 +418,19 @@ namespace smt {
                 }
                 func_interp * fi = m_model->get_func_interp(f);
                 if (fi == nullptr) {
-                    fi = alloc(func_interp, m_manager, f->get_arity());
+                    fi = alloc(func_interp, m, f->get_arity());
                     m_model->register_decl(f, fi);
                 }
                 SASSERT(m_model->has_interpretation(f));
                 SASSERT(m_model->get_func_interp(f) == fi);
                 // The entry must be new because n->get_cg() == n
                 TRACE("model", 
-                      tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m_manager) << "\nargs: ";
+                      tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m) << "\nargs: ";
                       for (unsigned i = 0; i < num_args; i++) {
                           tout << "#" << n->get_arg(i)->get_owner_id() << " ";
                       }
                       tout << "\n";
-                      tout << "value: #" << n->get_owner_id() << "\n" << mk_ismt2_pp(result, m_manager) << "\n";);
+                      tout << "value: #" << n->get_owner_id() << "\n" << mk_ismt2_pp(result, m) << "\n";);
                 if (fi->get_entry(args.c_ptr()) == nullptr)
                     fi->insert_new_entry(args.c_ptr(), result);
             }
@@ -457,7 +463,7 @@ namespace smt {
         for (enode * r : m_context->enodes()) {
             if (r == r->get_root() && m_context->is_relevant(r)) {
                 expr * n = r->get_owner();
-                if (m_manager.is_model_value(n)) {
+                if (m.is_model_value(n)) {
                     register_value(n);
                 }
             }
@@ -471,12 +477,12 @@ namespace smt {
     void model_generator::register_macros() {
         unsigned num = m_context->get_num_macros();
         TRACE("model", tout << "num. macros: " << num << "\n";);
-        expr_ref v(m_manager);
+        expr_ref v(m);
         for (unsigned i = 0; i < num; i++) {
             func_decl * f    = m_context->get_macro_interpretation(i, v);
-            func_interp * fi = alloc(func_interp, m_manager, f->get_arity());
+            func_interp * fi = alloc(func_interp, m, f->get_arity());
             fi->set_else(v);
-            TRACE("model", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";);
+            TRACE("model", tout << f->get_name() << "\n" << mk_pp(v, m) << "\n";);
             m_model->register_decl(f, fi);
         }
     }

src/smt/smt_model_generator.h

@@ -84,7 +84,7 @@ namespace smt {
         extra_fresh_value(sort * s, unsigned idx):m_sort(s), m_idx(idx), m_value(nullptr) {}
         sort * get_sort() const { return m_sort; }
         unsigned get_idx() const { return m_idx; }
-        void set_value(expr * n) { SASSERT(m_value == 0); m_value = n; }
+        void set_value(expr * n) { SASSERT(!m_value); m_value = n; }
         expr * get_value() const { return m_value; }
     };
 
@@ -178,7 +178,7 @@ namespace smt {
        \brief Auxiliary class used during model generation.
     */
     class model_generator {
-        ast_manager &                 m_manager;
+        ast_manager &                 m;
         context *                     m_context;
         ptr_vector<extra_fresh_value> m_extra_fresh_values;
         unsigned                      m_fresh_idx;
@@ -226,7 +226,7 @@ namespace smt {
         expr * get_some_value(sort * s);
         proto_model & get_model() { SASSERT(m_model); return *m_model; }
         void register_value(expr * val);
-        ast_manager & get_manager() { return m_manager; }
+        ast_manager & get_manager() { return m; }
         proto_model* mk_model();
 
         obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
@@ -235,7 +235,7 @@ namespace smt {
         void hide(func_decl * f) { 
             if (!m_hidden_ufs.contains(f)) {
                 m_hidden_ufs.insert(f);
-                m_manager.inc_ref(f); 
+                m.inc_ref(f); 
             }
         }
     };

src/smt/smt_theory.h

@@ -143,6 +143,13 @@ namespace smt {
         virtual void assign_eh(bool_var v, bool is_true) {
         }
 
+        /**
+           \brief use the theory to determine phase of the variable.
+         */
+        virtual lbool get_phase(bool_var v) {
+            return l_undef;
+        }
+
         /**
            \brief Equality propagation (v1 = v2): Core -> Theory
         */

src/smt/theory_array.cpp

@@ -95,7 +95,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";);
+        TRACE("array", tout << v << " " << 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));
         for (enode* n : d->m_stores) {
             instantiate_axiom2a(s, n);

src/smt/theory_array.h

@@ -110,6 +110,8 @@ namespace smt {
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
         void unmerge_eh(theory_var v1, theory_var v2);
+
+        ptr_vector<enode> const& parent_selects(enode* n) { return m_var_data[find(n->get_root()->get_th_var(get_id()))]->m_parent_selects; }
     };
 
 };

src/smt/theory_array_full.cpp

@@ -140,8 +140,8 @@ namespace smt {
             set_prop_upward(n->get_arg(0)->get_th_var(get_id()));
         }
         else if (is_map(n)) {
-            for (unsigned i = 0; i < n->get_num_args(); ++i) {
+            for (enode* arg : enode::args(n)) {
-                set_prop_upward(n->get_arg(i)->get_th_var(get_id()));
+                set_prop_upward(arg->get_th_var(get_id()));
             }
         }
     }
@@ -484,9 +484,9 @@ namespace smt {
         ptr_buffer<expr> args1, args2;
         vector<ptr_vector<expr> > args2l;
         args1.push_back(map);
-        for (unsigned j = 0; j < num_arrays; ++j) {
+        for (expr* ar : *map) {
             ptr_vector<expr> arg;
-            arg.push_back(map->get_arg(j));
+            arg.push_back(ar);
             args2l.push_back(arg);
         }
         for (unsigned i = 1; i < num_args; ++i) {
@@ -537,8 +537,8 @@ namespace smt {
         func_decl* f = to_func_decl(map->get_decl()->get_parameter(0).get_ast());
         SASSERT(map->get_num_args() == f->get_arity());
         ptr_buffer<expr> args2;
-        for (unsigned i = 0; i < map->get_num_args(); ++i) {
+        for (expr* arg : *map) {
-            args2.push_back(mk_default(map->get_arg(i)));
+            args2.push_back(mk_default(arg));
         }
 
         expr_ref def2(m.mk_app(f, args2.size(), args2.c_ptr()), m);

src/smt/theory_datatype.cpp

@@ -23,6 +23,7 @@ Revision History:
 #include "ast/ast_smt2_pp.h"
 #include "smt/smt_context.h"
 #include "smt/theory_datatype.h"
+#include "smt/theory_array.h"
 #include "smt/smt_model_generator.h"
 
 namespace smt {
@@ -332,6 +333,13 @@ namespace smt {
             for (unsigned i = 0; i < num_args; i++) {
                 enode * arg = e->get_arg(i);
                 sort * s    = get_manager().get_sort(arg->get_owner());
+                if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
+                    app_ref def(m_autil.mk_default(arg->get_owner()), get_manager());
+                    if (!ctx.e_internalized(def)) {
+                        ctx.internalize(def, false);
+                    }
+                    arg = ctx.get_enode(def);       
+                }
                 if (!m_util.is_datatype(s))
                     continue;
                 if (is_attached_to_var(arg))
@@ -371,15 +379,18 @@ namespace smt {
         //   (assert (> (len a) 1)
         //   
         // If the theory variable is not created for 'a', then a wrong model will be generated.
-        TRACE("datatype", tout << "apply_sort_cnstr: #" << n->get_owner_id() << "\n";);
+        TRACE("datatype", tout << "apply_sort_cnstr: #" << n->get_owner_id() << " " << mk_pp(n->get_owner(), get_manager()) << "\n";);
         TRACE("datatype_bug", 
               tout << "apply_sort_cnstr:\n" << mk_pp(n->get_owner(), get_manager()) << " ";
               tout << m_util.is_datatype(s) << " ";
               if (m_util.is_datatype(s)) tout << "is-infinite: " << s->is_infinite() << " "; 
               if (m_util.is_datatype(s)) tout << "attached: " << is_attached_to_var(n) << " ";
-                  tout << "\n";
+              tout << "\n";);
-                  );
+
-        if ((get_context().has_quantifiers() || (m_util.is_datatype(s) && !s->is_infinite())) && !is_attached_to_var(n)) {
+        if (!is_attached_to_var(n) &&
+            (get_context().has_quantifiers() || 
+             (m_util.is_datatype(s) && m_util.has_nested_arrays()) || 
+             (m_util.is_datatype(s) && !s->is_infinite()))) {
             mk_var(n);
         }
     }
@@ -500,6 +511,7 @@ namespace smt {
 
         // collect equalities on all children that may have been used.
         bool found = false;
+        ast_manager& m = get_manager();
         for (enode * arg : enode::args(parentc)) {
             // found an argument which is equal to root
             if (arg->get_root() == child->get_root()) {
@@ -508,6 +520,17 @@ namespace smt {
                 }
                 found = true;
             }
+            sort * s = m.get_sort(arg->get_owner());
+            if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
+                for (enode* aarg : get_array_args(arg)) {
+                    if (aarg->get_root() == child->get_root()) {
+                        if (aarg != child) {
+                            m_used_eqs.push_back(enode_pair(aarg, child));
+                        }
+                        found = true;
+                    }
+                }
+            }
         }
         VERIFY(found);
     }
@@ -542,6 +565,7 @@ namespace smt {
 
     // start exploring subgraph below `app`
     bool theory_datatype::occurs_check_enter(enode * app) {
+        context& ctx = get_context();
         app = app->get_root();
         theory_var v = app->get_th_var(get_id());
         if (v == null_theory_var) {
@@ -563,15 +587,44 @@ namespace smt {
                 occurs_check_explain(parent, arg);
                 return true;
             }
-            // explore `arg` (with paren)
+            // explore `arg` (with parent)
-            if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
+            expr* earg = arg->get_owner();
+            sort* s = get_manager().get_sort(earg);
+            if (m_util.is_datatype(s)) {
                 m_parent.insert(arg->get_root(), parent);
                 oc_push_stack(arg);
             }
+            else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
+                for (enode* aarg : get_array_args(arg)) {
+                    if (oc_cycle_free(aarg)) {
+                        continue;
+                    }
+                    if (oc_on_stack(aarg)) {
+                        occurs_check_explain(parent, aarg);
+                        return true;
+                    }
+                    if (m_util.is_datatype(get_manager().get_sort(aarg->get_owner()))) {
+                        m_parent.insert(aarg->get_root(), parent);
+                        oc_push_stack(aarg);
+                    }
+                }
+            }            
         }
         return false;
     }
 
+    ptr_vector<enode> const& theory_datatype::get_array_args(enode* n) {
+        m_array_args.reset();
+        context& ctx = get_context();
+        theory_array* th = dynamic_cast<theory_array*>(ctx.get_theory(m_autil.get_family_id()));
+        for (enode* p : th->parent_selects(n)) {
+            m_array_args.push_back(p);            
+        }
+        app_ref def(m_autil.mk_default(n->get_owner()), get_manager());
+        m_array_args.push_back(ctx.get_enode(def));
+        return m_array_args;
+    }
+
     /**
        \brief Check if n can be reached starting from n and following equalities and constructors.
        For example, occur_check(a1) returns true in the following set of equalities:
@@ -637,6 +690,7 @@ namespace smt {
         theory(m.mk_family_id("datatype")),
         m_params(p),
         m_util(m),
+        m_autil(m),
         m_find(*this),
         m_trail_stack(*this) {
     }
@@ -673,7 +727,7 @@ namespace smt {
     }
 
     bool theory_datatype::include_func_interp(func_decl* f) {
-        return false; // return m_util.is_accessor(f);
+        return false; 
     }
 
     void theory_datatype::init_model(model_generator & m) {
@@ -706,8 +760,15 @@ namespace smt {
         func_decl * c_decl = d->m_constructor->get_decl();
         datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
         unsigned num = d->m_constructor->get_num_args();
-        for (unsigned i = 0; i < num; i++) 
+        for (enode* arg : enode::args(d->m_constructor)) {
-            result->add_dependency(d->m_constructor->get_arg(i));
+            result->add_dependency(arg);
+        }
+        TRACE("datatype", 
+              tout << mk_pp(n->get_owner(), get_manager()) << "\n";
+              tout << "depends on\n";
+              for (enode* arg : enode::args(d->m_constructor)) {
+                  tout << " " << mk_pp(arg->get_owner(), get_manager()) << "\n";
+              });
         return result;
     }
 
@@ -882,7 +943,7 @@ namespace smt {
         TRACE("datatype_bug", tout << "non_rec_c: " << non_rec_c->get_name() << "\n";);
         unsigned non_rec_idx  = m_util.get_constructor_idx(non_rec_c);
         var_data * d          = m_var_data[v];
-        SASSERT(d->m_constructor == 0);
+        SASSERT(d->m_constructor == nullptr);
         func_decl * r         = nullptr;
         m_stats.m_splits++;
 

src/smt/theory_datatype.h

@@ -19,10 +19,11 @@ Revision History:
 #ifndef THEORY_DATATYPE_H_
 #define THEORY_DATATYPE_H_
 
-#include "smt/smt_theory.h"
 #include "util/union_find.h"
-#include "smt/params/theory_datatype_params.h"
+#include "ast/array_decl_plugin.h"
 #include "ast/datatype_decl_plugin.h"
+#include "smt/smt_theory.h"
+#include "smt/params/theory_datatype_params.h"
 #include "smt/proto_model/datatype_factory.h"
 
 namespace smt {
@@ -48,6 +49,7 @@ namespace smt {
         
         theory_datatype_params &  m_params;
         datatype_util             m_util;
+        array_util                m_autil;
         ptr_vector<var_data>      m_var_data;
         th_union_find             m_find;
         th_trail_stack            m_trail_stack;
@@ -89,6 +91,8 @@ namespace smt {
         bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); }
 
         void oc_push_stack(enode * n);
+        ptr_vector<enode> m_array_args;
+        ptr_vector<enode> const& get_array_args(enode* n);
 
         // class for managing state of final_check
         class final_check_st {

src/smt/theory_lra.cpp

@@ -939,6 +939,29 @@ public:
         m_asserted_atoms.push_back(delayed_atom(v, is_true));
     }
 
+    lbool get_phase(bool_var v) {
+        lp_api::bound* b;
+        if (!m_bool_var2bound.find(v, b)) {
+            return l_undef;
+        }
+        scoped_internalize_state st(*this);
+        st.vars().push_back(b->get_var());
+        st.coeffs().push_back(rational::one());
+        init_left_side(st);
+        lp::lconstraint_kind k = lp::EQ;
+        switch (b->get_bound_kind()) {
+        case lp_api::lower_t:
+            k = lp::GE;
+            break;
+        case lp_api::upper_t:
+            k = lp::LE;
+            break;
+        }         
+        auto vi = get_var_index(b->get_var());
+        rational bound = b->get_value();
+        return m_solver->compare_values(vi, k, bound) ? l_true : l_false;
+    }
+
     void new_eq_eh(theory_var v1, theory_var v2) {
         // or internalize_eq(v1, v2);
         m_arith_eq_adapter.new_eq_eh(v1, v2);            
@@ -3565,6 +3588,9 @@ void theory_lra::internalize_eq_eh(app * atom, bool_var v) {
 void theory_lra::assign_eh(bool_var v, bool is_true) {
     m_imp->assign_eh(v, is_true);
 }
+lbool theory_lra::get_phase(bool_var v) {
+    return m_imp->get_phase(v);
+}
 void theory_lra::new_eq_eh(theory_var v1, theory_var v2) {
     m_imp->new_eq_eh(v1, v2);
 }

src/smt/theory_lra.h

@@ -43,6 +43,8 @@ namespace smt {
 
         void assign_eh(bool_var v, bool is_true) override;
 
+        lbool get_phase(bool_var v) override;
+
         void new_eq_eh(theory_var v1, theory_var v2) override;
 
         bool use_diseqs() const override;

src/util/lp/lar_solver.cpp

@@ -1777,6 +1777,32 @@ constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, c
     return ci;
 }
 
+bool lar_solver::compare_values(var_index j, lconstraint_kind k, const mpq & rhs) {
+    if (is_term(j)) { // j is a term
+        impq lhs = 0;
+        for (auto const& cv : get_term(j)) {
+            lhs += cv.coeff() * get_column_value(cv.var());
+        }
+        return compare_values(lhs, k, rhs);
+    }
+    else {
+        return compare_values(get_column_value(j), k, rhs);
+    }
+}
+
+bool lar_solver::compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs) {
+    switch (k) {
+    case LT: return lhs < rhs;
+    case LE: return lhs <= rhs;
+    case GT: return lhs > rhs;
+    case GE: return lhs >= rhs;
+    case EQ: return lhs == rhs;
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
 void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) {
     switch (m_mpq_lar_core_solver.m_column_types[j]) {
     case column_type::free_column:

src/util/lp/lar_solver.h

@@ -178,6 +178,10 @@ public:
 
     constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ;
 
+    bool compare_values(var_index j, lconstraint_kind kind, const mpq & right_side);
+
+    bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs);
+
     void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index);
 
     void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);