diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 05:37:38 +0000 |
commit | 12c1e41862e4b12c3953272416a1edc103d299ee (patch) | |
tree | 9c7d3a044c33ffc3be177e6ca692eb4149add27c /src/parser/parser.h | |
parent | 08df44e6b61999a14dd24a7a134146694dcb3596 (diff) |
Tuesday end-of-day commit.
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 105 |
1 files changed, 81 insertions, 24 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 718b862ab..25fb30be6 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -55,18 +55,20 @@ enum DeclarationCheck { CHECK_NONE }; -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(DeclarationCheck check) { +/** + * Returns a string representation of the given object (for + * debugging). + */ +inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) { switch(check) { case CHECK_NONE: - return "CHECK_NONE"; + return out << "CHECK_NONE"; case CHECK_DECLARED: - return "CHECK_DECLARED"; + return out << "CHECK_DECLARED"; case CHECK_UNDECLARED: - return "CHECK_UNDECLARED"; + return out << "CHECK_UNDECLARED"; default: - Unreachable(); + return out << "DeclarationCheck!UNKNOWN"; } } @@ -80,16 +82,18 @@ enum SymbolType { SYM_SORT }; -/** Returns a string representation of the given object (for - debugging). */ -inline std::string toString(SymbolType type) { +/** + * Returns a string representation of the given object (for + * debugging). + */ +inline std::ostream& operator<<(std::ostream& out, SymbolType type) { switch(type) { case SYM_VARIABLE: - return "SYM_VARIABLE"; + return out << "SYM_VARIABLE"; case SYM_SORT: - return "SYM_SORT"; + return out << "SYM_SORT"; default: - Unreachable(); + return out << "SymbolType!UNKNOWN"; } } @@ -133,10 +137,22 @@ class CVC4_PUBLIC Parser { /** Are we parsing in strict mode? */ bool d_strictMode; + /** Are we only parsing? */ + bool d_parseOnly; + /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; /** + * The current set of unresolved types. We can get by with this NOT + * being on the scope, because we can only have one DATATYPE + * definition going on at one time. This is a bit hackish; we + * depend on mkMutualDatatypeTypes() to check everything and clear + * this out. + */ + std::set<SortType> d_unresolved; + + /** * "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. @@ -155,7 +171,7 @@ protected: * @param input the parser input * @param strictMode whether to incorporate strict(er) compliance checks */ - Parser(ExprManager* exprManager, Input* input, bool strictMode = false); + Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false); public: @@ -255,7 +271,7 @@ public: * @throws ParserException if checks are enabled and the check fails */ void checkDeclaration(const std::string& name, DeclarationCheck check, - SymbolType type = SYM_VARIABLE) throw (ParserException); + SymbolType type = SYM_VARIABLE) throw(ParserException); /** * Checks whether the given name is bound to a function. @@ -263,7 +279,7 @@ public: * @throws ParserException if checks are enabled and name is not * bound to a function */ - void checkFunctionLike(const std::string& name) throw (ParserException); + void checkFunctionLike(const std::string& name) throw(ParserException); /** * Check that <code>kind</code> can accept <code>numArgs</code> arguments. @@ -273,7 +289,7 @@ public: * <code>kind</code> cannot be applied to <code>numArgs</code> * arguments. */ - void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); + void checkArity(Kind kind, unsigned numArgs) throw(ParserException); /** * Check that <code>kind</code> is a legal operator in the current @@ -284,7 +300,7 @@ public: * @throws ParserException if the parser mode is strict and the * operator <code>kind</code> has not been enabled */ - void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); + void checkOperator(Kind kind, unsigned numArgs) throw(ParserException); /** * Returns the type for the variable with the given name. @@ -300,7 +316,7 @@ public: /** * Create a set of new CVC4 variable expressions of the given type. */ - const std::vector<Expr> + std::vector<Expr> mkVars(const std::vector<std::string> names, const Type& type); /** Create a new CVC4 function expression of the given type. */ @@ -327,17 +343,27 @@ public: /** * Creates a new sort with the given name. */ - Type mkSort(const std::string& name); + SortType mkSort(const std::string& name); /** * Creates a new sort constructor with the given name and arity. */ - Type mkSortConstructor(const std::string& name, size_t arity); + SortConstructorType mkSortConstructor(const std::string& name, size_t arity); /** * Creates new sorts with the given names (all of arity 0). */ - std::vector<Type> mkSorts(const std::vector<std::string>& names); + std::vector<SortType> mkSorts(const std::vector<std::string>& names); + + /** + * Creates a new "unresolved type," used only during parsing. + */ + SortType mkUnresolvedType(const std::string& name); + + /** + * Returns true IFF name is an unresolved type. + */ + bool isUnresolvedType(const std::string& name); /** * Create sorts of mutually-recursive datatypes. @@ -371,13 +397,37 @@ public: /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); + /** Parse and return the next command. */ Command* nextCommand() throw(ParserException); + + /** Parse and return the next expression. */ Expr nextExpression() throw(ParserException); - inline void parseError(const std::string& msg) throw (ParserException) { + /** Raise a parse error with the given message. */ + inline void parseError(const std::string& msg) throw(ParserException) { d_input->parseError(msg); } + /** + * If we are parsing only, don't raise an exception; if we are not, + * raise a parse error with the given message. There is no actual + * parse error, everything is as expected, but we cannot create the + * Expr, Type, or other requested thing yet due to internal + * limitations. Even though it's not a parse error, we throw a + * parse error so that the input line and column information is + * available. + * + * Think quantifiers. We don't have a TheoryQuantifiers yet, so we + * have no kind::FORALL or kind::EXISTS. But we might want to + * support parsing quantifiers (just not doing anything with them). + * So this mechanism gives you a way to do it with --parse-only. + */ + inline void unimplementedFeature(const std::string& msg) throw(ParserException) { + if(!d_parseOnly) { + parseError(msg); + } + } + inline void pushScope() { d_declScope->pushScope(); } inline void popScope() { d_declScope->popScope(); } @@ -405,7 +455,7 @@ public: * * In short, caveat emptor. */ - void useDeclarationsFrom(Parser* parser) { + inline void useDeclarationsFrom(Parser* parser) { if(parser == NULL) { d_declScope = &d_declScopeAllocated; } else { @@ -414,6 +464,13 @@ public: } /** + * Gets the current declaration level. + */ + inline size_t getDeclarationLevel() const throw() { + return d_declScope->getLevel(); + } + + /** * An expression stream interface for a parser. This stream simply * pulls expressions from the given Parser object. * |