minor edits

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@200 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/clean-install.sh b/clean-install.sh
index 6dfebb9ace6aab7a489888661802e8e5752939d3..2b948c4ad5b9b17f4671ea444ff8a2b46d1676a9 100755 (executable)
--- 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 080a4feaf452442e0af5ac1152dad79f1a0f4b7e..fc35e6d0e26e84a93a17b3fcb730b404b5478314 100644 (file)
--- 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 4699af9c51f6eeb325170949ec57f53e8e1c527d..fc45b30fb2ca7b44a48b0776b9f686b94b907e52 100644 (file)
--- 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);
     }