From b6e589a523e2c69abcc7a2cfdaf2bc622046f5db Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 31 Aug 2010 14:43:53 +0000 Subject: [PATCH] Fresh variables created for internal uses, for instance to replace READs during abstraction/refinement. Are now better tracked so that they can be ignored when the model is printed. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1010 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ArrayTransformer.cpp | 1 - src/AST/ArrayTransformer.h | 15 +------------ src/STPManager/STPManager.cpp | 14 ------------- src/STPManager/STPManager.h | 21 ++++++++++++++++--- .../CounterExample.cpp | 2 +- src/simplifier/bvsolver.cpp | 5 +++-- src/simplifier/simplifier.cpp | 2 +- 7 files changed, 24 insertions(+), 36 deletions(-) diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index f3b0dae..78c8691 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -587,7 +587,6 @@ namespace BEEV "array_" + string(arrName.GetName())); Arrayread_SymbolMap[processedTerm] = CurrentSymbol; - Introduced_SymbolsSet.insert(CurrentSymbol); } ASTNode ite = CurrentSymbol; diff --git a/src/AST/ArrayTransformer.h b/src/AST/ArrayTransformer.h index c941b43..c9bf61a 100644 --- a/src/AST/ArrayTransformer.h +++ b/src/AST/ArrayTransformer.h @@ -55,9 +55,7 @@ namespace BEEV // Read(A,j) is replaced with the following ITE: ITE(i=j,v1,v2) ASTNodeMap * Arrayread_IteMap; - // Set of new symbols introduced that replace the array read terms - ASTNodeSet Introduced_SymbolsSet; - + // Count to keep track of new symbolic constants introduced // corresponding to Array Reads unsigned int _symbol_count; @@ -117,7 +115,6 @@ namespace BEEV // Constructor ArrayTransformer(STPMgr * bm, Simplifier* s) : Arrayread_SymbolMap(), - Introduced_SymbolsSet(), bm(bm), simp(s), debug_transform(0), @@ -139,7 +136,6 @@ namespace BEEV { Arrayread_IteMap->clear(); delete Arrayread_IteMap; - Introduced_SymbolsSet.clear(); ASTNodeToVecMap::iterator it= Arrayname_ReadindicesMap->begin(); ASTNodeToVecMap::iterator itend= Arrayname_ReadindicesMap->end(); for(;it!=itend;it++) @@ -175,14 +171,6 @@ namespace BEEV return (*Arrayread_IteMap)[arrread]; } //End of ArrayRead_Ite - bool FoundIntroducedSymbolSet(const ASTNode& in) - { - if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end()) - { - return true; - } - return false; - } // End of IntroduceSymbolSet void ClearAllTables(void) { @@ -198,7 +186,6 @@ namespace BEEV Arrayname_ReadindicesMap->clear(); Arrayread_SymbolMap.clear(); Arrayread_IteMap->clear(); - Introduced_SymbolsSet.clear(); } }; //end of class Transformer diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 9273511..d20a787 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -639,20 +639,6 @@ namespace BEEV return newn; } - //Create a new variable of ValueWidth 'n' - ASTNode STPMgr::NewVar(unsigned int n) - { - std::string c("v"); - char d[32]; - sprintf(d, "%d", _symbol_count++); - std::string ccc(d); - c += "_solver_" + ccc; - - ASTNode CurrentSymbol = CreateSymbol(c.c_str(),0,n); - assert(0 !=n); - return CurrentSymbol; - } //end of NewVar() - bool STPMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) { if (READ == term.GetKind() diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index da455a8..6e63371 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -133,6 +133,9 @@ namespace BEEV ASTVec ones; ASTVec max; + // Set of new symbols introduced that replace the array read terms + ASTNodeSet Introduced_SymbolsSet; + public: /**************************************************************** @@ -383,18 +386,28 @@ namespace BEEV // Print assertions to the input stream void printAssertsToStream(ostream &os, int simplify); - // Create New Variables - ASTNode NewVar(unsigned int n); - + // Variables are added automatically to the introduced_symbolset. Variables + // in the set aren't printed out as part of the counter example. ASTNode CreateFreshVariable(int indexWidth, int valueWidth, std::string prefix) { char d[32 + prefix.length()]; sprintf(d, "%s_%d", prefix.c_str(), _symbol_count++); BEEV::ASTNode CurrentSymbol = CreateSymbol(d,indexWidth,valueWidth); + Introduced_SymbolsSet.insert(CurrentSymbol); return CurrentSymbol; } + bool FoundIntroducedSymbolSet(const ASTNode& in) + { + if(Introduced_SymbolsSet.find(in) != Introduced_SymbolsSet.end()) + { + return true; + } + return false; + } // End of IntroduceSymbolSet + + bool VarSeenInTerm(const ASTNode& var, const ASTNode& term); @@ -406,6 +419,8 @@ namespace BEEV TermsAlreadySeenMap.clear(); } + // This is called before SAT solving, so only junk that isn't needed + // after SAT solving should be cleaned out. void ClearAllTables(void) { NodeLetVarMap.clear(); diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp index ffcc5af..dfdf03f 100644 --- a/src/absrefine_counterexample/CounterExample.cpp +++ b/src/absrefine_counterexample/CounterExample.cpp @@ -745,7 +745,7 @@ namespace BEEV } //skip over introduced variables - if (f.GetKind() == SYMBOL && (ArrayTransform->FoundIntroducedSymbolSet( + if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet( f))) { continue; diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index ca27540..91e39be 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -457,7 +457,7 @@ namespace BEEV //then also add another entry for x = x1@t ASTNode var = lhs[0]; ASTNode newvar = - _bm->NewVar(var.GetValueWidth() - lhs.GetValueWidth()); + _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs.GetValueWidth(), "v_solver"); newvar = _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), newvar, rhs); assert(BVTypeCheck(newvar)); @@ -528,8 +528,9 @@ namespace BEEV if (ChosenVar_Is_Extract) { const ASTNode& var = lhs[1][0]; + ASTNode newvar = - _bm->NewVar(var.GetValueWidth() - lhs[1].GetValueWidth()); + _bm->CreateFreshVariable(0, var.GetValueWidth() - lhs[1].GetValueWidth(), "v_solver"); newvar = _bm->CreateTerm(BVCONCAT, var.GetValueWidth(), diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 20efa8e..3961f92 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -3597,7 +3597,7 @@ namespace BEEV ASTNode newVar; if (!CheckSimplifyMap(input, newVar, false)) { - newVar = _bm->NewVar(input.GetValueWidth()); + newVar = _bm->CreateFreshVariable(0,input.GetValueWidth(),"v_solver"); (*ReadOverWrite_NewName_Map)[input] = newVar; NewName_ReadOverWrite_Map[newVar] = input; -- 2.47.3