diff options
-rw-r--r-- | Makefile | 15 | ||||
-rw-r--r-- | config/antlr.m4 | 14 | ||||
-rw-r--r-- | contrib/Makefile.am | 1 | ||||
-rwxr-xr-x | contrib/get-antlr-3.4 | 47 | ||||
-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 |
9 files changed, 100 insertions, 8 deletions
@@ -43,6 +43,12 @@ examples: all YEAR := $(shell date +%Y) submission: + @if [ -n "`ls src/parser/*/generated`" ]; then \ + echo 'ERROR:' >&2; \ + echo 'ERROR: Please make maintainer-clean first.' >&2; \ + echo 'ERROR:' >&2; \ + exit 1; \ + fi if [ ! -e configure ]; then ./autogen.sh; fi ./configure competition --disable-shared --enable-static-binary --with-cln --with-portfolio $(MAKE) @@ -64,7 +70,14 @@ submission: echo 'exec ./pcvc4 -L smt2 --no-interactive' ) > cvc4-parallel-smtcomp-$(YEAR)/run chmod 755 cvc4-parallel-smtcomp-$(YEAR)/run tar cf cvc4-parallel-smtcomp-$(YEAR).tar cvc4-parallel-smtcomp-$(YEAR) - # application track + # application track is a separate build + make maintainer-clean + if [ ! -e configure ]; then ./autogen.sh; fi + ./configure competition --disable-shared --enable-static-binary --with-cln CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK + $(MAKE) + strip builds/bin/cvc4 + $(MAKE) regress1 + # package the application track tarball mkdir -p cvc4-application-smtcomp-$(YEAR) cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/cvc4 ( echo '#!/bin/sh'; \ diff --git a/config/antlr.m4 b/config/antlr.m4 index 18b2eff73..674feaed6 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -25,6 +25,14 @@ AC_DEFUN([AC_PROG_ANTLR], [ [No usable antlr3 script found. Make sure that the parser code has been generated already. To obtain ANTLR see <http://www.antlr.org/>.] ) + ANTLR_VERSION= + else + ANTLR_VERSION="`$ANTLR -version 2>&1 | sed 's,.*\<Version *\([[0-9.]]*\).*,\1,'`" + case "$ANTLR_VERSION" in + 3.2|3.2.*) ANTLR_VERSION=3.2 ;; + 3.4|3.4.*) ANTLR_VERSION=3.4 ;; + *) AC_MSG_WARN([unknown version of antlr: $ANTLR_VERSION]);; + esac fi ]) @@ -94,6 +102,9 @@ AC_DEFUN([AC_LIB_ANTLR],[ ])], [ AC_MSG_RESULT([found it (must be antlr3 3.2 or similar)]) + if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.2; then + AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!]) + fi CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ANTLR3_OLD_INPUT_STREAM" ], [ @@ -111,6 +122,9 @@ AC_DEFUN([AC_LIB_ANTLR],[ ])], [ AC_MSG_RESULT([found it (must be antlr3 3.4 or similar)]) + if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.4; then + AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!]) + fi ], [ AC_MSG_ERROR([cannot figure out how to create an antlr3 input stream, bailing..]) diff --git a/contrib/Makefile.am b/contrib/Makefile.am index 1439a1117..815c3377d 100644 --- a/contrib/Makefile.am +++ b/contrib/Makefile.am @@ -10,6 +10,7 @@ EXTRA_DIST = \ new-theory \ configure-in-place \ depgraph \ + get-antlr-3.4 \ theoryskel/kinds \ theoryskel/Makefile \ theoryskel/Makefile.am \ diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 new file mode 100755 index 000000000..c5211474a --- /dev/null +++ b/contrib/get-antlr-3.4 @@ -0,0 +1,47 @@ +#!/bin/bash +# +set -e + +cd "$(dirname "$0")/.." + +if ! [ -e src/parser/cvc/Cvc.g ]; then + echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +set -x +mkdir -p antlr-3.4/share/java +mkdir -p antlr-3.4/bin +mkdir -p antlr-3.4/src +cd antlr-3.4 +wget -c -O share/java/antlr-3.4-complete.jar http://antlr.org/download/antlr-3.4-complete.jar +wget -c -O src/libantlr3c-3.4.tar.gz http://antlr.org/download/C/libantlr3c-3.4.tar.gz +tee bin/antlr3 <<EOF +#!/bin/sh +export CLASSPATH=/usr/share/java/stringtemplate.jar:`pwd`/share/java/antlr-3.4-complete.jar:\$CLASSPATH +exec java org.antlr.Tool "\$@" +EOF +chmod a+x bin/antlr3 +cd src +tar xfzv libantlr3c-3.4.tar.gz +cd libantlr3c-3.4 +./configure --enable-64bit --prefix=`pwd`/../.. +cp Makefile Makefile.orig +sed 's,^CFLAGS = .*,\0 -fexceptions,' Makefile.orig > Makefile +make +make install +set +x +cd ../../.. + +echo +echo Invalidating generated parsers.. +touch src/parser/*/*.g + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 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" |