# HG changeset patch # User blanchet # Date 1332265365 -3600 # Node ID 16e2633f3b4bca059c7b6007504fed1a2e956008 # Parent b86864a2b16e6b916ec4426f5856b89d525c430f made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 18:42:45 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Mar 20 18:42:45 2012 +0100 @@ -117,14 +117,14 @@ fun run_some_atp ctxt format problem = let val thy = Proof_Context.theory_of ctxt - val prob_file = File.tmp_path (Path.explode "prob.tptp") + val prob_file = File.tmp_path (Path.explode "prob") val atp = case format of DFG _ => spass_newN | _ => eN val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp val ord = effective_term_order ctxt atp val _ = problem |> lines_for_atp_problem format ord (K []) |> File.write_list prob_file val command = - File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^ + File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^ " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ File.shell_path prob_file in diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 18:42:45 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Mar 20 18:42:45 2012 +0100 @@ -14,8 +14,8 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string * string, - required_execs : (string * string) list, + {exec : string list * string, + required_vars : string list list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -51,12 +51,12 @@ val satallaxN : string val snarkN : string val spassN : string + val spass_oldN : string val spass_newN : string val vampireN : string val waldmeisterN : string val z3_tptpN : string val remote_prefix : string - val effective_term_order : Proof.context -> string -> term_order val remote_atp : string -> string -> string list -> (string * string) list -> (failure * string) list -> formula_kind -> formula_kind @@ -66,6 +66,7 @@ val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool val refresh_systems_on_tptp : unit -> unit + val effective_term_order : Proof.context -> string -> term_order val setup : theory -> theory end; @@ -81,8 +82,8 @@ type slice_spec = int * atp_format * string * string * bool type atp_config = - {exec : string * string, - required_execs : (string * string) list, + {exec : string list * string, + required_vars : string list list, arguments : Proof.context -> bool -> string -> Time.time -> term_order * (unit -> (string * int) list) @@ -133,7 +134,7 @@ (* named ATPs *) val alt_ergoN = "alt_ergo" -val dummy_thfN = "dummy_thf" (* experimental *) +val dummy_thfN = "dummy_thf" (* for experiments *) val eN = "e" val e_sineN = "e_sine" val e_tofofN = "e_tofof" @@ -143,7 +144,8 @@ val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" -val spass_newN = "spass_new" (* experimental *) +val spass_oldN = "spass_old" (* for experiments *) +val spass_newN = "spass_new" (* for experiments *) val vampireN = "vampire" val waldmeisterN = "waldmeister" val z3_tptpN = "z3_tptp" @@ -178,30 +180,13 @@ val term_order = Attrib.setup_config_string @{binding atp_term_order} (K smartN) -fun effective_term_order ctxt atp = - let val ord = Config.get ctxt term_order in - if ord = smartN then - if atp = spass_newN then - {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true} - else - {is_lpo = false, gen_weights = false, gen_prec = false, - gen_simp = false} - else - let val is_lpo = String.isSubstring lpoN ord in - {is_lpo = is_lpo, - gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, - gen_prec = String.isSubstring xprecN ord, - gen_simp = String.isSubstring xsimpN ord} - end - end - (* Alt-Ergo *) val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit) val alt_ergo_config : atp_config = - {exec = ("WHY3_HOME", "why3"), - required_execs = [], + {exec = (["WHY3_HOME"], "why3"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "--format tff1 --prover alt-ergo --timelimit " ^ @@ -222,7 +207,7 @@ (* E *) -fun is_old_e_version () = (string_ord (getenv "E_VERSION", "1.3") = LESS) +fun is_new_e_version () = (string_ord (getenv "E_VERSION", "1.2") = GREATER) val tstp_proof_delims = [("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation"), @@ -300,11 +285,11 @@ end fun effective_e_selection_heuristic ctxt = - if is_old_e_version () then e_autoN else Config.get ctxt e_selection_heuristic + if is_new_e_version () then Config.get ctxt e_selection_heuristic else e_autoN val e_config : atp_config = - {exec = ("E_HOME", "eproof"), - required_execs = [], + {exec = (["E_HOME"], "eproof"), + required_vars = [], arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) => @@ -340,8 +325,8 @@ val leo2_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice) val leo2_config : atp_config = - {exec = ("LEO2_HOME", "leo"), - required_execs = [], + {exec = (["LEO2_HOME"], "leo"), + required_vars = [], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) @@ -368,8 +353,8 @@ val satallax_thf0 = THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice) val satallax_config : atp_config = - {exec = ("SATALLAX_HOME", "satallax"), - required_execs = [], + {exec = (["SATALLAX_HOME"], "satallax"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "-p hocore -t " ^ string_of_int (to_secs 1 timeout), @@ -387,11 +372,15 @@ (* SPASS *) -(* The "-VarWeight=3" option helps the higher-order problems, probably by - counteracting the presence of explicit application operators. *) -val spass_config : atp_config = - {exec = ("ISABELLE_ATP", "scripts/spass"), - required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], +fun is_new_spass_version () = + string_ord (getenv "SPASS_VERSION", "3.7") = GREATER orelse + getenv "SPASS_NEW_HOME" <> "" + +(* TODO: Legacy: Remove after planned Isabelle2012 release (and don't forget + "required_vars" and "script/spass"). *) +val spass_old_config : atp_config = + {exec = (["ISABELLE_ATP"], "scripts/spass"), + required_vars = [["SPASS_OLD_HOME", "SPASS_HOME"]], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) @@ -415,7 +404,7 @@ (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false), no_sosN)))] |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} -val spass = (spassN, spass_config) +val spass_old = (spass_oldN, spass_old_config) val spass_new_H2 = "-Heuristic=2" val spass_new_H2SOS = "-Heuristic=2 -SOS" @@ -423,17 +412,16 @@ val spass_new_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" -(* Experimental *) val spass_new_config : atp_config = - {exec = ("SPASS_NEW_HOME", "SPASS"), - required_execs = [], + {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"), + required_vars = [], arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ => ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout)) |> extra_options <> "" ? prefix (extra_options ^ " "), - 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, + proof_delims = #proof_delims spass_old_config, + known_failures = #known_failures spass_old_config, + conj_sym_kind = #conj_sym_kind spass_old_config, + prem_kind = #prem_kind spass_old_config, best_slices = fn _ => (* FUDGE *) [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))), @@ -447,19 +435,22 @@ val spass_new = (spass_newN, spass_new_config) +fun spass () = + (spassN, if is_new_spass_version () then spass_new_config + else spass_old_config) (* Vampire *) (* Vampire 1.8 has TFF support, but it's buggy and therefore disabled on SystemOnTPTP. *) -fun is_old_vampire_version () = - string_ord (getenv "VAMPIRE_VERSION", "1.8") <> GREATER +fun is_new_vampire_version () = + string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val vampire_config : atp_config = - {exec = ("VAMPIRE_HOME", "vampire"), - required_execs = [], + {exec = (["VAMPIRE_HOME"], "vampire"), + required_vars = [], arguments = fn _ => fn _ => fn sos => fn timeout => fn _ => "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ " --proof tptp --output_axiom_names on\ @@ -482,14 +473,14 @@ prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) - (if is_old_vampire_version () then + (if is_new_vampire_version () then + [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), + (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), + (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))] + else [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false), sosN))), (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false), sosN))), - (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))] - else - [(0.333, (false, ((150, vampire_tff0, "poly_guards??", combs_or_liftingN, false), sosN))), - (0.333, (false, ((500, vampire_tff0, "mono_native", combs_or_liftingN, false), sosN))), - (0.334, (true, ((50, vampire_tff0, "mono_native", combs_or_liftingN, false), no_sosN)))]) + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false), no_sosN)))]) |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)} @@ -501,8 +492,8 @@ val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) val z3_tptp_config : atp_config = - {exec = ("Z3_HOME", "z3"), - required_execs = [], + {exec = (["Z3_HOME"], "z3"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout), proof_delims = [], @@ -522,8 +513,8 @@ (* Not really a prover: Experimental Polymorphic TFF and THF output *) fun dummy_config format type_enc : atp_config = - {exec = ("ISABELLE_ATP", "scripts/dummy_atp"), - required_execs = [], + {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"), + required_vars = [], arguments = K (K (K (K (K "")))), proof_delims = [], known_failures = known_szs_status_failures, @@ -581,8 +572,8 @@ fun remote_config system_name system_versions proof_delims known_failures conj_sym_kind prem_kind best_slice : atp_config = - {exec = ("ISABELLE_ATP", "scripts/remote_atp"), - required_execs = [], + {exec = (["ISABELLE_ATP"], "scripts/remote_atp"), + required_vars = [], arguments = fn _ => fn _ => fn _ => fn timeout => fn _ => "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^ " -s " ^ the_system system_name system_versions, @@ -663,18 +654,37 @@ val supported_atps = Symtab.keys o Data.get fun is_atp_installed thy name = - let val {exec, required_execs, ...} = get_atp thy name in - forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) + let val {exec, required_vars, ...} = get_atp thy name in + forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars) end fun refresh_systems_on_tptp () = Synchronized.change systems (fn _ => get_systems ()) -val atps = - [alt_ergo, e, leo2, dummy_thf, satallax, spass, spass_new, vampire, z3_tptp, - remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, - remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark, - remote_waldmeister] -val setup = fold add_atp atps +fun effective_term_order ctxt atp = + let val ord = Config.get ctxt term_order in + if ord = smartN then + if atp = spass_newN orelse + (atp = spassN andalso is_new_spass_version ()) then + {is_lpo = false, gen_weights = true, gen_prec = false, gen_simp = true} + else + {is_lpo = false, gen_weights = false, gen_prec = false, + gen_simp = false} + else + let val is_lpo = String.isSubstring lpoN ord in + {is_lpo = is_lpo, + gen_weights = not is_lpo andalso String.isSubstring xweightsN ord, + gen_prec = String.isSubstring xprecN ord, + gen_simp = String.isSubstring xsimpN ord} + end + end + +fun atps () = + [alt_ergo, e, leo2, dummy_thf, satallax, spass_old, spass_new, spass (), + vampire, z3_tptp, remote_e, remote_e_sine, remote_e_tofof, remote_iprover, + remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, + remote_z3_tptp, remote_snark, remote_waldmeister] + +fun setup thy = fold add_atp (atps ()) thy end; diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/Tools/ATP/scripts/spass --- a/src/HOL/Tools/ATP/scripts/spass Tue Mar 20 18:42:45 2012 +0100 +++ b/src/HOL/Tools/ATP/scripts/spass Tue Mar 20 18:42:45 2012 +0100 @@ -7,12 +7,13 @@ options=${@:1:$(($#-1))} name=${@:$(($#)):1} +home=${SPASS_OLD_HOME:-$SPASS_HOME} -"$SPASS_HOME/SPASS" -Flotter "$name" \ +"$home/SPASS" -Flotter "$name" \ | sed 's/description({$/description({*/' \ | sed 's/set_ClauseFormulaRelation()\.//' \ > $name.cnf cat $name.cnf -"$SPASS_HOME/SPASS" $options "$name.cnf" \ +"$home/SPASS" $options "$name.cnf" \ | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/' rm -f "$name.cnf" diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 18:42:45 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 20 18:42:45 2012 +0100 @@ -215,8 +215,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put SPASS first. *) fun default_provers_param_value ctxt = - [spassN, spass_newN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, - waldmeisterN] + [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN] |> map_filter (remotify_prover_if_not_installed ctxt) |> avoid_too_many_threads ctxt (Multithreading.max_threads_value (), max_default_remote_threads) diff -r b86864a2b16e -r 16e2633f3b4b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 18:42:45 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Mar 20 18:42:45 2012 +0100 @@ -580,7 +580,7 @@ val atp_timeout_slack = seconds 1.0 fun run_atp mode name - ({exec, required_execs, arguments, proof_delims, known_failures, + ({exec, required_vars, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, best_slices, ...} : atp_config) (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_relevant, max_mono_iters, @@ -605,7 +605,11 @@ Path.append (Path.explode dest_dir) problem_file_name else error ("No such directory: " ^ quote dest_dir ^ ".") - val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) + val command = + case find_first (fn var => getenv var <> "") (fst exec) of + SOME var => Path.explode (getenv var ^ "/" ^ snd exec) + | NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^ + " is not set.") fun split_time s = let val split = String.tokens (fn c => str c = "\n") @@ -622,10 +626,12 @@ as_time t |> Time.fromMilliseconds) end fun run_on prob_file = - case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of - (home_var, _) :: _ => - error ("The environment variable " ^ quote home_var ^ " is not set.") - | [] => + case find_first (forall (fn var => getenv var = "")) + (fst exec :: required_vars) of + SOME home_vars => + error ("The environment variable " ^ quote (hd home_vars) ^ + " is not set.") + | NONE => if File.exists command then let (* If slicing is disabled, we expand the last slice to fill the