proof regressions

diff --git a/configure.ac b/configure.ac
index 922f654167c73b0e55bc5c3fb94cc0fdf3a380f0..729544391ce655d1a166f080c13309b0b6b083cc 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -478,7 +478,6 @@ if test "$enable_proof" = yes; then
   CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROOF"
 fi
 
-
 AC_MSG_CHECKING([whether to optimize libcvc4])
 
 AC_ARG_ENABLE([optimized],
@@ -722,6 +721,24 @@ if test "$CVC4_CONFIGURE_IN_BUILDS" = yes -a -n "$CXXTEST"; then
   esac
 fi
 
+AC_ARG_VAR(LFSC, [path to LFSC proof checker])
+AC_ARG_VAR(LFSCARGS, [arguments to pass to LFSC proof checker])
+if test -z "$LFSC"; then
+  AC_CHECK_PROGS(LFSC, lfsc, [], [])
+else
+  AC_CHECK_PROG(LFSC, "$LFSC", [], [])
+fi
+AM_CONDITIONAL([PROOF_REGRESSIONS], [test -n "$LFSC" -a "$enable_proof" = yes])
+if test -z "$LFSC"; then
+  support_proof_tests='no, lfsc proof checker unavailable'
+elif test "$enable_proof" = yes; then
+  support_proof_tests='yes, proof regression tests enabled'
+else
+  support_proof_tests='no, proof generation disabled for this build'
+fi
+AC_SUBST([LFSC])
+AC_SUBST([LFSCARGS])
+
 CXXTESTGEN=
 AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH])
 if test -z "$CXXTESTGEN"; then
@@ -1061,6 +1078,7 @@ Dumping      : $enable_dumping
 Muzzle       : $enable_muzzle
 
 Unit tests   : $support_unit_tests
+Proof tests  : $support_proof_tests
 gcov support : $enable_coverage
 gprof support: $enable_profiling
 CUDD         : $cvc4cudd

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 948731057122a5a817a3e9f03cada7dee9c8560e..3a4583805dba7d13cbae50ff4d2a8f8f5a89498d 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,6 +1,11 @@
 SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess
 
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../run_regression --proof @top_builddir@/src/main/cvc4
+else
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+endif
+
 MAKEFLAGS = -k
 
 # These are run for all build profiles.

diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index fe3450c27dd60f91330aef8fb0da8d7eb498b922..d6f428bdb3f0302e5c9fa078d33afbeca9a1bbd1 100644 (file)
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -805,3 +805,4 @@ a288 : BOOLEAN =
         ENDIF;
 QUERY a288;
 % EXIT: 20
+% PROOF

diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index 64231aaf5862946fac0549a07e041ad087d5716f..31204a6c1d2f5d8656073d20811a7891236d0fea 100644 (file)
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -178,3 +178,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
 
 QUERY FALSE;
 % EXIT: 20
+% PROOF

diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index 9469a990214d823176af6d708415870545072d82..1aedcbe2b09752c552e63598326cd0b6ce518191 100644 (file)
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -3,3 +3,4 @@ a, b, c : BOOLEAN;
 % EXPECT: valid
 QUERY a OR (a AND b) <=> a;
 % EXIT: 20
+% PROOF

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 28bb5cb4253df267040b314df973462f59517e64..b836b39f621b1a869edbb7b251ee2eeabfc72ec1 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -5,18 +5,24 @@
 #
 # usage:
 #
-#     run_regression cvc4-binary [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
+#     run_regression cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]
 #
 # 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 | benchmark.smt2 ]" >&2
+if [ $# -lt 2 -o $# -gt 3 ]; then
+  echo "usage: $prog cvc4-binary [ --proof ] [ benchmark.cvc | benchmark.smt | benchmark.smt2 ]" >&2
   exit 1
 fi
 
+proof=no
+if [ $1 = --proof ]; then
+  proof=yes
+  shift
+fi
+
 cvc4=$1
 benchmark=$2
 
@@ -47,6 +53,7 @@ function gettemp {
 tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   if test -e "$benchmark.expect"; then
+    expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -54,7 +61,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+  elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+    expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -63,16 +71,18 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     # this frustrates our auto-language-detection, so add explicit --lang
     gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
     command_line="${command_line:+$command_line }--lang=smt"
-    grep -v '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
+    grep -v '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" >"$tmpbenchmark"
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
     benchmark=$tmpbenchmark
   elif grep '^ *:status  *sat' "$benchmark" &>/dev/null; then
+    expected_proof=
     expected_output=sat
     expected_exit_status=10
     command_line=
   elif grep '^ *:status  *unsat' "$benchmark" &>/dev/null; then
+    expected_proof=
     expected_output=unsat
     expected_exit_status=20
     command_line=
@@ -81,6 +91,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
   fi
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
   if test -e "$benchmark.expect"; then
+    expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -88,7 +99,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     if [ -z "$expected_exit_status" ]; then
       error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
     fi
-  elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+  elif grep -q '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
+    expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
     expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
@@ -103,10 +115,12 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     fi
     benchmark=$tmpbenchmark
   elif grep '^ *(set-info  *:status  *sat' "$benchmark" &>/dev/null; then
+    expected_proof=
     expected_output=sat
     expected_exit_status=10
     command_line=
   elif grep '^ *(set-info  *:status  *unsat' "$benchmark" &>/dev/null; then
+    expected_proof=
     expected_output=unsat
     expected_exit_status=20
     command_line=
@@ -114,6 +128,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
+  expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
   expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
   if [ -z "$expected_output" -a -z "$expected_error" ]; then
@@ -183,8 +198,29 @@ if [ $diffexiterr -ne 0 ]; then
 fi
 
 if [ "$exit_status" != "$expected_exit_status" ]; then
-  echo  "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
+  echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'"
   exitcode=1
 fi
 
+if [ "$proof" = yes -a "$expected_proof" = yes ]; then
+  echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"` [from working dir `dirname "$benchmark"`]
+  ( cd `dirname "$benchmark"`;
+    "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$benchmark"`;
+    echo $? >"$exitstatusfile"
+  ) > "$outfile" 2> "$errfile"
+
+  if [ ! -s "$outfile" ]; then
+    echo "$prog: error: proof generation failed with empty output (stderr follows)"
+    cat "$errfile"
+    exitcode=1
+  else
+    echo running $LFSC "$outfile" [from working dir `dirname "$benchmark"`]
+    if ! $LFSC "$outfile" &> "$errfile"; then
+      echo "$prog: error: proof checker failed (output follows)"
+      cat "$errfile"
+      exitcode=1
+    fi
+  fi
+fi
+
 exit $exitcode