mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 07:36:38 +00:00
Code Activity

move get_std_regex_str to str_util

Browse source
This commit is contained in:
Murphy Berzish 2016-10-29 12:19:24 -04:00
parent ef0f6f1de3
commit 452eed6626
4 changed files with 46 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/ast/str_decl_plugin.cpp
View file

@ -331,3 +331,46 @@ str_util::str_util(ast_manager &m) :
m_plugin = static_cast<str_decl_plugin*>(m.get_plugin(m.mk_family_id(symbol("str"))));
m_fid = m_plugin->get_family_id();
}
static std::string str2RegexStr(std::string str) {
std::string res = "";
int len = str.size();
for (int i = 0; i < len; i++) {
char nc = str[i];
// 12 special chars
if (nc == '\\' || nc == '^' || nc == '$' || nc == '.' || nc == '|' || nc == '?'
|| nc == '*' || nc == '+' || nc == '(' || nc == ')' || nc == '[' || nc == '{') {
res.append(1, '\\');
}
res.append(1, str[i]);
}
return res;
}
std::string str_util::get_std_regex_str(expr * regex) {
app * a_regex = to_app(regex);
if (is_re_Str2Reg(a_regex)) {
expr * regAst = a_regex->get_arg(0);
std::string regStr = str2RegexStr(get_string_constant_value(regAst));
return regStr;
} else if (is_re_RegexConcat(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
expr * reg2Ast = a_regex->get_arg(1);
std::string reg1Str = get_std_regex_str(reg1Ast);
std::string reg2Str = get_std_regex_str(reg2Ast);
return "(" + reg1Str + ")(" + reg2Str + ")";
} else if (is_re_RegexUnion(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
expr * reg2Ast = a_regex->get_arg(1);
std::string reg1Str = get_std_regex_str(reg1Ast);
std::string reg2Str = get_std_regex_str(reg2Ast);
return "(" + reg1Str + ")|(" + reg2Str + ")";
} else if (is_re_RegexStar(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
std::string reg1Str = get_std_regex_str(reg1Ast);
return "(" + reg1Str + ")*";
} else {
TRACE("t_str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
UNREACHABLE(); return "";
}
}

2
src/ast/str_decl_plugin.h
View file

@ -182,6 +182,8 @@ public:
return m_manager.mk_app(get_fid(), OP_RE_REGEXSTAR, 1, es);
}
std::string get_std_regex_str(expr * regex);
};
#endif /* _STR_DECL_PLUGIN_H_ */

45
src/smt/theory_str.cpp
View file

@ -1572,49 +1572,6 @@ expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {
return regexIn;
}
static std::string str2RegexStr(std::string str) {
std::string res = "";
int len = str.size();
for (int i = 0; i < len; i++) {
char nc = str[i];
// 12 special chars
if (nc == '\\' || nc == '^' || nc == '$' || nc == '.' || nc == '|' || nc == '?'
|| nc == '*' || nc == '+' || nc == '(' || nc == ')' || nc == '[' || nc == '{') {
res.append(1, '\\');
}
res.append(1, str[i]);
}
return res;
}
std::string theory_str::get_std_regex_str(expr * regex) {
app * a_regex = to_app(regex);
if (is_Str2Reg(a_regex)) {
expr * regAst = a_regex->get_arg(0);
std::string regStr = str2RegexStr(m_strutil.get_string_constant_value(regAst));
return regStr;
} else if (is_RegexConcat(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
expr * reg2Ast = a_regex->get_arg(1);
std::string reg1Str = get_std_regex_str(reg1Ast);
std::string reg2Str = get_std_regex_str(reg2Ast);
return "(" + reg1Str + ")(" + reg2Str + ")";
} else if (is_RegexUnion(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
expr * reg2Ast = a_regex->get_arg(1);
std::string reg1Str = get_std_regex_str(reg1Ast);
std::string reg2Str = get_std_regex_str(reg2Ast);
return "(" + reg1Str + ")|(" + reg2Str + ")";
} else if (is_RegexStar(a_regex)) {
expr * reg1Ast = a_regex->get_arg(0);
std::string reg1Str = get_std_regex_str(reg1Ast);
return "(" + reg1Str + ")*";
} else {
TRACE("t_str", tout << "BUG: unrecognized regex term " << mk_pp(regex, get_manager()) << std::endl;);
UNREACHABLE(); return "";
}
}
void theory_str::instantiate_axiom_RegexIn(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
@ -1629,7 +1586,7 @@ void theory_str::instantiate_axiom_RegexIn(enode * e) {
TRACE("t_str_detail", tout << "instantiate RegexIn axiom for " << mk_pp(ex, m) << std::endl;);
{
std::string regexStr = get_std_regex_str(ex->get_arg(1));
std::string regexStr = m_strutil.get_std_regex_str(ex->get_arg(1));
std::pair<expr*, std::string> key1(ex->get_arg(0), regexStr);
// skip Z3str's map check, because we already check if we set up axioms on this term
regex_in_bool_map[key1] = ex;

1
src/smt/theory_str.h
View file

@ -478,7 +478,6 @@ namespace smt {
expr * gen_unroll_conditional_options(expr * var, std::set<expr*> & unrolls, std::string lcmStr);
expr * gen_unroll_assign(expr * var, std::string lcmStr, expr * testerVar, int l, int h);
void reduce_virtual_regex_in(expr * var, expr * regex, expr_ref_vector & items);
std::string get_std_regex_str(expr * regex);
void check_regex_in(expr * nn1, expr * nn2);
void dump_assignments();