src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 43290 07eb0ad9bb93
parent 43261 a4aeb26a6362
child 43292 ff3d49e77359
equal deleted inserted replaced
43289:0f2bbcfaf208 43290:07eb0ad9bb93
    17   val someN : string
    17   val someN : string
    18   val noneN : string
    18   val noneN : string
    19   val timeoutN : string
    19   val timeoutN : string
    20   val unknownN : string
    20   val unknownN : string
    21   val auto_minimize_min_facts : int Config.T
    21   val auto_minimize_min_facts : int Config.T
    22   val auto_minimize_max_seconds : real Config.T
    22   val auto_minimize_max_time : real Config.T
    23   val get_minimizing_prover : Proof.context -> mode -> string -> prover
    23   val get_minimizing_prover : Proof.context -> mode -> string -> prover
    24   val run_sledgehammer :
    24   val run_sledgehammer :
    25     params -> mode -> int -> relevance_override -> (string -> minimize_command)
    25     params -> mode -> int -> relevance_override -> (string -> minimize_command)
    26     -> Proof.state -> bool * (string * Proof.state)
    26     -> Proof.state -> bool * (string * Proof.state)
    27 end;
    27 end;
    67       "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    67       "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    68 
    68 
    69 val auto_minimize_min_facts =
    69 val auto_minimize_min_facts =
    70   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
    70   Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
    71       (fn generic => Config.get_generic generic binary_min_facts)
    71       (fn generic => Config.get_generic generic binary_min_facts)
    72 val auto_minimize_max_seconds =
    72 val auto_minimize_max_time =
    73   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_seconds}
    73   Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
    74       (K 5.0)
    74       (K 5.0)
    75 
    75 
    76 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    76 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    77              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    77              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    78              (result as {outcome, used_facts, run_time_in_msecs, preplay,
    78              (result as {outcome, used_facts, run_time_in_msecs, preplay,
    88             ((true, name), preplay)
    88             ((true, name), preplay)
    89           else
    89           else
    90             let
    90             let
    91               fun can_min_fast_enough msecs =
    91               fun can_min_fast_enough msecs =
    92                 0.001 * Real.fromInt ((num_facts + 2) * msecs)
    92                 0.001 * Real.fromInt ((num_facts + 2) * msecs)
    93                 <= Config.get ctxt auto_minimize_max_seconds
    93                 <= Config.get ctxt auto_minimize_max_time
    94               val prover_fast_enough =
    94               val prover_fast_enough =
    95                 run_time_in_msecs |> Option.map can_min_fast_enough
    95                 run_time_in_msecs |> Option.map can_min_fast_enough
    96                                   |> the_default false
    96                                   |> the_default false
    97             in
    97             in
    98               if isar_proof then
    98               if isar_proof then