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

fix is-unit test in seq rewriter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-21 17:08:33 -08:00
parent 0c1408b30e
commit 7b2590c026
2 changed files with 40 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -677,8 +677,22 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
}
// check if subsequence of a is in b.
expr_ref_vector as(m()), bs(m());
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
if (m_util.str.is_string(a, c)) {
for (unsigned i = 0; i < c.length(); ++i) {
as.push_back(m_util.str.mk_unit(m_util.str.mk_char(c, i)));
}
}
else {
m_util.str.get_concat(a, as);
}
if (m_util.str.is_string(b, d)) {
for (unsigned i = 0; i < d.length(); ++i) {
bs.push_back(m_util.str.mk_unit(m_util.str.mk_char(d, i)));
}
}
else {
m_util.str.get_concat(b, bs);
}
bool all_values = true;
TRACE("seq", tout << mk_pp(a, m()) << " contains " << mk_pp(b, m()) << "\n";);
@ -719,7 +733,6 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
}
}
if (as.empty()) {
result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
return BR_REWRITE2;
@ -755,14 +768,10 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
result = m().mk_true();
return BR_DONE;
}
bool all_units = true;
for (unsigned i = 0; i < bs.size(); ++i) {
all_units = m_util.str.is_unit(bs[i].get());
}
for (unsigned i = 0; i < as.size(); ++i) {
all_units = m_util.str.is_unit(as[i].get());
}
if (all_units) {
std::function<bool(expr*)> is_unit = [&](expr *e) { return m_util.str.is_unit(e); };
if (bs.forall(is_unit) && as.forall(is_unit)) {
if (as.size() < bs.size()) {
result = m().mk_false();
return BR_DONE;
@ -1595,6 +1604,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) {
return BR_REWRITE3;
}
bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change) {
expr* a, *b;
zstring s;

31
src/util/ref_vector.h
View file

@ -306,24 +306,31 @@ public:
// prevent abuse:
ref_vector & operator=(ref_vector const & other) = delete;
bool containsp(std::function<bool(T)>& predicate) const {
for (auto const& t : *this)
bool forall(std::function<bool(T*)>& predicate) const {
for (T* t : *this)
if (!predicate(t))
return false;
return true;
}
bool exists(std::function<bool(T*)>& predicate) const {
for (T* t : *this)
if (predicate(t))
return true;
return false;
}
ref_vector filter_pure(std::function<bool(T)>& predicate) const {
ref_vector filter_pure(std::function<bool(T*)>& predicate) const {
ref_vector result(m());
for (auto& t : *this)
for (T* t : *this)
if (predicate(t))
result.push_back(t);
return result;
}
#if 0
// TBD: not sure why some compilers complain here.
ref_vector& filter_update(std::function<bool(T)>& predicate) {
// TBD:
ref_vector& filter_update(std::function<bool(T*)>& predicate) {
unsigned j = 0;
for (auto& t : *this)
if (predicate(t))
@ -334,23 +341,23 @@ public:
#endif
template <typename S>
vector<S> mapv_pure(std::function<S(T)>& f) const {
vector<S> mapv_pure(std::function<S(T*)>& f) const {
vector<S> result;
for (auto& t : *this)
for (T* t : *this)
result.push_back(f(t));
return result;
}
ref_vector map_pure(std::function<T(T)>& f) const {
ref_vector map_pure(std::function<T*(T*)>& f) const {
ref_vector result(m());
for (auto& t : *this)
for (T* t : *this)
result.push_back(f(t));
return result;
}
ref_vector& map_update(std::function<T(T)>& f) {
ref_vector& map_update(std::function<T*(T*)>& f) {
unsigned j = 0;
for (auto& t : *this)
for (T* t : *this)
set(j++, f(t));
return *this;
}