From 7d09dbb8ec8685a0cb9b75bdf87733839fc179e1 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sun, 12 Jun 2016 20:46:52 -0400 Subject: [PATCH] basic infrastructure for string rewriting --- src/ast/rewriter/rewriter.txt | 2 + src/ast/rewriter/str_rewriter.cpp | 66 +++++++++++++++++++++++++++++++ src/ast/rewriter/str_rewriter.h | 46 +++++++++++++++++++++ src/ast/rewriter/th_rewriter.cpp | 8 ++++ 4 files changed, 122 insertions(+) create mode 100644 src/ast/rewriter/str_rewriter.cpp create mode 100644 src/ast/rewriter/str_rewriter.h diff --git a/src/ast/rewriter/rewriter.txt b/src/ast/rewriter/rewriter.txt index cdfba9f0f..a7a9e5eff 100644 --- a/src/ast/rewriter/rewriter.txt +++ b/src/ast/rewriter/rewriter.txt @@ -7,6 +7,8 @@ The following classes implement theory specific rewriting rules: - array_rewriter - datatype_rewriter - fpa_rewriter + - seq_rewriter + - str_rewriter Each of them provide the method br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp new file mode 100644 index 000000000..35a255871 --- /dev/null +++ b/src/ast/rewriter/str_rewriter.cpp @@ -0,0 +1,66 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + str_rewriter.cpp + +Abstract: + + AST rewriting rules for string terms. + +Author: + + Murphy Berzish + +Notes: + +--*/ + +#include"str_rewriter.h" +#include"arith_decl_plugin.h" +#include"ast_pp.h" +#include"ast_util.h" +#include"well_sorted.h" + +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;); + + switch(f->get_decl_kind()) { + default: + return BR_FAILED; + } +} + +br_status str_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { + // from seq_rewriter + expr_ref_vector lhs(m()), rhs(m()), res(m()); + bool changed = false; + if (!reduce_eq(l, r, lhs, rhs, changed)) { + result = m().mk_false(); + return BR_DONE; + } + if (!changed) { + return BR_FAILED; + } + for (unsigned i = 0; i < lhs.size(); ++i) { + res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get())); + } + result = mk_and(res); + return BR_REWRITE3; +} + +bool str_rewriter::reduce_eq(expr * l, expr * r, expr_ref_vector & lhs, expr_ref_vector & rhs, bool & change) { + // TODO inspect seq_rewriter::reduce_eq() + change = false; + return true; +} + +bool str_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) { + // TODO inspect seq_rewriter::reduce_eq() + change = false; + return true; +} + diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h new file mode 100644 index 000000000..fde36e92e --- /dev/null +++ b/src/ast/rewriter/str_rewriter.h @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + str_rewriter.h + +Abstract: + + AST rewriting rules for string terms. + +Author: + + Murphy Berzish + +Notes: + +--*/ + +#include"str_decl_plugin.h" +#include"arith_decl_plugin.h" +#include"rewriter_types.h" +#include"params.h" + +class str_rewriter { + str_util m_strutil; + arith_util m_autil; + +public: + str_rewriter(ast_manager & m, params_ref const & p = params_ref()) : + m_strutil(m), m_autil(m) { + } + + ast_manager & m() const { return m_strutil.get_manager(); } + family_id get_fid() const { return m_strutil.get_family_id(); } + + void updt_params(params_ref const & p) {} + static void get_param_descrs(param_descrs & r) {} + + 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); + + 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/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 6f6daf8df..a56ca91d8 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -27,6 +27,7 @@ Notes: #include"dl_rewriter.h" #include"pb_rewriter.h" #include"seq_rewriter.h" +#include"str_rewriter.h" #include"rewriter_def.h" #include"expr_substitution.h" #include"ast_smt2_pp.h" @@ -45,6 +46,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { dl_rewriter m_dl_rw; pb_rewriter m_pb_rw; seq_rewriter m_seq_rw; + str_rewriter m_str_rw; arith_util m_a_util; bv_util m_bv_util; unsigned long long m_max_memory; // in bytes @@ -79,6 +81,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_ar_rw.updt_params(p); m_f_rw.updt_params(p); m_seq_rw.updt_params(p); + m_str_rw.updt_params(p); updt_local_params(p); } @@ -179,6 +182,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_ar_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); + else if (s_fid == m_str_rw.get_fid()) + st = m_str_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; @@ -207,6 +212,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return m_pb_rw.mk_app_core(f, num, args, result); if (fid == m_seq_rw.get_fid()) return m_seq_rw.mk_app_core(f, num, args, result); + if (fid == m_str_rw.get_fid()) + return m_str_rw.mk_app_core(f, num, args, result); return BR_FAILED; } @@ -665,6 +672,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_dl_rw(m), m_pb_rw(m), m_seq_rw(m), + m_str_rw(m), m_a_util(m), m_bv_util(m), m_used_dependencies(m),