diff options
Diffstat (limited to 'src/parser/input.h')
-rw-r--r-- | src/parser/input.h | 251 |
1 files changed, 42 insertions, 209 deletions
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 <string> -#include <iostream> #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 <code>parseNextCommand</code> and <code>parseNextExpression</code> to + * extract a stream of <code>Command</code>'s and <code>Expr</code>'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., <code>newFileParser</code> and <code>newStringInput</code>, 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<Expr> d_varSymbolTable; - - /** The sort table */ - SymbolTable<Type*> 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 <code>ExprManager</code> 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 <code>kind</code> can accept <code>numArgs</codes> 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 <code>kind</code> cannot be - * applied to <code>numArgs</code> 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<Expr> - mkVars(const std::vector<std::string> 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<Type*> - newSorts(const std::vector<std::string>& 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 <code>ParserException</code> with the given error message. - * Implementations should fill in the <code>ParserException</code> 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 <code>ParserException</code> with the given error message. + * Implementations should fill in the <code>ParserException</code> 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 */ |