--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Jan 30 17:18:58 2012 +0100
@@ -2433,8 +2433,8 @@
(* Forcing explicit applications is expensive for polymorphic encodings, because
it takes only one existential variable ranging over "'a => 'b" to ruin
- everything. Hence we do it only if there are few facts (is normally the case
- for "metis" and the minimizer. *)
+ everything. Hence we do it only if there are few facts (which is normally the
+ case for "metis" and the minimizer). *)
val explicit_apply_threshold = 50
fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
@@ -2443,11 +2443,11 @@
val thy = Proof_Context.theory_of ctxt
val type_enc = type_enc |> adjust_type_enc format
val explicit_apply =
- if polymorphism_of_type_enc type_enc <> Polymorphic orelse
- length facts <= explicit_apply_threshold then
+ if polymorphism_of_type_enc type_enc = Polymorphic andalso
+ length facts >= explicit_apply_threshold then
+ SOME false
+ else
NONE
- else
- SOME false
val lam_trans =
if lam_trans = keep_lamsN andalso
not (is_type_enc_higher_order type_enc) then
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jan 30 17:18:58 2012 +0100
@@ -348,9 +348,12 @@
(* Experimental *)
val spass_new_config : atp_config =
- {exec = ("SPASS_HOME", "SPASS"),
+ {exec = ("ISABELLE_ATP", "scripts/spass_new"),
required_execs = [],
- arguments = #arguments spass_config,
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
+ (* -Splits=0 -FullRed=0 -VarWeight=3? *)
+ ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
+ |> sos = sosN ? prefix "-SOS=1 ",
proof_delims = #proof_delims spass_config,
known_failures = #known_failures spass_config,
conj_sym_kind = #conj_sym_kind spass_config,
@@ -358,11 +361,11 @@
best_slices = fn ctxt =>
(* FUDGE *)
[(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN,
- sosN))) (*,
- (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", liftingN,
- sosN))),
+ no_sosN))),
+ (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN,
+ no_sosN))),
(0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN,
- no_sosN)))*)]
+ no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/scripts/spass_new Mon Jan 30 17:18:58 2012 +0100
@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+#
+# Wrapper for SPASS 3.8 that also outputs the clause-to-formula relation
+#
+# Author: Jasmin Blanchette, TU Muenchen
+
+options=${@:1:$(($#-1))}
+name=${@:$(($#)):1}
+
+rm -f $name.prf
+"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options $name \
+ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
+cat $name.prf
+#rm -f $name.cnf