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_builder.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_builder.h')
-rw-r--r-- | src/parser/parser_builder.h | 50 |
1 files changed, 40 insertions, 10 deletions
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 0d01104eb..6f4f051ec 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -2,10 +2,10 @@ /*! \file parser_builder.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: 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) + ** Copyright (c) 2009, 2010, 2011 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 @@ -75,6 +75,10 @@ class CVC4_PUBLIC ParserBuilder { /** Should we memory-map a file input? */ bool d_mmap; + /** Are we parsing only? */ + bool d_parseOnly; + + /** Initialize this parser builder */ void init(ExprManager* exprManager, const std::string& filename); public: @@ -97,24 +101,50 @@ public: /** Set the parser to read a file for its input. (Default) */ ParserBuilder& withFileInput(); - /** Set the filename for use by the parser. If file input is used, + /** + * Set the filename for use by the parser. If file input is used, * this file will be opened and read by the parser. Otherwise, the * filename string (possibly a non-existent path) will only be used - * in error messages. */ + * in error messages. + */ ParserBuilder& withFilename(const std::string& filename); - /** Set the input language to be used by the parser. (Default: - LANG_AUTO). */ + /** + * Set the input language to be used by the parser. + * + * (Default: LANG_AUTO) + */ ParserBuilder& withInputLanguage(InputLanguage lang); - /** Should the parser memory-map its input? This is only relevant if - * the parser will have a file input. (Default: no) */ + /** + * Should the parser memory-map its input? This is only relevant if + * the parser will have a file input. + * + * (Default: no) + */ ParserBuilder& withMmap(bool flag = true); + /** + * Are we only parsing, or doing something with the resulting + * commands and expressions? This setting affects whether the + * parser will raise certain errors about unimplemented features, + * even if there isn't a parsing error, because the result of the + * parse would otherwise be an incorrect parse tree and the error + * would go undetected. This is specifically for circumstances + * where the parser is ahead of the functionality present elsewhere + * in CVC4 (such as quantifiers, subtypes, records, etc. in the CVC + * language parser). + */ + ParserBuilder& withParseOnly(bool flag = true); + /** Derive settings from the given options. */ ParserBuilder& withOptions(const Options& options); - /** Should the parser use strict mode? (Default: no) */ + /** + * Should the parser use strict mode? + * + * (Default: no) + */ ParserBuilder& withStrictMode(bool flag = true); /** Set the parser to use the given stream for its input. */ |