From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 30 Apr 2014 01:57:16 +0000 (-0400)
Subject: Fix warnings, cleanup in strings typechecker.
X-Git-Tag: cvc5-1.0.0~6941
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=221e509c0eb230aa549fe0107ba88514b6944ca2;p=cvc5.git

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 9ffe9150d..6d3a12cc4 100644
--- 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");