diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/main/driver.cpp | 8 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 8 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 5 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 5 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 5 |
5 files changed, 24 insertions, 7 deletions
diff --git a/src/main/driver.cpp b/src/main/driver.cpp index 042a8ef1d..00072d6d9 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -115,7 +115,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) { @@ -268,7 +268,11 @@ int runCvc4(int argc, char* argv[], Options& options) { ParserBuilder parserBuilder(&exprMgr, filename, 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(); @@ -311,7 +315,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); 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); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2988ae4ef..21f82f638 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -430,12 +430,15 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" #include "util/integer.h" diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 568f3bb92..9f1f458c9 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -50,12 +50,15 @@ options { */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" }/* @lexer::includes */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 59b6715b9..07998b58f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -51,12 +51,15 @@ options { */ #pragma GCC system_header +#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) /* This improves performance by ~10 percent on big inputs. * This option is only valid if we know the input is ASCII (or some 8-bit encoding). * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. * Otherwise, we have to let the lexer detect the encoding at runtime. */ -#define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_ASCII +# define ANTLR3_INLINE_INPUT_8BIT +#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */ #include "parser/antlr_tracing.h" |