Optionally split regression tests into test groups (#207)

To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.

diff --git a/.travis.yml b/.travis.yml
index 6ef64f0e242209e8c9bd643da3a328e2e229f0d2..47fc617c2f16831d80a238b0ecec95d6a58b1c42 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -15,9 +15,11 @@ env:
   # The next declaration is the encrypted COVERITY_SCAN_TOKEN, created
   #   via the "travis encrypt" command using the project repo's public key
   - secure: "fRfdzYwV10VeW5tVSvy5qpR8ZlkXepR7XWzCulzlHs9SRI2YY20BpzWRjyMBiGu2t7IeJKT7qdjq/CJOQEM8WS76ON7QJ1iymKaRDewDs3OhyPJ71fsFKEGgLky9blk7I9qZh23hnRVECj1oJAVry9IK04bc2zyIEjUYpjRkUAQ="
+  - TEST_GROUPS=2
  matrix:
   - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='production --enable-language-bindings=java,c --enable-proof --with-portfolio'
-  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio'
+  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=0
+  - TRAVIS_CVC4=yes TRAVIS_CVC4_CHECK_PORTFOLIO=yes TRAVIS_CVC4_CONFIG='debug --enable-language-bindings=java,c --enable-proof --with-portfolio' TEST_GROUP=1
   - TRAVIS_CVC4=yes TRAVIS_CVC4_CONFIG='--disable-proof'
   - TRAVIS_CVC4=yes TRAVIS_CVC4_DISTCHECK=yes TRAVIS_CVC4_CONFIG='--enable-proof'
   - TRAVIS_LFSC=yes

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 5bc46d4f9a5153f58b7d598973543c91b9271c76..f6dc00b3f99d74ecb1d52d7911eb4bc0b30e49bf 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -5,10 +5,16 @@
 #
 # usage:
 #
-#     run_regression cvc4-binary [ --proof | --dump ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
+#     run_regression [ --proof | --dump ] [ wrapper ] cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 | benchmark.p ]
 #
 # Runs benchmark and checks for correct exit status and output.
 #
+# The TEST_GROUP and TEST_GROUPS environment variables can be used to split the
+# benchmarks into groups and only run one of the groups. The benchmarks are
+# associated with a group based on a hash of their name. TEST_GROUPS controls
+# how many groups are created while TEST_GROUP specifies the group to run.
+# Currently, the primary use case for this is to split the benchmarks across
+# multiple Travis jobs.
 
 # ulimit -t 1    # For detecting long running regressions
 ulimit -s 65000  # Needed for some (esp. portfolio and model-building)
@@ -49,6 +55,16 @@ cvc4=$1
 benchmark_orig=$2
 benchmark="$benchmark_orig"
 
+if [ -n "$TEST_GROUP" ]; then
+  # Use the checksum of the benchmark name to determine the group of the
+  # benchmark
+  benchmark_group=$(( $(echo "$benchmark" | cksum | cut -d " " -f1) % $TEST_GROUPS ))
+  if (( $benchmark_group != $TEST_GROUP )); then
+    # Skip the benchmark if it is not in the expected test group
+    exit 77
+  fi
+fi
+
 function error {
   echo "$prog: error: $*"
   exit 1