mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 22:05:36 +00:00
Code Activity

fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-25 17:21:01 -04:00
parent 8c95dff33b
commit 4d8e4b5bd3
2 changed files with 27 additions and 20 deletions

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

@ -5607,7 +5607,7 @@ expr* seq_rewriter::concat_non_empty(expr_ref_vector& es) {
sort* s = es[0]->get_sort();
unsigned j = 0;
for (expr* e : es) {
if (str().is_unit(e) || str().is_string(e))
if (str().is_unit(e) || str().is_string(e) || m().is_ite(e))
es[j++] = e;
}
es.shrink(j);
@ -5623,23 +5623,16 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pa
zstring s;
expr* emp = nullptr;
for (unsigned i = 0; i < sz; ++i) {
if (str().is_unit(es[i])) {
if (all) return false;
}
else if (str().is_empty(es[i])) {
auto [bounded, len] = min_length(es[i]);
if (len > 0) {
if (all)
return false;
continue;
}
else if (str().is_string(es[i], s)) {
if (s.length() == 0)
continue;
if (all) {
return false;
}
}
else {
emp = emp?emp:str().mk_empty(es[i]->get_sort());
eqs.push_back(emp, es[i]);
}
if (bounded && len == 0)
continue;
emp = emp?emp:str().mk_empty(es[i]->get_sort());
eqs.push_back(emp, es[i]);
}
return true;
}
@ -5669,6 +5662,9 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
zstring s;
unsigned len = 0;
bool bounded = true;
if (sz == 0)
return { bounded, len };
expr* c, *th, *el;
auto visit = [&](expr* e) {
if (cache.contains(e))
@ -5703,13 +5699,13 @@ std::pair<bool, unsigned> seq_rewriter::min_length(unsigned sz, expr* const* ss)
return visited;
}
else if (m().is_ite(e, c, th, el)) {
unsigned sz = sub.size();
unsigned subsz = sub.size();
std::pair<bool, unsigned> r1, r2;
if (!cache.find(th, r1))
sub.push_back(th);
if (!cache.find(el, r2))
sub.push_back(el);
if (sz != sub.size())
if (subsz != sub.size())
return false;
cache.insert(e, { r1.first && r2.first && r1.second == r2.second, std::min(r1.second, r2.second)});
@ -5884,6 +5880,16 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
return false;
}
bool seq_rewriter::has_var(expr_ref_vector const& es) {
for (expr* e : es) {
auto [bounded, len] = min_length(e);
if (len == 0)
return true;
}
return false;
}
bool seq_rewriter::reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs,
expr_ref_pair_vector& eqs) {
@ -5896,14 +5902,14 @@ bool seq_rewriter::reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs,
return false;
if (bounded2 && len2 < len1)
return false;
if (bounded1 && len1 == len2 && len1 > 0) {
if (bounded1 && len1 == len2 && len1 > 0 && has_var(rs)) {
if (!set_empty(rs.size(), rs.data(), false, eqs))
return false;
eqs.push_back(concat_non_empty(ls), concat_non_empty(rs));
ls.reset();
rs.reset();
}
else if (bounded2 && len1 == len2 && len1 > 0) {
else if (bounded2 && len1 == len2 && len1 > 0 && has_var(ls)) {
if (!set_empty(ls.size(), ls.data(), false, eqs))
return false;
eqs.push_back(concat_non_empty(ls), concat_non_empty(rs));

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

@ -322,6 +322,7 @@ class seq_rewriter {
bool reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
bool reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
bool reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
bool has_var(expr_ref_vector const& es);
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);
std::pair<bool, unsigned> min_length(expr_ref_vector const& es);