diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 96590a40a..f46201ec7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -40,13 +40,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_LOOP: case OP_RE_EMPTY_SET: case OP_RE_FULL_SET: - case OP_RE_EMPTY_SEQ: case OP_RE_OF_PRED: return BR_FAILED; - - // string specific operators. - case OP_STRING_CONST: - return BR_FAILED; + case OP_SEQ_CONCAT: SASSERT(num_args == 2); return mk_seq_concat(args[0], args[1], result); @@ -62,26 +58,31 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_SEQ_AT: SASSERT(num_args == 2); return mk_str_at(args[0], args[1], result); - case OP_STRING_STRIDOF: - SASSERT(num_args == 3); - return mk_str_stridof(args[0], args[1], args[2], result); - case OP_STRING_STRREPL: - SASSERT(num_args == 3); - return mk_str_strrepl(args[0], args[1], args[2], result); case OP_SEQ_PREFIX: SASSERT(num_args == 2); return mk_seq_prefix(args[0], args[1], result); case OP_SEQ_SUFFIX: SASSERT(num_args == 2); return mk_seq_suffix(args[0], args[1], result); + case OP_SEQ_TO_RE: + return BR_FAILED; + case OP_SEQ_IN_RE: + return BR_FAILED; + + case OP_STRING_CONST: + return BR_FAILED; + case OP_STRING_STRIDOF: + SASSERT(num_args == 3); + return mk_str_stridof(args[0], args[1], args[2], result); + case OP_STRING_STRREPL: + SASSERT(num_args == 3); + return mk_str_strrepl(args[0], args[1], args[2], result); case OP_STRING_ITOS: SASSERT(num_args == 1); return mk_str_itos(args[0], result); case OP_STRING_STOI: SASSERT(num_args == 1); return mk_str_stoi(args[0], result); - case OP_SEQ_TO_RE: - case OP_SEQ_IN_RE: case OP_REGEXP_LOOP: return BR_FAILED; case _OP_STRING_CONCAT: @@ -140,7 +141,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { m_es.reset(); m_util.str.get_concat(a, m_es); size_t len = 0; - size_t j = 0; + unsigned j = 0; for (unsigned i = 0; i < m_es.size(); ++i) { if (m_util.str.is_string(m_es[i], b)) { len += b.length(); @@ -154,7 +155,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { result = m_autil.mk_numeral(rational(len, rational::ui64()), true); return BR_DONE; } - if (j != m_es.size()) { + if (j != m_es.size() || j != 1) { expr_ref_vector es(m()); for (unsigned i = 0; i < j; ++i) { es.push_back(m_util.str.mk_length(m_es[i])); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index b47c4209d..bdbf033d6 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -186,28 +186,27 @@ void seq_decl_plugin::init() { sort* seqAintT[2] = { seqA, intT }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. - m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); - m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); - m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA); + m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); + m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); + m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA); m_sigs[OP_SEQ_PREFIX] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT); - m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); - m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); - m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq-length", 1, 1, &seqA, intT); - m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); - m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA); - m_sigs[OP_RE_OPTION] = alloc(psig, m, "re.opt", 1, 1, &reA, reA); - m_sigs[OP_RE_RANGE] = alloc(psig, m, "re.range", 1, 2, seqAseqA, reA); - m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA); - m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); - m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA); + m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); + m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); + m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); + m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); + m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA); + m_sigs[OP_RE_OPTION] = alloc(psig, m, "re.opt", 1, 1, &reA, reA); + m_sigs[OP_RE_RANGE] = alloc(psig, m, "re.range", 1, 2, seqAseqA, reA); + m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA); + m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA); + m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA); m_sigs[OP_RE_LOOP] = alloc(psig, m, "re-loop", 1, 1, &reA, reA); - m_sigs[OP_RE_EMPTY_SEQ] = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re-empty-set", 1, 0, 0, reA); m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re-full-set", 1, 0, 0, reA); - m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA); + m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); m_sigs[OP_STRING_CONST] = 0; m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c61e3cc43..dc7c4634b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -54,7 +54,6 @@ enum seq_op_kind { OP_RE_LOOP, OP_RE_EMPTY_SET, OP_RE_FULL_SET, - OP_RE_EMPTY_SEQ, OP_RE_OF_PRED,