src/HOL/Tools/ATP_Manager/atp_wrapper.ML
author blanchet
Thu Apr 15 13:49:46 2010 +0200 (2010-04-15)
changeset 36167 c1a35be8e476
parent 36143 6490319b1703
child 36169 27b1cc58715e
permissions -rw-r--r--
make Sledgehammer's output more debugging friendly
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_wrapper.ML
     2     Author:     Fabian Immler, TU Muenchen
     3 
     4 Wrapper functions for external ATPs.
     5 *)
     6 
     7 signature ATP_WRAPPER =
     8 sig
     9   type prover = ATP_Manager.prover
    10 
    11   (* hooks for problem files *)
    12   val destdir : string Config.T
    13   val problem_prefix : string Config.T
    14   val measure_runtime : bool Config.T
    15 
    16   val refresh_systems_on_tptp : unit -> unit
    17   val setup : theory -> theory
    18 end;
    19 
    20 structure ATP_Wrapper : ATP_WRAPPER =
    21 struct
    22 
    23 open Sledgehammer_Fact_Preprocessor
    24 open Sledgehammer_HOL_Clause
    25 open Sledgehammer_Fact_Filter
    26 open Sledgehammer_Proof_Reconstruct
    27 open ATP_Manager
    28 
    29 (** generic ATP wrapper **)
    30 
    31 (* external problem files *)
    32 
    33 val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K "");
    34   (*Empty string means create files in Isabelle's temporary files directory.*)
    35 
    36 val (problem_prefix, problem_prefix_setup) =
    37   Attrib.config_string "atp_problem_prefix" (K "prob");
    38 
    39 val (measure_runtime, measure_runtime_setup) =
    40   Attrib.config_bool "atp_measure_runtime" (K false);
    41 
    42 
    43 (* prover configuration *)
    44 
    45 type prover_config =
    46  {command: Path.T,
    47   arguments: Time.time -> string,
    48   failure_strs: string list,
    49   max_new_clauses: int,
    50   prefers_theory_const: bool,
    51   supports_isar_proofs: bool};
    52 
    53 
    54 (* basic template *)
    55 
    56 fun with_path cleanup after f path =
    57   Exn.capture f path
    58   |> tap (fn _ => cleanup path)
    59   |> Exn.release
    60   |> tap (after path);
    61 
    62 fun find_failure strs proof =
    63   case filter (fn s => String.isSubstring s proof) strs of
    64     [] => if is_proof_well_formed proof then NONE
    65           else SOME "Ill-formed ATP output"
    66   | (failure :: _) => SOME failure
    67 
    68 fun generic_prover overlord get_facts prepare write cmd args failure_strs
    69         produce_answer name ({full_types, ...} : params)
    70         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    71          : problem) =
    72   let
    73     (* get clauses and prepare them for writing *)
    74     val (ctxt, (chain_ths, th)) = goal;
    75     val thy = ProofContext.theory_of ctxt;
    76     val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
    77     val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
    78     val the_filtered_clauses =
    79       (case filtered_clauses of
    80         NONE => get_facts relevance_override goal goal_cls
    81       | SOME fcls => fcls);
    82     val the_axiom_clauses =
    83       (case axiom_clauses of
    84         NONE => the_filtered_clauses
    85       | SOME axcls => axcls);
    86     val (internal_thm_names, clauses) =
    87       prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
    88 
    89     (* path to unique problem file *)
    90     val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
    91                    else Config.get ctxt destdir;
    92     val problem_prefix' = Config.get ctxt problem_prefix;
    93     fun prob_pathname nr =
    94       let
    95         val probfile =
    96           Path.basic (problem_prefix' ^
    97                       (if overlord then "_" ^ name else serial_string ())
    98                       ^ "_" ^ string_of_int nr)
    99       in
   100         if destdir' = "" then File.tmp_path probfile
   101         else if File.exists (Path.explode destdir')
   102         then Path.append  (Path.explode destdir') probfile
   103         else error ("No such directory: " ^ destdir')
   104       end;
   105 
   106     (* write out problem file and call prover *)
   107     fun cmd_line probfile =
   108       if Config.get ctxt measure_runtime
   109       then (* Warning: suppresses error messages of ATPs *)
   110         "TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd,
   111         args, File.shell_path probfile] ^ " 2> /dev/null" ^ " ; } 2>&1"
   112       else
   113         space_implode " " ["exec", File.shell_path cmd, args,
   114         File.shell_path probfile];
   115     fun split_time s =
   116       let
   117         val split = String.tokens (fn c => str c = "\n");
   118         val (proof, t) = s |> split |> split_last |> apfst cat_lines;
   119         fun as_num f = f >> (fst o read_int);
   120         val num = as_num (Scan.many1 Symbol.is_ascii_digit);
   121         val digit = Scan.one Symbol.is_ascii_digit;
   122         val num3 = as_num (digit ::: digit ::: (digit >> single));
   123         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
   124         val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
   125       in (proof, as_time t) end;
   126     fun split_time' s =
   127       if Config.get ctxt measure_runtime then split_time s else (s, 0)
   128     fun run_on probfile =
   129       if File.exists cmd then
   130         write full_types probfile clauses
   131         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
   132       else error ("Bad executable: " ^ Path.implode cmd ^ ".");
   133 
   134     (* If the problem file has not been exported, remove it; otherwise, export
   135        the proof file too. *)
   136     fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
   137     fun export probfile (((proof, _), _), _) =
   138       if destdir' = "" then ()
   139       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
   140 
   141     val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
   142       with_path cleanup export run_on (prob_pathname subgoal);
   143 
   144     (* Check for success and print out some information on failure. *)
   145     val failure = find_failure failure_strs proof;
   146     val success = rc = 0 andalso is_none failure;
   147     val (message, relevant_thm_names) =
   148       if is_some failure then ("ATP failed to find a proof.", [])
   149       else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
   150       else
   151         (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
   152                               subgoal));
   153   in
   154     {success = success, message = message,
   155      relevant_thm_names = relevant_thm_names,
   156      atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
   157      internal_thm_names = internal_thm_names,
   158      filtered_clauses = the_filtered_clauses}
   159   end;
   160 
   161 
   162 (* generic TPTP-based provers *)
   163 
   164 fun generic_tptp_prover
   165         (name, {command, arguments, failure_strs, max_new_clauses,
   166                 prefers_theory_const, supports_isar_proofs})
   167         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
   168                     theory_const, higher_order, follow_defs, isar_proof,
   169                     modulus, sorts, ...})
   170         timeout =
   171   generic_prover overlord
   172       (get_relevant_facts respect_no_atp relevance_threshold convergence
   173                           higher_order follow_defs max_new_clauses
   174                           (the_default prefers_theory_const theory_const))
   175       (prepare_clauses higher_order false) write_tptp_file command
   176       (arguments timeout) failure_strs
   177       (if supports_isar_proofs andalso isar_proof then
   178          structured_isar_proof modulus sorts
   179        else
   180          metis_lemma_list false) name params;
   181 
   182 fun tptp_prover name p = (name, generic_tptp_prover (name, p));
   183 
   184 
   185 (** common provers **)
   186 
   187 fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000
   188 
   189 (* Vampire *)
   190 
   191 (* NB: Vampire does not work without explicit time limit. *)
   192 
   193 val vampire_config : prover_config =
   194   {command = Path.explode "$VAMPIRE_HOME/vampire",
   195    arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
   196                               string_of_int (generous_to_secs timeout)),
   197    failure_strs =
   198      ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
   199    max_new_clauses = 60,
   200    prefers_theory_const = false,
   201    supports_isar_proofs = true}
   202 val vampire = tptp_prover "vampire" vampire_config
   203 
   204 
   205 (* E prover *)
   206 
   207 val e_config : prover_config =
   208   {command = Path.explode "$E_HOME/eproof",
   209    arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
   210                               \-tAutoDev --silent --cpu-limit=" ^
   211                               string_of_int (generous_to_secs timeout)),
   212    failure_strs =
   213        ["SZS status: Satisfiable", "SZS status Satisfiable",
   214         "SZS status: ResourceOut", "SZS status ResourceOut",
   215         "# Cannot determine problem status"],
   216    max_new_clauses = 100,
   217    prefers_theory_const = false,
   218    supports_isar_proofs = true}
   219 val e = tptp_prover "e" e_config
   220 
   221 
   222 (* SPASS *)
   223 
   224 fun generic_dfg_prover
   225         (name, ({command, arguments, failure_strs, max_new_clauses,
   226                  prefers_theory_const, ...} : prover_config))
   227         (params as {overlord, respect_no_atp, relevance_threshold, convergence,
   228                     theory_const, higher_order, follow_defs, ...})
   229         timeout =
   230   generic_prover overlord
   231       (get_relevant_facts respect_no_atp relevance_threshold convergence
   232                           higher_order follow_defs max_new_clauses
   233                           (the_default prefers_theory_const theory_const))
   234       (prepare_clauses higher_order true) write_dfg_file command
   235       (arguments timeout) failure_strs (metis_lemma_list true) name params;
   236 
   237 fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
   238 
   239 val spass_config : prover_config =
   240  {command = Path.explode "$SPASS_HOME/SPASS",
   241   arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
   242     " -FullRed=0 -DocProof -TimeLimit=" ^
   243     string_of_int (generous_to_secs timeout)),
   244   failure_strs =
   245     ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
   246      "SPASS beiseite: Maximal number of loops exceeded."],
   247   max_new_clauses = 40,
   248   prefers_theory_const = true,
   249   supports_isar_proofs = false}
   250 val spass = dfg_prover ("spass", spass_config)
   251 
   252 
   253 (* remote prover invocation via SystemOnTPTP *)
   254 
   255 val systems = Synchronized.var "atp_wrapper_systems" ([]: string list);
   256 
   257 fun get_systems () =
   258   let
   259     val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
   260   in
   261     if rc <> 0 then
   262       error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
   263     else
   264       split_lines answer
   265   end;
   266 
   267 fun refresh_systems_on_tptp () =
   268   Synchronized.change systems (fn _ => get_systems ());
   269 
   270 fun get_system prefix = Synchronized.change_result systems (fn systems =>
   271   (if null systems then get_systems () else systems)
   272   |> `(find_first (String.isPrefix prefix)));
   273 
   274 fun the_system prefix =
   275   (case get_system prefix of
   276     NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
   277   | SOME sys => sys);
   278 
   279 val remote_failure_strs = ["Remote-script could not extract proof"];
   280 
   281 fun remote_prover_config prover_prefix args
   282         ({failure_strs, max_new_clauses, prefers_theory_const, ...}
   283          : prover_config) : prover_config =
   284   {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
   285    arguments = (fn timeout =>
   286      args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^
   287      the_system prover_prefix),
   288    failure_strs = remote_failure_strs @ failure_strs,
   289    max_new_clauses = max_new_clauses,
   290    prefers_theory_const = prefers_theory_const,
   291    supports_isar_proofs = false}
   292 
   293 val remote_vampire =
   294   tptp_prover "remote_vampire"
   295               (remote_prover_config "Vampire---9" "" vampire_config)
   296 
   297 val remote_e =
   298   tptp_prover "remote_e" (remote_prover_config "EP---" "" e_config)
   299 
   300 val remote_spass =
   301   tptp_prover "remote_spass" (remote_prover_config "SPASS---" "-x" spass_config)
   302 
   303 val provers = [spass, vampire, e, remote_vampire, remote_spass, remote_e]
   304 val prover_setup = fold add_prover provers
   305 
   306 val setup =
   307   destdir_setup
   308   #> problem_prefix_setup
   309   #> measure_runtime_setup
   310   #> prover_setup;
   311 
   312 end;