some adjustments for stack use on large strings

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

src/ast/seq_decl_plugin.cpp

@@ -206,31 +206,45 @@ static const char esc_table[32][6] =
 std::string zstring::encode() const {
     SASSERT(m_encoding == ascii);
     std::ostringstream strm;
+    char buffer[100];
+    unsigned offset = 0;
+#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
     for (unsigned i = 0; i < m_buffer.size(); ++i) {
         unsigned char ch = m_buffer[i];
         if (0 <= ch && ch < 32) {
+            _flush();
             strm << esc_table[ch];
         }
         else if (ch == '\\') {
+            _flush();
             strm << "\\\\";
         }
         else if (ch >= 128) {
+            _flush();
             strm << "\\x" << std::hex << (unsigned)ch << std::dec; 
         }
         else {
-            strm << (char)(ch);
+            if (offset == 99) { 
+                _flush();
+            }
+            buffer[offset++] = (char)ch;
         }
     }
+    _flush();
     return strm.str();
 }
 
 std::string zstring::as_string() const {
     SASSERT(m_encoding == ascii);
     std::ostringstream strm;
+    char buffer[100];
+    unsigned offset = 0;
     for (unsigned i = 0; i < m_buffer.size(); ++i) {
+        if (offset == 99) { _flush(); }
         unsigned char ch = m_buffer[i];
-        strm << (char)(ch);        
+        buffer[offset++] = (char)(ch);        
     }
+    _flush();
     return strm.str();
 }
 
@@ -1007,8 +1021,7 @@ app* seq_util::str::mk_string(zstring const& s) const {
 }
 
 app*  seq_util::str::mk_char(zstring const& s, unsigned idx) const {
-    bv_util bvu(m);
+    return u.bv().mk_numeral(s[idx], s.num_bits());
-    return bvu.mk_numeral(s[idx], s.num_bits());
 }
 
 app*  seq_util::str::mk_char(char ch) const {
@@ -1016,26 +1029,27 @@ app*  seq_util::str::mk_char(char ch) const {
     return mk_char(s, 0);
 }
 
+bv_util& seq_util::bv() const {
+    if (!m_bv) m_bv = alloc(bv_util, m);
+    return *m_bv.get();
+}
+
 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) && sz == 8 && 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 {
-    bv_util bv(m);
+    return bv().mk_numeral(rational(ch), 8);
-    return bv.mk_numeral(rational(ch), 8);
 }
 
 app* seq_util::mk_le(expr* ch1, expr* ch2) const {
-    bv_util bv(m);
+    return bv().mk_ule(ch1, ch2);
-    return bv.mk_ule(ch1, ch2);
 }
 
 app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
-    bv_util bv(m);
+    return m.mk_not(bv().mk_ule(ch2, ch1));
-    return m.mk_not(bv.mk_ule(ch2, ch1));
 }
 
 bool seq_util::str::is_string(expr const* n, zstring& s) const {

src/ast/seq_decl_plugin.h

@@ -22,6 +22,7 @@ Revision History:
 #define SEQ_DECL_PLUGIN_H_
 
 #include "ast/ast.h"
+#include "ast/bv_decl_plugin.h"
 
 
 enum seq_sort_kind {
@@ -216,6 +217,8 @@ class seq_util {
     ast_manager& m;
     seq_decl_plugin& seq;
     family_id m_fid;
+    mutable scoped_ptr<bv_util> m_bv;
+    bv_util& bv() const;
 public:
 
     ast_manager& get_manager() const { return m; }

src/smt/theory_seq.cpp

@@ -4275,13 +4275,17 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     TRACE("seq", tout << mk_pp(n->get_owner(), m) << "\n";);
     e = get_ite_value(e);    
     if (m_util.is_seq(e)) {
-        ptr_vector<expr> concats;
+        unsigned start = m_concat.size();
-        get_ite_concat(e, concats);
+        SASSERT(m_todo.empty());
+        m_todo.push_back(e);
+        get_ite_concat(m_concat, m_todo);
         sort* srt = m.get_sort(e);
         seq_value_proc* sv = alloc(seq_value_proc, *this, srt);
        
+        unsigned end = m_concat.size();
         TRACE("seq", tout << mk_pp(e, m) << "\n";);
-        for (expr* c : concats) {
+        for (unsigned i = start; i < end; ++i) {
+            expr* c = m_concat[i];
             expr *c1;
             TRACE("seq", tout << mk_pp(c, m) << "\n";);
             if (m_util.str.is_unit(c, c1)) {
@@ -4301,6 +4305,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
                 sv->add_string(mk_value(to_app(c)));
             }
         }
+        m_concat.shrink(start);
         return sv;
     }
     else {
@@ -4308,7 +4313,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
     }
 }
 
-
 app* theory_seq::mk_value(app* e) {
     expr_ref result(m);
     e = get_ite_value(e);
@@ -6407,17 +6411,18 @@ bool theory_seq::canonizes(bool sign, expr* e) {
 }
 
 
-void theory_seq::get_ite_concat(expr* e, ptr_vector<expr>& concats) {
+void theory_seq::get_ite_concat(ptr_vector<expr>& concats, ptr_vector<expr>& todo) {
     expr* e1 = nullptr, *e2 = nullptr;
-    while (true) {
+    while (!todo.empty()) {
+        expr* e = todo.back();
+        todo.pop_back();
         e = m_rep.find(e);
         e = get_ite_value(e);
         if (m_util.str.is_concat(e, e1, e2)) {
-            get_ite_concat(e1, concats);
+            todo.push_back(e2, e1);
-            e = e2;
-            continue;
         }        
+        else {
             concats.push_back(e);        
-        return;
+        }
     }
 }

src/smt/theory_seq.h

@@ -383,7 +383,7 @@ namespace smt {
         symbol           m_prefix, m_suffix, m_accept, m_reject;
         symbol           m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
         symbol           m_pre, m_post, m_eq, m_seq_align;
-        ptr_vector<expr> m_todo;
+        ptr_vector<expr> m_todo, m_concat;
         unsigned         m_internalize_depth;
         expr_ref_vector  m_ls, m_rs, m_lhs, m_rhs;
 
@@ -432,7 +432,7 @@ namespace smt {
 
         void init_model(expr_ref_vector const& es);
         app* get_ite_value(expr* a);
-        void get_ite_concat(expr* e, ptr_vector<expr>& concats);
+        void get_ite_concat(ptr_vector<expr>& head, ptr_vector<expr>& tail);
         
         void len_offset(expr* e, rational val);
         void prop_arith_to_len_offset();