From cb566ad5ced242cad991c8381322522bcddc98eb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sun, 7 Aug 2016 15:43:08 -0400 Subject: [PATCH] fix model validation for theory_str --- src/ast/rewriter/str_rewriter.cpp | 17 +++++++++++++++++ src/ast/rewriter/str_rewriter.h | 1 + src/model/model_evaluator.cpp | 7 +++++++ 3 files changed, 25 insertions(+) diff --git a/src/ast/rewriter/str_rewriter.cpp b/src/ast/rewriter/str_rewriter.cpp index 1449afcc3..37b6b6cbf 100644 --- a/src/ast/rewriter/str_rewriter.cpp +++ b/src/ast/rewriter/str_rewriter.cpp @@ -23,6 +23,20 @@ Notes: #include"ast_util.h" #include"well_sorted.h" +br_status str_rewriter::mk_str_Concat(expr * arg0, expr * arg1, expr_ref & result) { + TRACE("t_str_rw", tout << "rewrite (Concat " << mk_pp(arg0, m()) << " " << mk_pp(arg1, m()) << ")" << std::endl;); + if(m_strutil.is_string(arg0) && m_strutil.is_string(arg1)) { + TRACE("t_str_rw", tout << "evaluating Concat of two constant strings" << std::endl;); + std::string arg0Str = m_strutil.get_string_constant_value(arg0); + std::string arg1Str = m_strutil.get_string_constant_value(arg1); + std::string resultStr = arg0Str + arg1Str; + result = m_strutil.mk_string(resultStr); + return BR_DONE; + } else { + return BR_FAILED; + } +} + 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, @@ -275,6 +289,9 @@ br_status str_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con // TODO more rewrites for really easy cases, e.g. (Concat "abc" "def")... switch(f->get_decl_kind()) { + case OP_STRCAT: + SASSERT(num_args == 2); + return mk_str_Concat(args[0], args[1], result); case OP_STR_CHARAT: SASSERT(num_args == 2); return mk_str_CharAt(args[0], args[1], result); diff --git a/src/ast/rewriter/str_rewriter.h b/src/ast/rewriter/str_rewriter.h index dccf4a6bd..58e88591b 100644 --- a/src/ast/rewriter/str_rewriter.h +++ b/src/ast/rewriter/str_rewriter.h @@ -40,6 +40,7 @@ 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_Concat(expr * arg0, expr * arg1, expr_ref & result); br_status mk_str_CharAt(expr * arg0, expr * arg1, expr_ref & result); br_status mk_str_StartsWith(expr * haystack, expr * needle, expr_ref & result); br_status mk_str_EndsWith(expr * haystack, expr * needle, expr_ref & result); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index eb2259263..fd420bad6 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -28,6 +28,7 @@ Revision History: #include"datatype_rewriter.h" #include"array_rewriter.h" #include"fpa_rewriter.h" +#include"str_rewriter.h" #include"rewriter_def.h" #include"cooperate.h" #include"ast_pp.h" @@ -44,6 +45,7 @@ struct evaluator_cfg : public default_rewriter_cfg { pb_rewriter m_pb_rw; fpa_rewriter m_f_rw; seq_rewriter m_seq_rw; + str_rewriter m_str_rw; array_util m_ar; unsigned long long m_max_memory; unsigned m_max_steps; @@ -63,6 +65,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_pb_rw(m), m_f_rw(m), m_seq_rw(m), + m_str_rw(m), m_ar(m) { bool flat = true; m_b_rw.set_flat(flat); @@ -152,6 +155,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_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); else if (s_fid == m_ar_rw.get_fid()) st = mk_array_eq(args[0], args[1], result); if (st != BR_FAILED) @@ -174,6 +179,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_app_core(f, num, args, result); else if (fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_app_core(f, num, args, result); + else if (fid == m_str_rw.get_fid()) + st = m_str_rw.mk_app_core(f, num, args, result); else if (fid == m().get_label_family_id() && num == 1) { result = args[0]; st = BR_DONE;