mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

Add rewrite rule for property encoded in #812

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-11 11:05:12 +01:00
parent 2307a7ffa7
commit 7cc093eee0
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -524,7 +524,7 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
result = m().mk_bool_val(c.contains(d)); result = m().mk_bool_val(c.contains(d));
return BR_DONE; return BR_DONE;
} }
// check if subsequence of b is in a. // check if subsequence of a is in b.
expr_ref_vector as(m()), bs(m()); expr_ref_vector as(m()), bs(m());
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);
@ -587,6 +587,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
SASSERT(sz > offs); SASSERT(sz > offs);
result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b); result = m_util.str.mk_contains(m_util.str.mk_concat(sz-offs, as.c_ptr()+offs), b);
return BR_REWRITE2; return BR_REWRITE2;
}
expr* x, *y, *z;
if (m_util.str.is_extract(b, x, y, z) && x == a) {
result = m().mk_true();
return BR_DONE;
} }
return BR_FAILED; return BR_FAILED;