src/HOL/Tools/ATP/atp_systems.ML
changeset 52754 d9d90d29860e
parent 52151 de43876e77bf
child 52995 ab98feb66684
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Jul 28 20:51:15 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Jul 29 15:30:31 2013 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5    type slice_spec = (int * string) * atp_format * string * string * bool
     1.6    type atp_config =
     1.7 -    {exec : string list * string list,
     1.8 +    {exec : unit -> string list * string list,
     1.9       arguments :
    1.10         Proof.context -> bool -> string -> Time.time -> string
    1.11         -> term_order * (unit -> (string * int) list)
    1.12 @@ -96,7 +96,7 @@
    1.13  type slice_spec = (int * string) * atp_format * string * string * bool
    1.14  
    1.15  type atp_config =
    1.16 -  {exec : string list * string list,
    1.17 +  {exec : unit -> string list * string list,
    1.18     arguments :
    1.19       Proof.context -> bool -> string -> Time.time -> string
    1.20       -> term_order * (unit -> (string * int) list)
    1.21 @@ -215,7 +215,7 @@
    1.22    THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
    1.23  
    1.24  val agsyhol_config : atp_config =
    1.25 -  {exec = (["AGSYHOL_HOME"], ["agsyHOL"]),
    1.26 +  {exec = K (["AGSYHOL_HOME"], ["agsyHOL"]),
    1.27     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
    1.28         "--proof --time-out " ^ string_of_int (to_secs 1 timeout) ^ " " ^
    1.29         file_name,
    1.30 @@ -236,7 +236,7 @@
    1.31  val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit)
    1.32  
    1.33  val alt_ergo_config : atp_config =
    1.34 -  {exec = (["WHY3_HOME"], ["why3"]),
    1.35 +  {exec = K (["WHY3_HOME"], ["why3"]),
    1.36     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
    1.37         "--format tptp --prover 'Alt-Ergo,0.95,' --timelimit " ^
    1.38         string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    1.39 @@ -259,6 +259,7 @@
    1.40  
    1.41  fun is_e_at_least_1_3 () = string_ord (getenv "E_VERSION", "1.3") <> LESS
    1.42  fun is_e_at_least_1_6 () = string_ord (getenv "E_VERSION", "1.6") <> LESS
    1.43 +fun is_e_at_least_1_8 () = string_ord (getenv "E_VERSION", "1.8") <> LESS
    1.44  
    1.45  val e_smartN = "smart"
    1.46  val e_autoN = "auto"
    1.47 @@ -330,12 +331,6 @@
    1.48         else "")
    1.49      end
    1.50  
    1.51 -fun e_shell_level_argument full_proof =
    1.52 -  if is_e_at_least_1_6 () then
    1.53 -    " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
    1.54 -  else
    1.55 -    ""
    1.56 -
    1.57  fun effective_e_selection_heuristic ctxt =
    1.58    if is_e_at_least_1_3 () then Config.get ctxt e_selection_heuristic
    1.59    else e_autoN
    1.60 @@ -343,16 +338,25 @@
    1.61  fun e_kbo () = if is_e_at_least_1_3 () then "KBO6" else "KBO"
    1.62  
    1.63  val e_config : atp_config =
    1.64 -  {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
    1.65 +  {exec = (fn () => (["E_HOME"],
    1.66 +       if is_e_at_least_1_8 () then ["eprover"] else ["eproof_ram", "eproof"])),
    1.67     arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
    1.68         fn file_name =>
    1.69         fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
    1.70 -       "--tstp-in --tstp-out --output-level=5 --silent " ^
    1.71 +       "--tstp-in --tstp-out --silent " ^
    1.72         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
    1.73         e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
    1.74         "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
    1.75         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
    1.76 -       e_shell_level_argument full_proof ^ " " ^ file_name,
    1.77 +       (if is_e_at_least_1_8 () then
    1.78 +          " --proof-object=1"
    1.79 +        else
    1.80 +          " --output-level=5" ^
    1.81 +          (if is_e_at_least_1_6 () then
    1.82 +             " --pcl-shell-level=" ^ (if full_proof then "0" else "2")
    1.83 +           else
    1.84 +             "")) ^
    1.85 +       " " ^ file_name,
    1.86     proof_delims =
    1.87       [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
    1.88       tstp_proof_delims,
    1.89 @@ -383,7 +387,7 @@
    1.90  (* E-MaLeS *)
    1.91  
    1.92  val e_males_config : atp_config =
    1.93 -  {exec = (["E_MALES_HOME"], ["emales.py"]),
    1.94 +  {exec = K (["E_MALES_HOME"], ["emales.py"]),
    1.95     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
    1.96         "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
    1.97     proof_delims = tstp_proof_delims,
    1.98 @@ -404,7 +408,7 @@
    1.99  (* E-Par *)
   1.100  
   1.101  val e_par_config : atp_config =
   1.102 -  {exec = (["E_HOME"], ["runepar.pl"]),
   1.103 +  {exec = K (["E_HOME"], ["runepar.pl"]),
   1.104     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   1.105         string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
   1.106         " 2" (* proofs *),
   1.107 @@ -421,7 +425,7 @@
   1.108  (* iProver *)
   1.109  
   1.110  val iprover_config : atp_config =
   1.111 -  {exec = (["IPROVER_HOME"], ["iprover"]),
   1.112 +  {exec = K (["IPROVER_HOME"], ["iprover"]),
   1.113     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   1.114         "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
   1.115         string_of_real (Time.toReal timeout) ^ " " ^ file_name,
   1.116 @@ -442,7 +446,7 @@
   1.117  (* iProver-Eq *)
   1.118  
   1.119  val iprover_eq_config : atp_config =
   1.120 -  {exec = (["IPROVER_EQ_HOME"], ["iprover-eq"]),
   1.121 +  {exec = K (["IPROVER_EQ_HOME"], ["iprover-eq"]),
   1.122     arguments = #arguments iprover_config,
   1.123     proof_delims = #proof_delims iprover_config,
   1.124     known_failures = #known_failures iprover_config,
   1.125 @@ -462,7 +466,7 @@
   1.126    THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
   1.127  
   1.128  val leo2_config : atp_config =
   1.129 -  {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
   1.130 +  {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
   1.131     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   1.132         "--foatp e --atp e=\"$E_HOME\"/eprover \
   1.133         \--atp epclextract=\"$E_HOME\"/epclextract \
   1.134 @@ -490,7 +494,7 @@
   1.135    THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_With_Defs)
   1.136  
   1.137  val satallax_config : atp_config =
   1.138 -  {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
   1.139 +  {exec = K (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
   1.140     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   1.141         "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   1.142     proof_delims =
   1.143 @@ -520,7 +524,7 @@
   1.144  
   1.145  (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
   1.146  val spass_config : atp_config =
   1.147 -  {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
   1.148 +  {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
   1.149     arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
   1.150         fn file_name => fn _ =>
   1.151         "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
   1.152 @@ -567,7 +571,7 @@
   1.153  val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit)
   1.154  
   1.155  val vampire_config : atp_config =
   1.156 -  {exec = (["VAMPIRE_HOME"], ["vampire"]),
   1.157 +  {exec = K (["VAMPIRE_HOME"], ["vampire"]),
   1.158     arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
   1.159         fn _ =>
   1.160         "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
   1.161 @@ -619,7 +623,7 @@
   1.162  val z3_tff0 = TFF (Monomorphic, TPTP_Implicit)
   1.163  
   1.164  val z3_tptp_config : atp_config =
   1.165 -  {exec = (["Z3_HOME"], ["z3"]),
   1.166 +  {exec = K (["Z3_HOME"], ["z3"]),
   1.167     arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
   1.168         "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
   1.169         string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
   1.170 @@ -641,7 +645,7 @@
   1.171  (* Not really a prover: Experimental Polymorphic THF and DFG output *)
   1.172  
   1.173  fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
   1.174 -  {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   1.175 +  {exec = K (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
   1.176     arguments = K (K (K (K (K (K ""))))),
   1.177     proof_delims = [],
   1.178     known_failures = known_szs_status_failures,
   1.179 @@ -710,7 +714,7 @@
   1.180  
   1.181  fun remote_config system_name system_versions proof_delims known_failures
   1.182                    prem_role best_slice : atp_config =
   1.183 -  {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   1.184 +  {exec = K (["ISABELLE_ATP"], ["scripts/remote_atp"]),
   1.185     arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
   1.186         fn _ =>
   1.187         (if command <> "" then "-c " ^ quote command ^ " " else "") ^
   1.188 @@ -796,7 +800,7 @@
   1.189  
   1.190  fun is_atp_installed thy name =
   1.191    let val {exec, ...} = get_atp thy name () in
   1.192 -    exists (fn var => getenv var <> "") (fst exec)
   1.193 +    exists (fn var => getenv var <> "") (fst (exec ()))
   1.194    end
   1.195  
   1.196  fun refresh_systems_on_tptp () =