From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 6 Oct 2009 01:16:35 +0000 (+0000)
Subject: moved all LET-variables related stuff into a separate class
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2fb6b88185201540f66f00b630a7dca65dfe0a96;p=francis%2Fstp.git

moved all LET-variables related stuff into a separate class

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

diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp
index 4838136..b91329f 100644
--- a/src/AST/ASTNode.cpp
+++ b/src/AST/ASTNode.cpp
@@ -244,9 +244,8 @@ namespace BEEV
                 /* If for some reason the variable being created here is
                  * already declared by the user then the printed output will
                  * not be a legal input to the system. too bad. I refuse to
-                 * check for this.  [Vijay is the author of this comment.]
+                 * check for this.
                  */
-
                 bm->NodeLetVarMap[ccc] = CurrentSymbol;
                 std::pair<ASTNode, ASTNode> node_letvar_pair(CurrentSymbol, ccc);
                 bm->NodeLetVarVec.push_back(node_letvar_pair);
diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp
index 0842935..354ee49 100644
--- a/src/STPManager/STPManager.cpp
+++ b/src/STPManager/STPManager.cpp
@@ -371,6 +371,63 @@ namespace BEEV
       return true;
   }
 
+  // Create and return an ASTNode for a term
+  ASTNode BeevMgr::CreateTerm(Kind kind, 
+			      unsigned int width, 
+			      const ASTVec &children)
+  {
+    if (!is_Term_kind(kind))
+      FatalError("CreateTerm:  Illegal kind to CreateTerm:", 
+		 ASTUndefined, kind);
+    ASTNode n = CreateNode(kind, children);
+    n.SetValueWidth(width);
+    
+    //by default we assume that the term is a Bitvector. If
+    //necessary the indexwidth can be changed later
+    n.SetIndexWidth(0);
+    return n;
+  }
+
+  ASTNode BeevMgr::CreateTerm(Kind kind, 
+			      unsigned int width, 
+			      const ASTNode& child0, 
+			      const ASTVec &children)
+  {
+    if (!is_Term_kind(kind))
+      FatalError("CreateTerm:  Illegal kind to CreateTerm:", ASTUndefined, kind);
+      ASTNode n = CreateNode(kind, child0, children);
+      n.SetValueWidth(width);
+      return n;
+  }
+
+  ASTNode BeevMgr::CreateTerm(Kind kind, 
+			      unsigned int width, 
+			      const ASTNode& child0,
+			      const ASTNode& child1, 
+			      const ASTVec &children)
+  {
+    if (!is_Term_kind(kind))
+      FatalError("CreateTerm:  Illegal kind to CreateTerm:", ASTUndefined, kind);
+    ASTNode n = CreateNode(kind, child0, child1, children);
+    n.SetValueWidth(width);
+    return n;
+  }
+  
+  ASTNode BeevMgr::CreateTerm(Kind kind,
+			      unsigned int width,
+			      const ASTNode& child0,
+			      const ASTNode& child1,
+			      const ASTNode& child2,
+			      const ASTVec &children)
+  {
+    if (!is_Term_kind(kind))
+      FatalError("CreateTerm:  Illegal kind to CreateTerm:", ASTUndefined, kind);
+    ASTNode n = CreateNode(kind, child0, child1, child2, children);
+    n.SetValueWidth(width);
+    return n;
+  }
+
+
   ////////////////////////////////////////////////////////////////
   //
   //  IO manipulators for Lisp format printing of AST.
@@ -827,8 +884,6 @@ namespace BEEV
     _arrayread_ite.clear();
     _arrayread_symbol.clear();
     _introduced_symbols.clear();
-    //TransformMap.clear();
-    _letid_expr_map->clear();
     CounterExampleMap.clear();
     ComputeFormulaMap.clear();
     StatInfoSet.clear();
@@ -874,7 +929,6 @@ namespace BEEV
     _arrayread_ite.clear();
     _arrayread_symbol.clear();
     _introduced_symbols.clear();
-    _letid_expr_map->clear();
     CounterExampleMap.clear();
     ComputeFormulaMap.clear();
     StatInfoSet.clear();
@@ -954,7 +1008,6 @@ namespace BEEV
 
     delete SimplifyMap;
     delete SimplifyNegMap;
-    delete _letid_expr_map;
     delete ReferenceCount;
   }
 
diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex
index 594a19a..b9cb95a 100644
--- a/src/parser/CVC.lex
+++ b/src/parser/CVC.lex
@@ -124,7 +124,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting
   // the whole grammar to eliminate the term/formula distinction.  
-  cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->ResolveID(nptr));
+  cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->GetLetMgr()->ResolveID(nptr));
   //cvclval.node = new BEEV::ASTNode(nptr);
   if ((cvclval.node)->GetType() == BOOLEAN_TYPE)
     return FORMID_TOK;
diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 90cdae1..2c49432 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -291,7 +291,7 @@ VarDecl		:      FORM_IDs ':' Type
 			   i->SetValueWidth($5->GetValueWidth());
 			   i->SetIndexWidth($5->GetIndexWidth());
 			   
-			   GlobalBeevMgr->LetExprMgr(*i,*$5);
+			   GlobalBeevMgr->GetLetMgr()->LetExprMgr(*i,*$5);
 			   delete $5;
 			 }
 		       }
@@ -309,7 +309,7 @@ VarDecl		:      FORM_IDs ':' Type
 			   i->SetValueWidth($5->GetValueWidth());
 			   i->SetIndexWidth($5->GetIndexWidth());
 			   
-			   GlobalBeevMgr->LetExprMgr(*i,*$5);
+			   GlobalBeevMgr->GetLetMgr()->LetExprMgr(*i,*$5);
 			   delete $5;
 			 }
 		       }                
@@ -424,7 +424,7 @@ Formula		:     '(' Formula ')'
 		       }
 		|      FORMID_TOK 
                        {  
-			 $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1;
+			 $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1)); delete $1;
 		       }
 		|      FORMID_TOK '(' Expr ')' 
                        {
@@ -659,7 +659,7 @@ Formula		:     '(' Formula ')'
                        {
 			 $$ = $4;
 			 //Cleanup the LetIDToExprMap
-			 GlobalBeevMgr->CleanupLetIDMap();
+			 GlobalBeevMgr->GetLetMgr()->CleanupLetIDMap();
 		       }
                 ;
 
@@ -701,7 +701,7 @@ Exprs		:      Expr
 		;
 
 /* Grammar for Expr */
-Expr		:      TERMID_TOK { $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); delete $1;}
+Expr		:      TERMID_TOK { $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1)); delete $1;}
                 |      '(' Expr ')' { $$ = $2; }
 	        |      BVCONST_TOK { $$ = $1; }
                 |      BOOL_TO_BV_TOK '(' Formula ')'		
@@ -1036,7 +1036,7 @@ LetDecl		:	FORMID_TOK '=' Expr
 			  //
 			  //2. Ensure that LET variables are not
 			  //2. defined more than once
-			  GlobalBeevMgr->LetExprMgr(*$1,*$3);
+			  GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$1,*$3);
 			  delete $1;
 			  delete $3;
 			}
@@ -1054,7 +1054,7 @@ LetDecl		:	FORMID_TOK '=' Expr
 			  $1->SetValueWidth($5->GetValueWidth());
 			  $1->SetIndexWidth($5->GetIndexWidth());
 
-			  GlobalBeevMgr->LetExprMgr(*$1,*$5);
+			  GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$1,*$5);
 			  delete $1;
 			  delete $5;
 			}
@@ -1068,7 +1068,7 @@ LetDecl		:	FORMID_TOK '=' Expr
 			  $1->SetIndexWidth($3->GetIndexWidth());
 
 			  //Do LET-expr management
-			  GlobalBeevMgr->LetExprMgr(*$1,*$3);
+			  GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$1,*$3);
 			  delete $1;
 			  delete $3;
 			}
@@ -1087,7 +1087,7 @@ LetDecl		:	FORMID_TOK '=' Expr
 			  $1->SetIndexWidth($5->GetIndexWidth());
 
 			  //Do LET-expr management
-			  GlobalBeevMgr->LetExprMgr(*$1,*$5);
+			  GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$1,*$5);
 			  delete $1;
 			  delete $5;
 			}                
diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index 75bb548..807d5f3 100644
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -8,8 +8,7 @@
  ********************************************************************/
 
 #include <stdlib.h>
-#include "../AST/AST.h"
-#include "../STPManager/STPManager.h"
+#include "let-funcs.h"
 
 namespace BEEV {
   //external parser table for declared symbols. Only symbols which are
@@ -26,7 +25,8 @@ namespace BEEV {
   //2. the function returns an error
   //
   //3. otherwise add the <var,letExpr> pair to the _letid_expr table.
-  void BeevMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) {
+  void LETMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) 
+  {
     ASTNodeMap::iterator it;
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
@@ -45,7 +45,8 @@ namespace BEEV {
   //this function looksup the "var to letexpr map" and returns the
   //corresponding letexpr. if there is no letexpr, then it simply
   //returns the var.
-  ASTNode BeevMgr::ResolveID(const ASTNode& v) {
+  ASTNode LETMgr::ResolveID(const ASTNode& v) 
+  {
     if (_letid_expr_map == NULL)
       InitializeLetIDMap();
 
@@ -74,10 +75,11 @@ namespace BEEV {
     //rid of this hack.
     (*_letid_expr_map)[v] = ASTUndefined;
     return v;    
-  }
+  }//End of ResolveID()
   
   // This function simply cleans up the LetID -> LetExpr Map.   
-  void BeevMgr::CleanupLetIDMap(void) { 
+  void LETMgr::CleanupLetIDMap(void) 
+  { 
     // ext/hash_map::clear() is very expensive on big empty lists. shortcut. 
     if (_letid_expr_map->size()  ==0)
       return;
@@ -95,10 +97,9 @@ namespace BEEV {
     // May contain lots of buckets, so reset.
     delete _letid_expr_map;
     _letid_expr_map = new ASTNodeMap();
-
   }//end of CleanupLetIDMap()
 
-  void BeevMgr::InitializeLetIDMap(void)
+  void LETMgr::InitializeLetIDMap(void)
   {
     _letid_expr_map = new ASTNodeMap();
   } //end of InitializeLetIDMap()
diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex
index 171cf24..db20a16 100644
--- a/src/parser/smtlib.lex
+++ b/src/parser/smtlib.lex
@@ -220,7 +220,7 @@ bit{DIGIT}+     {
   // Check valuesize to see if it's a prop var.  I don't like doing
   // type determination in the lexer, but it's easier than rewriting
   // the whole grammar to eliminate the term/formula distinction.  
-  smtlval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->ResolveID(nptr));
+  smtlval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->GetLetMgr()->ResolveID(nptr));
   //smtlval.node = new BEEV::ASTNode(nptr);
   if ((smtlval.node)->GetType() == BOOLEAN_TYPE)
     return FORMID_TOK;
diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y
index e532eba..9727ff3 100644
--- a/src/parser/smtlib.y
+++ b/src/parser/smtlib.y
@@ -625,7 +625,7 @@ an_formula:
     {
       $$ = $2;
       //Cleanup the LetIDToExprMap
-      GlobalBeevMgr->CleanupLetIDMap();			 
+      GlobalBeevMgr->GetLetMgr()->CleanupLetIDMap();			 
     }
 ;
 
@@ -647,7 +647,7 @@ letexpr_mgmt:
       //
       //2. Ensure that LET variables are not
       //2. defined more than once
-      GlobalBeevMgr->LetExprMgr(*$5,*$6);
+      GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$5,*$6);
       delete $5;
       delete $6;      
    }
@@ -661,7 +661,7 @@ letexpr_mgmt:
      $5->SetIndexWidth($6->GetIndexWidth());
      
      //Do LET-expr management
-     GlobalBeevMgr->LetExprMgr(*$5,*$6);
+     GlobalBeevMgr->GetLetMgr()->LetExprMgr(*$5,*$6);
      delete $5;
      delete $6;     
    }
@@ -703,7 +703,7 @@ an_nonbvconst_term:
     BITCONST_TOK { $$ = $1; }
   | var
     {
-      $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1));
+      $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1));
       delete $1;
     }
   | LPAREN_TOK an_term RPAREN_TOK
@@ -1136,12 +1136,12 @@ sort_symb:
 var:
     FORMID_TOK 
     {
-      $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); 
+      $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1)); 
       delete $1;      
     }
    | TERMID_TOK
     {
-      $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1));
+      $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1));
       delete $1;
     }
    | QUESTION_TOK TERMID_TOK
@@ -1157,7 +1157,7 @@ fvar:
     }
   | FORMID_TOK
     {
-      $$ = new ASTNode(GlobalBeevMgr->ResolveID(*$1)); 
+      $$ = new ASTNode(GlobalBeevMgr->GetLetMgr()->ResolveID(*$1)); 
       delete $1;      
     }   
 ;