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.cpp | |
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.cpp')
-rw-r--r-- | src/parser/parser_builder.cpp | 22 |
1 files changed, 14 insertions, 8 deletions
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 38f41f47a..9773445ed 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -2,10 +2,10 @@ /*! \file parser_builder.cpp ** \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 @@ -57,6 +57,7 @@ void ParserBuilder::init(ExprManager* exprManager, d_checksEnabled = true; d_strictMode = false; d_mmap = false; + d_parseOnly = false; } Parser *ParserBuilder::build() @@ -81,13 +82,13 @@ Parser *ParserBuilder::build() Parser *parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: - parser = new Smt(d_exprManager, input, d_strictMode); + parser = new Smt(d_exprManager, input, d_strictMode, d_parseOnly); break; case language::input::LANG_SMTLIB_V2: - parser = new Smt2(d_exprManager, input, d_strictMode); + parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; default: - parser = new Parser(d_exprManager, input, d_strictMode); + parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); } if( d_checksEnabled ) { @@ -124,18 +125,23 @@ ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { return *this; } - ParserBuilder& ParserBuilder::withMmap(bool flag) { d_mmap = flag; return *this; } +ParserBuilder& ParserBuilder::withParseOnly(bool flag) { + d_parseOnly = flag; + return *this; +} + ParserBuilder& ParserBuilder::withOptions(const Options& options) { return withInputLanguage(options.inputLanguage) .withMmap(options.memoryMap) .withChecks(options.semanticChecks) - .withStrictMode(options.strictParsing); + .withStrictMode(options.strictParsing) + .withParseOnly(options.parseOnly); } ParserBuilder& ParserBuilder::withStrictMode(bool flag) { |