From 7c8c0afea84b42cb04c15727aa8d806c86f90621 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Sep 2009 00:26:29 +0000
Subject: [PATCH] minor edits

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@200 e59a4935-1847-0410-ae03-e826735625c1
---
 clean-install.sh         |  1 -
 src/parser/CVC.y         | 23 ++++++++++++++---------
 src/parser/let-funcs.cpp |  2 +-
 3 files changed, 15 insertions(+), 11 deletions(-)

diff --git a/clean-install.sh b/clean-install.sh
index 6dfebb9..2b948c4 100755
--- a/clean-install.sh
+++ b/clean-install.sh
@@ -19,6 +19,5 @@ done
 
 ./scripts/configure --with-prefix=$PREFIX
 make clean
-make
 make install
 
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 080a4fe..fc35e6d 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -156,7 +156,7 @@
 
 %type <vec>  Exprs FORM_IDs reverseFORM_IDs
 %type <vec>  Asserts 
-%type <node> Expr Formula IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr
+%type <node> Expr Formula ForDecl IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr
 %type <Index_To_UpdateValue> Updates
 
 %type <indexvaluewidth>  BvType BoolType ArrayType Type 
@@ -334,6 +334,14 @@ FORM_IDs         :     reverseFORM_IDs
                       }
                 ;
 
+ForDecl         :      FORMID_TOK ':' Type
+                      {
+			$1->SetIndexWidth($3.indexwidth);
+			$1->SetValueWidth($3.valuewidth);
+			_parser_symbol_table.insert(*$1);
+			$$ = $1;			
+		      }
+
 /* Grammar for Types */
 Type		:      BvType { $$ = $1; }
                 |      BoolType { $$ = $1; }
@@ -443,7 +451,7 @@ Formula		:     '(' Formula ')' { $$ = $2; }
 			 delete $1;
 			 delete $3;
 		       }
-                |      FOR_TOK '(' FORMID_TOK ':' Type ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
+                |      FOR_TOK '(' ForDecl ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
                        {
 			 //Allows a compact representation of
 			 //parameterized set of formulas (bounded
@@ -458,24 +466,21 @@ Formula		:     '(' Formula ')' { $$ = $2; }
 			 //increment value (BVCONST)
 			 //
 			 //formula (it can be a nested forloop)			 
-			 $3->SetIndexWidth($5.indexwidth);
-			 $3->SetValueWidth($5.valuewidth);
-			 _parser_symbol_table.insert(*$3);
 			   
 			 ASTVec vec;
 			 vec.push_back(*$3);
+			 vec.push_back(*$5);
 			 vec.push_back(*$7);
 			 vec.push_back(*$9);
-			 vec.push_back(*$11);
-			 vec.push_back(*$14);
+			 vec.push_back(*$12);
 			 ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec));
 			 GlobalBeevMgr->BVTypeCheck(*n);
 			 $$ = n;
 			 delete $3;
+			 delete $5;
 			 delete $7;
 			 delete $9;
-			 delete $11;
-			 delete $14;
+			 delete $12;
 		       }
 		|      NOT_TOK Formula 
                        {
diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index 4699af9..fc45b30 100644
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -29,7 +29,7 @@ namespace BEEV {
     ASTNodeMap::iterator it;
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
-      FatalError("LetExprMgr:The LET-var v has already been defined"\ 
+      FatalError("LetExprMgr:The LET-var v has already been defined"\
 		 "in this LET scope: v =", var);
     }
 
-- 
2.47.3