src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 58061 3d060f43accb
parent 57776 1111a9a328fe
child 58498 59bdd4f57255
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,224 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
     1.5 +    Author:     Fabian Immler, TU Muenchen
     1.6 +    Author:     Makarius
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8 +
     1.9 +SMT solvers as Sledgehammer provers.
    1.10 +*)
    1.11 +
    1.12 +signature SLEDGEHAMMER_PROVER_SMT =
    1.13 +sig
    1.14 +  type stature = ATP_Problem_Generate.stature
    1.15 +  type mode = Sledgehammer_Prover.mode
    1.16 +  type prover = Sledgehammer_Prover.prover
    1.17 +
    1.18 +  val smt_builtins : bool Config.T
    1.19 +  val smt_triggers : bool Config.T
    1.20 +  val smt_max_slices : int Config.T
    1.21 +  val smt_slice_fact_frac : real Config.T
    1.22 +  val smt_slice_time_frac : real Config.T
    1.23 +  val smt_slice_min_secs : int Config.T
    1.24 +
    1.25 +  val is_smt_prover : Proof.context -> string -> bool
    1.26 +  val run_smt_solver : mode -> string -> prover
    1.27 +end;
    1.28 +
    1.29 +structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
    1.30 +struct
    1.31 +
    1.32 +open ATP_Util
    1.33 +open ATP_Proof
    1.34 +open ATP_Systems
    1.35 +open ATP_Problem_Generate
    1.36 +open ATP_Proof_Reconstruct
    1.37 +open Sledgehammer_Util
    1.38 +open Sledgehammer_Proof_Methods
    1.39 +open Sledgehammer_Isar
    1.40 +open Sledgehammer_Prover
    1.41 +
    1.42 +val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
    1.43 +val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    1.44 +
    1.45 +val is_smt_prover = member (op =) o SMT_Config.available_solvers_of
    1.46 +
    1.47 +(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    1.48 +   properly in the SMT module, we must interpret these here. *)
    1.49 +val z3_failures =
    1.50 +  [(101, OutOfResources),
    1.51 +   (103, MalformedInput),
    1.52 +   (110, MalformedInput),
    1.53 +   (112, TimedOut)]
    1.54 +val unix_failures =
    1.55 +  [(138, Crashed),
    1.56 +   (139, Crashed)]
    1.57 +val smt_failures = z3_failures @ unix_failures
    1.58 +
    1.59 +fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) =
    1.60 +    if genuine then Unprovable else GaveUp
    1.61 +  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
    1.62 +  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
    1.63 +    (case AList.lookup (op =) smt_failures code of
    1.64 +      SOME failure => failure
    1.65 +    | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
    1.66 +  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
    1.67 +  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
    1.68 +
    1.69 +(* FUDGE *)
    1.70 +val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
    1.71 +val smt_slice_fact_frac =
    1.72 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
    1.73 +val smt_slice_time_frac =
    1.74 +  Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
    1.75 +val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
    1.76 +
    1.77 +val is_boring_builtin_typ =
    1.78 +  not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
    1.79 +
    1.80 +fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
    1.81 +      ...} : params) state goal i =
    1.82 +  let
    1.83 +    fun repair_context ctxt =
    1.84 +      ctxt |> Context.proof_map (SMT_Config.select_solver name)
    1.85 +           |> Config.put SMT_Config.verbose debug
    1.86 +           |> (if overlord then
    1.87 +                 Config.put SMT_Config.debug_files
    1.88 +                   (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
    1.89 +               else
    1.90 +                 I)
    1.91 +           |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
    1.92 +           |> not (Config.get ctxt smt_builtins)
    1.93 +              ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
    1.94 +                 #> Config.put SMT_Systems.z3_extensions false)
    1.95 +           |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
    1.96 +                default_max_new_mono_instances
    1.97 +
    1.98 +    val state = Proof.map_context (repair_context) state
    1.99 +    val ctxt = Proof.context_of state
   1.100 +    val max_slices = if slice then Config.get ctxt smt_max_slices else 1
   1.101 +
   1.102 +    fun do_slice timeout slice outcome0 time_so_far (factss as (fact_filter, facts) :: _) =
   1.103 +      let
   1.104 +        val timer = Timer.startRealTimer ()
   1.105 +        val slice_timeout =
   1.106 +          if slice < max_slices then
   1.107 +            let val ms = Time.toMilliseconds timeout in
   1.108 +              Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   1.109 +                Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
   1.110 +              |> Time.fromMilliseconds
   1.111 +            end
   1.112 +          else
   1.113 +            timeout
   1.114 +        val num_facts = length facts
   1.115 +        val _ =
   1.116 +          if debug then
   1.117 +            quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
   1.118 +            " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
   1.119 +            |> Output.urgent_message
   1.120 +          else
   1.121 +            ()
   1.122 +        val birth = Timer.checkRealTimer timer
   1.123 +
   1.124 +        val filter_result as {outcome, ...} =
   1.125 +          SMT_Solver.smt_filter ctxt goal facts i slice_timeout
   1.126 +          handle exn =>
   1.127 +            if Exn.is_interrupt exn orelse debug then
   1.128 +              reraise exn
   1.129 +            else
   1.130 +              {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
   1.131 +               fact_ids = [], atp_proof = K []}
   1.132 +
   1.133 +        val death = Timer.checkRealTimer timer
   1.134 +        val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   1.135 +        val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   1.136 +        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   1.137 +
   1.138 +        val too_many_facts_perhaps =
   1.139 +          (case outcome of
   1.140 +            NONE => false
   1.141 +          | SOME (SMT_Failure.Counterexample _) => false
   1.142 +          | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   1.143 +          | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   1.144 +          | SOME SMT_Failure.Out_Of_Memory => true
   1.145 +          | SOME (SMT_Failure.Other_Failure _) => true)
   1.146 +      in
   1.147 +        if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   1.148 +           Time.> (timeout, Time.zeroTime) then
   1.149 +          let
   1.150 +            val new_num_facts =
   1.151 +              Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
   1.152 +            val factss as (new_fact_filter, _) :: _ =
   1.153 +              factss
   1.154 +              |> (fn (x :: xs) => xs @ [x])
   1.155 +              |> app_hd (apsnd (take new_num_facts))
   1.156 +            val show_filter = fact_filter <> new_fact_filter
   1.157 +
   1.158 +            fun num_of_facts fact_filter num_facts =
   1.159 +              string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
   1.160 +              " fact" ^ plural_s num_facts
   1.161 +
   1.162 +            val _ =
   1.163 +              if debug then
   1.164 +                quote name ^ " invoked with " ^
   1.165 +                num_of_facts fact_filter num_facts ^ ": " ^
   1.166 +                string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   1.167 +                " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   1.168 +                "..."
   1.169 +                |> Output.urgent_message
   1.170 +              else
   1.171 +                ()
   1.172 +          in
   1.173 +            do_slice timeout (slice + 1) outcome0 time_so_far factss
   1.174 +          end
   1.175 +        else
   1.176 +          {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
   1.177 +           used_from = facts, run_time = time_so_far}
   1.178 +      end
   1.179 +  in
   1.180 +    do_slice timeout 1 NONE Time.zeroTime
   1.181 +  end
   1.182 +
   1.183 +fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs,
   1.184 +      minimize, preplay_timeout, ...})
   1.185 +    ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   1.186 +  let
   1.187 +    val thy = Proof.theory_of state
   1.188 +    val ctxt = Proof.context_of state
   1.189 +
   1.190 +    val factss = map (apsnd (map (apsnd (Thm.transfer thy)))) factss
   1.191 +
   1.192 +    val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
   1.193 +      smt_filter_loop name params state goal subgoal factss
   1.194 +    val used_named_facts = map snd fact_ids
   1.195 +    val used_facts = sort_wrt fst (map fst used_named_facts)
   1.196 +    val outcome = Option.map failure_of_smt_failure outcome
   1.197 +
   1.198 +    val (preferred_methss, message) =
   1.199 +      (case outcome of
   1.200 +        NONE =>
   1.201 +        let
   1.202 +          val preferred_methss =
   1.203 +            (SMT_Method, bunches_of_proof_methods try0 (smt_proofs <> SOME false) false liftingN)
   1.204 +        in
   1.205 +          (preferred_methss,
   1.206 +           fn preplay =>
   1.207 +             let
   1.208 +               val _ = if verbose then Output.urgent_message "Generating proof text..." else ()
   1.209 +
   1.210 +               fun isar_params () =
   1.211 +                 (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
   1.212 +                  goal)
   1.213 +
   1.214 +               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
   1.215 +               val num_chained = length (#facts (Proof.goal state))
   1.216 +             in
   1.217 +               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
   1.218 +                 one_line_params
   1.219 +             end)
   1.220 +        end
   1.221 +      | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))
   1.222 +  in
   1.223 +    {outcome = outcome, used_facts = used_facts, used_from = used_from,
   1.224 +     preferred_methss = preferred_methss, run_time = run_time, message = message}
   1.225 +  end
   1.226 +
   1.227 +end;