From 46ac718790b5cfddc4d5ed215a301618285018de Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 26 Apr 2017 17:24:05 -0400 Subject: [PATCH 1/4] theory_str frontend changes --- src/ast/ast.cpp | 1 + src/ast/ast.h | 3 ++ src/ast/rewriter/seq_rewriter.cpp | 72 ++++++++++++++++++++++++++++--- src/ast/rewriter/seq_rewriter.h | 2 + src/ast/seq_decl_plugin.cpp | 4 +- 5 files changed, 76 insertions(+), 6 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7be7300a2..5f2de5170 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include"ast.h" #include"ast_pp.h" #include"ast_ll_pp.h" diff --git a/src/ast/ast.h b/src/ast/ast.h index 9259d5431..6bb3b01c9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -117,6 +117,9 @@ public: explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); + } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 3737f4651..85d2ba749 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con switch(f->get_decl_kind()) { case OP_SEQ_UNIT: - return BR_FAILED; + SASSERT(num_args == 1); + return mk_seq_unit(args[0], result); case OP_SEQ_EMPTY: return BR_FAILED; case OP_RE_PLUS: @@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_re_union(args[0], args[1], result); case OP_RE_RANGE: - return BR_FAILED; + SASSERT(num_args == 2); + return mk_re_range(args[0], args[1], result); case OP_RE_INTERSECT: SASSERT(num_args == 2); return mk_re_inter(args[0], args[1], result); @@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return BR_FAILED; } +/* + * (seq.unit (_ BitVector 8)) ==> String constant + */ +br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { + sort * s = m().get_sort(e); + bv_util bvu(m()); + + if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) { + // specifically we want (_ BitVector 8) + rational n_val; + unsigned int n_size; + if (bvu.is_numeral(e, n_val, n_size)) { + if (n_size == 8) { + // convert to string constant + char ch = (char)n_val.get_int32(); + TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); + char s_tmp[2] = {ch, '\0'}; + symbol s(s_tmp); + result = m_util.str.mk_string(s); + return BR_DONE; + } + } + } + + return BR_FAILED; +} + /* string + string = string a + (b + c) = (a + b) + c @@ -1401,6 +1430,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { return BR_FAILED; } +/* + * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + */ +br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { + TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); + zstring str_lo, str_hi; + if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { + if (str_lo.length() == 1 && str_hi.length() == 1) { + unsigned int c1 = str_lo[0]; + unsigned int c2 = str_hi[0]; + if (c1 > c2) { + // exchange c1 and c2 + unsigned int tmp = c1; + c2 = c1; + c1 = tmp; + } + zstring s(c1); + expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); + for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { + zstring s_ch(ch); + expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); + acc = m_util.re.mk_union(acc, acc2); + } + result = acc; + return BR_REWRITE2; + } else { + m().raise_exception("string constants in re.range must have length 1"); + } + } + + return BR_FAILED; +} + /* emp+ = emp all+ = all @@ -1430,9 +1492,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { return BR_DONE; } - return BR_FAILED; -// result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); -// return BR_REWRITE2; + //return BR_FAILED; + result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); + return BR_REWRITE2; } br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 2b434f475..210b2d72c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -98,6 +98,7 @@ class seq_rewriter { re2automaton m_re2aut; expr_ref_vector m_es, m_lhs, m_rhs; + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_seq_length(expr* a, expr_ref& result); br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result); @@ -119,6 +120,7 @@ class seq_rewriter { 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(unsigned num_args, expr* const* args, expr_ref& result); + br_status mk_re_range(expr* lo, expr* hi, expr_ref& result); bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs); bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f282043e6..353fb975f 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -573,7 +573,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { m_char = bv.mk_sort(8); 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_string = m->mk_sort(symbol("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); parameter paramS(m_string); m_re = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS); @@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol init(); sort_names.push_back(builtin_name("Seq", SEQ_SORT)); sort_names.push_back(builtin_name("RegEx", RE_SORT)); + // SMT-LIB 2.5 compatibility sort_names.push_back(builtin_name("String", _STRING_SORT)); + sort_names.push_back(builtin_name("StringSequence", _STRING_SORT)); } app* seq_decl_plugin::mk_string(symbol const& s) { From 7811a91bad1d1f4586f82d221049de956567368a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 13:59:02 -0400 Subject: [PATCH 2/4] fix is_string_term() --- src/ast/seq_decl_plugin.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 2882e905d..833455ff4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -273,6 +273,15 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } + bool is_string_term(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && u.is_string(s)); + } + + bool is_non_string_sequence(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && !u.is_string(s)); + } MATCH_BINARY(is_concat); MATCH_UNARY(is_length); From 12dd6d786b238d35ddcebb412d51516aec7a56b1 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 21:24:40 -0400 Subject: [PATCH 3/4] remove redundant is_seq() check --- src/ast/seq_decl_plugin.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 833455ff4..76b5ebe31 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -275,7 +275,7 @@ public: bool is_string_term(expr const * n) const { sort * s = get_sort(n); - return (u.is_seq(s) && u.is_string(s)); + return u.is_string(s); } bool is_non_string_sequence(expr const * n) const { From 05958193ab3dc8f1780f1c9e2ae9c1ad7ecc4855 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 22:30:02 -0400 Subject: [PATCH 4/4] revert change to String sort declaration --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 353fb975f..bf238d8c5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -573,7 +573,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { m_char = bv.mk_sort(8); m->inc_ref(m_char); parameter param(m_char); - m_string = m->mk_sort(symbol("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); + m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); parameter paramS(m_string); m_re = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS);