# HG changeset patch
# User blanchet
# Date 1290533289 -3600
# Node ID 8db6c2b1591dd32e751830f996577c4a2a2da35b
# Parent  1a65f0c748275b194b4663634114f957a5686cf8
try Metis to reconstruct SMT proofs, to increase success rate and reduce dependency on (often remote) SMT solvers or certificates

diff -r 1a65f0c74827 -r 8db6c2b1591d src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 23 18:26:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Nov 23 18:28:09 2010 +0100
@@ -32,7 +32,7 @@
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
-    {outcome: SMT_Failure.failure option, used_facts: 'a list,
+    {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
     run_time_in_msecs: int option}
 
   (*tactic*)
@@ -331,7 +331,7 @@
     val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
     val rm = SOME run_remote
   in
-    split_list xrules
+    (xrules, map snd xrules)
     ||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
     |-> map_filter o try o nth
     |> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
diff -r 1a65f0c74827 -r 8db6c2b1591d src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 18:26:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Nov 23 18:28:09 2010 +0100
@@ -493,6 +493,24 @@
       end
   in iter timeout 1 NONE (SOME 0) end
 
+(* taken from "Mirabelle" and generalized *)
+fun can_apply timeout tac state i =
+  let
+    val {context = ctxt, facts, goal} = Proof.goal state
+    val ctxt = ctxt |> Config.put Metis_Tactics.verbose false
+    val full_tac = Method.insert_tac facts i THEN tac ctxt i
+  in
+    case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
+      SOME (SOME _) => true
+    | _ => false
+  end
+
+val smt_metis_timeout = seconds 0.5
+
+fun can_apply_metis state i ths =
+  can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths)
+            state i
+
 fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
@@ -507,10 +525,16 @@
     val message =
       case outcome of
         NONE =>
-        try_command_line (proof_banner auto)
-                         (apply_on_subgoal subgoal subgoal_count ^
-                          command_call smtN (map fst used_facts)) ^
-        minimize_line minimize_command (map fst used_facts)
+        let
+          val method =
+            if can_apply_metis state subgoal (map snd used_facts) then "metis"
+            else "smt"
+        in
+          try_command_line (proof_banner auto)
+                           (apply_on_subgoal subgoal subgoal_count ^
+                            command_call method (map (fst o fst) used_facts)) ^
+          minimize_line minimize_command (map (fst o fst) used_facts)
+        end
       | SOME SMT_Failure.Time_Out => "Timed out."
       | SOME (SMT_Failure.Abnormal_Termination code) =>
         "The SMT solver terminated abnormally with exit code " ^
@@ -521,7 +545,7 @@
         SMT_Failure.string_of_failure ctxt failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
   in
-    {outcome = outcome, used_facts = used_facts,
+    {outcome = outcome, used_facts = map fst used_facts,
      run_time_in_msecs = run_time_in_msecs, message = message}
   end