From c4083c367a11e555e6d7665a40c658741bf2241e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Aug 2017 19:14:55 -0700
Subject: [PATCH] update handling of contains constraints taking string
 literals into account

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 43 +++++++++++++++++++++++++++++--
 src/ast/rewriter/seq_rewriter.h   |  3 +++
 2 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 581abdf1f..5f405e013 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -597,6 +597,45 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     return BR_FAILED;
 }
 
+bool seq_rewriter::cannot_contain_suffix(expr* a, expr* b) {
+    
+    if (m_util.str.is_unit(a) && m_util.str.is_unit(b) && m().are_distinct(a, b)) {
+        return true;
+    }
+    zstring A, B;
+    if (m_util.str.is_string(a, A) && m_util.str.is_string(b, B)) {
+        // some prefix of a is a suffix of b
+        bool found = false;
+        for (unsigned i = 1; !found && i <= A.length(); ++i) {
+            found = A.extract(0, i).suffixof(B);
+        }
+        return !found;
+    }
+
+    return false;
+}
+
+
+bool seq_rewriter::cannot_contain_prefix(expr* a, expr* b) {
+    
+    if (m_util.str.is_unit(a) && m_util.str.is_unit(b) && m().are_distinct(a, b)) {
+        return true;
+    }
+    zstring A, B;
+    if (m_util.str.is_string(a, A) && m_util.str.is_string(b, B)) {
+        // some suffix of a is a prefix of b
+        bool found = false;
+        for (unsigned i = 0; !found && i < A.length(); ++i) {
+            found = A.extract(i, A.length()-i).suffixof(B);
+        }
+        return !found;
+    }
+
+    return false;
+}
+
+
+
 br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     zstring c, d;
     if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
@@ -666,8 +705,8 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
     unsigned sz = as.size();
     expr* b0 = bs[0].get();
     expr* bL = bs[bs.size()-1].get();
-    for (; offs < as.size() && m_util.str.is_unit(b0) && m_util.str.is_unit(as[offs].get()) && m().are_distinct(b0, as[offs].get()); ++offs) {};
-    for (; sz > offs && m_util.str.is_unit(bL) && m_util.str.is_unit(as[sz-1].get()) && m().are_distinct(bL, as[sz-1].get()); --sz) {}
+    for (; offs < as.size() && cannot_contain_prefix(as[offs].get(), b0); ++offs) {}
+    for (; sz > offs && cannot_contain_suffix(as[sz-1].get(), bL); --sz) {}
     if (offs == sz) {
         result = m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)));
         return BR_REWRITE2;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index add941ddb..69f319168 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -122,6 +122,9 @@ class seq_rewriter {
     br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result);
     br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
 
+    bool cannot_contain_prefix(expr* a, expr* b);
+    bool cannot_contain_suffix(expr* a, expr* b);
+
     bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
     bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, 
                         expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);