Always parse streams with line buffer (#6532)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 13 May 2021 16:49:33 +0000 (09:49 -0700)
committerGitHub <noreply@github.com>
Thu, 13 May 2021 16:49:33 +0000 (16:49 +0000)
commit05239e9bdf31d848ff073334d26a790de5412e03
treefede281f5c25e7b19d36d91c34f5322d83facaa4
parent31242de4b423d7225174dd1672edb2dacb68f5b8
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.
src/main/driver_unified.cpp
src/parser/antlr_input.cpp
src/parser/antlr_input.h
src/parser/input.cpp
src/parser/input.h
src/parser/parser_builder.cpp
src/parser/parser_builder.h