src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author blanchet
Mon Mar 28 12:05:47 2016 +0200 (2016-03-28 ago)
changeset 62735 23de054397e5
parent 62505 9e2a65912111
child 62826 eb94e570c1a4
permissions -rw-r--r--
early warning when Sledgehammer finds a proof
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 SMT solvers as Sledgehammer provers.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVER_SMT =
    10 sig
    11   type stature = ATP_Problem_Generate.stature
    12   type mode = Sledgehammer_Prover.mode
    13   type prover = Sledgehammer_Prover.prover
    14 
    15   val smt_builtins : bool Config.T
    16   val smt_triggers : bool Config.T
    17   val smt_max_slices : int Config.T
    18   val smt_slice_fact_frac : real Config.T
    19   val smt_slice_time_frac : real Config.T
    20   val smt_slice_min_secs : int Config.T
    21 
    22   val is_smt_prover : Proof.context -> string -> bool
    23   val run_smt_solver : mode -> string -> prover
    24 end;
    25 
    26 structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
    27 struct
    28 
    29 open ATP_Util
    30 open ATP_Proof
    31 open ATP_Systems
    32 open ATP_Problem_Generate
    33 open ATP_Proof_Reconstruct
    34 open Sledgehammer_Util
    35 open Sledgehammer_Proof_Methods
    36 open Sledgehammer_Isar
    37 open Sledgehammer_Prover
    38 
    39 val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
    40 val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    41 
    42 val is_smt_prover = member (op =) o SMT_Config.available_solvers_of
    43 
    44 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    45    properly in the SMT module, we must interpret these here. *)
    46 val z3_failures =
    47   [(101, OutOfResources),
    48    (103, MalformedInput),
    49    (110, MalformedInput),
    50    (112, TimedOut)]
    51 val unix_failures =
    52   [(134, Crashed),
    53    (138, Crashed),
    54    (139, Crashed)]
    55 val smt_failures = z3_failures @ unix_failures
    56 
    57 fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) =
    58     if genuine then Unprovable else GaveUp
    59   | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
    60   | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
    61     (case AList.lookup (op =) smt_failures code of
    62       SOME failure => failure
    63     | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
    64   | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
    65   | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
    66 
    67 (* FUDGE *)
    68 val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
    69 val smt_slice_fact_frac =
    70   Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
    71 val smt_slice_time_frac =
    72   Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
    73 val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
    74 
    75 val is_boring_builtin_typ =
    76   not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
    77 
    78 fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
    79       ...} : params) state goal i =
    80   let
    81     fun repair_context ctxt =
    82       ctxt |> Context.proof_map (SMT_Config.select_solver name)
    83            |> Config.put SMT_Config.verbose debug
    84            |> (if overlord then
    85                  Config.put SMT_Config.debug_files
    86                    (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
    87                else
    88                  I)
    89            |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
    90            |> not (Config.get ctxt smt_builtins)
    91               ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
    92                  #> Config.put SMT_Systems.z3_extensions false)
    93            |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
    94                 default_max_new_mono_instances
    95 
    96     val state = Proof.map_context (repair_context) state
    97     val ctxt = Proof.context_of state
    98     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
    99 
   100     fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
   101       let
   102         val timer = Timer.startRealTimer ()
   103         val slice_timeout =
   104           if slice < max_slices then
   105             let val ms = Time.toMilliseconds timeout in
   106               Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   107                 Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
   108               |> Time.fromMilliseconds
   109             end
   110           else
   111             timeout
   112         val num_facts = length facts
   113         val _ =
   114           if debug then
   115             quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
   116             " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
   117             |> writeln
   118           else
   119             ()
   120         val birth = Timer.checkRealTimer timer
   121 
   122         val filter_result as {outcome, ...} =
   123           SMT_Solver.smt_filter ctxt goal facts i slice_timeout
   124           handle exn =>
   125             if Exn.is_interrupt exn orelse debug then
   126               Exn.reraise exn
   127             else
   128               {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
   129                fact_ids = NONE, atp_proof = K []}
   130 
   131         val death = Timer.checkRealTimer timer
   132         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   133         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   134         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   135 
   136         val too_many_facts_perhaps =
   137           (case outcome of
   138             NONE => false
   139           | SOME (SMT_Failure.Counterexample _) => false
   140           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   141           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   142           | SOME SMT_Failure.Out_Of_Memory => true
   143           | SOME (SMT_Failure.Other_Failure _) => true)
   144       in
   145         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   146            Time.> (timeout, Time.zeroTime) then
   147           let
   148             val new_num_facts =
   149               Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
   150             val factss as (new_fact_filter, _) :: _ =
   151               factss
   152               |> (fn (x :: xs) => xs @ [x])
   153               |> app_hd (apsnd (take new_num_facts))
   154             val show_filter = fact_filter <> new_fact_filter
   155 
   156             fun num_of_facts fact_filter num_facts =
   157               string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
   158               " fact" ^ plural_s num_facts
   159 
   160             val _ =
   161               if debug then
   162                 quote name ^ " invoked with " ^
   163                 num_of_facts fact_filter num_facts ^ ": " ^
   164                 string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   165                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   166                 "..."
   167                 |> writeln
   168               else
   169                 ()
   170           in
   171             do_slice timeout (slice + 1) outcome0 time_so_far factss
   172           end
   173         else
   174           {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
   175            used_from = facts, run_time = time_so_far}
   176       end
   177   in
   178     do_slice timeout 1 NONE Time.zeroTime
   179   end
   180 
   181 fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
   182       minimize, preplay_timeout, ...})
   183     ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) =
   184   let
   185     val thy = Proof.theory_of state
   186     val ctxt = Proof.context_of state
   187 
   188     val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
   189 
   190     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
   191       smt_filter_loop name params state goal subgoal factss
   192     val used_facts =
   193       (case fact_ids of
   194         NONE => map fst used_from
   195       | SOME ids => sort_by fst (map (fst o snd) ids))
   196     val outcome = Option.map failure_of_smt_failure outcome
   197 
   198     val (preferred_methss, message) =
   199       (case outcome of
   200         NONE =>
   201         let
   202           val _ = found_proof ();
   203           val smt_method = smt_proofs <> SOME false
   204           val preferred_methss =
   205             (if smt_method then SMT_Method else Metis_Method (NONE, NONE),
   206              bunches_of_proof_methods try0 smt_method false liftingN)
   207         in
   208           (preferred_methss,
   209            fn preplay =>
   210              let
   211                val _ = if verbose then writeln "Generating proof text..." else ()
   212 
   213                fun isar_params () =
   214                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
   215                   goal)
   216 
   217                val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
   218                val num_chained = length (#facts (Proof.goal state))
   219              in
   220                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
   221                  one_line_params
   222              end)
   223         end
   224       | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
   225   in
   226     {outcome = outcome, used_facts = used_facts, used_from = used_from,
   227      preferred_methss = preferred_methss, run_time = run_time, message = message}
   228   end
   229 
   230 end;