make Sledgehammer minimizer fully work with SMT
authorblanchet
Fri Oct 22 11:11:34 2010 +0200 (2010-10-22 ago)
changeset 40062cfaebaa8588f
parent 40061 71cc5aac8b76
child 40063 d086e3699e78
make Sledgehammer minimizer fully work with SMT
NEWS
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
     1.1 --- a/NEWS	Fri Oct 22 09:50:18 2010 +0200
     1.2 +++ b/NEWS	Fri Oct 22 11:11:34 2010 +0200
     1.3 @@ -296,7 +296,7 @@
     1.4      INCOMPATIBILITY.
     1.5    - Renamed options:
     1.6      sledgehammer [atps = ...] ~> sledgehammer [provers = ...]
     1.7 -    sledgehammer [atp = ...] ~> sledgehammer [provers = ...]
     1.8 +    sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
     1.9      INCOMPATIBILITY.
    1.10  
    1.11  
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 09:50:18 2010 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Oct 22 11:11:34 2010 +0200
     2.3 @@ -29,8 +29,8 @@
     2.4    lemmas: int,
     2.5    max_lems: int,
     2.6    time_isa: int,
     2.7 -  time_atp: int,
     2.8 -  time_atp_fail: int}
     2.9 +  time_prover: int,
    2.10 +  time_prover_fail: int}
    2.11  
    2.12  datatype me_data = MeData of {
    2.13    calls: int,
    2.14 @@ -51,10 +51,11 @@
    2.15  
    2.16  fun make_sh_data
    2.17        (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,
    2.18 -       time_atp,time_atp_fail) =
    2.19 +       time_prover,time_prover_fail) =
    2.20    ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,
    2.21           nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,
    2.22 -         time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
    2.23 +         time_isa=time_isa, time_prover=time_prover,
    2.24 +         time_prover_fail=time_prover_fail}
    2.25  
    2.26  fun make_min_data (succs, ab_ratios) =
    2.27    MinData{succs=succs, ab_ratios=ab_ratios}
    2.28 @@ -71,8 +72,8 @@
    2.29  
    2.30  fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
    2.31                                lemmas, max_lems, time_isa,
    2.32 -  time_atp, time_atp_fail}) = (calls, success, nontriv_calls, nontriv_success,
    2.33 -  lemmas, max_lems, time_isa, time_atp, time_atp_fail)
    2.34 +  time_prover, time_prover_fail}) = (calls, success, nontriv_calls,
    2.35 +  nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)
    2.36  
    2.37  fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
    2.38  
    2.39 @@ -127,40 +128,40 @@
    2.40  fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
    2.41  
    2.42  val inc_sh_calls =  map_sh_data
    2.43 -  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
    2.44 -    => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
    2.45 +  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
    2.46 +    => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
    2.47  
    2.48  val inc_sh_success = map_sh_data
    2.49 -  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
    2.50 -    => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
    2.51 +  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
    2.52 +    => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
    2.53  
    2.54  val inc_sh_nontriv_calls =  map_sh_data
    2.55 -  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
    2.56 -    => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail))
    2.57 +  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
    2.58 +    => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))
    2.59  
    2.60  val inc_sh_nontriv_success = map_sh_data
    2.61 -  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_atp, time_atp_fail)
    2.62 -    => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_atp, time_atp_fail))
    2.63 +  (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)
    2.64 +    => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))
    2.65  
    2.66  fun inc_sh_lemmas n = map_sh_data
    2.67 -  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
    2.68 -    => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_atp,time_atp_fail))
    2.69 +  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
    2.70 +    => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))
    2.71  
    2.72  fun inc_sh_max_lems n = map_sh_data
    2.73 -  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
    2.74 -    => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_atp,time_atp_fail))
    2.75 +  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
    2.76 +    => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))
    2.77  
    2.78  fun inc_sh_time_isa t = map_sh_data
    2.79 -  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
    2.80 -    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_atp,time_atp_fail))
    2.81 +  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
    2.82 +    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))
    2.83  
    2.84 -fun inc_sh_time_atp t = map_sh_data
    2.85 -  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
    2.86 -    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp + t,time_atp_fail))
    2.87 +fun inc_sh_time_prover t = map_sh_data
    2.88 +  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
    2.89 +    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))
    2.90  
    2.91 -fun inc_sh_time_atp_fail t = map_sh_data
    2.92 -  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail)
    2.93 -    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
    2.94 +fun inc_sh_time_prover_fail t = map_sh_data
    2.95 +  (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)
    2.96 +    => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))
    2.97  
    2.98  val inc_min_succs = map_min_data
    2.99    (fn (succs,ab_ratios) => (succs+1, ab_ratios))
   2.100 @@ -214,7 +215,7 @@
   2.101    if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
   2.102  
   2.103  fun log_sh_data log
   2.104 -    (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_atp, time_atp_fail) =
   2.105 +    (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =
   2.106   (log ("Total number of sledgehammer calls: " ^ str calls);
   2.107    log ("Number of successful sledgehammer calls: " ^ str success);
   2.108    log ("Number of sledgehammer lemmas: " ^ str lemmas);
   2.109 @@ -223,14 +224,14 @@
   2.110    log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);
   2.111    log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);
   2.112    log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));
   2.113 -  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_atp));
   2.114 -  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_atp_fail));
   2.115 +  log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));
   2.116 +  log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));
   2.117    log ("Average time for sledgehammer calls (Isabelle): " ^
   2.118      str3 (avg_time time_isa calls));
   2.119    log ("Average time for successful sledgehammer calls (ATP): " ^
   2.120 -    str3 (avg_time time_atp success));
   2.121 +    str3 (avg_time time_prover success));
   2.122    log ("Average time for failed sledgehammer calls (ATP): " ^
   2.123 -    str3 (avg_time time_atp_fail (calls - success)))
   2.124 +    str3 (avg_time time_prover_fail (calls - success)))
   2.125    )
   2.126  
   2.127  
   2.128 @@ -313,16 +314,16 @@
   2.129  fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
   2.130  
   2.131  
   2.132 -fun get_atp thy args =
   2.133 +fun get_prover thy args =
   2.134    let
   2.135 -    fun default_atp_name () =
   2.136 +    fun default_prover_name () =
   2.137        hd (#provers (Sledgehammer_Isar.default_params thy []))
   2.138        handle Empty => error "No ATP available."
   2.139 -    fun get_atp name = (name, Sledgehammer.run_atp thy name)
   2.140 +    fun get_prover name = (name, Sledgehammer.get_prover thy name)
   2.141    in
   2.142      (case AList.lookup (op =) args proverK of
   2.143 -      SOME name => get_atp name
   2.144 -    | NONE => get_atp (default_atp_name ()))
   2.145 +      SOME name => get_prover name
   2.146 +    | NONE => get_prover (default_prover_name ()))
   2.147    end
   2.148  
   2.149  type locality = Sledgehammer_Filter.locality
   2.150 @@ -349,7 +350,11 @@
   2.151        Sledgehammer_Isar.default_params thy
   2.152            [("timeout", Int.toString timeout ^ " s")]
   2.153      val relevance_override = {add = [], del = [], only = false}
   2.154 -    val {default_max_relevant, ...} = ATP_Systems.get_atp thy prover_name
   2.155 +    val default_max_relevant =
   2.156 +      if member (op =) Sledgehammer.smt_prover_names prover_name then
   2.157 +        Sledgehammer.smt_default_max_relevant
   2.158 +      else
   2.159 +        #default_max_relevant (ATP_Systems.get_atp thy prover_name)
   2.160      val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
   2.161      val axioms =
   2.162        Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
   2.163 @@ -362,14 +367,14 @@
   2.164        (case hard_timeout of
   2.165          NONE => I
   2.166        | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
   2.167 -    val ({outcome, message, used_axioms, run_time_in_msecs = time_atp, ...}
   2.168 +    val ({outcome, message, used_axioms, run_time_in_msecs = SOME time_prover, ...}
   2.169           : Sledgehammer.prover_result,
   2.170          time_isa) = time_limit (Mirabelle.cpu_time
   2.171                        (prover params (K ""))) problem
   2.172    in
   2.173      case outcome of
   2.174 -      NONE => (message, SH_OK (time_isa, time_atp, used_axioms))
   2.175 -    | SOME _ => (message, SH_FAIL (time_isa, time_atp))
   2.176 +      NONE => (message, SH_OK (time_isa, time_prover, used_axioms))
   2.177 +    | SOME _ => (message, SH_FAIL (time_isa, time_prover))
   2.178    end
   2.179    handle ERROR msg => ("error: " ^ msg, SH_ERROR)
   2.180         | TimeLimit.TimeOut => ("timeout", SH_ERROR)
   2.181 @@ -394,7 +399,7 @@
   2.182      val triv_str = if trivial then "[T] " else ""
   2.183      val _ = change_data id inc_sh_calls
   2.184      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
   2.185 -    val (prover_name, prover) = get_atp (Proof.theory_of st) args
   2.186 +    val (prover_name, prover) = get_prover (Proof.theory_of st) args
   2.187      val dir = AList.lookup (op =) args keepK
   2.188      val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
   2.189      val hard_timeout = AList.lookup (op =) args prover_hard_timeoutK
   2.190 @@ -402,7 +407,7 @@
   2.191      val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
   2.192    in
   2.193      case result of
   2.194 -      SH_OK (time_isa, time_atp, names) =>
   2.195 +      SH_OK (time_isa, time_prover, names) =>
   2.196          let
   2.197            fun get_thms (_, Sledgehammer_Filter.Chained) = NONE
   2.198              | get_thms (name, loc) =
   2.199 @@ -413,15 +418,15 @@
   2.200            change_data id (inc_sh_lemmas (length names));
   2.201            change_data id (inc_sh_max_lems (length names));
   2.202            change_data id (inc_sh_time_isa time_isa);
   2.203 -          change_data id (inc_sh_time_atp time_atp);
   2.204 +          change_data id (inc_sh_time_prover time_prover);
   2.205            named_thms := SOME (map_filter get_thms names);
   2.206            log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
   2.207 -            string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
   2.208 +            string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
   2.209          end
   2.210 -    | SH_FAIL (time_isa, time_atp) =>
   2.211 +    | SH_FAIL (time_isa, time_prover) =>
   2.212          let
   2.213            val _ = change_data id (inc_sh_time_isa time_isa)
   2.214 -          val _ = change_data id (inc_sh_time_atp_fail time_atp)
   2.215 +          val _ = change_data id (inc_sh_time_prover_fail time_prover)
   2.216          in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
   2.217      | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
   2.218    end
   2.219 @@ -436,7 +441,7 @@
   2.220      open Metis_Translate
   2.221      val thy = Proof.theory_of st
   2.222      val n0 = length (these (!named_thms))
   2.223 -    val (prover_name, _) = get_atp thy args
   2.224 +    val (prover_name, _) = get_prover thy args
   2.225      val timeout =
   2.226        AList.lookup (op =) args minimize_timeoutK
   2.227        |> Option.map (fst o read_int o explode)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 09:50:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Oct 22 11:11:34 2010 +0200
     3.3 @@ -42,13 +42,15 @@
     3.4  
     3.5    type prover_result =
     3.6      {outcome: failure option,
     3.7 -     message: string,
     3.8       used_axioms: (string * locality) list,
     3.9 -     run_time_in_msecs: int}
    3.10 +     run_time_in_msecs: int option,
    3.11 +     message: string}
    3.12  
    3.13    type prover = params -> minimize_command -> prover_problem -> prover_result
    3.14  
    3.15    val smtN : string
    3.16 +  val smt_prover_names : string list
    3.17 +  val smt_default_max_relevant : int
    3.18    val dest_dir : string Config.T
    3.19    val problem_prefix : string Config.T
    3.20    val measure_run_time : bool Config.T
    3.21 @@ -56,11 +58,7 @@
    3.22    val kill_provers : unit -> unit
    3.23    val running_provers : unit -> unit
    3.24    val messages : int option -> unit
    3.25 -  val run_atp : theory -> string -> prover
    3.26 -  val is_smt_solver_installed : unit -> bool
    3.27 -  val run_smt_solver :
    3.28 -    bool -> params -> minimize_command -> prover_problem
    3.29 -    -> string * (string * locality) list
    3.30 +  val get_prover : theory -> string -> prover
    3.31    val run_sledgehammer :
    3.32      params -> bool -> int -> relevance_override -> (string -> minimize_command)
    3.33      -> Proof.state -> bool * Proof.state
    3.34 @@ -87,12 +85,15 @@
    3.35  val das_Tool = "Sledgehammer"
    3.36  
    3.37  val smtN = "smt"
    3.38 -val smt_names = [smtN, remote_prefix ^ smtN]
    3.39 +val smt_prover_names = [smtN, remote_prefix ^ smtN]
    3.40 +
    3.41 +val smt_default_max_relevant = 300 (* FUDGE *)
    3.42 +val auto_max_relevant_divisor = 2 (* FUDGE *)
    3.43  
    3.44  fun available_provers thy =
    3.45    let
    3.46      val (remote_provers, local_provers) =
    3.47 -      sort_strings (available_atps thy) @ smt_names
    3.48 +      sort_strings (available_atps thy) @ smt_prover_names
    3.49        |> List.partition (String.isPrefix remote_prefix)
    3.50    in
    3.51      priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
    3.52 @@ -135,7 +136,7 @@
    3.53    {outcome: failure option,
    3.54     message: string,
    3.55     used_axioms: (string * locality) list,
    3.56 -   run_time_in_msecs: int}
    3.57 +   run_time_in_msecs: int option}
    3.58  
    3.59  type prover = params -> minimize_command -> prover_problem -> prover_result
    3.60  
    3.61 @@ -180,6 +181,9 @@
    3.62  fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
    3.63    | prepared_axiom _ (Prepared p) = p
    3.64  
    3.65 +fun int_option_add (SOME m) (SOME n) = SOME (m + n)
    3.66 +  | int_option_add _ _ = NONE
    3.67 +
    3.68  (* Important messages are important but not so important that users want to see
    3.69     them each time. *)
    3.70  val important_message_keep_factor = 0.1
    3.71 @@ -232,7 +236,7 @@
    3.72          val digit = Scan.one Symbol.is_ascii_digit;
    3.73          val num3 = as_num (digit ::: digit ::: (digit >> single));
    3.74          val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
    3.75 -        val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
    3.76 +        val as_time = Scan.read Symbol.stopper time o explode
    3.77        in (output, as_time t) end;
    3.78      fun run_on probfile =
    3.79        case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
    3.80 @@ -250,7 +254,7 @@
    3.81                           prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
    3.82                         else
    3.83                           I)
    3.84 -                  |>> (if measure_run_time then split_time else rpair 0)
    3.85 +                  |>> (if measure_run_time then split_time else rpair NONE)
    3.86                  val (tstplike_proof, outcome) =
    3.87                    extract_tstplike_proof_and_outcome complete res_code
    3.88                        proof_delims known_failures output
    3.89 @@ -277,7 +281,8 @@
    3.90                   ? (fn (_, msecs0, _, SOME _) =>
    3.91                         run true (Time.- (timeout, Timer.checkRealTimer timer))
    3.92                         |> (fn (output, msecs, tstplike_proof, outcome) =>
    3.93 -                              (output, msecs0 + msecs, tstplike_proof, outcome))
    3.94 +                              (output, int_option_add msecs0 msecs,
    3.95 +                               tstplike_proof, outcome))
    3.96                       | result => result)
    3.97            in ((pool, conjecture_shape, axiom_names), result) end
    3.98          else
    3.99 @@ -312,8 +317,8 @@
   3.100               axiom_names, goal, subgoal)
   3.101          |>> (fn message =>
   3.102                  message ^ (if verbose then
   3.103 -                             "\nATP real CPU time: " ^ string_of_int msecs ^
   3.104 -                             " ms."
   3.105 +                             "\nATP real CPU time: " ^
   3.106 +                             string_of_int (the msecs) ^ " ms."
   3.107                             else
   3.108                               "") ^
   3.109                  (if important_message <> "" then
   3.110 @@ -327,12 +332,12 @@
   3.111       run_time_in_msecs = msecs}
   3.112    end
   3.113  
   3.114 -fun run_atp thy name = atp_fun false name (get_atp thy name)
   3.115 +fun get_atp_as_prover thy name = atp_fun false name (get_atp thy name)
   3.116  
   3.117  fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
   3.118                                  expect, ...})
   3.119                      auto i n minimize_command
   3.120 -                    (prover_problem as {state, goal, axioms, ...})
   3.121 +                    (problem as {state, goal, axioms, ...})
   3.122                      (prover as {default_max_relevant, ...}, atp_name) =
   3.123    let
   3.124      val ctxt = Proof.context_of state
   3.125 @@ -345,7 +350,7 @@
   3.126        let
   3.127          fun really_go () =
   3.128            atp_fun auto atp_name prover params (minimize_command atp_name)
   3.129 -                  prover_problem
   3.130 +                  problem
   3.131            |> (fn {outcome, message, ...} =>
   3.132                   (if is_some outcome then "none" else "some", message))
   3.133          val (outcome_code, message) =
   3.134 @@ -383,37 +388,49 @@
   3.135    end
   3.136  
   3.137  (* FIXME: dummy *)
   3.138 -fun is_smt_solver_installed () = true
   3.139 -
   3.140 -(* FIXME: dummy *)
   3.141 -fun raw_run_smt_solver remote timeout state axioms i =
   3.142 -  ("", axioms |> take 5 |> map fst)
   3.143 +fun run_smt_solver remote timeout state axioms i =
   3.144 +  {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
   3.145 +   run_time_in_msecs = NONE}
   3.146  
   3.147 -fun run_smt_solver remote ({timeout, ...} : params) minimize_command
   3.148 -                   ({state, subgoal, axioms, ...} : prover_problem) =
   3.149 -  raw_run_smt_solver remote timeout state
   3.150 +fun get_smt_solver_as_prover remote ({timeout, ...} : params) minimize_command
   3.151 +                             ({state, subgoal, axioms, ...} : prover_problem) =
   3.152 +  let
   3.153 +    val {outcome, used_axioms, run_time_in_msecs} =
   3.154 +      run_smt_solver remote timeout state
   3.155                       (map_filter (try dest_Unprepared) axioms) subgoal
   3.156 +    val message =
   3.157 +      if outcome = NONE then
   3.158 +        sendback_line (proof_banner false)
   3.159 +                      (apply_on_subgoal subgoal (subgoal_count state) ^
   3.160 +                       command_call smtN (map fst used_axioms))
   3.161 +      else
   3.162 +        ""
   3.163 +  in
   3.164 +    {outcome = outcome, used_axioms = used_axioms,
   3.165 +     run_time_in_msecs = run_time_in_msecs, message = message}
   3.166 +  end
   3.167  
   3.168 -fun run_smt_solver_somehow state (params as {timeout, ...}) i n goal axioms
   3.169 +fun get_prover thy name =
   3.170 +  if member (op =) smt_prover_names name then
   3.171 +    get_smt_solver_as_prover (String.isPrefix remote_prefix)
   3.172 +  else
   3.173 +    get_atp_as_prover thy name
   3.174 +
   3.175 +fun run_smt_solver_somehow state params minimize_command i n goal axioms
   3.176                             (remote, name) =
   3.177    let
   3.178      val ctxt = Proof.context_of state
   3.179      val desc = prover_description ctxt params name (length axioms) i n goal
   3.180 -    val (failure, used_axioms) =
   3.181 -      raw_run_smt_solver remote timeout state axioms i
   3.182 -    val success = (failure = "")
   3.183 -    val message =
   3.184 -      das_Tool ^ ": " ^ desc ^ "\n" ^
   3.185 -      (if success then
   3.186 -         sendback_line (proof_banner false)
   3.187 -                       (apply_on_subgoal i n ^
   3.188 -                        command_call "smt" (map fst used_axioms))
   3.189 -       else
   3.190 -         "Error: " ^ failure)
   3.191 -  in priority message; success end
   3.192 -
   3.193 -val smt_default_max_relevant = 300 (* FUDGE *)
   3.194 -val auto_max_relevant_divisor = 2 (* FUDGE *)
   3.195 +    val problem =
   3.196 +      {state = state, goal = goal, subgoal = i,
   3.197 +       axioms = axioms |> map Unprepared, only = true}
   3.198 +    val {outcome, used_axioms, message, ...} =
   3.199 +      get_smt_solver_as_prover remote params minimize_command problem
   3.200 +    val _ =
   3.201 +      priority (das_Tool ^ ": " ^ desc ^ "\n" ^
   3.202 +                (if outcome = NONE then message
   3.203 +                 else "An unknown error occurred."))
   3.204 +  in outcome = NONE end
   3.205  
   3.206  fun run_sledgehammer (params as {blocking, provers, full_types,
   3.207                                   relevance_thresholds, max_relevant, timeout,
   3.208 @@ -433,7 +450,7 @@
   3.209        val _ = () |> not blocking ? kill_provers
   3.210        val _ = if auto then () else priority "Sledgehammering..."
   3.211        val (smts, atps) =
   3.212 -        provers |> List.partition (member (op =) smt_names)
   3.213 +        provers |> List.partition (member (op =) smt_prover_names)
   3.214                  |>> (take 1 #> map (`(String.isPrefix remote_prefix)))
   3.215                  ||> map (`(get_atp thy))
   3.216        fun run_atps (res as (success, state)) =
   3.217 @@ -451,12 +468,12 @@
   3.218                relevant_facts ctxt full_types relevance_thresholds
   3.219                               max_max_relevant relevance_override chained_ths
   3.220                               hyp_ts concl_t
   3.221 -            val prover_problem =
   3.222 +            val problem =
   3.223                {state = state, goal = goal, subgoal = i,
   3.224                 axioms = axioms |> map (Prepared o prepare_axiom ctxt),
   3.225                 only = only}
   3.226              val run_atp_somehow =
   3.227 -              run_atp_somehow params auto i n minimize_command prover_problem
   3.228 +              run_atp_somehow params auto i n minimize_command problem
   3.229            in
   3.230              if auto then
   3.231                fold (fn prover => fn (true, state) => (true, state)
   3.232 @@ -478,7 +495,8 @@
   3.233                               max_relevant relevance_override chained_ths
   3.234                               hyp_ts concl_t
   3.235            in
   3.236 -            smts |> map (run_smt_solver_somehow state params i n goal axioms)
   3.237 +            smts |> map (run_smt_solver_somehow state params minimize_command i
   3.238 +                                                n goal axioms)
   3.239                   |> exists I |> rpair state
   3.240            end
   3.241        fun run_atps_and_smt_solvers () =
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 09:50:18 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Oct 22 11:11:34 2010 +0200
     4.3 @@ -130,6 +130,9 @@
     4.4    val extend = I
     4.5    fun merge p : T = AList.merge (op =) (K true) p)
     4.6  
     4.7 +(* FIXME: dummy *)
     4.8 +fun is_smt_solver_installed () = true
     4.9 +
    4.10  fun maybe_remote_atp thy name =
    4.11    name |> not (is_atp_installed thy name) ? prefix remote_prefix
    4.12  fun maybe_remote_smt_solver thy =
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 09:50:18 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Oct 22 11:11:34 2010 +0200
     5.3 @@ -94,7 +94,7 @@
     5.4                     i (_ : int) state axioms =
     5.5    let
     5.6      val thy = Proof.theory_of state
     5.7 -    val prover = run_atp thy prover_name
     5.8 +    val prover = get_prover thy prover_name
     5.9      val msecs = Time.toMilliseconds timeout
    5.10      val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
    5.11      val {goal, ...} = Proof.goal state