# HG changeset patch # User blanchet # Date 1402940564 -7200 # Node ID 8b87114357bdf0f2ee292913a7bfa4333713389c # Parent 6a3b5085fb8fd39265eeddab94719facdb1ea227 integrated new Waldmeister code with 'sledgehammer' command diff -r 6a3b5085fb8f -r 8b87114357bd src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 19:41:42 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 19:42:44 2014 +0200 @@ -155,7 +155,6 @@ open ATP_Util - val parens = enclose "(" ")" (** ATP problem **) @@ -385,8 +384,7 @@ val dfg_individual_type = "iii" (* cannot clash *) -val suffix_type_of_types = - suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types) +val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types) fun str_of_type format ty = let @@ -439,9 +437,7 @@ let val of_type = string_of_type format val of_term = tptp_string_of_term format - fun app () = - tptp_string_of_app format s - (map of_type tys @ map of_term ts) + fun app () = tptp_string_of_app format s (map of_type tys @ map of_term ts) in if s = tptp_empty_list then (* used for lists in the optional "source" field of a derivation *) diff -r 6a3b5085fb8f -r 8b87114357bd src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:41:42 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 19:42:44 2014 +0200 @@ -49,6 +49,8 @@ val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list + val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list + val infer_formula_types : Proof.context -> term -> term val introduce_spass_skolem : (term, string) atp_step list -> (term, string) atp_step list val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> (term, string) atp_step list @@ -605,8 +607,7 @@ end fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab = - clean_up_atp_proof_dependencies - #> nasty_atp_proof pool + nasty_atp_proof pool #> map_term_names_in_atp_proof repair_name #> map_filter (termify_line ctxt format type_enc lifted sym_tab) #> local_prover = waldmeisterN ? repair_waldmeister_endgame diff -r 6a3b5085fb8f -r 8b87114357bd src/HOL/Tools/ATP/atp_waldmeister.ML --- a/src/HOL/Tools/ATP/atp_waldmeister.ML Mon Jun 16 19:41:42 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML Mon Jun 16 19:42:44 2014 +0200 @@ -7,48 +7,22 @@ signature ATP_WALDMEISTER = sig - type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term - type atp_connective = ATP_Problem.atp_connective - type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula - type atp_format = ATP_Problem.atp_format - type atp_formula_role = ATP_Problem.atp_formula_role type 'a atp_problem = 'a ATP_Problem.atp_problem - type ('a, 'b) atp_step = ('a,'b) ATP_Proof.atp_step - - val const_prefix : char - val var_prefix : char - val free_prefix : char - val thm_prefix : string - val hypothesis_prefix : string - val thms_header : string - val conjecture_condition_name : string - val hypothesis_header : string - val waldmeister_output_file_path : string + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + type 'a atp_proof = 'a ATP_Proof.atp_proof + type stature = ATP_Problem_Generate.stature - val waldmeister_simp_header : string - val waldmeister_simp_thms : thm list - - val thm_to_atps : bool -> thm -> (string * string, 'a) atp_term list - val trm_to_atp : term -> (string * string, 'a) atp_term - val atp_to_trm : (string, 'a) atp_term -> term - val trm_to_atp_to_trm : term -> term - val create_tptp_input : thm list -> term -> - (string * ((string * string ATP_Problem.atp_problem_line list) list - * (string Symtab.table * string Symtab.table) option)) option - val run_waldmeister : - string * (string ATP_Proof.atp_problem * (string Symtab.table * string Symtab.table) option) - -> string ATP_Proof.atp_proof - val atp_proof_step_to_term : - ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step - -> (term,string) atp_step - val fix_waldmeister_proof : - ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list -> - ((string, string, (string, string) atp_term, string) atp_formula,string) atp_step list + val generate_waldmeister_problem: Proof.context -> term list -> term -> + ((string * stature) * term) list -> + string atp_problem * string Symtab.table * (string * term) list * int Symtab.table + val termify_waldmeister_proof : Proof.context -> string Symtab.table -> string atp_proof -> + (term, string) atp_step list end; structure ATP_Waldmeister : ATP_WALDMEISTER = struct +open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof @@ -64,22 +38,11 @@ val const_prefix = #"c" val var_prefix = #"V" val free_prefix = #"f" -val thm_prefix = "fact" -val hypothesis_prefix = "hypothesis" -val thms_header = "facts" val conjecture_condition_name = "condition" -val hypothesis_header = "hypothesis" -val broken_waldmeister_formula_prefix = #"1" -val waldmeister_simp_header = "Waldmeister first order logic facts" -val waldmeister_simp_thms = @{thms waldmeister_fol} - -val temp_files_dir = "/home/albert/waldmeister" -val input_file_name = "input.tptp" -val output_file_name = "output.tptp" -val waldmeister_input_file_path = temp_files_dir ^ "/" ^ input_file_name -val waldmeister_output_file_path = temp_files_dir ^ "/" ^ output_file_name -val script_path = "/opt/Isabelle/src/HOL/Tools/ATP/scripts/remote_atp -s Waldmeister---710 -t 30" +val factsN = "Relevant facts" +val helpersN = "Helper facts" +val conjN = "Conjecture" exception Failure exception FailureMessage of string @@ -91,8 +54,6 @@ fun is_eq (Const (@{const_name "HOL.eq"}, _) $ _ $ _) = true | is_eq _ = false -fun is_eq_thm thm = thm |> Thm.prop_of |> Object_Logic.atomize_term @{theory } |> is_eq - fun gen_ascii_tuple str = (str, ascii_of str) (* @@ -108,28 +69,20 @@ fun trm_to_atp' trm = trm_to_atp'' trm [] |> hd fun eq_trm_to_atp (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = - ATerm (((tptp_equal, tptp_equal), []), [trm_to_atp' lhs, trm_to_atp' rhs]) + ATerm ((("equal", "equal"), []), [trm_to_atp' lhs, trm_to_atp' rhs]) | eq_trm_to_atp _ = raise Failure fun trm_to_atp trm = - if is_eq trm then - eq_trm_to_atp trm - else - HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp + if is_eq trm then eq_trm_to_atp trm + else HOLogic.mk_eq (trm, @{term True}) |> eq_trm_to_atp -fun thm_to_atps split_conj thm = - let - val prop_term = Thm.prop_of thm |> Object_Logic.atomize_term @{theory} - in - if split_conj then - map trm_to_atp (prop_term |> HOLogic.dest_conj) - else - [prop_term |> trm_to_atp] - end +fun thm_to_atps split_conj prop_term = + if split_conj then map trm_to_atp (prop_term |> HOLogic.dest_conj) + else [prop_term |> trm_to_atp] fun prepare_conjecture conj_term = let - fun split_conj_trm (Const (@{const_name Pure.imp}, _)$ condition $ consequence) = + fun split_conj_trm (Const (@{const_name Pure.imp}, _) $ condition $ consequence) = (SOME condition, consequence) | split_conj_trm conj = (NONE, conj) val (condition, consequence) = split_conj_trm conj_term @@ -161,7 +114,7 @@ | _ => Term.list_comb (construct_term (ATerm (descr, args)), map atp_to_trm' args)) | atp_to_trm' _ = raise Failure -fun atp_to_trm (ATerm (("equal", _), [lhs, rhs])) = +fun atp_to_trm (ATerm (("equal", _), [lhs, rhs])) = Const (@{const_name HOL.eq}, Type ("", [])) $ atp_to_trm' lhs $ atp_to_trm' rhs | atp_to_trm (ATerm (("$true", _), _)) = Const ("HOL.True", Type ("", [])) | atp_to_trm _ = raise Failure @@ -171,124 +124,68 @@ Const (@{const_name HOL.Not}, @{typ "bool \ bool"}) $ formula_to_trm aterm | formula_to_trm _ = raise Failure -(* Simple testing function for translation *) - -fun atp_only_readable_names (ATerm ((("=", _), ty), args)) = - ATerm (("equal", ty), map atp_only_readable_names args) - | atp_only_readable_names (ATerm (((descr, _), ty), args)) = - ATerm ((descr, ty), map atp_only_readable_names args) - | atp_only_readable_names _ = raise Failure - -val trm_to_atp_to_trm = eq_trm_to_atp #> atp_only_readable_names #> atp_to_trm - -(* Abstract translation from here on. *) - -fun name_of_thm thm = - Thm.get_tags thm - |> List.find (fn (x, _) => x = "name") - |> the |> snd +(* Abstract translation *) fun mk_formula prefix_name name atype aterm = - Formula ((prefix_name ^ "_" ^ ascii_of name, name), atype, AAtom aterm, NONE, []) + Formula ((prefix_name ^ ascii_of name, name), atype, AAtom aterm, NONE, []) -fun thms_to_problem_lines [] = [] - | thms_to_problem_lines (t::thms) = - (thm_to_atps false t |> - map (mk_formula thm_prefix (name_of_thm t) Axiom)) @ thms_to_problem_lines thms +fun problem_lines_of_fact prefix ((s, _), t) = + map (mk_formula prefix s Axiom) (thm_to_atps false t) fun make_nice problem = nice_atp_problem true CNF problem -fun problem_to_string [] = "" - | problem_to_string ((kind, lines)::problems) = - "% " ^ kind ^ "\n" - ^ String.concat (map (tptp_string_of_line CNF) lines) - ^ "\n" - ^ problem_to_string problems - fun mk_conjecture aterm = let val formula = mk_anot (AAtom aterm) in - Formula (gen_ascii_tuple hypothesis_prefix, Hypothesis, formula, NONE, []) + Formula ((conjecture_prefix ^ "0", ""), Hypothesis, formula, NONE, []) end -fun mk_condition_lines [] = [] - | mk_condition_lines (term::terms) = - mk_formula thm_prefix conjecture_condition_name Axiom term::mk_condition_lines terms - -fun create_tptp_input thms conj_t = - let - val (conditions, consequence) = prepare_conjecture conj_t - val thms_lines = thms_to_problem_lines thms - val condition_lines = mk_condition_lines conditions - val axiom_lines = thms_lines @ condition_lines - val conj_line = consequence |> mk_conjecture - val waldmeister_simp_lines = - if List.exists (fn x => not (is_eq_thm x)) thms orelse not (is_eq conj_t) then - [(waldmeister_simp_header, thms_to_problem_lines waldmeister_simp_thms)] - else - [] - val problem = - waldmeister_simp_lines @ [(thms_header, axiom_lines), (hypothesis_header, [conj_line])] - val (problem_nice, symtabs) = make_nice problem - in - SOME (problem_to_string problem_nice, (problem_nice, symtabs)) - end - -val waldmeister_proof_delims = - [("% SZS output start CNFRefutation", "% SZS output end CNFRefutation")] -val known_waldmeister_failures = [(OutOfResources, "Too many function symbols"), - (Inappropriate, "**** Unexpected end of file."), - (Crashed, "Unrecoverable Segmentation Fault")] - -fun extract_proof_part output = - case - extract_tstplike_proof_and_outcome true - waldmeister_proof_delims known_waldmeister_failures output of - (x, NONE) => x | (_, SOME y) => raise FailureMessage (string_of_atp_failure y) - -fun cleanup () = - (OS.Process.system ("rm " ^ waldmeister_input_file_path); - OS.Process.system ("rm " ^ waldmeister_output_file_path)) - -fun run_script input = - let - val outputFile = TextIO.openOut waldmeister_input_file_path - in - (TextIO.output (outputFile, input); - TextIO.flushOut outputFile; - TextIO.closeOut outputFile; - OS.Process.system (script_path ^ " " ^ waldmeister_input_file_path ^ " > " ^ - waldmeister_output_file_path)) - end - -fun read_result () = - let - val inputFile = TextIO.openIn waldmeister_output_file_path - fun readAllLines is = - if TextIO.endOfStream is then (TextIO.closeIn is; []) - else (TextIO.inputLine is |> the) :: readAllLines is - in - readAllLines inputFile |> String.concat - end - -fun run_waldmeister (input, (problem, SOME (_, nice_to_nasty_table))) = - (cleanup (); - run_script input; - read_result () - |> extract_proof_part - |> atp_proof_of_tstplike_proof waldmeister_newN problem - |> nasty_atp_proof nice_to_nasty_table) - | run_waldmeister _ = raise Failure - fun atp_proof_step_to_term (name, role, formula, formula_name, step_names) = (name, role, formula_to_trm formula, formula_name, step_names) -fun fix_waldmeister_proof [] = [] - | fix_waldmeister_proof (((name, extra_names), role, formula, formula_name, step_names)::steps) = - if String.sub (name, 0) = broken_waldmeister_formula_prefix then - ((name, extra_names), role, mk_anot formula, formula_name, step_names)::fix_waldmeister_proof steps - else - ((name, extra_names), role, formula, formula_name, step_names)::fix_waldmeister_proof steps +fun generate_waldmeister_problem ctxt hyp_ts0 concl_t0 facts0 = + let + val hyp_ts = map HOLogic.dest_Trueprop hyp_ts0 + val concl_t = HOLogic.dest_Trueprop concl_t0 + val facts = map (apsnd HOLogic.dest_Trueprop) facts0 + + val (conditions, consequence) = prepare_conjecture concl_t + val fact_lines = maps (problem_lines_of_fact (fact_prefix ^ "0_" (* FIXME *))) facts + val condition_lines = + map (mk_formula fact_prefix conjecture_condition_name Hypothesis) conditions + val axiom_lines = fact_lines @ condition_lines + val conj_line = mk_conjecture consequence + + val helper_lines = + if List.exists (is_eq o snd) facts orelse not (is_eq concl_t) then + [(helpersN, + @{thms waldmeister_fol} + |> map (fn th => (("", (Global, General)), HOLogic.dest_Trueprop (prop_of th))) + |> maps (problem_lines_of_fact helper_prefix))] + else + [] + val problem = (factsN, axiom_lines) :: helper_lines @ [(conjN, [conj_line])] + + val (nice_problem, symtabs) = make_nice problem + in + (nice_problem, Symtab.empty, [], Symtab.empty) + end + +fun termify_line ctxt (name, role, AAtom u, rule, deps) = + let + val thy = Proof_Context.theory_of ctxt + val t = u + |> atp_to_trm + |> infer_formula_types ctxt + |> HOLogic.mk_Trueprop + in + (name, role, t, rule, deps) + end + +fun termify_waldmeister_proof ctxt pool = + nasty_atp_proof pool + #> map (termify_line ctxt) + #> repair_waldmeister_endgame end; diff -r 6a3b5085fb8f -r 8b87114357bd src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:41:42 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 16 19:42:44 2014 +0200 @@ -29,6 +29,7 @@ open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct +open ATP_Waldmeister open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods @@ -142,6 +143,10 @@ val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters, best_max_new_mono_instances, ...} = get_atp thy name () + val local_name = perhaps (try (unprefix remote_prefix)) name + val waldmeister_new = (local_name = waldmeister_newN) + val spass = (local_name = spassN orelse local_name = spass_pirateN) + val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (dest_dir, problem_prefix) = @@ -261,8 +266,11 @@ |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd prop_of) - |> generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans - uncurried_aliases readable_names true hyp_ts concl_t + |> (if waldmeister_new then + generate_waldmeister_problem ctxt hyp_ts concl_t + else + generate_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