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 | |
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')
-rw-r--r-- | src/parser/parser.cpp | 66 | ||||
-rw-r--r-- | src/parser/parser.h | 19 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 46 |
3 files changed, 86 insertions, 45 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; } diff --git a/src/parser/parser.h b/src/parser/parser.h index 1c492c843..bc0142089 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -23,6 +23,7 @@ #include <string> #include <set> +#include <list> #include "input.h" #include "parser_exception.h" @@ -124,6 +125,13 @@ class CVC4_PUBLIC Parser { /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; + /** + * "Preemption commands": extra commands implied by subterms that + * should be issued before the currently-being-parsed command is + * issued. Used to support SMT-LIBv2 ":named" attribute on terms. + */ + std::list<Command*> d_commandQueue; + /** Lookup a symbol in the given namespace. */ Expr getSymbol(const std::string& var_name, SymbolType type); @@ -315,12 +323,20 @@ public: const std::vector<Type> mkSorts(const std::vector<std::string>& names); - /** Add an operator to the current legal set. + /** + * Add an operator to the current legal set. * * @param kind the built-in operator to add */ void addOperator(Kind kind); + /** + * Preempt the next returned command with other ones; used to + * support the :named attribute in SMT-LIBv2, which implicitly + * inserts a new command before the current one. + */ + void preemptCommand(Command* cmd); + /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); @@ -334,7 +350,6 @@ public: bool isPredicate(const std::string& name); Command* nextCommand() throw(ParserException); - Expr nextExpression() throw(ParserException); inline void parseError(const std::string& msg) throw (ParserException) { d_input->parseError(msg); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4c447f9c1..ddfd1804e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -196,7 +196,7 @@ command returns [CVC4::Command* cmd] sortSymbol[t] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { - t = EXPR_MANAGER->mkFunctionType(sorts,t); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } PARSER_STATE->mkVar(name, t); $cmd = new DeclarationCommand(name,t); } @@ -215,7 +215,7 @@ command returns [CVC4::Command* cmd] ++i) { sorts.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts,t); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } PARSER_STATE->pushScope(); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = @@ -320,6 +320,7 @@ term[CVC4::Expr& expr] Kind kind; std::string name; std::vector<Expr> args; + SExpr sexpr; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -361,8 +362,9 @@ term[CVC4::Expr& expr] PARSER_STATE->getFunction(name) : PARSER_STATE->getVariable(name); args[0] = expr; - // TODO: check arity - expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); } + expr = MK_EXPR(isDefinedFunction ? + CVC4::kind::APPLY : + CVC4::kind::APPLY_UF, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -374,9 +376,38 @@ term[CVC4::Expr& expr] RPAREN_TOK { PARSER_STATE->popScope(); } - | /* a variable */ - symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { expr = PARSER_STATE->getVariable(name); } + /* a variable */ + | symbol[name,CHECK_DECLARED,SYM_VARIABLE] + { const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + if(isDefinedFunction) { + expr = MK_EXPR(CVC4::kind::APPLY, + PARSER_STATE->getFunction(name)); + } else { + expr = PARSER_STATE->getVariable(name); + } + } + + /* attributed expressions */ + | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK + { std::string attr = AntlrInput::tokenText($KEYWORD); + if(attr == ":named") { + name = sexpr.getValue(); + // FIXME ensure expr is a closed subterm + // check that sexpr is a fresh function symbol + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + // define it + Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + // bind name to expr with define-fun + Command* c = + new DefineFunctionCommand(func, std::vector<Expr>(), expr); + PARSER_STATE->preemptCommand(c); + } else { + std::stringstream ss; + ss << "Attribute `" << attr << "' not supported"; + PARSER_STATE->parseError(ss.str()); + } + } /* constants */ | INTEGER_LITERAL @@ -558,6 +589,7 @@ GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; ITE_TOK : 'ite'; LET_TOK : 'let'; +ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; SET_LOGIC_TOK : 'set-logic'; |