Always parse streams with line buffer (#6532)

When cvc5 was compiled in competition mode (but not for the application
track), then it had a special behavior when reading from stdin. When it
received input from stdin, it would read all of stdin and then parse the
input as a string because it assumed that the full input is directly
available on stdin. However, the non-application tracks of SMT-COMP do
not use stdin anymore. They pass a filename to the solver. This special
case is not used as a result. Usually, cvc5 parses from stdin using the
line buffer, so this commit makes it so that this is always the case,
which simplifies the code.

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9b0ea4759db2fb5815b6da4c2cf6a8a2e369d88f..f27bf03f0e190748272c49d52a36a5fd94908000 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -263,11 +263,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
 
       if( inputFromStdin ) {
-#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
         parserBuilder.withStreamInput(cin);
-#else  /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
-        parserBuilder.withLineBufferedStreamInput(cin);
-#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
       }
 
       vector< vector<Command*> > allCommands;
@@ -419,11 +415,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
 
       if( inputFromStdin ) {
-#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK)
         parserBuilder.withStreamInput(cin);
-#else  /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
-        parserBuilder.withLineBufferedStreamInput(cin);
-#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */
       }
 
       std::unique_ptr<Parser> parser(parserBuilder.build());

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index de90ee14b068aa6e5861a5691c3f9bd36ff19af9..73d1b89b5973abd7d354634f953cd47acac2c0fc 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -16,7 +16,7 @@
 #include "parser/antlr_input.h"
 
 #include <antlr3.h>
-#include <limits.h>
+#include <limits>
 
 #include "base/check.h"
 #include "base/output.h"
@@ -152,61 +152,13 @@ AntlrInputStream::newFileInputStream(const std::string& name,
   return new AntlrInputStream(name, input, false, NULL, NULL);
 }
 
-
-AntlrInputStream*
-AntlrInputStream::newStreamInputStream(std::istream& input,
-                                       const std::string& name,
-                                       bool lineBuffered)
+AntlrInputStream* AntlrInputStream::newStreamInputStream(
+    std::istream& input, const std::string& name)
 {
   pANTLR3_INPUT_STREAM inputStream = NULL;
   pANTLR3_UINT8 inputStringCopy = NULL;
-  LineBuffer* line_buffer = NULL;
-
-  if(lineBuffered) {
-    line_buffer = new LineBuffer(&input);
-    inputStream = newAntlr3BufferedStream(input, name, line_buffer);
-  } else {
-
-    // Since these are all NULL on entry, realloc will be called
-    char *basep = NULL, *boundp = NULL, *cp = NULL;
-    /* 64KB seems like a reasonable default size. */
-    size_t bufSize = 0x10000;
-
-    /* Keep going until we can't go no more. */
-    while( !input.eof() && !input.fail() ) {
-
-      if( cp == boundp ) {
-        /* We ran out of room in the buffer. Realloc at double the size. */
-        ptrdiff_t offset = cp - basep;
-        basep = (char *) realloc(basep, bufSize);
-        if( basep == NULL ) {
-          throw InputStreamException("Failed buffering input stream: " + name);
-        }
-        cp = basep + offset;
-        boundp = basep + bufSize;
-        bufSize *= 2;
-      }
-
-      /* Read as much as we have room for. */
-      input.read( cp, boundp - cp );
-      cp += input.gcount();
-    }
-
-    /* Make sure the fail bit didn't get set. */
-    if( !input.eof() ) {
-      throw InputStreamException("Stream input failed: " + name);
-    }
-    ptrdiff_t offset = cp - basep;
-    Assert(offset >= 0);
-    Assert(offset <= std::numeric_limits<uint32_t>::max());
-    inputStringCopy = (pANTLR3_UINT8)basep;
-    inputStream = newAntrl3InPlaceStream(inputStringCopy, (uint32_t) offset, name);
-  }
-
-  if( inputStream == NULL ) {
-    throw InputStreamException("Couldn't initialize input: " + name);
-  }
-
+  LineBuffer* line_buffer = new LineBuffer(&input);
+  inputStream = newAntlr3BufferedStream(input, name, line_buffer);
   return new AntlrInputStream(name, inputStream, false, inputStringCopy,
                               line_buffer);
 }

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 5fcf853cc55db012720d14cca6ad5c0f6527fbdb..c7496218891fd05d8679238a868cefa882fe7f84 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -77,8 +77,7 @@ public:
 
   /** Create an input from an istream. */
   static AntlrInputStream* newStreamInputStream(std::istream& input,
-                                                const std::string& name,
-                                                bool lineBuffered = false);
+                                                const std::string& name);
 
   /** Create a string input.
    * NOTE: the new AntlrInputStream will take ownership of input over

diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index cfb418fbe1d5bfab0a797a2b11864e08d559f3b1..4c88978de17d2111beada989c17aa366775f6d80 100644 (file)
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -62,11 +62,10 @@ Input* Input::newFileInput(InputLanguage lang,
 
 Input* Input::newStreamInput(InputLanguage lang,
                              std::istream& input,
-                             const std::string& name,
-                             bool lineBuffered)
+                             const std::string& name)
 {
-  AntlrInputStream *inputStream =
-    AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
+  AntlrInputStream* inputStream =
+      AntlrInputStream::newStreamInputStream(input, name);
   return AntlrInput::newInput(lang, *inputStream);
 }
 

diff --git a/src/parser/input.h b/src/parser/input.h
index 47453e3670e3e15faed5b17b1cda058bcc355fec..1821bc0346e5c0f39cbf4c7685308595851fd716 100644 (file)
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -115,8 +115,7 @@ class CVC5_EXPORT Input
    */
   static Input* newStreamInput(InputLanguage lang,
                                std::istream& input,
-                               const std::string& name,
-                               bool lineBuffered = false);
+                               const std::string& name);
 
   /** Create an input for the given string
    *

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ad3b69f7e715f772fc29f67ad01d40ec67509ed5..220edb9d5cb4c969edcee0fcdd876e550bbc3892 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -75,10 +75,6 @@ Parser* ParserBuilder::build()
   case FILE_INPUT:
     input = Input::newFileInput(d_lang, d_filename, d_mmap);
     break;
-  case LINE_BUFFERED_STREAM_INPUT:
-    Assert(d_streamInput != NULL);
-    input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true);
-    break;
   case STREAM_INPUT:
     Assert(d_streamInput != NULL);
     input = Input::newStreamInput(d_lang, *d_streamInput, d_filename);
@@ -204,12 +200,6 @@ ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) {
-  d_inputType = LINE_BUFFERED_STREAM_INPUT;
-  d_streamInput = &input;
-  return *this;
-}
-
 ParserBuilder& ParserBuilder::withStringInput(const std::string& input) {
   d_inputType = STRING_INPUT;
   d_stringInput = input;

diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 5d73fedfaede17c8b4802c192ea269b6ed88b8d6..b43da3548e93063e96a3ed247954d94f65c05d1b 100644 (file)
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -46,7 +46,6 @@ class CVC5_EXPORT ParserBuilder
 {
   enum InputType {
     FILE_INPUT,
-    LINE_BUFFERED_STREAM_INPUT,
     STREAM_INPUT,
     STRING_INPUT
   };
@@ -177,9 +176,6 @@ class CVC5_EXPORT ParserBuilder
   /** Set the parser to use the given stream for its input. */
   ParserBuilder& withStreamInput(std::istream& input);
 
-  /** Set the parser to use the given stream for its input. */
-  ParserBuilder& withLineBufferedStreamInput(std::istream& input);
-
   /** Set the parser to use the given string for its input. */
   ParserBuilder& withStringInput(const std::string& input);