From 19779f1a9b0a567f498a1665805fbe7b3d68f14a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 31 Jan 2017 11:49:10 -0500 Subject: [PATCH] fix string operators in theory_str, this breaks theory_seq temporarily --- src/ast/seq_decl_plugin.cpp | 4 ++-- src/ast/str_decl_plugin.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 787648e19..779096038 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -477,8 +477,8 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_CHARAT] = alloc(psig, m, "str.at", 0, 2, strTint2T, strT); m_sigs[_OP_STRING_PREFIX] = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT); m_sigs[_OP_STRING_SUFFIX] = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT); - m_sigs[_OP_STRING_IN_REGEXP] = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT); - m_sigs[_OP_STRING_TO_REGEXP] = alloc(psig, m, "str.to.re", 0, 1, &strT, reT); + m_sigs[_OP_STRING_IN_REGEXP] = alloc(psig, m, "seqstr.in.re", 0, 2, strTreT, boolT); + m_sigs[_OP_STRING_TO_REGEXP] = alloc(psig, m, "seqstr.to.re", 0, 1, &strT, reT); m_sigs[_OP_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, 0, reT); m_sigs[_OP_REGEXP_FULL] = alloc(psig, m, "re.allchar", 0, 0, 0, reT); m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index bd6d70ebe..766fefdcf 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -297,8 +297,8 @@ void str_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("str.suffixof", OP_STR_SUFFIXOF)); op_names.push_back(builtin_name("str.to-int", OP_STR_STR2INT)); op_names.push_back(builtin_name("str.from-int", OP_STR_INT2STR)); - op_names.push_back(builtin_name("str.to.reg", OP_RE_STR2REGEX)); - op_names.push_back(builtin_name("str.in.reg", OP_RE_REGEXIN)); + op_names.push_back(builtin_name("str.to.re", OP_RE_STR2REGEX)); + op_names.push_back(builtin_name("str.in.re", OP_RE_REGEXIN)); op_names.push_back(builtin_name("re.++", OP_RE_REGEXCONCAT)); op_names.push_back(builtin_name("re.*", OP_RE_REGEXSTAR)); op_names.push_back(builtin_name("re.union", OP_RE_REGEXUNION));