From 389845180c0f03cc0f808ac7cd1cab3bac691e1d Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 13 Jun 2016 16:34:24 -0400 Subject: [PATCH] add CharAt to theory_str and basic rewrite rule for constant CharAt exprs --- src/ast/rewriter/str_rewriter.cpp | 44 +++++++++++++++++++++++++++++++ src/ast/rewriter/str_rewriter.h | 2 ++ src/ast/str_decl_plugin.cpp | 10 ++++++- src/ast/str_decl_plugin.h | 6 ++++- 4 files changed, 60 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 35a255871..3967453d4 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -23,12 +23,56 @@ Notes: #include"ast_util.h" #include"well_sorted.h" +br_status str_rewriter::mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (CharAt " << mk_pp(arg0, m()) << " " << mk_pp(arg1, m()) << ")" << std::endl;); + // if arg0 is a string constant and arg1 is an integer constant, + // we can rewrite this by evaluating the expression + rational arg1Int; + if (m_strutil.is_string(arg0) && m_autil.is_numeral(arg1, arg1Int)) { + TRACE("t_str_rw", tout << "evaluating constant CharAt expression" << std::endl;); + std::string arg0Str = m_strutil.get_string_constant_value(arg0); + std::string resultStr; + if (arg1Int >= rational(0) && arg1Int <= rational((unsigned)arg0Str.length())) { + resultStr = arg0Str.at(arg1Int.get_unsigned()); + TRACE("t_str_rw", tout << "result is '" << resultStr << "'" << std::endl;); + } else { + resultStr = ""; + TRACE("t_str_rw", tout << "bogus length argument, result is empty string" << std::endl;); + } + result = m_strutil.mk_string(resultStr); + return BR_DONE; + } else { + // TODO NEXT + NOT_IMPLEMENTED_YET(); + /* + Z3_ast ts0 = my_mk_internal_string_var(t); + Z3_ast ts1 = my_mk_internal_string_var(t); + Z3_ast ts2 = my_mk_internal_string_var(t); + + Z3_ast cond = mk_2_and(t, Z3_mk_ge(ctx, args[1], mk_int(ctx, 0)), Z3_mk_lt(ctx, args[1], mk_length(t, args[0]))); + + Z3_ast and_item[3]; + and_item[0] = Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, mk_concat(t, ts1, ts2))); + and_item[1] = Z3_mk_eq(ctx, args[1], mk_length(t, ts0)); + and_item[2] = Z3_mk_eq(ctx, mk_length(t, ts1), mk_int(ctx, 1)); + Z3_ast thenBranch = Z3_mk_and(ctx, 3, and_item); + Z3_ast elseBranch = Z3_mk_eq(ctx, ts1, my_mk_str_value(t, "")); + breakdownAssert = Z3_mk_ite(ctx, cond, thenBranch, elseBranch); + return ts1; + */ + } +} + br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); TRACE("t_str_rw", tout << "rewrite app: " << f->get_name() << std::endl;); + // TODO more rewrites for really easy cases, e.g. (Concat "abc" "def")... switch(f->get_decl_kind()) { + case OP_STR_CHARAT: + SASSERT(num_args == 2); + return mk_str_CharAt(args[0], args[1], result); default: return BR_FAILED; } diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index fde36e92e..01ccde242 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -40,6 +40,8 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result); + bool reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change); bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change); diff --git a/src/ast/str_decl_plugin.cpp b/src/ast/str_decl_plugin.cpp index cd9cae5a5..03fde5aeb 100644 --- a/src/ast/str_decl_plugin.cpp +++ b/src/ast/str_decl_plugin.cpp @@ -26,6 +26,7 @@ str_decl_plugin::str_decl_plugin(): m_str_decl(0), m_concat_decl(0), m_length_decl(0), + m_charat_decl(0), m_arith_plugin(0), m_arith_fid(0), m_int_sort(0){ @@ -39,6 +40,7 @@ void str_decl_plugin::finalize(void) { DEC_REF(m_str_decl); DEC_REF(m_concat_decl); DEC_REF(m_length_decl); + DEC_REF(m_charat_decl); DEC_REF(m_int_sort); } @@ -64,7 +66,11 @@ void str_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_OP(m_concat_decl, "Concat", OP_STRCAT, s); - m_length_decl = m->mk_func_decl(symbol("Length"), s, i, func_decl_info(id, OP_STRLEN)); m_manager->inc_ref(m_length_decl); + m_length_decl = m->mk_func_decl(symbol("Length"), s, i, func_decl_info(id, OP_STRLEN)); + m_manager->inc_ref(m_length_decl); + + m_charat_decl = m->mk_func_decl(symbol("CharAt"), s, i, s, func_decl_info(id, OP_STR_CHARAT)); + m_manager->inc_ref(m_charat_decl); } decl_plugin * str_decl_plugin::mk_fresh() { @@ -82,6 +88,7 @@ func_decl * str_decl_plugin::mk_func_decl(decl_kind k) { switch(k) { case OP_STRCAT: return m_concat_decl; case OP_STRLEN: return m_length_decl; + case OP_STR_CHARAT: return m_charat_decl; default: return 0; } } @@ -138,6 +145,7 @@ app * str_decl_plugin::mk_fresh_string() { void str_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { op_names.push_back(builtin_name("Concat", OP_STRCAT)); op_names.push_back(builtin_name("Length", OP_STRLEN)); + op_names.push_back(builtin_name("CharAt", OP_STR_CHARAT)); } void str_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/str_decl_plugin.h b/src/ast/str_decl_plugin.h index 4f46fa5ac..049ef08ba 100644 --- a/src/ast/str_decl_plugin.h +++ b/src/ast/str_decl_plugin.h @@ -27,9 +27,12 @@ enum str_sort_kind { enum str_op_kind { OP_STR, /* string constants */ - // + // basic string operators OP_STRCAT, OP_STRLEN, + // higher-level string functions -- these are reduced to basic operations + OP_STR_CHARAT, + // end LAST_STR_OP }; @@ -40,6 +43,7 @@ protected: func_decl * m_concat_decl; func_decl * m_length_decl; + func_decl * m_charat_decl; arith_decl_plugin * m_arith_plugin; family_id m_arith_fid;