From 4753d93bb721ab4eeb332c15659b1d4dfab19211 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 16 May 2020 14:00:02 -0700 Subject: [PATCH] add some of the SMTLIB2.6 conventions and features to strings Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 5 +++++ src/ast/rewriter/seq_rewriter.h | 1 + src/ast/seq_decl_plugin.cpp | 20 ++++++++++++++------ src/ast/seq_decl_plugin.h | 7 +++++++ 4 files changed, 27 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index fbeafee4d..c429e34ba 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2152,6 +2152,11 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } +br_status seq_rewriter::mk_re_diff(expr* a, expr* b, expr_ref& result) { + result = m_util.re.mk_inter(a, m_util.re.mk_complement(b)); + return BR_REWRITE2; +} + br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { rational n1, n2; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 885189aa5..7c9f3c102 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -157,6 +157,7 @@ class seq_rewriter { br_status mk_re_inter(expr* a, expr* b, expr_ref& result); br_status mk_re_complement(expr* a, expr_ref& result); br_status mk_re_star(expr* a, expr_ref& result); + br_status mk_re_diff(expr* a, expr* b, expr_ref& result); br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index d9fa8c43e..c310dea0e 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -612,7 +612,7 @@ void seq_decl_plugin::init() { 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_COMPLEMENT] = alloc(psig, m, "re.complement", 1, 1, &reA, reA); + m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re.comp", 1, 1, &reA, reA); m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re.empty", 1, 0, nullptr, reA); m_sigs[OP_RE_FULL_SEQ_SET] = alloc(psig, m, "re.all", 1, 0, nullptr, reA); m_sigs[OP_RE_FULL_CHAR_SET] = alloc(psig, m, "re.allchar", 1, 0, nullptr, reA); @@ -632,9 +632,9 @@ 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_REGEXP_EMPTY] = alloc(psig, m, "re.nostr", 0, 0, nullptr, reT); + 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_EMPTY] = alloc(psig, m, "re.none", 0, 0, nullptr, reT); m_sigs[_OP_REGEXP_FULL_CHAR] = alloc(psig, m, "re.allchar", 0, 0, nullptr, reT); m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); } @@ -771,14 +771,14 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, m_has_re = true; if (!range) range = m_re; match(*m_sigs[k], arity, domain, range, rng); - return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET)); + return m.mk_func_decl(symbol("re.none"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET)); case OP_RE_EMPTY_SET: m_has_re = true; if (!range) range = m_re; if (range == m_re) { match(*m_sigs[k], arity, domain, range, rng); - return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, k)); + return m.mk_func_decl(symbol("re.none"), arity, domain, rng, func_decl_info(m_family_id, k)); } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k)); @@ -922,6 +922,10 @@ void seq_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name(m_sigs[i]->m_name.str().c_str(), i)); } } + op_names.push_back(builtin_name("str.in.re", _OP_STRING_IN_REGEXP)); + op_names.push_back(builtin_name("str.to.re", _OP_STRING_TO_REGEXP)); + op_names.push_back(builtin_name("re.nostr", _OP_REGEXP_EMPTY)); + op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT)); } void seq_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { @@ -1168,6 +1172,10 @@ app* seq_util::re::mk_empty(sort* s) { return m.mk_app(m_fid, OP_RE_EMPTY_SET, 0, nullptr, 0, nullptr, s); } +app* seq_util::re::mk_of_pred(expr* p) { + return m.mk_app(m_fid, OP_RE_OF_PRED, 0, nullptr, 1, &p); +} + bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi) { if (is_loop(n)) { app const* a = to_app(n); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index e6d1d753a..99a907aab 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -56,6 +56,7 @@ enum seq_op_kind { OP_RE_RANGE, OP_RE_CONCAT, OP_RE_UNION, + OP_RE_DIFF, OP_RE_INTERSECT, OP_RE_LOOP, OP_RE_COMPLEMENT, @@ -376,6 +377,7 @@ public: app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); } app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } + app* mk_diff(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_DIFF, r1, r2); } app* mk_complement(expr* r) { return m.mk_app(m_fid, OP_RE_COMPLEMENT, r); } app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); } app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); } @@ -387,11 +389,13 @@ public: app* mk_full_char(sort* s); app* mk_full_seq(sort* s); app* mk_empty(sort* s); + app* mk_of_pred(expr* p); bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } 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_intersection(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); } + bool is_diff(expr const* n) const { return is_app_of(n, m_fid, OP_RE_DIFF); } bool is_complement(expr const* n) const { return is_app_of(n, m_fid, OP_RE_COMPLEMENT); } 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); } @@ -401,15 +405,18 @@ public: bool is_empty(expr const* n) const { return is_app_of(n, m_fid, OP_RE_EMPTY_SET); } bool is_full_char(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_CHAR_SET); } bool is_full_seq(expr const* n) const { return is_app_of(n, m_fid, OP_RE_FULL_SEQ_SET); } + bool is_of_pred(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OF_PRED); } MATCH_UNARY(is_to_re); MATCH_BINARY(is_concat); MATCH_BINARY(is_union); MATCH_BINARY(is_intersection); + MATCH_BINARY(is_diff); MATCH_BINARY(is_range); MATCH_UNARY(is_complement); MATCH_UNARY(is_star); MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); + MATCH_UNARY(is_of_pred); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); bool is_loop(expr const* n, expr*& body, unsigned& lo); bool is_loop(expr const* n, expr*& body, expr*& lo, expr*& hi);