From 08bfd0841221833bf146a70f8fe9f5801eb1ee65 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Dec 2015 22:15:56 -0800 Subject: [PATCH] merging seq and string Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 5 ++ src/ast/rewriter/seq_rewriter.cpp | 30 ++------ src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/seq_decl_plugin.cpp | 119 +++++++++++++++--------------- src/ast/seq_decl_plugin.h | 45 +++++------ src/smt/theory_seq_empty.h | 6 +- 6 files changed, 93 insertions(+), 114 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 9ffbbd127..62a6a586e 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -424,6 +424,11 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { fs.push_back(mk_unsigned(m, sbits)); return mk_seq1(m, fs.begin(), fs.end(), f2f(), "_"); } + if (get_sutil().is_seq(s) && !get_sutil().is_string(s)) { + ptr_buffer fs; + fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); + return mk_seq1(m, fs.begin(), fs.end(), f2f(), "Seq"); + } return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ac87bdb3d..00b94e60d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -19,6 +19,7 @@ Notes: #include"seq_rewriter.h" #include"arith_decl_plugin.h" +#include"ast_pp.h" br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -28,13 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_SEQ_UNIT: case OP_SEQ_EMPTY: - case OP_SEQ_CONCAT: - case OP_SEQ_CONS: - case OP_SEQ_REV_CONS: - case OP_SEQ_HEAD: - case OP_SEQ_TAIL: - case OP_SEQ_LAST: - case OP_SEQ_FIRST: case OP_SEQ_PREFIX_OF: case OP_SEQ_SUFFIX_OF: case OP_SEQ_SUBSEQ_OF: @@ -49,8 +43,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_CONCAT: case OP_RE_UNION: case OP_RE_INTERSECT: - case OP_RE_COMPLEMENT: - case OP_RE_DIFFERENCE: case OP_RE_LOOP: case OP_RE_EMPTY_SET: case OP_RE_FULL_SET: @@ -63,9 +55,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con // string specific operators. case OP_STRING_CONST: return BR_FAILED; - case OP_STRING_CONCAT: + case OP_SEQ_CONCAT: + case _OP_STRING_CONCAT: SASSERT(num_args == 2); - return mk_str_concat(args[0], args[1], result); + return mk_seq_concat(args[0], args[1], result); case OP_STRING_LENGTH: SASSERT(num_args == 1); return mk_str_length(args[0], result); @@ -96,19 +89,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STRING_STOI: SASSERT(num_args == 1); return mk_str_stoi(args[0], result); - //case OP_STRING_U16TOS: - //case OP_STRING_STOU16: - //case OP_STRING_U32TOS: - //case OP_STRING_STOU32: case OP_STRING_IN_REGEXP: case OP_STRING_TO_REGEXP: - case OP_REGEXP_CONCAT: - case OP_REGEXP_UNION: - case OP_REGEXP_INTER: - case OP_REGEXP_STAR: - case OP_REGEXP_PLUS: - case OP_REGEXP_OPT: - case OP_REGEXP_RANGE: case OP_REGEXP_LOOP: return BR_FAILED; } @@ -122,7 +104,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con "" + a = a (a + string) + string = a + string */ -br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) { +br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { std::string s1, s2; expr* c, *d; bool isc1 = m_util.str.is_const(a, s1); @@ -145,7 +127,7 @@ br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) { } if (m_util.str.is_concat(a, c, d) && m_util.str.is_const(d, s1) && isc2) { - result = m_util.str.mk_string(s1 + s2); + result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2)); return BR_DONE; } return BR_FAILED; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index cefa451fa..2d2909018 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -34,7 +34,7 @@ class seq_rewriter { arith_util m_autil; ptr_vector m_es; - br_status mk_str_concat(expr* a, expr* b, expr_ref& result); + br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_str_length(expr* a, expr_ref& result); br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result); br_status mk_str_strctn(expr* a, expr* b, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7a48d8efd..5fd8c0df7 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -19,16 +19,19 @@ Revision History: #include "seq_decl_plugin.h" #include "arith_decl_plugin.h" #include "array_decl_plugin.h" +#include "ast_pp.h" #include seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), - m_string(0) {} + m_string(0), + m_char(0) {} void seq_decl_plugin::finalize() { for (unsigned i = 0; i < m_sigs.size(); ++i) dealloc(m_sigs[i]); m_manager->dec_ref(m_string); + m_manager->dec_ref(m_char); } bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { @@ -38,29 +41,32 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { } bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { + ast_manager& m = *m_manager; if (s == sP) return true; unsigned i; if (is_sort_param(sP, i)) { if (binding.size() <= i) binding.resize(i+1); if (binding[i] && (binding[i] != s)) return false; + TRACE("seq", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";); binding[i] = s; return true; } + if (s->get_family_id() == sP->get_family_id() && s->get_decl_kind() == sP->get_decl_kind() && - s->get_name() == sP->get_name()) { - SASSERT(s->get_num_parameters() == sP->get_num_parameters()); - for (unsigned i = 0; i < s->get_num_parameters(); ++i) { - parameter const& p = s->get_parameter(i); - if (p.is_ast() && is_sort(p.get_ast())) { - parameter const& p2 = sP->get_parameter(i); - if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false; - } + s->get_num_parameters() == sP->get_num_parameters()) { + for (unsigned i = 0; i < s->get_num_parameters(); ++i) { + parameter const& p = s->get_parameter(i); + if (p.is_ast() && is_sort(p.get_ast())) { + parameter const& p2 = sP->get_parameter(i); + if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false; } + } return true; } else { + TRACE("seq", tout << "Could not match " << mk_pp(s, m) << " and " << mk_pp(sP, m) << "\n";); return false; } } @@ -71,6 +77,11 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { ptr_vector binding; ast_manager& m = *m_manager; + TRACE("seq", + tout << sig.m_name << ": "; + for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " "; + if (range) tout << " range: " << mk_pp(range, m); + tout << "\n";); if (dsz == 0) { std::ostringstream strm; strm << "Unexpected number of arguments to '" << sig.m_name << "' "; @@ -91,6 +102,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); + TRACE("seq", tout << mk_pp(range_out, m) << "\n";); } void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { @@ -162,10 +174,8 @@ void seq_decl_plugin::init() { sort* u16T = 0; sort* u32T = 0; sort* seqAseqA[2] = { seqA, seqA }; - sort* seqAA[2] = { seqA, A }; sort* seqAB[2] = { seqA, B }; sort* seqAreA[2] = { seqA, reA }; - sort* AseqA[2] = { A, seqA }; sort* reAreA[2] = { reA, reA }; sort* AA[2] = { A, A }; sort* seqABB[3] = { seqA, B, B }; @@ -177,30 +187,22 @@ void seq_decl_plugin::init() { sort* str2TintT[3] = { strT, strT, 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-concat", 1, 2, seqAseqA, seqA); - m_sigs[OP_SEQ_CONS] = alloc(psig, m, "seq-cons", 1, 2, AseqA, seqA); - m_sigs[OP_SEQ_REV_CONS] = alloc(psig, m, "seq-rev-cons", 1, 2, seqAA, seqA); - m_sigs[OP_SEQ_HEAD] = alloc(psig, m, "seq-head", 1, 1, &seqA, A); - m_sigs[OP_SEQ_TAIL] = alloc(psig, m, "seq-tail", 1, 1, &seqA, seqA); - m_sigs[OP_SEQ_LAST] = alloc(psig, m, "seq-last", 1, 1, &seqA, A); - m_sigs[OP_SEQ_FIRST] = alloc(psig, m, "seq-first", 1, 1, &seqA, seqA); - m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq-prefix-of", 1, 2, seqAseqA, boolT); - m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq-suffix-of", 1, 2, seqAseqA, boolT); + 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_OF] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT); + m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_SUBSEQ_OF] = alloc(psig, m, "seq-subseq-of", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq-extract", 2, 3, seqABB, seqA); m_sigs[OP_SEQ_NTH] = alloc(psig, m, "seq-nth", 2, 2, seqAB, A); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq-length", 1, 1, &seqA, intT); - m_sigs[OP_RE_PLUS] = alloc(psig, m, "re-plus", 1, 1, &reA, reA); - m_sigs[OP_RE_STAR] = alloc(psig, m, "re-star", 1, 1, &reA, reA); - m_sigs[OP_RE_OPTION] = alloc(psig, m, "re-option", 1, 1, &reA, reA); - m_sigs[OP_RE_RANGE] = alloc(psig, m, "re-range", 1, 2, AA, reA); - m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re-concat", 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-intersect", 1, 2, reAreA, reA); - m_sigs[OP_RE_DIFFERENCE] = alloc(psig, m, "re-difference", 1, 2, reAreA, reA); - m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re-complement", 1, 1, &reA, reA); + 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); @@ -209,7 +211,7 @@ void seq_decl_plugin::init() { m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA); m_sigs[OP_RE_MEMBER] = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT); m_sigs[OP_STRING_CONST] = 0; - m_sigs[OP_STRING_CONCAT] = alloc(psig, m, "str.++", 0, 2, str2T, strT); + m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT); m_sigs[OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT); m_sigs[OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT); m_sigs[OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT); @@ -222,19 +224,15 @@ void seq_decl_plugin::init() { m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); 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_REGEXP_CONCAT] = alloc(psig, m, "re.++", 0, 2, re2T, reT); - m_sigs[OP_REGEXP_UNION] = alloc(psig, m, "re.union", 0, 2, re2T, reT); - m_sigs[OP_REGEXP_INTER] = alloc(psig, m, "re.inter", 0, 2, re2T, reT); - m_sigs[OP_REGEXP_STAR] = alloc(psig, m, "re.*", 0, 1, &reT, reT); - m_sigs[OP_REGEXP_PLUS] = alloc(psig, m, "re.+", 0, 1, &reT, reT); - m_sigs[OP_REGEXP_OPT] = alloc(psig, m, "re.opt", 0, 1, &reT, reT); - m_sigs[OP_REGEXP_RANGE] = alloc(psig, m, "re.range", 0, 2, str2T, reT); m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments. } void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { decl_plugin::set_manager(m, id); - m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, STRING_SORT, 0, (parameter const*)0)); + m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, CHAR_SORT, 0, (parameter const*)0)); + m->inc_ref(m_char); + parameter param(m_char); + m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); } @@ -249,6 +247,9 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { m.raise_exception("invalid sequence sort, parameter is not a sort"); } + if (parameters[0].get_ast() == m_char) { + return m_string; + } return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters)); case RE_SORT: if (num_parameters != 1) { @@ -260,6 +261,8 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); case STRING_SORT: return m_string; + case CHAR_SORT: + return m_char; default: UNREACHABLE(); return 0; @@ -274,12 +277,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, switch(k) { case OP_SEQ_UNIT: case OP_SEQ_EMPTY: - case OP_SEQ_CONS: - case OP_SEQ_REV_CONS: - case OP_SEQ_HEAD: - case OP_SEQ_TAIL: - case OP_SEQ_LAST: - case OP_SEQ_FIRST: case OP_SEQ_PREFIX_OF: case OP_SEQ_SUFFIX_OF: case OP_SEQ_SUBSEQ_OF: @@ -289,9 +286,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_OPTION: case OP_RE_RANGE: case OP_RE_UNION: - case OP_RE_INTERSECT: - case OP_RE_DIFFERENCE: - case OP_RE_COMPLEMENT: case OP_RE_EMPTY_SEQ: case OP_RE_EMPTY_SET: case OP_RE_OF_SEQ: @@ -317,15 +311,28 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); - case OP_SEQ_CONCAT: - case OP_RE_CONCAT: - case OP_REGEXP_CONCAT: - case OP_STRING_CONCAT: { + case OP_SEQ_CONCAT: { + match_left_assoc(*m_sigs[k], arity, domain, range, rng); + + func_decl_info info(m_family_id, k); + info.set_left_associative(); + if (rng == m_string) { + return m.mk_func_decl(m_sigs[_OP_STRING_CONCAT]->m_name, rng, rng, rng, info); + } + return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); + } + case OP_RE_CONCAT: { match_left_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k); info.set_left_associative(); return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); } + case _OP_STRING_CONCAT: { + match_left_assoc(*m_sigs[k], arity, domain, range, rng); + func_decl_info info(m_family_id, OP_SEQ_CONCAT); + info.set_left_associative(); + return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); + } case OP_STRING_LENGTH: case OP_STRING_SUBSTR: @@ -339,12 +346,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_STRING_STOI: case OP_STRING_IN_REGEXP: case OP_STRING_TO_REGEXP: - case OP_REGEXP_UNION: - case OP_REGEXP_INTER: - case OP_REGEXP_STAR: - case OP_REGEXP_PLUS: - case OP_REGEXP_OPT: - case OP_REGEXP_RANGE: case OP_REGEXP_LOOP: 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)); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 35e2cbf8a..e85d01799 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -25,19 +25,14 @@ Revision History: enum seq_sort_kind { SEQ_SORT, RE_SORT, - STRING_SORT + STRING_SORT, + CHAR_SORT }; enum seq_op_kind { OP_SEQ_UNIT, OP_SEQ_EMPTY, OP_SEQ_CONCAT, - OP_SEQ_CONS, - OP_SEQ_REV_CONS, - OP_SEQ_HEAD, - OP_SEQ_TAIL, - OP_SEQ_LAST, - OP_SEQ_FIRST, OP_SEQ_PREFIX_OF, OP_SEQ_SUFFIX_OF, OP_SEQ_SUBSEQ_OF, @@ -52,8 +47,6 @@ enum seq_op_kind { OP_RE_CONCAT, OP_RE_UNION, OP_RE_INTERSECT, - OP_RE_COMPLEMENT, - OP_RE_DIFFERENCE, OP_RE_LOOP, OP_RE_EMPTY_SET, OP_RE_FULL_SET, @@ -65,7 +58,7 @@ enum seq_op_kind { // string specific operators. OP_STRING_CONST, - OP_STRING_CONCAT, + _OP_STRING_CONCAT, OP_STRING_LENGTH, OP_STRING_SUBSTR, OP_STRING_STRCTN, @@ -78,13 +71,6 @@ enum seq_op_kind { OP_STRING_STOI, OP_STRING_IN_REGEXP, OP_STRING_TO_REGEXP, - OP_REGEXP_CONCAT, - OP_REGEXP_UNION, - OP_REGEXP_INTER, - OP_REGEXP_STAR, - OP_REGEXP_PLUS, - OP_REGEXP_OPT, - OP_REGEXP_RANGE, OP_REGEXP_LOOP, LAST_SEQ_OP @@ -112,6 +98,7 @@ class seq_decl_plugin : public decl_plugin { bool m_init; symbol m_stringc_sym; sort* m_string; + sort* m_char; void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng); @@ -148,6 +135,8 @@ public: virtual bool is_unique_value(app * e) const { return is_value(e); } + bool is_char(ast* a) const { return a == m_char; } + app* mk_string(symbol const& s); }; @@ -159,6 +148,9 @@ public: ast_manager& get_manager() const { return m; } + bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); } + bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } + class str { seq_util& u; ast_manager& m; @@ -169,7 +161,7 @@ public: app* mk_string(symbol const& s); app* mk_string(char const* s) { return mk_string(symbol(s)); } app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); } - app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_CONCAT, 2, es); } + app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); } app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); } @@ -183,8 +175,7 @@ public: return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } - bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); } - bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_CONCAT); } + bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LENGTH); } bool is_substr(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); } bool is_strctn(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRCTN); } @@ -222,13 +213,13 @@ public: re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} bool is_to_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); } - bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_CONCAT); } - bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_UNION); } - bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_INTER); } - bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_STAR); } - bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_PLUS); } - bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_OPT); } - bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_RANGE); } + bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } + bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); } + bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); } + bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); } + bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); } + bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); } + bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); } bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); } MATCH_UNARY(is_to_regexp); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index b99336b29..03ea3edf8 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -42,13 +42,13 @@ namespace smt { } virtual expr* get_some_value(sort* s) { - if (u.str.is_string(s)) + if (u.is_string(s)) return u.str.mk_string(symbol("")); NOT_IMPLEMENTED_YET(); return 0; } virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) { - if (u.str.is_string(s)) { + if (u.is_string(s)) { v1 = u.str.mk_string("a"); v2 = u.str.mk_string("b"); return true; @@ -57,7 +57,7 @@ namespace smt { return false; } virtual expr* get_fresh_value(sort* s) { - if (u.str.is_string(s)) { + if (u.is_string(s)) { while (true) { std::ostringstream strm; strm << "S" << m_next++;