mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
starting regex support, rewriter
This commit is contained in:
Murphy Berzish
parent
a808a8c587
commit
4c34629806
4 changed files with 63 additions and 0 deletions
|
|
@ -198,6 +198,27 @@ br_status str_rewriter::mk_str_Replace(expr * base, expr * source, expr * target
|
|||
}
|
||||
}
|
||||
|
||||
br_status str_rewriter::mk_re_Str2Reg(expr * str, expr_ref & result) {
|
||||
// the argument to Str2Reg *must* be a string constant
|
||||
// TODO is an assertion error too strict here? this basically crashes the solver
|
||||
VERIFY(m_strutil.is_string(str));
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status str_rewriter::mk_re_RegexIn(expr * str, expr * re, expr_ref & result) {
|
||||
// fast path:
|
||||
// (RegexIn E (Str2Reg S)) --> (= E S)
|
||||
if (m_strutil.is_re_Str2Reg(re)) {
|
||||
TRACE("t_str_rw", tout << "RegexIn fast path: " << mk_pp(str, m()) << " in " << mk_pp(re, m()) << std::endl;);
|
||||
expr * regexStr = to_app(re)->get_arg(0);
|
||||
VERIFY(m_strutil.is_string(regexStr));
|
||||
result = m().mk_eq(str, regexStr);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
SASSERT(f->get_family_id() == get_fid());
|
||||
|
||||
|
|
@ -229,6 +250,12 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_STR_REPLACE:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_Replace(args[0], args[1], args[2], result);
|
||||
case OP_RE_STR2REGEX:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_re_Str2Reg(args[0], result);
|
||||
case OP_RE_REGEXIN:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_re_RegexIn(args[0], args[1], result);
|
||||
default:
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -49,6 +49,9 @@ public:
|
|||
br_status mk_str_LastIndexof(expr * haystack, expr * needle, expr_ref & result);
|
||||
br_status mk_str_Replace(expr * base, expr * source, expr * target, expr_ref & result);
|
||||
|
||||
br_status mk_re_Str2Reg(expr * str, expr_ref & result);
|
||||
br_status mk_re_RegexIn(expr * str, expr * re, expr_ref & result);
|
||||
|
||||
bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change);
|
||||
bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change);
|
||||
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Revision History:
|
|||
str_decl_plugin::str_decl_plugin():
|
||||
m_strv_sym("String"),
|
||||
m_str_decl(0),
|
||||
m_regex_decl(0),
|
||||
m_concat_decl(0),
|
||||
m_length_decl(0),
|
||||
m_charat_decl(0),
|
||||
|
|
@ -35,6 +36,8 @@ str_decl_plugin::str_decl_plugin():
|
|||
m_lastindexof_decl(0),
|
||||
m_substr_decl(0),
|
||||
m_replace_decl(0),
|
||||
m_re_str2regex_decl(0),
|
||||
m_re_regexin_decl(0),
|
||||
m_arith_plugin(0),
|
||||
m_arith_fid(0),
|
||||
m_int_sort(0){
|
||||
|
|
@ -46,6 +49,7 @@ str_decl_plugin::~str_decl_plugin(){
|
|||
void str_decl_plugin::finalize(void) {
|
||||
#define DEC_REF(decl) if (decl) { m_manager->dec_ref(decl); } ((void) 0)
|
||||
DEC_REF(m_str_decl);
|
||||
DEC_REF(m_regex_decl);
|
||||
DEC_REF(m_concat_decl);
|
||||
DEC_REF(m_length_decl);
|
||||
DEC_REF(m_charat_decl);
|
||||
|
|
@ -57,6 +61,8 @@ void str_decl_plugin::finalize(void) {
|
|||
DEC_REF(m_lastindexof_decl);
|
||||
DEC_REF(m_substr_decl);
|
||||
DEC_REF(m_replace_decl);
|
||||
DEC_REF(m_re_str2regex_decl);
|
||||
DEC_REF(m_re_regexin_decl);
|
||||
DEC_REF(m_int_sort);
|
||||
}
|
||||
|
||||
|
|
@ -66,6 +72,10 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
|
|||
m->inc_ref(m_str_decl);
|
||||
sort * s = m_str_decl;
|
||||
|
||||
m_regex_decl = m->mk_sort(symbol("Regex"), sort_info(id, REGEX_SORT));
|
||||
m->inc_ref(m_regex_decl);
|
||||
sort * re = m_regex_decl;
|
||||
|
||||
SASSERT(m_manager->has_plugin(symbol("arith")));
|
||||
m_arith_fid = m_manager->mk_family_id("arith");
|
||||
m_arith_plugin = static_cast<arith_decl_plugin*>(m_manager->get_plugin(m_arith_fid));
|
||||
|
|
@ -122,6 +132,13 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) {
|
|||
m_replace_decl = m->mk_func_decl(symbol("Replace"), 3, d, s, func_decl_info(id, OP_STR_REPLACE));
|
||||
m_manager->inc_ref(m_replace_decl);
|
||||
}
|
||||
|
||||
m_re_str2regex_decl = m->mk_func_decl(symbol("Str2Reg"), s, re, func_decl_info(id, OP_RE_STR2REGEX));
|
||||
m_manager->inc_ref(m_re_str2regex_decl);
|
||||
|
||||
m_re_regexin_decl = m->mk_func_decl(symbol("RegexIn"), s, re, boolT, func_decl_info(id, OP_RE_REGEXIN));
|
||||
m_manager->inc_ref(m_re_regexin_decl);
|
||||
|
||||
}
|
||||
|
||||
decl_plugin * str_decl_plugin::mk_fresh() {
|
||||
|
|
@ -131,6 +148,7 @@ decl_plugin * str_decl_plugin::mk_fresh() {
|
|||
sort * str_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
|
||||
switch (k) {
|
||||
case STRING_SORT: return m_str_decl;
|
||||
case REGEX_SORT: return m_regex_decl;
|
||||
default: return 0;
|
||||
}
|
||||
}
|
||||
|
|
@ -148,6 +166,8 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) {
|
|||
case OP_STR_LASTINDEXOF: return m_lastindexof_decl;
|
||||
case OP_STR_SUBSTR: return m_substr_decl;
|
||||
case OP_STR_REPLACE: return m_replace_decl;
|
||||
case OP_RE_STR2REGEX: return m_re_str2regex_decl;
|
||||
case OP_RE_REGEXIN: return m_re_regexin_decl;
|
||||
default: return 0;
|
||||
}
|
||||
}
|
||||
|
|
@ -213,10 +233,13 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
|
|||
op_names.push_back(builtin_name("LastIndexof", OP_STR_LASTINDEXOF));
|
||||
op_names.push_back(builtin_name("Substring", OP_STR_SUBSTR));
|
||||
op_names.push_back(builtin_name("Replace", OP_STR_REPLACE));
|
||||
op_names.push_back(builtin_name("Str2Reg", OP_RE_STR2REGEX));
|
||||
op_names.push_back(builtin_name("RegexIn", OP_RE_REGEXIN));
|
||||
}
|
||||
|
||||
void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
|
||||
sort_names.push_back(builtin_name("String", STRING_SORT));
|
||||
sort_names.push_back(builtin_name("Regex", REGEX_SORT));
|
||||
}
|
||||
|
||||
bool str_decl_plugin::is_value(app * e) const {
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
|
||||
enum str_sort_kind {
|
||||
STRING_SORT,
|
||||
REGEX_SORT,
|
||||
};
|
||||
|
||||
enum str_op_kind {
|
||||
|
|
@ -40,6 +41,9 @@ enum str_op_kind {
|
|||
OP_STR_LASTINDEXOF,
|
||||
OP_STR_SUBSTR,
|
||||
OP_STR_REPLACE,
|
||||
// regular expression operators
|
||||
OP_RE_STR2REGEX,
|
||||
OP_RE_REGEXIN,
|
||||
// end
|
||||
LAST_STR_OP
|
||||
};
|
||||
|
|
@ -48,6 +52,7 @@ class str_decl_plugin : public decl_plugin {
|
|||
protected:
|
||||
symbol m_strv_sym;
|
||||
sort * m_str_decl;
|
||||
sort * m_regex_decl;
|
||||
|
||||
func_decl * m_concat_decl;
|
||||
func_decl * m_length_decl;
|
||||
|
|
@ -62,6 +67,9 @@ protected:
|
|||
func_decl * m_substr_decl;
|
||||
func_decl * m_replace_decl;
|
||||
|
||||
func_decl * m_re_str2regex_decl;
|
||||
func_decl * m_re_regexin_decl;
|
||||
|
||||
arith_decl_plugin * m_arith_plugin;
|
||||
family_id m_arith_fid;
|
||||
sort * m_int_sort;
|
||||
|
|
@ -103,6 +111,8 @@ public:
|
|||
bool is_string(expr const * n, const char ** val) const;
|
||||
bool is_string(expr const * n) const;
|
||||
|
||||
bool is_re_Str2Reg(expr const * n) const { return is_app_of(n, get_fid(), OP_RE_STR2REGEX); }
|
||||
|
||||
std::string get_string_constant_value(expr const *n) const;
|
||||
// TODO
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue