diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-09 09:49:35 +0000 |
commit | 0131e18b811bdf2825a1cde5a6d68d523b19aacc (patch) | |
tree | 9c4dcb4c1bf355b943926a5df85d3c3446750878 /src/parser/parser.cpp | |
parent | ec86769172d29ff7f5ed959866ecef339264552b (diff) |
support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary define-fun; several set-info, set-option, get-option, get-info improvementss
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 66 |
1 files changed, 30 insertions, 36 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 297a2d804..09e65526d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -103,7 +103,9 @@ bool Parser::isFunction(const std::string& name) { /* Returns true if name is bound to a defined function. */ bool Parser::isDefinedFunction(const std::string& name) { - return isFunction(name) && d_declScope.isBoundDefinedFunction(name); + // more permissive in type than isFunction(), because defined + // functions can be zero-ary and declared functions cannot. + return d_declScope.isBoundDefinedFunction(name); } /* Returns true if name is bound to a function returning boolean. */ @@ -286,50 +288,42 @@ void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); } +void Parser::preemptCommand(Command* cmd) { + d_commandQueue.push_back(cmd); +} + Command* Parser::nextCommand() throw(ParserException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; - if(!done()) { - try { - cmd = d_input->parseCommand(); - if(cmd == NULL) { - setDone(); - } - } catch(ParserException& e) { + if(!d_commandQueue.empty()) { + cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + if(cmd == NULL) { setDone(); - throw; - } catch(Exception& e) { - setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); } - } - Debug("parser") << "nextCommand() => " << cmd << std::endl; - return cmd; -} - -Expr Parser::nextExpression() throw(ParserException) { - Debug("parser") << "nextExpression()" << std::endl; - Expr result; - if(!done()) { - try { - result = d_input->parseExpr(); - if(result.isNull()) { + } else { + if(!done()) { + try { + cmd = d_input->parseCommand(); + d_commandQueue.push_back(cmd); + cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + if(cmd == NULL) { + setDone(); + } + } catch(ParserException& e) { setDone(); + throw; + } catch(Exception& e) { + setDone(); + stringstream ss; + ss << e; + parseError( ss.str() ); } - } catch(ParserException& e) { - setDone(); - throw; - } catch(Exception& e) { - setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); } } - Debug("parser") << "nextExpression() => " << result << std::endl; - return result; + Debug("parser") << "nextCommand() => " << cmd << std::endl; + return cmd; } |