src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author wenzelm
Thu Mar 27 17:12:40 2014 +0100 (2014-03-27 ago)
changeset 56303 4cc3f4db3447
parent 56081 72fad75baf7e
child 56985 82c83978fbd9
permissions -rw-r--r--
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
     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_weights : bool Config.T
    18   val smt_weight_min_facts : int Config.T
    19   val smt_min_weight : int Config.T
    20   val smt_max_weight : int Config.T
    21   val smt_max_weight_index : int Config.T
    22   val smt_weight_curve : (int -> int) Unsynchronized.ref
    23   val smt_max_slices : int Config.T
    24   val smt_slice_fact_frac : real Config.T
    25   val smt_slice_time_frac : real Config.T
    26   val smt_slice_min_secs : int Config.T
    27 
    28   val is_smt_prover : Proof.context -> string -> bool
    29   val run_smt_solver : mode -> string -> prover
    30 end;
    31 
    32 structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
    33 struct
    34 
    35 open ATP_Util
    36 open ATP_Proof
    37 open ATP_Systems
    38 open ATP_Problem_Generate
    39 open ATP_Proof_Reconstruct
    40 open Sledgehammer_Util
    41 open Sledgehammer_Proof_Methods
    42 open Sledgehammer_Prover
    43 
    44 val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)
    45 val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    46 val smt_weights = Attrib.setup_config_bool @{binding sledgehammer_smt_weights} (K true)
    47 val smt_weight_min_facts =
    48   Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
    49 
    50 fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
    51 
    52 (* FUDGE *)
    53 val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
    54 val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
    55 val smt_max_weight_index =
    56   Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
    57 val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
    58 
    59 fun smt_fact_weight ctxt j num_facts =
    60   if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
    61     let
    62       val min = Config.get ctxt smt_min_weight
    63       val max = Config.get ctxt smt_max_weight
    64       val max_index = Config.get ctxt smt_max_weight_index
    65       val curve = !smt_weight_curve
    66     in
    67       SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
    68     end
    69   else
    70     NONE
    71 
    72 fun weight_smt_fact ctxt num_facts ((info, th), j) =
    73   let val thy = Proof_Context.theory_of ctxt in
    74     (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
    75   end
    76 
    77 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
    78    properly in the SMT module, we must interpret these here. *)
    79 val z3_failures =
    80   [(101, OutOfResources),
    81    (103, MalformedInput),
    82    (110, MalformedInput),
    83    (112, TimedOut)]
    84 val unix_failures =
    85   [(138, Crashed),
    86    (139, Crashed)]
    87 val smt_failures = z3_failures @ unix_failures
    88 
    89 fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
    90     if is_real_cex then Unprovable else GaveUp
    91   | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
    92   | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
    93     (case AList.lookup (op =) smt_failures code of
    94       SOME failure => failure
    95     | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
    96   | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
    97   | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
    98 
    99 (* FUDGE *)
   100 val smt_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt_max_slices} (K 8)
   101 val smt_slice_fact_frac =
   102   Attrib.setup_config_real @{binding sledgehammer_smt_slice_fact_frac} (K 0.667)
   103 val smt_slice_time_frac =
   104   Attrib.setup_config_real @{binding sledgehammer_smt_slice_time_frac} (K 0.333)
   105 val smt_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt_slice_min_secs} (K 3)
   106 
   107 val is_boring_builtin_typ =
   108   not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
   109 
   110 fun smt_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
   111       ...} : params) state goal i =
   112   let
   113     fun repair_context ctxt =
   114       ctxt |> Context.proof_map (SMT_Config.select_solver name)
   115            |> Config.put SMT_Config.verbose debug
   116            |> (if overlord then
   117                  Config.put SMT_Config.debug_files
   118                    (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
   119                else
   120                  I)
   121            |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers)
   122            |> not (Config.get ctxt smt_builtins)
   123               ? (SMT_Builtin.filter_builtins is_boring_builtin_typ
   124                  #> Config.put SMT_Config.datatypes false)
   125            |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
   126                 default_max_new_mono_instances
   127 
   128     val state = Proof.map_context (repair_context) state
   129     val ctxt = Proof.context_of state
   130     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
   131 
   132     fun do_slice timeout slice outcome0 time_so_far
   133         (weighted_factss as (fact_filter, weighted_facts) :: _) =
   134       let
   135         val timer = Timer.startRealTimer ()
   136         val slice_timeout =
   137           if slice < max_slices then
   138             let val ms = Time.toMilliseconds timeout in
   139               Int.min (ms, Int.max (1000 * Config.get ctxt smt_slice_min_secs,
   140                 Real.ceil (Config.get ctxt smt_slice_time_frac * Real.fromInt ms)))
   141               |> Time.fromMilliseconds
   142             end
   143           else
   144             timeout
   145         val num_facts = length weighted_facts
   146         val _ =
   147           if debug then
   148             quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
   149             " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
   150             |> Output.urgent_message
   151           else
   152             ()
   153         val birth = Timer.checkRealTimer timer
   154         val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
   155 
   156         val (outcome, used_facts) =
   157           SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
   158           |> SMT_Solver.smt_filter_apply slice_timeout
   159           |> (fn {outcome, used_facts} => (outcome, used_facts))
   160           handle exn =>
   161             if Exn.is_interrupt exn then reraise exn
   162             else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
   163 
   164         val death = Timer.checkRealTimer timer
   165         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   166         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   167 
   168         val too_many_facts_perhaps =
   169           (case outcome of
   170             NONE => false
   171           | SOME (SMT_Failure.Counterexample _) => false
   172           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   173           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   174           | SOME SMT_Failure.Out_Of_Memory => true
   175           | SOME (SMT_Failure.Other_Failure _) => true)
   176 
   177         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   178       in
   179         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   180            Time.> (timeout, Time.zeroTime) then
   181           let
   182             val new_num_facts =
   183               Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
   184             val weighted_factss as (new_fact_filter, _) :: _ =
   185               weighted_factss
   186               |> (fn (x :: xs) => xs @ [x])
   187               |> app_hd (apsnd (take new_num_facts))
   188             val show_filter = fact_filter <> new_fact_filter
   189 
   190             fun num_of_facts fact_filter num_facts =
   191               string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
   192               " fact" ^ plural_s num_facts
   193 
   194             val _ =
   195               if debug then
   196                 quote name ^ " invoked with " ^
   197                 num_of_facts fact_filter num_facts ^ ": " ^
   198                 string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   199                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   200                 "..."
   201                 |> Output.urgent_message
   202               else
   203                 ()
   204           in
   205             do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
   206           end
   207         else
   208           {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
   209            used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
   210       end
   211   in
   212     do_slice timeout 1 NONE Time.zeroTime
   213   end
   214 
   215 fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
   216     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   217   let
   218     val thy = Proof.theory_of state
   219     val ctxt = Proof.context_of state
   220 
   221     fun weight_facts facts =
   222       let val num_facts = length facts in
   223         map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
   224       end
   225 
   226     val weighted_factss = factss |> map (apsnd weight_facts)
   227     val {outcome, used_facts = used_pairs, used_from, run_time} =
   228       smt_filter_loop name params state goal subgoal weighted_factss
   229     val used_facts = used_pairs |> map fst
   230     val outcome = outcome |> Option.map failure_of_smt_failure
   231 
   232     val (preplay, message, message_tail) =
   233       (case outcome of
   234         NONE =>
   235         (Lazy.lazy (fn () =>
   236            play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
   237              SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
   238          fn preplay =>
   239             let
   240               val one_line_params =
   241                 (preplay, proof_banner mode name, used_facts,
   242                  choose_minimize_command thy params minimize_command name preplay, subgoal,
   243                  subgoal_count)
   244               val num_chained = length (#facts (Proof.goal state))
   245             in
   246               one_line_proof_text num_chained one_line_params
   247             end,
   248          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
   249       | SOME failure =>
   250         (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
   251          fn _ => string_of_atp_failure failure, ""))
   252   in
   253     {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   254      preplay = preplay, message = message, message_tail = message_tail}
   255   end
   256 
   257 end;