# HG changeset patch
# User blanchet
# Date 1394791537 -3600
# Node ID e03c0f6ad1b6be9e502da0f0014dff55156322ac
# Parent  315cc3c0a19ac45f53d5ff1ee8317e2f682ce472
tuning

diff -r 315cc3c0a19a -r e03c0f6ad1b6 src/HOL/Tools/SMT2/smt2_solver.ML
--- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 10:17:32 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri Mar 14 11:05:37 2014 +0100
@@ -15,12 +15,12 @@
     command: unit -> string list,
     options: Proof.context -> string list,
     default_max_relevant: int,
-    supports_filter: bool,
+    can_filter: bool,
     outcome: string -> string list -> outcome * string list,
     cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
       term list * term list) option,
     replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
+      ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
 
   (*registry*)
   val add_solver: solver_config -> theory -> theory
@@ -147,12 +147,12 @@
   command: unit -> string list,
   options: Proof.context -> string list,
   default_max_relevant: int,
-  supports_filter: bool,
+  can_filter: bool,
   outcome: string -> string list -> outcome * string list,
   cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
     term list * term list) option,
   replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option }
+    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm) option}
 
 
 (* check well-sortedness *)
@@ -172,9 +172,9 @@
 type solver_info = {
   command: unit -> string list,
   default_max_relevant: int,
-  supports_filter: bool,
-  replay: Proof.context -> string list * SMT2_Translate.replay_data ->
-    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm }
+  can_filter: bool,
+  finish: Proof.context -> SMT2_Translate.replay_data -> string list ->
+    ((int * (int * thm)) list * Z3_New_Proof.z3_step list) * thm}
 
 structure Solvers = Generic_Data
 (
@@ -186,7 +186,7 @@
 
 local
   fun finish outcome cex_parser replay ocl outer_ctxt
-      (output, (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data)) =
+      (replay_data as {context=ctxt, ...} : SMT2_Translate.replay_data) output =
     (case outcome output of
       (Unsat, ls) =>
         if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay
@@ -206,30 +206,25 @@
   val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
 in
 
-fun add_solver cfg =
+fun add_solver ({name, class, avail, command, options, default_max_relevant, can_filter,
+    outcome, cex_parser, replay} : solver_config) =
   let
-    val {name, class, avail, command, options, default_max_relevant,
-      supports_filter, outcome, cex_parser, replay} = cfg
-
-    fun core_oracle () = cfalse
-
     fun solver ocl = {
       command = command,
       default_max_relevant = default_max_relevant,
-      supports_filter = supports_filter,
-      replay = finish (outcome name) cex_parser replay ocl }
+      can_filter = can_filter,
+      finish = finish (outcome name) cex_parser replay ocl}
 
     val info = {name=name, class=class, avail=avail, options=options}
   in
-    Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
+    Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, ocl) =>
     Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
     Context.theory_map (SMT2_Config.add_solver info)
   end
 
 end
 
-fun get_info ctxt name =
-  the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
+fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
 
 val solver_name_of = SMT2_Config.solver_of
 
@@ -242,11 +237,12 @@
 fun apply_solver ctxt wthms0 =
   let
     val wthms = map (apsnd (check_topsort ctxt)) wthms0
-    val (name, {command, replay, ...}) = name_and_info_of ctxt
-  in replay ctxt (invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt) end
+    val (name, {command, finish, ...}) = name_and_info_of ctxt
+    val (output, replay_data) = invoke name command (SMT2_Normalize.normalize ctxt wthms) ctxt
+  in finish ctxt replay_data output end
 
 val default_max_relevant = #default_max_relevant oo get_info
-val supports_filter = #supports_filter o snd o name_and_info_of 
+val can_filter = #can_filter o snd o name_and_info_of 
 
 
 (* filter *)
@@ -282,7 +278,7 @@
     |> fst
     |> (fn (iidths0, z3_proof) =>
       let
-        val iidths = if supports_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
+        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
       in
         {outcome = NONE, 
          conjecture_id =
diff -r 315cc3c0a19a -r e03c0f6ad1b6 src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 10:17:32 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Fri Mar 14 11:05:37 2014 +0100
@@ -55,7 +55,7 @@
   command = make_command "CVC3_NEW",
   options = cvc3_options,
   default_max_relevant = 400 (* FUDGE *),
-  supports_filter = false,
+  can_filter = false,
   outcome =
     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   cex_parser = NONE,
@@ -77,7 +77,7 @@
       string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout)),
     "--smtlib"]),
   default_max_relevant = 350 (* FUDGE *),
-  supports_filter = false,
+  can_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
   replay = NONE }
@@ -144,7 +144,7 @@
   command = z3_make_command "Z3_NEW",
   options = z3_options,
   default_max_relevant = 350 (* FUDGE *),
-  supports_filter = true,
+  can_filter = true,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = SOME Z3_New_Model.parse_counterex,
   replay = SOME Z3_New_Replay.replay }
diff -r 315cc3c0a19a -r e03c0f6ad1b6 src/HOL/Tools/SMT2/smt2_translate.ML
--- a/src/HOL/Tools/SMT2/smt2_translate.ML	Fri Mar 14 10:17:32 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML	Fri Mar 14 11:05:37 2014 +0100
@@ -250,8 +250,7 @@
       val (Ts, T) = Term.strip_type (Term.type_of t)
     in find_min 0 (take i (rev Ts)) T end
 
-  fun app u (t, T) =
-    (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
+  fun app u (t, T) = (Const (@{const_name SMT2.fun_app}, T --> T) $ t $ u, Term.range_type T)
 
   fun apply i t T ts =
     let
diff -r 315cc3c0a19a -r e03c0f6ad1b6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 10:17:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 14 11:05:37 2014 +0100
@@ -87,7 +87,7 @@
   | add_line_pass1 line lines = line :: lines
 
 fun add_lines_pass2 res [] = rev res
-  | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
+  | add_lines_pass2 res ((line as (name, role, t, rule, deps)) :: lines) =
     let
       val is_last_line = null lines
 
@@ -102,7 +102,7 @@
       if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
          is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
          is_before_skolemize_rule () then
-        add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
+        add_lines_pass2 (line :: res) lines
       else
         add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
     end