From 12c1e41862e4b12c3953272416a1edc103d299ee Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 20 Apr 2011 05:37:38 +0000
Subject: 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
---
 src/parser/parser_builder.cpp | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

(limited to 'src/parser/parser_builder.cpp')

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) {
-- 
cgit v1.2.3