fix const-char test

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

src/ast/rewriter/seq_rewriter.cpp

@@ -307,6 +307,9 @@ eautomaton* re2automaton::re2aut(expr* e) {
     else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
         return m_sa->mk_product(*a, *b);
     }
+    else {
+        TRACE("seq", tout << "not handled " << mk_pp(e, m) << "\n";);
+    }
     
     return nullptr;
 }
@@ -1234,6 +1237,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     scoped_ptr<eautomaton> aut;
     expr_ref_vector seq(m());
     if (!(aut = m_re2aut(b))) {
+        TRACE("seq", tout << "not translated to automaton " << mk_pp(b, m()) << "\n";);
         return BR_FAILED;
     }
 
@@ -1250,6 +1254,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
     }
 
     if (!is_sequence(a, seq)) {
+        TRACE("seq", tout << "not a sequence " << mk_pp(a, m()) << "\n";);
         return BR_FAILED;
     } 
         
@@ -1301,17 +1306,16 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         }
     }
     u_map<expr*> const& frontier = maps[select_map];
-    u_map<expr*>::iterator it = frontier.begin(), end = frontier.end();
     expr_ref_vector ors(m());
-    for (; it != end; ++it) {
+    for (auto const& kv : frontier) {
         unsigned_vector states;
         bool has_final = false;
-        aut->get_epsilon_closure(it->m_key, states);
+        aut->get_epsilon_closure(kv.m_key, states);
         for (unsigned i = 0; i < states.size() && !has_final; ++i) {
             has_final = aut->is_final_state(states[i]);
         }
         if (has_final) {
-            ors.push_back(it->m_value);
+            ors.push_back(kv.m_value);
         }
     }
     result = mk_or(ors);

src/ast/seq_decl_plugin.cpp

@@ -972,7 +972,7 @@ bool seq_util::is_const_char(expr* e, unsigned& c) const {
     bv_util bv(m);
     rational r;    
     unsigned sz;
-    return bv.is_numeral(e, r, sz) && r.is_unsigned(), c = r.get_unsigned(), true;
+    return bv.is_numeral(e, r, sz) && sz == 8 && r.is_unsigned() && (c = r.get_unsigned(), true);
 }
 
 app* seq_util::mk_char(unsigned ch) const {

src/smt/theory_seq.cpp

@@ -3737,6 +3737,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
     st.update("seq extensionality", m_stats.m_extensionality);
     st.update("seq fixed length", m_stats.m_fixed_length);
     st.update("seq int.to.str", m_stats.m_int_string);
+    st.update("seq automata", m_stats.m_propagate_automata);
 }
 
 void theory_seq::init_search_eh() {
@@ -5476,6 +5477,7 @@ void theory_seq::propagate_step(literal lit, expr* step) {
    acc(s, idx, re, i) -> idx < max_unfolding
  */
 void theory_seq::propagate_accept(literal lit, expr* acc) {
+    ++m_stats.m_propagate_automata;
     expr *e = nullptr, *idx = nullptr, *re = nullptr;
     unsigned src = 0;
     context& ctx = get_context();

src/smt/theory_str.cpp

@@ -7219,20 +7219,18 @@ namespace smt {
     expr_ref theory_str::aut_path_rewrite_constraint(expr * cond, expr * ch_var) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
-        bv_util bvu(m);
 
         expr_ref retval(m);
-
-        rational char_val;
-        unsigned int bv_width;
+        
+        unsigned char_val = 0;
 
         expr * lhs;
         expr * rhs;
 
-        if (bvu.is_numeral(cond, char_val, bv_width)) {
-            SASSERT(char_val.is_nonneg() && char_val.get_unsigned() < 256);
+        if (u.is_const_char(cond, char_val)) {
+            SASSERT(char_val < 256);
             TRACE("str", tout << "rewrite character constant " << char_val << std::endl;);
-            zstring str_const(char_val.get_unsigned());
+            zstring str_const(char_val);
             retval = u.str.mk_string(str_const);
             return retval;
         } else if (is_var(cond)) {
@@ -7377,23 +7375,20 @@ namespace smt {
                     } else if (mv.t()->is_range()) {
                         expr_ref range_lo(mv.t()->get_lo(), m);
                         expr_ref range_hi(mv.t()->get_hi(), m);
-                        bv_util bvu(m);
 
-                        rational lo_val, hi_val;
-                        unsigned int bv_width;
+                        unsigned lo_val, hi_val;
 
-                        if (bvu.is_numeral(range_lo, lo_val, bv_width) && bvu.is_numeral(range_hi, hi_val, bv_width)) {
+                        if (u.is_const_char(range_lo, lo_val) && u.is_const_char(range_hi, hi_val)) {
                             TRACE("str", tout << "make range predicate from " << lo_val << " to " << hi_val << std::endl;);
                             expr_ref cond_rhs(m);
 
                             if (hi_val < lo_val) {
-                                rational tmp = lo_val;
-                                lo_val = hi_val;
-                                hi_val = tmp;
+                                // NSB: why? The range would be empty. 
+                                std::swap(lo_val, hi_val);
                             }
 
                             expr_ref_vector cond_rhs_terms(m);
-                            for (unsigned i = lo_val.get_unsigned(); i <= hi_val.get_unsigned(); ++i) {
+                            for (unsigned i = lo_val; i <= hi_val; ++i) {
                                 zstring str_const(i);
                                 expr_ref str_expr(u.str.mk_string(str_const), m);
                                 cond_rhs_terms.push_back(ctx.mk_eq_atom(ch, str_expr));