From 452eed662603e658372712f37250fd3a1bde2832 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 29 Oct 2016 12:19:24 -0400 Subject: [PATCH] move get_std_regex_str to str_util --- src/ast/str_decl_plugin.cpp | 43 +++++++++++++++++++++++++++++++++++ src/ast/str_decl_plugin.h | 2 ++ src/smt/theory_str.cpp | 45 +------------------------------------ src/smt/theory_str.h | 1 - 4 files changed, 46 insertions(+), 45 deletions(-) diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index e8455ffbd..333ae2a02 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -331,3 +331,46 @@ str_util::str_util(ast_manager &m) : m_plugin = static_cast(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 ""; + } +} diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index ba2b4f751..e9ab43865 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -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_ */ diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 23b2af0fb..1050e4a66 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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 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; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 85209c631..43552f31a 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -478,7 +478,6 @@ namespace smt { expr * gen_unroll_conditional_options(expr * var, std::set & 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();