Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..

5 files changed, 28 insertions, 13 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3a4583805..e564b567a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -45,6 +45,7 @@ SMT2_TESTS = \
 
 # Regression tests for PL inputs
 CVC_TESTS = \
+	boolean.cvc \
 	boolean-prec.cvc \
 	hole6.cvc \
 	ite.cvc \
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc
index d6f428bdb..2d0eb59b2 100644
--- a/test/regress/regress0/boolean.cvc
+++ b/test/regress/regress0/boolean.cvc
@@ -804,5 +804,5 @@ a288 : BOOLEAN =
         ELSE FALSE
         ENDIF;
 QUERY a288;
-% EXIT: 20
 % PROOF
+% EXIT: 20
diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc
index 31204a6c1..ece29e17c 100644
--- a/test/regress/regress0/hole6.cvc
+++ b/test/regress/regress0/hole6.cvc
@@ -177,5 +177,5 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37;
 
 
 QUERY FALSE;
-% EXIT: 20
 % PROOF
+% EXIT: 20
diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc
index 1aedcbe2b..04c7dafe0 100644
--- a/test/regress/regress0/wiki.05.cvc
+++ b/test/regress/regress0/wiki.05.cvc
@@ -2,5 +2,5 @@ a, b, c : BOOLEAN;
 
 % EXPECT: valid
 QUERY a OR (a AND b) <=> a;
-% EXIT: 20
 % PROOF
+% EXIT: 20
diff --git a/test/regress/run_regression b/test/regress/run_regression
index b836b39f6..6c06175d2 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -52,6 +52,8 @@ function gettemp {
 
 tmpbenchmark=
 if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
+  proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1
+  lang=smt
   if test -e "$benchmark.expect"; then
     expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
@@ -68,9 +70,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
     command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
-    # this frustrates our auto-language-detection, so add explicit --lang
+    # this frustrates our auto-language-detection
     gettemp tmpbenchmark cvc4_benchmark.smt.$$.XXXXXXXXXX
-    command_line="${command_line:+$command_line }--lang=smt"
     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"
@@ -90,6 +91,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
+  proof_command='(get-proof)'
+  lang=smt2
   if test -e "$benchmark.expect"; then
     expected_proof=`grep -q '^% PROOF' "$benchmark.expect" && echo yes`
     expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
@@ -106,9 +109,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
     command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
     # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
-    # this frustrates our auto-language-detection, so add explicit --lang
+    # this frustrates our auto-language-detection
     gettemp tmpbenchmark cvc4_benchmark.smt2.$$.XXXXXXXXXX
-    command_line="${command_line:+$command_line }--lang=smt2"
     grep -v '^% \(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"
@@ -128,6 +130,8 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
+  proof_command='DUMP_PROOF;'
+  lang=cvc4
   expected_proof=`grep -q '^% PROOF' "$benchmark" && echo yes`
   expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
@@ -145,6 +149,8 @@ else
   error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2"
 fi
 
+command_line="${command_line:+$command_line }--lang=$lang"
+
 gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX
 gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX
 gettemp outfile cvc4_stdout.$$.XXXXXXXXXX
@@ -203,19 +209,27 @@ if [ "$exit_status" != "$expected_exit_status" ]; then
 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"`;
+  gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX
+  cp "$benchmark" "$pfbenchmark";
+  echo "$proof_command" >>"$pfbenchmark";
+  echo running $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`]
+  ( cd `dirname "$pfbenchmark"`;
+    "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"`;
     echo $? >"$exitstatusfile"
   ) > "$outfile" 2> "$errfile"
 
-  if [ ! -s "$outfile" ]; then
+  gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX
+  diff --unchanged-group-format='' \
+       --old-group-format='' \
+       --new-group-format='%>' \
+       "$expoutfile" "$outfile" > "$pfoutfile"
+  if [ ! -s "$pfoutfile" ]; 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 running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`]
+    if ! $LFSC "$pfoutfile" &> "$errfile"; then
       echo "$prog: error: proof checker failed (output follows)"
       cat "$errfile"
       exitcode=1