Minor improvements to strings. Refactor rewriter. Enable fairness for multiple sorts...

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index ad878e0f3c15676e4367ae9f5636f0699cc20780..f4019450de9fc2deca31631b3a345d43da80e805 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -506,6 +506,7 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
       Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one);
       Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], d_one);
       return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], d_one);
       break;
     }
 
@@ -530,6 +531,7 @@ Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) {
       Node totalf = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
       Node uf = NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_ufSubstr, node[0], node[1], node[2]);
       return NodeManager::currentNM()->mkNode( kind::ITE, cond, totalf, uf );
+      //return NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, node[0], node[1], node[2]);
       break;
     }
 
@@ -687,9 +689,9 @@ bool TheoryStrings::doPreprocess( Node atom ) {
       }
       plem = Rewriter::rewrite( plem );
       Trace("strings-assert") << "(assert " << plem << ")" << std::endl;
-      Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess" << std::endl;
+      Trace("strings-lemma") << "Strings::Lemma " << plem << " by preprocess reduction" << std::endl;
       d_out->lemma( plem );
-      Trace("strings-pp-lemma") << "Preprocess reduce lemma : " << plem << std::endl;
+      Trace("strings-pp-lemma") << "Preprocess reduction lemma : " << plem << std::endl;
       Trace("strings-pp-lemma") << "...from " << atom << std::endl;
     }else{
       Trace("strings-assertion-debug") << "...preprocess ok." << std::endl;
@@ -700,6 +702,7 @@ bool TheoryStrings::doPreprocess( Node atom ) {
       Trace("strings-assertion-debug") << "...new nodes : " << nnlem << std::endl;
       Trace("strings-pp-lemma") << "Preprocess lemma : " << nnlem << std::endl;
       Trace("strings-pp-lemma") << "...from " << atom << std::endl;
+      Trace("strings-lemma") << "Strings::Lemma " << nnlem << " by preprocess" << std::endl;
       Trace("strings-assert") << "(assert " << nnlem << ")" << std::endl;
       d_out->lemma( nnlem );
     }
@@ -1291,12 +1294,12 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec,
   }
   return true;
 }
-Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){
+Node TheoryStrings::mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit ){
   //return mkSkolemS( c, isLenSplit );
-  std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit );
+  std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( id );
   if( it==d_skolem_cache[a][b].end() ){
     Node sk = mkSkolemS( c, isLenSplit );
-    d_skolem_cache[a][b][isLenSplit] = sk;
+    d_skolem_cache[a][b][id] = sk;
     return sk;
   }else{
     return it->second;
@@ -1410,10 +1413,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                     antec.insert( antec.end(), curr_exp.begin(), curr_exp.end() );
                     Node xnz = other_str.eqNode(d_emptyString).negate();
                     antec.push_back( xnz );
-                    //Node sk = mkSkolemS( "c_spt" );
                     Node conc;
-                    if( normal_forms[nconst_k].size() > nconst_index_k + 1 &&
-                      normal_forms[nconst_k][nconst_index_k + 1].isConst() ) {
+                    if( normal_forms[nconst_k].size() > nconst_index_k + 1 && 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 stra1 = stra.substr(1);
@@ -1421,14 +1422,14 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                       size_t p2 = stra1.find(strb);
                       p = p2==std::string::npos? p : ( p>p2+1? p2+1 : p );
                       Node prea = p==stra.size()? const_str : NodeManager::currentNM()->mkConst(stra.substr(0, p));
-                      Node sk = mkSkolemSplit( other_str, prea, "c_spt" );
+                      Node sk = mkSkolemCached( other_str, prea, sk_id_c_spt, "c_spt" );
                       conc = other_str.eqNode( mkConcat(prea, sk) );
                       Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << std::endl;
                     } else {
                       // normal v/c split
                       Node firstChar = const_str.getConst<String>().size() == 1 ? const_str :
                         NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) );
-                      Node sk = mkSkolemSplit( other_str, firstChar, "c_spt" );
+                      Node sk = mkSkolemCached( other_str, firstChar, sk_id_vc_spt, "c_spt" );
                       conc = other_str.eqNode( mkConcat(firstChar, sk) );
                       Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << const_str << " (normal) " << std::endl;
                     }
@@ -1460,8 +1461,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms
                     }
                   }
 
-                  //Node sk = mkSkolemS( "v_spt", 1 );
-                  Node sk = mkSkolemSplit( normal_forms[i][index_i], normal_forms[j][index_j], "v_spt", 1 );
+                  Node sk = mkSkolemCached( normal_forms[i][index_i], normal_forms[j][index_j], sk_id_v_spt, "v_spt", 1 );
                   Node eq1 = normal_forms[i][index_i].eqNode( mkConcat(normal_forms[j][index_j], sk) );
                   Node eq2 = normal_forms[j][index_j].eqNode( mkConcat(normal_forms[i][index_i], sk) );
                   conc = Rewriter::rewrite(NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ));
@@ -1777,18 +1777,16 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) {
             }
             antec_new_lits.push_back( li.eqNode( lj ).negate() );
             std::vector< Node > conc;
-            Node sk1 = mkSkolemS( "x_dsplit" );
-            Node sk2 = mkSkolemS( "y_dsplit" );
-            Node sk3 = mkSkolemS( "z_dsplit", 1 );
+            Node sk1 = mkSkolemCached( i, j, sk_id_deq_x, "x_dsplit" );
+            Node sk2 = mkSkolemCached( i, j, sk_id_deq_y, "y_dsplit" );
+            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 );
             conc.push_back( lsk1.eqNode( li ) );
             Node lsk2 = getLength( 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 ) ) ) );
-
+            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" );
             ++(d_statistics.d_deq_splits);
             return true;
@@ -1954,25 +1952,9 @@ bool TheoryStrings::registerTerm( Node n ) {
     d_registered_terms_cache.insert(n);
     Debug("strings-register") << "TheoryStrings::registerTerm() " << n << endl;
     if(n.getType().isString()) {
-      if(n.getKind() == kind::STRING_SUBSTR_TOTAL) {
-        Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
-                  NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[0] ),
-                  NodeManager::currentNM()->mkNode( kind::PLUS, n[1], n[2] ) );
-        Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero);
-        Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GT, n[2], d_zero);
-        Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
-        Node sk1 = mkSkolemS( "ss1", 2 );
-        Node sk3 = mkSkolemS( "ss3", 2 );
-        Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) );
-        Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
-        Node lenc = n[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n ) );
-        Node lemma = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::ITE, cond,
-          NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
-          n.eqNode(d_emptyString)));
-        Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl;
-         Trace("strings-assert") << "(assert " << lemma << ")" << std::endl;
-        d_out->lemma(lemma);
-      }
+      //register length information:
+      //  for variables, split on empty vs positive length
+      //  for concat/const, introduce proxy var and state length relation
       if( n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
         if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
           sendLengthLemma( n );
@@ -3947,6 +3929,8 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) {
               return;
             }
           }
+        //}else if( hasTerm( nrc ) && !areEqual( nrc, n ) ){
+        //  Trace("strings-extf-debug") << "Reduction inference : " << nrc << " " << n << std::endl;  TODO?
         }else{
           if( effort==1 ){
             Trace("strings-extf") << "  cannot rewrite extf : " << nrc << std::endl;
@@ -4063,8 +4047,8 @@ void TheoryStrings::checkPosContains( std::vector< Node >& posContains ) {
       Node s = atom[1];
       if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
         if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) {
-          Node sk1 = mkSkolemS( "sc1" );
-          Node sk2 = mkSkolemS( "sc2" );
+          Node sk1 = mkSkolemCached( x, s, sk_id_ctn_pre, "sc1" );
+          Node sk2 = mkSkolemCached( x, s, sk_id_ctn_post, "sc2" );
           Node eq = Rewriter::rewrite( x.eqNode( mkConcat( sk1, s, sk2 ) ) );
           sendLemma( atom, eq, "POS-INC" );
           d_pos_ctn_cached.insert( atom );

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index ce2422faf71ee6428906d9001ab2bcba0f3e6ba4..7e09a8e5b10e71367dcaca250bcc5ba90e18fe0f 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -360,9 +360,19 @@ protected:
   void printConcat( std::vector< Node >& n, const char * c );
 
   void inferSubstitutionProxyVars( Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& unproc );
-
+  
+  enum {
+    sk_id_c_spt,
+    sk_id_vc_spt,
+    sk_id_v_spt,
+    sk_id_ctn_pre,
+    sk_id_ctn_post,
+    sk_id_deq_x,
+    sk_id_deq_y,
+    sk_id_deq_z,
+  };
   std::map< Node, std::map< Node, std::map< int, Node > > > d_skolem_cache;
-  Node mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit = 0 );
+  Node mkSkolemCached( Node a, Node b, int id, const char * c, int isLenSplit = 0 );
 private:
 
   // Special String Functions

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index e9b144a23dae041462a8de2ded67a28cd6a08210..4e2b00fb1a0d981c25b1a5e77c54a7f47ff6a591 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -212,8 +212,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool d
     Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" );
     Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) );
     Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+    Node lenc = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t ) );
     Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond,
-            NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ),
+            NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i, lenc ),
             t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
     new_nodes.push_back( lemma );
     d_cache[t] = t;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index fc17198c2cc8688b515afe3867a1b00c85de10f9..6356277ede3378d017a29f0eebe961e7be5ca68a 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -1084,262 +1084,12 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
         }
       }
     }
-  } else if( node.getKind() == kind::STRING_STRCTN ){
-    if( node[0] == node[1] ) {
-      retNode = NodeManager::currentNM()->mkConst( true );
-    } else if( node[0].isConst() && node[1].isConst() ) {
-      CVC4::String s = node[0].getConst<String>();
-      CVC4::String t = node[1].getConst<String>();
-      if( s.find(t) != std::string::npos ){
-        retNode = NodeManager::currentNM()->mkConst( true );
-      }else{
-        retNode = NodeManager::currentNM()->mkConst( false );
-      }
-    }else if( node[0].getKind()==kind::STRING_CONCAT ) {
-      //component-wise containment
-      unsigned n1 = node[0].getNumChildren();
-      std::vector< Node > nc1;
-      getConcat( node[1], nc1 );
-      unsigned n2 = nc1.size();
-      if( n1>n2 ){
-        bool flag = false;
-        unsigned diff = n1-n2;
-        for(unsigned i=0; i<diff; i++) {
-          if( node[0][i]==nc1[0] ){
-            flag = true;
-            for(unsigned j=1; j<n2; j++) {
-              if( node[0][i+j]!=nc1[j] ){
-                flag = false;
-                break;
-              }
-            }
-            if(flag) {
-              break;
-            }
-          }
-        }
-        if( flag ){
-          retNode = NodeManager::currentNM()->mkConst( true );
-        }
-      }
-      if( retNode==node ){
-        if( node[1].isConst() ){
-          CVC4::String t = node[1].getConst<String>();
-          for(unsigned i=0; i<node[0].getNumChildren(); i++) {
-            //constant contains
-            if( node[0][i].isConst() ){
-              CVC4::String s = node[0][i].getConst<String>();
-              if( s.find(t)!=std::string::npos ) {
-                retNode = NodeManager::currentNM()->mkConst( true );
-                break;
-              }else{
-                //if no overlap, we can split into disjunction
-                // if first child, only require no left overlap
-                // if last child, only require no right overlap
-                if( i==0 || i==node[0].getNumChildren()-1 || t.find(s)==std::string::npos ){
-                  bool do_split = false;
-                  int sot = s.overlap( t );
-                  Trace("strings-ext-rewrite") << "Overlap " << s << " " << t << " is " << sot << std::endl;
-                  if( sot==0 ){
-                    do_split = i==0;
-                  }
-                  if( !do_split && ( i==(node[0].getNumChildren()-1) || sot==0 ) ){
-                    int tos = t.overlap( s );
-                    Trace("strings-ext-rewrite") << "Overlap " << t << " " << s << " is " << tos << std::endl;
-                    if( tos==0 ){
-                      do_split = true;
-                    }
-                  }
-                  if( do_split ){
-                    std::vector< Node > nc0;
-                    getConcat( node[0], nc0 );
-                    std::vector< Node > spl[2];
-                    if( i>0 ){
-                      spl[0].insert( spl[0].end(), nc0.begin(), nc0.begin()+i );
-                    }
-                    if( i<nc0.size()-1 ){
-                      spl[1].insert( spl[1].end(), nc0.begin()+i+1, nc0.end() );
-                    }
-                    retNode = NodeManager::currentNM()->mkNode( kind::OR,
-                                NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[0] ), node[1] ),
-                                NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[1] ), node[1] ) );
-                    break;
-                  }
-                }
-              }
-            }
-          }
-        }
-      }
-    }else if( node[0].isConst() ){
-      if( node[1].getKind()==kind::STRING_CONCAT ){
-        //must find constant components in order
-        size_t pos = 0;
-        CVC4::String t = node[0].getConst<String>();
-        for(unsigned i=0; i<node[1].getNumChildren(); i++) {
-          if( node[1][i].isConst() ){
-            CVC4::String s = node[1][i].getConst<String>();
-            size_t new_pos = t.find(s,pos);
-            if( new_pos==std::string::npos ) {
-              retNode = NodeManager::currentNM()->mkConst( false );
-              break;
-            }else{
-              pos = new_pos + s.size();
-            }
-          }
-        }
-      }
-    }
+  }else if( node.getKind() == kind::STRING_STRCTN ){
+    retNode = rewriteContains( node );
   }else if( node.getKind()==kind::STRING_STRIDOF ){
-    std::vector< Node > children;
-    getConcat( node[0], children );
-    //std::vector< Node > children1;
-    //getConcat( node[1], children1 );  TODO
-    std::size_t start = 0;
-    std::size_t val2 = 0;
-    if( node[2].isConst() ){
-      CVC4::Rational RMAXINT(LONG_MAX);
-      if( node[2].getConst<Rational>()>RMAXINT ){
-        Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of");
-        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-      }else if( node[2].getConst<Rational>().sgn()==-1 ){
-        //constant negative
-        retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-      }else{
-        val2 = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
-        start = val2;
-      }
-    }
-    if( retNode==node ){
-      bool prefixNoOverlap = false;
-      CVC4::String t;
-      if( node[1].isConst() ){
-        t = node[1].getConst<String>();
-      }
-      //unsigned ch1_index = 0;
-      for( unsigned i=0; i<children.size(); i++ ){
-        bool do_splice = false;
-        if( children[i].isConst() ){
-          CVC4::String s = children[i].getConst<String>();
-          if( node[1].isConst() ){
-            if( i==0 ){
-              std::size_t ret = s.find( t, start );
-              if( ret!=std::string::npos ) {
-                //exact if start value was constant
-                if( node[2].isConst() ){
-                  retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) );
-                  break;
-                }
-              }else{
-                //exact if we scanned the entire string
-                if( node[0].isConst() ){
-                  retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
-                  break;
-                }else{
-                  prefixNoOverlap = (s.overlap(t)==0);
-                  Trace("strings-rewrite-debug") << "Prefix no overlap : " << s << " " << t << " " << prefixNoOverlap << std::endl;
-                }
-              }
-            }else if( !node[2].isConst() ){
-              break;
-            }else{
-              std::size_t ret = s.find(t, start);
-              //remove remaining children after finding the string
-              if( ret!=std::string::npos ){
-                Assert( ret+t.size()<=s.size() );
-                children[i] = NodeManager::currentNM()->mkConst( ::CVC4::String( s.substr(0,ret+t.size()) ) );
-                do_splice = true;
-              }else{
-                //if no overlap on last child, can remove
-                if( t.overlap( s )==0 && i==children.size()-1 ){
-                  std::vector< Node > spl;
-                  spl.insert( spl.end(), children.begin(), children.begin()+i );
-                  retNode = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] );
-                  break;
-                }
-              }
-            }
-          }
-          //decrement the start index
-          if( start>0 ){
-            if( s.size()>start ){
-              start = 0;
-            }else{
-              start = start - s.size();
-            }
-          }
-        }else if( !node[2].isConst() ){
-          break;
-        }else{
-          if( children[i]==node[1] && start==0 ){
-            //can remove beyond this
-            do_splice = true;
-          }
-        }
-        if( do_splice ){
-          std::vector< Node > spl;
-          //since we definitely will find the string, we can safely add the length of the constant non-overlapping prefix
-          if( prefixNoOverlap ){
-            Node pl = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, children[0] ) );
-            Assert( pl.isConst() );
-            Assert( node[2].isConst() );
-            int new_start = val2 - pl.getConst<Rational>().getNumerator().toUnsignedInt();
-            if( new_start<0 ){
-              new_start = 0;
-            }
-            spl.insert( spl.end(), children.begin()+1, children.begin()+i+1 );
-            retNode = NodeManager::currentNM()->mkNode( kind::PLUS, pl,
-                        NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], NodeManager::currentNM()->mkConst( Rational(new_start) ) ) );
-          }else{
-            spl.insert( spl.end(), children.begin(), children.begin()+i+1 );
-            retNode = NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] );
-          }
-          break;
-        }
-      }
-    }
+    retNode = rewriteIndexof( node );
   }else if( node.getKind() == kind::STRING_STRREPL ){
-    if( node[1]==node[2] ){
-      retNode = node[0];
-    }else{
-      std::vector< Node > children;
-      getConcat( node[0], children );
-      if( children[0].isConst() && node[1].isConst() ){
-        CVC4::String s = children[0].getConst<String>();
-        CVC4::String t = node[1].getConst<String>();
-        std::size_t p = s.find(t);
-        if( p != std::string::npos ) {
-          if( node[2].isConst() ){
-            CVC4::String r = node[2].getConst<String>();
-            CVC4::String ret = s.replace(t, r);
-            retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) );
-          } else {
-            CVC4::String s1 = s.substr(0, (int)p);
-            CVC4::String s3 = s.substr((int)p + (int)t.size());
-            Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) );
-            Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) );
-            retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 );
-          }
-          if( children.size()>1 ){
-            children[0] = retNode;
-            retNode = mkConcat( kind::STRING_CONCAT, children );
-          }
-        }else{
-          //could not find replacement string
-          if( node[0].isConst() ){
-            retNode = node[0];
-          }else{
-            //check for overlap, if none, we can remove the prefix
-            if( s.overlap(t)==0 ){
-              std::vector< Node > spl;
-              spl.insert( spl.end(), children.begin()+1, children.end() );
-              retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0],
-                          NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) );
-            }
-          }
-        }
-      }
-    }
+    retNode = rewriteReplace( node );
   }else if( node.getKind() == kind::STRING_PREFIX ){
     if( node[0].isConst() && node[1].isConst() ){
       CVC4::String s = node[1].getConst<String>();
@@ -1629,6 +1379,260 @@ RewriteResponse TheoryStringsRewriter::preRewrite(TNode node) {
   return RewriteResponse(orig==retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL, retNode);
 }
 
+
+Node TheoryStringsRewriter::rewriteContains( Node node ) {
+  if( node[0] == node[1] ){
+    return NodeManager::currentNM()->mkConst( true );
+  }else if( node[0].isConst() && node[1].isConst() ){
+    CVC4::String s = node[0].getConst<String>();
+    CVC4::String t = node[1].getConst<String>();
+    if( s.find(t) != std::string::npos ){
+      return NodeManager::currentNM()->mkConst( true );
+    }else{
+      return NodeManager::currentNM()->mkConst( false );
+    }
+  }else if( node[0].getKind()==kind::STRING_CONCAT ){
+    //component-wise containment
+    unsigned n1 = node[0].getNumChildren();
+    std::vector< Node > nc1;
+    getConcat( node[1], nc1 );
+    unsigned n2 = nc1.size();
+    if( n1>n2 ){
+      unsigned diff = n1-n2;
+      for(unsigned i=0; i<diff; i++) {
+        if( node[0][i]==nc1[0] ){
+          bool flag = true;
+          for(unsigned j=1; j<n2; j++) {
+            if( node[0][i+j]!=nc1[j] ){
+              flag = false;
+              break;
+            }
+          }
+          if(flag) {
+            return NodeManager::currentNM()->mkConst( true );
+          }
+        }
+      }
+    }
+    if( node[1].isConst() ){
+      CVC4::String t = node[1].getConst<String>();
+      for(unsigned i=0; i<node[0].getNumChildren(); i++){
+        //constant contains
+        if( node[0][i].isConst() ){
+          CVC4::String s = node[0][i].getConst<String>();
+          if( s.find(t)!=std::string::npos ) {
+            return NodeManager::currentNM()->mkConst( true );
+          }else{
+            //if no overlap, we can split into disjunction
+            // if first child, only require no left overlap
+            // if last child, only require no right overlap
+            if( i==0 || i==node[0].getNumChildren()-1 || t.find(s)==std::string::npos ){
+              bool do_split = false;
+              int sot = s.overlap( t );
+              Trace("strings-ext-rewrite") << "Overlap " << s << " " << t << " is " << sot << std::endl;
+              if( sot==0 ){
+                do_split = i==0;
+              }
+              if( !do_split && ( i==(node[0].getNumChildren()-1) || sot==0 ) ){
+                int tos = t.overlap( s );
+                Trace("strings-ext-rewrite") << "Overlap " << t << " " << s << " is " << tos << std::endl;
+                if( tos==0 ){
+                  do_split = true;
+                }
+              }
+              if( do_split ){
+                std::vector< Node > nc0;
+                getConcat( node[0], nc0 );
+                std::vector< Node > spl[2];
+                if( i>0 ){
+                  spl[0].insert( spl[0].end(), nc0.begin(), nc0.begin()+i );
+                }
+                if( i<nc0.size()-1 ){
+                  spl[1].insert( spl[1].end(), nc0.begin()+i+1, nc0.end() );
+                }
+                return NodeManager::currentNM()->mkNode( kind::OR,
+                            NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[0] ), node[1] ),
+                            NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, mkConcat( kind::STRING_CONCAT, spl[1] ), node[1] ) );
+              }
+            }
+          }
+        }
+      }
+    }
+  }else if( node[0].isConst() ){
+    if( node[1].getKind()==kind::STRING_CONCAT ){
+      //must find constant components in order
+      size_t pos = 0;
+      CVC4::String t = node[0].getConst<String>();
+      for(unsigned i=0; i<node[1].getNumChildren(); i++) {
+        if( node[1][i].isConst() ){
+          CVC4::String s = node[1][i].getConst<String>();
+          size_t new_pos = t.find(s,pos);
+          if( new_pos==std::string::npos ) {
+            return NodeManager::currentNM()->mkConst( false );
+          }else{
+            pos = new_pos + s.size();
+          }
+        }
+      }
+    }
+  }
+  return node;
+}
+
+Node TheoryStringsRewriter::rewriteIndexof( Node node ) {
+  std::vector< Node > children;
+  getConcat( node[0], children );
+  //std::vector< Node > children1;
+  //getConcat( node[1], children1 );  TODO
+  std::size_t start = 0;
+  std::size_t val2 = 0;
+  if( node[2].isConst() ){
+    CVC4::Rational RMAXINT(LONG_MAX);
+    if( node[2].getConst<Rational>()>RMAXINT ){
+      Assert(node[2].getConst<Rational>() <= RMAXINT, "Number exceeds LONG_MAX in string index_of");
+      return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+    }else if( node[2].getConst<Rational>().sgn()==-1 ){
+      //constant negative
+      return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+    }else{
+      val2 = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+      start = val2;
+    }
+  }
+  bool prefixNoOverlap = false;
+  CVC4::String t;
+  if( node[1].isConst() ){
+    t = node[1].getConst<String>();
+  }
+  //unsigned ch1_index = 0;
+  for( unsigned i=0; i<children.size(); i++ ){
+    bool do_splice = false;
+    if( children[i].isConst() ){
+      CVC4::String s = children[i].getConst<String>();
+      if( node[1].isConst() ){
+        if( i==0 ){
+          std::size_t ret = s.find( t, start );
+          if( ret!=std::string::npos ) {
+            //exact if start value was constant
+            if( node[2].isConst() ){
+              return NodeManager::currentNM()->mkConst( ::CVC4::Rational((unsigned) ret) );
+            }
+          }else{
+            //exact if we scanned the entire string
+            if( node[0].isConst() ){
+              return NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) );
+            }else{
+              prefixNoOverlap = (s.overlap(t)==0);
+              Trace("strings-rewrite-debug") << "Prefix no overlap : " << s << " " << t << " " << prefixNoOverlap << std::endl;
+            }
+          }
+        }else if( !node[2].isConst() ){
+          break;
+        }else{
+          std::size_t ret = s.find(t, start);
+          //remove remaining children after finding the string
+          if( ret!=std::string::npos ){
+            Assert( ret+t.size()<=s.size() );
+            children[i] = NodeManager::currentNM()->mkConst( ::CVC4::String( s.substr(0,ret+t.size()) ) );
+            do_splice = true;
+          }else{
+            //if no overlap on last child, can remove
+            if( t.overlap( s )==0 && i==children.size()-1 ){
+              std::vector< Node > spl;
+              spl.insert( spl.end(), children.begin(), children.begin()+i );
+              return NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] );
+            }
+          }
+        }
+      }
+      //decrement the start index
+      if( start>0 ){
+        if( s.size()>start ){
+          start = 0;
+        }else{
+          start = start - s.size();
+        }
+      }
+    }else if( !node[2].isConst() ){
+      break;
+    }else{
+      if( children[i]==node[1] && start==0 ){
+        //can remove beyond this
+        do_splice = true;
+      }
+    }
+    if( do_splice ){
+      std::vector< Node > spl;
+      //since we definitely will find the string, we can safely add the length of the constant non-overlapping prefix
+      if( prefixNoOverlap ){
+        Node pl = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, children[0] ) );
+        Assert( pl.isConst() );
+        Assert( node[2].isConst() );
+        int new_start = val2 - pl.getConst<Rational>().getNumerator().toUnsignedInt();
+        if( new_start<0 ){
+          new_start = 0;
+        }
+        spl.insert( spl.end(), children.begin()+1, children.begin()+i+1 );
+        return NodeManager::currentNM()->mkNode( kind::PLUS, pl,
+                 NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], NodeManager::currentNM()->mkConst( Rational(new_start) ) ) );
+      }else{
+        spl.insert( spl.end(), children.begin(), children.begin()+i+1 );
+        return NodeManager::currentNM()->mkNode( kind::STRING_STRIDOF, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] );
+      }
+    }
+  }
+  return node;
+}
+
+Node TheoryStringsRewriter::rewriteReplace( Node node ) {
+  if( node[1]==node[2] ){
+    return node[0];
+  }else{
+    std::vector< Node > children;
+    getConcat( node[0], children );
+    if( children[0].isConst() && node[1].isConst() ){
+      CVC4::String s = children[0].getConst<String>();
+      CVC4::String t = node[1].getConst<String>();
+      std::size_t p = s.find(t);
+      if( p != std::string::npos ) {
+        Node retNode;
+        if( node[2].isConst() ){
+          CVC4::String r = node[2].getConst<String>();
+          CVC4::String ret = s.replace(t, r);
+          retNode = NodeManager::currentNM()->mkConst( ::CVC4::String(ret) );
+        } else {
+          CVC4::String s1 = s.substr(0, (int)p);
+          CVC4::String s3 = s.substr((int)p + (int)t.size());
+          Node ns1 = NodeManager::currentNM()->mkConst( ::CVC4::String(s1) );
+          Node ns3 = NodeManager::currentNM()->mkConst( ::CVC4::String(s3) );
+          retNode = NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, ns1, node[2], ns3 );
+        }
+        if( children.size()>1 ){
+          children[0] = retNode;
+          return mkConcat( kind::STRING_CONCAT, children );
+        }else{
+          return retNode;
+        }
+      }else{
+        //could not find replacement string
+        if( node[0].isConst() ){
+          return node[0];
+        }else{
+          //check for overlap, if none, we can remove the prefix
+          if( s.overlap(t)==0 ){
+            std::vector< Node > spl;
+            spl.insert( spl.end(), children.begin()+1, children.end() );
+            return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, children[0],
+                        NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, mkConcat( kind::STRING_CONCAT, spl ), node[1], node[2] ) );
+          }
+        }
+      }
+    }
+  }
+  return node;
+}
+
 void TheoryStringsRewriter::getConcat( Node n, std::vector< Node >& c ) {
   if( n.getKind()==kind::STRING_CONCAT || n.getKind()==kind::REGEXP_CONCAT ){
     for( unsigned i=0; i<n.getNumChildren(); i++ ){

diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index 2a8258a092ee0a08d45910d4136c8574dbed1fd8..f8b420904fb5a0d5612867f73b242b0b83f6dbef 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -54,6 +54,10 @@ public:
   static inline void init() {}
   static inline void shutdown() {}
 
+  static Node rewriteContains( Node n );
+  static Node rewriteIndexof( Node n );
+  static Node rewriteReplace( Node n );
+  
   static void getConcat( Node n, std::vector< Node >& c );
   static Node mkConcat( Kind k, std::vector< Node >& c );
   static Node splitConstant( Node a, Node b, int& index, bool isRev );

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index cde3aef1ce5c61d0c5e920b0a2990f17caeea7de..c62a0dd4a3a1b54814188226f7540bd1e1ee61ef 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -104,7 +104,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     return (*it).second;
   }
   Node ret = n;
-  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL) {
+  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) {
     // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
     // However, if the Decision Engine stops us early, there might be a
     // quantifier that isn't assigned.  In conjunction with miniscoping, this
@@ -193,9 +193,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
       if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) {
         ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
       }
-      if(ret.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
-        //do nothing
-      }
       d_modelCache[n] = ret;
       return ret;
     }

diff --git a/src/theory/uf/options b/src/theory/uf/options
index d9e4c94770258e726747dedb8036d957e378d2ce..cb6ddc0fad7c3b6e027077071e7db36024ef64b0 100644 (file)
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -36,7 +36,7 @@ option ufssCliqueSplits --uf-ss-clique-splits bool :default false
 
 option ufssSymBreak --uf-ss-sym-break bool :default false
  finite model finding symmetry breaking techniques
-option ufssFairness --uf-ss-fair bool :default false
+option ufssFairness --uf-ss-fair bool :default true
  use fair strategy for finite model finding multiple sorts
 
 endmodule

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 8587610787663939ab9e2ab2b69afdd394c57b0a..95671d6ecc985b3c1e3bd0f1de6ecdae4a2270c2 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -124,6 +124,10 @@ void TheoryUF::check(Effort level) {
         ss << "Try using a logic containing \"UFC\"." << std::endl;
         throw Exception( ss.str() );
       }
+      //needed for models
+      if( options::produceModels() && atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ){
+        d_equalityEngine.assertPredicate(atom, polarity, fact);
+      }
     } else {
       d_equalityEngine.assertPredicate(atom, polarity, fact);
     }