From f7d8a5cb624b74724e5746e4fc058c7377118314 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 24 Feb 2011 01:42:37 +0000 Subject: [PATCH] Finish refactoring of the ArrayTransformer class. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1167 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 99 ++++++++---------------------------- src/AST/ArrayTransformer.h | 84 ++---------------------------- 2 files changed, 23 insertions(+), 160 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 97307c5..e82e662 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -560,68 +560,32 @@ namespace BEEV } } - // The read index has already been recursively transformed. - 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()) - { - result = it->second; - break; - } - */ - - //Constructing Symbolic variable corresponding to 'processedTerm' - ASTNode CurrentSymbol; - ASTNodeMap::const_iterator it1; - // First, check if read index is constant and it has a - // constant value in the substitution map. - if (simp->CheckSubstitutionMap(processedTerm, CurrentSymbol)) - { - //Arrayread_SymbolMap[processedTerm] = CurrentSymbol; - } - // Check if it already has an abstract variable. - //else if ((it1 = Arrayread_SymbolMap.find(processedTerm)) - // != Arrayread_SymbolMap.end()) - // { - // CurrentSymbol = it1->second; - // } - else - { - // Make up a new abstract variable. Build symbolic name - // corresponding to array read. The symbolic name has 2 - // components: stringname, and a count - - CurrentSymbol = bm->CreateFreshVariable( - processedTerm.GetIndexWidth(), - processedTerm.GetValueWidth(), - "array_" + string(arrName.GetName())); + // Make up a new abstract variable. Build symbolic name + // corresponding to array read. The symbolic name has 2 + // components: stringname, and a count - //Arrayread_SymbolMap[processedTerm] = CurrentSymbol; - } + ASTNode CurrentSymbol = bm->CreateFreshVariable( + term.GetIndexWidth(), + term.GetValueWidth(), + "array_" + string(arrName.GetName())); result = CurrentSymbol; if (bm->UserFlags.arrayread_refinement_flag) { - // ite is really a variable here; it is an ite in the + // result is a variable here; it is an ite in the // else-branch } else { + // Full Array transform if we're not doing read refinement. + //list of array-read indices corresponding to arrName, seen while //traversing the AST tree. we need this list to construct the ITEs - // Dill: we hope to make this irrelevant. Harmless for now. - const map& new_read_Indices = arrayToIndexToRead[arrName]; + const arrTypeMap& new_read_Indices = arrayToIndexToRead[arrName]; - // Full Array transform if we're not doing read refinement. - map::const_iterator it2 = new_read_Indices.begin(); - map::const_iterator it2end = new_read_Indices.end(); + arrTypeMap::const_iterator it2 = new_read_Indices.begin(); + arrTypeMap::const_iterator it2end = new_read_Indices.end(); for (; it2 != it2end; it2++) { ASTNode cond = simp->CreateSimplifiedEQ(readIndex, it2->first); @@ -631,15 +595,9 @@ namespace BEEV result = simp->CreateSimplifiedTermITE(cond, it2->second.ite, result); } - } - //(*Arrayname_ReadindicesMap)[arrName].push_back(readIndex); - //save the ite corresponding to 'processedTerm' - //(*Arrayread_IteMap)[processedTerm] = result; - assert(arrName.GetType() == ARRAY_TYPE); - assert(result.GetValueWidth() == CurrentSymbol.GetValueWidth()); arrayToIndexToRead[arrName].insert(make_pair(readIndex,ArrayRead (result, CurrentSymbol))); break; } //end of READ over a SYMBOL @@ -800,13 +758,6 @@ namespace BEEV } //end of TransformArray() - //This function records all the const-indices seen so far for each - //array. It populates the map 'Arrayname_ReadindicesMap' whose key is - //the arrayname, and vlaue is a vector of read-indices. - // - //fill the arrayname_readindices vector if e0 is a READ(Arr,index) - //and index is a BVCONST. - // //Since these arrayreads are being nuked and recorded in the //substitutionmap, we have to also record the fact that each //arrayread (e0 is of the form READ(Arr,const) here is represented @@ -815,24 +766,14 @@ namespace BEEV void ArrayTransformer::FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1) { - assert(e0.GetKind() == READ); - assert(e1.GetKind() == BVCONST); - - if (e0[0].GetKind() != SYMBOL) - return; - if (e0[1].GetKind() != BVCONST) - return; + assert (e0.GetKind() == READ); + assert (e0[0].GetKind() == SYMBOL); + assert (e0[1].GetKind() == BVCONST); + assert (e1.GetKind() == BVCONST); + assert(arrayToIndexToRead[e0[0]].find(e0[1]) ==arrayToIndexToRead[e0[0]].end()); - if (!simp->CheckSubstitutionMap(e0)) - { - //(*Arrayname_ReadindicesMap)[e0[0]].push_back(e0[1]); - //e0 is the array read : READ(A,i) and e1 is a bvconst - //Arrayread_SymbolMap[e0] = e1; - arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1))); - return; - } - - } //End of Fillup + arrayToIndexToRead[e0[0]].insert(make_pair(e0[1],ArrayRead (e1, e1))); + } } //end of namespace BEEV diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index fbd1b6b..eb03e54 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -28,6 +28,7 @@ namespace BEEV ArrayRead(ASTNode _ite, ASTNode _symbol) { assert(! _symbol.IsNull()); + assert(_ite.GetValueWidth() == _symbol.GetValueWidth()); assert ((SYMBOL == _symbol.GetKind() || BVCONST == _symbol.GetKind())); ite = _ite; @@ -47,7 +48,8 @@ namespace BEEV // a symbolic constant, say v1, and Read(A,j) is replaced with the // following ITE: ITE(i=j,v1,v2) - typedef map > ArrType ; + typedef map arrTypeMap; + typedef map ArrType ; ArrType arrayToIndexToRead; private: @@ -58,44 +60,12 @@ namespace BEEV // Handy defs ASTNode ASTTrue, ASTFalse, ASTUndefined; - - // MAP: This is a map from Array Names to list of array-read - // indices in the input. This map is used by the TransformArray() - // function. This map is useful in converting array reads into - // nested ITE constructs. Suppose there are two 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) - // - // CAUTION: I tried using a set instead of vector for read - // indicies. for some odd reason the performance went down - // considerably. this is totally inexplicable. - //ASTNodeToVecMap * Arrayname_ReadindicesMap; - - // MAP: This is a map from array-reads to symbolic constants. This - // map is used by the TransformArray() - //ASTNodeMap Arrayread_SymbolMap; - - // MAP: This is a map from Array Names to nested ITE constructs, - // which are built as described below. This map is used by the - // TransformArray() function. This map is useful in converting - // array reads into nested ITE constructs. Suppose there are two - // 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) - - //ASTNodeMap * Arrayread_IteMap; // Memo table used by the transformer while it is transforming the // formulas and terms ASTNodeMap* TransformMap; - // For finiteloop construct. A list of all finiteloop constructs - // in the input formula - // - // ASTVec GlobalList_Of_FiniteLoops; - // Flag for debuggin the transformer const bool debug_transform; @@ -118,11 +88,6 @@ namespace BEEV ASTNode TranslateSignedDivModRem(const ASTNode& in); ASTNode TransformTerm(const ASTNode& inputterm); void assertTransformPostConditions(const ASTNode & term, ASTNodeSet& visited); - - /**************************************************************** - * Helper functions to for creating substitution map * - ****************************************************************/ - ASTNode TransformArrayRead(const ASTNode& term); @@ -141,14 +106,11 @@ namespace BEEV // Constructor ArrayTransformer(STPMgr * bm, Simplifier* s) : - //Arrayread_SymbolMap(), bm(bm), simp(s), debug_transform(0), TransformMap(NULL) { - //Arrayread_IteMap = new ASTNodeMap(); - //Arrayname_ReadindicesMap = new ASTNodeToVecMap(); nf = bm->defaultNodeFactory; runTimes = bm->GetRunTimes(); @@ -157,52 +119,12 @@ namespace BEEV ASTUndefined = bm->CreateNode(UNDEFINED); } - // Destructor - ~ArrayTransformer() - { - //Arrayread_IteMap->clear(); - //delete Arrayread_IteMap; - /*ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin(); - ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end(); - for(;it!=itend;it++) - { - ((*it).second).clear(); - } - Arrayname_ReadindicesMap->clear(); - delete Arrayname_ReadindicesMap; - */ - } - // Takes a formula, transforms it by replacing array reads with // variables, and returns the transformed formula ASTNode TransformFormula_TopLevel(const ASTNode& form); - //const ASTNodeToVecMap * ArrayName_ReadIndicesMap() - //{ -// return Arrayname_ReadindicesMap; - // } //End of ArrayName_ReadIndicesMap - - //const ASTNode ArrayRead_SymbolMap(const ASTNode& arrread) - //{ - //ASTNode symbol = Arrayread_SymbolMap[arrread]; - //return symbol; - // } //End of ArrayRead_SymbolMap - void ClearAllTables(void) { - - /*for (ASTNodeToVecMap::iterator - iset = Arrayname_ReadindicesMap->begin(), - iset_end = Arrayname_ReadindicesMap->end(); - iset != iset_end; iset++) - { - iset->second.clear(); - } - - Arrayname_ReadindicesMap->clear(); -*/ - //Arrayread_SymbolMap.clear(); - //Arrayread_IteMap->clear(); arrayToIndexToRead.clear(); } }; //end of class Transformer -- 2.47.3