mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fixed bug in is_char_const_range (#5724)

Browse source
This commit is contained in:
Margus Veanes 2021-12-19 17:46:42 -08:00 committed by GitHub
parent 25d54ebb40
commit be38b256c8
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4956,8 +4956,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
expr_ref_vector conds_range(m()); expr_ref_vector conds_range(m());
flatten_and(cond, conds); flatten_and(cond, conds);
expr* lhs = nullptr, *rhs = nullptr, *e1 = nullptr; expr* lhs = nullptr, *rhs = nullptr, *e1 = nullptr;
bool all_ranges = true; bool all_ranges = false;
if (u().is_char(elem)) { if (u().is_char(elem)) {
all_ranges = true;
unsigned ch = 0, ch2 = 0; unsigned ch = 0, ch2 = 0;
svector<std::pair<unsigned, unsigned>> ranges, ranges1; svector<std::pair<unsigned, unsigned>> ranges, ranges1;
ranges.push_back(std::make_pair(0, u().max_char())); ranges.push_back(std::make_pair(0, u().max_char()));
@ -5057,8 +5058,10 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
if (conds.empty()) if (conds.empty())
// all ranges were removed as trivially true // all ranges were removed as trivially true
cond = m().mk_true(); cond = m().mk_true();
else if (conds.size() == 1)
cond = conds.get(0);
else else
cond = m().mk_and(conds_range); cond = m().mk_and(conds);
} }
} }

8
src/ast/seq_decl_plugin.cpp
View file

@ -832,7 +832,7 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const {
} }
bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const { bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned& u, bool& negated) const {
expr* a, * b, * e1, * e2, * lb, * ub; expr* a, * b, * e0, * e1, * e2, * lb, * ub;
e1 = e; e1 = e;
negated = (m.is_not(e, e1)) ? true : false; negated = (m.is_not(e, e1)) ? true : false;
if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) { if (m.is_eq(e1, a, b) && (a == x && is_const_char(b, l))) {
@ -849,7 +849,7 @@ bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned
u = max_char(); u = max_char();
return true; return true;
} }
if (m.is_and(e1, e1, e2) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && if (m.is_and(e1, e0, e2) && is_char_le(e0, lb, a) && a == x && is_const_char(lb, l) &&
is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) is_char_le(e2, b, ub) && b == x && is_const_char(ub, u))
// (l <= x) & (x <= u) // (l <= x) & (x <= u)
return true; return true;
@ -857,8 +857,8 @@ bool seq_util::is_char_const_range(expr const* x, expr* e, unsigned& l, unsigned
u = l; u = l;
return true; return true;
} }
if (m.is_and(e1, e2, e1) && is_char_le(e1, lb, a) && a == x && is_const_char(lb, l) && if (m.is_and(e1, e0, e2) && is_char_le(e0, a, ub) && a == x && is_const_char(ub, u) &&
is_char_le(e2, b, ub) && b == x && is_const_char(ub, u)) is_char_le(e2, lb, b) && b == x && is_const_char(lb, l))
// (x <= u) & (l <= x) // (x <= u) & (l <= x)
return true; return true;
return false; return false;