Fix warnings, cleanup in strings typechecker.

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 9ffe9150dce9739678af6ff761561bbd8507cb57..6d3a12cc4ed9bcc4bdb564c7b89ab3c9982a7a9d 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -306,9 +306,7 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      TypeNode t = (*it).getType(check);
+      TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
@@ -322,9 +320,7 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      TypeNode t = (*it).getType(check);
+      TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
@@ -338,9 +334,7 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      TypeNode t = (*it).getType(check);
+      TypeNode t = n[0].getType(check);
       if (!t.isRegExp()) {
         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
       }
@@ -355,7 +349,6 @@ public:
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
       char ch[2];
 
       for(int i=0; i<2; ++i) {
@@ -421,9 +414,7 @@ public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      TypeNode t = (*it).getType(check);
+      TypeNode t = n[0].getType(check);
       if (!t.isString()) {
         throw TypeCheckingExceptionPrivate(n, "expecting string terms");
       }
@@ -441,7 +432,6 @@ public:
       throw (TypeCheckingExceptionPrivate, AssertionException) {
     if( check ) {
       TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
       TypeNode t = (*it).getType(check);
       if (!t.isString()) {
         throw TypeCheckingExceptionPrivate(n, "expecting string terms");