Saving state between lines in interactive mode (Fixes: #223)

2 files changed, 19 insertions, 0 deletions

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 348fb6e6d..35f7ee16c 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -83,6 +83,7 @@ ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filena
   d_filename = filename;
   d_streamInput = NULL;
   d_exprManager = exprManager;
+  d_parserToUseForState = NULL;
   d_checksEnabled = true;
   d_strictMode = false;
   d_mmap = false;
@@ -122,6 +123,11 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
     parser->disableChecks();
   }
 
+  if( d_parserToUseForState != NULL ) {
+    parser->d_declScope = d_parserToUseForState->d_declScope;
+    parser->d_logicOperators = d_parserToUseForState->d_logicOperators;
+  }
+
   return parser;
 }
 
@@ -164,6 +170,11 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) {
       .withStrictMode(options.strictParsing);
   }
 
+ParserBuilder& ParserBuilder::withStateFrom(const Parser* parser) {
+  d_parserToUseForState = parser;
+  return *this;
+}
+
 ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
   d_strictMode = flag;
   return *this;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 4e8c06f78..44cb8285e 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -80,6 +80,9 @@ class CVC4_PUBLIC ParserBuilder {
   /** The expression manager */
   ExprManager& d_exprManager;
 
+  /** Parser to derive the initial state from. */
+  const Parser* d_parserToUseForState;
+
   /** Should semantic checks be enabled during parsing? */
   bool d_checksEnabled;
 
@@ -128,6 +131,11 @@ public:
   /** Derive settings from the given options. */
   ParserBuilder& withOptions(const Options& options);
 
+  /** Copy the state (e.g., variable and type declaration) from
+   * an existing parser. If <code>parser</code> is <code>NULL</code>,
+   * the default initial state will be used. */
+  ParserBuilder& withStateFrom(const Parser* parser);
+
   /** Should the parser use strict mode? (Default: no) */
   ParserBuilder& withStrictMode(bool flag = true);