rev const split

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f283ab1e769f1a759070ec5a15339f215be08b74..d41359a882adf96c8e0f68ba419b297aad8874bf 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -995,7 +995,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                do
                                {
                                        //---------------------do simple stuff first
-                                       if( processSimpleNeq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j ) ){
+                                       if( processSimpleNeq( normal_forms, normal_form_src, curr_exp, i, j, index_i, index_j, false ) ){
                                                //added a lemma, return
                                                return true;
                                        }
@@ -1060,43 +1060,21 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                                                                        unsigned nconst_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_j : index_i;
                                                                        Node const_str = normal_forms[const_k][const_index_k];
                                                                        Node other_str = normal_forms[nconst_k][nconst_index_k];
-                                                                       if( other_str.getKind() == kind::CONST_STRING ) {
-                                                                               unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
-                                                                               if( const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short) ) {
-                                                                                       //same prefix
-                                                                                       //k is the index of the string that is shorter
-                                                                                       int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
-                                                                                       int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
-                                                                                       int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
-                                                                                       int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
-                                                                                       Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(len_short) );
-                                                                                       Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
-                                                                                       normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
-                                                                                       normal_forms[l][index_l] = normal_forms[k][index_k];
-                                                                                       success = true;
-                                                                               } else {
-                                                                                       //curr_exp is conflict
-                                                                                       antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                                                       Node ant = mkExplain( antec );
-                                                                                       sendLemma( ant, conc, "Conflict" );
-                                                                                       return true;
-                                                                               }
-                                                                       } else {
-                                                                               Assert( other_str.getKind()!=kind::STRING_CONCAT );
-                                                                               antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
-                                                                               Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
-                                                                                       NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-                                                                               //split the string
-                                                                               Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
-                                                                               Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
-                                                                               d_pending_req_phase[ eq1 ] = true;
-                                                                               conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
-                                                                               Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
-
-                                                                               Node ant = mkExplain( antec );
-                                                                               sendLemma( ant, conc, "CST-SPLIT" );
-                                                                               return true;
-                                                                       }
+                                                                       Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." );
+                                                                       Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
+                                                                       antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+                                                                       Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
+                                                                               NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
+                                                                       //split the string
+                                                                       Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) );
+                                                                       Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false );
+                                                                       d_pending_req_phase[ eq1 ] = true;
+                                                                       conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 );
+                                                                       Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl;
+
+                                                                       Node ant = mkExplain( antec );
+                                                                       sendLemma( ant, conc, "CST-SPLIT" );
+                                                                       return true;
                                                                } else {
                                                                        std::vector< Node > antec_new_lits;
                                                                        antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
@@ -1162,7 +1140,7 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
        t_curr_exp.insert( t_curr_exp.begin(), curr_exp.begin(), curr_exp.end() );
        unsigned index_i = 0;
        unsigned index_j = 0;
-       bool ret = processSimpleNeq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j );
+       bool ret = processSimpleNeq( normal_forms, normal_form_src, t_curr_exp, i, j, index_i, index_j, true );
 
        //reverse normal form of i, j
        std::reverse( normal_forms[i].begin(), normal_forms[i].end() );
@@ -1173,7 +1151,7 @@ bool TheoryStrings::processReverseNEq( std::vector< std::vector< Node > > &norma
 
 bool TheoryStrings::processSimpleNeq( std::vector< std::vector< Node > > &normal_forms,
                                                                          std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp,
-                                                                         unsigned i, unsigned j, unsigned& index_i, unsigned& index_j ) {
+                                                                         unsigned i, unsigned j, unsigned& index_i, unsigned& index_j, bool isRev ) {
        bool success;
        do {
                success = false;
@@ -1250,6 +1228,42 @@ bool TheoryStrings::processSimpleNeq( std::vector< std::vector< Node > > &normal
                                                index_i = normal_forms[i].size();
                                                index_j = normal_forms[j].size();
                                        }
+                               } else if(normal_forms[i][index_i].isConst() && normal_forms[j][index_j].isConst()) {
+                                       Node const_str = normal_forms[i][index_i];
+                                       Node other_str = normal_forms[j][index_j];
+                                       Trace("strings-solve-debug") << "Simple Case 3 : Const Split : " << const_str << " vs " << other_str << std::endl;
+                                       unsigned len_short = const_str.getConst<String>().size() <= other_str.getConst<String>().size() ? const_str.getConst<String>().size() : other_str.getConst<String>().size();
+                                       bool isSameFix = isRev ? const_str.getConst<String>().rstrncmp(other_str.getConst<String>(), len_short): const_str.getConst<String>().strncmp(other_str.getConst<String>(), len_short);
+                                       if( isSameFix ) {
+                                               //same prefix/suffix
+                                               //k is the index of the string that is shorter
+                                               int k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? i : j;
+                                               int index_k = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_i : index_j;
+                                               int l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? j : i;
+                                               int index_l = const_str.getConst<String>().size()<other_str.getConst<String>().size() ? index_j : index_i;
+                                               if(isRev) {
+                                                       int new_len = normal_forms[l][index_l].getConst<String>().size() - len_short;
+                                                       Node remainderStr = NodeManager::currentNM()->mkConst( normal_forms[l][index_l].getConst<String>().substr(0, new_len) );
+                                                       Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+                                                       normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
+                                               } else {
+                                                       Node remainderStr = NodeManager::currentNM()->mkConst(normal_forms[l][index_l].getConst<String>().substr(len_short));
+                                                       Trace("strings-solve-debug-test") << "Break normal form of " << normal_forms[l][index_l] << " into " << normal_forms[k][index_k] << ", " << remainderStr << std::endl;
+                                                       normal_forms[l].insert( normal_forms[l].begin()+index_l + 1, remainderStr );
+                                               }
+                                               normal_forms[l][index_l] = normal_forms[k][index_k];
+                                               index_i++;
+                                               index_j++;
+                                               success = true;
+                                       } else {
+                                               Node conc;
+                                               std::vector< Node > antec;
+                                               //curr_exp is conflict
+                                               antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() );
+                                               Node ant = mkExplain( antec );
+                                               sendLemma( ant, conc, "Const Conflict" );
+                                               return true;
+                                       }
                                }
                        }
                }

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 3d9d1641f90b3bbb188d6fe1599bc5c36a3fb15b..e7f8751577d7643b82c3dc15cf6aa4dd1fb23ba2 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -213,7 +213,7 @@ private:
                                                   std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j );
        bool processSimpleNeq( std::vector< std::vector< Node > > &normal_forms,
                                                   std::vector< Node > &normal_form_src, std::vector< Node > &curr_exp, unsigned i, unsigned j,
-                                                  unsigned& index_i, unsigned& index_j );
+                                                  unsigned& index_i, unsigned& index_j, bool isRev );
     bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp );
     bool normalizeDisequality( Node n1, Node n2 );
        bool unrollStar( Node atom );

diff --git a/src/util/regexp.h b/src/util/regexp.h
index f6c5b2b0fac0a26635b0c31f8fa133bc1cb5b922..82b83831538175796b4b6dd87dff0c6bc44a7c2d 100644 (file)
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -130,6 +130,11 @@ public:
       return true;
   }
 
+  bool rstrncmp(const String &y, unsigned int n) const {
+      for(unsigned int i=0; i<n; ++i)
+          if(d_str[d_str.size() - i - 1] != y.d_str[y.d_str.size() - i - 1]) return false;
+      return true;
+  }
 
   bool isEmptyString() const {
          return ( d_str.size() == 0 );