isabelle: src/HOL/TPTP/lib/Tools/tptp_refute@e275d520f49d (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
54434 e275d520f49d implemented 'tptp_translate' blanchet parents: 52124 diff changeset	31	"$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP \| grep --line-buffered -v "^###\\|^PROOF FAILED for depth\\|^Failure node\\|inferences so far. Searching to depth\\|^val \\|^Loading theory"
46319 c248e4f1be74 rebranded Nitrox, for more uniformity blanchet parents: diff changeset	32	done

author	blanchet
	Thu, 14 Nov 2013 19:54:10 +0100
changeset 54434	e275d520f49d
parent 52124	c54170ee898b
child 60544	3daf5eacec05
permissions	-rwxr-xr-x