# HG changeset patch # User blanchet # Date 1328017161 -3600 # Node ID 7e049e9f5c8b7e4dbf00bf6a497b08071eda9072 # Parent de5dd84717c1ea34d6f0f16180255ed3474c3f3b new SPASS setup diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jan 31 12:43:48 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jan 31 14:39:21 2012 +0100 @@ -439,7 +439,7 @@ if top_level then case extract_isabelle_info info of SOME s' => if s' = simpN then s ^ ":lr" - else if s' = eqN then s ^ ":lr" (* not yet ":lt" *) + else if s' = eqN then s ^ ":lt" else s | NONE => s else diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 31 12:43:48 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jan 31 14:39:21 2012 +0100 @@ -1186,8 +1186,7 @@ |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts val lam_facts = map2 (fn t => fn j => - ((lam_fact_prefix ^ Int.toString j, (Global, General)), - (Axiom, t))) + ((lam_fact_prefix ^ Int.toString j, (Global, Eq)), (Axiom, t))) lambda_ts (1 upto length lambda_ts) in (facts, lam_facts) end diff -r de5dd84717c1 -r 7e049e9f5c8b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 31 12:43:48 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 31 14:39:21 2012 +0100 @@ -37,6 +37,7 @@ val e_default_sym_offs_weight : real Config.T val e_sym_offs_weight_base : real Config.T val e_sym_offs_weight_span : real Config.T + val spass_incompleteN : string val eN : string val e_sineN : string val e_tofofN : string @@ -312,6 +313,8 @@ (* SPASS *) +val spass_incompleteN = "incomplete" + (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of explicit application operators. *) val spass_config : atp_config = @@ -350,24 +353,21 @@ val spass_new_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass_new"), required_execs = [], - arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => - (* -Splits=0 -FullRed=0 -VarWeight=3? *) + arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ => ("-Auto -LR=1 -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) - |> sos = sosN ? prefix "-SOS=1 ", + |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ", proof_delims = #proof_delims spass_config, known_failures = #known_failures spass_config, conj_sym_kind = #conj_sym_kind spass_config, prem_kind = #prem_kind spass_config, best_slices = fn ctxt => (* FUDGE *) - [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", liftingN, - no_sosN))), + [(0.333, (false, (150, DFG DFG_Sorted, "poly_tags??", combs_and_liftingN, + ""))), (0.333, (false, (300, DFG DFG_Sorted, "mono_simple", liftingN, - no_sosN))), - (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", liftingN, - no_sosN)))] - |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single - else I)} + spass_incompleteN))), + (0.334, (false, (50, DFG DFG_Sorted, "mono_simple", combs_and_liftingN, + "")))]} val spass_new = (spass_newN, spass_new_config)