Clean up explanations involving string length. Add regression.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ad1163d05147745ebcbfc72247329b4a763dc220..607552188ee24399bf98341aa0e30ef90095c358 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -172,25 +172,21 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
   }
 }
 
-Node TheoryStrings::getLengthTerm( Node t ) {
+Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ) {
+  Assert( areEqual( t, te ) );
   EqcInfo * ei = getOrMakeEqcInfo( t, false );
   Node length_term = ei ? ei->d_length_term : Node::null();
-  if( length_term.isNull()) {
+  if( length_term.isNull() ){
     //typically shouldnt be necessary
     length_term = t;
   }
-  Debug("strings") << "TheoryStrings::getLengthTerm" << t << std::endl;
-  return length_term;
+  Debug("strings") << "TheoryStrings::getLengthTerm " << t << " is " << length_term << std::endl;
+  addToExplanation( length_term, te, exp );
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, length_term ) );
 }
 
-Node TheoryStrings::getLength( Node t, bool use_t ) {
-  Node retNode;
-  if( use_t ){
-    retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t );
-  } else {
-    retNode = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, getLengthTerm( t ) );
-  }
-  return Rewriter::rewrite( retNode );
+Node TheoryStrings::getLength( Node t, std::vector< Node >& exp ) {
+  return getLengthExp( t, exp, t );
 }
 
 void TheoryStrings::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -658,7 +654,7 @@ void TheoryStrings::checkReduction( Node atom, int pol, int effort ) {
         Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
         sendLemma( atom, eq, "POS-CTN" );
       }else{
-        // for STRING_SUBSTR, 
+        // for STRING_SUBSTR,
         //     STRING_STRIDOF, STRING_ITOS, STRING_U16TOS, STRING_U32TOS, STRING_STOI, STRING_STOU16, STRING_STOU32, STRING_STRREPL
         std::vector< Node > new_nodes;
         Node res = d_preproc.decompose( atom, new_nodes );
@@ -794,6 +790,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   Trace("strings-pending") << "Assert pending fact : " << atom << " " << polarity << " from " << exp << std::endl;
   Assert(atom.getKind() != kind::OR, "Infer error: a split.");
   if( atom.getKind()==kind::EQUAL ){
+    Trace("strings-pending-debug") << "  Register term" << std::endl;
     //AJR : is this necessary?
     for( unsigned j=0; j<2; j++ ) {
       if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
@@ -801,7 +798,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
         registerTerm( atom[j] );
       }
     }
+    Trace("strings-pending-debug") << "  Now assert equality" << std::endl;
+    Trace("strings-pending-debug") << atom << std::endl;
+    Trace("strings-pending-debug") << Rewriter::rewrite( atom ) << std::endl;
     d_equalityEngine.assertEquality( atom, polarity, exp );
+    Trace("strings-pending-debug") << "  Finished assert equality" << std::endl;
   } else {
     if( atom.getKind()==kind::STRING_IN_REGEXP ) {
       if( d_ext_func_terms.find( atom )==d_ext_func_terms.end() ){
@@ -811,9 +812,11 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
     }
     d_equalityEngine.assertPredicate( atom, polarity, exp );
   }
+  Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   //collect extended function terms in the atom
   std::map< Node, bool > visited;
   collectExtendedFuncTerms( atom, visited );
+  Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }
 
 void TheoryStrings::doPendingFacts() {
@@ -1310,13 +1313,12 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
             //we're done
             //addNormalFormPair( normal_form_src[i], normal_form_src[j] );
           } else {
-            Node length_term_i = getLength( normal_forms[i][index_i] );
-            Node length_term_j = getLength( normal_forms[j][index_j] );
+            std::vector< Node > lexp;
+            Node length_term_i = getLength( normal_forms[i][index_i], lexp );
+            Node length_term_j = getLength( normal_forms[j][index_j], lexp );
             //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-            if( !areDisequal(length_term_i, length_term_j) &&
-              !areEqual(length_term_i, length_term_j) &&
-              normal_forms[i][index_i].getKind()!=kind::CONST_STRING &&
-              normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
+            if( !areDisequal(length_term_i, length_term_j) && !areEqual(length_term_i, length_term_j) &&
+                normal_forms[i][index_i].getKind()!=kind::CONST_STRING && normal_forms[j][index_j].getKind()!=kind::CONST_STRING ) {
               //length terms are equal, merge equivalence classes if not already done so
               Node length_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, length_term_i, length_term_j );
               Trace("strings-solve-debug") << "Non-simple Case 1 : string lengths neither equal nor disequal" << std::endl;
@@ -1329,8 +1331,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
               Trace("strings-solve-debug") << "Non-simple Case 2 : must compare strings" << std::endl;
               int loop_in_i = -1;
               int loop_in_j = -1;
-              if(detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j)) {
-                if(!flag_lb) {
+              if( detectLoop(normal_forms, i, j, index_i, index_j, loop_in_i, loop_in_j) ){
+                if( !flag_lb ){
                   c_i = i;
                   c_j = j;
                   c_loop_n_index = loop_in_i!=-1 ? i : j;
@@ -1354,8 +1356,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                 Node conc;
                 std::vector< Node > antec;
                 Trace("strings-solve-debug") << "No loops detected." << std::endl;
-                if( normal_forms[i][index_i].getKind() == kind::CONST_STRING ||
-                  normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
+                if( normal_forms[i][index_i].getKind() == kind::CONST_STRING || normal_forms[j][index_j].getKind() == kind::CONST_STRING) {
                   unsigned const_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? i : j;
                   unsigned const_index_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? index_i : index_j;
                   unsigned nconst_k = normal_forms[i][index_i].getKind() == kind::CONST_STRING ? j : i;
@@ -1508,29 +1509,21 @@ bool TheoryStrings::processSimpleNEq( std::vector< std::vector< Node > > &normal
         index_i++;
         success = true;
       } else {
-        Node length_term_i = getLength( normal_forms[i][index_i] );
-        Node length_term_j = getLength( normal_forms[j][index_j] );
+        std::vector< Node > temp_exp;
+        Node length_term_i = getLength( normal_forms[i][index_i], temp_exp );
+        Node length_term_j = getLength( normal_forms[j][index_j], temp_exp );
         //check  length(normal_forms[i][index]) == length(normal_forms[j][index])
-        if( areEqual(length_term_i, length_term_j) ) {
+        if( areEqual( length_term_i, length_term_j ) ){
           Trace("strings-solve-debug") << "Simple Case 2 : string lengths are equal" << std::endl;
           Node eq = normal_forms[i][index_i].eqNode( normal_forms[j][index_j] );
           //eq = Rewriter::rewrite( eq );
           Node length_eq = length_term_i.eqNode( length_term_j );
-          std::vector< Node > temp_exp;
           temp_exp.insert(temp_exp.end(), curr_exp.begin(), curr_exp.end() );
           temp_exp.push_back(length_eq);
-          //must add explanation for length terms
-          if( !normal_forms[i][index_i].isConst() && !length_term_i.isConst() && length_term_i[0]!=normal_forms[i][index_i] ){
-            temp_exp.push_back( length_term_i[0].eqNode( normal_forms[i][index_i] ) );
-          }
-          if( !normal_forms[j][index_j].isConst() && !length_term_j.isConst() && length_term_j[0]!=normal_forms[j][index_j] ){
-            temp_exp.push_back( length_term_j[0].eqNode( normal_forms[j][index_j] ) );
-          }
-          Node eq_exp = mkAnd( temp_exp );
-          sendInfer( eq_exp, eq, "LengthEq" );
+          sendInfer( mkAnd( temp_exp ), eq, "LengthEq" );
           return true;
-        } else if(( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) ||
-              ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ) {
+        }else if( ( normal_forms[i][index_i].getKind()!=kind::CONST_STRING && index_i==normal_forms[i].size()-1 ) ||
+                  ( normal_forms[j][index_j].getKind()!=kind::CONST_STRING && index_j==normal_forms[j].size()-1 ) ){
           Trace("strings-solve-debug") << "Simple Case 3 : at endpoint" << std::endl;
           Node conc;
           std::vector< Node > antec;
@@ -1716,8 +1709,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
         Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
         if( !areEqual( i, j ) ) {
           Assert( i.getKind()!=kind::CONST_STRING || j.getKind()!=kind::CONST_STRING );
-          Node li = getLength( i );
-          Node lj = getLength( j );
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
           if( areDisequal(li, lj) ){
             //if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
 
@@ -1740,9 +1734,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
             Node sk3 = mkSkolemCached( i, j, sk_id_deq_z, "z_dsplit", 1 );
             //Node nemp = sk3.eqNode(d_emptyString).negate();
             //conc.push_back(nemp);
-            Node lsk1 = getLength( sk1 );
+            Node lsk1 = mkLength( sk1 );
             conc.push_back( lsk1.eqNode( li ) );
-            Node lsk2 = getLength( sk2 );
+            Node lsk2 = mkLength( sk2 );
             conc.push_back( lsk2.eqNode( lj ) );
             conc.push_back( NodeManager::currentNM()->mkNode( kind::OR, j.eqNode( mkConcat( sk1, sk3 ) ), i.eqNode( mkConcat( sk2, sk3 ) ) ) );
             sendLemma( mkExplain( antec, antec_new_lits ), NodeManager::currentNM()->mkNode( kind::AND, conc ), "D-DISL-Split" );
@@ -1794,11 +1788,9 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
       Trace("strings-solve-debug") << "Disequality normalize empty" << std::endl;
       std::vector< Node > ant;
       //we have a conflict : because the lengths are equal, the remainder needs to be empty, which will lead to a conflict
-      Node lni = getLength( ni );
-      Node lnj = getLength( nj );
+      Node lni = getLengthExp( ni, ant, d_normal_forms_base[ni] );
+      Node lnj = getLengthExp( nj, ant, d_normal_forms_base[nj] );
       ant.push_back( lni.eqNode( lnj ) );
-      ant.push_back( getLengthTerm( ni ).eqNode( d_normal_forms_base[ni] ) );
-      ant.push_back( getLengthTerm( nj ).eqNode( d_normal_forms_base[nj] ) );
       ant.insert( ant.end(), d_normal_forms_exp[ni].begin(), d_normal_forms_exp[ni].end() );
       ant.insert( ant.end(), d_normal_forms_exp[nj].begin(), d_normal_forms_exp[nj].end() );
       std::vector< Node > cc;
@@ -1844,8 +1836,9 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node
             return 1;
           }
         } else {
-          Node li = getLength( i );
-          Node lj = getLength( j );
+          std::vector< Node > lexp;
+          Node li = getLength( i, lexp );
+          Node lj = getLength( j, lexp );
           if( areEqual( li, lj ) && areDisequal( i, j ) ) {
             Trace("strings-solve") << "Simple Case 2 : found equal length disequal sub strings " << i << " " << j << std::endl;
             //we are done: D-Remove
@@ -2117,6 +2110,10 @@ Node TheoryStrings::mkConcat( const std::vector< Node >& c ) {
   return Rewriter::rewrite( c.size()>1 ? NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, c ) : ( c.size()==1 ? c[0] : d_emptyString ) );
 }
 
+Node TheoryStrings::mkLength( Node t ) {
+  return Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
+}
+
 //isLenSplit: 0-yes, 1-no, 2-ignore
 Node TheoryStrings::mkSkolemS( const char *c, int isLenSplit ) {
   Node n = NodeManager::currentNM()->mkSkolem( c, NodeManager::currentNM()->stringType(), "string sko" );
@@ -2338,7 +2335,8 @@ void TheoryStrings::checkFlatForms() {
               }else{
                 Node curr = d_flat_form[a][count];
                 Node curr_c = d_eqc_to_const[curr];
-                Node lcurr = getLength( curr );
+                std::vector< Node > lexp;
+                Node lcurr = getLength( curr, lexp );
                 for( unsigned i=1; i<it->second.size(); i++ ){
                   b = it->second[i];
                   if( std::find( inelig.begin(), inelig.end(), b )==inelig.end() ){
@@ -2382,16 +2380,12 @@ void TheoryStrings::checkFlatForms() {
                           break;
                         }else{
                           //if lengths are the same, apply LengthEq
-                          Node lcc = getLength( cc );
+                          Node lcc = getLength( cc, lexp );
                           if( areEqual( lcurr, lcc ) ){
+                            Trace("strings-ff-debug") << "Infer " << ac << " == " << bc << " since " << lcurr << " == " << lcc << std::endl;
                             //exp_n.push_back( getLength( curr, true ).eqNode( getLength( cc, true ) ) );
+                            exp.insert( exp.end(), lexp.begin(), lexp.end() );
                             addToExplanation( lcurr, lcc, exp );
-                            if( !lcc.isConst() ){
-                              addToExplanation( bc, lcc[0], exp );
-                            }
-                            if( !lcurr.isConst() ){
-                              addToExplanation( ac, lcurr[0], exp );
-                            }
                             conc = ac.eqNode( bc );
                             inf_type = 1;
                             break;
@@ -2485,12 +2479,8 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
               Node ncy = checkCycles( nr, curr, exp );
               if( !ncy.isNull() ){
                 Trace("strings-cycle") << eqc << " cycle: " << ncy << " at " << n << "[" << i << "] : " << n[i] << std::endl;
-                if( n!=eqc ){
-                  exp.push_back( n.eqNode( eqc ) );
-                }
-                if( nr!=n[i] ){
-                  exp.push_back( nr.eqNode( n[i] ) );
-                }
+                addToExplanation( n, eqc, exp );
+                addToExplanation( nr, n[i], exp );
                 if( ncy==eqc ){
                   //can infer all other components must be empty
                   for( unsigned j=0; j<n.getNumChildren(); j++ ){
@@ -2529,8 +2519,10 @@ Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vecto
 
 void TheoryStrings::checkNormalForms() {
   // simple extended func reduction
+  Trace("strings-process") << "Check extended function reduction effort=1..." << std::endl;
   checkExtfReduction( 1 );
-  if( !hasProcessed() ){  
+  Trace("strings-process") << "Done check extended function reduction" << std::endl;
+  if( !hasProcessed() ){
     Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
     //calculate normal forms for each equivalence class, possibly adding splitting lemmas
     d_normal_forms.clear();
@@ -2658,7 +2650,7 @@ void TheoryStrings::checkLengthsEqc() {
                 Node pv = (*it).second;
                 Assert( d_proxy_var_to_length.find( pv )!=d_proxy_var_to_length.end() );
                 Node pvl = d_proxy_var_to_length[pv];
-                Node ceq = Rewriter::rewrite( getLength( pv, true ).eqNode( pvl ) );
+                Node ceq = Rewriter::rewrite( mkLength( pv ).eqNode( pvl ) );
                 sendLemma( d_true, ceq, "LEN-NORM-I" );
               }
             }
@@ -3911,10 +3903,10 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
         to_reduce = n;
       }
       if( !to_reduce.isNull() ){
-        checkExtfInference( n, to_reduce, effort );
         if( effort==1 ){
           Trace("strings-extf") << "  cannot rewrite extf : " << to_reduce << std::endl;
         }
+        checkExtfInference( n, to_reduce, effort );
         if( Trace.isOn("strings-extf-list") ){
           Trace("strings-extf-list") << "  * " << to_reduce;
           if( d_extf_pol[n]!=0 ){
@@ -3957,7 +3949,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
         }
       }else{
         //store this (reduced) assertion
-        Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
+        //Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
         bool pol = n_pol==1;
         if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
           Trace("strings-extf-debug") << "  store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
@@ -4089,22 +4081,23 @@ void TheoryStrings::checkNegContains( std::vector< Node >& negContains ) {
       Node atom = negContains[i];
       Node x = atom[0];
       Node s = atom[1];
-      Node lenx = getLength(x);
-      Node lens = getLength(s);
+      std::vector< Node > lexp;
+      Node lenx = getLength( x, lexp );
+      Node lens = getLength( s, lexp );
       if( areEqual(lenx, lens) ){
         if(d_neg_ctn_eqlen.find(atom) == d_neg_ctn_eqlen.end()) {
-          Node eq = lenx.eqNode(lens);
-          Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, atom.negate(), eq ) );
+          lexp.push_back( lenx.eqNode(lens) );
+          lexp.push_back( atom.negate() );
           Node xneqs = x.eqNode(s).negate();
           d_neg_ctn_eqlen.insert( atom );
-          sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+          sendLemma( mkExplain( lexp ), xneqs, "NEG-CTN-EQL" );
         }
-      }else if( !areDisequal(lenx, lens) ){
+      }else if( !areDisequal( lenx, lens ) ){
         if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) {
           lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x);
           lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
           d_neg_ctn_ulen.insert( atom );
-          sendSplit(lenx, lens, "NEG-CTN-SP");
+          sendSplit( lenx, lens, "NEG-CTN-SP" );
         }
       }else{
         if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) {

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 52bc37cb8b24c2d79133c3faf47046fe7cbd82ac..721ba864e4af038309fb2f0543acc4f7aedca75b 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -133,8 +133,9 @@ private:
   bool hasTerm( Node a );
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
-  Node getLengthTerm( Node t );
-  Node getLength( Node t, bool use_t = false );
+  // t is representative, te = t, add lt = te to explanation exp
+  Node getLengthExp( Node t, std::vector< Node >& exp, Node te );
+  Node getLength( Node t, std::vector< Node >& exp );
 
 private:
   /** The notify class */
@@ -300,7 +301,7 @@ private:
   void checkLengthsEqc();
   //cardinality check
   void checkCardinality();
-  
+
 public:
   /** preregister term */
   void preRegisterTerm(TNode n);
@@ -323,7 +324,7 @@ public:
 protected:
   /** compute care graph */
   void computeCareGraph();
-  
+
   //do pending merges
   void assertPendingFact(Node atom, bool polarity, Node exp);
   void doPendingFacts();
@@ -331,7 +332,7 @@ protected:
   bool hasProcessed();
   void addToExplanation( Node a, Node b, std::vector< Node >& exp );
   void addToExplanation( Node lit, std::vector< Node >& exp );
-  
+
   //register term
   bool registerTerm( Node n );
   //send lemma
@@ -343,6 +344,7 @@ protected:
   inline Node mkConcat( Node n1, Node n2 );
   inline Node mkConcat( Node n1, Node n2, Node n3 );
   inline Node mkConcat( const std::vector< Node >& c );
+  inline Node mkLength( Node n );
   //mkSkolem
   inline Node mkSkolemS(const char * c, int isLenSplit = 0);
   //inline Node mkSkolemI(const char * c);

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index ccce5a86d4e3d512ec98556ed59bdc434e85b68f..80eb89cc32f56fa0b191cff79a6643dca88cff8f 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -113,20 +113,20 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     //length is positive
     Node c3 = NodeManager::currentNM()->mkNode( kind::GT, t[2], d_zero );
     Node cond = NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3 );
-    
+
     Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for substr" );
     Node sk2 = NodeManager::currentNM()->mkSkolem( "ss2", NodeManager::currentNM()->stringType(), "created for substr" );
     Node b11 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk2 ) );
     //length of first skolem is second argument
     Node b12 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ).eqNode( t[1] );
     //length of second skolem is abs difference between end point and end of string
-    Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode( 
-                 NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ), 
+    Node b13 = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ).eqNode(
+                 NodeManager::currentNM()->mkNode( kind::ITE, NodeManager::currentNM()->mkNode( kind::GEQ, lt0, t12 ),
                     NodeManager::currentNM()->mkNode( kind::MINUS, lt0, t12 ), d_zero ) );
-    
+
     Node b1 = NodeManager::currentNM()->mkNode( kind::AND, b11, b12, b13 );
     Node b2 = t.eqNode( NodeManager::currentNM()->mkConst( ::CVC4::String("") ) );
-    
+
     Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, b1, b2 ) );
     new_nodes.push_back( lemma );
     d_cache[t] = t;
@@ -488,7 +488,7 @@ Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
   unsigned num = t.getNumChildren();
   if(num == 0) {
     return simplify(t, new_nodes);
-  } else {
+  }else{
     bool changed = false;
     std::vector< Node > cc;
     if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 16860646281ca6b8432021af92644fd352f62679..6d84ace907476eb96dff670bef33cd9d4523f5c4 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1025,8 +1025,6 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
   } else if(node.getKind() == kind::STRING_LENGTH) {
     if(node[0].isConst()) {
       retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( node[0].getConst<String>().size() ) );
-    } else if(node[0].getKind() == kind::STRING_SUBSTR) {
-      //retNode = node[0][2];
     } else if(node[0].getKind() == kind::STRING_CONCAT) {
       Node tmpNode = rewriteConcatString(node[0]);
       if(tmpNode.isConst()) {
@@ -1054,6 +1052,8 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
       }
     }
+    //else if(node[0].getKind() == kind::STRING_SUBSTR) {
+    //retNode = node[0][2];
   }else if( node.getKind() == kind::STRING_CHARAT ){
     Node one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
     retNode = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, node[0], node[1], one);
@@ -1080,7 +1080,7 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
               }else{
                 children.erase( children.begin(), children.begin()+1 );
-                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ), 
+                retNode = NodeManager::currentNM()->mkNode( kind::STRING_SUBSTR, mkConcat( kind::STRING_CONCAT, children ),
                                                             NodeManager::currentNM()->mkNode( kind::MINUS, node[1], NodeManager::currentNM()->mkConst( size ) ),
                                                             node[2] );
               }

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 4d1da2efb1fd0cf5133305c3a63a69ef7b61e2f0..f5c6048e67d07656062af015cc4784ccb25f3329 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -73,7 +73,8 @@ TESTS = \
   bug686dd.smt2 \
   idof-handg.smt2 \
   fmf001.smt2 \
-  type002.smt2
+  type002.smt2 \
+  crash-1019.smt2
 
 FAILING_TESTS =
 

diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
new file mode 100755 (executable)
index 0000000..1a41ba7
--- /dev/null
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)\r
+(set-option :strings-exp true)\r
+(set-option :rewrite-divk true)\r
+(set-info :status unsat)\r
+ \r
+(declare-fun s () String)\r
+ \r
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))\r
+ \r
+(check-sat)\r