diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/parser/smt2 | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 260 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 9 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 20 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 7 |
4 files changed, 209 insertions, 87 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6919c86c4..4c742adfc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -61,7 +61,7 @@ options { using namespace CVC4; using namespace CVC4::parser; -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Smt2*)LEXER->super) } @@ -91,7 +91,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Smt2*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() @@ -112,7 +112,7 @@ parseExpr returns [CVC4::Expr expr] ; /** - * Parses a command + * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ parseCommand returns [CVC4::Command* cmd] @@ -126,15 +126,18 @@ parseCommand returns [CVC4::Command* cmd] command returns [CVC4::Command* cmd] @declarations { std::string name; + std::vector<std::string> names; Expr expr; Type t; + std::vector<Expr> terms; std::vector<Type> sorts; + std::vector<std::pair<std::string, Type> > sortedVars; SExpr sexpr; } : /* set the logic */ SET_LOGIC_TOK SYMBOL { name = AntlrInput::tokenText($SYMBOL); - Debug("parser") << "set logic: '" << name << "' " << std::endl; + Debug("parser") << "set logic: '" << name << "'" << std::endl; if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) { PARSER_STATE->parseError("Only one set-logic is allowed."); } @@ -142,35 +145,113 @@ command returns [CVC4::Command* cmd] $cmd = new SetBenchmarkLogicCommand(name); } | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setInfo(name,sexpr); + PARSER_STATE->setInfo(name,sexpr); cmd = new SetInfoCommand(name,sexpr); } + | /* get-info */ + GET_INFO_TOK KEYWORD + { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD)); } + | /* set-option */ + SET_OPTION_TOK KEYWORD symbolicExpr[sexpr] + { name = AntlrInput::tokenText($KEYWORD); + PARSER_STATE->setOption(name,sexpr); + cmd = new SetOptionCommand(name,sexpr); } + | /* get-option */ + GET_OPTION_TOK KEYWORD + { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD)); } | /* sort declaration */ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL - { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; - if( AntlrInput::tokenToInteger(n) > 0 ) { - Unimplemented("Parameterized user sorts."); - } - PARSER_STATE->mkSort(name); + { Debug("parser") << "declare sort: '" << name + << "' arity=" << n << std::endl; + PARSER_STATE->mkSort(name, AntlrInput::tokenToUnsigned(n)); $cmd = new DeclarationCommand(name,EXPR_MANAGER->kindType()); } + | /* sort definition */ + DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] + LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK + { + PARSER_STATE->pushScope(); + for(std::vector<std::string>::const_iterator i = names.begin(), + iend = names.end(); + i != iend; + ++i) { + sorts.push_back(PARSER_STATE->mkSort(*i)); + } + } + sortSymbol[t] + { PARSER_STATE->popScope(); + // Do NOT call mkSort, since that creates a new sort! + // This name is not its own distinct sort, it's an alias. + PARSER_STATE->defineParameterizedType(name, sorts, t); + $cmd = new EmptyCommand; + } | /* function declaration */ - DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - LPAREN_TOK sortList[sorts] RPAREN_TOK + DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t] - { Debug("parser") << "declare fun: '" << name << "' " << std::endl; + { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts,t); } - PARSER_STATE->mkVar(name, t); - $cmd = new DeclarationCommand(name,t); } + PARSER_STATE->mkVar(name, t); + $cmd = new DeclarationCommand(name,t); } + | /* function definition */ + DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK + sortSymbol[t] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define fun: '" << name << "'" << std::endl; + if( sortedVars.size() > 0 ) { + std::vector<CVC4::Type> sorts; + sorts.reserve(sortedVars.size()); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVars.begin(), iend = sortedVars.end(); + i != iend; + ++i) { + sorts.push_back((*i).second); + } + t = EXPR_MANAGER->mkFunctionType(sorts,t); + } + PARSER_STATE->pushScope(); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVars.begin(), iend = sortedVars.end(); + i != iend; + ++i) { + PARSER_STATE->mkVar((*i).first, (*i).second); + } + } + term[expr] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + PARSER_STATE->mkVar(name, t); + $cmd = new DefineFunctionCommand(name,sortedVars,t,expr); + } + | /* value query */ + GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK + { if(terms.size() == 1) { + $cmd = new GetValueCommand(terms[0]); + } else { + CommandSequence* seq = new CommandSequence(); + for(std::vector<Expr>::const_iterator i = terms.begin(), + iend = terms.end(); + i != iend; + ++i) { + seq->addCommand(new GetValueCommand(*i)); + } + $cmd = seq; + } + } | /* assertion */ ASSERT_TOK term[expr] { cmd = new AssertCommand(expr); } | /* checksat */ - CHECKSAT_TOK + CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); } + | /* get-assertions */ + GET_ASSERTIONS_TOK + { cmd = new GetAssertionsCommand; } | EXIT_TOK - { // TODO: Explicitly represent exit as command? - cmd = 0; } + { cmd = NULL; } ; symbolicExpr[CVC4::SExpr& sexpr] @@ -187,12 +268,12 @@ symbolicExpr[CVC4::SExpr& sexpr] { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); } | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } - | LPAREN_TOK - (symbolicExpr[sexpr] { children.push_back(sexpr); } )* + | LPAREN_TOK + (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK { sexpr = SExpr(children); } ; - + /** * Matches a term. * @return the expression representing the formula @@ -202,11 +283,11 @@ term[CVC4::Expr& expr] Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; std::string name; - std::vector<Expr> args; -} + std::vector<Expr> args; +} : /* a built-in operator application */ - LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK - { + LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK + { if( kind == CVC4::kind::EQUAL && args.size() > 0 && args[0].getType() == EXPR_MANAGER->booleanType() ) { @@ -214,13 +295,13 @@ term[CVC4::Expr& expr] kind = CVC4::kind::IFF; } - if( !PARSER_STATE->strictModeEnabled() && - (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && + if( !PARSER_STATE->strictModeEnabled() && + (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); - } else if( CVC4::kind::isAssociative(kind) && + } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ expr = EXPR_MANAGER->mkAssociative(kind,args); @@ -233,7 +314,7 @@ term[CVC4::Expr& expr] } | /* A non-built-in function application */ - LPAREN_TOK + LPAREN_TOK functionSymbol[expr] { args.push_back(expr); } termList[args,expr] RPAREN_TOK @@ -241,18 +322,18 @@ term[CVC4::Expr& expr] { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } // | /* An ite expression */ - // LPAREN_TOK ITE_TOK + // LPAREN_TOK ITE_TOK // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // term[expr] - // { args.push_back(expr); } + // { args.push_back(expr); } // RPAREN_TOK // { expr = MK_EXPR(CVC4::kind::ITE, args); } | /* a let binding */ - LPAREN_TOK LET_TOK LPAREN_TOK + LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(); } ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK { PARSER_STATE->defineVar(name,expr); } )+ @@ -270,7 +351,8 @@ term[CVC4::Expr& expr] { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL - { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string + { // FIXME: This doesn't work because an SMT rational is not a + // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } | HEX_LITERAL @@ -290,8 +372,8 @@ term[CVC4::Expr& expr] * vector. * @param formulas the vector to fill with terms * @param expr an Expr reference for the elements of the sequence - */ -/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every + */ +/* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every * time through this rule. */ termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr] : ( term[expr] { formulas.push_back(expr); } )+ @@ -334,7 +416,7 @@ builtinOp[CVC4::Kind& kind] * @param check what kind of check to do with the symbol */ functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : symbol[name,check,SYM_VARIABLE] + : symbol[name,check,SYM_VARIABLE] ; /** @@ -348,23 +430,38 @@ functionSymbol[CVC4::Expr& fun] { PARSER_STATE->checkFunction(name); fun = PARSER_STATE->getVariable(name); } ; - + /** - * Matches a sequence of sort symbols and fills them into the given vector. + * Matches a sequence of sort symbols and fills them into the given + * vector. */ sortList[std::vector<CVC4::Type>& sorts] @declarations { Type t; } - : ( sortSymbol[t] { sorts.push_back(t); })* + : ( sortSymbol[t] { sorts.push_back(t); } )* + ; + +/** + * Matches a sequence of (variable,sort) symbol pairs and fills them + * into the given vector. + */ +sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars] +@declarations { + std::string name; + Type t; +} + : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK + { sortedVars.push_back(make_pair(name, t)); } + )* ; /** * Matches the sort symbol, which can be an arbitrary symbol. * @param check the check to perform on the name */ -sortName[std::string& name, CVC4::parser::DeclarationCheck check] - : symbol[name,check,SYM_SORT] +sortName[std::string& name, CVC4::parser::DeclarationCheck check] + : symbol[name,check,SYM_SORT] ; sortSymbol[CVC4::Type& t] @@ -372,15 +469,15 @@ sortSymbol[CVC4::Type& t] std::string name; std::vector<CVC4::Type> args; } - : sortName[name,CHECK_NONE] + : sortName[name,CHECK_NONE] { t = PARSER_STATE->getSort(name); } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK - { + { if( name == "Array" ) { if( args.size() != 2 ) { PARSER_STATE->parseError("Illegal array type."); } - t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); + t = EXPR_MANAGER->mkArrayType( args[0], args[1] ); } else { PARSER_STATE->parseError("Unhandled parameterized type."); } @@ -388,14 +485,27 @@ sortSymbol[CVC4::Type& t] ; /** + * Matches a list of symbols, with check and type arguments as for the + * symbol[] rule below. + */ +symbolList[std::vector<std::string>& names, + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] +@declarations { + std::string id; +} + : ( symbol[id,check,type] { names.push_back(id); } )* + ; + +/** * Matches an symbol and sets the string reference parameter id. * @param id string to hold the symbol * @param check what kinds of check to do on the symbol * @param type the intended namespace for the symbol */ symbol[std::string& id, - CVC4::parser::DeclarationCheck check, - CVC4::parser::SymbolType type] + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] : SYMBOL { id = AntlrInput::tokenText($SYMBOL); Debug("parser") << "symbol: " << id @@ -411,6 +521,10 @@ CHECKSAT_TOK : 'check-sat'; //DIFFICULTY_TOK : ':difficulty'; DECLARE_FUN_TOK : 'declare-fun'; DECLARE_SORT_TOK : 'declare-sort'; +DEFINE_FUN_TOK : 'define-fun'; +DEFINE_SORT_TOK : 'define-sort'; +GET_VALUE_TOK : 'get-value'; +GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; //FALSE_TOK : 'false'; ITE_TOK : 'ite'; @@ -421,6 +535,8 @@ RPAREN_TOK : ')'; //SAT_TOK : 'sat'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; +SET_OPTION_TOK : 'set-option'; +GET_OPTION_TOK : 'get-option'; //SMT_VERSION_TOK : ':smt-lib-version'; //SOURCE_TOK : ':source'; //STATUS_TOK : ':status'; @@ -456,8 +572,8 @@ TILDE_TOK : '~'; XOR_TOK : 'xor'; /** - * Matches a symbol from the input. A symbol is a "simple" symbol or a - * sequence of printable ASCII characters that starts and ends with | and + * Matches a symbol from the input. A symbol is a "simple" symbol or a + * sequence of printable ASCII characters that starts and ends with | and * does not otherwise contain |. */ SYMBOL @@ -473,11 +589,11 @@ KEYWORD : ':' SIMPLE_SYMBOL ; -/** Matches a "simple" symbol: a non-empty sequence of letters, digits and - * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a - * digit. +/** Matches a "simple" symbol: a non-empty sequence of letters, digits and + * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a + * digit. */ -fragment SIMPLE_SYMBOL +fragment SIMPLE_SYMBOL : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)* ; @@ -485,7 +601,7 @@ fragment SIMPLE_SYMBOL * Matches and skips whitespace in the input. */ WHITESPACE - : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN;; } + : (' ' | '\t' | '\f' | '\r' | '\n')+ { $channel = HIDDEN; } ; /** @@ -503,19 +619,19 @@ fragment NUMERAL char *start = (char*) GETCHARINDEX(); } : DIGIT+ - { Debug("parser-extra") << "NUMERAL: " - << (uintptr_t)start << ".." << GETCHARINDEX() + { Debug("parser-extra") << "NUMERAL: " + << (uintptr_t)start << ".." << GETCHARINDEX() << " strict? " << (bool)(PARSER_STATE->strictModeEnabled()) << " ^0? " << (bool)(*start == '0') << " len>1? " << (bool)(start < (char*)(GETCHARINDEX() - 1)) << std::endl; } - { !PARSER_STATE->strictModeEnabled() || + { !PARSER_STATE->strictModeEnabled() || *start != '0' || start == (char*)(GETCHARINDEX() - 1) }? ; - + /** - * Matches a decimal constant from the input. + * Matches a decimal constant from the input. */ DECIMAL_LITERAL : NUMERAL '.' DIGIT+ @@ -537,18 +653,18 @@ DECIMAL_LITERAL /** - * Matches a double quoted string literal. Escaping is supported, and escape - * character '\' has to be escaped. + * Matches a double quoted string literal. Escaping is supported, and + * escape character '\' has to be escaped. */ -STRING_LITERAL - : '"' (ESCAPE | ~('"'|'\\'))* '"' +STRING_LITERAL + : '"' (ESCAPE | ~('"'|'\\'))* '"' ; /** * Matches the comments and ignores them */ -COMMENT - : ';' (~('\n' | '\r'))* { $channel = HIDDEN;; } +COMMENT + : ';' (~('\n' | '\r'))* { $channel = HIDDEN; } ; @@ -556,9 +672,9 @@ COMMENT * Matches any letter ('a'-'z' and 'A'-'Z'). */ fragment -ALPHA - : 'a'..'z' - | 'A'..'Z' +ALPHA + : 'a'..'z' + | 'A'..'Z' ; /** @@ -568,10 +684,10 @@ fragment DIGIT : '0'..'9'; fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; -/** Matches the characters that may appear in a "symbol" (i.e., an identifier) +/** Matches the characters that may appear in a "symbol" (i.e., an identifier) */ -fragment SYMBOL_CHAR - : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' +fragment SYMBOL_CHAR + : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' | '&' | '^' | '<' | '>' | '@' ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e704d027d..308f45ed0 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -98,7 +98,8 @@ bool Smt2::logicIsSet() { } /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * Sets the logic for the current benchmark. Declares any logic and + * theory symbols. * * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) @@ -124,7 +125,7 @@ void Smt2::setLogic(const std::string& name) { case Smt::QF_NIA: addTheory(THEORY_INTS); break; - + case Smt::QF_LRA: case Smt::QF_RDL: addTheory(THEORY_REALS); @@ -162,5 +163,9 @@ void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } +void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { + // TODO: ??? +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index fe152a7f6..6398fa735 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -57,28 +57,28 @@ public: * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ - void - addTheory(Theory theory); + void addTheory(Theory theory); - bool - logicIsSet(); + bool logicIsSet(); /** - * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * Sets the logic for the current benchmark. Declares any logic and + * theory symbols. * * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - void - setLogic(const std::string& name); + void setLogic(const std::string& name); - void - setInfo(const std::string& flag, const SExpr& sexpr); + void setInfo(const std::string& flag, const SExpr& sexpr); + + void setOption(const std::string& flag, const SExpr& sexpr); private: void addArithmeticOperators(); -}; +};/* class Smt2 */ + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 320f5ab75..02a480971 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -64,7 +64,8 @@ public: /** * Create a string input. * - * @param exprManager the manager to use when building expressions from the input + * @param exprManager the manager to use when building expressions + * from the input * @param input the string to read * @param name the "filename" to use when reporting errors */ @@ -81,7 +82,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* parseCommand() + Command* parseCommand() throw(ParserException, TypeCheckingException, AssertionException); /** @@ -90,7 +91,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr parseExpr() + Expr parseExpr() throw(ParserException, TypeCheckingException, AssertionException); };/* class Smt2Input */ |