throttel extract/ite rewriting to avoid perf-bug exposed in example from Lucas Cordeiro and Alessandro Trindade

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

src/ast/rewriter/bv_rewriter.cpp

@@ -779,12 +779,15 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
         }
     }
 
-    if (m().is_ite(arg)) {
+    expr* c = nullptr, *t = nullptr, *e = nullptr;
-        result = m().mk_ite(to_app(arg)->get_arg(0),
+    if (m().is_ite(arg, c, t, e)) {
-                            m_mk_extract(high, low, to_app(arg)->get_arg(1)),
+        if ((t->get_ref_count() == 1 && e->get_ref_count() == 1) ||
-                            m_mk_extract(high, low, to_app(arg)->get_arg(2)));
+            (!m().is_ite(t) && !m().is_ite(e))) {
+            //std::cout << "n-ite\n";
+            result = m().mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e));
             return BR_REWRITE2;
         }
+    }
 
     return BR_FAILED;
 }

src/ast/rewriter/seq_rewriter.cpp

@@ -387,6 +387,7 @@ eautomaton* re2automaton::seq2aut(expr* e) {
 br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_family_id() == get_fid());
     
+    br_status st = BR_FAILED;
     switch(f->get_decl_kind()) {
         
     case OP_SEQ_UNIT:
@@ -448,7 +449,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         return mk_seq_length(args[0], result);
     case OP_SEQ_EXTRACT:
         SASSERT(num_args == 3);
-        return mk_seq_extract(args[0], args[1], args[2], result);
+        st = mk_seq_extract(args[0], args[1], args[2], result);
+        break;
     case OP_SEQ_CONTAINS: 
         SASSERT(num_args == 2);
         return mk_seq_contains(args[0], args[1], result);
@@ -499,7 +501,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case _OP_STRING_STRIDOF: 
         UNREACHABLE();
     }
-    return BR_FAILED;
+    TRACE("seq", tout << result << "\n";);
+    return st;
 }
 
 /*
@@ -607,6 +610,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
 
+    
     // case 1: pos<0 or len<=0
     // rewrite to ""
     if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) {
@@ -615,7 +619,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     }
     // case 1.1: pos >= length(base)
     // rewrite to ""
-    if (constantBase && constantPos && pos >= rational(s.length())) {
+    if (constantPos && constantBase && pos >= rational(s.length())) {
         result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
@@ -623,53 +627,75 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     constantPos &= pos.is_unsigned();
     constantLen &= len.is_unsigned();
 
-    if (constantBase && constantPos && constantLen) {
+    if (constantPos && constantLen && constantBase) {
-        if (pos.get_unsigned() + len.get_unsigned() >= s.length()) {
+        unsigned _pos = pos.get_unsigned();
+        unsigned _len = len.get_unsigned();
+        if (_pos + _len >= s.length()) {
             // case 2: pos+len goes past the end of the string
-            unsigned _len = s.length() - pos.get_unsigned() + 1;
+            unsigned _len = s.length() - _pos + 1;
-            result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len));
+            result = m_util.str.mk_string(s.extract(_pos, _len));
         } else {
             // case 3: pos+len still within string
-            result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned()));
+            result = m_util.str.mk_string(s.extract(_pos, _len));
         }
         return BR_DONE;
     }
 
-    if (constantPos && constantLen) {
+
-        unsigned _pos = pos.get_unsigned();
-        unsigned _len = len.get_unsigned();
-        SASSERT(_len > 0);
     expr_ref_vector as(m()), bs(m());
-        m_util.str.get_concat(a, as);
+    m_util.str.get_concat_units(a, as);
     if (as.empty()) {
+        result = m_util.str.mk_empty(m().get_sort(a));
+        return BR_DONE;
+    }
+
+    if (!constantPos) {
+        return BR_FAILED;
+    }
+    unsigned _pos = pos.get_unsigned();
+
+    // (extract s 0 (len s)) = s 
+    expr* a2 = nullptr;
+    if (_pos == 0 && m_util.str.is_length(c, a2) && a == a2) {
         result = a;
         return BR_DONE;
     }
-        for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
+
-            if (m_util.str.is_unit(as[i].get())) {
+    unsigned offset = 0;
-                if (_pos == 0) {
+    for (; offset < as.size() && m_util.str.is_unit(as.get(offset)) && offset < _pos; ++offset) {};
-                    bs.push_back(as[i].get());
+    if (offset == 0 && _pos > 0) {
-                    --_len;
-                }
-                else {
-                    --_pos;
-                }
-            }              
-            else {
         return BR_FAILED;
     }
+    if (_pos == 0 && !constantLen) {
+        return BR_FAILED;
     }
-        if (bs.empty()) {
+    // (extract (++ (unit x) (unit y)) 3 c) = empty
+    if (offset == as.size()) {
         result = m_util.str.mk_empty(m().get_sort(a));
-        }
-        else {
-            result = m_util.str.mk_concat(bs);
-        }
         return BR_DONE;
     }
+    SASSERT(offset != 0 || _pos == 0);
     
+    if (constantLen && _pos == offset) {
+        unsigned _len = len.get_unsigned();
+        // (extract (++ (unit a) (unit b) (unit c) x) 1 2) = (++ (unit b) (unit c))
+        unsigned i = offset;
+        for (; i < as.size() && m_util.str.is_unit(as.get(i)) && i - offset < _len; ++i);
+        if (i - offset == _len) {
+            result = m_util.str.mk_concat(_len, as.c_ptr() + offset);
+            return BR_DONE;
+        }
+    }
+    if (offset == 0) {
         return BR_FAILED;
     }
+    expr_ref len1(m()), pos1(m());
+    pos1 = m_autil.mk_sub(b, m_autil.mk_int(offset));
+    len1 = m_autil.mk_sub(c, m_autil.mk_int(offset));
+    result = m_util.str.mk_concat(as.size() - offset, as.c_ptr() + offset);
+    result = m_util.str.mk_substr(result, pos1, len1);
+    return BR_REWRITE3;
+}
 
 bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
     

src/smt/theory_seq.cpp

@@ -2396,6 +2396,7 @@ bool theory_seq::is_var(expr* a) const {
         !m_util.str.is_string(a) &&
         !m_util.str.is_unit(a) &&
         !m_util.str.is_itos(a) && 
+        !m_util.str.is_extract(a) && 
         !m.is_ite(a);
 }