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 48381364ee07abe7267af66f7b623241f4accdbd..b91329f58bada09583158bc369e64cab81cac898 100644 (file)
--- 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 0842935c2f7c83534b6a2907f44baabcacabdbc4..354ee49b036a027d83167c311cd403ff8f3ca3c4 100644 (file)
--- 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 594a19a7a45c5896d12a739f2ddecf424fab875b..b9cb95a1bd8988154e49c13a5addb11838efb67b 100644 (file)
--- 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 90cdae10ddac264854551b1811b66d7cb9a9f6c8..2c49432750807206f2ac52536e7bcd9f65db8226 100644 (file)
--- 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 75bb548fc953638a9c819950cf6b5bd30cbd2781..807d5f3329839b3197218a925ad167f26ab3587b 100644 (file)
--- 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 171cf24a51d90cc924d4f70069a534dde1ae94da..db20a16dddac2c958b184ae5936d5d199de81f4d 100644 (file)
--- 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 e532ebafad93ff38ab1c5f25adefb1e381017b15..9727ff39dbf4af2907d1ccadb89d5a8c8f0a2ea6 100644 (file)
--- 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;      
     }   
 ;