Commit 4d229969 authored by MARCHE Claude's avatar MARCHE Claude

prover: improved bench using eprover, spass

parent f0560855
#!/bin/sh
# tests for the safe prover
timelimit=5
timelimit=2
memlimit=1000
file=$1
......@@ -27,21 +27,21 @@ else
printf "Not proved $time\n" >> $report
fi
# zenon
# $WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s zenon-0.7.1 -p0 -itptp -max-size $memlimit"M" -max-time $timelimit"s" $file 2> $TMPERR > $TMP
# ret=$?
# res=`sed -n -e 's|.*(\* \(.*PROOF.*\) \*).*|\1|p' $TMP`
# time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
# printf "zenon: $res $time\n" >> $report
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s zenon-0.7.1 -p0 -itptp -max-size $memlimit"M" -max-time $timelimit"s" $file 2> $TMPERR > $TMP
ret=$?
res=`sed -n -e 's|.*(\* \(.*PROOF.*\) \*).*|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
printf "zenon: $res $time\n" >> $report
# eprover
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s eprover -s -R -xAuto -tAuto --cpu-limit=$timelimit --tstp-in $file 2> $TMPERR > $TMP
ret=$?
res=`sed -n -e 's|\(.*Proof.*\)|\1|p' $TMP`
res=`sed -n -e 's|# SZS status \(.*\)|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
printf "eprover: $res $time\n" >> $report
# SPASS
$WHY3CPULIMIT `expr $timelimit + 1` $memlimit -s SPASS -TPTP -PGiven=0 -PProblem=0 -TimeLimit=$timelimit $file 2> $TMPERR > $TMP
ret=$?
res=`sed -n -e 's|.*: \([^:]*.*Proof.*\)|\1|p' $TMP`
res=`sed -n -e 's|SPASS beiseite: \(.*\)|\1|p' $TMP`
time=`sed -n -e 's|.*time : \(.*\) s.*|\1|p' $TMPERR`
printf "SPASS: $res $time\n" >> $report
fi
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment