use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200
@@ -66,7 +66,7 @@
val ord = effective_term_order ctxt atp
val _ = problem |> lines_for_atp_problem format ord (K [])
|> File.write_list prob_file
- val path = getenv (List.last (fst exec)) ^ "/" ^ snd exec
+ val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
val command =
File.shell_path (Path.explode path) ^
" " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 20 22:19:45 2012 +0200
@@ -14,8 +14,7 @@
type slice_spec = int * atp_format * string * string * bool
type atp_config =
- {exec : string list * string,
- required_vars : string list list,
+ {exec : string list * string list,
arguments :
Proof.context -> bool -> string -> Time.time
-> term_order * (unit -> (string * int) list)
@@ -87,8 +86,7 @@
type slice_spec = int * atp_format * string * string * bool
type atp_config =
- {exec : string list * string,
- required_vars : string list list,
+ {exec : string list * string list,
arguments :
Proof.context -> bool -> string -> Time.time
-> term_order * (unit -> (string * int) list)
@@ -190,8 +188,7 @@
val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
val alt_ergo_config : atp_config =
- {exec = (["WHY3_HOME"], "why3"),
- required_vars = [],
+ {exec = (["WHY3_HOME"], ["why3"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"--format tff1 --prover alt-ergo --timelimit " ^
@@ -263,7 +260,7 @@
\--prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconjmax -F1 \
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*" ^
e_selection_heuristic_case heuristic "FunWeight" "SymOffsetWeight" ^
- "(SimulateSOS, " ^
+ "(SimulateSOS," ^
(e_selection_heuristic_case heuristic
e_default_fun_weight e_default_sym_offs_weight
|> Config.get ctxt |> Real.ceil |> signed_string_of_int) ^
@@ -303,8 +300,7 @@
fun e_kbo () = if is_recent_e_version () then "KBO6" else "KBO"
val e_config : atp_config =
- {exec = (["E_HOME"], "eproof"),
- required_vars = [],
+ {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
arguments =
fn ctxt => fn full_proof => fn heuristic => fn timeout =>
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
@@ -314,11 +310,7 @@
"--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
"--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
e_shell_level_argument full_proof,
- proof_delims =
- (* work-around for bug in "epclextract" version 1.6 *)
- ("# SZS status Theorem\n# SZS output start Saturation.",
- "# SZS output end Saturation.") ::
- tstp_proof_delims,
+ proof_delims = tstp_proof_delims,
known_failures =
[(TimedOut, "Failure: Resource limit exceeded (time)"),
(TimedOut, "time limit exceeded")] @
@@ -348,8 +340,7 @@
THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
val leo2_config : atp_config =
- {exec = (["LEO2_HOME"], "leo"),
- required_vars = [],
+ {exec = (["LEO2_HOME"], ["leo"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"--foatp e --atp e=\"$E_HOME\"/eprover \
@@ -377,8 +368,7 @@
THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
val satallax_config : atp_config =
- {exec = (["SATALLAX_HOME"], "satallax"),
- required_vars = [],
+ {exec = (["SATALLAX_HOME"], ["satallax"]),
arguments =
fn _ => fn _ => fn _ => fn timeout => fn _ =>
"-p hocore -t " ^ string_of_int (to_secs 1 timeout),
@@ -405,8 +395,7 @@
(* FIXME: Make "SPASS_NEW_HOME" legacy. *)
val spass_config : atp_config =
- {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], "SPASS"),
- required_vars = [],
+ {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
|> extra_options <> "" ? prefix (extra_options ^ " "),
@@ -447,8 +436,7 @@
val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
val vampire_config : atp_config =
- {exec = (["VAMPIRE_HOME"], "vampire"),
- required_vars = [],
+ {exec = (["VAMPIRE_HOME"], ["vampire"]),
arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
"--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
" --proof tptp --output_axiom_names on\
@@ -491,8 +479,7 @@
val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
val z3_tptp_config : atp_config =
- {exec = (["Z3_HOME"], "z3"),
- required_vars = [],
+ {exec = (["Z3_HOME"], ["z3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
"MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
proof_delims = [],
@@ -513,8 +500,7 @@
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
fun dummy_config format type_enc : atp_config =
- {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"),
- required_vars = [],
+ {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
arguments = K (K (K (K (K "")))),
proof_delims = [],
known_failures = known_szs_status_failures,
@@ -577,8 +563,7 @@
fun remote_config system_name system_versions proof_delims known_failures
prem_role best_slice : atp_config =
- {exec = (["ISABELLE_ATP"], "scripts/remote_atp"),
- required_vars = [],
+ {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
(if command <> "" then "-c " ^ quote command ^ " " else "") ^
"-s " ^ the_system system_name system_versions ^ " " ^
@@ -660,8 +645,8 @@
val supported_atps = Symtab.keys o Data.get
fun is_atp_installed thy name =
- let val {exec, required_vars, ...} = get_atp thy name () in
- forall (exists (fn var => getenv var <> "")) (fst exec :: required_vars)
+ let val {exec, ...} = get_atp thy name () in
+ exists (fn var => getenv var <> "") (fst exec)
end
fun refresh_systems_on_tptp () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Jul 20 22:19:45 2012 +0200
@@ -631,9 +631,8 @@
val mono_max_privileged_facts = 10
fun run_atp mode name
- ({exec, required_vars, arguments, proof_delims, known_failures,
- prem_role, best_slices, best_max_mono_iters,
- best_max_new_mono_instances, ...} : atp_config)
+ ({exec, arguments, proof_delims, known_failures, prem_role, best_slices,
+ best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, max_facts, max_mono_iters,
max_new_mono_instances, isar_proof, isar_shrink_factor,
@@ -660,9 +659,17 @@
Path.append (Path.explode dest_dir) problem_file_name
else
error ("No such directory: " ^ quote dest_dir ^ ".")
- val command =
+ val command0 =
case find_first (fn var => getenv var <> "") (fst exec) of
- SOME var => Path.explode (getenv var ^ "/" ^ snd exec)
+ SOME var =>
+ let
+ val pref = getenv var ^ "/"
+ val paths = map (Path.explode o prefix pref) (snd exec)
+ in
+ case find_first File.exists paths of
+ SOME path => path
+ | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
+ end
| NONE => error ("The environment variable " ^ quote (hd (fst exec)) ^
" is not set.")
fun split_time s =
@@ -680,179 +687,162 @@
raw_explode #> Scan.read Symbol.stopper time #> the_default 0
in (output, as_time t |> Time.fromMilliseconds) end
fun run_on prob_file =
- 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 entire
+ time available. *)
+ val actual_slices = get_slices slice (best_slices ctxt)
+ val num_actual_slices = length actual_slices
+ fun monomorphize_facts facts =
+ let
+ val ctxt =
+ ctxt
+ |> repair_monomorph_context max_mono_iters best_max_mono_iters
+ max_new_mono_instances best_max_new_mono_instances
+ (* pseudo-theorem involving the same constants as the subgoal *)
+ val subgoal_th =
+ Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy
+ val rths =
+ facts |> chop mono_max_privileged_facts
+ |>> map (pair 1 o snd)
+ ||> map (pair 2 o snd)
+ |> op @
+ |> cons (0, subgoal_th)
+ in
+ Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl
+ |> curry ListPair.zip (map fst facts)
+ |> maps (fn (name, rths) =>
+ map (pair name o zero_var_indexes o snd) rths)
+ end
+ fun run_slice time_left (cache_key, cache_value)
+ (slice, (time_frac, (complete,
+ (key as (best_max_facts, format, best_type_enc,
+ best_lam_trans, best_uncurried_aliases),
+ extra)))) =
let
- (* If slicing is disabled, we expand the last slice to fill the
- entire time available. *)
- val actual_slices = get_slices slice (best_slices ctxt)
- val num_actual_slices = length actual_slices
- fun monomorphize_facts facts =
- let
- val ctxt =
- ctxt
- |> repair_monomorph_context max_mono_iters best_max_mono_iters
- max_new_mono_instances best_max_new_mono_instances
- (* pseudo-theorem involving the same constants as the subgoal *)
- val subgoal_th =
- Logic.list_implies (hyp_ts, concl_t)
- |> Skip_Proof.make_thm thy
- val rths =
- facts |> chop mono_max_privileged_facts
- |>> map (pair 1 o snd)
- ||> map (pair 2 o snd)
- |> op @
- |> cons (0, subgoal_th)
- in
- Monomorph.monomorph atp_schematic_consts_of rths ctxt
- |> fst |> tl
- |> curry ListPair.zip (map fst facts)
- |> maps (fn (name, rths) =>
- map (pair name o zero_var_indexes o snd) rths)
- end
- fun run_slice time_left (cache_key, cache_value)
- (slice, (time_frac, (complete,
- (key as (best_max_facts, format, best_type_enc,
- best_lam_trans, best_uncurried_aliases),
- extra)))) =
- let
- val num_facts =
- length facts |> is_none max_facts ? Integer.min best_max_facts
- val soundness = if strict then Strict else Non_Strict
- val type_enc =
- type_enc |> choose_type_enc soundness best_type_enc format
- val sound = is_type_enc_sound type_enc
- val real_ms = Real.fromInt o Time.toMilliseconds
- val slice_timeout =
- ((real_ms time_left
- |> (if slice < num_actual_slices - 1 then
- curry Real.min (time_frac * real_ms timeout)
- else
- I))
- * 0.001) |> seconds
- val generous_slice_timeout =
- Time.+ (slice_timeout, atp_timeout_slack)
- val _ =
- if debug then
- quote name ^ " slice #" ^ string_of_int (slice + 1) ^
- " with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^
- string_from_time slice_timeout ^ "..."
- |> Output.urgent_message
- else
- ()
- val readable_names = not (Config.get ctxt atp_full_names)
- val lam_trans =
- case lam_trans of
- SOME s => s
- | NONE => best_lam_trans
- val uncurried_aliases =
- case uncurried_aliases of
- SOME b => b
- | NONE => best_uncurried_aliases
- val value as (atp_problem, _, fact_names, _, _) =
- if cache_key = SOME key then
- cache_value
- else
- facts
- |> map untranslated_fact
- |> not sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
- |> take num_facts
- |> not (is_type_enc_polymorphic type_enc)
- ? monomorphize_facts
- |> map (apsnd prop_of)
- |> prepare_atp_problem ctxt format prem_role type_enc
- atp_mode lam_trans uncurried_aliases
- readable_names true hyp_ts concl_t
- fun sel_weights () = atp_problem_selection_weights atp_problem
- fun ord_info () = atp_problem_term_order_info atp_problem
- val ord = effective_term_order ctxt name
- val full_proof = debug orelse isar_proof
- val args = arguments ctxt full_proof extra slice_timeout
- (ord, ord_info, sel_weights)
- val command =
- File.shell_path command ^ " " ^ args ^ " " ^
- File.shell_path prob_file
- |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
- val _ =
- atp_problem
- |> lines_for_atp_problem format ord ord_info
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
- val ((output, run_time), (atp_proof, outcome)) =
- TimeLimit.timeLimit generous_slice_timeout
- Isabelle_System.bash_output command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
- |> fst |> split_time
- |> (fn accum as (output, _) =>
- (accum,
- extract_tstplike_proof_and_outcome verbose complete
- proof_delims known_failures output
- |>> atp_proof_from_tstplike_proof atp_problem
- handle UNRECOGNIZED_ATP_PROOF () =>
- ([], SOME ProofIncomplete)))
- handle TimeLimit.TimeOut =>
- (("", slice_timeout), ([], SOME TimedOut))
- val outcome =
- case outcome of
- NONE =>
- (case used_facts_in_unsound_atp_proof ctxt fact_names
- atp_proof
- |> Option.map (sort string_ord) of
- SOME facts =>
- let
- val failure =
- UnsoundProof (is_type_enc_sound type_enc, facts)
- in
- if debug then
- (warning (string_for_failure failure); NONE)
- else
- SOME failure
- end
- | NONE => NONE)
- | _ => outcome
- in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
- val timer = Timer.startRealTimer ()
- fun maybe_run_slice slice
- (result as (cache, (_, run_time0, _, SOME _))) =
- let
- val time_left = Time.- (timeout, Timer.checkRealTimer timer)
- in
- if Time.<= (time_left, Time.zeroTime) then
- result
- else
- run_slice time_left cache slice
- |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
- (cache, (output, Time.+ (run_time0, run_time),
- atp_proof, outcome)))
- end
- | maybe_run_slice _ result = result
- in
- ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
- ("", Time.zeroTime, [], SOME InternalError))
- |> fold maybe_run_slice actual_slices
- end
- else
- error ("Bad executable: " ^ Path.print command)
+ val num_facts =
+ length facts |> is_none max_facts ? Integer.min best_max_facts
+ val soundness = if strict then Strict else Non_Strict
+ val type_enc =
+ type_enc |> choose_type_enc soundness best_type_enc format
+ val sound = is_type_enc_sound type_enc
+ val real_ms = Real.fromInt o Time.toMilliseconds
+ val slice_timeout =
+ ((real_ms time_left
+ |> (if slice < num_actual_slices - 1 then
+ curry Real.min (time_frac * real_ms timeout)
+ else
+ I))
+ * 0.001) |> seconds
+ val generous_slice_timeout =
+ Time.+ (slice_timeout, atp_timeout_slack)
+ val _ =
+ if debug then
+ quote name ^ " slice #" ^ string_of_int (slice + 1) ^
+ " with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for " ^
+ string_from_time slice_timeout ^ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val readable_names = not (Config.get ctxt atp_full_names)
+ val lam_trans =
+ case lam_trans of
+ SOME s => s
+ | NONE => best_lam_trans
+ val uncurried_aliases =
+ case uncurried_aliases of
+ SOME b => b
+ | NONE => best_uncurried_aliases
+ val value as (atp_problem, _, fact_names, _, _) =
+ if cache_key = SOME key then
+ cache_value
+ else
+ facts
+ |> map untranslated_fact
+ |> not sound
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
+ |> take num_facts
+ |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
+ |> map (apsnd prop_of)
+ |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
+ lam_trans uncurried_aliases
+ readable_names true hyp_ts concl_t
+ fun sel_weights () = atp_problem_selection_weights atp_problem
+ fun ord_info () = atp_problem_term_order_info atp_problem
+ val ord = effective_term_order ctxt name
+ val full_proof = debug orelse isar_proof
+ val args = arguments ctxt full_proof extra slice_timeout
+ (ord, ord_info, sel_weights)
+ val command =
+ File.shell_path command0 ^ " " ^ args ^ " " ^
+ File.shell_path prob_file
+ |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+ val _ =
+ atp_problem
+ |> lines_for_atp_problem format ord ord_info
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
+ val ((output, run_time), (atp_proof, outcome)) =
+ TimeLimit.timeLimit generous_slice_timeout
+ Isabelle_System.bash_output command
+ |>> (if overlord then
+ prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
+ else
+ I)
+ |> fst |> split_time
+ |> (fn accum as (output, _) =>
+ (accum,
+ extract_tstplike_proof_and_outcome verbose complete
+ proof_delims known_failures output
+ |>> atp_proof_from_tstplike_proof atp_problem
+ handle UNRECOGNIZED_ATP_PROOF () =>
+ ([], SOME ProofIncomplete)))
+ handle TimeLimit.TimeOut =>
+ (("", slice_timeout), ([], SOME TimedOut))
+ val outcome =
+ case outcome of
+ NONE =>
+ (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
+ |> Option.map (sort string_ord) of
+ SOME facts =>
+ let
+ val failure =
+ UnsoundProof (is_type_enc_sound type_enc, facts)
+ in
+ if debug then (warning (string_for_failure failure); NONE)
+ else SOME failure
+ end
+ | NONE => NONE)
+ | _ => outcome
+ in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
+ val timer = Timer.startRealTimer ()
+ fun maybe_run_slice slice
+ (result as (cache, (_, run_time0, _, SOME _))) =
+ let
+ val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if Time.<= (time_left, Time.zeroTime) then
+ result
+ else
+ run_slice time_left cache slice
+ |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time),
+ atp_proof, outcome)))
+ end
+ | maybe_run_slice _ result = result
+ in
+ ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
+ ("", Time.zeroTime, [], SOME InternalError))
+ |> fold maybe_run_slice actual_slices
+ end
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
fun cleanup prob_file =
if dest_dir = "" then try File.rm prob_file else NONE
fun export prob_file (_, (output, _, _, _)) =
- if dest_dir = "" then
- ()
- else
- File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
+ if dest_dir = "" then ()
+ else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
val ((_, (_, pool, fact_names, _, sym_tab)),
(output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name