diff options
author | lianah <lianahady@gmail.com> | 2013-11-05 20:03:49 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-11-05 20:03:49 -0500 |
commit | ad0f78965f23b0994cac6a210650697b9a20cceb (patch) | |
tree | b28418322c642ecf7f3d47ba356c4026c4ece4be /test | |
parent | 347ac2260da73297776c547f7397b33beb59cf2b (diff) |
fixed proof regression script and added a new uf test case
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/uf/proof00.smt2 | 21 | ||||
-rwxr-xr-x | test/regress/run_regression | 16 |
3 files changed, 35 insertions, 5 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index bf9a36df1..19e673fea 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -42,7 +42,8 @@ TESTS = \ simple.01.cvc \ simple.02.cvc \ simple.03.cvc \ - simple.04.cvc + simple.04.cvc \ + proof00.smt2 EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/proof00.smt2 b/test/regress/regress0/uf/proof00.smt2 new file mode 100644 index 000000000..1b7e7b8dd --- /dev/null +++ b/test/regress/regress0/uf/proof00.smt2 @@ -0,0 +1,21 @@ +; PROOF +(set-logic QF_UF) +(set-info :source | +CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC + for more information. + +This benchmark was obtained by trying to find a finite model of a first-order +formula (Albert Oliveras). +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort U 0) +(declare-fun c3 () U) +(declare-fun f1 (U U) U) +(declare-fun f4 (U) U) +(declare-fun c2 () U) +(declare-fun c_0 () U) +(declare-fun c_1 () U) +(assert (let ((?v_1 (f1 c3 c_0))) (let ((?v_0 (f1 ?v_1 c_0)) (?v_2 (f1 c_0 c_0)) (?v_4 (f1 c_0 c_1)) (?v_3 (f1 ?v_1 c_1)) (?v_6 (f1 c3 c_1))) (let ((?v_5 (f1 ?v_6 c_0)) (?v_7 (f1 c_1 c_0)) (?v_9 (f1 c_1 c_1)) (?v_8 (f1 ?v_6 c_1)) (?v_10 (f4 c_0))) (let ((?v_11 (f1 c_0 ?v_10)) (?v_12 (f4 c_1))) (let ((?v_13 (f1 c_1 ?v_12)) (?v_15 (f1 c2 c_0))) (let ((?v_14 (f1 ?v_15 c_0)) (?v_16 (f1 ?v_15 c_1)) (?v_18 (f1 c2 c_1))) (let ((?v_17 (f1 ?v_18 c_0)) (?v_19 (f1 ?v_18 c_1))) (and (distinct c_0 c_1) (= (f1 ?v_0 c_0) (f1 c_0 ?v_2)) (= (f1 ?v_0 c_1) (f1 c_0 ?v_4)) (= (f1 ?v_3 c_0) (f1 c_1 ?v_2)) (= (f1 ?v_3 c_1) (f1 c_1 ?v_4)) (= (f1 ?v_5 c_0) (f1 c_0 ?v_7)) (= (f1 ?v_5 c_1) (f1 c_0 ?v_9)) (= (f1 ?v_8 c_0) (f1 c_1 ?v_7)) (= (f1 ?v_8 c_1) (f1 c_1 ?v_9)) (not (= ?v_11 (f1 ?v_10 ?v_11))) (not (= ?v_13 (f1 ?v_12 ?v_13))) (= (f1 ?v_14 c_0) (f1 (f1 ?v_2 c_0) c_0)) (= (f1 ?v_14 c_1) (f1 (f1 ?v_4 c_0) c_1)) (= (f1 ?v_16 c_0) (f1 (f1 ?v_2 c_1) c_0)) (= (f1 ?v_16 c_1) (f1 (f1 ?v_4 c_1) c_1)) (= (f1 ?v_17 c_0) (f1 (f1 ?v_7 c_0) c_0)) (= (f1 ?v_17 c_1) (f1 (f1 ?v_9 c_0) c_1)) (= (f1 ?v_19 c_0) (f1 (f1 ?v_7 c_1) c_0)) (= (f1 ?v_19 c_1) (f1 (f1 ?v_9 c_1) c_1)) (or (= ?v_2 c_0) (= ?v_2 c_1)) (or (= ?v_4 c_0) (= ?v_4 c_1)) (or (= ?v_7 c_0) (= ?v_7 c_1)) (or (= ?v_9 c_0) (= ?v_9 c_1)) (or (= ?v_10 c_0) (= ?v_10 c_1)) (or (= ?v_12 c_0) (= ?v_12 c_1)) (or (= c3 c_0) (= c3 c_1)) (or (= c2 c_0) (= c2 c_1))))))))))) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index e9c17a3af..44517cc0c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -112,7 +112,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then proof_command='(get-proof)' lang=smt2 if test -e "$benchmark.expect"; then - expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes` + expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && 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,,'` @@ -140,7 +140,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=10 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= + expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=20 command_line= @@ -276,8 +276,15 @@ fi if [ "$proof" = yes -a "$expected_proof" = yes ]; then gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - cp "$benchmark" "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; + # remove exit command to add proof command for smt2 benchmarks + if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then + head -n -0 "$benchmark" > "$pfbenchmark"; + echo "$proof_command" >>"$pfbenchmark"; + echo "(exit)" >> "$pfbenchmark"; + else + cp $benchmark $pfbenchmark + echo "$proof_command" >>"$pfbenchmark"; + fi echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof --segv-nospin `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] time ( :; \ ( cd `dirname "$pfbenchmark"`; @@ -286,6 +293,7 @@ if [ "$proof" = yes -a "$expected_proof" = yes ]; then ) > "$outfile" 2> "$errfile" ) gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX + diff --unchanged-group-format='' \ --old-group-format='' \ --new-group-format='%>' \ |