mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fix model validation for theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-08-07 15:43:08 -04:00
parent 395ec4543c
commit cb566ad5ce
3 changed files with 25 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/rewriter/str_rewriter.cpp
View file

@ -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);

1
src/ast/rewriter/str_rewriter.h
View file

@ -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);

7
src/model/model_evaluator.cpp
View file

@ -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;