Quelle  tptp_sledgehammer   Sprache: unbekannt

#!/usr/bin/env bash
#
# Author: Jasmin Blanchette
# Author: Martin Desharnais-Schäfer
#
# DESCRIPTION: Sledgehammer for TPTP

PRG="$(basename "$0")"

function usage() {
  echo
  echo "Usage: isabelle $PRG TIMEOUT FILES"
  echo
  echo " Runs Sledgehammer on TPTP problems."
  echo " Each problem is allocated at most TIMEOUT seconds."
  echo
  exit 1
}

[ "$#" -eq 0 -o "$1" = "-?" ] && usage

SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
SCRATCH_FILE=/tmp/${SCRATCH}.thy

TIMEOUT=$1
shift

for FILE in "$@"
do
  echo "theory ${SCRATCH} imports \"HOL-TPTP.ATP_Problem_Import\" begin java.lang.NullPointerException
ML ‹ ATP_Problem_Import.sledgehammer_tptp_file @{theory} (${TIMEOUT}) \"${FILE}\" › end" \
    > "${SCRATCH_FILE}"

  isabelle process_theories -O -U -l HOL-TPTP -f "${SCRATCH_FILE}" "${SCRATCH}" java.lang.NullPointerException
      | grep --line-buffered -vE java.lang.NullPointerException
          -e '^Running Draft ...$' java.lang.NullPointerException
          -e '^[[:space:]]*$' java.lang.NullPointerException
          -e '^Output \(line [[:digit:]]+ of ".*"):$' java.lang.NullPointerException
          -e '^val it = \(\): unit$' java.lang.NullPointerException
          -e '^Finished Draft \([0-9:]+ elapsed time(, [0-9:]+ cpu time, factor [0-9.]+)?\)$' java.lang.NullPointerException
          -e '^PROOF FAILED for depth' java.lang.NullPointerException
          -e '^Failure node' java.lang.NullPointerException
          -e 'inferences so far. Searching to depth' java.lang.NullPointerException
          -e '^val ' java.lang.NullPointerException
          -e 'Loading theory' java.lang.NullPointerException
          -e '^poly.*warning: The type of' java.lang.NullPointerException
          -e '^ monotype.$'
done