From a527bae4d543d1066f3e17ba420a5f71494b2981 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 19 Jan 2011 04:06:24 +0000 Subject: [PATCH] Speedup. When parsing don't create symbols for the let names. Use strings instead. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1076 e59a4935-1847-0410-ae03-e826735625c1 --- src/parser/LetMgr.cpp | 59 +++++++++++----------------------- src/parser/LetMgr.h | 35 +++++++++++++++------ src/parser/ParserInterface.h | 11 +++++++ src/parser/smtlib2.lex | 45 +++++++++++++++++++------- src/parser/smtlib2.y | 61 +++++++++++++++++++----------------- 5 files changed, 121 insertions(+), 90 deletions(-) diff --git a/src/parser/LetMgr.cpp b/src/parser/LetMgr.cpp index a64692d..9ab65e1 100644 --- a/src/parser/LetMgr.cpp +++ b/src/parser/LetMgr.cpp @@ -11,7 +11,7 @@ #include "LetMgr.h" namespace BEEV { - // FUNC: This function maintains a map between LET-var names and + // FUNC: This function builds the map between LET-var names and // LET-expressions // //1. if the Let-var is already defined in the LET scope, then the @@ -23,27 +23,29 @@ namespace BEEV { //3. otherwise add the pair to the _letid_expr table. void LETMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) { - ASTNodeMap::iterator it; - if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && - it->second != ASTUndefined) { - FatalError("LetExprMgr:The LET-var v has already been defined"\ - "in this LET scope: v =", var); + string name = var.GetName(); + MapType::iterator it; + if(((it = _letid_expr_map->find(name)) != _letid_expr_map->end())) + { + FatalError("LetExprMgr:The LET-var v has already been defined"\ + "in this LET scope: v =", var); } - if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) { - FatalError("LetExprMgr:This var is already declared. "\ - "cannot redeclare as a letvar: v =", var); + if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) + { + FatalError("LetExprMgr:This var is already declared. "\ + "cannot redeclare as a letvar: v =", var); } - (*_letid_expr_map)[var] = letExpr; + (*_letid_expr_map)[name] = letExpr; }//end of LetExprMgr() - //this function looksup the "var to letexpr map" and returns the + //this function looks up the "var to letexpr map" and returns the //corresponding letexpr. if there is no letexpr, then it simply //returns the var. ASTNode LETMgr::ResolveID(const ASTNode& v) { - if (v.GetKind() != SYMBOL) { + if (v.GetKind() != SYMBOL) { return v; } @@ -51,22 +53,12 @@ namespace BEEV { return v; } - ASTNodeMap::iterator it; - if((it =_letid_expr_map->find(v)) != _letid_expr_map->end()) { - if(it->second == ASTUndefined) - FatalError("ResolveID :: Unresolved Identifier: ",v); - else + MapType::iterator it; + if((it =_letid_expr_map->find(v.GetName())) != _letid_expr_map->end()) + { return it->second; - } + } - //this is to mark the let-var as undefined. the let var is defined - //only after the LetExprMgr has completed its work, and until then - //'v' is undefined. - // - //declared variables also get stored in this map, but there value - //is ASTUndefined. This is really a hack. I don't know how to get - //rid of this hack. - (*_letid_expr_map)[v] = ASTUndefined; return v; }//End of ResolveID() @@ -77,19 +69,6 @@ namespace BEEV { if (_letid_expr_map->size() ==0) return; - // If ?v0 is encountered and is set with a bitwidth of 6 (say), - // when it's next encountered in another let, then we want it to - // have a formula type. - ASTNodeMap::iterator it = _letid_expr_map->begin(); - ASTNodeMap::iterator itend = _letid_expr_map->end(); - for(;it!=itend;it++) { - if(it->second != ASTUndefined) { - it->first.SetValueWidth(0); - it->first.SetIndexWidth(0); - } - } - - // May contain lots of buckets, so reset. delete _letid_expr_map; InitializeLetIDMap(); @@ -97,6 +76,6 @@ namespace BEEV { void LETMgr::InitializeLetIDMap(void) { - _letid_expr_map = new ASTNodeMap(); + _letid_expr_map = new hash_map(); } //end of InitializeLetIDMap() }; diff --git a/src/parser/LetMgr.h b/src/parser/LetMgr.h index 976a23e..7fc5a57 100644 --- a/src/parser/LetMgr.h +++ b/src/parser/LetMgr.h @@ -11,34 +11,53 @@ #define LETMGR_H #include "../AST/AST.h" + + // Hash function for the hash_map of a string.. + _GLIBCXX_BEGIN_NAMESPACE(__gnu_cxx) + template <> + struct hash { + size_t operator() (const std::string& x) const { + return hash()(x.c_str()); + } + }; + }; + namespace BEEV { //LET Management class LETMgr { private: - const ASTNode ASTUndefined; - // MAP: This map is from bound IDs that occur in LETs to + typedef hash_map > MapType; + + // MAP: This map is from bound IDs that occur in LETs to // expression. The map is useful in checking replacing the IDs // with the corresponding expressions. As soon as the brackets - // that close a let expression is reached, it is emptied by + // that close a let expression is reached, it is emptied by // a call to CleanupLetIDMap(). - ASTNodeMap *_letid_expr_map; + MapType *_letid_expr_map; //Allocate LetID map void InitializeLetIDMap(void); - public: - + public: + + // I think this keeps a reference to symbols so they don't get garbage collected. ASTNodeSet _parser_symbol_table; + + // A let with this name has already been declared. + bool isLetDeclared(string s) + { + return _letid_expr_map->find(s) !=_letid_expr_map->end(); + } + void cleanupParserSymbolTable() { _parser_symbol_table.clear(); } - LETMgr(ASTNode undefined) : ASTUndefined(undefined) { @@ -59,8 +78,6 @@ namespace BEEV //Delete Letid Map. Called when we move onto the expression after (let ... ) void CleanupLetIDMap(void); - //Substitute Let-vars with LetExprs - //ASTNode SubstituteLetExpr(ASTNode inExpr); };// End of class LETMgr }; //end of namespace diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index 89569d8..0b8cb7f 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -91,6 +91,17 @@ public: { return bm.LookupOrCreateSymbol(name); } + + ASTNode LookupOrCreateSymbol(string name) + { + return bm.LookupOrCreateSymbol(name.c_str()); + } + + + bool isSymbolAlreadyDeclared(string name) + { + return bm.LookupSymbol(name.c_str()); + } }; } diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex index edeae9c..7b27f20 100644 --- a/src/parser/smtlib2.lex +++ b/src/parser/smtlib2.lex @@ -68,18 +68,39 @@ if (s[0] == '|' && s[str.size()-1] == '|') str = str.substr(1,str.length()-2); - BEEV::ASTNode nptr = BEEV::parserInterface->LookupOrCreateSymbol(str.c_str()); - - // Check valuesize to see if it's a prop var. I don't like doing - // type determination in the lexer, but it's easier than rewriting - // the whole grammar to eliminate the term/formula distinction. - smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr)); - if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE) - return FORMID_TOK; - else - return TERMID_TOK; - } - + BEEV::ASTNode nptr; + bool found = false; + + if (BEEV::parserInterface->isSymbolAlreadyDeclared(str)) // it's a symbol. + { + nptr= BEEV::parserInterface->LookupOrCreateSymbol(str); + found = true; + } + else if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let. + { + nptr= BEEV::parserInterface->LookupOrCreateSymbol(str); + nptr = BEEV::parserInterface->letMgr.ResolveID(nptr); + found = true; + } + + if (found) + { + // Check valuesize to see if it's a prop var. I don't like doing + // type determination in the lexer, but it's easier than rewriting + // the whole grammar to eliminate the term/formula distinction. + smt2lval.node = new BEEV::ASTNode(BEEV::parserInterface->letMgr.ResolveID(nptr)); + if ((smt2lval.node)->GetType() == BEEV::BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; + } + else + { + // it has not been seen before. + smt2lval.str = new std::string(str); + return STRING_TOK; + } + } %} %option noyywrap diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y index 35b393b..9763e71 100644 --- a/src/parser/smtlib2.y +++ b/src/parser/smtlib2.y @@ -226,25 +226,21 @@ cmdi: commands.push_back("check-sat"); } | - LPAREN_TOK LOGIC_TOK FORMID_TOK RPAREN_TOK + LPAREN_TOK LOGIC_TOK STRING_TOK RPAREN_TOK { - if (!(0 == strcmp($3->GetName(),"QF_BV") || - 0 == strcmp($3->GetName(),"QF_ABV") || - 0 == strcmp($3->GetName(),"QF_AUFBV"))) { + if (!(0 == strcmp($3->c_str(),"QF_BV") || + 0 == strcmp($3->c_str(),"QF_ABV") || + 0 == strcmp($3->c_str(),"QF_AUFBV"))) { yyerror("Wrong input logic:"); } delete $3; } -| LPAREN_TOK NOTES_TOK attribute FORMID_TOK RPAREN_TOK +| LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK { delete $4; } | LPAREN_TOK NOTES_TOK attribute DECIMAL_TOK RPAREN_TOK {} -| LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK - { - delete $4; - } | LPAREN_TOK NOTES_TOK attribute RPAREN_TOK {} | LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK @@ -286,36 +282,39 @@ SOURCE_TOK ; var_decl: -FORMID_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK +STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK { - parserInterface->letMgr._parser_symbol_table.insert(*$1); + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); + parserInterface->letMgr._parser_symbol_table.insert(s); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var - $1->SetIndexWidth(0); - $1->SetValueWidth($7); + s.SetIndexWidth(0); + s.SetValueWidth($7); delete $1; } -| FORMID_TOK LPAREN_TOK RPAREN_TOK BOOL_TOK +| STRING_TOK LPAREN_TOK RPAREN_TOK BOOL_TOK { - $1->SetIndexWidth(0); - $1->SetValueWidth(0); - parserInterface->letMgr._parser_symbol_table.insert(*$1); + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); + s.SetIndexWidth(0); + s.SetValueWidth(0); + parserInterface->letMgr._parser_symbol_table.insert(s); delete $1; } -| FORMID_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK ARRAY_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK +| STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK ARRAY_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK { - parserInterface->letMgr._parser_symbol_table.insert(*$1); + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); + parserInterface->letMgr._parser_symbol_table.insert(s); unsigned int index_len = $9; unsigned int value_len = $14; if(index_len > 0) { - $1->SetIndexWidth($9); + s.SetIndexWidth($9); } else { FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); } if(value_len > 0) { - $1->SetValueWidth($14); + s.SetValueWidth($14); } else { FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); @@ -531,11 +530,13 @@ lets: let lets | let {}; -let: LPAREN_TOK FORMID_TOK an_formula RPAREN_TOK +let: LPAREN_TOK STRING_TOK an_formula RPAREN_TOK { + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str()); + //set the valuewidth of the identifier - $2->SetValueWidth($3->GetValueWidth()); - $2->SetIndexWidth($3->GetIndexWidth()); + s.SetValueWidth($3->GetValueWidth()); + s.SetIndexWidth($3->GetIndexWidth()); //populate the hashtable from LET-var --> //LET-exprs and then process them: @@ -545,16 +546,18 @@ let: LPAREN_TOK FORMID_TOK an_formula RPAREN_TOK // //2. Ensure that LET variables are not //2. defined more than once - parserInterface->letMgr.LetExprMgr(*$2,*$3); + parserInterface->letMgr.LetExprMgr(s,*$3); delete $2; delete $3; } -| LPAREN_TOK FORMID_TOK an_term RPAREN_TOK +| LPAREN_TOK STRING_TOK an_term RPAREN_TOK { + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str()); + //set the valuewidth of the identifier - $2->SetValueWidth($3->GetValueWidth()); - $2->SetIndexWidth($3->GetIndexWidth()); + s.SetValueWidth($3->GetValueWidth()); + s.SetIndexWidth($3->GetIndexWidth()); //populate the hashtable from LET-var --> //LET-exprs and then process them: @@ -564,7 +567,7 @@ let: LPAREN_TOK FORMID_TOK an_formula RPAREN_TOK // //2. Ensure that LET variables are not //2. defined more than once - parserInterface->letMgr.LetExprMgr(*$2,*$3); + parserInterface->letMgr.LetExprMgr(s,*$3); delete $2; delete $3; -- 2.47.3