From aedd13ee57e0ce12a069b7d7d059cf732458e0fd Mon Sep 17 00:00:00 2001
From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Wed, 7 May 2014 14:43:42 -0500
Subject: [PATCH] add splits

---
 src/theory/strings/theory_strings.cpp | 49 +++++++++++++++++++++++++--
 src/util/regexp.cpp                   | 10 +++---
 src/util/regexp.h                     |  2 +-
 3 files changed, 53 insertions(+), 8 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4bb0711fe..e60e67ac1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1237,7 +1237,51 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                     normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
                     CVC4::String stra = const_str.getConst<String>();
                     CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>();
-                    CVC4::String fc = strb.substr(0, 1);
+                    Node conc;
+                    Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" );
+                    if(stra == strb) {
+                      conc = other_str.eqNode( d_emptyString );
+                      CVC4::String stra1 = stra.substr(1);
+                      std::size_t p = stra1.overlap(strb);
+                      Node eq = p==0? other_str.eqNode( mkConcat(const_str, sk) )
+                                    : other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) );
+                      conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq);
+                    } else {
+                      CVC4::String fc = strb.substr(0, 1);
+                      std::size_t p;
+                      if((p=stra.find(fc)) != std::string::npos) {
+                        if( (p = stra.find(strb)) == std::string::npos ) {
+                          if((p = stra.overlap(strb)) == 0) {
+                            conc = other_str.eqNode( mkConcat(const_str, sk) );
+                          } else {
+                            conc = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) );
+                          }
+                        } else {
+                          if(p == 0) {
+                            conc = other_str.eqNode( d_emptyString );
+                            CVC4::String stra1 = stra.substr(1);
+                            if((p = stra1.find(strb)) != std::string::npos) {
+                              Node eq = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, p + 1) ), sk) );
+                              conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq);
+                            } else {
+                              p = stra1.overlap(strb);
+                              Node eq = p==0? other_str.eqNode( mkConcat(const_str, sk) )
+                                            : other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, stra.size() - p) ), sk) );
+                              conc = NodeManager::currentNM()->mkNode(kind::OR, conc, eq);
+                            }
+                          } else {
+                            conc = other_str.eqNode( mkConcat(NodeManager::currentNM()->mkConst( stra.substr(0, p - 1) ), sk) );
+                          }
+                        }
+                      } else {
+                        conc = other_str.eqNode( mkConcat(const_str, sk) );
+                      }
+                    }
+                    Node ant = mkExplain( antec );
+                    conc = Rewriter::rewrite( conc );
+                    sendLemma(ant, conc, "CST-EPS");
+                    optflag = true;
+                    /*
                     if( stra.find(fc) == std::string::npos ||
                       (stra.find(strb) == std::string::npos &&
                        !stra.overlap(strb)) ) {
@@ -1246,7 +1290,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                       Node ant = mkExplain( antec );
                       sendLemma(ant, eq, "CST-EPS");
                       optflag = true;
-                    }
+                    }*/
                   }
                   if(!optflag){
                     Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
@@ -2752,6 +2796,7 @@ bool TheoryStrings::checkPosContains() {
           sendLemma( atom, eq, "POS-INC" );
           addedLemma = true;
           d_pos_ctn_cached.insert( atom );
+          Trace("strings-ctn") << "... add lemma: " << eq << std::endl;
         } else {
           Trace("strings-ctn") << "... is already rewritten." << std::endl;
         }
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index c0e2947cb..62cf2b647 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -95,16 +95,16 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
     }
 }
 
-bool String::overlap(String &y) const {
-  unsigned n = d_str.size() < y.size() ? d_str.size() : y.size();
-  for(unsigned i=1; i<n; i++) {
+std::size_t String::overlap(String &y) const {
+  std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size();
+  for(; i>0; i--) {
     String s = suffix(i);
     String p = y.prefix(i);
     if(s == p) {
-      return true;
+      return i;
     }
   }
-  return false;
+  return i;
 }
 
 std::string String::toString() const {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index b7eea929d..effc40257 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -260,7 +260,7 @@ public:
   String suffix(unsigned i) const {
     return substr(d_str.size() - i, i);
   }
-  bool overlap(String &y) const;
+  std::size_t overlap(String &y) const;
 
   bool isNumber() const {
    if(d_str.size() == 0) return false;
-- 
2.30.2