change handling of weak array mode. Insert weak delay variables into a queue that gets consumed by the next propagation when the array_weak parameter is changed #2686

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

src/smt/theory_array.cpp

@@ -104,10 +104,6 @@ namespace smt {
             for (enode* store : d->m_parent_stores) {
                 SASSERT(is_store(store));
                 if (!m_params.m_array_cg || store->is_cgr()) {
-                    if (m_params.m_array_weak) {
-                        found_unsupported_op(store->get_owner());
-                        break;
-                    }
                     instantiate_axiom2b(s, store);
                 }
             }
@@ -125,10 +121,6 @@ namespace smt {
         if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) {
             for (enode* n : d->m_parent_selects) {
                 if (!m_params.m_array_cg || n->is_cgr()) {
-                    if (m_params.m_array_weak) {
-                        found_unsupported_op(s);
-                        break;
-                    }
                     instantiate_axiom2b(n, s);
                 }
             }
@@ -152,13 +144,13 @@ namespace smt {
         v = find(v);
         var_data * d = m_var_data[v];
         if (!d->m_prop_upward) {
+            if (m_params.m_array_weak) {
+                add_weak_var(v);
+                return;
+            }
             TRACE("array", tout << "#" << v << "\n";);
             m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
             d->m_prop_upward = true;
-            if (m_params.m_array_weak) {
-                found_unsupported_op(v);
-                return;
-            }
             if (!m_params.m_array_delay_exp_axiom) 
                 instantiate_axiom2b_for(v);
             for (enode * n : d->m_stores) 
@@ -401,7 +393,8 @@ namespace smt {
                     r = assert_delayed_axioms();
             }
         }
-        if (r == FC_DONE && m_found_unsupported_op && !get_context().get_fparams().m_array_fake_support) 
+        bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
+        if (r == FC_DONE && should_giveup && !get_context().get_fparams().m_array_fake_support) 
             r = FC_GIVEUP;
         CTRACE("array", r != FC_DONE || m_found_unsupported_op, tout << r << "\n";);
         return r;

src/smt/theory_array.h

@@ -69,7 +69,7 @@ namespace smt {
         void reset_eh() override;
         void init_search_eh() override { m_final_check_idx = 0; }
 
-        virtual void set_prop_upward(theory_var v);
+        void set_prop_upward(theory_var v) override;
         virtual void set_prop_upward(enode* n);
         virtual void set_prop_upward(theory_var v, var_data* d);
 

src/smt/theory_array_base.cpp

@@ -28,10 +28,16 @@ namespace smt {
 
     theory_array_base::theory_array_base(ast_manager & m):
         theory(m.mk_family_id("array")),
-        m_found_unsupported_op(false)
+        m_found_unsupported_op(false),
+        m_array_weak_head(0)
     {
     }
 
+    void theory_array_base::add_weak_var(theory_var v) {
+        get_context().push_trail(push_back_vector<context, svector<theory_var>>(m_array_weak_trail));
+        m_array_weak_trail.push_back(v);
+    }
+
     void theory_array_base::found_unsupported_op(expr * n) {
         if (!get_context().get_fparams().m_array_fake_support && !m_found_unsupported_op) {
             TRACE("array", tout << mk_ll_pp(n, get_manager()) << "\n";);            
@@ -404,7 +410,12 @@ namespace smt {
     }
 
     bool theory_array_base::can_propagate() {
-        return !m_axiom1_todo.empty() || !m_axiom2_todo.empty() || !m_extensionality_todo.empty() || !m_congruent_todo.empty();
+        return 
+            !m_axiom1_todo.empty() || 
+            !m_axiom2_todo.empty() || 
+            !m_extensionality_todo.empty() || 
+            !m_congruent_todo.empty() ||
+            (!get_context().get_fparams().m_array_weak && has_propagate_up_trail());
     }
 
     void theory_array_base::propagate() {
@@ -421,6 +432,12 @@ namespace smt {
                 assert_congruent_core(m_congruent_todo[i].first, m_congruent_todo[i].second);
             m_extensionality_todo.reset();
             m_congruent_todo.reset();
+            if (!get_context().get_fparams().m_array_weak && has_propagate_up_trail()) {
+                get_context().push_trail(value_trail<context, unsigned>(m_array_weak_head));
+                for (; m_array_weak_head < m_array_weak_trail.size(); ++m_array_weak_head) {
+                    set_prop_upward(m_array_weak_trail[m_array_weak_head]);
+                }                
+            }
         }
     }
 

src/smt/theory_array_base.h

@@ -30,7 +30,11 @@ namespace smt {
         friend class theory_array_bapa;
     protected:
         bool m_found_unsupported_op;
-
+        unsigned m_array_weak_head;
+        svector<theory_var> m_array_weak_trail;
+        bool has_propagate_up_trail() const { return m_array_weak_head < m_array_weak_trail.size(); }
+        void add_weak_var(theory_var v);
+        virtual void set_prop_upward(theory_var v) {}
         void found_unsupported_op(expr * n);
         void found_unsupported_op(enode* n) { found_unsupported_op(n->get_owner()); }
         void found_unsupported_op(theory_var v) { found_unsupported_op(get_enode(v)->get_owner()); }

src/smt/theory_array_full.cpp

@@ -91,10 +91,6 @@ namespace smt {
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             for (enode * n : d->m_parent_selects) {
                 if (!m_params.m_array_cg || n->is_cgr()) {
-                    if (m_params.m_array_weak) {
-                        found_unsupported_op(s);
-                        break;
-                    }
                     instantiate_select_map_axiom(n, s);
                 }                
             }
@@ -108,13 +104,13 @@ namespace smt {
         v = find(v);
         var_data * d = m_var_data[v];
         if (!d->m_prop_upward) {
+            if (m_params.m_array_weak) {
+                add_weak_var(v);
+                return;
+            }
             m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
             d->m_prop_upward = true;
             TRACE("array", tout << "#" << v << "\n";);
-            if (m_params.m_array_weak) {
-                found_unsupported_op(v);
-                return;
-            }
             if (!m_params.m_array_delay_exp_axiom) {
                 instantiate_axiom2b_for(v);
                 instantiate_axiom_map_for(v);
@@ -364,14 +360,9 @@ namespace smt {
         }        
 
         if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
-            if (m_params.m_array_weak) {
-                found_unsupported_op(v);
-            }
-            else {
             instantiate_parent_stores_default(v);            
         }
     }
-    }
 
     void theory_array_full::add_parent_select(theory_var v, enode * s) {
         TRACE("array", 
@@ -393,10 +384,6 @@ namespace smt {
             for (enode * map : d_full->m_parent_maps) {
                 SASSERT(is_map(map));
                 if (!m_params.m_array_cg || map->is_cgr()) {
-                    if (m_params.m_array_weak) {
-                        found_unsupported_op(s);
-                        break;
-                    }
                     instantiate_select_map_axiom(s, map);
                 }
             }
@@ -757,10 +744,7 @@ namespace smt {
                 if (d->m_prop_upward && instantiate_axiom_map_for(v))
                     r = FC_CONTINUE;
                 if (d->m_prop_upward) {
-                    if (m_params.m_array_weak) {
+                    if (instantiate_parent_stores_default(v))
-                        found_unsupported_op(v);
-                    }
-                    else if (instantiate_parent_stores_default(v))
                         r = FC_CONTINUE;
                 }
             }
@@ -775,8 +759,8 @@ namespace smt {
         if (r == FC_DONE && m_bapa) {
             r = m_bapa->final_check();
         }
-
+        bool should_giveup = m_found_unsupported_op || has_propagate_up_trail();
-        if (r == FC_DONE && m_found_unsupported_op)
+        if (r == FC_DONE && should_giveup)
             r = FC_GIVEUP;
         return r;
     }