From ed25d7b7527691442ab48d02353e20c87ab8e2da Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 1 Apr 2010 19:55:45 +0000 Subject: [PATCH] Parser tweaks to address review Private members of Input moved to new class ParserState --- src/main/main.cpp | 12 +- src/parser/Makefile.am | 2 + src/parser/antlr_input.cpp | 28 +-- src/parser/cvc/Cvc.g | 23 +-- src/parser/input.cpp | 284 ++++-------------------------- src/parser/input.h | 251 +++++---------------------- src/parser/parser_state.cpp | 234 +++++++++++++++++++++++++ src/parser/parser_state.h | 258 ++++++++++++++++++++++++++++ src/parser/smt/Smt.g | 37 ++-- test/unit/Makefile.am | 2 +- test/unit/parser/parser_white.h | 295 ++++++++++++++++++++++++++++++++ 11 files changed, 918 insertions(+), 508 deletions(-) create mode 100644 src/parser/parser_state.cpp create mode 100644 src/parser/parser_state.h create mode 100644 test/unit/parser/parser_white.h diff --git a/src/main/main.cpp b/src/main/main.cpp index 174ab4b7f..5e1f4be93 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -146,23 +146,23 @@ int runCvc4(int argc, char* argv[]) { } // Create the parser - Input* parser; - istream* input = NULL; + Input* input; + /* TODO: Hack ANTLR3 to support input from streams */ // if(inputFromStdin) { // parser = Parser::getNewParser(&exprMgr, options.lang, cin, ""); // } else { - parser = Input::newFileParser(&exprMgr, options.lang, argv[firstArgIndex], + input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex], options.memoryMap); // } if(!options.semanticChecks) { - parser->disableChecks(); + input->disableChecks(); } // Parse and execute commands until we are done Command* cmd; - while((cmd = parser->parseNextCommand())) { + while((cmd = input->parseNextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); } @@ -170,7 +170,7 @@ int runCvc4(int argc, char* argv[]) { } // Remove the parser - delete parser; + delete input; delete input; switch(lastResult.asSatisfiabilityResult().isSAT()) { diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 5d8b75f38..1aaf7ab69 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -46,5 +46,7 @@ libcvc4parser_noinst_la_SOURCES = \ memory_mapped_input_buffer.cpp \ parser_options.h \ parser_exception.h \ + parser_state.h \ + parser_state.cpp \ symbol_table.h diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 16f10cd93..0d6f63812 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -17,15 +17,17 @@ #include #include +#include "antlr_input.h" +#include "bounded_token_buffer.h" +#include "bounded_token_factory.h" +#include "memory_mapped_input_buffer.h" +#include "parser_exception.h" +#include "parser_state.h" + #include "util/output.h" #include "util/Assert.h" #include "expr/command.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/bounded_token_buffer.h" -#include "parser/bounded_token_factory.h" -#include "parser/memory_mapped_input_buffer.h" -#include "parser/parser_exception.h" using namespace std; using namespace CVC4; @@ -92,12 +94,14 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { void AntlrInput::parseError(const std::string& message) throw (ParserException) { - Debug("parser") << "Throwing exception: " << getFilename() << ":" + Debug("parser") << "Throwing exception: " + << getParserState()->getFilename() << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; - throw ParserException(message, getFilename(), d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); + throw ParserException(message, getParserState()->getFilename(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); } void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { @@ -268,11 +272,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // Now get ready to throw an exception pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super); AlwaysAssert(parser!=NULL); - AntlrInput *input = (AntlrInput*)(parser->super); - AlwaysAssert(input!=NULL); + ParserState *parserState = (ParserState*)(parser->super); + AlwaysAssert(parserState!=NULL); // Call the error display routine - input->parseError(ss.str()); + parserState->parseError(ss.str()); } void AntlrInput::setLexer(pANTLR3_LEXER pLexer) { @@ -304,7 +308,7 @@ void AntlrInput::setParser(pANTLR3_PARSER pParser) { // We could also use @parser::context to add a field to the generated parser, but then // it would have to be declared separately in every input's grammar and we'd have to // pass it in as an address anyway. - d_parser->super = this; + d_parser->super = getParserState(); d_parser->rec->reportError = &reportError; } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index feb2e6d35..8b8f251ae 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -48,7 +48,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/input.h" +#include "parser/parser_state.h" namespace CVC4 { class Expr; @@ -60,6 +60,7 @@ namespace CVC4 { #include "expr/kind.h" #include "expr/type.h" #include "parser/antlr_input.h" +#include "parser/parser_state.h" #include "util/output.h" #include @@ -68,10 +69,10 @@ 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 ANTLR_INPUT -#define ANTLR_INPUT ((Input*)PARSER->super) +#undef PARSER_STATE +#define PARSER_STATE ((ParserState*)PARSER->super) #undef EXPR_MANAGER -#define EXPR_MANAGER ANTLR_INPUT->getExprManager() +#define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST @@ -136,10 +137,10 @@ declType[CVC4::Type*& t, std::vector& idList] } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK - { ANTLR_INPUT->newSorts(idList); + { PARSER_STATE->newSorts(idList); t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ - type[t] { ANTLR_INPUT->mkVars(idList,t); } + type[t] { PARSER_STATE->mkVars(idList,t); } ; /** @@ -190,7 +191,7 @@ identifier[std::string& id, CVC4::parser::SymbolType type] : IDENTIFIER { id = AntlrInput::tokenText($IDENTIFIER); - ANTLR_INPUT->checkDeclaration(id, check, type); } + PARSER_STATE->checkDeclaration(id, check, type); } ; /** @@ -215,7 +216,7 @@ typeSymbol[CVC4::Type*& t] Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; } : identifier[id,CHECK_DECLARED,SYM_SORT] - { t = ANTLR_INPUT->getSort(id); } + { t = PARSER_STATE->getSort(id); } ; /** @@ -376,7 +377,7 @@ term[CVC4::Expr& f] | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { f = ANTLR_INPUT->getVariable(name); } + { f = PARSER_STATE->getVariable(name); } ; /** @@ -420,8 +421,8 @@ functionSymbol[CVC4::Expr& f] std::string name; } : identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { ANTLR_INPUT->checkFunction(name); - f = ANTLR_INPUT->getVariable(name); } + { PARSER_STATE->checkFunction(name); + f = PARSER_STATE->getVariable(name); } ; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 3b7b322ca..4d5f348d8 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -13,33 +13,34 @@ ** Parser implementation. **/ -#include -#include #include #include "input.h" +#include "parser_exception.h" +#include "parser_options.h" +#include "parser_state.h" #include "expr/command.h" #include "expr/expr.h" -#include "expr/kind.h" -#include "expr/type.h" -#include "util/output.h" -#include "util/Assert.h" -#include "parser/parser_exception.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" +#include "util/output.h" +#include "util/Assert.h" using namespace std; -using namespace CVC4::kind; namespace CVC4 { namespace parser { -void Input::setDone(bool done) { - d_done = done; +bool Input::done() const { + return d_parserState->done(); } -bool Input::done() const { - return d_done; +void Input::disableChecks() { + d_parserState->disableChecks(); +} + +void Input::enableChecks() { + d_parserState->enableChecks(); } Command* Input::parseNextCommand() throw (ParserException) { @@ -49,10 +50,10 @@ Command* Input::parseNextCommand() throw (ParserException) { try { cmd = doParseCommand(); if(cmd == NULL) { - setDone(); + d_parserState->setDone(); } } catch(ParserException& e) { - setDone(); + d_parserState->setDone(); throw ParserException(e.toString()); } } @@ -67,9 +68,9 @@ Expr Input::parseNextExpression() throw (ParserException) { try { result = doParseExpr(); if(result.isNull()) - setDone(); + d_parserState->setDone(); } catch(ParserException& e) { - setDone(); + d_parserState->setDone(); throw ParserException(e.toString()); } } @@ -77,271 +78,52 @@ Expr Input::parseNextExpression() throw (ParserException) { return result; } -Input::~Input() { +Input::Input(ExprManager* exprManager, const std::string& filename) { + d_parserState = new ParserState(exprManager,filename,this); } -Input::Input(ExprManager* exprManager, const std::string& filename) : - d_exprManager(exprManager), - d_filename(filename), - d_done(false), - d_checksEnabled(true) { +Input::~Input() { + delete d_parserState; } -Input* Input::newFileParser(ExprManager* em, InputLanguage lang, - const std::string& filename, bool useMmap) { +Input* Input::newFileInput(ExprManager* em, InputLanguage lang, + const std::string& filename, bool useMmap) { - Input* parser = 0; + Input* input = 0; switch(lang) { case LANG_CVC4: - parser = new CvcInput(em,filename,useMmap); + input = new CvcInput(em,filename,useMmap); break; case LANG_SMTLIB: - parser = new SmtInput(em,filename,useMmap); + input = new SmtInput(em,filename,useMmap); break; default: Unhandled(lang); } - return parser; -} - -/* -Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, - istream& input, string filename) { - antlr::CharBuffer* inputBuffer = new CharBuffer(input); - return getNewParser(em, lang, inputBuffer, filename); -} -*/ - -/* -Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, - std::istream& input, const std::string& name) { - Parser* parser = 0; - - switch(lang) { - case LANG_CVC4: { - antlrLexer = new AntlrCvcLexer(*inputBuffer); - antlrParser = new AntlrCvcParser(*antlrLexer); - break; - } - case LANG_SMTLIB: - parser = new Smt(em,input,name); - break; - - default: - Unhandled("Unknown Input language!"); - } - return parser; + return input; } -*/ -Input* Input::newStringParser(ExprManager* em, InputLanguage lang, - const std::string& input, const std::string& name) { - Input* parser = 0; +Input* Input::newStringInput(ExprManager* em, InputLanguage lang, + const std::string& str, const std::string& name) { + Input* input = 0; switch(lang) { case LANG_CVC4: { - parser = new CvcInput(em,input,name); + input = new CvcInput(em,str,name); break; } case LANG_SMTLIB: - parser = new SmtInput(em,input,name); + input = new SmtInput(em,str,name); break; default: Unhandled(lang); } - return parser; + return input; } -Expr Input::getSymbol(const std::string& name, SymbolType type) { - Assert( isDeclared(name, type) ); - - - switch( type ) { - - case SYM_VARIABLE: // Functions share var namespace - return d_varSymbolTable.getObject(name); - - default: - Unhandled(type); - } -} - - -Expr Input::getVariable(const std::string& name) { - return getSymbol(name, SYM_VARIABLE); -} - -Type* -Input::getType(const std::string& var_name, - SymbolType type) { - Assert( isDeclared(var_name, type) ); - Type* t = getSymbol(var_name,type).getType(); - return t; -} - -Type* Input::getSort(const std::string& name) { - Assert( isDeclared(name, SYM_SORT) ); - Type* t = d_sortTable.getObject(name); - return t; -} - -/* Returns true if name is bound to a boolean variable. */ -bool Input::isBoolean(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); -} - -/* Returns true if name is bound to a function. */ -bool Input::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); -} - -/* Returns true if name is bound to a function returning boolean. */ -bool Input::isPredicate(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); -} - -Expr -Input::mkVar(const std::string& name, Type* type) { - Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(type, name); - defineVar(name,expr); - return expr; -} - -const std::vector -Input::mkVars(const std::vector names, - Type* type) { - std::vector vars; - for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i], type)); - } - return vars; -} - -void -Input::defineVar(const std::string& name, const Expr& val) { - Assert(!isDeclared(name)); - d_varSymbolTable.bindName(name,val); - Assert(isDeclared(name)); -} - -void -Input::undefineVar(const std::string& name) { - Assert(isDeclared(name)); - d_varSymbolTable.unbindName(name); - Assert(!isDeclared(name)); -} - -void -Input::setLogic(const std::string& name) { - if( name == "QF_UF" ) { - newSort("U"); - } else { - Unhandled(name); - } -} - -Type* -Input::newSort(const std::string& name) { - Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name, SYM_SORT) ) ; - Type* type = d_exprManager->mkSort(name); - d_sortTable.bindName(name, type); - Assert( isDeclared(name, SYM_SORT) ) ; - return type; -} - -const std::vector -Input::newSorts(const std::vector& names) { - std::vector types; - for(unsigned i = 0; i < names.size(); ++i) { - types.push_back(newSort(names[i])); - } - return types; -} - -bool Input::isDeclared(const std::string& name, SymbolType type) { - switch(type) { - case SYM_VARIABLE: - return d_varSymbolTable.isBound(name); - case SYM_SORT: - return d_sortTable.isBound(name); - default: - Unhandled(type); - } -} - -void Input::checkDeclaration(const std::string& varName, - DeclarationCheck check, - SymbolType type) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - switch(check) { - case CHECK_DECLARED: - if( !isDeclared(varName, type) ) { - parseError("Symbol " + varName + " not declared"); - } - break; - - case CHECK_UNDECLARED: - if( isDeclared(varName, type) ) { - parseError("Symbol " + varName + " previously declared"); - } - break; - - case CHECK_NONE: - break; - - default: - Unhandled(check); - } -} - -void Input::checkFunction(const std::string& name) - throw (ParserException) { - if( d_checksEnabled && !isFunction(name) ) { - parseError("Expecting function symbol, found '" + name + "'"); - } -} - -void Input::checkArity(Kind kind, unsigned int numArgs) - throw (ParserException) { - if(!d_checksEnabled) { - return; - } - - unsigned int min = d_exprManager->minArity(kind); - unsigned int max = d_exprManager->maxArity(kind); - - if( numArgs < min || numArgs > max ) { - stringstream ss; - ss << "Expecting "; - if( numArgs < min ) { - ss << "at least " << min << " "; - } else { - ss << "at most " << max << " "; - } - ss << "arguments for operator '" << kind << "', "; - ss << "found " << numArgs; - parseError(ss.str()); - } -} - -void Input::enableChecks() { - d_checksEnabled = true; -} - -void Input::disableChecks() { - d_checksEnabled = false; -} - - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index ad888c6cc..0e924364d 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -15,101 +15,44 @@ #include "cvc4parser_public.h" -#ifndef __CVC4__PARSER__PARSER_H -#define __CVC4__PARSER__PARSER_H +#ifndef __CVC4__PARSER__INPUT_H +#define __CVC4__PARSER__INPUT_H #include -#include #include "expr/expr.h" -#include "expr/kind.h" #include "parser/parser_exception.h" #include "parser/parser_options.h" -#include "parser/symbol_table.h" -#include "util/Assert.h" namespace CVC4 { // Forward declarations -class BooleanType; class ExprManager; class Command; -class FunctionType; -class KindType; class Type; namespace parser { -/** Types of check for the symols */ -enum DeclarationCheck { - /** Enforce that the symbol has been declared */ - CHECK_DECLARED, - /** Enforce that the symbol has not been declared */ - CHECK_UNDECLARED, - /** Don't check anything */ - CHECK_NONE -}; - -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(DeclarationCheck check) { - switch(check) { - case CHECK_NONE: return "CHECK_NONE"; - case CHECK_DECLARED: return "CHECK_DECLARED"; - case CHECK_UNDECLARED: return "CHECK_UNDECLARED"; - default: Unreachable(); - } -} - -/** - * Types of symbols. Used to define namespaces. - */ -enum SymbolType { - /** Variables */ - SYM_VARIABLE, - /** Sorts */ - SYM_SORT -}; - -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(SymbolType type) { - switch(type) { - case SYM_VARIABLE: return "SYM_VARIABLE"; - case SYM_SORT: return "SYM_SORT"; - default: Unreachable(); - } -} +class ParserState; /** - * The parser. The parser should be obtained by calling the static methods - * getNewParser, and should be deleted when done. + * An input to be parsed. This class serves two purposes: to the client, it provides + * the methods parseNextCommand and parseNextExpression to + * extract a stream of Command's and Expr's from the input; + * to the parser, it provides a repository for state data, like the variable symbol + * table, and a variety of convenience functions for updating and checking the state. * - * This class includes convenience methods for interacting with the ExprManager - * from within a grammar. + * An Input should be created using the static factory methods, + * e.g., newFileParser and newStringInput, and + * should be deleted when done. */ class CVC4_PUBLIC Input { + friend class ParserState; /** Whether to de-allocate the input */ -// bool d_deleteInput; - - /** The expression manager */ - ExprManager* d_exprManager; - - /** The symbol table lookup */ - SymbolTable d_varSymbolTable; - - /** The sort table */ - SymbolTable d_sortTable; - - /** The name of the input file. */ - std::string d_filename; - - /** Are we done */ - bool d_done; + // bool d_deleteInput; - /** Are semantic checks enabled during parsing? */ - bool d_checksEnabled; + ParserState *d_parserState; public: @@ -123,17 +66,17 @@ public: /** * Destructor. */ - ~Input(); + virtual ~Input(); - /** Create a parser for the given file. + /** Create an input for the given file. * * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param filename the input filename */ - static Input* newFileParser(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false); + static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false); - /** Create a parser for the given input stream. + /** Create an input for the given stream. * * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language @@ -142,19 +85,27 @@ public: */ //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name); - /** Create a parser for the given input string + /** Create an input for the given string * * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name); + static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name); - /** Get the ExprManager associated with this input. */ - inline ExprManager* getExprManager() const { - return d_exprManager; - } + /** + * Check if we are done -- either the end of input has been reached, or some + * error has been encountered. + * @return true if parser is done + */ + bool done() const; + + /** Enable semantic checks during parsing. */ + void enableChecks(); + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks(); /** * Parse the next command of the input. If EOF is encountered a EmptyCommand @@ -172,127 +123,6 @@ public: */ Expr parseNextExpression() throw(ParserException); - /** - * Check if we are done -- either the end of input has been reached, or some - * error has been encountered. - * @return true if parser is done - */ - bool done() const; - - /** Enable semantic checks during parsing. */ - void enableChecks(); - - /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ - void disableChecks(); - - /** Get the name of the input file. */ - inline const std::string getFilename() { - return d_filename; - } - - /** - * Sets the logic for the current benchmark. Declares any logic symbols. - * - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ - void setLogic(const std::string& name); - - /** - * Returns a variable, given a name and a type. - * @param var_name the name of the variable - * @return the variable expression - */ - Expr getVariable(const std::string& var_name); - - /** - * Returns a sort, given a name - */ - Type* getSort(const std::string& sort_name); - - /** - * Checks if a symbol has been declared. - * @param name the symbol name - * @param type the symbol type - * @return true iff the symbol has been declared with the given type - */ - bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); - - /** - * Checks if the declaration policy we want to enforce holds - * for the given symbol. - * @param name the symbol to check - * @param check the kind of check to perform - * @param type the type of the symbol - * @throws ParserException if checks are enabled and the check fails - */ - void checkDeclaration(const std::string& name, - DeclarationCheck check, - SymbolType type = SYM_VARIABLE) - throw (ParserException); - - /** - * Checks whether the given name is bound to a function. - * @param name the name to check - * @throws ParserException if checks are enabled and name is not bound to a function - */ - void checkFunction(const std::string& name) throw (ParserException); - - /** - * Check that kind can accept numArgs arguments. - * @param kind the built-in operator to check - * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator kind cannot be - * applied to numArgs arguments. - */ - void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); - - /** - * Returns the type for the variable with the given name. - * @param name the symbol to lookup - * @param type the (namespace) type of the symbol - */ - Type* getType(const std::string& var_name, - SymbolType type = SYM_VARIABLE); - - /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, Type* type); - - /** Create a set of new CVC4 variable expressions of the given - type. */ - const std::vector - mkVars(const std::vector names, - Type* type); - - - /** Create a new variable definition (e.g., from a let binding). */ - void defineVar(const std::string& name, const Expr& val); - /** Remove a variable definition (e.g., from a let binding). */ - void undefineVar(const std::string& name); - - /** - * Creates a new sort with the given name. - */ - Type* newSort(const std::string& name); - - /** - * Creates a new sorts with the given names. - */ - const std::vector - newSorts(const std::vector& names); - - /** Is the symbol bound to a boolean variable? */ - bool isBoolean(const std::string& name); - - /** Is the symbol bound to a function? */ - bool isFunction(const std::string& name); - - /** Is the symbol bound to a predicate? */ - bool isPredicate(const std::string& name); - - /** Throws a ParserException with the given error message. - * Implementations should fill in the ParserException with - * line number information, etc. */ - virtual void parseError(const std::string& msg) throw (ParserException) = 0; protected: @@ -313,17 +143,20 @@ protected: */ virtual Expr doParseExpr() throw(ParserException) = 0; -private: + inline ParserState* getParserState() const { + return d_parserState; + } - /** Sets the done flag */ - void setDone(bool done = true); +private: - /** Lookup a symbol in the given namespace. */ - Expr getSymbol(const std::string& var_name, SymbolType type); + /** Throws a ParserException with the given error message. + * Implementations should fill in the ParserException with + * line number information, etc. */ + virtual void parseError(const std::string& msg) throw (ParserException) = 0; -}; // end of class Parser +}; // end of class Input }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__PARSER_H */ +#endif /* __CVC4__PARSER__INPUT_H */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp new file mode 100644 index 000000000..9e8ff577e --- /dev/null +++ b/src/parser/parser_state.cpp @@ -0,0 +1,234 @@ +/********************* */ +/** parser_state.cpp + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Parser state implementation. + **/ + +#include +#include +#include + +#include "input.h" +#include "expr/command.h" +#include "expr/expr.h" +#include "expr/kind.h" +#include "expr/type.h" +#include "util/output.h" +#include "util/Assert.h" +#include "parser/parser_exception.h" +#include "parser/symbol_table.h" +#include "parser/cvc/cvc_input.h" +#include "parser/smt/smt_input.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace parser { + +ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) : + d_exprManager(exprManager), + d_input(input), + d_filename(filename), + d_done(false), + d_checksEnabled(true) { +} + +Expr ParserState::getSymbol(const std::string& name, SymbolType type) { + Assert( isDeclared(name, type) ); + + + switch( type ) { + + case SYM_VARIABLE: // Functions share var namespace + return d_varTable.getObject(name); + + default: + Unhandled(type); + } +} + + +Expr ParserState::getVariable(const std::string& name) { + return getSymbol(name, SYM_VARIABLE); +} + +Type* +ParserState::getType(const std::string& var_name, + SymbolType type) { + Assert( isDeclared(var_name, type) ); + Type* t = getSymbol(var_name,type).getType(); + return t; +} + +Type* ParserState::getSort(const std::string& name) { + Assert( isDeclared(name, SYM_SORT) ); + Type* t = d_sortTable.getObject(name); + return t; +} + +/* Returns true if name is bound to a boolean variable. */ +bool ParserState::isBoolean(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name)->isBoolean(); +} + +/* Returns true if name is bound to a function. */ +bool ParserState::isFunction(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); +} + +/* Returns true if name is bound to a function returning boolean. */ +bool ParserState::isPredicate(const std::string& name) { + return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); +} + +Expr +ParserState::mkVar(const std::string& name, Type* type) { + Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; + Expr expr = d_exprManager->mkVar(type, name); + defineVar(name,expr); + return expr; +} + +const std::vector +ParserState::mkVars(const std::vector names, + Type* type) { + std::vector vars; + for(unsigned i = 0; i < names.size(); ++i) { + vars.push_back(mkVar(names[i], type)); + } + return vars; +} + +void +ParserState::defineVar(const std::string& name, const Expr& val) { + Assert(!isDeclared(name)); + d_varTable.bindName(name,val); + Assert(isDeclared(name)); +} + +void +ParserState::undefineVar(const std::string& name) { + Assert(isDeclared(name)); + d_varTable.unbindName(name); + Assert(!isDeclared(name)); +} + +void +ParserState::setLogic(const std::string& name) { + if( name == "QF_UF" ) { + newSort("U"); + } else { + Unhandled(name); + } +} + +Type* +ParserState::newSort(const std::string& name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Assert( !isDeclared(name, SYM_SORT) ) ; + Type* type = d_exprManager->mkSort(name); + d_sortTable.bindName(name, type); + Assert( isDeclared(name, SYM_SORT) ) ; + return type; +} + +const std::vector +ParserState::newSorts(const std::vector& names) { + std::vector types; + for(unsigned i = 0; i < names.size(); ++i) { + types.push_back(newSort(names[i])); + } + return types; +} + +bool ParserState::isDeclared(const std::string& name, SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return d_varTable.isBound(name); + case SYM_SORT: + return d_sortTable.isBound(name); + default: + Unhandled(type); + } +} + +void ParserState::checkDeclaration(const std::string& varName, + DeclarationCheck check, + SymbolType type) + throw (ParserException) { + if(!d_checksEnabled) { + return; + } + + switch(check) { + case CHECK_DECLARED: + if( !isDeclared(varName, type) ) { + parseError("Symbol " + varName + " not declared"); + } + break; + + case CHECK_UNDECLARED: + if( isDeclared(varName, type) ) { + parseError("Symbol " + varName + " previously declared"); + } + break; + + case CHECK_NONE: + break; + + default: + Unhandled(check); + } +} + +void ParserState::checkFunction(const std::string& name) + throw (ParserException) { + if( d_checksEnabled && !isFunction(name) ) { + parseError("Expecting function symbol, found '" + name + "'"); + } +} + +void ParserState::checkArity(Kind kind, unsigned int numArgs) + throw (ParserException) { + if(!d_checksEnabled) { + return; + } + + unsigned int min = d_exprManager->minArity(kind); + unsigned int max = d_exprManager->maxArity(kind); + + if( numArgs < min || numArgs > max ) { + stringstream ss; + ss << "Expecting "; + if( numArgs < min ) { + ss << "at least " << min << " "; + } else { + ss << "at most " << max << " "; + } + ss << "arguments for operator '" << kind << "', "; + ss << "found " << numArgs; + parseError(ss.str()); + } +} + +void ParserState::enableChecks() { + d_checksEnabled = true; +} + +void ParserState::disableChecks() { + d_checksEnabled = false; +} + + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h new file mode 100644 index 000000000..3130e1f46 --- /dev/null +++ b/src/parser/parser_state.h @@ -0,0 +1,258 @@ +/********************* */ +/** parser_state.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** A collection of state for use by parser implementations. + **/ + +#ifndef __CVC4__PARSER__PARSER_STATE_H_ +#define __CVC4__PARSER__PARSER_STATE_H_ + +#include + +#include "expr/expr.h" +#include "expr/kind.h" +#include "parser/input.h" +#include "parser/parser_exception.h" +#include "parser/parser_options.h" +#include "parser/symbol_table.h" +#include "util/Assert.h" + +namespace CVC4 { + +// Forward declarations +class BooleanType; +class ExprManager; +class Command; +class FunctionType; +class KindType; +class Type; + +namespace parser { + +/** Types of check for the symols */ +enum DeclarationCheck { + /** Enforce that the symbol has been declared */ + CHECK_DECLARED, + /** Enforce that the symbol has not been declared */ + CHECK_UNDECLARED, + /** Don't check anything */ + CHECK_NONE +}; + +/** Returns a string representation of the given object (for + debugging). */ +inline std::string toString(DeclarationCheck check) { + switch(check) { + case CHECK_NONE: + return "CHECK_NONE"; + case CHECK_DECLARED: + return "CHECK_DECLARED"; + case CHECK_UNDECLARED: + return "CHECK_UNDECLARED"; + default: + Unreachable(); + } +} + +/** + * Types of symbols. Used to define namespaces. + */ +enum SymbolType { + /** Variables */ + SYM_VARIABLE, + /** Sorts */ + SYM_SORT +}; + +/** Returns a string representation of the given object (for + debugging). */ +inline std::string toString(SymbolType type) { + switch(type) { + case SYM_VARIABLE: + return "SYM_VARIABLE"; + case SYM_SORT: + return "SYM_SORT"; + default: + Unreachable(); + } +} + +class ParserState { + + /** The expression manager */ + ExprManager *d_exprManager; + + /** The input that we're parsing. */ + Input *d_input; + + /** The symbol table lookup */ + SymbolTable d_varTable; + + /** The sort table */ + SymbolTable d_sortTable; + + /** The name of the input file. */ + std::string d_filename; + + /** Are we done */ + bool d_done; + + /** Are semantic checks enabled during parsing? */ + bool d_checksEnabled; + + + /** Lookup a symbol in the given namespace. */ + Expr getSymbol(const std::string& var_name, SymbolType type); + +public: + ParserState(ExprManager* exprManager, const std::string& filename, Input* input); + + /** Get the associated ExprManager. */ + inline ExprManager* getExprManager() const { + return d_exprManager; + } + + /** Get the associated input. */ + inline Input* getInput() const { + return d_input; + } + + /** + * Check if we are done -- either the end of input has been reached, or some + * error has been encountered. + * @return true if parser is done + */ + inline bool done() const { + return d_done; + } + + /** Sets the done flag */ + inline void setDone(bool done = true) { + d_done = done; + } + + /** Enable semantic checks during parsing. */ + void enableChecks(); + + /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */ + void disableChecks(); + + /** Get the name of the input file. */ + inline const std::string getFilename() { + return d_filename; + } + + /** + * Sets the logic for the current benchmark. Declares any logic symbols. + * + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ + void setLogic(const std::string& name); + + /** + * Returns a variable, given a name and a type. + * @param var_name the name of the variable + * @return the variable expression + */ + Expr getVariable(const std::string& var_name); + + /** + * Returns a sort, given a name + */ + Type* getSort(const std::string& sort_name); + + /** + * Checks if a symbol has been declared. + * @param name the symbol name + * @param type the symbol type + * @return true iff the symbol has been declared with the given type + */ + bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE); + + /** + * Checks if the declaration policy we want to enforce holds + * for the given symbol. + * @param name the symbol to check + * @param check the kind of check to perform + * @param type the type of the symbol + * @throws ParserException if checks are enabled and the check fails + */ + void checkDeclaration(const std::string& name, DeclarationCheck check, + SymbolType type = SYM_VARIABLE) throw (ParserException); + + /** + * Checks whether the given name is bound to a function. + * @param name the name to check + * @throws ParserException if checks are enabled and name is not bound to a function + */ + void checkFunction(const std::string& name) throw (ParserException); + + /** + * Check that kind can accept numArgs arguments. + * @param kind the built-in operator to check + * @param numArgs the number of actual arguments + * @throws ParserException if checks are enabled and the operator kind cannot be + * applied to numArgs arguments. + */ + void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); + + /** + * Returns the type for the variable with the given name. + * @param name the symbol to lookup + * @param type the (namespace) type of the symbol + */ + Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); + + /** Create a new CVC4 variable expression of the given type. */ + Expr mkVar(const std::string& name, Type* type); + + /** Create a set of new CVC4 variable expressions of the given + type. */ + const std::vector + mkVars(const std::vector names, Type* type); + + /** Create a new variable definition (e.g., from a let binding). */ + void defineVar(const std::string& name, const Expr& val); + /** Remove a variable definition (e.g., from a let binding). */ + void undefineVar(const std::string& name); + + /** + * Creates a new sort with the given name. + */ + Type* newSort(const std::string& name); + + /** + * Creates a new sorts with the given names. + */ + const std::vector + newSorts(const std::vector& names); + + /** Is the symbol bound to a boolean variable? */ + bool isBoolean(const std::string& name); + + /** Is the symbol bound to a function? */ + bool isFunction(const std::string& name); + + /** Is the symbol bound to a predicate? */ + bool isPredicate(const std::string& name); + + inline void parseError(const std::string& msg) throw (ParserException) { + d_input->parseError(msg); + } + +}; // class ParserState + +} // namespace parser + +} // namespace CVC4 + +#endif /* __CVC4__PARSER__PARSER_STATE_H_ */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 86c1b015d..9bcee54fd 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -48,7 +48,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/input.h" +#include "parser/parser_state.h" namespace CVC4 { class Expr; @@ -60,6 +60,7 @@ namespace CVC4 { #include "expr/kind.h" #include "expr/type.h" #include "parser/antlr_input.h" +#include "parser/parser_state.h" #include "util/output.h" #include @@ -68,10 +69,10 @@ 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 ANTLR_INPUT -#define ANTLR_INPUT ((Input*)PARSER->super) +#undef PARSER_STATE +#define PARSER_STATE ((ParserState*)PARSER->super) #undef EXPR_MANAGER -#define EXPR_MANAGER ANTLR_INPUT->getExprManager() +#define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST @@ -129,7 +130,7 @@ benchAttribute returns [CVC4::Command* smt_command] Expr expr; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { ANTLR_INPUT->setLogic(name); + { PARSER_STATE->setLogic(name); smt_command = new SetBenchmarkLogicCommand(name); } | ASSUMPTION_TOK annotatedFormula[expr] { smt_command = new AssertCommand(expr); } @@ -157,7 +158,7 @@ annotatedFormula[CVC4::Expr& expr] } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK - { ANTLR_INPUT->checkArity(kind, args.size()); + { PARSER_STATE->checkArity(kind, args.size()); if((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. */ @@ -196,16 +197,16 @@ annotatedFormula[CVC4::Expr& expr] (LET_TOK LPAREN_TOK let_identifier[name,CHECK_UNDECLARED] | FLET_TOK LPAREN_TOK flet_identifier[name,CHECK_UNDECLARED] ) annotatedFormula[expr] RPAREN_TOK - { ANTLR_INPUT->defineVar(name,expr); } + { PARSER_STATE->defineVar(name,expr); } annotatedFormula[expr] RPAREN_TOK - { ANTLR_INPUT->undefineVar(name); } + { PARSER_STATE->undefineVar(name); } | /* a variable */ ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] | let_identifier[name,CHECK_DECLARED] | flet_identifier[name,CHECK_DECLARED] ) - { expr = ANTLR_INPUT->getVariable(name); } + { expr = PARSER_STATE->getVariable(name); } /* constants */ | TRUE_TOK { expr = MK_CONST(true); } @@ -268,8 +269,8 @@ functionSymbol[CVC4::Expr& fun] std::string name; } : functionName[name,CHECK_DECLARED] - { ANTLR_INPUT->checkFunction(name); - fun = ANTLR_INPUT->getVariable(name); } + { PARSER_STATE->checkFunction(name); + fun = PARSER_STATE->getVariable(name); } ; /** @@ -293,7 +294,7 @@ functionDeclaration } else { t = EXPR_MANAGER->mkFunctionType(sorts); } - ANTLR_INPUT->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); } ; /** @@ -311,7 +312,7 @@ predicateDeclaration } else { t = EXPR_MANAGER->mkPredicateType(p_sorts); } - ANTLR_INPUT->mkVar(name, t); } + PARSER_STATE->mkVar(name, t); } ; sortDeclaration @@ -320,7 +321,7 @@ sortDeclaration } : sortName[name,CHECK_UNDECLARED] { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - ANTLR_INPUT->newSort(name); } + PARSER_STATE->newSort(name); } ; /** @@ -343,7 +344,7 @@ sortSymbol returns [CVC4::Type* t] std::string name; } : sortName[name,CHECK_NONE] - { $t = ANTLR_INPUT->getSort(name); } + { $t = PARSER_STATE->getSort(name); } ; /** @@ -376,7 +377,7 @@ identifier[std::string& id, Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; - ANTLR_INPUT->checkDeclaration(id, check, type); } + PARSER_STATE->checkDeclaration(id, check, type); } ; /** @@ -390,7 +391,7 @@ let_identifier[std::string& id, { id = AntlrInput::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id << " check? " << toString(check) << std::endl; - ANTLR_INPUT->checkDeclaration(id, check, SYM_VARIABLE); } + PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } ; /** @@ -404,7 +405,7 @@ flet_identifier[std::string& id, { id = AntlrInput::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id << " check? " << toString(check) << std::endl; - ANTLR_INPUT->checkDeclaration(id, check); } + PARSER_STATE->checkDeclaration(id, check); } ; diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 0b40698cd..768a56a9b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -8,7 +8,7 @@ UNIT_TESTS = \ expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ - parser/parser_black \ + parser/parser_white \ context/context_black \ context/context_mm_black \ context/cdo_black \ diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h new file mode 100644 index 000000000..f4d104a93 --- /dev/null +++ b/test/unit/parser/parser_white.h @@ -0,0 +1,295 @@ +/********************* */ +/** parser_white.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::parser::SmtParser. + **/ + +#include +//#include +#include + +#include "expr/expr.h" +#include "expr/expr_manager.h" +#include "parser/input.h" +#include "parser/parser_state.h" +#include "expr/command.h" +#include "util/output.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + + +/************************** CVC test inputs ********************************/ + +const string goodCvc4Inputs[] = { + "", // empty string is OK + "ASSERT TRUE;", + "QUERY TRUE;", + "CHECKSAT FALSE;", + "a, b : BOOLEAN;", + "a, b : BOOLEAN; QUERY (a => b) AND a => b;", + "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", + "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", + "%% nothing but a comment", + "% a comment\nASSERT TRUE; %a command\n% another comment", + }; + +const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); + + +/* The following expressions are valid after setupContext. */ +const string goodCvc4Exprs[] = { + "a AND b", + "a AND b OR c", + "(a => b) AND a => b", + "(a <=> b) AND (NOT a)", + "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" +}; + +const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); + +const string badCvc4Inputs[] = { + ";", // no command + "ASSERT;", // no args + "QUERY", + "CHECKSAT", + "a, b : boolean;", // lowercase boolean isn't a type + "0x : INT;", // 0x isn't an identifier + "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl + "a : BOOLEAN; a: BOOLEAN;" // double decl + "a, b: BOOLEAN; QUERY a(b);" // non-function used as function + }; + +const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); + +/* The following expressions are invalid even after setupContext. */ +const string badCvc4Exprs[] = { + "a AND", // wrong arity + "AND(a,b)", // not infix + "(OR (AND a b) c)", // not infix + "a IMPLIES b", // should be => + "a NOT b", // wrong arity, not infix + "a and b" // wrong case +}; + +const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); + +/************************** SMT test inputs ********************************/ + +const string goodSmtInputs[] = { + "", // empty string is OK + "(benchmark foo :assumption true)", + "(benchmark bar :formula true)", + "(benchmark qux :formula false)", + "(benchmark baz :extrapreds ( (a) (b) ) )", + "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", + "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", + "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", + ";; nothing but a comment", + "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" + }; + +const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); + +/* The following expressions are valid after setupContext. */ +const string goodSmtExprs[] = { + "(and a b)", + "(or (and a b) c)", + "(implies (and (implies a b) a) b)", + "(and (iff a b) (not a))", + "(iff (xor a b) (and (or a b) (not (and a b))))", + "(ite a (f x) y)", + "(if_then_else a (f x) y)" +}; + +const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); + +const string badSmtInputs[] = { + "(benchmark foo)", // empty benchmark is not OK + "(benchmark bar :assumption)", // no args + "(benchmark bar :formula)", + "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl + "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens + }; + +const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); + +/* The following expressions are invalid even after setupContext. */ +const string badSmtExprs[] = { + "(and)", // wrong arity + "(and a b", // no closing paren + "(a and b)", // infix + "(OR (AND a b) c)", // wrong case + "(a IMPLIES b)", // infix AND wrong case + "(not a b)", // wrong arity + "not a", // needs parens + "(ite a x)", // wrong arity + "(a b)" // using non-function as function +}; + +const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); + +class ParserBlack : public CxxTest::TestSuite { + ExprManager *d_exprManager; + + /* Set up declaration context for expr inputs */ + + void setupContext(ParserState* parserState) { + /* a, b, c: BOOLEAN */ + parserState->mkVar("a",(Type*)d_exprManager->booleanType()); + parserState->mkVar("b",(Type*)d_exprManager->booleanType()); + parserState->mkVar("c",(Type*)d_exprManager->booleanType()); + /* t, u, v: TYPE */ + Type *t = parserState->newSort("t"); + Type *u = parserState->newSort("u"); + Type *v = parserState->newSort("v"); + /* f : t->u; g: u->v; h: v->t; */ + parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); + parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); + parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); + /* x:t; y:u; z:v; */ + parserState->mkVar("x",t); + parserState->mkVar("y",u); + parserState->mkVar("z",v); + } + + void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { + try { +// Debug.on("parser"); +// Debug.on("parser-extra"); + Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; +// istringstream stream(goodInputs[i]); + Input* parser = Input::newStringInput(d_exprManager, d_lang, goodInputs[i], "test"); + TS_ASSERT( !parser->done() ); + Command* cmd; + while((cmd = parser->parseNextCommand())) { + // cout << "Parsed command: " << (*cmd) << endl; + } + TS_ASSERT( parser->parseNextCommand() == NULL ); + TS_ASSERT( parser->done() ); + delete parser; +// Debug.off("parser"); +// Debug.off("parser-extra"); + } catch (Exception& e) { + cout << "\nGood input failed:\n" << goodInputs[i] << endl + << e << endl; +// Debug.off("parser-extra"); + throw; + } + } + } + + void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { + for(int i = 0; i < numInputs; ++i) { +// cout << "Testing bad input: '" << badInputs[i] << "'\n"; +// Debug.on("parser"); + Input* parser = Input::newStringInput(d_exprManager, d_lang, badInputs[i], "test"); + TS_ASSERT_THROWS + ( while(parser->parseNextCommand()); + cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, + ParserException ); +// Debug.off("parser"); + delete parser; + } + } + + void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { + // cout << "Using context: " << context << endl; +// Debug.on("parser"); +// Debug.on("parser-extra"); + for(int i = 0; i < numExprs; ++i) { + try { + // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; + // Debug.on("parser"); +// istringstream stream(context + goodBooleanExprs[i]); + Input* input = Input::newStringInput(d_exprManager, d_lang, + goodBooleanExprs[i], "test"); + TS_ASSERT( !input->done() ); + setupContext(input->getParserState()); + TS_ASSERT( !input->done() ); + Expr e = input->parseNextExpression(); + TS_ASSERT( !e.isNull() ); + e = input->parseNextExpression(); + TS_ASSERT( input->done() ); + TS_ASSERT( e.isNull() ); + delete input; + } catch (Exception& e) { + cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; + cout << e; + throw e; + } + } + } + + void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { + //Debug.on("parser"); + for(int i = 0; i < numExprs; ++i) { + // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; +// istringstream stream(context + badBooleanExprs[i]); + Input* input = Input::newStringInput(d_exprManager, d_lang, + badBooleanExprs[i], "test"); + + TS_ASSERT( !input->done() ); + setupContext(input->getParserState()); + TS_ASSERT( !input->done() ); + TS_ASSERT_THROWS + ( input->parseNextExpression(); + cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, + ParserException ); + delete input; + } + //Debug.off("parser"); + } + +public: + void setUp() { + d_exprManager = new ExprManager(); + } + + void tearDown() { + delete d_exprManager; + } + + void testGoodCvc4Inputs() { + tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); + } + + void testBadCvc4Inputs() { + tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); + } + + void testGoodCvc4Exprs() { + tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); + } + + void testBadCvc4Exprs() { + tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); + } + + void testGoodSmtInputs() { + tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); + } + + void testBadSmtInputs() { + tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); + } + + void testGoodSmtExprs() { + tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); + } + + void testBadSmtExprs() { + tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); + } +}; -- 2.30.2