From: trevor_hansen Date: Thu, 24 Mar 2011 03:15:35 +0000 (+0000) Subject: Improvement. Create fewer objects. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7b19b344ebe9a38cb2a432fbccedf9c6cd64775f;p=francis%2Fstp.git Improvement. Create fewer objects. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1234 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index dd8c134..3aef19e 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -164,6 +164,20 @@ namespace BEEV return true; } + bool STPMgr::LookupSymbol(const char * const name, ASTNode& output) + { + ASTSymbol temp_sym(name); + ASTSymbolSet::const_iterator it = _symbol_unique_table.find(&temp_sym); + if (it != _symbol_unique_table.end()) + { + output = ASTNode(*it); + return true; + } + return false; + } + + + //Create a ASTBVConst node ASTNode STPMgr::CreateBVConst(unsigned int width, @@ -209,36 +223,32 @@ namespace BEEV } - ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width) + ASTNode STPMgr::charToASTNode(unsigned char* strval, int base , int bit_width) { + assert ((2 == base || 10 == base || 16 == base)); + assert (bit_width > 0); - if (bit_width <= 0) - FatalError("CreateBVConst: trying to create a bvconst of width: ", - ASTUndefined, bit_width); - - - if (!(2 == base || 10 == base || 16 == base)) - { - FatalError("CreateBVConst: unsupported base: ", ASTUndefined, base); - } + // We create a single bvconst that gets reused. + if (NULL == CreateBVConstVal) + CreateBVConstVal = CONSTANTBV::BitVector_Create(65, true); + CreateBVConstVal = CONSTANTBV::BitVector_Resize(CreateBVConstVal,bit_width); + CONSTANTBV::BitVector_Empty(CreateBVConstVal); - //checking if the input is in the correct format - CBV bv = CONSTANTBV::BitVector_Create(bit_width, true); CONSTANTBV::ErrCode e; if (2 == base) { - e = CONSTANTBV::BitVector_from_Bin(bv, - (unsigned char*) strval.c_str()); + e = CONSTANTBV::BitVector_from_Bin(CreateBVConstVal, + strval); } else if (10 == base) { - e = CONSTANTBV::BitVector_from_Dec(bv, - (unsigned char*) strval.c_str()); + e = CONSTANTBV::BitVector_from_Dec(CreateBVConstVal, + strval); } else if (16 == base) { - e = CONSTANTBV::BitVector_from_Hex(bv, - (unsigned char*) strval.c_str()); + e = CONSTANTBV::BitVector_from_Hex(CreateBVConstVal, + strval); } else { @@ -251,17 +261,25 @@ namespace BEEV FatalError("", ASTUndefined); } - return CreateBVConst(bv, bit_width); + ASTBVConst temp_bvconst(CreateBVConstVal, bit_width,ASTBVConst::CBV_MANAGED_OUTSIDE); + ASTNode n(LookupOrCreateBVConst(temp_bvconst)); + return n; + } + + ASTNode STPMgr::CreateBVConst(string& strval, int base, int bit_width) + { + assert (bit_width > 0); + + return charToASTNode((unsigned char*)strval.c_str(), base , bit_width); } - //Create a ASTBVConst node from std::string + //Create a ASTBVConst node from a char* ASTNode STPMgr::CreateBVConst(const char* const strval, int base) { + assert ((2 == base || 10 == base || 16 == base)); + size_t width = strlen((const char *) strval); - if (!(2 == base || 10 == base || 16 == base)) - { - FatalError("CreateBVConst: unsupported base: ", ASTUndefined, base); - } + //FIXME Tim: Earlier versions of the code assume that the length of //binary strings is 32 bits. if (10 == base) @@ -269,45 +287,15 @@ namespace BEEV if (16 == base) width = width * 4; - //checking if the input is in the correct format - CBV bv = CONSTANTBV::BitVector_Create(width, true); - CONSTANTBV::ErrCode e; - if (2 == base) - { - e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*) strval); - } - else if (10 == base) - { - e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*) strval); - } - else if (16 == base) - { - e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*) strval); - } - else - { - e = CONSTANTBV::ErrCode_Pars; - } - - if (0 != e) - { - cerr << "CreateBVConst: " << BitVector_Error(e); - FatalError("", ASTUndefined); - } - - //FIXME - return CreateBVConst(bv, width); + return charToASTNode((unsigned char*)strval, base , width); } - //FIXME Code currently assumes that it will destroy the bitvector - //passed to it + //NB Assumes that it will destroy the bitvector passed to it ASTNode STPMgr::CreateBVConst(CBV bv, unsigned width) { - ASTBVConst temp_bvconst(bv, width); + ASTBVConst temp_bvconst(bv, width,ASTBVConst::CBV_MANAGED_OUTSIDE); ASTNode n(LookupOrCreateBVConst(temp_bvconst)); - CONSTANTBV::BitVector_Destroy(bv); - return n; } @@ -392,9 +380,7 @@ namespace BEEV ASTBVConstSet::const_iterator it; if ((it = _bvconst_unique_table.find(s_ptr)) == _bvconst_unique_table.end()) { - // Make a new ASTBVConst with duplicated string (can't assign - // _name because it's const). Can cast the iterator to - // non-const -- carefully. + // Make a new ASTBVConst with duplicated constant. ASTBVConst * s_copy = new ASTBVConst(s); s_copy->SetNodeNum(NewNodeNum()); @@ -405,7 +391,7 @@ namespace BEEV } else { - // return symbol found in table. + // return constant found in table. return *it; } } diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index ac92426..24aefb8 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -141,6 +141,7 @@ namespace BEEV public: bool LookupSymbol(const char * const name); + bool LookupSymbol(const char * const name, ASTNode& output); /**************************************************************** * Public Flags * @@ -277,6 +278,7 @@ namespace BEEV ASTNode CreateBVConst(const char *strval, int base); ASTNode CreateBVConst(string& strval, int base, int bit_width); ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); + ASTNode charToASTNode(unsigned char* strval, int base , int bit_width); /**************************************************************** * Create Node functions * diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index eaf4507..83e7f91 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -99,6 +99,11 @@ public: return bm.LookupOrCreateSymbol(name.c_str()); } + bool LookupSymbol(const char * const name, ASTNode& output) + { + return bm.LookupSymbol(name,output); + } + bool isSymbolAlreadyDeclared(char* name) { return bm.LookupSymbol(name); diff --git a/src/parser/cvc.lex b/src/parser/cvc.lex index a7b93c4..bfdbbcd 100644 --- a/src/parser/cvc.lex +++ b/src/parser/cvc.lex @@ -125,9 +125,8 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) ASTNode nptr; - if (BEEV::parserInterface->isSymbolAlreadyDeclared(yytext)) // it's a symbol. + if (BEEV::parserInterface->LookupSymbol(yytext,nptr)) // it's a symbol. { - nptr= BEEV::parserInterface->LookupOrCreateSymbol(yytext); cvclval.node = BEEV::parserInterface->newNode(nptr); if ((cvclval.node)->GetType() == BEEV::BOOLEAN_TYPE) return FORMID_TOK;