src/HOL/Tools/ATP_Manager/atp_minimal.ML
author blanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19)
changeset 35866 513074557e06
parent 35865 2f8fb5242799
child 35867 16279c4c7a33
permissions -rw-r--r--
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_minimal.ML
     2     Author:     Philipp Meyer, TU Muenchen
     3 
     4 Minimization of theorem list for metis by using an external automated theorem prover
     5 *)
     6 
     7 signature ATP_MINIMAL =
     8 sig
     9   type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    10   val linear_minimize : 'a minimize_fun
    11   val binary_minimize : 'a minimize_fun
    12   val minimize_theorems :
    13     (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
    14     -> Proof.state -> (string * thm list) list
    15     -> (string * thm list) list option * string
    16 end;
    17 
    18 structure ATP_Minimal : ATP_MINIMAL =
    19 struct
    20 
    21 open Sledgehammer_Fact_Preprocessor
    22 
    23 type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
    24 
    25 (* Linear minimization algorithm *)
    26 
    27 fun linear_minimize p s =
    28   let
    29     fun aux [] needed = needed
    30       | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
    31   in aux s [] end;
    32 
    33 (* Binary minimalization *)
    34 
    35 local
    36   fun isplit (l, r) [] = (l, r)
    37     | isplit (l, r) [h] = (h :: l, r)
    38     | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t
    39 in
    40   fun split lst = isplit ([], []) lst
    41 end
    42 
    43 local
    44   fun min _ _ [] = raise Empty
    45     | min _ _ [s0] = [s0]
    46     | min p sup s =
    47       let
    48         val (l0, r0) = split s
    49       in
    50         if p (sup @ l0) then
    51           min p sup l0
    52         else if p (sup @ r0) then
    53           min p sup r0
    54         else
    55           let
    56             val l = min p (sup @ r0) l0
    57             val r = min p (sup @ l) r0
    58           in l @ r end
    59       end
    60 in
    61   (* return a minimal subset v of s that satisfies p
    62    @pre p(s) & ~p([]) & monotone(p)
    63    @post v subset s & p(v) &
    64          forall e in v. ~p(v \ e)
    65    *)
    66   fun binary_minimize p s =
    67     case min p [] s of
    68       [x] => if p [] then [] else [x]
    69     | m => m
    70 end
    71 
    72 
    73 (* failure check and producing answer *)
    74 
    75 datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
    76 
    77 val string_of_result =
    78   fn Success _ => "Success"
    79    | Failure => "Failure"
    80    | Timeout => "Timeout"
    81    | Error => "Error"
    82 
    83 val failure_strings =
    84   [("SPASS beiseite: Ran out of time.", Timeout),
    85    ("Timeout", Timeout),
    86    ("time limit exceeded", Timeout),
    87    ("# Cannot determine problem status within resource limit", Timeout),
    88    ("Error", Error)]
    89 
    90 fun produce_answer (result : ATP_Wrapper.prover_result) =
    91   let
    92     val {success, proof = result_string, internal_thm_names = thm_name_vec,
    93       filtered_clauses = filtered, ...} = result
    94   in
    95     if success then
    96       (Success (Vector.foldr (op ::) [] thm_name_vec, filtered), result_string)
    97     else
    98       let
    99         val failure = failure_strings |> get_first (fn (s, t) =>
   100             if String.isSubstring s result_string then SOME (t, result_string) else NONE)
   101       in
   102         (case failure of
   103           SOME res => res
   104         | NONE => (Failure, result_string))
   105       end
   106   end
   107 
   108 
   109 (* wrapper for calling external prover *)
   110 
   111 fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs =
   112   let
   113     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
   114     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
   115     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
   116     val {context = ctxt, facts, goal} = Proof.goal state
   117     val problem =
   118      {with_full_types = ! ATP_Manager.full_types,
   119       subgoal = subgoalno,
   120       goal = (ctxt, (facts, goal)),
   121       axiom_clauses = SOME axclauses,
   122       filtered_clauses = filtered}
   123     val (result, proof) = produce_answer (prover time_limit problem)
   124     val _ = priority (string_of_result result)
   125   in
   126     (result, proof)
   127   end
   128 
   129 
   130 (* minimalization of thms *)
   131 
   132 fun minimize_theorems gen_min prover prover_name time_limit state
   133                       name_thms_pairs =
   134   let
   135     val _ =
   136       priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
   137         " theorems, prover: " ^ prover_name ^
   138         ", time limit: " ^ string_of_int time_limit ^ " seconds")
   139     val test_thms_fun = sh_test_thms prover time_limit 1 state
   140     fun test_thms filtered thms =
   141       case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   142   in
   143     (* try prove first to check result and get used theorems *)
   144     (case test_thms_fun NONE name_thms_pairs of
   145       (Success (used, filtered), _) =>
   146         let
   147           val ordered_used = sort_distinct string_ord used
   148           val to_use =
   149             if length ordered_used < length name_thms_pairs then
   150               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
   151             else name_thms_pairs
   152           val min_thms =
   153             if null to_use then []
   154             else gen_min (test_thms (SOME filtered)) to_use
   155           val min_names = sort_distinct string_ord (map fst min_thms)
   156           val _ = priority (cat_lines
   157             ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
   158         in
   159           (SOME min_thms, "Try this command: " ^
   160             Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
   161         end
   162     | (Timeout, _) =>
   163         (NONE, "Timeout: You may need to increase the time limit of " ^
   164           string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
   165     | (Error, msg) =>
   166         (NONE, "Error in prover: " ^ msg)
   167     | (Failure, _) =>
   168         (NONE, "Failure: No proof with the theorems supplied"))
   169     handle Sledgehammer_HOL_Clause.TRIVIAL =>
   170         (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
   171       | ERROR msg => (NONE, "Error: " ^ msg)
   172   end
   173 
   174 end;