added cleartables for each of the big classes

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

diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h
index ca6f111b561071590482d38e07741781f7e96bb9..97b7775727acae432ca04fb7943ce1db3ce3390e 100644 (file)
--- a/src/AST/ArrayTransformer.h
+++ b/src/AST/ArrayTransformer.h
@@ -174,6 +174,14 @@ namespace BEEV
       return false;
     } // End of IntroduceSymbolSet
 
+    void ClearAllTables(void)
+    {
+      Arrayname_ReadindicesMap->clear();
+      Arrayread_SymbolMap.clear();
+      Arrayread_IteMap->clear();
+      Introduced_SymbolsSet.clear();
+      TransformMap->clear();
+    }
   }; //end of class Transformer
 
 };//end of namespace

diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h
index 6ed713076241fac364377f07844085b2a166d16f..af204298b8ea1b36768686204b6393c0bbb31af9 100644 (file)
--- a/src/STPManager/STPManager.h
+++ b/src/STPManager/STPManager.h
@@ -371,6 +371,13 @@ namespace BEEV
       TermsAlreadySeenMap.clear();
     }
 
+    void ClearAllTables(void) 
+    {
+      _interior_unique_table.clear();
+      _bvconst_unique_table.clear();
+      _symbol_unique_table.clear();
+    }
+
   };//End of Class STPMgr
 };//end of namespace
 #endif

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index 6a2ec50851edf0d127fcda1bbb58f2edaf3df025..d2629db344722e08e0595f4f7040793f00ea519b 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -37,7 +37,7 @@ namespace BEEV
        ASTNode::ASTNodeHasher, 
        ASTNode::ASTNodeEqual> ASTtoBitvectorMap;
 
-      ASTtoBitvectorMap _ASTNode_to_Bitvector;
+      ASTtoBitvectorMap _ASTNode_to_BitvectorMap;
 
       // This memo map is used by the ComputeFormulaUsingModel()
       ASTNodeMap ComputeFormulaMap;
@@ -171,6 +171,11 @@ namespace BEEV
       //     finiteloop); ASTNode Check_FiniteLoop_UsingModel(const
       //     ASTNode& finiteloop);
 
+      void ClearAllTables(void)
+      {
+       _ASTNode_to_BitvectorMap.clear();
+       ComputeFormulaMap.clear();
+      } //End of ClearAllTables()
     };//End of Class CounterExample
 
   class CompleteCounterExample

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 39e892f1e5d3af8c3a6a293e86082ffe43814bd4..7b4c9cfadaae9b9807acc257c79d98a366e71a77 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -53,12 +53,15 @@ namespace BEEV
 
                 //'v' is the map from bit-index to bit-value
                 HASHMAP<unsigned, bool> * v;
-                if (_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end())
-                  _ASTNode_to_Bitvector[symbol] = 
-                   new HASHMAP<unsigned, bool> (symbolWidth);
+                if (_ASTNode_to_BitvectorMap.find(symbol) == 
+                   _ASTNode_to_BitvectorMap.end())
+                 {
+                   _ASTNode_to_BitvectorMap[symbol] = 
+                     new HASHMAP<unsigned, bool> (symbolWidth);
+                 }
 
                 //v holds the map from bit-index to bit-value
-                v = _ASTNode_to_Bitvector[symbol];
+                v = _ASTNode_to_BitvectorMap[symbol];
 
                 //kk is the index of BVGETBIT
                 unsigned int kk = GetUnsignedConst(s[1]);
@@ -96,15 +99,17 @@ namespace BEEV
     //iterate over the ASTNode_to_Bitvector data-struct and construct
     //the the aggregate value of the bitvector, and populate the
     //CounterExampleMap datastructure
-    for (ASTtoBitvectorMap::iterator it = _ASTNode_to_Bitvector.begin(), 
-          itend = _ASTNode_to_Bitvector.end(); it != itend; it++)
+    for (ASTtoBitvectorMap::iterator it = _ASTNode_to_BitvectorMap.begin(), 
+          itend = _ASTNode_to_BitvectorMap.end(); it != itend; it++)
       {
         ASTNode var = it->first;
         //debugging
         //cerr << var;
         if (SYMBOL != var.GetKind())
-          FatalError("ConstructCounterExample: error while constructing counterexample: not a variable: ", var);
-
+         {
+           FatalError("ConstructCounterExample:"\
+                      "error while constructing counterexample: not a variable: ", var);
+         }
         //construct the bitvector value
         HASHMAP<unsigned, bool> * w = it->second;
         ASTNode value = BoolVectoBVConst(w, var.GetValueWidth());

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 929f68b517dbfdd63176bcc6c7fc3420781e2305..5f113ccdd9bc13f1c5a7d7456095346a700f2a72 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -242,6 +242,16 @@ namespace BEEV
        return SolverMap;
       } // End of SolverMap()
 
+      void ClearAllTables(void) 
+      {
+       SimplifyMap->clear();
+       SimplifyNegMap->clear();
+       SolverMap->clear();
+       ReadOverWrite_NewName_Map->clear();
+       NewName_ReadOverWrite_Map.clear();
+       AlwaysTrueFormMap.clear();
+       MultInverseMap.clear();
+      }
     };//end of class Simplifier
 }; //end of namespace
 #endif

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 458581e22382937786f4068d7cc8d1dc853d5a96..57d6a3aad64b530be2e018394c7d9fb9b71dd6e5 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -22,15 +22,15 @@ namespace BEEV
 
     //look for the symbol in the global map from ASTNodes to ints. if
     //not found, create a S.newVar(), else use the existing one.
-    if ((it = _ASTNode_to_SATVar.find(n)) == _ASTNode_to_SATVar.end())
+    if ((it = _ASTNode_to_SATVar_Map.find(n)) == _ASTNode_to_SATVar_Map.end())
       {
         v = newS.newVar();
-        _ASTNode_to_SATVar[n] = v;
+        _ASTNode_to_SATVar_Map[n] = v;
 
         //ASSUMPTION: I am assuming that the newS.newVar() call increments v
         //by 1 each time it is called, and the initial value of a
         //MINISAT::Var is 0.
-        _SATVar_to_AST.push_back(n);
+        _SATVar_to_AST_Vector.push_back(n);
       }
     else
       v = it->second;
@@ -140,7 +140,7 @@ namespace BEEV
   // Returns ASTTrue if true, ASTFalse if false or undefined.
   ASTNode ToSAT::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form)
   {
-    MINISAT::Var satvar = _ASTNode_to_SATVar[form];
+    MINISAT::Var satvar = _ASTNode_to_SATVar_Map[form];
     if (newS.model[satvar] == MINISAT::l_True)
       {
         return ASTTrue;

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h
index 0b7b753be277ff8f92406bcd515d7ea53fb35641..92a7ad481ea26710e1837780dea4831e814074e9 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ToSAT.h
@@ -40,14 +40,14 @@ namespace BEEV
       MINISAT::Var, 
       ASTNode::ASTNodeHasher, 
       ASTNode::ASTNodeEqual> ASTtoSATMap;
-    ASTtoSATMap _ASTNode_to_SATVar;
+    ASTtoSATMap _ASTNode_to_SATVar_Map;
 
     // MAP: This is a map from MINISAT::Vars to ASTNodes
     //
     // Reverse map used in building counterexamples. MINISAT returns a
     // model in terms of MINISAT Vars, and this map helps us convert
     // it to a model over ASTNode variables.
-    vector<ASTNode> _SATVar_to_AST;
+    vector<ASTNode> _SATVar_to_AST_Vector;
 
     // Ptr to STPManager
     STPMgr * bm;
@@ -114,9 +114,14 @@ namespace BEEV
 
     ASTNode SATVar_to_ASTMap(int i)
     {
-      return _SATVar_to_AST[i];
+      return _SATVar_to_AST_Vector[i];
     }
 
+    void ClearAllTables(void)
+    {
+      _ASTNode_to_SATVar_Map.clear();
+      _SATVar_to_AST_Vector.clear();
+    }
   }; //end of class ToSAT
 }; //end of namespace