# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID d58157bb1ae7e2119eb380483943d7bac08ca6f0
# Parent  54b3c9c056643d9cc9b9eca90cddb082fbf35a68
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction

diff -r 54b3c9c05664 -r d58157bb1ae7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -21,7 +21,7 @@
   val repair_conjecture_shape_and_fact_names :
     string -> int list list -> (string * locality) list vector
     -> int list list * (string * locality) list vector
-  val apply_on_subgoal : int -> int -> string
+  val apply_on_subgoal : string -> int -> int -> string
   val command_call : string -> string list -> string
   val try_command_line : string -> string -> string
   val minimize_line : ('a list -> string) -> 'a list -> string
@@ -116,9 +116,12 @@
 
 fun string_for_label (s, num) = s ^ string_of_int num
 
-fun apply_on_subgoal _ 1 = "by "
-  | apply_on_subgoal 1 _ = "apply "
-  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
+fun set_settings "" = ""
+  | set_settings settings = "using [[" ^ settings ^ "]] "
+fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
+  | apply_on_subgoal settings 1 _ = set_settings settings ^ "apply "
+  | apply_on_subgoal settings i n =
+    "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
 fun command_call name [] = name
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
 fun try_command_line banner command =
@@ -130,7 +133,7 @@
   if types_dangerous_types type_sys then "metisFT" else "metis"
 fun metis_call type_sys ss = command_call (metis_name type_sys) ss
 fun metis_command type_sys i n (ls, ss) =
-  using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss
+  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
 fun metis_line banner type_sys i n ss =
   try_command_line banner (metis_command type_sys i n ([], ss))
 fun minimize_line _ [] = ""
diff -r 54b3c9c05664 -r d58157bb1ae7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -540,15 +540,16 @@
       case outcome of
         NONE =>
         let
-          val method =
+          val (method, settings) =
             if can_apply_metis debug state subgoal (map snd used_facts) then
-              "metis"
+              ("metis", "")
             else
-              "smt"
+              ("smt", if suffix = SMT_Config.solver_of @{context} then ""
+                      else "smt_solver = " ^ maybe_quote suffix)
         in
           try_command_line (proof_banner auto)
-                           (apply_on_subgoal subgoal subgoal_count ^
-                            command_call method (map fst other_lemmas)) ^
+              (apply_on_subgoal settings subgoal subgoal_count ^
+               command_call method (map fst other_lemmas)) ^
           minimize_line minimize_command
                         (map fst (other_lemmas @ chained_lemmas))
         end