1.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 10:17:32 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:05:37 2014 +0100
     1.3 @@ -15,12 +15,12 @@
     1.4      command: unit -> string list,
     1.5      options: Proof.context -> string list,
     1.6      default_max_relevant: int,
     1.7 -    supports_filter: bool,
     1.8 +    can_filter: bool,
     1.9      outcome: string -> string list -> outcome * string list,
    1.10      cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    1.11        term list * term list) option,
    1.12      replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    1.13 -      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
    1.14 +      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
    1.15  
    1.16    (*registry*)
    1.17    val add_solver: solver_config -> theory -> theory
    1.18 @@ -147,12 +147,12 @@
    1.19    command: unit -> string list,
    1.20    options: Proof.context -> string list,
    1.21    default_max_relevant: int,
    1.22 -  supports_filter: bool,
    1.23 +  can_filter: bool,
    1.24    outcome: string -> string list -> outcome * string list,
    1.25    cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    1.26      term list * term list) option,
    1.27    replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
    1.28 -    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
    1.29 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
    1.30  
    1.31  
    1.32  (* check well-sortedness *)
    1.33 @@ -172,9 +172,9 @@
    1.34  type solver_info = {
    1.35    command: unit -> string list,
    1.36    default_max_relevant: int,
    1.37 -  supports_filter: bool,
    1.38 -  replay: Proof.context -> string list * SMT2_Translate.replay_data ->
    1.39 -    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm }
    1.40 +  can_filter: bool,
    1.41 +  finish: Proof.context -> SMT2_Translate.replay_data -> string list ->
    1.42 +    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm}
    1.43  
    1.44  structure Solvers = Generic_Data
    1.45  (
    1.46 @@ -186,7 +186,7 @@
    1.47  
    1.48  local
    1.49    fun finish outcome cex_parser replay ocl outer_ctxt
    1.50 -      (output, (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data)) =
    1.51 +      (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data) output =
    1.52      (case outcome output of
    1.53        (Unsat, ls) =>
    1.54          if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay
    1.55 @@ -206,30 +206,25 @@
    1.56    val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
    1.57  in
    1.58  
    1.59 -fun add_solver cfg =
    1.60 +fun add_solver ({name, class, avail, command, options, default_max_relevant, can_filter,
    1.61 +    outcome, cex_parser, replay} : solver_config) =
    1.62    let
    1.63 -    val {name, class, avail, command, options, default_max_relevant,
    1.64 -      supports_filter, outcome, cex_parser, replay} = cfg
    1.65 -
    1.66 -    fun core_oracle () = cfalse
    1.67 -
    1.68      fun solver ocl = {
    1.69        command = command,
    1.70        default_max_relevant = default_max_relevant,
    1.71 -      supports_filter = supports_filter,
    1.72 -      replay = finish (outcome name) cex_parser replay ocl }
    1.73 +      can_filter = can_filter,
    1.74 +      finish = finish (outcome name) cex_parser replay ocl}
    1.75  
    1.76      val info = {name=name, class=class, avail=avail, options=options}
    1.77    in
    1.78 -    Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
    1.79 +    Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, ocl) =>
    1.80      Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
    1.81      Context.theory_map (SMT2_Config.add_solver info)
    1.82    end
    1.83  
    1.84  end
    1.85  
    1.86 -fun get_info ctxt name =
    1.87 -  the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
    1.88 +fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
    1.89  
    1.90  val solver_name_of = SMT2_Config.solver_of
    1.91  
    1.92 @@ -242,11 +237,12 @@
    1.93  fun apply_solver ctxt wthms0 =
    1.94    let
    1.95      val wthms = map (apsnd (check_topsort ctxt)) wthms0
    1.96 -    val (name, {command, replay, ...}) = name_and_info_of ctxt
    1.97 -  in replay ctxt (invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt) end
    1.98 +    val (name, {command, finish, ...}) = name_and_info_of ctxt
    1.99 +    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
   1.100 +  in finish ctxt replay_data output end
   1.101  
   1.102  val default_max_relevant = #default_max_relevant oo get_info
   1.103 -val supports_filter = #supports_filter o snd o name_and_info_of 
   1.104 +val can_filter = #can_filter o snd o name_and_info_of 
   1.105  
   1.106  
   1.107  (* filter *)
   1.108 @@ -282,7 +278,7 @@
   1.109      |> fst
   1.110      |> (fn (iidths0, z3_proof) =>
   1.111        let
   1.112 -        val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
   1.113 +        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
   1.114        in
   1.115          {outcome = NONE, 
   1.116           conjecture_id =

     2.1 --- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 10:17:32 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 11:05:37 2014 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4    command = make_command "CVC3_NEW",
     2.5    options = cvc3_options,
     2.6    default_max_relevant = 400 (* FUDGE *),
     2.7 -  supports_filter = false,
     2.8 +  can_filter = false,
     2.9    outcome =
    2.10      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    2.11    cex_parser = NONE,
    2.12 @@ -77,7 +77,7 @@
    2.13        string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
    2.14      "--smtlib"]),
    2.15    default_max_relevant = 350 (* FUDGE *),
    2.16 -  supports_filter = false,
    2.17 +  can_filter = false,
    2.18    outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    2.19    cex_parser = NONE,
    2.20    replay = NONE }
    2.21 @@ -144,7 +144,7 @@
    2.22    command = z3_make_command "Z3_NEW",
    2.23    options = z3_options,
    2.24    default_max_relevant = 350 (* FUDGE *),
    2.25 -  supports_filter = true,
    2.26 +  can_filter = true,
    2.27    outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    2.28    cex_parser = SOME Z3_New_Model.parse_counterex,
    2.29    replay = SOME Z3_New_Replay.replay }

     3.1 --- a/src/HOL/Tools/SMT2/smt2_translate.ML	Fri Mar 14 10:17:32 2014 +0100
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Fri Mar 14 11:05:37 2014 +0100
     3.3 @@ -250,8 +250,7 @@
     3.4        val (Ts, T) = Term.strip_type (Term.type_of t)
     3.5      in find_min 0 (take i (rev Ts)) T end
     3.6  
     3.7 -  fun app u (t, T) =
     3.8 -    (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
     3.9 +  fun app u (t, T) = (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
    3.10  
    3.11    fun apply i t T ts =
    3.12      let

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 10:17:32 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:05:37 2014 +0100
     4.3 @@ -87,7 +87,7 @@
     4.4    | add_line_pass1 line lines = line :: lines
     4.5  
     4.6  fun add_lines_pass2 res [] = rev res
     4.7 -  | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
     4.8 +  | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
     4.9      let
    4.10        val is_last_line = null lines
    4.11  
    4.12 @@ -102,7 +102,7 @@
    4.13        if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
    4.14           is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
    4.15           is_before_skolemize_rule () then
    4.16 -        add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
    4.17 +        add_lines_pass2 (line :: res) lines
    4.18        else
    4.19          add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
    4.20      end