more smtcomp-submission script work

diff --git a/Makefile b/Makefile
index a1d2a27f0bed2de8d7573d0ba91b486d34029790..45e70d8e097dab3eef7d97718f37a00344167c5a 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -40,85 +40,126 @@ doc: doc-builds
 doc-internals: doc-internals-builds
 
 YEAR := $(shell date +%Y)
-submission submission-main:
+submission:
+       @if [ -d builds-smtcomp ]; then \
+         echo 'ERROR: remove the builds-smtcomp directory' >&2; \
+         exit 1; \
+       fi
+       @if test -d cvc4-smtcomp-$(YEAR) || test -e cvc4-smtcomp-$(YEAR).zip || \
+           test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip || \
+           test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip || \
+           test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \
+         echo 'ERROR: remove cvc4-smtcomp*-$(YEAR) and corresponding zipfiles.' >&2; \
+         exit 1; \
+       fi
+       $(MAKE) submission-main
+       $(MAKE) submission-application
+       $(MAKE) submission-parallel
+       mkdir -p cvc4-smtcomp-$(YEAR)/bin
+       cp -p cvc4-smtcomp-main-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-main
+       cp -p cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_default
+       cp -p cvc4-smtcomp-application-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4-application
+       cp -p cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_application
+       cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/pcvc4
+       cp -p cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default cvc4-smtcomp-$(YEAR)/bin/starexec_run_parallel
+       cat cvc4-smtcomp-main-$(YEAR)/starexec_description.txt \
+           cvc4-smtcomp-application-$(YEAR)/starexec_description.txt \
+           cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt \
+           > cvc4-smtcomp-$(YEAR)/starexec_description.txt
+       cd cvc4-smtcomp-$(YEAR) && zip -r ../cvc4-smtcomp-$(YEAR).zip *
+submission-main:
+       @if [ -d builds-smtcomp/main ]; then \
+         echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
+         exit 1; \
+       fi
        @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
          echo 'ERROR:' >&2; \
          echo 'ERROR: Please make maintainer-clean first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
-       @if test -d cvc4-smtcomp-$(YEAR) || test -e cvc4-smtcomp-$(YEAR).zip; then \
+       @if test -d cvc4-smtcomp-main-$(YEAR) || test -e cvc4-smtcomp-main-$(YEAR).zip; then \
          echo 'ERROR:' >&2; \
-         echo 'ERROR: Please remove cvc4-smtcomp-$(YEAR) and cvc4-smtcomp-$(YEAR).zip first.' >&2; \
+         echo 'ERROR: Please remove cvc4-smtcomp-main-$(YEAR) and cvc4-smtcomp-main-$(YEAR).zip first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
        ./autogen.sh
-       ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl
-       $(MAKE)
-       strip builds/bin/cvc4
-       $(MAKE) check
-       #$(MAKE) -C test/regress/regress1 check
+       mkdir -p builds-smtcomp/main
+       ( cd builds-smtcomp/main; \
+         ../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl; \
+         $(MAKE) V=1; \
+         strip src/main/cvc4; \
+         $(MAKE) check )
        # main track
-       mkdir -p cvc4-smtcomp-$(YEAR)/bin
-       cp -p builds/bin/cvc4 cvc4-smtcomp-$(YEAR)/bin/cvc4
-       cp contrib/run-script-smtcomp2014 cvc4-smtcomp-$(YEAR)/bin/starexec_run_default
-       chmod 755 cvc4-smtcomp-$(YEAR)/bin/starexec_run_default
-       echo "CVC4 for SMT_COMP main track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-$(YEAR)/starexec_description.txt
-       cd cvc4-smtcomp-$(YEAR) && zip -r ../cvc4-smtcomp-$(YEAR).zip *
+       mkdir -p cvc4-smtcomp-main-$(YEAR)/bin
+       cp -p builds-smtcomp/main/src/main/cvc4 cvc4-smtcomp-main-$(YEAR)/bin/cvc4
+       cp contrib/run-script-smtcomp2014 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default
+       chmod 755 cvc4-smtcomp-main-$(YEAR)/bin/starexec_run_default
+       echo "CVC4 for SMT_COMP main track `builds-smtcomp/main/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-main-$(YEAR)/starexec_description.txt
+       cd cvc4-smtcomp-main-$(YEAR) && zip -r ../cvc4-smtcomp-main-$(YEAR).zip *
 submission-application:
        # application track is a separate build because it has different preprocessor #defines
+       @if [ -d builds-smtcomp/application ]; then \
+         echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
+         exit 1; \
+       fi
        @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
          echo 'ERROR:' >&2; \
          echo 'ERROR: Please make maintainer-clean first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
-       @if test -d cvc4-application-smtcomp-$(YEAR) || test -e cvc4-application-smtcomp-$(YEAR).zip; then \
+       @if test -d cvc4-smtcomp-application-$(YEAR) || test -e cvc4-smtcomp-application-$(YEAR).zip; then \
          echo 'ERROR:' >&2; \
-         echo 'ERROR: Please remove cvc4-application-smtcomp-$(YEAR) and cvc4-application-smtcomp-$(YEAR).zip first.' >&2; \
+         echo 'ERROR: Please remove cvc4-smtcomp-application-$(YEAR) and cvc4-smtcomp-application-$(YEAR).zip first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
        ./autogen.sh
-       ./configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK
-       $(MAKE)
-       strip builds/bin/cvc4
-       $(MAKE) check
-       #$(MAKE) -C test/regress/regress1 check
+       mkdir -p builds-smtcomp/application
+       ( cd builds-smtcomp/application; \
+         ../../configure competition --disable-shared --enable-static-binary --with-cln --with-glpk --with-abc --without-readline --enable-gpl CXXFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK CFLAGS=-DCVC4_SMTCOMP_APPLICATION_TRACK; \
+         $(MAKE) V=1; \
+         strip src/main/cvc4; \
+         $(MAKE) check )
        # package the application track zipfile
-       mkdir -p cvc4-application-smtcomp-$(YEAR)/bin
-       cp -p builds/bin/cvc4 cvc4-application-smtcomp-$(YEAR)/bin/cvc4
-       cp contrib/run-script-smtcomp2014-application cvc4-application-smtcomp-$(YEAR)/bin/starexec_run_default
-       chmod 755 cvc4-application-smtcomp-$(YEAR)/bin/starexec_run_default
-       echo "CVC4 for SMT_COMP application track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-application-smtcomp-$(YEAR)/starexec_description.txt
-       cd cvc4-application-smtcomp-$(YEAR) && zip -r ../cvc4-application-smtcomp-$(YEAR).zip *
+       mkdir -p cvc4-smtcomp-application-$(YEAR)/bin
+       cp -p builds-smtcomp/application/src/main/cvc4 cvc4-smtcomp-application-$(YEAR)/bin/cvc4
+       cp contrib/run-script-smtcomp2014-application cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default
+       chmod 755 cvc4-smtcomp-application-$(YEAR)/bin/starexec_run_default
+       echo "CVC4 for SMT_COMP application track `builds-smtcomp/application/src/main/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-application-$(YEAR)/starexec_description.txt
+       cd cvc4-smtcomp-application-$(YEAR) && zip -r ../cvc4-smtcomp-application-$(YEAR).zip *
 submission-parallel:
        # parallel track can't be built with -cln, so it's a separate build
+       @if [ -d builds-smtcomp/parallel ]; then \
+         echo 'ERROR: remove the builds-smtcomp/main directory' >&2; \
+         exit 1; \
+       fi
        @if [ -n "`ls src/parser/*/generated 2>/dev/null`" ]; then \
          echo 'ERROR:' >&2; \
          echo 'ERROR: Please make maintainer-clean first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
-       @if test -d cvc4-parallel-smtcomp-$(YEAR) || test -e cvc4-parallel-smtcomp-$(YEAR).zip; then \
+       @if test -d cvc4-smtcomp-parallel-$(YEAR) || test -e cvc4-smtcomp-parallel-$(YEAR).zip; then \
          echo 'ERROR:' >&2; \
-         echo 'ERROR: Please remove cvc4-parallel-smtcomp-$(YEAR) and cvc4-parallel-smtcomp-$(YEAR).zip first.' >&2; \
+         echo 'ERROR: Please remove cvc4-smtcomp-parallel-$(YEAR) and cvc4-smtcomp-parallel-$(YEAR).zip first.' >&2; \
          echo 'ERROR:' >&2; \
          exit 1; \
        fi
        ./autogen.sh
-       ./configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl
-       $(MAKE)
-       strip builds/bin/pcvc4
-       # some test cases fail (and are known to fail)
-       -$(MAKE) check BINARY=pcvc4
-       #$(MAKE) -C test/regress/regress1 check BINARY=pcvc4
+       mkdir -p builds-smtcomp/parallel
+       ( cd builds-smtcomp/parallel; \
+         ../../configure competition --disable-shared --enable-static-binary --with-gmp --with-portfolio --with-glpk --with-abc --without-readline --enable-gpl; \
+         $(MAKE) V=1; \
+         strip src/main/pcvc4; \
+         $(MAKE) check BINARY=pcvc4 CVC4_REGRESSION_ARGS=--fallback-sequential )
        # package the parallel track zipfile
-       mkdir -p cvc4-parallel-smtcomp-$(YEAR)/bin
-       cp -p builds/bin/pcvc4 cvc4-parallel-smtcomp-$(YEAR)/bin/pcvc4
+       mkdir -p cvc4-smtcomp-parallel-$(YEAR)/bin
+       cp -p builds-smtcomp/parallel/src/main/pcvc4 cvc4-smtcomp-parallel-$(YEAR)/bin/pcvc4
        ( echo '#!/bin/sh'; \
-         echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive "$@"' ) > cvc4-parallel-smtcomp-$(YEAR)/bin/starexec_run_default
-       chmod 755 cvc4-parallel-smtcomp-$(YEAR)/bin/starexec_run_default
-       echo "CVC4 for SMT_COMP parallel track `builds/bin/cvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-parallel-smtcomp-$(YEAR)/starexec_description.txt
-       cd cvc4-parallel-smtcomp-$(YEAR) && zip -r ../cvc4-parallel-smtcomp-$(YEAR).zip *
+         echo 'exec ./pcvc4 --threads 2 -L smt2 --no-checking --no-interactive "$@"' ) > cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default
+       chmod 755 cvc4-smtcomp-parallel-$(YEAR)/bin/starexec_run_default
+       echo "CVC4 for SMT_COMP parallel track `builds-smtcomp/parallel/src/main/pcvc4 --version | head -1 | sed 's,.*version ,,;s,-,_,g;s,[^a-zA-Z0-9. _],,g'`" > cvc4-smtcomp-parallel-$(YEAR)/starexec_description.txt
+       cd cvc4-smtcomp-parallel-$(YEAR) && zip -r ../cvc4-smtcomp-parallel-$(YEAR).zip *