cleaned up FOR-construct parsing, and printing

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 8c51e89af38281e6c46cfef05c7f62091f4d347e..8cf5cbecfa80e2dc89ec02f7327d6b6375604a41 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
+ * AUTHORS: Vijay Ganesh
  *
  * BEGIN DATE: November, 2005
  *

diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp
index 6622c7683442293cea6b9c606728d6f6f7c736e6..aae364678dbfcc59191bead220441f7ff753b099 100644 (file)
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/AST/AbstractionRefinement.cpp
@@ -290,7 +290,7 @@ namespace BEEV
          //'value' for the same 'key'       
          (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
        } //end of While
-      }
+      } //end of recursion FORs
 
     ASTVec forloopFormulaVector;
     //Expand the leaf level FOR-construct completely
@@ -303,19 +303,20 @@ namespace BEEV
        
        //Check the currentformula against the model, and add it to the
        //SAT solver if it is false against the model
-       if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) {
-         forloopFormulaVector.push_back(currentFormula);
-         ASTNode forloopFormulas = 
-           (forloopFormulaVector.size() != 1) ?
-           CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0];
-               
-         SOLVER_RETURN_TYPE result = 
-           CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input);
-         if(result != SOLVER_UNDECIDED)             
-           {
-             return result;
-           }
-       }
+       if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) 
+         {
+           forloopFormulaVector.push_back(currentFormula);
+           ASTNode forloopFormulas = 
+             (forloopFormulaVector.size() != 1) ?
+             CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0];
+           
+           SOLVER_RETURN_TYPE result = 
+             CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input);
+           if(result != SOLVER_UNDECIDED)           
+             {
+               return result;
+             }
+         }
        
        //Update ParamToCurrentValMap with parameter and its current
        //value 
@@ -323,7 +324,8 @@ namespace BEEV
        //FIXME: Possible leak since I am not freeing the previous
        //'value' for the same 'key'
        (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
-      }
+      } //end of expanding the FOR loop
+    
     return SOLVER_UNDECIDED;
   } //end of the SATBased_FiniteLoop_Refinement()
 

diff --git a/src/AST/Makefile b/src/AST/Makefile
index fb3ebd16585c86eb490318af971422e0755876ed..b9bedad0d0169d6a555070c07be99881a56eb1ad 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -29,7 +29,7 @@ ASTKind.h ASTKind.cpp:        ASTKind.kinds genkinds.pl
 
 clean:
        rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#*
-       rm -rf printer/*.o
+       rm -rf printer/*.o printer/*~
 
 depend:
        makedepend -Y -- $(CFLAGS) -- $(SRCS)

diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp
index 73b22cbe9a9febcabaa2f6fc7d12b5005f1ab67c..7115ba3f275096821335b605affe75e18654cf8c 100644 (file)
--- a/src/AST/printer/AssortedPrinters.cpp
+++ b/src/AST/printer/AssortedPrinters.cpp
@@ -6,6 +6,7 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 // -*- c++ -*-
+
 #include "../AST.h"
 #include "AssortedPrinters.h"
 #include "printers.h"
@@ -14,7 +15,7 @@
 // to get the PRIu64 macro from inttypes, this needs to be defined.
 #define __STDC_FORMAT_MACROS
 #include <inttypes.h>
-#undef __STDC_FORMAT_MACROS
+//#undef __STDC_FORMAT_MACROS
 
 namespace BEEV
 {
@@ -172,7 +173,14 @@ namespace BEEV
           {
             os << "ASSERT( ";
             f.PL_Print(os,0);
-            os << " = ";
+           if(BOOLEAN_TYPE == f.GetType()) 
+             {
+             os << "<=>";
+             }
+           else 
+             {
+             os << " = ";
+             }
             if (BITVECTOR_TYPE == se.GetType())
               {
                 TermToConstTermUsingModel(se, false).PL_Print(os, 0);

diff --git a/src/AST/printer/AssortedPrinters.h b/src/AST/printer/AssortedPrinters.h
index bfaaef1eb2a5387004f5378b625a2f9afdf92fd7..c8871280d1ba36690f76751211a5dcbc623d0665 100644 (file)
--- a/src/AST/printer/AssortedPrinters.h
+++ b/src/AST/printer/AssortedPrinters.h
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
+ * AUTHORS: Vijay Ganesh
  *
  * BEGIN DATE: November, 2005
  *

diff --git a/src/AST/printer/CPrinter.cpp b/src/AST/printer/CPrinter.cpp
index f272b69b44dd52f9374e495df8e9a8cb7643387e..dfef1d8bdca0c6dd677ae0de9ba972f931e249ab 100644 (file)
--- a/src/AST/printer/CPrinter.cpp
+++ b/src/AST/printer/CPrinter.cpp
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #include "printers.h"
 #include <cassert>
 

diff --git a/src/AST/printer/LispPrinter.cpp b/src/AST/printer/LispPrinter.cpp
index 51bada56fac88b326c0814c6c5e2bb6ecc8862a7..ca49afe1573a4b05df203f24b8d77b429474c232 100644 (file)
--- a/src/AST/printer/LispPrinter.cpp
+++ b/src/AST/printer/LispPrinter.cpp
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #include "printers.h"
 
 namespace printer

diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp
index b76515be24bac82c6bcbd4c4f162d22e9bec56ba..2044c16069bcbb7f5dd13519d2f6e811a937171e 100644 (file)
--- a/src/AST/printer/PLPrinter.cpp
+++ b/src/AST/printer/PLPrinter.cpp
@@ -1,3 +1,12 @@
+// -*- c++ -*-
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+
 #include "printers.h"
 
 namespace printer
@@ -164,6 +173,19 @@ namespace printer
         PL_Print1(os, c[2], indentation, letize);
         os << endl << "ENDIF";
         break;
+      case FOR:
+       os << "FOR(";
+       PL_Print1(os, c[0], indentation, letize);
+       os << ";";
+       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);
+       os << "} \n";
+       break;
       case BVLT:
       case BVLE:
       case BVGT:

diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp
index 15ca41e643e868bd975d0bb52d711ca3feafbafe..1839e58b08825aa84c08a0cb8022b16054140e6a 100644 (file)
--- a/src/AST/printer/SMTLIBPrinter.cpp
+++ b/src/AST/printer/SMTLIBPrinter.cpp
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #include "printers.h"
 #include <cassert>
 

diff --git a/src/AST/printer/dotPrinter.cpp b/src/AST/printer/dotPrinter.cpp
index b2b24a0b24361fe806a69e7df1e4744a85961a22..1fdb0b701023bd5a65c916926870880fb1777e90 100644 (file)
--- a/src/AST/printer/dotPrinter.cpp
+++ b/src/AST/printer/dotPrinter.cpp
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #include "printers.h"
 
 /*

diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h
index 46c1e4f549b26d3e867cb3df4b1cbc97f01abbf3..06815f285d0918a4968e9fb0e8ae9cd15078e108 100644 (file)
--- a/src/AST/printer/printers.h
+++ b/src/AST/printer/printers.h
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #ifndef PRINTERS_H_
 #define PRINTERS_H_
 

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 15b068dc00fc145d28e234bac27483fb5fb60814..293dc3cfb19ddbcfbab5f81ceb7d1907a5db5383 100644 (file)
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -442,21 +442,35 @@ Formula           :     '(' Formula ')' { $$ = $2; }
                         delete $1;
                         delete $3;
                       }
-                |      FOR_TOK '(' Formula ';' Formula ';' Formula ')' '{' Formula '}'
+                |      FOR_TOK '(' TERMID_TOK ';' BVCONST_TOK ';' BVCONST_TOK ';' BVCONST_TOK ')' '{' Formula '}'
                        {
                         //Allows a compact representation of
-                        //parameterized set of formulas
+                        //parameterized set of formulas (bounded
+                        //universal quantification)
                         //
-                        //$1 is the initialization (this is an AND of
-                        //formulas of the form var = constant)
+                        //parameter name (a variable)
                         //
-                        //$2 is the constant bounding (this is an AND
-                        //of formulas of the form var < constant).
+                        //initial value (BVCONST)
                         //
-                        //$3 is the increment (this is an AND of
-                        //formulas of the form var = var + constant).
+                        //limit value (BVCONST)
                         //
-                        //$4 is the parameterized formula
+                        //increment value (BVCONST)
+                        //
+                        //formula (it can be a nested forloop)
+                        BEEV::ASTVec vec;
+                        vec.push_back(*$3);
+                        vec.push_back(*$5);
+                        vec.push_back(*$7);
+                        vec.push_back(*$9);
+                        vec.push_back(*$12);
+                        BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FOR,vec));
+                        BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+                        $$ = n;
+                        delete $3;
+                        delete $5;
+                        delete $7;
+                        delete $9;
+                        delete $12;
                       }
                |      NOT_TOK Formula 
                        {