From c07a63cf8e29fa4995c96409d0286341403d01f9 Mon Sep 17 00:00:00 2001
From: Thai Trinh <trinhmt@comp.nus.edu.sg>
Date: Tue, 12 Dec 2017 05:00:34 +0800
Subject: [PATCH] coalesce seq.unit into string in mk_skolem

---
 src/ast/rewriter/seq_rewriter.cpp |  2 +-
 src/smt/theory_seq.cpp            | 57 +++++++++++++++++++++++++++++++
 src/smt/theory_seq.h              |  1 +
 3 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index fa95278b4..2f9f3f9ce 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -453,7 +453,7 @@ br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) {
     if (bvu.is_bv(e) && bvu.is_numeral(e, n_val, n_size) && n_size == 8) {
         // convert to string constant
         zstring str(n_val.get_unsigned());
-        TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
+        TRACE("seq_verbose", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << str<< "\"" << std::endl;);
         result = m_util.str.mk_string(str);
         return BR_DONE;
     }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 57be6c205..6626c05ac 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4976,13 +4976,70 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
 }
 
+expr* theory_seq::coalesce_chars(expr* const& e) {
+    expr* s;
+    if (m_util.str.is_concat(e)) {
+        expr_ref_vector concats(m);
+        m_util.str.get_concat(e, concats);
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < concats.size(); ++i) {
+            expr_ref tmp(coalesce_chars(concats[i].get()), m);
+            if (m_util.str.is_empty(tmp)) continue;
+            zstring zs, a;
+            bool flag = false;
+            while (m_util.str.is_string(tmp, a)) {
+                if (flag)
+                    zs = zs + a;
+                else
+                    zs = a;
+                flag = true;
+                if (i < concats.size()-1)
+                    tmp = coalesce_chars(concats[++i].get());
+                else {
+                    ++i;
+                    break;
+                }
+            }
+            if (flag) {
+                result.push_back(m_util.str.mk_string(zs));
+                if (i < concats.size())
+                    result.push_back(tmp);
+            }
+            else
+                result.push_back(tmp);
+        }
+        SASSERT(result.size() > 0);
+        if (result.size() > 1)
+            return m_util.str.mk_concat(result.size(), result.c_ptr());
+        else 
+            return e;
+    }
+    else if (m_util.str.is_unit(e, s)) {
+        bv_util bvu(m);
+        if (bvu.is_bv(s)) {
+            expr_ref result(m);
+            expr * args[1] = {s};
+            if (m_seq_rewrite.mk_app_core(to_app(s)->get_decl(), 1, args, result)) {
+                return result;
+            }
+        }
+    }
+    return e;
+}
 
 expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, expr*e4, sort* range) {
     expr* es[4] = { e1, e2, e3, e4 };
     unsigned len = e4?4:(e3?3:(e2?2:1));
+
     if (!range) {
         range = m.get_sort(e1);
     }
+    if (name == symbol("seq.align")) {
+        for (unsigned i = 0; i < len; ++i) {
+      	    es[i] = coalesce_chars(es[i]);
+      	    TRACE("seq", tout << mk_pp(es[i], m) << "\n";);
+        }
+    }
     return expr_ref(m_util.mk_skolem(name, len, es, range), m);
 }
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 9424ed227..08eb205d6 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -565,6 +565,7 @@ namespace smt {
         bool get_length(expr* s, rational& val) const;
 
         void mk_decompose(expr* e, expr_ref& head, expr_ref& tail);
+        expr* coalesce_chars(expr* const& str);
         expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, expr* e4 = 0, sort* range = 0);
         bool is_skolem(symbol const& s, expr* e) const;