--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Thu Mar 04 22:46:44 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Mar 05 08:22:34 2021 +0100
@@ -14,7 +14,7 @@
type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
- {exec : bool -> string list * string list,
+ {exec : string list * string list,
arguments : Proof.context -> bool -> string -> Time.time -> string ->
term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
@@ -73,7 +73,7 @@
type slice_spec = (int * string) * atp_format * string * string * bool
type atp_config =
- {exec : bool -> string list * string list,
+ {exec : string list * string list,
arguments : Proof.context -> bool -> string -> Time.time -> string ->
term_order * (unit -> (string * int) list) * (unit -> (string * real) list) -> string,
proof_delims : (string * string) list,
@@ -165,7 +165,7 @@
(* agsyHOL *)
val agsyhol_config : atp_config =
- {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
+ {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
proof_delims = tstp_proof_delims,
@@ -183,7 +183,7 @@
(* Alt-Ergo *)
val alt_ergo_config : atp_config =
- {exec = K (["WHY3_HOME"], ["why3"]),
+ {exec = (["WHY3_HOME"], ["why3"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--format tptp --prover 'Alt-Ergo,0.95.2,' --timelimit " ^ string_of_int (to_secs 1 timeout) ^
" " ^ file_name,
@@ -272,7 +272,7 @@
end
val e_config : atp_config =
- {exec = fn _ => (["E_HOME"], ["eprover"]),
+ {exec = (["E_HOME"], ["eprover"]),
arguments = fn ctxt => fn _ => fn heuristic => fn timeout => fn file_name =>
fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
"--auto-schedule --tstp-in --tstp-out --silent " ^
@@ -320,7 +320,7 @@
(* iProver *)
val iprover_config : atp_config =
- {exec = K (["IPROVER_HOME"], ["iproveropt", "iprover"]),
+ {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
"--clausifier \"$E_HOME\"/eprover " ^
"--clausifier_options \"--tstp-format --silent --cnf\" " ^
@@ -342,7 +342,7 @@
(* LEO-II *)
val leo2_config : atp_config =
- {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
+ {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
"--foatp e --atp e=\"$E_HOME\"/eprover \
\--atp epclextract=\"$E_HOME\"/epclextract \
@@ -368,7 +368,7 @@
(* Include choice? Disabled now since it's disabled for Satallax as well. *)
val leo3_config : atp_config =
- {exec = K (["LEO3_HOME"], ["leo3"]),
+ {exec = (["LEO3_HOME"], ["leo3"]),
arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
\-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
@@ -389,7 +389,7 @@
(* Choice is disabled until there is proper reconstruction for it. *)
val satallax_config : atp_config =
- {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
+ {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
(case getenv "E_HOME" of
"" => ""
@@ -418,34 +418,38 @@
val spass_H2SOS = "-Heuristic=2 -SOS"
val spass_config : atp_config =
- {exec = K (["SPASS_HOME"], ["SPASS"]),
- arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ =>
- "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
- "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
- |> extra_options <> "" ? prefix (extra_options ^ " "),
- proof_delims = [("Here is a proof", "Formulae used in the proof")],
- known_failures =
- [(GaveUp, "SPASS beiseite: Completion found"),
- (TimedOut, "SPASS beiseite: Ran out of time"),
- (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
- (MalformedInput, "Undefined symbol"),
- (MalformedInput, "Free Variable"),
- (Unprovable, "No formulae and clauses found in input file"),
- (InternalError, "Please report this error")] @
- known_perl_failures,
- prem_role = Conjecture,
- best_slices = fn _ =>
- (* FUDGE *)
- [(0.1667, (((150, meshN), DFG Monomorphic, "mono_native", combsN, true), "")),
- (0.1667, (((500, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
- (0.1666, (((50, meshN), DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0)),
- (0.1000, (((250, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0)),
- (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
- (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
- (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
- (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
+ let
+ val format = DFG Monomorphic
+ in
+ {exec = (["SPASS_HOME"], ["SPASS"]),
+ arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ =>
+ "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -Splits=0 " else "") ^
+ "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
+ |> extra_options <> "" ? prefix (extra_options ^ " "),
+ proof_delims = [("Here is a proof", "Formulae used in the proof")],
+ known_failures =
+ [(GaveUp, "SPASS beiseite: Completion found"),
+ (TimedOut, "SPASS beiseite: Ran out of time"),
+ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
+ (MalformedInput, "Undefined symbol"),
+ (MalformedInput, "Free Variable"),
+ (Unprovable, "No formulae and clauses found in input file"),
+ (InternalError, "Please report this error")] @
+ known_perl_failures,
+ prem_role = Conjecture,
+ best_slices = fn _ =>
+ (* FUDGE *)
+ [(0.1667, (((150, meshN), format, "mono_native", combsN, true), "")),
+ (0.1667, (((500, meshN), format, "mono_native", liftingN, true), spass_H2SOS)),
+ (0.1666, (((50, meshN), format, "mono_native", liftingN, true), spass_H2LR0LT0)),
+ (0.1000, (((250, meshN), format, "mono_native", combsN, true), spass_H2NuVS0)),
+ (0.1000, (((1000, mepoN), format, "mono_native", liftingN, true), spass_H1SOS)),
+ (0.1000, (((150, meshN), format, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
+ (0.1000, (((300, meshN), format, "mono_native", combsN, true), spass_H2SOS)),
+ (0.1000, (((100, meshN), format, "mono_native", combs_and_liftingN, true), spass_H2))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+ end
val spass = (spassN, fn () => spass_config)
@@ -486,32 +490,36 @@
"vampire " ^ vampire_basic_options ^ " " ^ vampire_full_proof_options ^ " -t %d %s"
val vampire_config : atp_config =
- {exec = K (["VAMPIRE_HOME"], ["vampire"]),
- arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ =>
- (check_vampire_noncommercial ();
- vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
- " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name
- |> sos = sosN ? prefix "--sos on "),
- proof_delims =
- [("=========== Refutation ==========",
- "======= End of refutation =======")] @
- tstp_proof_delims,
- known_failures =
- [(GaveUp, "UNPROVABLE"),
- (GaveUp, "CANNOT PROVE"),
- (Unprovable, "Satisfiability detected"),
- (Unprovable, "Termination reason: Satisfiable"),
- (Interrupted, "Aborted by signal SIGINT")] @
- known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices = fn ctxt =>
- (* FUDGE *)
- [(0.333, (((500, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), sosN)),
- (0.333, (((150, meshN), TFF (Without_FOOL, Monomorphic), "poly_tags??", combs_or_liftingN, false), sosN)),
- (0.334, (((50, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combs_or_liftingN, false), no_sosN))]
- |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+ let
+ val format = TFF (Without_FOOL, Monomorphic)
+ in
+ {exec = (["VAMPIRE_HOME"], ["vampire"]),
+ arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn file_name => fn _ =>
+ (check_vampire_noncommercial ();
+ vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+ " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ file_name
+ |> sos = sosN ? prefix "--sos on "),
+ proof_delims =
+ [("=========== Refutation ==========",
+ "======= End of refutation =======")] @
+ tstp_proof_delims,
+ known_failures =
+ [(GaveUp, "UNPROVABLE"),
+ (GaveUp, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
+ (Unprovable, "Termination reason: Satisfiable"),
+ (Interrupted, "Aborted by signal SIGINT")] @
+ known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.333, (((500, meshN), format, "mono_native", combs_or_liftingN, false), sosN)),
+ (0.333, (((150, meshN), format, "poly_tags??", combs_or_liftingN, false), sosN)),
+ (0.334, (((50, meshN), format, "mono_native", combs_or_liftingN, false), no_sosN))]
+ |> Config.get ctxt force_sos ? (hd #> apfst (K 1.0) #> single),
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+ end
val vampire = (vampireN, fn () => vampire_config)
@@ -519,20 +527,24 @@
(* Z3 with TPTP syntax (half experimental, half legacy) *)
val z3_tptp_config : atp_config =
- {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
- arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
- proof_delims = [("SZS status Theorem", "")],
- known_failures = known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices =
- (* FUDGE *)
- K [(0.5, (((250, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
- (0.25, (((125, mepoN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
- (0.125, (((62, mashN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), "")),
- (0.125, (((31, meshN), TFF (Without_FOOL, Monomorphic), "mono_native", combsN, false), ""))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+ let
+ val format = TFF (Without_FOOL, Monomorphic)
+ in
+ {exec = (["Z3_TPTP_HOME"], ["z3_tptp"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+ proof_delims = [("SZS status Theorem", "")],
+ known_failures = known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices =
+ (* FUDGE *)
+ K [(0.5, (((250, meshN), format, "mono_native", combsN, false), "")),
+ (0.25, (((125, mepoN), format, "mono_native", combsN, false), "")),
+ (0.125, (((62, mashN), format, "mono_native", combsN, false), "")),
+ (0.125, (((31, meshN), format, "mono_native", combsN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}
+ end
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
@@ -544,20 +556,24 @@
val zipperposition_cdots = "--mode ho-competitive --boolean-reasoning cases-simpl --ext-rules ext-family --ext-rules-max-depth 1 --ho-prim-enum pragmatic --ho-prim-max 1 --bool-subterm-selection A --avatar off --recognize-injectivity true --ho-elim-leibniz 1 --ho-unif-level full-framework --no-max-vars -q '6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)' -q '6|const|conjecture-relative-var(1.02,l,f)' -q '1|prefer-processed|fifo' -q '1|prefer-non-goals|conjecture-relative-var(1,l,f)' -q '4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)' --select e-selection7 --ho-choice-inst true --sine 50 --sine-tolerance 2 --sine-depth-max 4 --sine-depth-min 1 --scan-clause-ac true --lambdasup 0 --kbo-weight-fun invfreqrank"
val zipperposition_config : atp_config =
- {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
- arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
- "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
- |> extra_options <> "" ? prefix (extra_options ^ " "),
- proof_delims = tstp_proof_delims,
- known_failures = known_szs_status_failures,
- prem_role = Hypothesis,
- best_slices = fn _ =>
- (* FUDGE *)
- [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
- (0.333, (((32, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
- (0.334, (((512, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
- best_max_mono_iters = default_max_mono_iters,
- best_max_new_mono_instances = default_max_new_mono_instances}
+ let
+ val format = THF (Without_FOOL, Polymorphic, THF_Without_Choice)
+ in
+ {exec = (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
+ arguments = fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
+ "--input tptp --output tptp --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
+ |> extra_options <> "" ? prefix (extra_options ^ " "),
+ proof_delims = tstp_proof_delims,
+ known_failures = known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices = fn _ =>
+ (* FUDGE *)
+ [(0.333, (((128, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),
+ (0.333, (((32, "meshN"), format, "poly_native_higher", keep_lamsN, false), zipperposition_s6)),
+ (0.334, (((512, "meshN"), format, "mono_native_higher", keep_lamsN, false), zipperposition_cdots))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+ end
val zipperposition = (zipperpositionN, fn () => zipperposition_config)
@@ -604,7 +620,7 @@
val max_remote_secs = 1000 (* give Geoff Sutcliffe's servers a break *)
fun remote_config system_name system_versions proof_delims known_failures prem_role best_slice =
- {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
+ {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
arguments = fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
(if command <> "" then "-c " ^ quote command ^ " " else "") ^
"-s " ^ the_remote_system system_name system_versions ^ " " ^
@@ -666,7 +682,7 @@
(* Dummy prover *)
fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
- {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
+ {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
arguments = K (K (K (K (K (K ""))))),
proof_delims = [],
known_failures = known_szs_status_failures,
@@ -698,7 +714,7 @@
fun is_atp_installed thy name =
let val {exec, ...} = get_atp thy name () in
- exists (fn var => getenv var <> "") (fst (exec false))
+ exists (fn var => getenv var <> "") (fst exec)
end
fun refresh_systems_on_tptp () =