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
6SMT solvers as Sledgehammer provers.
7*)
8
9signature SLEDGEHAMMER_PROVER_SMT =
10sig
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
24end;
25
26structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
27struct
28
29open ATP_Util
30open ATP_Proof
31open ATP_Systems
32open ATP_Problem_Generate
33open ATP_Proof_Reconstruct
34open Sledgehammer_Util
35open Sledgehammer_Proof_Methods
36open Sledgehammer_Isar
37open Sledgehammer_Prover
38
39val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true)
40val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true)
41
42val 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. *)
46val z3_failures =
47  [(101, OutOfResources),
48   (103, MalformedInput),
49   (110, MalformedInput),
50   (112, TimedOut)]
51val unix_failures =
52  [(134, Crashed),
53   (138, Crashed),
54   (139, Crashed)]
55val smt_failures = z3_failures @ unix_failures
56
57fun 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 *)
68val smt_max_slices = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_max_slices\<close> (K 8)
69val smt_slice_fact_frac =
70  Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_fact_frac\<close> (K 0.667)
71val smt_slice_time_frac =
72  Attrib.setup_config_real \<^binding>\<open>sledgehammer_smt_slice_time_frac\<close> (K 0.333)
73val smt_slice_min_secs = Attrib.setup_config_int \<^binding>\<open>sledgehammer_smt_slice_min_secs\<close> (K 3)
74
75val is_boring_builtin_typ =
76  not o exists_subtype (member (op =) [\<^typ>\<open>nat\<close>, \<^typ>\<open>int\<close>, HOLogic.realT])
77
78fun 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_so_far + (death - birth)
134        val timeout = 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           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
181fun 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
230end;
231