wneuper/isa: comparison src/HOL/Tools/ATP_Manager/atp

equal deleted inserted replaced

-:23908b4dbc2f
+:2f8fb5242799
 (*prover configuration, problem format, and prover result*)
 type prover_config =
 {command: Path.T,
 arguments: int -> string,
+failure_strs: string list,
 max_new_clauses: int,
 insert_theory_const: bool,
 emit_structured_proof: bool}
 type problem =
 {with_full_types: bool,
 val remote_eprover: string * prover
 val remote_spass: string * prover
 val refresh_systems: unit -> unit
 end;
-structure ATP_Wrapper: ATP_WRAPPER =
+structure ATP_Wrapper : ATP_WRAPPER =
 struct
-structure SFF = Sledgehammer_Fact_Filter
+open Sledgehammer_HOL_Clause
-structure SPR = Sledgehammer_Proof_Reconstruct
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
 (** generic ATP wrapper **)
 (* external problem files *)
 (* prover configuration, problem format, and prover result *)
 type prover_config =
 {command: Path.T,
 arguments: int -> string,
+failure_strs: string list,
 max_new_clauses: int,
 insert_theory_const: bool,
 emit_structured_proof: bool};
 type problem =
 Exn.capture f path
 |> tap (fn _ => cleanup path)
 |> Exn.release
 |> tap (after path);
-fun external_prover relevance_filter prepare write cmd args produce_answer name
+fun find_failure strs proof =
-({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
+case filter (fn s => String.isSubstring s proof) strs of
+[] => if is_proof_well_formed proof then NONE
+else SOME "Ill-formed ATP output"
+| (failure :: _) => SOME failure
+fun external_prover relevance_filter prepare write cmd args failure_strs
+produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
+filtered_clauses}: problem) =
 let
 (* get clauses and prepare them for writing *)
 val (ctxt, (chain_ths, th)) = goal;
 val thy = ProofContext.theory_of ctxt;
-val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths;
+val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
 val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
 val the_filtered_clauses =
 (case filtered_clauses of
 NONE => relevance_filter goal goal_cls
 | SOME fcls => fcls);
 val (((proof, time), rc), conj_pos) =
 with_path cleanup export run_on (prob_pathname subgoal);
 (* check for success and print out some information on failure *)
-val failure = SPR.find_failure proof;
+val failure = find_failure failure_strs proof;
 val success = rc = 0 andalso is_none failure;
 val (message, real_thm_names) =
 if is_some failure then ("External prover failed.", [])
 else if rc <> 0 then ("External prover failed: " ^ proof, [])
 else apfst (fn s => "Try this command: " ^ s)
 end;
 (* generic TPTP-based provers *)
-fun gen_tptp_prover (name, prover_config) timeout problem =
+fun generic_tptp_prover
-let
+(name, {command, arguments, failure_strs, max_new_clauses,
-val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
+insert_theory_const, emit_structured_proof}) timeout =
-prover_config;
+external_prover (get_relevant_facts max_new_clauses insert_theory_const)
-in
+(prepare_clauses false) write_tptp_file command (arguments timeout)
-external_prover
+failure_strs
-(SFF.get_relevant max_new_clauses insert_theory_const)
+(if emit_structured_proof then structured_isar_proof
-(SFF.prepare_clauses false)
+else metis_lemma_list false) name;
-Sledgehammer_HOL_Clause.tptp_write_file
-command
+fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
-(arguments timeout)
-(if emit_structured_proof then SPR.structured_proof
-else SPR.lemma_list false)
-name
-problem
-end;
-fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
 (** common provers **)
 (* Vampire *)
 (*NB: Vampire does not work without explicit timelimit*)
+val vampire_failure_strs =
+["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
 val vampire_max_new_clauses = 60;
 val vampire_insert_theory_const = false;
 fun vampire_prover_config full : prover_config =
 {command = Path.explode "$VAMPIRE_HOME/vampire",
 arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
 " -t " ^ string_of_int timeout),
+failure_strs = vampire_failure_strs,
 max_new_clauses = vampire_max_new_clauses,
 insert_theory_const = vampire_insert_theory_const,
 emit_structured_proof = full};
 val vampire = tptp_prover ("vampire", vampire_prover_config false);
 val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true);
 (* E prover *)
+val eprover_failure_strs =
+["SZS status: Satisfiable", "SZS status Satisfiable",
+"SZS status: ResourceOut", "SZS status ResourceOut",
+"# Cannot determine problem status"];
 val eprover_max_new_clauses = 100;
 val eprover_insert_theory_const = false;
 fun eprover_config full : prover_config =
 {command = Path.explode "$E_HOME/eproof",
 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
 " --silent --cpu-limit=" ^ string_of_int timeout),
+failure_strs = eprover_failure_strs,
 max_new_clauses = eprover_max_new_clauses,
 insert_theory_const = eprover_insert_theory_const,
 emit_structured_proof = full};
 val eprover = tptp_prover ("e", eprover_config false);
 val eprover_full = tptp_prover ("e_full", eprover_config true);
 (* SPASS *)
+val spass_failure_strs =
+["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+"SPASS beiseite: Maximal number of loops exceeded."];
 val spass_max_new_clauses = 40;
 val spass_insert_theory_const = true;
 fun spass_config insert_theory_const: prover_config =
 {command = Path.explode "$SPASS_HOME/SPASS",
 arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
 " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
+failure_strs = spass_failure_strs,
 max_new_clauses = spass_max_new_clauses,
 insert_theory_const = insert_theory_const,
 emit_structured_proof = false};
-fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
+fun generic_dfg_prover
-let
+(name, ({command, arguments, failure_strs, max_new_clauses,
-val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
+insert_theory_const, ...} : prover_config)) timeout =
-in
+external_prover
-external_prover
+(get_relevant_facts max_new_clauses insert_theory_const)
-(SFF.get_relevant max_new_clauses insert_theory_const)
+(prepare_clauses true)
-(SFF.prepare_clauses true)
+write_dfg_file
-Sledgehammer_HOL_Clause.dfg_write_file
+command
-command
+(arguments timeout)
-(arguments timeout)
+failure_strs
-(SPR.lemma_list true)
+(metis_lemma_list true)
-name
+name;
-problem
-end;
+fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
-fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
 val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
 val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
 fun the_system prefix =
 (case get_system prefix of
 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP")
 | SOME sys => sys);
+val remote_failure_strs = ["Remote-script could not extract proof"];
 fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
 {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
-arguments =
+arguments = (fn timeout =>
-(fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
+args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
+failure_strs = remote_failure_strs,
 max_new_clauses = max_new,
 insert_theory_const = insert_tc,
 emit_structured_proof = false};
 val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config

changeset 35865	2f8fb5242799
parent 35826	1590abc3d42a
child 35867	16279c4c7a33