diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 02:34:04 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-10 02:34:04 +0000 |
commit | 0cd57d89001a73ea1ebe0d43b2cb720d68cca82a (patch) | |
tree | 422a6682cb3d37086b98379ee474547160220955 /src/parser/antlr_parser.cpp | |
parent | 8d85fb035b92f0fa0d852257dc00c9a85b1a350e (diff) |
Adding preliminary let/flet support to SMT parser (Bug #51)
Diffstat (limited to 'src/parser/antlr_parser.cpp')
-rw-r--r-- | src/parser/antlr_parser.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 9b18eeb5a..cadff04ac 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -171,10 +171,8 @@ const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) { Expr AntlrParser::mkVar(const std::string& name, const Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; - Assert( !isDeclared(name) ); Expr expr = d_exprManager->mkVar(type, name); - d_varSymbolTable.bindName(name, expr); - Assert( isDeclared(name) ); + defineVar(name,expr); return expr; } @@ -188,6 +186,12 @@ AntlrParser::mkVars(const std::vector<std::string> names, return vars; } +void +AntlrParser::defineVar(const std::string& name, const Expr& val) { + Assert(!isDeclared(name)); + d_varSymbolTable.bindName(name,val); + Assert(isDeclared(name)); +} const Type* AntlrParser::newSort(const std::string& name) { |