mirror of
https://github.com/Z3Prover/z3
synced 2025-07-17 09:56:39 +00:00
parent
43a19cadf6
commit
e593b5b2c8
3 changed files with 12 additions and 9 deletions
|
@ -699,9 +699,11 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
||||||
if (lengthPos) {
|
if (lengthPos) {
|
||||||
|
|
||||||
m_lhs.reset();
|
m_lhs.reset();
|
||||||
expr_ref_vector lens(m()), other(m());
|
expr_ref_vector lens(m());
|
||||||
m_util.str.get_concat(a, m_lhs);
|
m_util.str.get_concat(a, m_lhs);
|
||||||
get_lengths(b, lens, other, pos);
|
if (!get_lengths(b, lens, pos)) {
|
||||||
|
return BR_FAILED;
|
||||||
|
}
|
||||||
unsigned rsz = lens.size();
|
unsigned rsz = lens.size();
|
||||||
unsigned i = 0;
|
unsigned i = 0;
|
||||||
for (; i < m_lhs.size(); ++i) {
|
for (; i < m_lhs.size(); ++i) {
|
||||||
|
@ -728,9 +730,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
||||||
for (expr* rhs : lens) {
|
for (expr* rhs : lens) {
|
||||||
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
|
t2 = m_autil.mk_add(t2, m_util.str.mk_length(rhs));
|
||||||
}
|
}
|
||||||
for (expr* rhs : other) {
|
|
||||||
t2 = m_autil.mk_add(t2, rhs);
|
|
||||||
}
|
|
||||||
result = m_util.str.mk_substr(t1, t2, c);
|
result = m_util.str.mk_substr(t1, t2, c);
|
||||||
return BR_REWRITE2;
|
return BR_REWRITE2;
|
||||||
}
|
}
|
||||||
|
@ -782,12 +781,12 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
||||||
return BR_REWRITE3;
|
return BR_REWRITE3;
|
||||||
}
|
}
|
||||||
|
|
||||||
void seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector& other, rational& pos) {
|
bool seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, rational& pos) {
|
||||||
expr* arg = nullptr;
|
expr* arg = nullptr;
|
||||||
rational pos1;
|
rational pos1;
|
||||||
if (m_autil.is_add(e)) {
|
if (m_autil.is_add(e)) {
|
||||||
for (expr* arg1 : *to_app(e)) {
|
for (expr* arg1 : *to_app(e)) {
|
||||||
get_lengths(arg1, lens, other, pos);
|
if (!get_lengths(arg1, lens, pos)) return false;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
else if (m_util.str.is_length(e, arg)) {
|
else if (m_util.str.is_length(e, arg)) {
|
||||||
|
@ -797,8 +796,9 @@ void seq_rewriter::get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector&
|
||||||
pos += pos1;
|
pos += pos1;
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
other.push_back(e);
|
return false;
|
||||||
}
|
}
|
||||||
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
|
bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
|
||||||
|
|
|
@ -155,7 +155,7 @@ class seq_rewriter {
|
||||||
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
|
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
|
||||||
bool is_epsilon(expr* e) const;
|
bool is_epsilon(expr* e) const;
|
||||||
void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
|
void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
|
||||||
void get_lengths(expr* e, expr_ref_vector& lens, expr_ref_vector& other, rational& pos);
|
bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
|
||||||
|
|
||||||
|
|
||||||
public:
|
public:
|
||||||
|
|
|
@ -4746,6 +4746,9 @@ void theory_seq::add_itos_length_axiom(expr* len) {
|
||||||
literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
|
literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
|
||||||
|
|
||||||
add_axiom(~n_ge_10hi, len_ge);
|
add_axiom(~n_ge_10hi, len_ge);
|
||||||
|
add_axiom(n_ge_10hi, ~len_ge);
|
||||||
|
|
||||||
|
add_axiom(n_ge_100hi, len_le);
|
||||||
add_axiom(~n_ge_100hi, ~len_le);
|
add_axiom(~n_ge_100hi, ~len_le);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue