changed regressall to regresscvc

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

diff --git a/INSTALL b/INSTALL
index c19d047d927cfa50502a016f623247dc91b5316b..d869acb57d1ae7247d7e01c6300ffa9820fbcb0d 100644 (file)
--- a/INSTALL
+++ b/INSTALL
@@ -22,7 +22,7 @@
 
 3. Run tests:
 
-   make regressall
+   make regresscvc
 
 NB: 
 

diff --git a/README b/README
index ab02b5c148e9f6888beb8810715e7287dcf44598..b3582e26e461612cdf7ffe4325cfab4718b8417b 100644 (file)
--- a/README
+++ b/README
@@ -43,7 +43,7 @@ REGRESSIONS
 
 Assumes you have downloaded the testcases
 
-make regressall
+make regresscvc
 make regress_smt
 make regress_c_api
 make regressbigarray
\ No newline at end of file

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 1f769ca82a41657dd16417f2bd0831afd12fc151..6c8beaa95ae7542ed62b9dd6ec8cbc613cf88b73 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -77,7 +77,7 @@ REGRESS_LOG = `date +%Y-%m-%d`"-regress-cvc.log"
 PROGNAME=bin/stp
 ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
 
-.PHONY: regressall
+.PHONY: regresscvc
 regressall:
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)

diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index c4d3ab623fe29ca5d20dc0c76dccd6208e1d2efd..72d7d03d0addcc4cfebe0442aea31d8be20bae01 100644 (file)
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -802,7 +802,7 @@ namespace BEEV
             break;
             //case BVVARSHIFT:
             //case BVSRSHIFT:
-            break;
+            //break;
           default:
             break;
           }

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 49cdf64c1e4766936623593d7b27f6f8eff79275..89646e1de5114d12a931c4c948ed61ce5008f48e 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -253,14 +253,15 @@ namespace BEEV
           result = bm.CreateNode(k, vec);
           break;
         }
+      case FOR:
       default:
         if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
           result = simpleForm;
         else
           {
+            FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k);
             cerr << "The input is: " << simpleForm << endl;
             cerr << "The valuewidth of input is : " << simpleForm.GetValueWidth() << endl;
-            FatalError("TransformFormula: Illegal kind: ", bm.CreateNode(UNDEFINED), k);
           }
         break;
       }

diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp
index 2044c16069bcbb7f5dd13519d2f6e811a937171e..8bb759805b72bf6da80265e9f8c9815ebf09a402 100644 (file)
--- a/src/AST/printer/PLPrinter.cpp
+++ b/src/AST/printer/PLPrinter.cpp
@@ -180,10 +180,8 @@ namespace printer
        PL_Print1(os, c[1], indentation, letize);
        os << ";";
        PL_Print1(os, c[2], indentation, letize);
-       os << ";";
-       PL_Print1(os, c[3], indentation, letize);
        os << "){ \n";
-       PL_Print1(os, c[4], indentation, letize);
+       PL_Print1(os, c[3], indentation, letize);
        os << "} \n";
        break;
       case BVLT:

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index af3439ace5a0700a43126f766dc321231ce11c77..42ff10b35fa23b78b4eefd35c3998950a831eff4 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -271,10 +271,6 @@ VarDecl            :      FORM_IDs ':' Type
                           _parser_symbol_table.insert(*i);
                           i->SetIndexWidth($3.indexwidth);
                           i->SetValueWidth($3.valuewidth);
-
-                          //FIXME: HACK_ATTACK. this vector was hacked into the code to
-                          //support a special request by Dawson' group. They want the
-                          //counterexample to be printed in the order of variables declared.
                           GlobalBeevMgr->ListOfDeclaredVars.push_back(*i);
                         }
                         delete $1;
@@ -447,7 +443,7 @@ Formula             :     '(' Formula ')' { $$ = $2; }
                         delete $1;
                         delete $3;
                       }
-                |      FOR_TOK '(' TERMID_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
+                |      FOR_TOK '(' FORMID_TOK ':' Type ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
                        {
                         //Allows a compact representation of
                         //parameterized set of formulas (bounded
@@ -462,20 +458,24 @@ Formula           :     '(' Formula ')' { $$ = $2; }
                         //increment value (BVCONST)
                         //
                         //formula (it can be a nested forloop)
+                        _parser_symbol_table.insert(*$3);
+                        $3->SetIndexWidth($5.indexwidth);
+                        $3->SetValueWidth($5.valuewidth);
+                          
                         ASTVec vec;
                         vec.push_back(*$3);
-                        vec.push_back(*$5);
                         vec.push_back(*$7);
                         vec.push_back(*$9);
-                        vec.push_back(*$12);
+                        vec.push_back(*$11);
+                        vec.push_back(*$14);
                         ASTNode * n = new ASTNode(GlobalBeevMgr->CreateNode(FOR,vec));
                         GlobalBeevMgr->BVTypeCheck(*n);
                         $$ = n;
                         delete $3;
-                        delete $5;
                         delete $7;
                         delete $9;
-                        delete $12;
+                        delete $11;
+                        delete $14;
                       }
                |      NOT_TOK Formula 
                        {

diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index 0f65e21ccefe170736e63dae7bda314c06c97b58..63f5a780adf7e05e22e46f20e3e5c833a4dda427 100644 (file)
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -37,7 +37,7 @@ namespace BEEV {
     }
 
     (*_letid_expr_map)[var] = letExpr;   
-  }
+  }//end of LetExprMgr()
 
   //this function looksup the "var to letexpr map" and returns the
   //corresponding letexpr. if there is no letexpr, then it simply
@@ -57,10 +57,10 @@ namespace BEEV {
     ASTNodeMap::iterator it;
     if((it =_letid_expr_map->find(v)) != _letid_expr_map->end()) {
       if(it->second == ASTUndefined) 
-        FatalError("Unresolved Identifier: ",v);
+        FatalError("ResolveID :: Unresolved Identifier: ",v);
       else
         return it->second;
-    }
+    }//end of ResolveID()
 
     //this is to mark the let-var as undefined. the let var is defined
     //only after the LetExprMgr has completed its work, and until then
@@ -75,7 +75,6 @@ namespace BEEV {
   
   // This function simply cleans up the LetID -> LetExpr Map.   
   void BeevMgr::CleanupLetIDMap(void) { 
-
     // ext/hash_map::clear() is very expensive on big empty lists. shortcut. 
     if (_letid_expr_map->size()  ==0)
       return;
@@ -94,10 +93,10 @@ namespace BEEV {
     delete _letid_expr_map;
     _letid_expr_map = new ASTNodeMap();
 
-  }
+  }//end of CleanupLetIDMap()
 
   void BeevMgr::InitializeLetIDMap(void)
   {
     _letid_expr_map = new ASTNodeMap();
-  }
+  } //end of InitializeLetIDMap()
 };

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index c53a1ef33941d73b3752d86d1659da6fb666f80d..aeea77b9f26c850709738d8e74daee9f21b7ac35 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -46,7 +46,11 @@ namespace BEEV
 
     if (pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end())
       {
-        output = (ASTFalse == it->second) ? ASTTrue : (ASTTrue == it->second) ? ASTFalse : CreateNode(NOT, it->second);
+        output = 
+         (ASTFalse == it->second) ? 
+         ASTTrue : 
+         (ASTTrue == it->second) ? 
+         ASTFalse : CreateNode(NOT, it->second);
         CountersAndStats("2nd_Successful_CheckSimplifyMap");
         return true;
       }