mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-28 20:05:32 -07:00
parent ea1f50b77e
commit 0911a06d81
2 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2345,7 +2345,7 @@ bool seq_rewriter::non_overlap(zstring const& s1, zstring const& s2) const {
for (unsigned j = 0; j + sz1 < sz2; ++j) for (unsigned j = 0; j + sz1 < sz2; ++j)
if (can_overlap(0, sz1, j)) if (can_overlap(0, sz1, j))
return false; return false;
for (unsigned j = sz2-sz1+1; j < sz2; ++j) for (unsigned j = sz2 - sz1; j < sz2; ++j)
if (can_overlap(0, sz2 - j, j)) if (can_overlap(0, sz2 - j, j))
return false; return false;
return true; return true;
@ -2381,24 +2381,24 @@ bool seq_rewriter::non_overlap(expr_ref_vector const& p1, expr_ref_vector const&
for (unsigned j = 0; j + sz1 < sz2; ++j) for (unsigned j = 0; j + sz1 < sz2; ++j)
if (can_overlap(0, sz1, j)) if (can_overlap(0, sz1, j))
return false; return false;
for (unsigned j = sz2-sz1+1; j < sz2; ++j) for (unsigned j = sz2 - sz1; j < sz2; ++j)
if (can_overlap(0, sz2 - j, j)) if (can_overlap(0, sz2 - j, j))
return false; return false;
return true; return true;
} }
bool seq_rewriter::rewrite_contains(expr* a, expr* b, expr_ref& result) { /**
simplify extended contains patterns into simpler membership constraints
(x ++ "abc" ++ s) in (all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all)
=>
("abc" ++ s) in (all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all)
or x in (all ++ "de" ++ all) & ("abc" ++ s) in (all ++ "ee" ++ all ++ "ff" ++ all)
or x in (all ++ "de" ++ all ++ "ee" ++ all) & ("abc" ++ s) in (all ++ "ff" ++ all)
or x in (all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all) & .. simplifies to true ..
*/
bool seq_rewriter::rewrite_contains_pattern(expr* a, expr* b, expr_ref& result) {
//
// simplify extended contains patterns into simpler membership constraints
//
// x ++ "abc" ++ s in all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all
// =>
// "abc" ++ s in (all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all)
// or x in all ++ "de" ++ all & "abc" ++ s in (all ++ "ee" ++ all ++ "ff" ++ all)
// or x in (all ++ "de" ++ all ++ "ee" ++ all) & "abc" ++ s in (all ++ "ff" ++ all)
// or x in (all ++ "de" ++ all ++ "ee" ++ all ++ "ff" ++ all) & .. simplifies to true ..
//
vector<expr_ref_vector> patterns; vector<expr_ref_vector> patterns;
expr* x = nullptr, *y = nullptr, *z = nullptr, *u = nullptr; expr* x = nullptr, *y = nullptr, *z = nullptr, *u = nullptr;
@ -2470,7 +2470,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
} }
} }
if (rewrite_contains(a, b, result)) if (rewrite_contains_pattern(a, b, result))
return BR_REWRITE_FULL; return BR_REWRITE_FULL;
return BR_FAILED; return BR_FAILED;

2
src/ast/rewriter/seq_rewriter.h
View file

@ -183,7 +183,7 @@ class seq_rewriter {
bool is_re_contains_pattern(expr* r, vector<expr_ref_vector>& patterns); bool is_re_contains_pattern(expr* r, vector<expr_ref_vector>& patterns);
bool non_overlap(expr_ref_vector const& p1, expr_ref_vector const& p2) const; bool non_overlap(expr_ref_vector const& p1, expr_ref_vector const& p2) const;
bool non_overlap(zstring const& p1, zstring const& p2) const; bool non_overlap(zstring const& p1, zstring const& p2) const;
bool rewrite_contains(expr* a, expr* b, expr_ref& result); bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result); br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);