mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

parse RegLan

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-16 14:26:44 -07:00
parent d3c00ca2c3
commit 21c4d451d8
2 changed files with 36 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/ast/seq_decl_plugin.cpp
View file

@ -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, &param));
m->inc_ref(m_string);
parameter paramS(m_string);
m_re = m->mk_sort(m_family_id, RE_SORT, 1, &paramS);
m->inc_ref(m_re);
m_reglan = m->mk_sort(m_family_id, RE_SORT, 1, &paramS);
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<builtin_name> & 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));
}

12
src/ast/seq_decl_plugin.h
View file

@ -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;