# HG changeset patch # User blanchet # Date 1272037105 -7200 # Node ID 2482446a604c92c884b6df5a698561935f711a62 # Parent 19c0c4b8b445802defd27ce2dcaeec95a4c8a534 move the minimizer to the Sledgehammer directory diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Apr 23 16:59:48 2010 +0200 +++ b/src/HOL/IsaMakefile Fri Apr 23 17:38:25 2010 +0200 @@ -283,7 +283,6 @@ $(SRC)/Provers/Arith/extract_common_term.ML \ $(SRC)/Tools/Metis/metis.ML \ Tools/ATP_Manager/atp_manager.ML \ - Tools/ATP_Manager/atp_minimal.ML \ Tools/ATP_Manager/atp_wrapper.ML \ Tools/Groebner_Basis/groebner.ML \ Tools/Groebner_Basis/misc.ML \ @@ -320,6 +319,7 @@ Tools/Sledgehammer/meson_tactic.ML \ Tools/Sledgehammer/metis_tactics.ML \ Tools/Sledgehammer/sledgehammer_fact_filter.ML \ + Tools/Sledgehammer/sledgehammer_fact_minimizer.ML \ Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \ Tools/Sledgehammer/sledgehammer_fol_clause.ML \ Tools/Sledgehammer/sledgehammer_hol_clause.ML \ diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Fri Apr 23 16:59:48 2010 +0200 +++ b/src/HOL/Sledgehammer.thy Fri Apr 23 17:38:25 2010 +0200 @@ -19,7 +19,7 @@ ("Tools/Sledgehammer/sledgehammer_fact_filter.ML") ("Tools/ATP_Manager/atp_manager.ML") ("Tools/ATP_Manager/atp_wrapper.ML") - ("Tools/ATP_Manager/atp_minimal.ML") + ("Tools/Sledgehammer/sledgehammer_fact_minimizer.ML") ("Tools/Sledgehammer/sledgehammer_isar.ML") ("Tools/Sledgehammer/meson_tactic.ML") ("Tools/Sledgehammer/metis_tactics.ML") @@ -103,7 +103,7 @@ use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup -use "Tools/ATP_Manager/atp_minimal.ML" +use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML" use "Tools/Sledgehammer/sledgehammer_isar.ML" diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Apr 23 16:59:48 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,128 +0,0 @@ -(* Title: HOL/Tools/ATP_Manager/atp_minimal.ML - Author: Philipp Meyer, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - -Minimization of theorem list for Metis using automatic theorem provers. -*) - -signature ATP_MINIMAL = -sig - type params = ATP_Manager.params - type prover = ATP_Manager.prover - type prover_result = ATP_Manager.prover_result - - val minimize_theorems : - params -> prover -> string -> int -> Proof.state -> (string * thm list) list - -> (string * thm list) list option * string -end; - -structure ATP_Minimal : ATP_MINIMAL = -struct - -open Sledgehammer_Util -open Sledgehammer_Fact_Preprocessor -open Sledgehammer_Proof_Reconstruct -open ATP_Manager - -(* Linear minimization algorithm *) - -fun linear_minimize test s = - let - fun aux [] p = p - | aux (x :: xs) (needed, result) = - case test (xs @ needed) of - SOME result => aux xs (needed, result) - | NONE => aux xs (x :: needed, result) - in aux s end - - -(* wrapper for calling external prover *) - -fun string_for_failure Unprovable = "Unprovable." - | 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 - -fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoal state filtered_clauses name_thms_pairs = - let - val num_theorems = length name_thms_pairs - val _ = priority ("Testing " ^ string_of_int num_theorems ^ - " theorem" ^ plural_s num_theorems ^ "...") - val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_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 axclauses, - filtered_clauses = SOME (the_default axclauses filtered_clauses)} - in - prover params (K "") timeout problem - |> tap (priority o string_for_outcome o #outcome) - end - -(* minimalization of thms *) - -fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus, - sorts, ...}) - prover atp_name i state name_thms_pairs = - let - val msecs = Time.toMilliseconds minimize_timeout - val n = length name_thms_pairs - val _ = - priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^ - " with a time limit of " ^ string_of_int msecs ^ " ms.") - val test_thms_fun = - sledgehammer_test_theorems params prover minimize_timeout i state - fun test_thms filtered thms = - case test_thms_fun filtered thms of - (result as {outcome = NONE, ...}) => SOME result - | _ => NONE - - val {context = ctxt, facts, goal} = Proof.goal state; - val n = Logic.count_prems (prop_of goal) - in - (* try prove first to check result and get used theorems *) - (case test_thms_fun NONE name_thms_pairs of - result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} => - let - val used = internal_thm_names |> Vector.foldr (op ::) [] - |> sort_distinct string_ord - val to_use = - if length used < length name_thms_pairs then - filter (fn (name1, _) => List.exists (curry (op =) name1) used) - name_thms_pairs - else name_thms_pairs - val (min_thms, {proof, internal_thm_names, ...}) = - linear_minimize (test_thms (SOME filtered_clauses)) to_use - ([], result) - val n = length min_thms - val _ = priority (cat_lines - ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") - in - (SOME min_thms, - proof_text isar_proof debug modulus sorts ctxt - (K "", proof, internal_thm_names, goal, i) |> fst) - end - | {outcome = SOME TimedOut, ...} => - (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {outcome = SOME UnknownError, ...} => - (* Failure sometimes mean timeout, unfortunately. *) - (NONE, "Failure: No proof was found with the current time limit. You \ - \can increase the time limit using the \"timeout\" \ - \option (e.g., \"timeout = " ^ - string_of_int (10 + msecs div 1000) ^ " s\").") - | {message, ...} => (NONE, "ATP error: " ^ message)) - handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], metis_line i n []) - | ERROR msg => (NONE, "Error: " ^ msg) - end - -end; diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 17:38:25 2010 +0200 @@ -0,0 +1,128 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML + Author: Philipp Meyer, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + +Minimization of theorem list for Metis using automatic theorem provers. +*) + +signature SLEDGEHAMMER_FACT_MINIMIZER = +sig + type params = ATP_Manager.params + type prover = ATP_Manager.prover + type prover_result = ATP_Manager.prover_result + + val minimize_theorems : + params -> prover -> string -> int -> Proof.state -> (string * thm list) list + -> (string * thm list) list option * string +end; + +structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = +struct + +open Sledgehammer_Util +open Sledgehammer_Fact_Preprocessor +open Sledgehammer_Proof_Reconstruct +open ATP_Manager + +(* Linear minimization algorithm *) + +fun linear_minimize test s = + let + fun aux [] p = p + | aux (x :: xs) (needed, result) = + case test (xs @ needed) of + SOME result => aux xs (needed, result) + | NONE => aux xs (x :: needed, result) + in aux s end + + +(* wrapper for calling external prover *) + +fun string_for_failure Unprovable = "Unprovable." + | 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 + +fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover + timeout subgoal state filtered_clauses name_thms_pairs = + let + val num_theorems = length name_thms_pairs + val _ = priority ("Testing " ^ string_of_int num_theorems ^ + " theorem" ^ plural_s num_theorems ^ "...") + val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs + val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_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 axclauses, + filtered_clauses = SOME (the_default axclauses filtered_clauses)} + in + prover params (K "") timeout problem + |> tap (priority o string_for_outcome o #outcome) + end + +(* minimalization of thms *) + +fun minimize_theorems (params as {debug, minimize_timeout, isar_proof, modulus, + sorts, ...}) + prover atp_name i state name_thms_pairs = + let + val msecs = Time.toMilliseconds minimize_timeout + val n = length name_thms_pairs + val _ = + priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^ + " with a time limit of " ^ string_of_int msecs ^ " ms.") + val test_thms_fun = + sledgehammer_test_theorems params prover minimize_timeout i state + fun test_thms filtered thms = + case test_thms_fun filtered thms of + (result as {outcome = NONE, ...}) => SOME result + | _ => NONE + + val {context = ctxt, facts, goal} = Proof.goal state; + val n = Logic.count_prems (prop_of goal) + in + (* try prove first to check result and get used theorems *) + (case test_thms_fun NONE name_thms_pairs of + result as {outcome = NONE, internal_thm_names, filtered_clauses, ...} => + let + val used = internal_thm_names |> Vector.foldr (op ::) [] + |> sort_distinct string_ord + val to_use = + if length used < length name_thms_pairs then + filter (fn (name1, _) => List.exists (curry (op =) name1) used) + name_thms_pairs + else name_thms_pairs + val (min_thms, {proof, internal_thm_names, ...}) = + linear_minimize (test_thms (SOME filtered_clauses)) to_use + ([], result) + val n = length min_thms + val _ = priority (cat_lines + ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") + in + (SOME min_thms, + proof_text isar_proof debug modulus sorts ctxt + (K "", proof, internal_thm_names, goal, i) |> fst) + end + | {outcome = SOME TimedOut, ...} => + (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {outcome = SOME UnknownError, ...} => + (* Failure sometimes mean timeout, unfortunately. *) + (NONE, "Failure: No proof was found with the current time limit. You \ + \can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") + | {message, ...} => (NONE, "ATP error: " ^ message)) + handle Sledgehammer_HOL_Clause.TRIVIAL => + (SOME [], metis_line i n []) + | ERROR msg => (NONE, "Error: " ^ msg) + end + +end; diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 23 16:59:48 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Apr 23 17:38:25 2010 +0200 @@ -1,5 +1,6 @@ -(* Title: HOL/Sledgehammer/sledgehammer_hol_clause.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Author: Jia Meng, NICTA + Author: Jasmin Blanchette, TU Muenchen FOL clauses translated from HOL formulae. *) diff -r 19c0c4b8b445 -r 2482446a604c src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 16:59:48 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 23 17:38:25 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Sledgehammer/sledgehammer_isar.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML Author: Jasmin Blanchette, TU Muenchen Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. @@ -19,8 +19,8 @@ open Sledgehammer_Util open ATP_Manager -open ATP_Minimal open ATP_Wrapper +open Sledgehammer_Fact_Minimizer structure K = OuterKeyword and P = OuterParse