minor fix

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b1e37f85e72d3fd264cb6961e00a27e41ab57ec4..cf24ae82c05fdf4e1a33b5aa5b22a96a92eec125 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1252,8 +1252,8 @@ 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; }
-//  | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
-//  | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
+  | STRCTN_TOK     { $kind = CVC4::kind::STRING_STRCTN; }
+  | STRCAT_TOK     { $kind = CVC4::kind::STRING_CHARAT; }
   | STRINRE_TOK    { $kind = CVC4::kind::STRING_IN_REGEXP; }
   | STRTORE_TOK    { $kind = CVC4::kind::STRING_TO_REGEXP; }
   | RECON_TOK      { $kind = CVC4::kind::REGEXP_CONCAT; }

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index 355b182c91c9ba749228e2b0f0ebe0effd5fbded..111c4f51d1513fab049103287b5321be333d357e 100644 (file)
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -144,18 +144,21 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
                        std::vector< Node > or_vec;
                        or_vec.push_back( w.eqNode(y) );
                        Node x1 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+                       Node b1 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x1 );
+                       Node c1 = NodeManager::currentNM()->mkNode( kind::EXISTS, b1, NodeManager::currentNM()->mkNode( kind::AND,
                                                        x1.eqNode( emptyString ).negate(),
                                                        w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x1, y ) )));
                        or_vec.push_back( c1 );
                        Node z2 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+                       Node b2 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, z2 );
+                       Node c2 = NodeManager::currentNM()->mkNode( kind::EXISTS, b2, NodeManager::currentNM()->mkNode( kind::AND,
                                                        z2.eqNode( emptyString ).negate(),
                                                        w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, y, z2 ) )));
                        or_vec.push_back( c2 );
                        Node x3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
                        Node z3 = NodeManager::currentNM()->mkBoundVar( t[0].getType() );
-                       Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, NodeManager::currentNM()->mkNode( kind::AND,
+                       Node b3 = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, x3, z3 );
+                       Node c3 = NodeManager::currentNM()->mkNode( kind::EXISTS, b3, NodeManager::currentNM()->mkNode( kind::AND,
                                                        x3.eqNode( emptyString ).negate(), z3.eqNode( emptyString ).negate(),
                                                        w.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, x3, y, z3 ) )));
                        or_vec.push_back( c3 );

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index df9d29f0f218e8af8b15f2f0d749e57551d19a25..9d3197517fa958967a97646c01a45e731516bec9 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -57,9 +57,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-               if(n.getNumChildren() != 1) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 1 term in string length");
-               }
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
@@ -74,9 +71,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-               if(n.getNumChildren() != 3) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 3 terms in substr");
-               }
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
@@ -99,9 +93,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-               if(n.getNumChildren() != 2) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string contain");
-               }
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
@@ -111,7 +102,7 @@ public:
           throw TypeCheckingExceptionPrivate(n, "expecting a target string term in string contain");
         }
     }
-    return nodeManager->stringType();
+    return nodeManager->booleanType();
   }
 };
 
@@ -120,9 +111,6 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ){
-               if(n.getNumChildren() != 2) {
-          throw TypeCheckingExceptionPrivate(n, "expecting 2 terms in string char at");
-               }
         TypeNode t = n[0].getType(check);
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at");