mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c9d6dccc12
commit
9ae3339c33
|
@ -140,8 +140,10 @@ namespace seq {
|
|||
return;
|
||||
}
|
||||
if (is_extract_suffix(s, _i, _l)) {
|
||||
extract_suffix_axiom(e, i, l);
|
||||
return;
|
||||
}
|
||||
TRACE("seq", tout << s << " " << i << " " << l << "\n";);
|
||||
expr_ref x = m_sk.mk_pre(s, i);
|
||||
expr_ref ls = mk_len(_s);
|
||||
expr_ref lx = mk_len(x);
|
||||
|
|
|
@ -987,7 +987,7 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
unsigned len_a;
|
||||
rational len_a;
|
||||
if (constantPos && max_length(a, len_a) && rational(len_a) <= pos) {
|
||||
result = str().mk_empty(a_sort);
|
||||
return BR_DONE;
|
||||
|
@ -1162,7 +1162,7 @@ bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
|
|||
else if (str().is_length(e, arg)) {
|
||||
lens.push_back(arg);
|
||||
}
|
||||
else if (m_autil.is_mul(e, e1, e2) && m_autil.is_numeral(e1, pos1) && str().is_length(e2, arg) && pos1 <= 10) {
|
||||
else if (m_autil.is_mul(e, e1, e2) && m_autil.is_numeral(e1, pos1) && str().is_length(e2, arg) && 0 <= pos1 && pos1 <= 10) {
|
||||
while (pos1 > 0) {
|
||||
lens.push_back(arg);
|
||||
pos1 -= rational(1);
|
||||
|
@ -4531,7 +4531,7 @@ bool seq_rewriter::min_length(expr_ref_vector const& es, unsigned& len) {
|
|||
return bounded;
|
||||
}
|
||||
|
||||
bool seq_rewriter::max_length(expr* e, unsigned& len) {
|
||||
bool seq_rewriter::max_length(expr* e, rational& len) {
|
||||
if (str().is_unit(e)) {
|
||||
len = 1;
|
||||
return true;
|
||||
|
@ -4542,15 +4542,21 @@ bool seq_rewriter::max_length(expr* e, unsigned& len) {
|
|||
}
|
||||
zstring s;
|
||||
if (str().is_string(e, s)) {
|
||||
len = s.length();
|
||||
len = rational(s.length());
|
||||
return true;
|
||||
}
|
||||
if (str().is_empty(e)) {
|
||||
len = 0;
|
||||
return true;
|
||||
}
|
||||
expr* s1 = nullptr, *i = nullptr, *l = nullptr;
|
||||
rational n;
|
||||
if (str().is_extract(e, s1, i, l) && m_autil.is_numeral(l, n) && !n.is_neg()) {
|
||||
len = n;
|
||||
return true;
|
||||
}
|
||||
if (str().is_concat(e)) {
|
||||
unsigned l = 0;
|
||||
rational l(0);
|
||||
len = 0;
|
||||
for (expr* arg : *to_app(e)) {
|
||||
if (!max_length(arg, l))
|
||||
|
|
|
@ -282,7 +282,7 @@ class seq_rewriter {
|
|||
bool reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
|
||||
bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);
|
||||
bool min_length(expr_ref_vector const& es, unsigned& len);
|
||||
bool max_length(expr* e, unsigned& len);
|
||||
bool max_length(expr* e, rational& len);
|
||||
expr* concat_non_empty(expr_ref_vector& es);
|
||||
|
||||
bool is_string(unsigned n, expr* const* es, zstring& s) const;
|
||||
|
|
|
@ -482,11 +482,6 @@ inline bool operator<=(rational const & r1, rational const & r2) {
|
|||
return !operator>(r1, r2);
|
||||
}
|
||||
|
||||
inline bool operator<=(rational const & r1, int r2) {
|
||||
return r1 <= rational(r2);
|
||||
}
|
||||
|
||||
|
||||
inline bool operator>=(rational const & r1, rational const & r2) {
|
||||
return !operator<(r1, r2);
|
||||
}
|
||||
|
@ -499,7 +494,6 @@ inline bool operator>(int a, rational const & b) {
|
|||
return rational(a) > b;
|
||||
}
|
||||
|
||||
|
||||
inline bool operator>=(rational const& a, int b) {
|
||||
return a >= rational(b);
|
||||
}
|
||||
|
@ -508,6 +502,13 @@ inline bool operator>=(int a, rational const& b) {
|
|||
return rational(a) >= b;
|
||||
}
|
||||
|
||||
inline bool operator<=(rational const& a, int b) {
|
||||
return a <= rational(b);
|
||||
}
|
||||
|
||||
inline bool operator<=(int a, rational const& b) {
|
||||
return rational(a) <= b;
|
||||
}
|
||||
|
||||
inline bool operator!=(rational const& a, int b) {
|
||||
return !(a == rational(b));
|
||||
|
|
Loading…
Reference in a new issue