partial function charat

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d97c070637e9c76174fa2797bfd3bcf2c471fb19..0afe29ccc11c96c29c28c9fc9fd2a5d9740c1d89 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -278,6 +278,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::STRING_CONCAT: out << "str.++ "; break;
   case kind::STRING_IN_REGEXP: out << "str.in.re "; break;
   case kind::STRING_LENGTH: out << "str.len "; break;
+  case kind::STRING_SUBSTR_TOTAL:
   case kind::STRING_SUBSTR: out << "str.substr "; break;
   case kind::STRING_CHARAT: out << "str.at "; break;
   case kind::STRING_STRCTN: out << "str.contain "; break;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0b4fe80c5a00d79e6466cbf410979c2935e1bbd1..367f3fe4f11a0fc3bf4841b0aad9601982578fca 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1785,17 +1785,18 @@ bool TheoryStrings::checkSimple() {
                                                                //add lemma
                                                                lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst<String>().size() ) );
                                                        } else if( n.getKind() == kind::STRING_SUBSTR_TOTAL ) {
-                                                               lsum = n[2];/*
-                                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
-                                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
-                                                               d_statistics.d_new_skolems += 2;
                                                                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::GEQ, n[2], d_zero);
-                                                               Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ));
                                                                Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 ));
+                                                               lsum = NodeManager::currentNM()->mkNode( kind::ITE, cond, n[2], d_zero );
+                                                               /*
+                                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "st1_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+                                                               Node sk3 = NodeManager::currentNM()->mkSkolem( "st3_$$", NodeManager::currentNM()->stringType(), "created for substr" );
+                                                               d_statistics.d_new_skolems += 2;
+                                                               Node x_eq_123 = n[0].eqNode(NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk, sk3 ));
                                                                Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, n[1],
                                                                                                                NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) );
                                                                Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i );

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 1e2eb2572b027d2b2f5851e19b8d7d1519934e5a..7bdacb92daeccc948677b48b38afde881777ee16 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -180,8 +180,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                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 len_uf_eq_j = t[2].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, uf ) );
-               Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, 
-                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i )) );
+               Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, 
+                                               NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ),
+                                               t.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") )) ));
                new_nodes.push_back( lemma );
                retNode = t;
                d_cache[t] = t;

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index b0899492700b5241034237cc38009ec4bfec748d..84f58a16d993cb333c37ad719845f7bf4df3059e 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -323,15 +323,15 @@ 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_TOTAL) {
+        } /*else if(node[0].getKind() == kind::STRING_SUBSTR_TOTAL) {
             retNode = node[0][2];
-        } else if(node[0].getKind() == kind::STRING_CONCAT) {
+        }*/ else if(node[0].getKind() == kind::STRING_CONCAT) {
             Node tmpNode = rewriteConcatString(node[0]);
             if(tmpNode.isConst()) {
                 retNode = NodeManager::currentNM()->mkConst( ::CVC4::Rational( tmpNode.getConst<String>().size() ) );
-            } else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
+            } /*else if(tmpNode.getKind() == kind::STRING_SUBSTR_TOTAL) {
                                retNode = tmpNode[2];
-            } else {
+            }*/ else {
                 // it has to be string concat
                 std::vector<Node> node_vec;
                 for(unsigned int i=0; i<tmpNode.getNumChildren(); ++i) {
@@ -353,8 +353,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) {
                } else 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) ) {
+                       if( node[0].getConst<String>().size() >= (unsigned) (i + j) && i>=0 && j>=0 ) {
                                retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+                       } else {
+                               retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
                        }
                }
        } else if(node.getKind() == kind::STRING_STRCTN) {