Move regression tests to single Makefile.am (#1658)

Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).

This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.

1 files changed, 0 insertions, 196 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
deleted file mode 100644
index 7127c5739..000000000
--- a/test/regress/regress0/Makefile.am
+++ /dev/null
@@ -1,196 +0,0 @@
-SUBDIRS = . expect arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets rels parser sygus sep nl ho
-DIST_SUBDIRS = $(SUBDIRS)
-
-# don't override a BINARY imported from a personal.mk
-@mk_if@eq ($(BINARY),)
-@mk_empty@BINARY = cvc4
-end@mk_if@
-
-LOG_COMPILER = @srcdir@/../run_regression
-AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
-
-if AUTOMAKE_1_11
-# old-style (pre-automake 1.12) test harness
-TESTS_ENVIRONMENT = \
-	$(LOG_COMPILER) \
-	$(AM_LOG_FLAGS) $(LOG_FLAGS)
-endif
-
-MAKEFLAGS = -k
-
-# These are run for all build profiles.
-# If a test shouldn't be run in e.g. competition mode,
-# put it below in "TESTS +="
-
-# Regression tests for SMT inputs
-SMT_TESTS = \
-	distinct.smt \
-	flet.smt \
-	flet2.smt \
-	fuzz_1.smt \
-	fuzz_3.smt \
-	ineq_basic.smt \
-	ineq_slack.smt \
-	ite_real_int_type.smt \
-	ite_real_valid.smt \
-	let.smt \
-	let2.smt \
-	simplification_bug.smt \
-	simplification_bug2.smt \
-	simple.smt \
-	simple2.smt \
-	simple-lra.smt \
-	simple-rdl.smt \
-	simple-uf.smt \
-	constant-rewrite.smt
-
-# Regression tests for SMT2 inputs
-SMT2_TESTS = \
-	arrayinuf_declare.smt2 \
-	boolean-terms-kernel1.smt2 \
-	boolean-terms-bug-array.smt2 \
-	chained-equality.smt2 \
-	ite2.smt2 \
-	ite3.smt2 \
-	ite4.smt2 \
-	simple-lra.smt2 \
-	simple-rdl.smt2 \
-	simple-uf.smt2 \
-	parallel-let.smt2 \
-	get-value-incremental.smt2 \
-	get-value-reals.smt2 \
-	get-value-ints.smt2 \
-	get-value-reals-ints.smt2 \
-	hung13sdk_output1.smt2 \
-	hung10_itesdk_output2.smt2 \
-	hung10_itesdk_output1.smt2 \
-	hung13sdk_output2.smt2 \
-	declare-funs.smt2 \
-	declare-fun-is-match.smt2 \
-	issue1063-overloading-dt-cons.smt2 \
-	issue1063-overloading-dt-sel.smt2 \
-	issue1063-overloading-dt-fun.smt2 \
-	reset-assertions.smt2 \
-	rec-fun-const-parse-bug.smt2
-
-# Regression tests for PL inputs
-CVC_TESTS = \
-	boolean-prec.cvc \
-	boolean-terms.cvc \
-	ite.cvc \
-	let.cvc \
-	logops.01.cvc \
-	logops.02.cvc \
-	logops.03.cvc \
-	logops.04.cvc \
-	logops.05.cvc \
-	simple.cvc \
-	smallcnf.cvc \
-	test9.cvc \
-	test11.cvc \
-	uf20-03.cvc \
-	wiki.01.cvc \
-	wiki.02.cvc \
-	wiki.03.cvc \
-	wiki.04.cvc \
-	wiki.05.cvc \
-	wiki.06.cvc \
-	wiki.07.cvc \
-	wiki.08.cvc \
-	wiki.09.cvc \
-	wiki.10.cvc \
-	wiki.11.cvc \
-	wiki.12.cvc \
-	wiki.13.cvc \
-	wiki.14.cvc \
-	wiki.15.cvc \
-	wiki.16.cvc \
-	wiki.17.cvc \
-	wiki.18.cvc \
-	wiki.19.cvc \
-	wiki.20.cvc \
-	wiki.21.cvc \
-	queries0.cvc \
-	print_lambda.cvc \
-	cvc3.userdoc.01.cvc \
-	cvc3.userdoc.02.cvc \
-	cvc3.userdoc.03.cvc \
-	cvc3.userdoc.04.cvc \
-	cvc3.userdoc.05.cvc \
-	cvc3.userdoc.06.cvc
-
-# Regression tests for TPTP inputs
-TPTP_TESTS =
-
-# Regression tests derived from bug reports
-BUG_TESTS = \
-	smt2output.smt2 \
-	bug32.cvc \
-	bug49.smt \
-	bug161.smt \
-	bug164.smt \
-	bug167.smt \
-	bug168.smt \
-	bug187.smt2 \
-	bug217.smt2 \
-	bug220.smt2 \
-	bug239.smt \
-	bug274.cvc \
-	bug288.smt \
-	bug288b.smt \
-	bug288c.smt \
-	buggy-ite.smt2 \
-	bug303.smt2 \
-	bug310.cvc \
-	bug322.cvc \
-	bug322b.cvc \
-	bug339.smt2 \
-	bug365.smt2 \
-	bug382.smt2 \
-	bug383.smt2 \
-	bug398.smt2 \
-	bug421.smt2 \
-	bug421b.smt2 \
-	bug480.smt2 \
-	bug484.smt2 \
-	bug486.cvc \
-	bug512.minimized.smt2 \
-	bug521.minimized.smt2 \
-	bug522.smt2 \
-	bug528a.smt2 \
-	bug541.smt2 \
-	bug544.smt2 \
-	bug548a.smt2 \
-	bug576.smt2 \
-	bug576a.smt2 \
-	bug578.smt2 \
-	bug586.cvc \
-	bug595.cvc \
-	bug596.cvc \
-	bug596b.cvc \
-	bug605.cvc \
-	bug639.smt2 \
-	bt-test-00.smt2 \
-	bt-test-01.smt2 \
-	bug1247.smt2
-
-TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
-
-# bug512 -- taking too long, --time-per not working perhaps? in any case,
-# we have a minimized version still getting tested
-# bug639 -- still fails, reopened bug
-# bug585 -- contains subrange type (not supported)
-
-
-EXTRA_DIST = $(TESTS)
-
-# and make sure to distribute it
-EXTRA_DIST += $(DISABLED_TESTS)
-
-# synonyms for "check" in this directory
-.PHONY: regress regress0 test
-regress regress0 test: check
-
-# do nothing in this subdir
-.PHONY: regress1 regress2 regress3 regress4
-regress1 regress2 regress3 regress4: