From 30f17b1509319d15a1b9485b202799fc0d430b45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 May 2020 12:28:30 -0700 Subject: [PATCH] fix #4355 Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 3360e300e..8b1453af7 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -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);