taking a look at mbp_qel for arrays

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/ast/array_decl_plugin.h

@@ -33,6 +33,18 @@ inline sort* get_array_domain(sort const * s, unsigned idx) {
     return to_sort(s->get_parameter(idx).get_ast());
 }
 
+inline expr_container array_select_indices(app* e) {
+    return expr_container(e->get_args() + 1, e->get_args() + e->get_num_args());
+}
+
+inline expr_container array_store_indices(app* e) {
+    return expr_container(e->get_args() + 1, e->get_args() + e->get_num_args() - 1);
+}
+
+inline expr* array_store_elem(app* e) {
+    return e->get_arg(e->get_num_args() - 1);
+}
+
 enum array_sort_kind {
     ARRAY_SORT,
     _SET_SORT

src/ast/ast.h

@@ -690,8 +690,21 @@ class expr : public ast {
 
     sort* get_sort() const;
 
-    unsigned get_small_id() const { return get_id(); }
-    
+    unsigned get_small_id() const { return get_id(); }    
+};
+
+class expr_container {
+    expr* const* m_pos;
+    expr* const* m_end;
+public:
+    expr_container(expr* const* pos, expr* const* end) :m_pos(pos), m_end(end) {}
+    expr_container& operator++() { ++m_pos; return *this; }
+    expr_container operator++(int) { expr_container tmp = *this; ++(*this); return tmp; }
+    bool operator==(expr_container const& it) const { return m_pos == it.m_pos; }
+    bool operator!=(expr_container const& it) const { return m_pos != it.m_pos; }
+    expr* operator*() const { return *m_pos; }
+    expr* const* begin() const { return m_pos; }
+    expr* const* end() const { return m_end; }
 };
 
 // -----------------------------------

src/qe/mbp/mbp_qel.cpp

@@ -126,6 +126,9 @@ class mbp_qel::impl {
         init(vars, fml, mdl);
         // Apply MBP rules till saturation
 
+        TRACE("mbp_tg",
+            tout << "mbp tg " << m_tg.get_lits() << "\nand vars " << vars << "\n";);
+
         // First, apply rules without splitting on model
         saturate(vars);
 
@@ -135,18 +138,15 @@ class mbp_qel::impl {
         saturate(vars);
 
         TRACE("mbp_tg",
-              tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars;);
+              tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars << "\n";);
         TRACE("mbp_tg_verbose", obj_hashtable<app> vars_tmp;
               collect_uninterp_consts(mk_and(m_tg.get_lits()), vars_tmp);
-              for (auto a
-                   : vars_tmp) tout
-              << mk_pp(a->get_decl(), m) << "\n";
-              for (auto b
-                   : m_tg.get_lits()) tout
-              << expr_ref(b, m) << "\n";
-              for (auto a
-                   : vars) tout
-              << expr_ref(a, m) << " ";);
+              for (auto a : vars_tmp) 
+                  tout << mk_pp(a->get_decl(), m) << "\n";
+              for (auto b : m_tg.get_lits()) 
+                  tout << expr_ref(b, m) << "\n";
+              for (auto a : vars) tout << expr_ref(a, m) << " ";
+              tout << "\n");
 
         // 1. Apply qe_lite to remove all c-ground variables
         // 2. Collect all core variables in the output (variables used as array
@@ -171,11 +171,10 @@ class mbp_qel::impl {
         };
         expr_sparse_mark red_vars;
         for (auto v : vars)
-            if (is_red(v)) red_vars.mark(v);
+            if (is_red(v)) 
+                red_vars.mark(v);
         CTRACE("mbp_tg", !core_vars.empty(), tout << "vars not redundant ";
-               for (auto v
-                    : core_vars) tout
-               << " " << app_ref(v, m);
+               for (auto v : core_vars) tout << " " << app_ref(v, m);
                tout << "\n";);
 
         std::function<bool(expr *)> non_core = [&](expr *e) {

src/qe/mbp/mbp_qel_util.cpp

@@ -80,23 +80,25 @@ struct proc {
     obj_hashtable<app> &m_vars;
     array_util m_array_util;
     datatype_util m_dt_util;
+    bool is_accessor(expr* e) const {
+        return is_app(e) && m_dt_util.is_accessor(to_app(e)->get_decl());
+    }
     proc(obj_hashtable<app> &vars, ast_manager &man)
         : m(man), m_vars(vars), m_array_util(m), m_dt_util(m) {}
     void operator()(expr *n) const {}
     void operator()(app *n) {
         if (m_array_util.is_select(n)) {
-            expr *idx = n->get_arg(1);
-            if (is_app(idx) && m_dt_util.is_accessor(to_app(idx)->get_decl()))
-                return;
-            collect_uninterp_consts(idx, m_vars);
-        } else if (m_array_util.is_store(n)) {
-            expr *idx = n->get_arg(1), *elem = n->get_arg(2);
-            if (!(is_app(idx) &&
-                  m_dt_util.is_accessor(to_app(idx)->get_decl())))
-                collect_uninterp_consts(idx, m_vars);
-            if (!(is_app(elem) &&
-                  m_dt_util.is_accessor(to_app(elem)->get_decl())))
+            for (expr* arg : array_select_indices(n)) 
+                if (!is_accessor(arg))
+                    collect_uninterp_consts(arg, m_vars);            
+        } 
+        else if (m_array_util.is_store(n)) {
+            expr* elem = array_store_elem(n);
+            if (!is_accessor(elem))
                 collect_uninterp_consts(elem, m_vars);
+            for (expr* idx : array_store_indices(n)) 
+                if (!is_accessor(idx))
+                    collect_uninterp_consts(idx, m_vars);            
         }
     }
 };