isabelle: src/HOL/Tools/ATP/scripts/spass@e6b51fab96f7 (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}
47055 16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release blanchet parents: 46403 diff changeset	10	home=${SPASS_OLD_HOME:-$SPASS_HOME}
37962 d7dbe01f48d7 keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems; blanchet parents: diff changeset	11
47055 16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release blanchet parents: 46403 diff changeset	12	"$home/SPASS" -Flotter "$name" \
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()\.//' \
45304 e6901aa86a9e always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions blanchet parents: 45302 diff changeset	15	> $name.cnf
e6901aa86a9e always use DFG format to talk to SPASS -- since that's what we'll need to use anyway to benefit from sorts and other extensions blanchet parents: 45302 diff changeset	16	cat $name.cnf
47055 16e2633f3b4b made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release blanchet parents: 46403 diff changeset	17	"$home/SPASS" $options "$name.cnf" \
37990 586130f71c78 remove confusing line in SPASS output (because the axiom names are off -- bug in SPASS) blanchet parents: 37962 diff changeset	18	\| sed 's/$Formulae used in the proof :$.*/\1 N\/A/'
46403 3069344da626 improve SPASS scripts blanchet parents: 45304 diff changeset	19	rm -f "$name.cnf"

author	blanchet
	Mon, 21 May 2012 10:39:31 +0200
changeset 47944	e6b51fab96f7
parent 47055	16e2633f3b4b
permissions	-rwxr-xr-x