isabelle: src/HOL/TPTP/lib/Tools/tptp_refute@1b01a57d2749 (annotated)

46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	1	#!/usr/bin/env bash
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	2	#
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	3	# Author: Jasmin Blanchette
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	4	#
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	5	# DESCRIPTION: Refute for TPTP
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	6
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	7
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	8	PRG="$(basename "$0")"
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	9
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	10	function usage() {
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	11	echo
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	12	echo "Usage: isabelle $PRG TIMEOUT FILES"
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	13	echo
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	14	echo " Runs Refute on TPTP problems."
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	15	echo
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	16	exit 1
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	17	}
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	18
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	19	[ "$#" -eq 0 -o "$1" = "-?" ] && usage
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	20
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	21	SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	22
47670 24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	23	TIMEOUT=$1
24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	24	shift
24babc4b1925 added timeout argument to TPTP tools blanchet parents: 46324 diff changeset	25
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	26	for FILE in "$@"
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	27	do
46324 e4bccf5ec61e added problem importer blanchet parents: 46319 diff changeset	28	echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
47794 4ad62c5f9f88 thread theory cleanly and use "smt" method rather than Sledgehammer for Z3 (because of obscure debilitating bug) blanchet parents: 47670 diff changeset	29	ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end;" \
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	30	> /tmp/$SCRATCH.thy
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	31	"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	32	done

author	wenzelm
	Sat, 15 Dec 2012 13:14:55 +0100
changeset 50546	1b01a57d2749
parent 47794	4ad62c5f9f88
child 52096	7e9cd79e25b3
permissions	-rwxr-xr-x