equal
deleted
inserted
replaced
7 |
7 |
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() { |
10 function usage() { |
11 echo |
11 echo |
12 echo "Usage: isabelle $PRG FILES" |
12 echo "Usage: isabelle $PRG TIMEOUT FILES" |
13 echo |
13 echo |
14 echo " Runs Sledgehammer on TPTP problems." |
14 echo " Runs Sledgehammer on TPTP problems." |
|
15 echo " Each problem is allocated at most TIMEOUT seconds." |
15 echo |
16 echo |
16 exit 1 |
17 exit 1 |
17 } |
18 } |
18 |
19 |
19 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
20 [ "$#" -eq 0 -o "$1" = "-?" ] && usage |
20 |
21 |
21 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 SCRATCH="Scratch_${PRG}_$$_${RANDOM}" |
22 |
23 |
|
24 TIMEOUT=$1 |
|
25 shift |
|
26 |
23 for FILE in "$@" |
27 for FILE in "$@" |
24 do |
28 do |
25 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
29 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \ |
26 ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \ |
30 ML {* ATP_Problem_Import.sledgehammer_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \ |
27 > /tmp/$SCRATCH.thy |
31 > /tmp/$SCRATCH.thy |
28 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
32 "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" |
29 done |
33 done |