add splits

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4bb0711fe292961b6443d4860a68e0e9783d2848..e60e67ac1aa51c39183f71148d2b4e931341a637 100644 (file)
--- 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 c0e2947cb0fc9eca26e665f5700b8788677df0f9..62cf2b64773013eb9334384559b66176b622d9de 100644 (file)
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -95,16 +95,16 @@ void String::getCharSet(std::set<unsigned int> &cset) const {
     }\r
 }\r
 \r
-bool String::overlap(String &y) const {\r
-  unsigned n = d_str.size() < y.size() ? d_str.size() : y.size();\r
-  for(unsigned i=1; i<n; i++) {\r
+std::size_t String::overlap(String &y) const {\r
+  std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size();\r
+  for(; i>0; i--) {\r
     String s = suffix(i);\r
     String p = y.prefix(i);\r
     if(s == p) {\r
-      return true;\r
+      return i;\r
     }\r
   }\r
-  return false;\r
+  return i;\r
 }\r
 \r
 std::string String::toString() const {\r

diff --git a/src/util/regexp.h b/src/util/regexp.h
index b7eea929d393168508baa14a9d0272fee0dae074..effc4025731dc7ee371bcc247d147297ed6d660a 100644 (file)
--- 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;