merge from replay branch

3 files changed, 94 insertions, 33 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index f99eef4a1..dc9d0604d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -40,7 +40,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
    ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
    /* Create parser with bogus input. */
    d_parser = parserBuilder.withStringInput("").build();
-}
+}/* InteractiveShell::InteractiveShell() */
 
 
 Command* InteractiveShell::readCommand() {
@@ -139,6 +139,7 @@ Command* InteractiveShell::readCommand() {
   // d_lastParser = parser;
 
   return cmd_seq;
-}
+}/* InteractiveShell::readCommand() */
+
+}/* CVC4 namespace */
 
-} // CVC4 namespace
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index faa80fb84..a08e2cbb4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -2,10 +2,10 @@
 /*! \file interactive_shell.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** 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
@@ -24,13 +24,13 @@
 
 namespace CVC4 {
 
-  class Command;
-  class ExprManager;
-  class Options;
+class Command;
+class ExprManager;
+class Options;
 
-  namespace parser {
-    class Parser;
-  }
+namespace parser {
+  class Parser;
+}/* CVC4::parser namespace */
 
 class CVC4_PUBLIC InteractiveShell {
   std::istream& d_in;
@@ -41,14 +41,24 @@ class CVC4_PUBLIC InteractiveShell {
   static const std::string INPUT_FILENAME;
 
 public:
-  InteractiveShell(ExprManager& exprManager,
-                   const Options& options);
+  InteractiveShell(ExprManager& exprManager, const Options& options);
+
+  /**
+   * Read a command from the interactive shell. This will read as
+   * many lines as necessary to parse a well-formed command.
+   */
+  Command* readCommand();
+
+  /**
+   * Return the internal parser being used.
+   */
+  parser::Parser* getParser() {
+    return d_parser;
+  }
+
+};/* class InteractiveShell */
 
-  /** Read a command from the interactive shell. This will read as
-      many lines as necessary to parse a well-formed command. */
-  Command *readCommand();
-};
+}/* CVC4 namespace */
 
-} // CVC4 namespace
+#endif /* __CVC4__INTERACTIVE_SHELL_H */
 
-#endif // __CVC4__INTERACTIVE_SHELL_H
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 655562512..56c4bb422 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -2,10 +2,10 @@
 /*! \file main.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, cconway
- ** Minor contributors (to current version): barrett, dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): barrett, dejan, taking
  ** 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
@@ -228,20 +228,60 @@ int runCvc4(int argc, char* argv[]) {
     }
   }
 
-  if(!Configuration::isMuzzledBuild()) {
-    OutputLanguage language = language::toOutputLanguage(options.inputLanguage);
-    Debug.getStream() << Expr::setlanguage(language);
-    Trace.getStream() << Expr::setlanguage(language);
-    Notice.getStream() << Expr::setlanguage(language);
-    Chat.getStream() << Expr::setlanguage(language);
-    Message.getStream() << Expr::setlanguage(language);
-    Warning.getStream() << Expr::setlanguage(language);
+  OutputLanguage outLang = language::toOutputLanguage(options.inputLanguage);
+  // Determine which messages to show based on smtcomp_mode and verbosity
+  if(Configuration::isMuzzledBuild()) {
+    Debug.setStream(CVC4::null_os);
+    Trace.setStream(CVC4::null_os);
+    Notice.setStream(CVC4::null_os);
+    Chat.setStream(CVC4::null_os);
+    Message.setStream(CVC4::null_os);
+    Warning.setStream(CVC4::null_os);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    Debug.getStream() << Expr::setlanguage(outLang);
+    Trace.getStream() << Expr::setlanguage(outLang);
+    Notice.getStream() << Expr::setlanguage(outLang);
+    Chat.getStream() << Expr::setlanguage(outLang);
+    Message.getStream() << Expr::setlanguage(outLang);
+    Warning.getStream() << Expr::setlanguage(outLang);
+  }
+
+  Parser* replayParser = NULL;
+  if( options.replayFilename != "" ) {
+    ParserBuilder replayParserBuilder(exprMgr, options.replayFilename, options);
+
+    if( options.replayFilename == "-") {
+      if( inputFromStdin ) {
+        throw OptionException("Replay file and input file can't both be stdin.");
+      }
+      replayParserBuilder.withStreamInput(cin);
+    }
+    replayParser = replayParserBuilder.build();
+    options.replayStream = new Parser::ExprStream(replayParser);
+  }
+  if( options.replayLog != NULL ) {
+    *options.replayLog << Expr::setlanguage(outLang) << Expr::setdepth(-1);
   }
 
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    InteractiveShell shell(exprMgr,options);
+    InteractiveShell shell(exprMgr, options);
+    if(replayParser != NULL) {
+      // have the replay parser use the declarations input interactively
+      replayParser->useDeclarationsFrom(shell.getParser());
+    }
     while((cmd = shell.readCommand())) {
       doCommand(smt,cmd);
       delete cmd;
@@ -255,6 +295,10 @@ int runCvc4(int argc, char* argv[]) {
     }
 
     Parser *parser = parserBuilder.build();
+    if(replayParser != NULL) {
+      // have the replay parser use the file's declarations
+      replayParser->useDeclarationsFrom(parser);
+    }
     while((cmd = parser->nextCommand())) {
       doCommand(smt, cmd);
       delete cmd;
@@ -263,6 +307,12 @@ int runCvc4(int argc, char* argv[]) {
     delete parser;
   }
 
+  if( options.replayStream != NULL ) {
+    // this deletes the expression parser too
+    delete options.replayStream;
+    options.replayStream = NULL;
+  }
+
   string result = smt.getInfo(":status").getValue();
   int returnValue;