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

@@ -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;

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) {

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());

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);