From 21c4d451d8778d0a987096eb3a55d1d77f18c58c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 May 2020 14:26:44 -0700 Subject: [PATCH] parse RegLan Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 40 ++++++++++++++++++++++++------------- src/ast/seq_decl_plugin.h | 12 +++++++++-- 2 files changed, 36 insertions(+), 16 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index c310dea0e..5f19994ca 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -412,7 +412,7 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false), m_charc_sym("Char"), m_string(nullptr), m_char(nullptr), - m_re(nullptr), + m_reglan(nullptr), m_has_re(false), m_has_seq(false) {} @@ -422,7 +422,7 @@ void seq_decl_plugin::finalize() { } m_manager->dec_ref(m_string); m_manager->dec_ref(m_char); - m_manager->dec_ref(m_re); + m_manager->dec_ref(m_reglan); } bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { @@ -642,14 +642,15 @@ void seq_decl_plugin::init() { void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); bv_util bv(*m); + // to be changed to Unicode (abstract sort) m_char = bv.mk_sort(8); m->inc_ref(m_char); 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_re = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS); - m->inc_ref(m_re); + 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) { @@ -676,8 +677,12 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter } return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); } + case _CHAR_SORT: + return m_char; case _STRING_SORT: return m_string; + case _REGLAN_SORT: + return m_reglan; default: UNREACHABLE(); return nullptr; @@ -749,14 +754,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_re; + if (!range) range = m_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_re; - if (range == m_re) { + if (!range) range = m_reglan; + if (range == m_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)); } @@ -764,19 +769,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_re; + if (!range) range = m_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_re; + if (!range) range = m_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_re; - if (range == m_re) { + if (!range) range = m_reglan; + if (range == m_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)); } @@ -792,12 +797,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_re != domain[0] || !arith_util(m).is_int(domain[1])) { + if (m_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_re != domain[0] || !arith_util(m).is_int(domain[1]) || !arith_util(m).is_int(domain[2])) { + if (m_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)); @@ -932,8 +937,15 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol init(); sort_names.push_back(builtin_name("Seq", SEQ_SORT)); sort_names.push_back(builtin_name("RegEx", RE_SORT)); - // SMT-LIB 2.5 compatibility + + // TBD: + // sort_names.push_back(builtin_name("Unicode", CHAR_SORT)); + + // SMTLIB 2.6 RegLan, String + sort_names.push_back(builtin_name("RegLan", _REGLAN_SORT)); sort_names.push_back(builtin_name("String", _STRING_SORT)); + + // SMTLIB 2.5 compatibility sort_names.push_back(builtin_name("StringSequence", _STRING_SORT)); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 99a907aab..305db0a94 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -17,6 +17,12 @@ Revision History: Updated to string sequences 2015-12-5 +TBD: +- ((_ re.^ n) RegLan RegLan) +- (str.replace_re_all String RegLan String String) +- (str.replace_re String RegLan String String) +- (str.replace_all String String String String) + --*/ #ifndef SEQ_DECL_PLUGIN_H_ #define SEQ_DECL_PLUGIN_H_ @@ -28,7 +34,9 @@ Revision History: enum seq_sort_kind { SEQ_SORT, RE_SORT, - _STRING_SORT // internal only + _CHAR_SORT, // internal only + _STRING_SORT, + _REGLAN_SORT }; enum seq_op_kind { @@ -153,7 +161,7 @@ class seq_decl_plugin : public decl_plugin { symbol m_charc_sym; sort* m_string; sort* m_char; - sort* m_re; + sort* m_reglan; bool m_has_re; bool m_has_seq;