From 90980842179961ed15e6df5294f0e1c43a19cf8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Mar 2021 11:54:44 -0700 Subject: [PATCH] reduce overhead of creating seq-plugin, enable parameter cleanup for #5095 --- src/ast/ast.cpp | 4 ++-- src/ast/bv_decl_plugin.cpp | 8 ++++---- src/ast/seq_decl_plugin.cpp | 35 +++++++++++++++++++++-------------- src/ast/seq_decl_plugin.h | 2 ++ 4 files changed, 29 insertions(+), 20 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 235e14f63..400ae7e9c 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1941,7 +1941,7 @@ void ast_manager::delete_node(ast * n) { #endif switch (n->get_kind()) { case AST_SORT: - if (to_sort(n)->m_info != nullptr && !m_debug_ref_count) { + if (to_sort(n)->m_info != nullptr) { sort_info * info = to_sort(n)->get_info(); info->del_eh(*this); dealloc(info); @@ -1949,7 +1949,7 @@ void ast_manager::delete_node(ast * n) { break; case AST_FUNC_DECL: { func_decl* f = to_func_decl(n); - if (f->m_info != nullptr && !m_debug_ref_count) { + if (f->m_info != nullptr) { func_decl_info * info = f->get_info(); if (info->is_lambda()) { push_dec_ref(m_lambda_defs[f]); diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 369492b7f..8f0ebe3d1 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -44,9 +44,9 @@ bv_decl_plugin::bv_decl_plugin(): void bv_decl_plugin::set_manager(ast_manager * m, family_id id) { decl_plugin::set_manager(m, id); - for (unsigned i = 1; i <= 64; i++) { + for (unsigned i = 1; i <= 64; i++) mk_bv_sort(i); - } + m_bit0 = m->mk_const_decl(symbol("bit0"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT0)); m_bit1 = m->mk_const_decl(symbol("bit1"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT1)); m->inc_ref(m_bit0); @@ -138,7 +138,7 @@ void bv_decl_plugin::finalize() { void bv_decl_plugin::mk_bv_sort(unsigned bv_size) { force_ptr_array_size(m_bv_sorts, bv_size + 1); - if (m_bv_sorts[bv_size] == 0) { + if (!m_bv_sorts[bv_size]) { parameter p(bv_size); sort_size sz; if (sort_size::is_very_big_base2(bv_size)) { @@ -155,7 +155,7 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) { inline sort * bv_decl_plugin::get_bv_sort(unsigned bv_size) { if (bv_size < (1 << 12)) { mk_bv_sort(bv_size); - return m_bv_sorts[bv_size]; + return m_bv_sorts[bv_size]; } parameter p(bv_size); sort_size sz(sort_size::mk_very_big()); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 57ae9b564..c16071cdf 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -172,7 +172,7 @@ sort* seq_decl_plugin::apply_binding(ptr_vector const& binding, sort* s) { if (p == m_char && s->get_decl_kind() == SEQ_SORT) return m_string; if (p == m_string && s->get_decl_kind() == RE_SORT) - return m_reglan; + return mk_reglan(); return mk_sort(s->get_decl_kind(), 1, ¶m); } return s; @@ -273,6 +273,16 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); } +sort* seq_decl_plugin::mk_reglan() { + if (!m_reglan) { + ast_manager& m = *m_manager; + parameter paramS(m_string); + m_reglan = m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, 1, ¶mS)); + m.inc_ref(m_reglan); + } + return m_reglan; +} + void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); m_char_plugin = static_cast(m_manager->get_plugin(m_manager->mk_family_id("char"))); @@ -281,9 +291,6 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { parameter param(m_char); m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); - parameter paramS(m_string); - m_reglan = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS); - m->inc_ref(m_reglan); } sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { @@ -313,7 +320,7 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter case _STRING_SORT: return m_string; case _REGLAN_SORT: - return m_reglan; + return mk_reglan(); default: UNREACHABLE(); return nullptr; @@ -403,14 +410,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case _OP_REGEXP_FULL_CHAR: m_has_re = true; - if (!range) range = m_reglan; + if (!range) range = mk_reglan(); match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_CHAR_SET)); case OP_RE_FULL_CHAR_SET: m_has_re = true; - if (!range) range = m_reglan; - if (range == m_reglan) { + if (!range) range = mk_reglan(); + if (range == mk_reglan()) { match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, k)); } @@ -418,19 +425,19 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_FULL_SEQ_SET: m_has_re = true; - if (!range) range = m_reglan; + if (!range) range = mk_reglan(); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k)); case _OP_REGEXP_EMPTY: m_has_re = true; - if (!range) range = m_reglan; + if (!range) range = mk_reglan(); match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.none"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET)); case OP_RE_EMPTY_SET: m_has_re = true; - if (!range) range = m_reglan; - if (range == m_reglan) { + if (!range) range = mk_reglan(); + if (range == mk_reglan()) { match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.none"), arity, domain, rng, func_decl_info(m_family_id, k)); } @@ -446,12 +453,12 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); case 2: - if (m_reglan != domain[0] || !arith_util(m).is_int(domain[1])) { + if (mk_reglan() != domain[0] || !arith_util(m).is_int(domain[1])) { m.raise_exception("Incorrect type of arguments passed to re.loop. Expecting regular expression and two integer parameters"); } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); case 3: - if (m_reglan != domain[0] || !arith_util(m).is_int(domain[1]) || !arith_util(m).is_int(domain[2])) { + if (mk_reglan() != domain[0] || !arith_util(m).is_int(domain[1]) || !arith_util(m).is_int(domain[2])) { m.raise_exception("Incorrect type of arguments passed to re.loop. Expecting regular expression and two integer parameters"); } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 02015f90b..f985f9de8 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -155,6 +155,8 @@ class seq_decl_plugin : public decl_plugin { void set_manager(ast_manager * m, family_id id) override; + sort* mk_reglan(); + public: seq_decl_plugin();