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.

1 files changed, 0 insertions, 8 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9b0ea4759..f27bf03f0 100644
--- 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());