isabelle: src/HOL/Tools/ATP/scripts/spass@2621046c550a (annotated)

37962 d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	1	#!/usr/bin/env bash
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	2	#
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	3	# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	4	# Isar proof reconstruction)
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	5	#
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	6	# Author: Jasmin Blanchette, TU Muenchen
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	7
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	8	options=${@:1:$(($#-1))}
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	9	name=${@:$(($#)):1}
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	10
41456 006d85ad56d3 allow spaces in $SPASS_HOME value; wenzelm parents: 38046 diff changeset	11	"$SPASS_HOME/tptp2dfg" $name $name.fof.dfg
006d85ad56d3 allow spaces in $SPASS_HOME value; wenzelm parents: 38046 diff changeset	12	"$SPASS_HOME/SPASS" -Flotter $name.fof.dfg \
37962 d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	13	\| sed 's/description({$/description({*/' \
44391 7b4104df2be6 gracefully handle empty SPASS problems blanchet parents: 41456 diff changeset	14	\| sed 's/set_ClauseFormulaRelation()\.//' \
37962 d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	15	> $name.cnf.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	16	rm -f $name.fof.dfg
d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	17	cat $name.cnf.dfg
41456 006d85ad56d3 allow spaces in $SPASS_HOME value; wenzelm parents: 38046 diff changeset	18	"$SPASS_HOME/SPASS" $options $name.cnf.dfg \
37990 586130f71c78 remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS) blanchet parents: 37962 diff changeset	19	\| sed 's/$Formulae used in the proof :$.*/\1 N\/A/'
37962 d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	20	rm -f $name.cnf.dfg

author	blanchet
	Tue, 30 Aug 2011 16:07:46 +0200
changeset 44596	2621046c550a
parent 44391	7b4104df2be6
child 45302	04c87dec70b8
permissions	-rwxr-xr-x