Implementing input from stdin (Fixes: #144)

7 files changed, 181 insertions, 28 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 300b181a6..9d75dd31f 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -40,8 +40,10 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
-AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
-  InputStream(name),
+AntlrInputStream::AntlrInputStream(std::string name, 
+                                   pANTLR3_INPUT_STREAM input,
+                                   bool fileIsTemporary) :
+  InputStream(name,fileIsTemporary),
   d_input(input) {
   AlwaysAssert( input != NULL );
 }
@@ -54,7 +56,9 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
   return d_input;
 }
 
-AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap)
+AntlrInputStream* 
+AntlrInputStream::newFileInputStream(const std::string& name, 
+                                     bool useMmap)
   throw (InputStreamException) {
   pANTLR3_INPUT_STREAM input = NULL;
   if( useMmap ) {
@@ -68,7 +72,53 @@ AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name,
   return new AntlrInputStream( name, input );
 }
 
-AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name)
+AntlrInputStream* 
+AntlrInputStream::newStreamInputStream(std::istream& input, 
+                                       const std::string& name)
+  throw (InputStreamException) {
+  // // TODO: make this more portable
+  // char *filename = strdup("/tmp/streaminput.XXXXXX");
+  // int fd = mkstemp(filename);
+  // if( fd == -1 ) {
+  //   throw InputStreamException("Couldn't create temporary for stream input: " + name); 
+  // }
+  
+  // // We don't want to use the temp file directly, so first close it
+  // close(fd);
+
+  // // Make a FIFO with our reserved temporary name
+  // int fd = mkfifo(filename, s_IRUSR);
+
+  // // Just stuff everything from the istream into the FIFO
+  // char buf[4096];
+  // while( !input.eof() && !input.fail() ) {
+  //   input.read( buf, sizeof(buf) );
+  //   write( fd, buf, input.gcount() );
+  // }
+
+  // if( !input.eof() ) {
+  //   throw InputStreamException("Stream input failed: " + name);
+  // }
+
+  // // Now create the ANTLR stream
+  // pANTLR3_INPUT_STREAM input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename);
+  
+  // if( input == NULL ) {
+  //   throw InputStreamException("Couldn't create stream input: " + name);
+  // }
+
+  // // Create the stream with fileIsTemporary = true
+  // return new AntlrInputStream( name, input, true );
+
+  stringstream ss( ios_base::out );
+  ss << input.rdbuf();
+  return newStringInputStream( ss.str(), name );
+}
+
+
+AntlrInputStream* 
+AntlrInputStream::newStringInputStream(const std::string& input, 
+                                       const std::string& name)
   throw (InputStreamException) {
   char* inputStr = strdup(input.c_str());
   char* nameStr = strdup(name.c_str());
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 27337c35f..642dc9654 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -47,7 +47,9 @@ namespace parser {
 class AntlrInputStream : public InputStream {
   pANTLR3_INPUT_STREAM d_input;
 
-  AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input);
+  AntlrInputStream(std::string name,
+                   pANTLR3_INPUT_STREAM input,
+                   bool fileIsTemporary = false);
 
   /* This is private and unimplemented, because you should never use it. */
   AntlrInputStream(const AntlrInputStream& inputStream);
@@ -67,18 +69,22 @@ public:
    * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
    * input will use the standard ANTLR3 I/O implementation.
    */
-  static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false)
+  static AntlrInputStream* newFileInputStream(const std::string& name, 
+                                              bool useMmap = false)
     throw (InputStreamException);
 
   /** Create an input from an istream. */
-  // AntlrInputStream newInputStream(std::istream& input, const std::string& name);
+  static AntlrInputStream* newStreamInputStream(std::istream& input, 
+                                                const std::string& name)
+    throw (InputStreamException);
 
   /** Create a string input.
    *
    * @param input the string to read
    * @param name the "filename" to use when reporting errors
    */
-  static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name)
+  static AntlrInputStream* newStringInputStream(const std::string& input, 
+                                                const std::string& name)
     throw (InputStreamException);
 };
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 9ee167897..a900765b5 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -55,7 +55,17 @@ Input* Input::newFileInput(InputLanguage lang,
                            const std::string& filename,
                            bool useMmap)
   throw (InputStreamException) {
-  AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap);
+  AntlrInputStream *inputStream = 
+    AntlrInputStream::newFileInputStream(filename,useMmap);
+  return AntlrInput::newInput(lang,*inputStream);
+}
+
+Input* Input::newStreamInput(InputLanguage lang, 
+                             std::istream& input, 
+                             const std::string& name) 
+  throw (InputStreamException) {
+  AntlrInputStream *inputStream = 
+    AntlrInputStream::newStreamInputStream(input,name);
   return AntlrInput::newInput(lang,*inputStream);
 }
 
diff --git a/src/parser/input.h b/src/parser/input.h
index ccae2d84b..926ebe156 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -20,6 +20,7 @@
 
 #include <iostream>
 #include <string>
+#include <stdio.h>
 #include <vector>
 
 #include "expr/expr.h"
@@ -49,17 +50,26 @@ class InputStream {
   /** The name of this input stream. */
   std::string d_name;
 
+  /** Indicates whether the input file is a temporary that we should
+    * delete on exit. */
+  bool d_fileIsTemporary;
+
 protected:
 
   /** Initialize the input stream with a name. */
-  InputStream(std::string name) :
-    d_name(name) {
+  InputStream(std::string name, bool isTemporary=false) :
+    d_name(name),
+    d_fileIsTemporary(isTemporary) {
   }
 
 public:
 
-  /** Do-nothing destructor. */
-  virtual ~InputStream() { }
+  /** Destructor. */
+  virtual ~InputStream() { 
+    if( d_fileIsTemporary ) {
+      remove(d_name.c_str());
+    }
+  }
 
   /** Get the name of this input stream. */
   const std::string getName() const;
@@ -92,7 +102,9 @@ class CVC4_PUBLIC Input {
     * @param filename the input filename
     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
     */
-  static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false)
+  static Input* newFileInput(InputLanguage lang, 
+                             const std::string& filename, 
+                             bool useMmap=false)
       throw (InputStreamException);
 
   /** Create an input for the given stream.
@@ -101,7 +113,10 @@ class CVC4_PUBLIC Input {
    * @param input the input stream
    * @param name the name of the stream, for use in error messages
    */
-  //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name);
+  static Input* newStreamInput(InputLanguage lang, 
+                               std::istream& input, 
+                               const std::string& name) 
+    throw (InputStreamException);
 
   /** Create an input for the given string
    *
@@ -109,7 +124,9 @@ class CVC4_PUBLIC Input {
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
+  static Input* newStringInput(InputLanguage lang, 
+                               const std::string& input, 
+                               const std::string& name)
     throw (InputStreamException);
 
 public:
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index b2bb15a6a..a9b3c461d 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -52,31 +52,37 @@ public:
   }
 };*/
 
-ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) :
+ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) :
     d_inputType(FILE_INPUT),
-    d_lang(lang),
+    d_lang(LANG_AUTO),
     d_filename(filename),
-    d_exprManager(NULL),
+    d_streamInput(NULL),
+    d_exprManager(exprManager),
     d_checksEnabled(true),
     d_strictMode(false),
     d_mmap(false) {
 }
 
-Parser *ParserBuilder::build() throw (InputStreamException) {
+Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
   Input *input;
   switch( d_inputType ) {
   case FILE_INPUT:
     input = Input::newFileInput(d_lang,d_filename,d_mmap);
     break;
+  case STREAM_INPUT:
+    AlwaysAssert( d_streamInput != NULL,
+                  "Uninitialized stream input in ParserBuilder::build()" );
+    input = Input::newStreamInput(d_lang,*d_streamInput,d_filename);
+    break;
   case STRING_INPUT:
     input = Input::newStringInput(d_lang,d_stringInput,d_filename);
     break;
   }
   switch(d_lang) {
   case LANG_SMTLIB_V2:
-    return new Smt2(d_exprManager, input, d_strictMode);
+    return new Smt2(&d_exprManager, input, d_strictMode);
   default:
-    return new Parser(d_exprManager, input, d_strictMode);
+    return new Parser(&d_exprManager, input, d_strictMode);
   }
 }
 
@@ -115,6 +121,27 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) {
   return *this;
 }
 
+ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
+  d_exprManager = exprManager;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withFileInput() {
+  d_inputType = FILE_INPUT;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withFilename(const std::string& filename) {
+  d_filename = filename;
+  return *this;
+}
+
+ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
+  d_lang = lang;
+  return *this;
+}
+
+
 ParserBuilder& ParserBuilder::withMmap(bool flag) {
   d_mmap = flag;
   return *this;
@@ -125,8 +152,9 @@ ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) {
-  d_exprManager = &exprManager;
+ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
+  d_inputType = STREAM_INPUT;
+  d_streamInput = &input;
   return *this;
 }
 
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index d0b8b7bb2..92b44a82d 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -45,9 +45,15 @@ public:
 
 class Parser;
 
+/**
+ * A builder for input language parsers. <code>build()</code> can be
+ * called any number of times on an instance and will generate a fresh
+ * parser each time.
+ */
 class CVC4_PUBLIC ParserBuilder {
   enum InputType {
     FILE_INPUT,
+    STREAM_INPUT,
     STRING_INPUT
   };
 
@@ -63,8 +69,11 @@ class CVC4_PUBLIC ParserBuilder {
   /** The string input, if any. */
   std::string d_stringInput;
 
+  /** The stream input, if any. */
+  std::istream *d_streamInput;
+
   /** The expression manager */
-  ExprManager *d_exprManager;
+  ExprManager& d_exprManager;
 
   /** Should semantic checks be enabled during parsing? */
   bool d_checksEnabled;
@@ -76,12 +85,43 @@ class CVC4_PUBLIC ParserBuilder {
   bool d_mmap;
 
 public:
-  ParserBuilder(InputLanguage lang, const std::string& filename);
-  Parser *build() throw (InputStreamException);
+
+  /** Create a parser builder using the given ExprManager and filename. */
+  ParserBuilder(ExprManager& exprManager, const std::string& filename);
+
+  /** Build the parser, using the current settings. */
+  Parser *build() throw (InputStreamException,AssertionException);
+
+  /** Should semantic checks be enabled in the parser? (Default: yes) */
   ParserBuilder& withChecks(bool flag = true);
+
+  /** Set the ExprManager to use with the parser. */
+  ParserBuilder& withExprManager(ExprManager& exprManager);
+
+  /** Set the parser to read a file for its input. (Default) */
+  ParserBuilder& withFileInput();
+
+  /** Set the filename for use by the parser. If file input is used,
+   * this file will be opened and read by the parser. Otherwise, the
+   * filename string (possibly a non-existent path) will only be used
+   * in error messages. */
+  ParserBuilder& withFilename(const std::string& filename);
+
+  /** Set the input language to be used by the parser. (Default:
+      LANG_AUTO). */
+  ParserBuilder& withInputLanguage(InputLanguage lang);
+
+  /** Should the parser memory-map its input? This is only relevant if
+   * the parser will have a file input. (Default: no) */
   ParserBuilder& withMmap(bool flag = true);
+
+  /** Should the parser use strict mode? (Default: no) */
   ParserBuilder& withStrictMode(bool flag = true);
-  ParserBuilder& withExprManager(ExprManager& exprManager);
+
+  /** Set the parser to use the given stream for its input. */
+  ParserBuilder& withStreamInput(std::istream& input);
+
+  /** Set the parser to use the given string for its input. */
   ParserBuilder& withStringInput(const std::string& input);
 };
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d76d8ba38..f6089382c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -145,6 +145,8 @@ void Smt2::setLogic(const std::string& name) {
   case AUFNIRA:
   case QF_AUFBV:
   case QF_AUFLIA:
+  case QF_AX:
+  case QF_BV:
     Unhandled(name);
   }
 }