From d5ee7e24bcd5bab2bae7d898877b2fc490a9e396 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Jul 2016 11:50:39 -0700
Subject: [PATCH] add simplification for equalities between itos and constant
strings, Issue #589
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/rewriter/seq_rewriter.cpp | 55 +++++++++++++++++++++++++++++++
src/ast/rewriter/seq_rewriter.h | 5 +++
src/ast/seq_decl_plugin.cpp | 10 ------
src/ast/seq_decl_plugin.h | 1 -
4 files changed, 60 insertions(+), 11 deletions(-)
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 29bfe25e5..3a447d0f5 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1515,6 +1515,11 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
unsigned szl = ls.size() - head1, szr = rs.size() - head2;
expr* const* _ls = ls.c_ptr() + head1, * const* _rs = rs.c_ptr() + head2;
+ if (solve_itos(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
+ ls.reset(); rs.reset();
+ change = true;
+ return is_sat;
+ }
if (length_constrained(szl, _ls, szr, _rs, lhs, rhs, is_sat)) {
ls.reset(); rs.reset();
@@ -1679,6 +1684,56 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) {
return bounded;
}
+bool seq_rewriter::is_string(unsigned n, expr* const* es, zstring& s) const {
+ zstring s1;
+ expr* e;
+ bv_util bv(m());
+ rational val;
+ unsigned sz;
+ for (unsigned i = 0; i < n; ++i) {
+ if (m_util.str.is_string(es[i], s1)) {
+ s = s + s1;
+ }
+ else if (m_util.str.is_unit(es[i], e) && bv.is_numeral(e, val, sz)) {
+ s = s + zstring(val.get_unsigned());
+ }
+ else {
+ return false;
+ }
+ }
+ return true;
+}
+
+bool seq_rewriter::solve_itos(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs,
+ expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
+
+ expr* l, *r;
+ if (szl == 1 && m_util.str.is_itos(ls[0], l)) {
+ if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
+ lhs.push_back(l);
+ rhs.push_back(r);
+ is_sat = true;
+ return true;
+ }
+ zstring s;
+ if (is_string(szr, rs, s)) {
+ std::string s1 = s.encode();
+ rational r(s1.c_str());
+ if (s1 == r.to_string()) {
+ lhs.push_back(l);
+ rhs.push_back(m_autil.mk_numeral(r, true));
+ return true;
+ }
+ }
+ }
+
+ if (szr == 1 && m_util.str.is_itos(rs[0], r)) {
+ return solve_itos(szr, rs, szl, ls, rhs, lhs, is_sat);
+ }
+
+ return false;
+}
+
bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
is_sat = true;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 040bae1b4..82579d53a 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -125,15 +125,20 @@ class seq_rewriter {
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
+ bool solve_itos(unsigned n, expr* const* l, unsigned m, expr* const* r,
+ expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool min_length(unsigned n, expr* const* es, unsigned& len);
expr* concat_non_empty(unsigned n, expr* const* es);
+ bool is_string(unsigned n, expr* const* es, zstring& s) const;
+
void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
bool is_epsilon(expr* e) const;
void split_units(expr_ref_vector& lhs, expr_ref_vector& rhs);
+
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_re2aut(m), m_es(m), m_lhs(m), m_rhs(m) {
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 21af0773a..dc7307741 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -822,16 +822,6 @@ app* seq_util::str::mk_char(char ch) {
return mk_char(s, 0);
}
-bool seq_util::str::is_char(expr* n, zstring& c) const {
- if (u.is_char(n)) {
- c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
- return true;
- }
- else {
- return false;
- }
-}
-
bool seq_util::str::is_string(expr const* n, zstring& s) const {
if (is_string(n)) {
s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str());
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 78672182a..fbbcba5de 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -250,7 +250,6 @@ public:
}
bool is_string(expr const* n, zstring& s) const;
- bool is_char(expr* n, zstring& s) const;
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);