return unknown if m_array_weak was used and result is satisfiable

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

src/ast/rewriter/seq_rewriter.cpp

@@ -954,6 +954,16 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
         return BR_FAILED;
     }
     unsigned len = r.get_unsigned();
+    expr* a2 = nullptr, *i2 = nullptr;
+    if (m_util.str.is_at(a, a2, i2)) {
+        if (len > 0) {
+            result = m_util.str.mk_empty(m().get_sort(a));
+        }
+        else {
+            result = a2;
+        }
+        return BR_DONE;            
+    }
 
     expr_ref_vector as(m());
     m_util.str.get_concat_units(a, as);

src/smt/theory_array.cpp

@@ -100,10 +100,14 @@ namespace smt {
         for (enode* n : d->m_stores) {
             instantiate_axiom2a(s, n);
         }
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
+        if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             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);
                 }
             }
@@ -118,10 +122,17 @@ namespace smt {
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
-        if (!m_params.m_array_weak && !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 (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);
+                }
+            }
+        }
     }
 
     bool theory_array::instantiate_axiom2b_for(theory_var v) {
@@ -138,15 +149,17 @@ namespace smt {
        \brief Mark v for upward propagation. That is, enables the propagation of select(v, i) to store(v,j,k).
     */
     void theory_array::set_prop_upward(theory_var v) {
-        if (m_params.m_array_weak)
-            return;
         v = find(v);
         var_data * d = m_var_data[v];
         if (!d->m_prop_upward) {
             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_delay_exp_axiom)
+            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) 
                 set_prop_upward(n);

src/smt/theory_array_base.h

@@ -32,6 +32,8 @@ namespace smt {
         bool m_found_unsupported_op;
 
         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()); }
 
         bool is_store(app const* n) const { return n->is_app_of(get_id(), OP_STORE); }
         bool is_map(app const* n) const { return n->is_app_of(get_id(), OP_ARRAY_MAP); }

src/smt/theory_array_full.cpp

@@ -87,9 +87,13 @@ namespace smt {
         var_data_full * d_full     = m_var_data_full[v];
         d_full->m_parent_maps.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
+        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);
                 }                
             }
@@ -100,14 +104,16 @@ namespace smt {
     // set set_prop_upward on root and recursively on children if necessary.
     // 
     void theory_array_full::set_prop_upward(theory_var v) {
-        if (m_params.m_array_weak)
-            return;
         v = find(v);
         var_data * d = m_var_data[v];
         if (!d->m_prop_upward) {
             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);
@@ -355,8 +361,13 @@ namespace smt {
             instantiate_default_store_axiom(store);
         }        
 
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
-            instantiate_parent_stores_default(v);
+        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);
+            }
         }
     }
 
@@ -376,10 +387,14 @@ namespace smt {
             SASSERT(is_map(map));
             instantiate_select_map_axiom(s, map);
         }
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
+        if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
             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);
                 }
             }
@@ -748,8 +763,11 @@ namespace smt {
                 var_data * d = m_var_data[v];
                 if (d->m_prop_upward && instantiate_axiom_map_for(v))
                     r = FC_CONTINUE;
-                if (d->m_prop_upward && !m_params.m_array_weak) {
-                    if (instantiate_parent_stores_default(v))
+                if (d->m_prop_upward) {
+                    if (m_params.m_array_weak) {
+                        found_unsupported_op(v);
+                    }
+                    else if (instantiate_parent_stores_default(v))
                         r = FC_CONTINUE;
                 }
             }

src/smt/theory_seq.cpp

@@ -5208,7 +5208,7 @@ void theory_seq::add_nth_axiom(expr* e) {
         expr_ref zero(m_autil.mk_int(0), m);
         literal i_ge_0 = mk_simplified_literal(m_autil.mk_ge(i, zero));
         literal i_ge_len_s = mk_simplified_literal(m_autil.mk_ge(mk_sub(i, mk_len(s)), zero));
-        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));
+        add_axiom(~i_ge_0, i_ge_len_s, mk_eq(m_util.str.mk_unit(e), m_util.str.mk_at(s, i), false));        
     }
 }
 

src/util/params.cpp

@@ -324,8 +324,8 @@ class params {
         };
     };
     typedef std::pair<symbol, value> entry;
-    svector<entry> m_entries;
-    std::atomic<unsigned>       m_ref_count;
+    svector<entry>        m_entries;
+    std::atomic<unsigned> m_ref_count;
     void del_value(entry & e);
     void del_values();