Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow condition when reading from stdin. This should completely resolve bug #319.

However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track

Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works).  For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.

Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.

Closing bug #319.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index c1c3f699b..1908d3e90 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -232,7 +232,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC4_COMPETITION_MODE
   *options.out << unitbuf;
-#endif
+#endif /* CVC4_COMPETITION_MODE */
 
   // We only accept one input file
   if(argc > firstArgIndex + 1) {
@@ -429,7 +429,11 @@ int runCvc4(int argc, char *argv[], Options& options) {
         withOptions(options);
 
     if( inputFromStdin ) {
+#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
+      parserBuilder.withStreamInput(cin);
+#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
       parserBuilder.withLineBufferedStreamInput(cin);
+#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
     }
 
     Parser *parser = parserBuilder.build();
@@ -567,7 +571,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
   // exit, don't return
   // (don't want destructors to run)
   exit(returnValue);
-#endif
+#endif /* CVC4_COMPETITION_MODE */
 
   // ReferenceStat< Result > s_statSatResult("sat/unsat", result);
   // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult);