#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
//3. otherwise add the <var,letExpr> 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;
}
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()
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();
void LETMgr::InitializeLetIDMap(void)
{
- _letid_expr_map = new ASTNodeMap();
+ _letid_expr_map = new hash_map<string,ASTNode>();
} //end of InitializeLetIDMap()
};
#define LETMGR_H
#include "../AST/AST.h"
+
+ // Hash function for the hash_map of a string..
+ _GLIBCXX_BEGIN_NAMESPACE(__gnu_cxx)
+ template <>
+ struct hash<std::string> {
+ size_t operator() (const std::string& x) const {
+ return hash<const char*>()(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<string,ASTNode, __gnu_cxx::hash<std::string> > 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)
{
//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
{
return bm.LookupOrCreateSymbol(name);
}
+
+ ASTNode LookupOrCreateSymbol(string name)
+ {
+ return bm.LookupOrCreateSymbol(name.c_str());
+ }
+
+
+ bool isSymbolAlreadyDeclared(string name)
+ {
+ return bm.LookupSymbol(name.c_str());
+ }
};
}
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
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
;
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");
| 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:
//
//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:
//
//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;
projects / francis / stp.git / commitdiff