From 66e61b8a31a04a858af570e0665fcdd61fc0c2d2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 Apr 2017 03:03:59 -0700
Subject: [PATCH] issues #963 #912

---
 src/ast/rewriter/seq_rewriter.cpp | 31 ++++++++++++++++++++++-
 src/smt/theory_seq.cpp            | 41 +++++++++++++++++++++++++------
 src/smt/theory_seq.h              |  1 +
 3 files changed, 64 insertions(+), 9 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index b4dbfa6df..3737f4651 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -60,7 +60,12 @@ expr_ref sym_expr::accept(expr* e) {
 }
 
 std::ostream& sym_expr::display(std::ostream& out) const {
-    return out << m_t;
+    switch (m_ty) {
+    case t_char: return out << m_t;
+    case t_range: return out << m_t << ":" << m_s;
+    case t_pred: return out << m_t;
+    }
+    return out << "expression type not recognized";
 }
 
 struct display_expr1 {
@@ -237,6 +242,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
             unsigned nb = s1.num_bits();
             expr_ref _start(bv.mk_numeral(start, nb), m);
             expr_ref _stop(bv.mk_numeral(stop, nb), m);
+            TRACE("seq", tout << "Range: " << start << " " << stop << "\n";);
             a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
             return a.detach();
         }
@@ -646,6 +652,29 @@ 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) {
+        if (as.size() < bs.size()) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        expr_ref_vector ors(m());
+        for (unsigned i = 0; i < as.size() - bs.size() + 1; ++i) {
+            expr_ref_vector ands(m());
+            for (unsigned j = 0; j < bs.size(); ++j) {
+                ands.push_back(m().mk_eq(as[i + j].get(), bs[j].get()));
+            }
+            ors.push_back(::mk_and(ands));
+        }
+        result = ::mk_or(ors);
+        return BR_REWRITE_FULL;
+    }
 
     return BR_FAILED;
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 672d3c440..9dd082de0 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -255,6 +255,11 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>solve_eqs\n";);
         return FC_CONTINUE;
     }
+    if (check_contains()) {
+        ++m_stats.m_propagate_contains;
+        TRACE("seq", tout << ">>propagate_contains\n";);
+        return FC_CONTINUE;
+    }
     if (solve_nqs(0)) {
         ++m_stats.m_solve_nqs;
         TRACE("seq", tout << ">>solve_nqs\n";);
@@ -290,11 +295,6 @@ final_check_status theory_seq::final_check_eh() {
         TRACE("seq", tout << ">>propagate_automata\n";);
         return FC_CONTINUE;
     }
-    if (check_contains()) {
-        ++m_stats.m_propagate_contains;
-        TRACE("seq", tout << ">>propagate_contains\n";);
-        return FC_CONTINUE;
-    }
     if (is_solved()) {
         TRACE("seq", tout << ">>is_solved\n";);
         return FC_DONE;
@@ -1159,7 +1159,7 @@ bool theory_seq::check_extensionality() {
 }
 
 /*
-  \brief check negated contains constriants.
+  \brief check negated contains constraints.
  */
 bool theory_seq::check_contains() {
     context & ctx = get_context();
@@ -1199,6 +1199,11 @@ bool theory_seq::is_solved() {
         IF_VERBOSE(10, display_disequation(verbose_stream() << "(seq.giveup ", m_nqs[0]); verbose_stream() << " is unsolved)\n";);
         return false;
     }
+    if (!m_ncs.empty()) {
+        TRACE("seq", display_nc(tout << "(seq.giveup ", m_ncs[0]); tout << " is unsolved)\n";);
+        IF_VERBOSE(10, display_nc(verbose_stream() << "(seq.giveup ", m_ncs[0]); verbose_stream() << " is unsolved)\n";);
+        return false;
+    }
 
     return true;
 }
@@ -1984,6 +1989,22 @@ bool theory_seq::solve_nc(unsigned idx) {
         m_new_propagation = true;
         return true;
     }
+
+    expr* e1, *e2;
+    if (m.is_eq(c, e1, e2)) {
+        literal eq = mk_eq(e1, e2, false);
+        propagate_lit(deps, 0, 0, ~eq);
+        return true;
+    }
+
+    if (m.is_or(c)) {
+        for (unsigned i = 0; i < to_app(c)->get_num_args(); ++i) {
+            expr_ref ci(to_app(c)->get_arg(i), m);
+            m_ncs.push_back(nc(ci, deps));
+        }
+        m_new_propagation = true;
+        return true;
+    }
     return false;
 }
 
@@ -2418,13 +2439,17 @@ void theory_seq::display(std::ostream & out) const {
     if (!m_ncs.empty()) {
         out << "Non contains:\n";
         for (unsigned i = 0; i < m_ncs.size(); ++i) {
-            out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n";
-            display_deps(out << "  <- ", m_ncs[i].deps()); out << "\n";
+            display_nc(out, m_ncs[i]);
         }
     }
 
 }
 
+void theory_seq::display_nc(std::ostream& out, nc const& nc) const {
+    out << "not " << mk_pp(nc.contains(), m) << "\n";
+    display_deps(out << "  <- ", nc.deps()); out << "\n";
+}
+
 void theory_seq::display_equations(std::ostream& out) const {
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
         display_equation(out, m_eqs[i]);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index aa7ddec1b..2b8fb2fd7 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -570,6 +570,7 @@ namespace smt {
         void display_disequation(std::ostream& out, ne const& e) const;
         void display_deps(std::ostream& out, dependency* deps) const;
         void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
+        void display_nc(std::ostream& out, nc const& nc) const;
     public:
         theory_seq(ast_manager& m);
         virtual ~theory_seq();