src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
author blanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12 ago)
changeset 57243 8c261f0a9b32
parent 57165 7b1bf424ec5f
child 57245 f6bf6d5341ee
permissions -rw-r--r--
reintroduced vital 'Thm.transfer'
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.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_SMT2 =
    10 sig
    11   type stature = ATP_Problem_Generate.stature
    12   type mode = Sledgehammer_Prover.mode
    13   type prover = Sledgehammer_Prover.prover
    14 
    15   val smt2_builtins : bool Config.T
    16   val smt2_triggers : bool Config.T
    17   val smt2_max_slices : int Config.T
    18   val smt2_slice_fact_frac : real Config.T
    19   val smt2_slice_time_frac : real Config.T
    20   val smt2_slice_min_secs : int Config.T
    21 
    22   val is_smt2_prover : Proof.context -> string -> bool
    23   val run_smt2_solver : mode -> string -> prover
    24 end;
    25 
    26 structure Sledgehammer_Prover_SMT2 : SLEDGEHAMMER_PROVER_SMT2 =
    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 smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
    40 val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true)
    41 
    42 val is_smt2_prover = member (op =) o SMT2_Config.available_solvers_of
    43 
    44 (* "SMT2_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   [(138, Crashed),
    53    (139, Crashed)]
    54 val smt2_failures = z3_failures @ unix_failures
    55 
    56 fun failure_of_smt2_failure (SMT2_Failure.Counterexample genuine) =
    57     if genuine then Unprovable else GaveUp
    58   | failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut
    59   | failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) =
    60     (case AList.lookup (op =) smt2_failures code of
    61       SOME failure => failure
    62     | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
    63   | failure_of_smt2_failure SMT2_Failure.Out_Of_Memory = OutOfResources
    64   | failure_of_smt2_failure (SMT2_Failure.Other_Failure s) = UnknownError s
    65 
    66 (* FUDGE *)
    67 val smt2_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt2_max_slices} (K 8)
    68 val smt2_slice_fact_frac =
    69   Attrib.setup_config_real @{binding sledgehammer_smt2_slice_fact_frac} (K 0.667)
    70 val smt2_slice_time_frac =
    71   Attrib.setup_config_real @{binding sledgehammer_smt2_slice_time_frac} (K 0.333)
    72 val smt2_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt2_slice_min_secs} (K 3)
    73 
    74 val is_boring_builtin_typ =
    75   not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
    76 
    77 fun smt2_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
    78       ...} : params) state goal i =
    79   let
    80     fun repair_context ctxt =
    81       ctxt |> Context.proof_map (SMT2_Config.select_solver name)
    82            |> Config.put SMT2_Config.verbose debug
    83            |> (if overlord then
    84                  Config.put SMT2_Config.debug_files
    85                    (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
    86                else
    87                  I)
    88            |> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
    89            |> not (Config.get ctxt smt2_builtins)
    90               ? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
    91                  #> Config.put SMT2_Systems.z3_extensions false)
    92            |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
    93                 default_max_new_mono_instances
    94 
    95     val state = Proof.map_context (repair_context) state
    96     val ctxt = Proof.context_of state
    97     val max_slices = if slice then Config.get ctxt smt2_max_slices else 1
    98 
    99     fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
   100       let
   101         val timer = Timer.startRealTimer ()
   102         val slice_timeout =
   103           if slice < max_slices then
   104             let val ms = Time.toMilliseconds timeout in
   105               Int.min (ms, Int.max (1000 * Config.get ctxt smt2_slice_min_secs,
   106                 Real.ceil (Config.get ctxt smt2_slice_time_frac * Real.fromInt ms)))
   107               |> Time.fromMilliseconds
   108             end
   109           else
   110             timeout
   111         val num_facts = length facts
   112         val _ =
   113           if debug then
   114             quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
   115             " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
   116             |> Output.urgent_message
   117           else
   118             ()
   119         val birth = Timer.checkRealTimer timer
   120 
   121         val filter_result as {outcome, ...} =
   122           SMT2_Solver.smt2_filter ctxt goal facts i slice_timeout
   123           handle exn =>
   124             if Exn.is_interrupt exn orelse debug then
   125               reraise exn
   126             else
   127               {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
   128                fact_ids = [], atp_proof = K []}
   129 
   130         val death = Timer.checkRealTimer timer
   131         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   132         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   133         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   134 
   135         val too_many_facts_perhaps =
   136           (case outcome of
   137             NONE => false
   138           | SOME (SMT2_Failure.Counterexample _) => false
   139           | SOME SMT2_Failure.Time_Out => slice_timeout <> timeout
   140           | SOME (SMT2_Failure.Abnormal_Termination _) => true (* kind of *)
   141           | SOME SMT2_Failure.Out_Of_Memory => true
   142           | SOME (SMT2_Failure.Other_Failure _) => true)
   143       in
   144         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   145            Time.> (timeout, Time.zeroTime) then
   146           let
   147             val new_num_facts =
   148               Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts)
   149             val factss as (new_fact_filter, _) :: _ =
   150               factss
   151               |> (fn (x :: xs) => xs @ [x])
   152               |> app_hd (apsnd (take new_num_facts))
   153             val show_filter = fact_filter <> new_fact_filter
   154 
   155             fun num_of_facts fact_filter num_facts =
   156               string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
   157               " fact" ^ plural_s num_facts
   158 
   159             val _ =
   160               if debug then
   161                 quote name ^ " invoked with " ^
   162                 num_of_facts fact_filter num_facts ^ ": " ^
   163                 string_of_atp_failure (failure_of_smt2_failure (the outcome)) ^
   164                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   165                 "..."
   166                 |> Output.urgent_message
   167               else
   168                 ()
   169           in
   170             do_slice timeout (slice + 1) outcome0 time_so_far factss
   171           end
   172         else
   173           {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
   174            used_from = facts, run_time = time_so_far}
   175       end
   176   in
   177     do_slice timeout 1 NONE Time.zeroTime
   178   end
   179 
   180 fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
   181       try0_isar, smt_proofs, minimize, preplay_timeout, ...})
   182     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   183   let
   184     val thy = Proof.theory_of state
   185     val ctxt = Proof.context_of state
   186 
   187     val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
   188 
   189     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
   190       smt2_filter_loop name params state goal subgoal factss
   191     val used_named_facts = map snd fact_ids
   192     val used_facts = map fst used_named_facts
   193     val outcome = Option.map failure_of_smt2_failure outcome
   194 
   195     val (preplay, message, message_tail) =
   196       (case outcome of
   197         NONE =>
   198         (Lazy.lazy (fn () =>
   199            play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
   200              SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
   201          fn preplay =>
   202             let
   203               fun isar_params () =
   204                 (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
   205                  minimize <> SOME false, atp_proof (), goal)
   206 
   207               val one_line_params =
   208                 (preplay, proof_banner mode name, used_facts,
   209                  choose_minimize_command thy params minimize_command name preplay, subgoal,
   210                  subgoal_count)
   211               val num_chained = length (#facts (Proof.goal state))
   212             in
   213               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
   214             end,
   215          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
   216       | SOME failure =>
   217         (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
   218          fn _ => string_of_atp_failure failure, ""))
   219   in
   220     {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   221      preplay = preplay, message = message, message_tail = message_tail}
   222   end
   223 
   224 end;