From 3117dadc590f4d5168979585abe46df886993c56 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Tue, 13 Oct 2009 15:44:00 +0000 Subject: [PATCH] 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 --- src/AST/ArrayTransformer.h | 8 +++++++ src/STPManager/STPManager.h | 7 +++++++ .../AbsRefine_CounterExample.h | 7 ++++++- .../CounterExample.cpp | 21 ++++++++++++------- src/simplifier/simplifier.h | 10 +++++++++ src/to-sat/ToSAT.cpp | 8 +++---- src/to-sat/ToSAT.h | 11 +++++++--- 7 files changed, 56 insertions(+), 16 deletions(-) diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index ca6f111..97b7775 100644 --- 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 6ed7130..af20429 100644 --- 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 6a2ec50..d2629db 100644 --- 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 39e892f..7b4c9cf 100644 --- 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 * v; - if (_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) - _ASTNode_to_Bitvector[symbol] = - new HASHMAP (symbolWidth); + if (_ASTNode_to_BitvectorMap.find(symbol) == + _ASTNode_to_BitvectorMap.end()) + { + _ASTNode_to_BitvectorMap[symbol] = + new HASHMAP (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 * w = it->second; ASTNode value = BoolVectoBVConst(w, var.GetValueWidth()); diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index 929f68b..5f113cc 100644 --- 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 458581e..57d6a3a 100644 --- 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 0b7b753..92a7ad4 100644 --- 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 _SATVar_to_AST; + vector _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 -- 2.47.3