From ab5905cf7fd5299fa27d76ee2d3aa959d68f8ec0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jan 2020 22:08:24 -0800 Subject: [PATCH] some adjustments for stack use on large strings Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 38 +++++++++++++++++++++++++------------ src/ast/seq_decl_plugin.h | 3 +++ src/smt/theory_seq.cpp | 27 +++++++++++++++----------- src/smt/theory_seq.h | 4 ++-- 4 files changed, 47 insertions(+), 25 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 3efbc85bb..3bfe25877 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/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 bvu.mk_numeral(s[idx], s.num_bits()); + return u.bv().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 { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 82eaa3fb0..f94c3aa38 100644 --- a/src/ast/seq_decl_plugin.h +++ b/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 m_bv; + bv_util& bv() const; public: ast_manager& get_manager() const { return m; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b00c248a6..b739d528e 100644 --- a/src/smt/theory_seq.cpp +++ b/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 concats; - get_ite_concat(e, concats); + unsigned start = m_concat.size(); + 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& concats) { +void theory_seq::get_ite_concat(ptr_vector& concats, ptr_vector& 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); - e = e2; - continue; + todo.push_back(e2, e1); } - concats.push_back(e); - return; + else { + concats.push_back(e); + } } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 63efdeef2..709c7741f 100644 --- a/src/smt/theory_seq.h +++ b/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 m_todo; + ptr_vector 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& concats); + void get_ite_concat(ptr_vector& head, ptr_vector& tail); void len_offset(expr* e, rational val); void prop_arith_to_len_offset();