diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-04 19:01:55 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-04 19:01:55 +0000 |
commit | 3203c9bf8ec818b287c8b4030bb4b71d48ede9f1 (patch) | |
tree | cf737891c4f8edaaa05c7a362849165c8a20b5d5 /test/regress | |
parent | 70a4ae1e6a7dae928e2ec83bd190b9b81e11bf02 (diff) |
test infrastructure updated for multiple-level regressions
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/Makefile | 4 | ||||
-rw-r--r-- | test/regress/Makefile.am | 49 | ||||
-rw-r--r-- | test/regress/regress0/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 10 | ||||
-rw-r--r-- | test/regress/regress1/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress1/Makefile.am | 10 | ||||
-rw-r--r-- | test/regress/regress2/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress2/Makefile.am | 10 | ||||
-rw-r--r-- | test/regress/regress3/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress3/Makefile.am | 10 | ||||
-rwxr-xr-x | test/regress/run_regression | 77 |
11 files changed, 154 insertions, 48 deletions
diff --git a/test/regress/Makefile b/test/regress/Makefile index 06fe0f1fb..663fc1407 100644 --- a/test/regress/Makefile +++ b/test/regress/Makefile @@ -4,5 +4,5 @@ srcdir = test/regress include $(topdir)/Makefile.subdir # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: test +test: check diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 819a892bd..bec1fce3e 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,48 +1,5 @@ -TESTS_ENVIRONMENT = @top_builddir@/../../bin/cvc4 -TESTS = \ - simple.cvc \ - simple.smt \ - hole6.cvc \ - hole7.cvc \ - hole8.cvc \ - hole9.cvc \ - hole10.cvc \ - wiki.cvc \ - test9.cvc \ - test11.cvc \ - bmc-ibm-1.smt \ - bmc-ibm-2.smt \ - bmc-ibm-3.smt \ - bmc-ibm-4.smt \ - bmc-ibm-5.smt \ - uf20-03.cvc \ - qwh.35.405.shuffled-as.sat03-1651.smt \ - C880mul.miter.shuffled-as.sat03-348.smt \ - instance_1151.smt \ - instance_1444.smt - -#Tests that currently do not work -FUTURETESTS = \ - logops.cvc \ - test12.cvc \ - bug1.cvc \ - boolean.cvc - -#Tests that take too long to be put in the default regress level -#TODO Make multiple regression levels. Some of which are off by default. -LONGTESTS = \ - friedman_n4_i5.smt \ - friedman_n6_i4.smt \ - bmc-galileo-8.smt \ - bmc-galileo-9.smt \ - bmc-ibm-6.smt \ - bmc-ibm-7.smt \ - bmc-ibm-10.smt \ - bmc-ibm-11.smt \ - bmc-ibm-12.smt \ - bmc-ibm-13.smt \ - comb2.shuffled-as.sat03-420.smt +SUBDIRS = regress0 regress1 regress2 regress3 # synonyms for "check" -.PHONY: regress regress0 regress1 regress2 regress3 test -regress regress0 regress1 regress2 regress3 test: check +.PHONY: regress test +regress test: check diff --git a/test/regress/regress0/Makefile b/test/regress/regress0/Makefile new file mode 100644 index 000000000..894759aa3 --- /dev/null +++ b/test/regress/regress0/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress0 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am new file mode 100644 index 000000000..b0caacf1b --- /dev/null +++ b/test/regress/regress0/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress1/Makefile b/test/regress/regress1/Makefile new file mode 100644 index 000000000..b720980f1 --- /dev/null +++ b/test/regress/regress1/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress1 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am new file mode 100644 index 000000000..a99ed3f70 --- /dev/null +++ b/test/regress/regress1/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 +regress0 regress2 regress3: diff --git a/test/regress/regress2/Makefile b/test/regress/regress2/Makefile new file mode 100644 index 000000000..5a9aa63be --- /dev/null +++ b/test/regress/regress2/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress2 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am new file mode 100644 index 000000000..72742f201 --- /dev/null +++ b/test/regress/regress2/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress2 test +regress regress2 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress3 +regress0 regress1 regress3: diff --git a/test/regress/regress3/Makefile b/test/regress/regress3/Makefile new file mode 100644 index 000000000..223547305 --- /dev/null +++ b/test/regress/regress3/Makefile @@ -0,0 +1,8 @@ +topdir = ../../.. +srcdir = test/regress/regress3 + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am new file mode 100644 index 000000000..202bc553f --- /dev/null +++ b/test/regress/regress3/Makefile.am @@ -0,0 +1,10 @@ +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS = + +# synonyms for "check" +.PHONY: regress regress3 test +regress regress3 test: check + +# do nothing in this subdir +.PHONY: regress0 regress1 regress2 +regress0 regress1 regress2: diff --git a/test/regress/run_regression b/test/regress/run_regression new file mode 100755 index 000000000..4cf9f07cf --- /dev/null +++ b/test/regress/run_regression @@ -0,0 +1,77 @@ +#!/bin/bash +# +# Morgan Deters <mdeters@cs.nyu.edu> +# for the CVC4 project +# +# usage: +# +# run_regression cvc4-binary [ benchmark.cvc | benchmark.smt ] +# +# Runs benchmark and checks for correct exit status and output. +# + +prog=`basename "$0"` + +if [ $# != 2 ]; then + echo "usage: $prog cvc4-binary [ benchmark.cvc | benchmark.smt ]" >&2 + exit 1 +fi + +cvc4=$1 +benchmark=$2 + +function error { + echo "$prog: error: $*" + exit 1 +} + +if ! [ -x "$cvc4" ]; then + error "\`$cvc4' doesn't exist or isn't executable" >&2 +fi +if ! [ -r "$benchmark" ]; then + error "\`$benchmark' doesn't exist or isn't readable" >&2 +fi + +if expr "$benchmark" : '.*\.smt$' &>/dev/null; then + if grep '^ *:status *sat' &>/dev/null; then + expected_output=sat + expected_exit_status=10 + elif grep '^ *:status *unsat' &>/dev/null; then + expected_output=unsat + expected_exit_status=20 + else + error "cannot determine status of \`$benchmark'" + fi +elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then + expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` + if [ -z "$expected_output" ]; then + error "cannot determine status of \`$benchmark'" + fi + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` +else + error "benchmark \`$benchmark' must be *.cvc or *.smt" +fi + +expfile=`mktemp -t cvc4test.exp.XXXXXXXXXX` +outfile=`mktemp -t cvc4test.out.XXXXXXXXXX` +echo "$expected_output" >"$expfile" + +echo "$cvc4" --segv-nospin "$benchmark" +"$cvc4" --segv-nospin "$benchmark" | tee "$outfile" +exit_status=$? + +diffs=`diff -u "$expfile" "$outfile"` +rm -f "$expfile" +rm -f "$outfile" +if [ $? -ne 0 ]; then + echo "$prog: error: differences between expected and actual output" + echo "$diffs" + exit 1 +fi + +if [ -n "$expected_exit_status" ]; then + if [ $exit_status != "$expected_exit_status" ]; then + error "expected exit status \`$expected_exit_status' but got \`$exit_status'" + fi +fi + |