mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

address bug reported in #1196 and include additional ad-hoc rewrites to handle some string cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-12 17:41:18 -07:00
parent f99048f3e7
commit 85cdfd885f
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/rewriter/seq_rewriter.cpp
View file

@ -608,6 +608,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
m_util.str.get_concat(a, as); m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs); m_util.str.get_concat(b, bs);
bool all_values = true; bool all_values = true;
TRACE("seq", tout << mk_pp(a, m()) << " contains " << mk_pp(b, m()) << "\n";);
if (bs.empty()) { if (bs.empty()) {
result = m().mk_true(); result = m().mk_true();
@ -652,6 +653,15 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
return BR_REWRITE2; return BR_REWRITE2;
} }
if (bs.size() == 1 && m_util.str.is_string(bs[0].get(), c)) {
for (auto a_i : as) {
if (m_util.str.is_string(a_i, d) && d.contains(c)) {
result = m().mk_true();
return BR_DONE;
}
}
}
unsigned offs = 0; unsigned offs = 0;
unsigned sz = as.size(); unsigned sz = as.size();
expr* b0 = bs[0].get(); expr* b0 = bs[0].get();