From e96f9de70b56554ec6564741607041a5c12f795e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Nov 2018 06:02:32 -0800 Subject: [PATCH] perf #1988 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 8 ++++---- src/ast/seq_decl_plugin.h | 1 + src/smt/theory_seq.cpp | 11 +++++++++-- 3 files changed, 14 insertions(+), 6 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 8fc130ef1..c4813f9f7 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -435,7 +435,7 @@ void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* do } void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { - ptr_vector binding; + m_binding.reset(); ast_manager& m = *m_manager; if (sig.m_dom.size() != dsz) { std::ostringstream strm; @@ -445,10 +445,10 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { - is_match = match(binding, dom[i], sig.m_dom[i].get()); + is_match = match(m_binding, dom[i], sig.m_dom[i].get()); } if (range && is_match) { - is_match = match(binding, range, sig.m_range); + is_match = match(m_binding, range, sig.m_range); } if (!is_match) { std::ostringstream strm; @@ -474,7 +474,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran strm << "is ambiguous. Function takes no arguments and sort of range has not been constrained"; m.raise_exception(strm.str().c_str()); } - range_out = apply_binding(binding, sig.m_range); + range_out = apply_binding(m_binding, sig.m_range); SASSERT(range_out); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index f8107f1e0..4b23f81d0 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -140,6 +140,7 @@ class seq_decl_plugin : public decl_plugin { }; ptr_vector m_sigs; + ptr_vector m_binding; bool m_init; symbol m_stringc_sym; symbol m_charc_sym; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 44acfdfd6..ccd85c42a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5553,8 +5553,15 @@ void theory_seq::propagate_accept(literal lit, expr* acc) { void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { TRACE("seq", tout << "add_theory_assumption " << m_util.has_re() << "\n";); if (m_util.has_re()) { - expr_ref dlimit = mk_max_unfolding_depth(); - m_max_unfolding_lit = mk_literal(dlimit); + expr_ref dlimit(m); + if (m_max_unfolding_lit != null_literal && + m_max_unfolding_depth == 1) { + dlimit = mk_max_unfolding_depth(); + m_max_unfolding_lit = mk_literal(dlimit); + } + else { + dlimit = get_context().bool_var2expr(m_max_unfolding_lit.var()); + } TRACE("seq", tout << "add_theory_assumption " << dlimit << " " << assumptions << "\n";); assumptions.push_back(dlimit); }