Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Newer
Older
100755 21 lines (15 sloc) 0.429 kb
42ebcb3 Several new scripts to facilitate exploration with TPTP files.
Jesse Alama authored
1 #!/bin/bash -
2
70c04ba Use ulimit to cap the amount of time for a proof.
Jesse Alama authored
3 theory=$1;
e9e752a syntax error in assigning the default value
Jesse Alama authored
4 timeout=${2-"30"};
70c04ba Use ulimit to cap the amount of time for a proof.
Jesse Alama authored
5
e82ad07 assign a default value to the timeout
Jesse Alama authored
6 if [ -z $theory ]; then
7 echo "Usage: `basename $0` THEORY [TIMEOUT]";
9b7b170 exit if called incorrectly
Jesse Alama authored
8 exit 1;
e82ad07 assign a default value to the timeout
Jesse Alama authored
9 fi
70c04ba Use ulimit to cap the amount of time for a proof.
Jesse Alama authored
10
89644a9 die if the theory isn't readable
Jesse Alama authored
11 if [ ! -r $theory ]; then
12 echo "Error: the supplied theory '$theory' is not readable.";
13 exit 1;
14 fi
15
aa684aa check argument to ulimit -t
Jesse Alama authored
16 ulimit -t $timeout \
17 || (echo "Error: '$timeout' is not an acceptable argument to ulimit -t." && exit 1);
e82ad07 assign a default value to the timeout
Jesse Alama authored
18
d4bf913 dump memory limit
Jesse Alama authored
19 eprover -l4 -xAuto -tAuto -R --tptp3-in $theory \
1144d5a Use the sentries.
Jesse Alama authored
20 | eprover-sentry.pl
Something went wrong with that request. Please try again.