# HG changeset patch # User blanchet # Date 1280495022 -7200 # Node ID d44a5f602b8c893bede0c002394c71542b98b74f # Parent 61280b97b7612cea8bd63ed1408978f7fa9176ee# Parent 373351f5f834b97bf12a625665f8be2efb48842e merged diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 30 15:03:42 2010 +0200 @@ -306,11 +306,11 @@ ctxt |> change_dir dir |> Config.put Sledgehammer.measure_runtime true - val params = Sledgehammer_Isar.default_params thy [] + val params = Sledgehammer_Isar.default_params thy + [("timeout", Int.toString timeout ^ " s")] val problem = {subgoal = 1, goal = (ctxt', (facts, goal)), - relevance_override = {add = [], del = [], only = false}, - axiom_clauses = NONE, filtered_clauses = NONE} + relevance_override = {add = [], del = [], only = false}, axioms = NONE} val time_limit = (case hard_timeout of NONE => I @@ -318,7 +318,7 @@ val ({outcome, message, used_thm_names, atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result, time_isa) = time_limit (Mirabelle.cpu_time - (prover params (K "") (Time.fromSeconds timeout))) problem + (prover params (K ""))) problem in case outcome of NONE => (message, SH_OK (time_isa, time_atp, used_thm_names)) @@ -381,7 +381,6 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let open Metis_Clauses - open Sledgehammer_Isar val thy = Proof.theory_of st val n0 = length (these (!named_thms)) val (prover_name, _) = get_atp thy args @@ -389,8 +388,8 @@ AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) |> the_default 5 - val params = default_params thy - [("atps", prover_name), ("minimize_timeout", Int.toString timeout)] + val params = Sledgehammer_Isar.default_params thy + [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")] val minimize = Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st) val _ = log separator diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Jul 30 15:03:42 2010 +0200 @@ -49,9 +49,10 @@ val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm ("equal", ts)) = + space_implode " = " (map string_for_term ts) | string_for_term (ATerm (s, ts)) = - if s = "equal" then space_implode " = " (map string_for_term ts) - else s ^ "(" ^ commas (map string_for_term ts) ^ ")" + s ^ "(" ^ commas (map string_for_term ts) ^ ")" fun string_for_quantifier AForall = "!" | string_for_quantifier AExists = "?" fun string_for_connective ANot = "~" diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 30 15:03:42 2010 +0200 @@ -13,8 +13,8 @@ MalformedOutput | UnknownError type prover_config = - {executable: string * string, - required_executables: (string * string) list, + {exec: string * string, + required_execs: (string * string) list, arguments: bool -> Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, @@ -44,8 +44,8 @@ MalformedOutput | UnknownError type prover_config = - {executable: string * string, - required_executables: (string * string) list, + {exec: string * string, + required_execs: (string * string) list, arguments: bool -> Time.time -> string, proof_delims: (string * string) list, known_failures: (failure * string) list, @@ -60,14 +60,14 @@ fun string_for_failure Unprovable = "The ATP problem is unprovable." | string_for_failure IncompleteUnprovable = "The ATP cannot prove the problem." - | string_for_failure CantConnect = "Can't connect to remote ATP." + | string_for_failure CantConnect = "Can't connect to remote server." | string_for_failure TimedOut = "Timed out." | string_for_failure OutOfResources = "The ATP ran out of resources." | string_for_failure OldSpass = - "Warning: Isabelle requires a more recent version of SPASS with \ - \support for the TPTP syntax. To install it, download and extract the \ - \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \ - \add the \"spass-3.7\" directory's absolute path to " ^ + "Isabelle requires a more recent version of SPASS with support for the \ + \TPTP syntax. To install it, download and extract the package \ + \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \ + \\"spass-3.7\" directory's absolute path to " ^ quote (Path.implode (Path.expand (Path.appends (Path.variable "ISABELLE_HOME_USER" :: map Path.basic ["etc", "components"])))) ^ @@ -76,17 +76,18 @@ | string_for_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail | string_for_failure MalformedInput = - "Internal Isabelle error: The ATP problem is malformed. Please report \ - \this to the Isabelle developers." - | string_for_failure MalformedOutput = "Error: The ATP output is malformed." - | string_for_failure UnknownError = "Error: An unknown ATP error occurred." + "The ATP problem is malformed. Please report this to the Isabelle \ + \developers." + | string_for_failure MalformedOutput = "The ATP output is malformed." + | string_for_failure UnknownError = "An unknown ATP error occurred." fun known_failure_in_output output = find_first (fn (_, pattern) => String.isSubstring pattern output) #> Option.map fst val known_perl_failures = - [(NoPerl, "env: perl"), + [(CantConnect, "HTTP error"), + (NoPerl, "env: perl"), (NoLibwwwPerl, "Can't locate HTTP")] (* named provers *) @@ -124,8 +125,8 @@ ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") val e_config : prover_config = - {executable = ("E_HOME", "eproof"), - required_executables = [], + {exec = ("E_HOME", "eproof"), + required_execs = [], arguments = fn _ => fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_generous_secs timeout), @@ -139,7 +140,7 @@ "# Cannot determine problem status within resource limit"), (OutOfResources, "SZS status: ResourceOut"), (OutOfResources, "SZS status ResourceOut")], - max_new_relevant_facts_per_iter = 80 (* FIXME *), + max_new_relevant_facts_per_iter = 90 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} val e = ("e", e_config) @@ -148,13 +149,13 @@ (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) val spass_config : prover_config = - {executable = ("ISABELLE_ATP", "scripts/spass"), - required_executables = [("SPASS_HOME", "SPASS")], + {exec = ("ISABELLE_ATP", "scripts/spass"), + required_execs = [("SPASS_HOME", "SPASS")], (* "div 2" accounts for the fact that SPASS is often run twice. *) arguments = fn complete => fn timeout => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ - string_of_int (to_generous_secs timeout div 2)) + string_of_int ((to_generous_secs timeout + 1) div 2)) |> not complete ? prefix "-SOS=1 ", proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = @@ -165,7 +166,7 @@ (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (OldSpass, "tptp2dfg")], - max_new_relevant_facts_per_iter = 26 (* FIXME *), + max_new_relevant_facts_per_iter = 35 (* FIXME *), prefers_theory_relevant = true, explicit_forall = true} val spass = ("spass", spass_config) @@ -173,8 +174,8 @@ (* Vampire *) val vampire_config : prover_config = - {executable = ("VAMPIRE_HOME", "vampire"), - required_executables = [], + {exec = ("VAMPIRE_HOME", "vampire"), + required_execs = [], arguments = fn _ => fn timeout => "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^ " --input_file ", @@ -186,9 +187,10 @@ known_failures = [(Unprovable, "UNPROVABLE"), (IncompleteUnprovable, "CANNOT PROVE"), + (TimedOut, "SZS status Timeout"), (Unprovable, "Satisfiability detected"), (OutOfResources, "Refutation not found")], - max_new_relevant_facts_per_iter = 40 (* FIXME *), + max_new_relevant_facts_per_iter = 50 (* FIXME *), prefers_theory_relevant = false, explicit_forall = false} val vampire = ("vampire", vampire_config) @@ -221,16 +223,15 @@ ({proof_delims, known_failures, max_new_relevant_facts_per_iter, prefers_theory_relevant, explicit_forall, ...} : prover_config) : prover_config = - {executable = ("ISABELLE_ATP", "scripts/remote_atp"), - required_executables = [], + {exec = ("ISABELLE_ATP", "scripts/remote_atp"), + required_execs = [], arguments = fn _ => fn timeout => " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^ the_system atp_prefix, proof_delims = insert (op =) tstp_proof_delims proof_delims, known_failures = known_failures @ known_perl_failures @ - [(CantConnect, "HTTP-Error"), - (TimedOut, "says Timeout")], + [(TimedOut, "says Timeout")], max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter, prefers_theory_relevant = prefers_theory_relevant, explicit_forall = explicit_forall} @@ -243,8 +244,8 @@ val remote_e = remote_prover e "EP---" val remote_vampire = remote_prover vampire "Vampire---9" -fun is_installed ({executable, required_executables, ...} : prover_config) = - forall (curry (op <>) "" o getenv o fst) (executable :: required_executables) +fun is_installed ({exec, required_execs, ...} : prover_config) = + forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) fun maybe_remote (name, config) = name |> not (is_installed config) ? remote_name diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/ATP/scripts/remote_atp --- a/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Fri Jul 30 15:03:42 2010 +0200 @@ -98,7 +98,7 @@ if(!$Response->is_success) { my $message = $Response->message; $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//; - print $message . "\n"; + print "HTTP error: " . $message . "\n"; exit(-1); } elsif (exists($Options{'w'})) { print $Response->content; diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Jul 30 15:03:42 2010 +0200 @@ -16,9 +16,9 @@ TConsLit of name * name * name list | TVarLit of name * name datatype arity_clause = - ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} datatype class_rel_clause = - ClassRelClause of {axiom_name: string, subclass: name, superclass: name} + ClassRelClause of {name: string, subclass: name, superclass: name} datatype combtyp = CombTVar of name | CombTFree of name | @@ -84,8 +84,6 @@ val tvar_prefix = "T_"; val tfree_prefix = "t_"; -val class_rel_clause_prefix = "clsrel_"; - val const_prefix = "c_"; val type_const_prefix = "tc_"; val class_prefix = "class_"; @@ -259,7 +257,7 @@ TVarLit of name * name datatype arity_clause = - ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} fun gen_TVars 0 = [] @@ -271,12 +269,12 @@ (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) (*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) = +fun make_axiom_arity_clause (tcons, name, (cls,args)) = let val tvars = gen_TVars (length args) val tvars_srts = ListPair.zip (tvars, args) in - ArityClause {axiom_name = axiom_name, + ArityClause {name = name, conclLit = TConsLit (`make_type_class cls, `make_fixed_type_const tcons, tvars ~~ tvars), @@ -287,7 +285,7 @@ (**** Isabelle class relations ****) datatype class_rel_clause = - ClassRelClause of {axiom_name: string, subclass: name, superclass: name} + ClassRelClause of {name: string, subclass: name, superclass: name} (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs _ [] _ = [] @@ -299,10 +297,9 @@ in fold add_supers subs [] end fun make_class_rel_clause (sub,super) = - ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^ - ascii_of super, + ClassRelClause {name = sub ^ "_" ^ super, subclass = `make_type_class sub, - superclass = `make_type_class super}; + superclass = `make_type_class super} fun make_class_rel_clauses thy subs supers = map make_class_rel_clause (class_pairs thy subs supers); diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jul 30 15:03:42 2010 +0200 @@ -86,11 +86,11 @@ val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis.Term.Var v - | _ => raise Fail "hol_term_to_fol_FO"; + | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm") -fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s - | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = +fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist) + | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); @@ -764,12 +764,11 @@ (_,ith)::_ => (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); [ith]) - | _ => (trace_msg (fn () => "Metis: No result"); - raise METIS ("FOL_SOLVE", "")) + | _ => (trace_msg (fn () => "Metis: No result"); []) end | Metis.Resolution.Satisfiable _ => (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); - raise METIS ("FOL_SOLVE", "")) + []) end; val type_has_top_sort = @@ -798,10 +797,8 @@ if mode = HO then (warning ("Metis: Falling back on \"metisFT\"."); generic_metis_tac FT ctxt ths i st0) - else if msg = "" then + else Seq.empty - else - raise error ("Metis (" ^ loc ^ "): " ^ msg) val metis_tac = generic_metis_tac HO val metisF_tac = generic_metis_tac FO diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jul 30 15:03:42 2010 +0200 @@ -30,8 +30,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} + axioms: (string * thm) list option} type prover_result = {outcome: failure option, message: string, @@ -41,10 +40,8 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list list, - filtered_clauses: (string * thm) list} - type prover = - params -> minimize_command -> Time.time -> problem -> prover_result + conjecture_shape: int list list} + type prover = params -> minimize_command -> problem -> prover_result val dest_dir : string Config.T val problem_prefix : string Config.T @@ -72,8 +69,13 @@ (** The Sledgehammer **) +(* Identifier to distinguish Sledgehammer from other tools using + "Async_Manager". *) val das_Tool = "Sledgehammer" +(* Freshness almost guaranteed! *) +val sledgehammer_weak_prefix = "Sledgehammer:" + fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs" fun running_atps () = Async_Manager.running_threads das_Tool "ATPs" val messages = Async_Manager.thread_messages das_Tool "ATP" @@ -100,8 +102,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option, - filtered_clauses: (string * thm) list option} + axioms: (string * thm) list option} type prover_result = {outcome: failure option, @@ -112,11 +113,9 @@ output: string, proof: string, internal_thm_names: string Vector.vector, - conjecture_shape: int list list, - filtered_clauses: (string * thm) list} + conjecture_shape: int list list} -type prover = - params -> minimize_command -> Time.time -> problem -> prover_result +type prover = params -> minimize_command -> problem -> prover_result (* configuration attributes *) @@ -163,7 +162,7 @@ (* Clause preparation *) datatype fol_formula = - FOLFormula of {formula_name: string, + FOLFormula of {name: string, kind: kind, combformula: (name, combterm) formula, ctypes_sorts: typ list} @@ -175,12 +174,12 @@ AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) (* ### FIXME: reintroduce -fun make_clause_table xs = +fun make_formula_table xs = fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty -(* Remove existing axiom clauses from the conjecture clauses, as this can +(* Remove existing axioms from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) -fun subtract_cls ax_clauses = - filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) +fun subtract_cls axioms = + filter_out (Termtab.defined (make_formula_table axioms) o prop_of) *) fun combformula_for_prop thy = @@ -235,11 +234,15 @@ | aux _ t = t in aux (maxidx_of_term t + 1) t end -(* FIXME: Guarantee freshness *) -fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j +fun presimplify_term thy = + Skip_Proof.make_thm thy + #> Meson.presimplify + #> prop_of + +fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j fun conceal_bounds Ts t = subst_bounds (map (Free o apfst concealed_bound_name) - (length Ts - 1 downto 0 ~~ rev Ts), t) + (0 upto length Ts - 1 ~~ Ts), t) fun reveal_bounds Ts = subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) (0 upto length Ts - 1 ~~ Ts)) @@ -281,29 +284,42 @@ Axiom => HOLogic.true_const | Conjecture => HOLogic.false_const -(* making axiom and conjecture clauses *) -fun make_clause ctxt (formula_name, kind, t) = +(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the + same in Sledgehammer to prevent the discovery of unreplable proofs. *) +fun freeze_term t = + let + fun aux (t $ u) = aux t $ aux u + | aux (Abs (s, T, t)) = Abs (s, T, aux t) + | aux (Var ((s, i), T)) = + Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) + | aux t = t + in t |> exists_subterm is_Var t ? aux end + +(* making axiom and conjecture formulas *) +fun make_formula ctxt presimp (name, kind, t) = let val thy = ProofContext.theory_of ctxt - (* ### FIXME: perform other transformations previously done by - "Clausifier.to_nnf", e.g. "HOL.If" *) val t = t |> transform_elim_term |> Object_Logic.atomize_term thy + val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop |> extensionalize_term + |> presimp ? presimplify_term thy + |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind + |> kind = Conjecture ? freeze_term val (combformula, ctypes_sorts) = combformula_for_prop thy t [] in - FOLFormula {formula_name = formula_name, combformula = combformula, - kind = kind, ctypes_sorts = ctypes_sorts} + FOLFormula {name = name, combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts} end -fun make_axiom_clause ctxt (name, th) = - (name, make_clause ctxt (name, Axiom, prop_of th)) -fun make_conjecture_clauses ctxt ts = - map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t)) +fun make_axiom ctxt presimp (name, th) = + (name, make_formula ctxt presimp (name, Axiom, prop_of th)) +fun make_conjectures ctxt ts = + map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t)) (0 upto length ts - 1) ts -(** Helper clauses **) +(** Helper facts **) fun count_combterm (CombConst ((s, _), _, _)) = Symtab.map_entry s (Integer.add 1) @@ -328,52 +344,40 @@ Symtab.make (maps (maps (map (rpair 0) o fst)) [optional_helpers, optional_typed_helpers]) -fun get_helper_clauses ctxt is_FO full_types conjectures axclauses = +fun get_helper_facts ctxt is_FO full_types conjectures axioms = let - val ct = fold (fold count_fol_formula) [conjectures, axclauses] - init_counters + val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 - val cnfs = - (optional_helpers - |> full_types ? append optional_typed_helpers - |> maps (fn (ss, ths) => - if exists is_needed ss then map (`Thm.get_name_hint) ths - else [])) @ - (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) - in map (snd o make_axiom_clause ctxt) cnfs end + in + (optional_helpers + |> full_types ? append optional_typed_helpers + |> maps (fn (ss, ths) => + if exists is_needed ss then map (`Thm.get_name_hint) ths + else [])) @ + (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers) + |> map (snd o make_axiom ctxt false) + end -fun s_not (@{const Not} $ t) = t - | s_not t = @{const Not} $ t +fun meta_not t = @{const "==>"} $ t $ @{prop False} -(* prepare for passing to writer, - create additional clauses based on the information from extra_cls *) -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls = +fun prepare_formulas ctxt full_types hyp_ts concl_t axcls = let val thy = ProofContext.theory_of ctxt val goal_t = Logic.list_implies (hyp_ts, concl_t) val is_FO = Meson.is_fol_term thy goal_t - val axtms = map (prop_of o snd) extra_cls + val axtms = map (prop_of o snd) axcls val subs = tfree_classes_of_terms [goal_t] val supers = tvar_classes_of_terms axtms val tycons = type_consts_of_terms thy (goal_t :: axtms) - (* TFrees in conjecture clauses; TVars in axiom clauses *) - val conjectures = - map (s_not o HOLogic.dest_Trueprop) hyp_ts @ - [HOLogic.dest_Trueprop concl_t] - |> make_conjecture_clauses ctxt - val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls - val (clnames, axiom_clauses) = - ListPair.unzip (map (make_axiom_clause ctxt) axcls) - (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the - "get_helper_clauses" call? *) - val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures extra_clauses + (* TFrees in the conjecture; TVars in the axioms *) + val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt + val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls) + val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in (Vector.fromList clnames, - (conjectures, axiom_clauses, extra_clauses, helper_clauses, - class_rel_clauses, arity_clauses)) + (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) end fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -397,10 +401,15 @@ val (head, args) = strip_combterm_comb u val (x, ty_args) = case head of - CombConst (name, _, ty_args) => - if fst name = "equal" then + CombConst (name as (s, s'), _, ty_args) => + if s = "equal" then (if top_level andalso length args = 2 then name else ("c_fequal", @{const_name fequal}), []) + else if top_level then + case s of + "c_False" => (("$false", s'), []) + | "c_True" => (("$true", s'), []) + | _ => (name, if full_types then [] else ty_args) else (name, if full_types then [] else ty_args) | CombVar (name, _) => (name, []) @@ -424,15 +433,14 @@ (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) -fun problem_line_for_axiom full_types - (formula as FOLFormula {formula_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of formula_name, kind, - formula_for_axiom full_types formula) +fun problem_line_for_fact prefix full_types + (formula as FOLFormula {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) -fun problem_line_for_class_rel_clause - (ClassRelClause {axiom_name, subclass, superclass, ...}) = +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, + superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in - Fof (ascii_of axiom_name, Axiom, + Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), AAtom (ATerm (superclass, [ty_arg]))])) end @@ -442,17 +450,17 @@ | fo_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun problem_line_for_arity_clause - (ArityClause {axiom_name, conclLit, premLits, ...}) = - Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, + ...}) = + Fof (arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_for_fo_literal o apfst not o fo_literal_for_arity_literal) premLits) (formula_for_fo_literal (fo_literal_for_arity_literal conclLit))) fun problem_line_for_conjecture full_types - (FOLFormula {formula_name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ formula_name, kind, + (FOLFormula {name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ name, kind, formula_for_combformula full_types combformula) fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = @@ -596,17 +604,18 @@ (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, extra_clauses, - helper_clauses, class_rel_clauses, arity_clauses) = + file (conjectures, axioms, helper_facts, class_rel_clauses, + arity_clauses) = let - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses + val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms + val helper_lines = + map (problem_line_for_fact helper_prefix full_types) helper_facts + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_clauses - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = @@ -638,7 +647,8 @@ val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id + --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")" --| Scan.option ($$ ",") val parse_clause_formula_relation = Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" @@ -664,8 +674,8 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map (the o AList.lookup (op =) name_map) - |> map (fn s => case try (unprefix axiom_prefix) s of + seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the + |> try (unprefix axiom_prefix) of SOME s' => undo_ascii_of s' | NONE => "") |> Vector.fromList) @@ -677,33 +687,29 @@ (* generic TPTP-based provers *) fun prover_fun name - {executable, required_executables, arguments, proof_delims, - known_failures, max_new_relevant_facts_per_iter, - prefers_theory_relevant, explicit_forall} + {exec, required_execs, arguments, proof_delims, known_failures, + max_new_relevant_facts_per_iter, prefers_theory_relevant, + explicit_forall} ({debug, overlord, full_types, explicit_apply, relevance_threshold, relevance_convergence, theory_relevant, defs_relevant, isar_proof, - isar_shrink_factor, ...} : params) - minimize_command timeout - ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} - : problem) = + isar_shrink_factor, timeout, ...} : params) + minimize_command + ({subgoal, goal, relevance_override, axioms} : problem) = let - (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt (* ### FIXME: (1) preprocessing for "if" etc. *) val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - val the_filtered_clauses = - case filtered_clauses of - SOME fcls => fcls + val the_axioms = + case axioms of + SOME axioms => axioms | NONE => relevant_facts full_types relevance_threshold relevance_convergence defs_relevant max_new_relevant_facts_per_iter (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t - val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses - val (internal_thm_names, clauses) = - prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses - the_filtered_clauses + val (internal_thm_names, formulas) = + prepare_formulas ctxt full_types hyp_ts concl_t the_axioms (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -722,7 +728,7 @@ else error ("No such directory: " ^ the_dest_dir ^ ".") end; - val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable) + val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) (* write out problem file and call prover *) fun command_line complete probfile = let @@ -746,8 +752,7 @@ val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (output, as_time t) end; fun run_on probfile = - case filter (curry (op =) "" o getenv o fst) - (executable :: required_executables) of + case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of (home_var, _) :: _ => error ("The environment variable " ^ quote home_var ^ " is not set.") | [] => @@ -771,7 +776,7 @@ val readable_names = debug andalso overlord val (pool, conjecture_offset) = write_tptp_file thy readable_names explicit_forall full_types - explicit_apply probfile clauses + explicit_apply probfile formulas val conjecture_shape = conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |> map single @@ -814,8 +819,7 @@ {outcome = outcome, message = message, pool = pool, used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs, output = output, proof = proof, internal_thm_names = internal_thm_names, - conjecture_shape = conjecture_shape, - filtered_clauses = the_filtered_clauses} + conjecture_shape = conjecture_shape} end fun get_prover_fun thy name = prover_fun name (get_prover thy name) @@ -837,10 +841,9 @@ let val problem = {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axiom_clauses = NONE, - filtered_clauses = NONE} + relevance_override = relevance_override, axioms = NONE} in - prover params (minimize_command name) timeout problem |> #message + prover params (minimize_command name) problem |> #message handle ERROR message => "Error: " ^ message ^ "\n" end) end diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jul 30 15:03:42 2010 +0200 @@ -88,18 +88,9 @@ (fn [] => [] | ctypss => insert (op =) ctyps ctypss) val fresh_prefix = "Sledgehammer.Fresh." - val flip = Option.map not - -val boring_natural_consts = [@{const_name If}] -(* Including equality in this list might be expected to stop rules like - subset_antisym from being chosen, but for some reason filtering works better - with them listed. The logical signs All, Ex, &, and --> are omitted for CNF - because any remaining occurrences must be within comprehensions. *) -val boring_cnf_consts = - [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all}, - @{const_name "=="}, @{const_name "op |"}, @{const_name Not}, - @{const_name "op ="}] +(* These are typically simplified away by "Meson.presimplify". *) +val boring_consts = [@{const_name If}, @{const_name Let}] fun get_consts_typs thy pos ts = let @@ -149,7 +140,7 @@ do_term t0 #> do_formula pos t1 (* theory constant *) | _ => do_term t in - Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts + Symtab.empty |> fold (Symtab.update o rpair []) boring_consts |> fold (do_formula pos) ts end @@ -213,11 +204,8 @@ (the (Symtab.lookup const_tab c) handle Option.Option => raise Fail ("Const: " ^ c)) 0 -(*A surprising number of theorems contain only a few significant constants. - These include all induction rules, and other general theorems. Filtering - theorems in clause form reveals these complexities in the form of Skolem - functions. If we were instead to filter theorems in their natural form, - some other method of measuring theorem complexity would become necessary.*) +(* A surprising number of theorems contain only a few significant constants. + These include all induction rules, and other general theorems. *) (* "log" seems best in practice. A constant function of one ignores the constant frequencies. *) @@ -228,13 +216,13 @@ (*Relevant constants are weighted according to frequency, but irrelevant constants are simply counted. Otherwise, Skolem functions, - which are rare, would harm a clause's chances of being picked.*) -fun clause_weight const_tab gctyps consts_typs = - let val rel = filter (uni_mem gctyps) consts_typs - val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 - in - rel_weight / (rel_weight + real (length consts_typs - length rel)) - end; + which are rare, would harm a formula's chances of being picked.*) +fun formula_weight const_tab gctyps consts_typs = + let + val rel = filter (uni_mem gctyps) consts_typs + val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0 + val res = rel_weight / (rel_weight + real (length consts_typs - length rel)) + in if Real.isFinite res then res else 0.0 end (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*) fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys; @@ -270,13 +258,13 @@ | _ => false end; -type annotated_cnf_thm = (string * thm) * (string * const_typ list) list +type annotated_thm = (string * thm) * (string * const_typ list) list (*For a reverse sort, putting the largest values first.*) fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1) -(*Limit the number of new clauses, to prevent runaway acceptance.*) -fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) = +(* Limit the number of new facts, to prevent runaway acceptance. *) +fun take_best max_new (newpairs : (annotated_thm * real) list) = let val nnew = length newpairs in if nnew <= max_new then (map #1 newpairs, []) @@ -294,8 +282,8 @@ end end; -fun relevant_clauses ctxt relevance_convergence defs_relevant max_new - ({add, del, ...} : relevance_override) const_tab = +fun relevant_facts ctxt relevance_convergence defs_relevant max_new + ({add, del, ...} : relevance_override) const_tab = let val thy = ProofContext.theory_of ctxt val add_thms = maps (ProofContext.get_fact ctxt) add @@ -323,7 +311,8 @@ val weight = if member Thm.eq_thm add_thms th then 1.0 else if member Thm.eq_thm del_thms th then 0.0 - else clause_weight const_tab rel_const_tab consts_typs + else formula_weight const_tab rel_const_tab consts_typs +val _ = (if Real.isFinite weight then () else error ("*** " ^ Real.toString weight)) (*###*) in if weight >= threshold orelse (defs_relevant andalso defines thy th rel_const_tab) then @@ -335,7 +324,7 @@ relevant (newrels, ax :: rejects) axs end in - trace_msg (fn () => "relevant_clauses, current threshold: " ^ + trace_msg (fn () => "relevant_facts, current threshold: " ^ Real.toString threshold); relevant ([], []) end @@ -353,7 +342,7 @@ val const_tab = fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty val goal_const_tab = get_consts_typs thy (SOME true) goal_ts - val relevance_threshold = 0.9 * relevance_threshold (* FIXME *) + val relevance_threshold = 0.8 * relevance_threshold (* FIXME *) val _ = trace_msg (fn () => "Initial constants: " ^ commas (goal_const_tab @@ -361,11 +350,11 @@ |> filter (curry (op <>) [] o snd) |> map fst)) val relevant = - relevant_clauses ctxt relevance_convergence defs_relevant max_new - relevance_override const_tab relevance_threshold - goal_const_tab - (map (pair_consts_typs_axiom theory_relevant thy) - axioms) + relevant_facts ctxt relevance_convergence defs_relevant max_new + relevance_override const_tab relevance_threshold + goal_const_tab + (map (pair_consts_typs_axiom theory_relevant thy) + axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -387,11 +376,9 @@ String.isSuffix "_def" a orelse String.isSuffix "_defs" a end; -fun make_clause_table xs = +fun make_fact_table xs = fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty - -fun make_unique xs = - Termtab.fold (cons o snd) (make_clause_table xs) [] +fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) [] (* FIXME: put other record thms here, or declare as "no_atp" *) val multi_base_blacklist = @@ -427,8 +414,7 @@ | apply_depth _ = 0 fun is_formula_too_complex t = - apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse - formula_has_too_many_lambdas [] t + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t val exists_sledgehammer_const = exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) @@ -459,7 +445,8 @@ (facts, []) |-> Facts.fold_static (fn (name, ths0) => if Facts.is_concealed facts name orelse (respect_no_atp andalso is_package_def name) orelse - member (op =) multi_base_blacklist (Long_Name.base_name name) then + member (op =) multi_base_blacklist (Long_Name.base_name name) orelse + String.isSuffix "_def_raw" (* FIXME: crude hack *) name then I else let @@ -512,12 +499,13 @@ (* ATP invocation methods setup *) (***************************************************************) -(**** Predicates to detect unwanted clauses (prolific or likely to cause +(**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) (** Too general means, positive equality literal with a variable X as one operand, when X does not occur properly in the other operand. This rules out clearly - inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **) + inconsistent facts such as V = a | V = b, though it by no means guarantees + soundness. **) fun var_occurs_in_term ix = let @@ -532,6 +520,7 @@ (*Unwanted equalities include (1) those between a variable that does not properly occur in the second operand, (2) those between a variable and a record, since these seem to be prolific "cases" thms + (* FIXME: still a problem? *) *) fun too_general_eqterms (Var (ix,T), t) = not (var_occurs_in_term ix t) orelse is_record_type T @@ -544,14 +533,14 @@ fun has_typed_var tycons = exists_subterm (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false); -(* Clauses are forbidden to contain variables of these types. The typical reason +(* Facts are forbidden to contain variables of these types. The typical reason is that they lead to unsoundness. Note that "unit" satisfies numerous - equations like "?x = ()". The resulting clause will have no type constraint, + equations like "?x = ()". The resulting clauses will have no type constraint, yielding false proofs. Even "bool" leads to many unsound proofs, though only for higher-order problems. *) val dangerous_types = [@{type_name unit}, @{type_name bool}]; -(* Clauses containing variables of type "unit" or "bool" or of the form +(* Facts containing variables of type "unit" or "bool" or of the form "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are omitted. *) fun is_dangerous_term _ @{prop True} = true diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Jul 30 15:03:42 2010 +0200 @@ -18,7 +18,7 @@ structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = struct -open Metis_Clauses +open ATP_Systems open Sledgehammer_Util open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct @@ -27,44 +27,61 @@ (* wrapper for calling external prover *) fun string_for_failure Unprovable = "Unprovable." - | string_for_failure IncompleteUnprovable = "Failed." | string_for_failure TimedOut = "Timed out." - | string_for_failure OutOfResources = "Failed." - | string_for_failure OldSpass = "Error." - | string_for_failure MalformedOutput = "Error." - | string_for_failure UnknownError = "Failed." -fun string_for_outcome NONE = "Success." - | string_for_outcome (SOME failure) = string_for_failure failure + | string_for_failure _ = "Unknown error." -fun sledgehammer_test_theorems (params : params) prover timeout subgoal state - filtered_clauses name_thms_pairs = +fun n_theorems name_thms_pairs = + let val n = length name_thms_pairs in + string_of_int n ^ " theorem" ^ plural_s n ^ + (if n > 0 then + ": " ^ space_implode " " + (name_thms_pairs + |> map (perhaps (try (unprefix chained_prefix))) + |> sort_distinct string_ord) + else + "") + end + +fun test_theorems ({debug, verbose, overlord, atps, full_types, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, isar_shrink_factor, + ...} : params) + (prover : prover) explicit_apply timeout subgoal state + name_thms_pairs = let - val num_theorems = length name_thms_pairs val _ = - priority ("Testing " ^ string_of_int num_theorems ^ - " theorem" ^ plural_s num_theorems ^ - (if num_theorems > 0 then - ": " ^ space_implode " " - (name_thms_pairs - |> map fst |> sort_distinct string_ord) - else - "") ^ "...") - val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs + priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...") + val params = + {debug = debug, verbose = verbose, overlord = overlord, atps = atps, + full_types = full_types, explicit_apply = explicit_apply, + relevance_threshold = relevance_threshold, + relevance_convergence = relevance_convergence, + theory_relevant = theory_relevant, defs_relevant = defs_relevant, + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + timeout = timeout, minimize_timeout = timeout} + val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, - axiom_clauses = SOME name_thm_pairs, - filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)} + axioms = SOME axioms} + val result as {outcome, used_thm_names, ...} = + prover params (K "") problem in - prover params (K "") timeout problem - |> tap (fn result : prover_result => - priority (string_for_outcome (#outcome result))) + priority (case outcome of + NONE => + if length used_thm_names = length name_thms_pairs then + "Found proof." + else + "Found proof with " ^ n_theorems used_thm_names ^ "." + | SOME failure => string_for_failure failure); + result end (* minimalization of thms *) -fun filter_used_facts used = filter (member (op =) used o fst) +fun filter_used_facts used = + filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst) fun sublinear_minimize _ [] p = p | sublinear_minimize test (x :: xs) (seen, result) = @@ -75,34 +92,52 @@ (filter_used_facts used_thm_names seen, result) | _ => sublinear_minimize test xs (x :: seen, result) -fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, - isar_proof, isar_shrink_factor, ...}) - i n state name_thms_pairs = +(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer + preprocessing time is included in the estimate below but isn't part of the + timeout. *) +val fudge_msecs = 250 + +fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set." + | minimize_theorems + (params as {debug, verbose, overlord, atps as atp :: _, full_types, + relevance_threshold, relevance_convergence, theory_relevant, + defs_relevant, isar_proof, isar_shrink_factor, + minimize_timeout, ...}) + i n state name_thms_pairs = let val thy = Proof.theory_of state - val prover = case atps of - [atp_name] => get_prover_fun thy atp_name - | _ => error "Expected a single ATP." + val prover = get_prover_fun thy atp val msecs = Time.toMilliseconds minimize_timeout val _ = - priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^ + priority ("Sledgehammer minimizer: ATP " ^ quote atp ^ " with a time limit of " ^ string_of_int msecs ^ " ms.") - val test_facts = - sledgehammer_test_theorems params prover minimize_timeout i state - val {context = ctxt, goal, ...} = Proof.goal state; + val {context = ctxt, goal, ...} = Proof.goal state + val (_, hyp_ts, concl_t) = strip_subgoal goal i + val explicit_apply = + not (forall (Meson.is_fol_term thy) + (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs)) + fun do_test timeout = + test_theorems params prover explicit_apply timeout i state + val timer = Timer.startRealTimer () in - (* try prove first to check result and get used theorems *) - (case test_facts NONE name_thms_pairs of - result as {outcome = NONE, pool, proof, used_thm_names, - conjecture_shape, filtered_clauses, ...} => + (case do_test minimize_timeout name_thms_pairs of + result as {outcome = NONE, pool, used_thm_names, + conjecture_shape, ...} => let + val time = Timer.checkRealTimer timer + val new_timeout = + Int.min (msecs, Time.toMilliseconds time + fudge_msecs) + |> Time.fromMilliseconds val (min_thms, {proof, internal_thm_names, ...}) = - sublinear_minimize (test_facts (SOME filtered_clauses)) - (filter_used_facts used_thm_names name_thms_pairs) - ([], result) - val m = length min_thms + sublinear_minimize (do_test new_timeout) + (filter_used_facts used_thm_names name_thms_pairs) ([], result) + val n = length min_thms val _ = priority (cat_lines - ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") + ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ + (case filter (String.isPrefix chained_prefix o fst) min_thms of + [] => "" + | chained => " (including " ^ Int.toString (length chained) ^ + " chained)") ^ ".") in (SOME min_thms, proof_text isar_proof diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 30 15:03:42 2010 +0200 @@ -88,8 +88,8 @@ ("no_isar_proof", "isar_proof")] val params_for_minimize = - ["debug", "verbose", "overlord", "full_types", "explicit_apply", - "isar_proof", "isar_shrink_factor", "minimize_timeout"] + ["debug", "verbose", "overlord", "full_types", "isar_proof", + "isar_shrink_factor", "minimize_timeout"] val property_dependent_params = ["atps", "full_types", "timeout"] diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 30 15:03:42 2010 +0200 @@ -12,6 +12,8 @@ val axiom_prefix : string val conjecture_prefix : string + val helper_prefix : string + val class_rel_clause_prefix : string val arity_clause_prefix : string val tfrees_name : string val metis_line: bool -> int -> int -> string list -> string @@ -40,7 +42,9 @@ val axiom_prefix = "ax_" val conjecture_prefix = "conj_" -val arity_clause_prefix = "clsarity_" +val helper_prefix = "help_" +val class_rel_clause_prefix = "clrel_"; +val arity_clause_prefix = "arity_" val tfrees_name = "tfrees" (* Simple simplifications to ensure that sort annotations don't leave a trail of @@ -67,10 +71,10 @@ fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) fun index_in_shape x = find_index (exists (curry (op =) x)) -fun is_axiom_clause_number thm_names num = +fun is_axiom_number thm_names num = num > 0 andalso num <= Vector.length thm_names andalso Vector.sub (thm_names, num - 1) <> "" -fun is_conjecture_clause_number conjecture_shape num = +fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = @@ -281,7 +285,7 @@ (SOME b, [T]) => (pos, b, T) | _ => raise FO_TERM [u] -(** Accumulate type constraints in a clause: negative type literals **) +(** Accumulate type constraints in a formula: negative type literals **) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) | add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) @@ -407,8 +411,8 @@ | frees as (_, free_T) :: _ => Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t) -(* Interpret a list of syntax trees as a clause, extracting sort constraints - as they appear in the formula. *) +(* Interpret an ATP formula as a HOL term, extracting sort constraints as they + appear in the formula. *) fun prop_from_formula thy full_types tfrees phi = let fun do_formula pos phi = @@ -484,13 +488,13 @@ | replace_deps_in_line p (Inference (num, t, deps)) = Inference (num, t, fold (union (op =) o replace_one_dep p) deps []) -(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ - only in type information.*) +(* Discard axioms; consolidate adjacent lines that prove the same formula, since + they differ only in type information.*) fun add_line _ _ (line as Definition _) lines = line :: lines | add_line conjecture_shape thm_names (Inference (num, t, [])) lines = - (* No dependencies: axiom, conjecture clause, or internal axioms or - definitions (Vampire). *) - if is_axiom_clause_number thm_names num then + (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or + definitions. *) + if is_axiom_number thm_names num then (* Axioms are not proof lines. *) if is_only_type_information t then map (replace_deps_in_line (num, [])) lines @@ -499,8 +503,8 @@ (_, []) => lines (*no repetition of proof line*) | (pre, Inference (num', _, _) :: post) => pre @ map (replace_deps_in_line (num', [num])) post - else if is_conjecture_clause_number conjecture_shape num then - Inference (num, t, []) :: lines + else if is_conjecture_number conjecture_shape num then + Inference (num, negate_term t, []) :: lines else map (replace_deps_in_line (num, [])) lines | add_line _ _ (Inference (num, t, deps)) lines = @@ -539,8 +543,8 @@ | add_desired_line isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, - if is_axiom_clause_number thm_names num orelse - is_conjecture_clause_number conjecture_shape num orelse + if is_axiom_number thm_names num orelse + is_conjecture_number conjecture_shape num orelse (not (is_only_type_information t) andalso null (Term.add_tvars t []) andalso not (exists_subterm (is_bad_free frees) t) andalso @@ -562,10 +566,8 @@ let fun axiom_name num = let val j = Int.fromString num |> the_default ~1 in - if is_axiom_clause_number thm_names j then - SOME (Vector.sub (thm_names, j - 1)) - else - NONE + if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1)) + else NONE end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") @@ -655,7 +657,7 @@ | smart_case_split proofs facts = CaseSplit (proofs, facts) fun add_fact_from_dep thm_names num = - if is_axiom_clause_number thm_names num then + if is_axiom_number thm_names num then apsnd (insert (op =) (Vector.sub (thm_names, num - 1))) else apfst (insert (op =) (raw_prefix, num)) diff -r 61280b97b761 -r d44a5f602b8c src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Jul 29 18:16:35 2010 +0200 +++ b/src/HOL/Tools/meson.ML Fri Jul 30 15:03:42 2010 +0200 @@ -14,6 +14,7 @@ val too_many_clauses: Proof.context option -> term -> bool val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context val finish_cnf: thm list -> thm list + val presimplify: thm -> thm val make_nnf: Proof.context -> thm -> thm val skolemize: Proof.context -> thm -> thm val is_fol_term: theory -> term -> bool @@ -389,10 +390,13 @@ fun sort_clauses ths = sort (make_ord fewerlits) ths; -(*True if the given type contains bool anywhere*) -fun has_bool (Type("bool",_)) = true - | has_bool (Type(_, Ts)) = exists has_bool Ts - | has_bool _ = false; +fun has_bool @{typ bool} = true + | has_bool (Type (_, Ts)) = exists has_bool Ts + | has_bool _ = false + +fun has_fun (Type (@{type_name fun}, _)) = true + | has_fun (Type (_, Ts)) = exists has_fun Ts + | has_fun _ = false (*Is the string the name of a connective? Really only | and Not can remain, since this code expects to be called on a clause form.*) @@ -404,7 +408,7 @@ of any argument contains bool.*) val has_bool_arg_const = exists_Const - (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T)); + (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T)); (*A higher-order instance of a first-order constant? Example is the definition of one, 1, at a function type in theory SetsAndFunctions.*) @@ -417,8 +421,9 @@ Also rejects functions whose arguments are Booleans or other functions.*) fun is_fol_term thy t = Term.is_first_order ["all","All","Ex"] t andalso - not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse - has_bool_arg_const t orelse + not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T + | _ => false) t orelse + has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t orelse has_meta_conn t); @@ -529,9 +534,12 @@ HOL_basic_ss addsimps nnf_extra_simps addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; +val presimplify = + rewrite_rule (map safe_mk_meta_eq nnf_simps) + #> simplify nnf_ss + fun make_nnf ctxt th = case prems_of th of - [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps) - |> simplify nnf_ss + [] => th |> presimplify |> make_nnf1 ctxt | _ => raise THM ("make_nnf: premises in argument", 0, [th]);