Adding support for interactive mode

4 files changed, 193 insertions, 16 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 3cd062158..b6cdbb1f4 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -6,11 +6,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 bin_PROGRAMS = cvc4
 
 cvc4_SOURCES = \
-	main.cpp \
 	getopt.cpp \
-	util.cpp \
+	interactive_shell.h \
+	interactive_shell.cpp \
 	main.h \
-	usage.h
+	main.cpp \
+	usage.h \
+	util.cpp
 
 cvc4_LDADD = \
 	../parser/libcvc4parser.la \
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
new file mode 100644
index 000000000..7af72ed2d
--- /dev/null
+++ b/src/main/interactive_shell.cpp
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \file interactive_shell.cpp
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: 
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ ** information.\endverbatim
+ **
+ ** \brief Interactive shell for CVC4
+ **/
+
+#include <iostream>
+
+#include "interactive_shell.h"
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+Command* InteractiveShell::readCommand() {
+  /* Don't do anything if the input is closed. */
+  if( d_in.eof() ) {
+    return NULL;
+  }
+
+  /* If something's wrong with the input, there's nothing we can do. */
+  if( !d_in.good() ) {
+    throw ParserException("Interactive input broken.");
+  }
+
+  string input;
+
+  /* Prompt the user for input. */
+  d_out << "CVC4> " << flush;
+  while(true) {
+    stringbuf sb;
+    string line;
+
+    /* Read a line */
+    d_in.get(sb,'\n');
+    line = sb.str();
+    // cout << "Input was '" << input << "'" << endl << flush;
+
+    /* If we hit EOF, we're done. */
+    if( d_in.eof() ) {
+      input += line;
+      break;
+    }
+
+    /* Check for failure */
+    if( d_in.fail() ) {
+      /* This should only happen if the input line was empty. */
+      Assert( line.empty() );
+      d_in.clear();
+    }
+
+    /* Extract the newline delimiter from the stream too */
+    int c = d_in.get();
+    Assert( c == '\n' );
+
+    // cout << "Next char is '" << (char)c << "'" << endl << flush;
+
+    /* Strip trailing whitespace. */
+    int n = line.length() - 1;
+    while( !line.empty() && isspace(line[n]) ) { 
+      line.erase(n,1); 
+      n--;
+    }
+
+    input += line;
+    
+    /* If the last char was a backslash, continue on the next line. */
+    if( !line.empty() && line[n] == '\\' ) {
+      n = input.length() - 1;
+      Assert( input[n] == '\\' );
+      input[n] = '\n';
+      d_out << "... > " << flush;
+    } else {
+      /* No continuation, we're done. */
+      //cout << "Leaving input loop." << endl << flush;
+      break;
+    }
+  }
+
+  Parser *parser = 
+    d_parserBuilder
+        .withStringInput(input)
+        .build();
+
+  /* There may be more than one command in the input. Build up a
+     sequence. */
+  CommandSequence *cmd_seq = new CommandSequence();
+  Command *cmd;
+
+  while( (cmd = parser->nextCommand()) ) {
+    cmd_seq->addCommand(cmd);
+  }
+
+  delete parser;
+  return cmd_seq;
+}
+
+} // CVC4 namespace
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
new file mode 100644
index 000000000..6bd9db295
--- /dev/null
+++ b/src/main/interactive_shell.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file interactive_shell.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: 
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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
+ ** information.\endverbatim
+ **
+ ** \brief Interactive shell for CVC4
+ **/
+
+#ifndef __CVC4__INTERACTIVE_SHELL_H
+#define __CVC4__INTERACTIVE_SHELL_H
+
+#include <iostream>
+#include <string>
+
+#include "parser/parser_builder.h"
+
+namespace CVC4 {
+
+  class Command;
+
+  using namespace parser;
+
+class InteractiveShell {
+  std::istream& d_in;
+  std::ostream& d_out;
+  ParserBuilder d_parserBuilder;
+
+public:
+  InteractiveShell(std::istream& in, 
+                   std::ostream& out, 
+                   ParserBuilder& parserBuilder) : 
+    d_in(in),
+    d_out(out),
+    d_parserBuilder(parserBuilder) {
+  }
+
+  /** 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
+
+#endif // __CVC4__INTERACTIVE_SHELL_H
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d879e81df..2f524c3f6 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -24,9 +24,11 @@
 
 #include "cvc4autoconfig.h"
 #include "main.h"
+#include "interactive_shell.h"
 #include "usage.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
+#include "parser/parser_exception.h"
 #include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "expr/command.h"
@@ -119,9 +121,13 @@ int runCvc4(int argc, char* argv[]) {
     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 
   // if we're reading from stdin, default to interactive mode
-  if(!options.interactiveSetByUser) {
-    options.interactive = inputFromStdin;
-  }
+  // [chris 10/20/10] The expected behavior of interactive is
+  // different from the expected behavior of file input from
+  // stdin, due to EOL escapes in interactive mode
+
+  // if(!options.interactiveSetByUser) {
+  //   options.interactive = inputFromStdin;
+  // }
 
   // Create the expression manager
   ExprManager exprMgr(options.earlyTypeChecking);
@@ -193,18 +199,22 @@ int runCvc4(int argc, char* argv[]) {
     parserBuilder.withStreamInput(cin);
   }
 
-  Parser *parser = parserBuilder.build();
-
   // Parse and execute commands until we are done
   Command* cmd;
   if( options.interactive ) {
-    // cout << "CVC4> " << flush;
-  }
-  while((cmd = parser->nextCommand())) {
-    if( !options.parseOnly ) {
+    InteractiveShell shell(cin,cout,parserBuilder);
+    while((cmd = shell.readCommand())) {
+      doCommand(smt,cmd);
+      delete cmd;
+    }
+  } else {
+    Parser *parser = parserBuilder.build();
+    while((cmd = parser->nextCommand())) {
       doCommand(smt, cmd);
+      delete cmd;
     }
-    delete cmd;
+    // Remove the parser
+    delete parser;
   }
 
   string result = smt.getInfo(":status").getValue();
@@ -224,9 +234,6 @@ int runCvc4(int argc, char* argv[]) {
   exit(returnValue);
 #endif
 
-  // Remove the parser
-  delete parser;
-
   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
   StatisticsRegistry::registerStat(&s_statSatResult);
 
@@ -240,7 +247,12 @@ int runCvc4(int argc, char* argv[]) {
   return returnValue;
 }
 
+/** Executes a command. Deletes the command after execution. */
 void doCommand(SmtEngine& smt, Command* cmd) {
+  if( options.parseOnly ) {
+    return;
+  }
+
   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
   if(seq != NULL) {
     for(CommandSequence::iterator subcmd = seq->begin();