adds partial function substr. the use of this function should be guarded, especially...

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index c0365ab55f163b803f7ed81b95f448ba07d06568..885a7c4875e4605585e27a4fc88b6073e3f4570b 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -870,10 +870,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  //| /* substring */
-    //LPAREN_TOK STRSUB_TOK n1=INTEGER_LITERAL n2=INTEGER_LITERAL RPAREN_TOK
-       //{
-       //}
   | /* A non-built-in function application */
     LPAREN_TOK
     functionName[name, CHECK_DECLARED]
@@ -1250,6 +1246,7 @@ builtinOp[CVC4::Kind& kind]
 
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
+  | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }
@@ -1622,7 +1619,7 @@ INT2BV_TOK : 'int2bv';
 //STRCST_TOK : 'str.cst';
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
-//STRSUB_TOK : 'str.sub' ;
+STRSUB_TOK : 'str.sub' ;
 STRINRE_TOK : 'str.in.re';
 STRTORE_TOK : 'str.to.re';
 RECON_TOK : 're.++';

diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 814276a7c9321942ee4ac8fa2aa76205d3b3703f..fe7b9b3d935e46c88d02204b793ad090cf0b7a4b 100644 (file)
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -16,6 +16,8 @@ operator STRING_IN_REGEXP 2 "membership"
 
 operator STRING_LENGTH 1 "string length"
 
+operator STRING_SUBSTR 3 "string substr"
+
 #sort CHAR_TYPE \
 #    Cardinality::INTEGERS \
 #    well-founded \
@@ -99,6 +101,7 @@ typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
 
 typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
 typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
+typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
 
 typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
 

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index bf61d3852f72d91122ad75303eef8fe1eaddcede..291af408bfc0c9ec6eaff29b85ca07b0eed740c8 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -364,7 +364,7 @@ void TheoryStrings::check(Effort e) {
   bool addedLemma = false;
   if( e == EFFORT_FULL && !d_conflict ) {
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-      while( !eqcs_i.isFinished() ){
+      while( !eqcs_i.isFinished() ) {
         Node eqc = (*eqcs_i);
         //if eqc.getType is string
         if (eqc.getType().isString()) {
@@ -372,60 +372,59 @@ void TheoryStrings::check(Effort e) {
             //get the constant for the equivalence class
             //int c_len = ...;
             eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-            while( !eqc_i.isFinished() ){
-              Node n = (*eqc_i);
-
-              //if n is concat, and
-              //if n has not instantiatied the concat..length axiom
-              //then, add lemma
-              if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
-                if( d_length_inst.find(n)==d_length_inst.end() ){
-                    d_length_inst[n] = true;
-                    Trace("strings-debug") << "get n: " << n << endl;
-                    Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
-                                       d_length_intro_vars.push_back( sk );
-                    Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
-                    eq = Rewriter::rewrite(eq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << eq << std::endl;
-                    d_out->lemma(eq);
-                    Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
-                    Node lsum;
-                    if( n.getKind() == kind::STRING_CONCAT ){
-                        //add lemma
-                        std::vector<Node> node_vec;
-                        for( unsigned i=0; i<n.getNumChildren(); i++ ) {
-                            Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
-                            node_vec.push_back(lni);
-                        }
-                        lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
-                    }else{
-                        //add lemma
-                        lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
-                    }
-                    Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
-                    ceq = Rewriter::rewrite(ceq);
-                    Trace("strings-lemma") << "Strings: Add lemma " << ceq << std::endl;
-                    d_out->lemma(ceq);
-                    addedLemma = true;
-                }
-              }
-              ++eqc_i;
-            }
+                       while( !eqc_i.isFinished() ){
+                               Node n = (*eqc_i);
+                               //if n is concat, and
+                               //if n has not instantiatied the concat..length axiom
+                               //then, add lemma
+                               if( n.getKind() == kind::STRING_CONCAT || n.getKind() == kind::CONST_STRING ){
+                                       if( d_length_inst.find(n)==d_length_inst.end() ){
+                                               d_length_inst[n] = true;
+                                               Trace("strings-debug") << "get n: " << n << endl;
+                                               Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" );
+                                               d_length_intro_vars.push_back( sk );
+                                               Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
+                                               eq = Rewriter::rewrite(eq);
+                                               Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl;
+                                               d_out->lemma(eq);
+                                               Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk );
+                                               Node lsum;
+                                               if( n.getKind() == kind::STRING_CONCAT ){
+                                                       //add lemma
+                                                       std::vector<Node> node_vec;
+                                                       for( unsigned i=0; i<n.getNumChildren(); i++ ) {
+                                                               Node lni = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n[i] );
+                                                               node_vec.push_back(lni);
+                                                       }
+                                                       lsum = NodeManager::currentNM()->mkNode( kind::PLUS, node_vec );
+                                               }else{
+                                                       //add lemma
+                                                       lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
+                                               }
+                                               Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum );
+                                               ceq = Rewriter::rewrite(ceq);
+                                               Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl;
+                                               d_out->lemma(ceq);
+                                               addedLemma = true;
+                                       }
+                               }
+                               ++eqc_i;
+                       }
         }
         ++eqcs_i;
-  }
-  if( !addedLemma ){
-      addedLemma = checkNormalForms();
-         Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-      if(!d_conflict && !addedLemma) {
-          addedLemma = checkCardinality();
-                 Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-          if( !d_conflict && !addedLemma ){
-            addedLemma = checkInductiveEquations();
-                       Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
-          }
-      }
-  }
+         }
+         if( !addedLemma ){
+                 addedLemma = checkNormalForms();
+                 Trace("strings-process") << "Done check normal forms, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                 if(!d_conflict && !addedLemma) {
+                         addedLemma = checkCardinality();
+                         Trace("strings-process") << "Done check cardinality, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                         if( !d_conflict && !addedLemma ){
+                               addedLemma = checkInductiveEquations();
+                               Trace("strings-process") << "Done check inductive equations, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                         }
+                 }
+         }
   }
   Trace("strings-check") << "Theory of strings, done check : " << e << std::endl;
   Trace("strings-process") << "Theory of strings, done check : " << e << std::endl;

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 8fa4345e53df6423c8d201e3747a9b34457f3d70..f303fd33368888c02789323004abcdb5ec04a55b 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -84,7 +84,8 @@ void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret
        }
 }
 
-Node StringsPreprocess::simplify( Node t ) {
+
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
     std::hash_map<TNode, Node, TNodeHashFunction>::const_iterator i = d_cache.find(t);
     if(i != d_cache.end()) {
       return (*i).second.isNull() ? t : (*i).second;
@@ -92,21 +93,39 @@ Node StringsPreprocess::simplify( Node t ) {
 
        if( t.getKind() == kind::STRING_IN_REGEXP ){
                // t0 in t1
+               Node t0 = simplify( t[0], new_nodes );
                //rewrite it
                std::vector< Node > ret;
-               simplifyRegExp( t[0], t[1], ret );
+               simplifyRegExp( t0, t[1], ret );
 
                Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
                d_cache[t] = (t == n) ? Node::null() : n;
                return n;
-    }else if( t.getNumChildren()>0 ){
+       }else if( t.getKind() == kind::STRING_SUBSTR ){
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" );
+               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" );
+               Node x = simplify( t[0], new_nodes );
+               Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL,
+                                                       NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x );
+               new_nodes.push_back( x_eq_123 );
+               Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
+               new_nodes.push_back( len_sk1_eq_i );
+               Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2],
+                                                               NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) );
+               new_nodes.push_back( len_sk2_eq_j );
+
+               d_cache[t] = sk2;
+               return sk2;
+       } else if( t.getNumChildren()>0 ){
                std::vector< Node > cc;
                if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
                        cc.push_back(t.getOperator());
                }
                bool changed = false;
                for( unsigned i=0; i<t.getNumChildren(); i++ ){
-                       Node tn = simplify( t[i] );
+                       Node tn = simplify( t[i], new_nodes );
                        cc.push_back( tn );
                        changed = changed || tn!=t[i];
                }
@@ -125,9 +144,11 @@ Node StringsPreprocess::simplify( Node t ) {
 }
 
 void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
+       std::vector< Node > new_nodes;
        for( unsigned i=0; i<vec_node.size(); i++ ){
-               vec_node[i] = simplify( vec_node[i] );
+               vec_node[i] = simplify( vec_node[i], new_nodes );
        }
+       vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() );
 }
 
 }/* CVC4::theory::strings namespace */

diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index f82a3cf247c5adcfb3db725a5aeb147513a7c17e..d07249a02a0edd3418cd3e6fd7d9c0e756862191 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -32,7 +32,7 @@ class StringsPreprocess {
        std::hash_map<TNode, Node, TNodeHashFunction> d_cache;
 private:
        void simplifyRegExp( Node s, Node r, std::vector< Node > &ret );
-       Node simplify( Node t );
+       Node simplify( Node t, std::vector< Node > &new_nodes );
 public:
 void simplify(std::vector< Node > &vec_node);
 };

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 412135675cde8d6cbab937d0b3eff05346a428a3..3a7ad1ee0cf0b0d5516c3c8925e2fafffc403998 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -137,7 +137,20 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                 retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
             }
         }
-    }
+    } else if(node.getKind() == kind::STRING_SUBSTR) {
+               if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) {
+                       int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+                       int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+                       if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
+                               retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+                       } else {
+                               // TODO: some issues, must be guarded by users
+                               retNode = NodeManager::currentNM()->mkConst( false );
+                       }
+               } else {
+                       //handled by preprocess
+               }
+       }
 
   Trace("strings-postrewrite") << "Strings::postRewrite returning " << node << std::endl;
   return RewriteResponse(REWRITE_DONE, retNode);

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 8fc6302069215128ca676a6d2e585c95391a6520..ef8f58f80a43de6af8b62d341bd3174d0545d11b 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -61,6 +61,28 @@ public:
   }
 };
 
+class StringSubstrTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+      throw (TypeCheckingExceptionPrivate, AssertionException) {
+    if( check ){
+        TypeNode t = n[0].getType(check);
+        if (!t.isString()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting string terms in substr");
+        }
+               t = n[1].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting start int terms in substr");
+        }
+               t = n[2].getType(check);
+        if (!t.isInteger()) {
+          throw TypeCheckingExceptionPrivate(n, "expecting length int terms in substr");
+        }
+    }
+    return nodeManager->stringType();
+  }
+};
+
 class RegExpConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)

diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 90872cf4df10a79e84372d5791e22efb3ec97d97..9b9fdef7a3dfac27773f3bf0778ca45ab07ebf62 100644 (file)
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -26,6 +26,7 @@ TESTS =       \
   str004.smt2 \
   str005.smt2 \
   model001.smt2 \
+  substr001.smt2 \
   loop001.smt2 \
   loop002.smt2 \
   loop003.smt2 \

diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2
new file mode 100644 (file)
index 0000000..b5ff587
--- /dev/null
+++ b/test/regress/regress0/strings/substr001.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_S)\r
+(set-info :status sat)\r
+\r
+(declare-fun x () String)\r
+(declare-fun i1 () Int)\r
+(declare-fun i2 () Int)\r
+(declare-fun i3 () Int)\r
+(declare-fun i4 () Int)\r
+\r
+(assert (= "efg" (str.sub x i1 i2) ) )\r
+(assert (= "bef" (str.sub x i3 i4) ) )\r
+(assert (> (str.len x) 5))\r
+\r
+(check-sat)\r