mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix string operators in theory_str, this breaks theory_seq temporarily

Browse source
This commit is contained in:
Murphy Berzish 2017-01-31 11:49:10 -05:00
parent ebcfa966c7
commit 19779f1a9b
2 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.cpp
View file

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

4
src/ast/str_decl_plugin.cpp
View file

@ -297,8 +297,8 @@ void str_decl_plugin::get_op_names(svector<builtin_name> & 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));