src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
author blanchet
Thu Jun 12 17:02:03 2014 +0200 (2014-06-12 ago)
changeset 57243 8c261f0a9b32
parent 57078 a91d126338a4
permissions -rw-r--r--
reintroduced vital 'Thm.transfer'
     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))
    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 
   155         val (outcome, used_facts) =
   156           SMT_Solver.smt_filter_preprocess ctxt [] goal weighted_facts i
   157           |> SMT_Solver.smt_filter_apply slice_timeout
   158           |> (fn {outcome, used_facts} => (outcome, used_facts))
   159           handle exn =>
   160             if Exn.is_interrupt exn then reraise exn
   161             else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
   162 
   163         val death = Timer.checkRealTimer timer
   164         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
   165         val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
   166 
   167         val too_many_facts_perhaps =
   168           (case outcome of
   169             NONE => false
   170           | SOME (SMT_Failure.Counterexample _) => false
   171           | SOME SMT_Failure.Time_Out => slice_timeout <> timeout
   172           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
   173           | SOME SMT_Failure.Out_Of_Memory => true
   174           | SOME (SMT_Failure.Other_Failure _) => true)
   175 
   176         val timeout = Time.- (timeout, Timer.checkRealTimer timer)
   177       in
   178         if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
   179            Time.> (timeout, Time.zeroTime) then
   180           let
   181             val new_num_facts =
   182               Real.ceil (Config.get ctxt smt_slice_fact_frac * Real.fromInt num_facts)
   183             val weighted_factss as (new_fact_filter, _) :: _ =
   184               weighted_factss
   185               |> (fn (x :: xs) => xs @ [x])
   186               |> app_hd (apsnd (take new_num_facts))
   187             val show_filter = fact_filter <> new_fact_filter
   188 
   189             fun num_of_facts fact_filter num_facts =
   190               string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
   191               " fact" ^ plural_s num_facts
   192 
   193             val _ =
   194               if debug then
   195                 quote name ^ " invoked with " ^
   196                 num_of_facts fact_filter num_facts ^ ": " ^
   197                 string_of_atp_failure (failure_of_smt_failure (the outcome)) ^
   198                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   199                 "..."
   200                 |> Output.urgent_message
   201               else
   202                 ()
   203           in
   204             do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
   205           end
   206         else
   207           {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
   208            used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
   209       end
   210   in
   211     do_slice timeout 1 NONE Time.zeroTime
   212   end
   213 
   214 fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
   215     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   216   let
   217     val thy = Proof.theory_of state
   218     val ctxt = Proof.context_of state
   219 
   220     fun weight_facts facts =
   221       let val num_facts = length facts in
   222         map (weight_smt_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
   223       end
   224 
   225     val weighted_factss = factss |> map (apsnd weight_facts)
   226     val {outcome, used_facts = used_pairs, used_from, run_time} =
   227       smt_filter_loop name params state goal subgoal weighted_factss
   228     val used_facts = used_pairs |> map fst
   229     val outcome = outcome |> Option.map failure_of_smt_failure
   230 
   231     val (preplay, message, message_tail) =
   232       (case outcome of
   233         NONE =>
   234         (Lazy.lazy (fn () =>
   235            play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal
   236              SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
   237          fn preplay =>
   238             let
   239               val one_line_params =
   240                 (preplay, proof_banner mode name, used_facts,
   241                  choose_minimize_command thy params minimize_command name preplay, subgoal,
   242                  subgoal_count)
   243               val num_chained = length (#facts (Proof.goal state))
   244             in
   245               one_line_proof_text ctxt num_chained one_line_params
   246             end,
   247          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
   248       | SOME failure =>
   249         (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
   250          fn _ => string_of_atp_failure failure, ""))
   251   in
   252     {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   253      preplay = preplay, message = message, message_tail = message_tail}
   254   end
   255 
   256 end;