mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix #4355

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-17 12:28:30 -07:00
parent 951c769fc9
commit 30f17b1509
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/seq_decl_plugin.cpp
View file

@ -739,9 +739,12 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_STRING_STOI:
case OP_STRING_LT:
case OP_STRING_LE:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
case OP_STRING_IS_DIGIT:
case OP_STRING_TO_CODE:
case OP_STRING_FROM_CODE:
m.raise_exception("character function is not yet supported");
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
@ -824,6 +827,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
m_has_re = true;
return mk_assoc_fun(k, arity, domain, range, k, k);
case OP_SEQ_REPLACE_RE_ALL:
case OP_SEQ_REPLACE_RE:
m_has_re = true;
case OP_SEQ_REPLACE_ALL:
m.raise_exception("replace-all operation is not yet supported");
return mk_str_fun(k, arity, domain, range, k);
case OP_SEQ_CONCAT:
return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT);