From f352888a72003b96e087c499b872735168827c60 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 24 Feb 2011 00:46:48 +0000 Subject: [PATCH] Partial refactoring. Removing the arrayread_itemap. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1164 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 18 ++++++- src/AST/ArrayTransformer.h | 22 ++++----- .../CounterExample.cpp | 48 ++++++++++--------- 3 files changed, 50 insertions(+), 38 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 8cf7ac5..51c5ca7 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -547,12 +547,26 @@ namespace BEEV * ..... */ + { + ArrType::const_iterator it; + if ((it = arrayToIndexToRead.find(arrName)) != arrayToIndexToRead.end()) + { + map::const_iterator it2; + if ((it2 = it->second.find(readIndex)) != it->second.end()) + { + result = it2->second.ite; + break; + } + } + } + // Recursively transform read index, which may also contain reads. ASTNode processedTerm = nf->CreateTerm(READ, width, arrName, readIndex); //check if the 'processedTerm' has a corresponding ITE construct //already. if so, return it. else continue processing. + /* ASTNodeMap::const_iterator it; if ((it = Arrayread_IteMap->find(processedTerm)) != Arrayread_IteMap->end()) @@ -560,6 +574,8 @@ namespace BEEV result = it->second; break; } + */ + //Constructing Symbolic variable corresponding to 'processedTerm' ASTNode CurrentSymbol; ASTNodeMap::const_iterator it1; @@ -636,7 +652,7 @@ namespace BEEV (*Arrayname_ReadindicesMap)[arrName].push_back(readIndex); //save the ite corresponding to 'processedTerm' - (*Arrayread_IteMap)[processedTerm] = result; + //(*Arrayread_IteMap)[processedTerm] = result; assert(arrName.GetType() == ARRAY_TYPE); assert(result.GetValueWidth() == CurrentSymbol.GetValueWidth()); diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index accb2dc..d3451fe 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -83,9 +83,9 @@ namespace BEEV // array reads in the input Read(A,i) and Read(A,j). Then // Read(A,i) is replaced with a symbolic constant, say v1, and // Read(A,j) is replaced with the following ITE: ITE(i=j,v1,v2) - public: - ASTNodeMap * Arrayread_IteMap; - private: + + //ASTNodeMap * Arrayread_IteMap; + // Memo table used by the transformer while it is transforming the // formulas and terms @@ -147,7 +147,7 @@ namespace BEEV debug_transform(0), TransformMap(NULL) { - Arrayread_IteMap = new ASTNodeMap(); + //Arrayread_IteMap = new ASTNodeMap(); Arrayname_ReadindicesMap = new ASTNodeToVecMap(); nf = bm->defaultNodeFactory; @@ -160,8 +160,8 @@ namespace BEEV // Destructor ~ArrayTransformer() { - Arrayread_IteMap->clear(); - delete Arrayread_IteMap; + //Arrayread_IteMap->clear(); + //delete Arrayread_IteMap; ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin(); ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end(); for(;it!=itend;it++) @@ -187,13 +187,6 @@ namespace BEEV return symbol; } //End of ArrayRead_SymbolMap - - ASTNode ArrayRead_Ite(const ASTNode& arrread) - { - return (*Arrayread_IteMap)[arrread]; - } //End of ArrayRead_Ite - - void ClearAllTables(void) { @@ -207,7 +200,8 @@ namespace BEEV Arrayname_ReadindicesMap->clear(); Arrayread_SymbolMap.clear(); - Arrayread_IteMap->clear(); + //Arrayread_IteMap->clear(); + arrayToIndexToRead.clear(); } }; //end of class Transformer diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index 77da0c6..726977b 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -82,30 +82,32 @@ namespace BEEV } } - //In this loop, we compute the value of each array read, the - //corresponding ITE against the counterexample generated above. - for (ASTNodeMap::const_iterator it = - ArrayTransform->Arrayread_IteMap->begin(), itend = - ArrayTransform->Arrayread_IteMap->end(); it != itend; it++) + for (ArrayTransformer::ArrType::const_iterator it = ArrayTransform->arrayToIndexToRead.begin(), itend = + ArrayTransform->arrayToIndexToRead.end(); it != itend; it++) { - //the array read - const ASTNode& arrayread = it->first; - const ASTNode& value_ite = it->second; - - //convert it to a constant array-read and store it in the - //counter-example. First convert the index into a constant. then - //construct the appropriate array-read and store it in the - //counterexample - ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1],false); - ASTNode key = bm->CreateTerm(READ, arrayread.GetValueWidth(), - arrayread[0], arrayread_index); - - //Get the ITE corresponding to the array-read and convert it - //to a constant against the model - ASTNode value = TermToConstTermUsingModel(value_ite); - //save the result in the counter_example - if (!simp->CheckSubstitutionMap(key)) - CounterExampleMap[key] = value; + const ASTNode& array = it->first; + const map& mapper = it->second; + + for (map::const_iterator it2 = mapper.begin(), it2end = mapper.end(); it2 + != it2end; it2++) + { + const ASTNode& index = it2->first; + const ASTNode& value_ite = it2->second.ite; + + //convert it to a constant array-read and store it in the + //counter-example. First convert the index into a constant. then + //construct the appropriate array-read and store it in the + //counterexample + ASTNode arrayread_index = TermToConstTermUsingModel(index, false); + ASTNode key = bm->CreateTerm(READ, array.GetValueWidth(), array, arrayread_index); + + //Get the ITE corresponding to the array-read and convert it + //to a constant against the model + ASTNode value = TermToConstTermUsingModel(value_ite); + //save the result in the counter_example + if (!simp->CheckSubstitutionMap(key)) + CounterExampleMap[key] = value; + } } } //End of ConstructCounterExample -- 2.47.3