# HG changeset patch # User blanchet # Date 1402493363 -7200 # Node ID 6fc0e3d4e1e5ff6702d5cc5608affc9692049313 # Parent c4986877deea27ea34901f497339723986629dd6 moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle diff -r c4986877deea -r 6fc0e3d4e1e5 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Sledgehammer.thy Wed Jun 11 15:29:23 2014 +0200 @@ -14,6 +14,11 @@ lemma size_ne_size_imp_ne: "size x \ size y \ x \ y" by (erule contrapos_nn) (rule arg_cong) +(* Has all needed simplification lemmas for logic. + "HOL.simp_thms(35-42)" are about \ and \. These lemmas are left out for now. *) +lemmas waldmeister_fol = simp_thms(1-34) disj_absorb disj_left_absorb conj_absorb conj_left_absorb + eq_ac disj_comms disj_assoc conj_comms conj_assoc + ML_file "Tools/Sledgehammer/async_manager.ML" ML_file "Tools/Sledgehammer/sledgehammer_util.ML" ML_file "Tools/Sledgehammer/sledgehammer_fact.ML" @@ -27,10 +32,13 @@ ML_file "Tools/Sledgehammer/sledgehammer_prover.ML" ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML" ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML" +ML_file "Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML" ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML" ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" ML_file "Tools/Sledgehammer/sledgehammer.ML" ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" +hide_fact (open) waldmeister_fol + end diff -r c4986877deea -r 6fc0e3d4e1e5 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jun 11 11:28:46 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jun 11 15:29:23 2014 +0200 @@ -59,6 +59,7 @@ val spass_pirateN : string val vampireN : string val waldmeisterN : string + val waldmeister_newN : string val z3_tptpN : string val zipperpositionN : string val remote_prefix : string @@ -112,11 +113,11 @@ val spass_pirateN = "spass_pirate" val vampireN = "vampire" val waldmeisterN = "waldmeister" +val waldmeister_newN = "waldmeister_new" val z3_tptpN = "z3_tptp" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" - val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) val satallax_core_rule = "__satallax_core" (* arbitrary *) val spass_input_rule = "Inp" diff -r c4986877deea -r 6fc0e3d4e1e5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML Wed Jun 11 15:29:23 2014 +0200 @@ -0,0 +1,294 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_waldmeister.ML + Author: Albert Steckermeier, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +General-purpose functions used by the Sledgehammer modules. +*) + +signature SLEDGEHAMMER_PROVER_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 + + 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 +end; + +structure Sledgehammer_Prover_Waldmeister : SLEDGEHAMMER_PROVER_WALDMEISTER = +struct + +open ATP_Problem +open ATP_Problem_Generate +open ATP_Proof +open ATP_Proof_Reconstruct + +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 + +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" + +exception Failure +exception FailureMessage of string + +(* +Some utilitary functions for translation. +*) + +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) + +(* +Translation from Isabelle theorms and terms to ATP terms. +*) + +fun trm_to_atp'' (Const (x,_)) args = [ATerm ((gen_ascii_tuple (String.str const_prefix ^ x),[]),args)] + | trm_to_atp'' (Free (x,_)) args = ATerm ((gen_ascii_tuple (String.str free_prefix ^ x),[]),[])::args + | trm_to_atp'' (Var ((x,_),_)) args = ATerm ((gen_ascii_tuple (String.str var_prefix ^ x),[]),[])::args + | trm_to_atp'' (trm1 $ trm2) args = trm_to_atp'' trm1 (trm_to_atp'' trm2 [] @ args) + | trm_to_atp'' _ args = args + +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]) + | 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 + +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 prepare_conjecture conj_term = + let + 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 + in + (case condition of SOME x => HOLogic.dest_conj x |> map trm_to_atp | NONE => [] + ,trm_to_atp consequence) + end + +(* Translation from ATP terms to Isabelle terms. *) + +fun construct_term (ATerm ((name,_),_)) = + let + val prefix = String.sub (name,0) + in + if prefix = const_prefix then + Const (String.extract (name,1,NONE),Type ("",[])) + else if prefix = free_prefix then + Free (String.extract (name,1,NONE),TFree ("",[])) + else if Char.isUpper prefix then + Var ((name,0),TVar (("",0),[])) + else + raise Failure + end + | construct_term _ = raise Failure + +fun atp_to_trm' (ATerm (descr,args)) = + (case args of + [] => construct_term (ATerm (descr,args)) + | _ => 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])) = + 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 + +fun formula_to_trm (AAtom aterm) = atp_to_trm aterm + | formula_to_trm (AConn (ANot,[aterm])) = + 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 + +fun mk_formula prefix_name name atype aterm = + 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 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,[]) + 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 + +end;