# HG changeset patch
# User blanchet
# Date 1288091803 -7200
# Node ID 3788b7adab363d5372544bfd618d1ea64bbf5c7f
# Parent  7ecfa9beef91588074c2cefb476b9d5c352a96a3
integrated "smt" proof method with Sledgehammer

diff -r 7ecfa9beef91 -r 3788b7adab36 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Main.thy	Tue Oct 26 13:16:43 2010 +0200
@@ -1,7 +1,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Record Predicate_Compile Nitpick SMT
+imports Plain Record Predicate_Compile Nitpick
 begin
 
 text {*
diff -r 7ecfa9beef91 -r 3788b7adab36 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Oct 26 13:16:43 2010 +0200
@@ -7,7 +7,7 @@
 header {* Sledgehammer: Isabelle--ATP Linkup *}
 
 theory Sledgehammer
-imports ATP
+imports ATP SMT
 uses "Tools/Sledgehammer/sledgehammer_util.ML"
      "Tools/Sledgehammer/sledgehammer_filter.ML"
      "Tools/Sledgehammer/sledgehammer_atp_translate.ML"
diff -r 7ecfa9beef91 -r 3788b7adab36 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 13:16:43 2010 +0200
@@ -8,7 +8,7 @@
 
 signature SLEDGEHAMMER =
 sig
-  type failure = ATP_Systems.failure
+  type failure = ATP_Proof.failure
   type locality = Sledgehammer_Filter.locality
   type relevance_fudge = Sledgehammer_Filter.relevance_fudge
   type relevance_override = Sledgehammer_Filter.relevance_override
@@ -99,7 +99,7 @@
 
 fun is_prover_installed ctxt name =
   let val thy = ProofContext.theory_of ctxt in
-    if is_smt_prover name then true (* FIXME *)
+    if is_smt_prover name then SMT_Solver.is_locally_installed ctxt
     else is_atp_installed thy name
   end
 
@@ -406,34 +406,33 @@
      run_time_in_msecs = msecs}
   end
 
-(* FIXME: dummy *)
-fun saschas_run_smt_solver remote timeout state axioms i =
-  (OS.Process.sleep (Time.fromMilliseconds 1500);
-   {outcome = NONE, used_axioms = axioms |> take 5 |> map fst,
-    run_time_in_msecs = NONE})
+fun failure_from_smt_failure SMT_Solver.Time_Out = TimedOut
+  | failure_from_smt_failure (SMT_Solver.Counterexample _) = Unprovable
+  | failure_from_smt_failure (SMT_Solver.Other_Failure _) = UnknownError
 
 fun run_smt_solver remote ({timeout, ...} : params) minimize_command
                    ({state, subgoal, subgoal_count, axioms, ...}
                     : prover_problem) =
   let
-    val {outcome, used_axioms, run_time_in_msecs} =
-      saschas_run_smt_solver remote timeout state
-                             (map_filter (try dest_Untranslated) axioms) subgoal
+    val {outcome, used_facts, run_time_in_msecs} =
+      SMT_Solver.smt_filter remote timeout state
+                            (map_filter (try dest_Untranslated) axioms) subgoal
     val message =
       if outcome = NONE then
         try_command_line (proof_banner false)
                          (apply_on_subgoal subgoal subgoal_count ^
-                          command_call smtN (map fst used_axioms)) ^
-        minimize_line minimize_command (map fst used_axioms)
+                          command_call smtN (map fst used_facts)) ^
+        minimize_line minimize_command (map fst used_facts)
       else
         ""
   in
-    {outcome = outcome, used_axioms = used_axioms,
-     run_time_in_msecs = run_time_in_msecs, message = message}
+    {outcome = outcome |> Option.map failure_from_smt_failure,
+     used_axioms = used_facts, run_time_in_msecs = SOME run_time_in_msecs,
+     message = message}
   end
 
 fun get_prover thy auto name =
-  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix)
+  if is_smt_prover name then run_smt_solver (String.isPrefix remote_prefix name)
   else run_atp auto name (get_atp thy name)
 
 fun run_prover (params as {blocking, debug, max_relevant, timeout, expect, ...})
diff -r 7ecfa9beef91 -r 3788b7adab36 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 12:23:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 26 13:16:43 2010 +0200
@@ -130,9 +130,6 @@
   val extend = I
   fun merge p : T = AList.merge (op =) (K true) p)
 
-(* FIXME: dummy *)
-fun is_smt_solver_installed ctxt = true
-
 fun remotify_prover_if_available_and_not_already_remote thy name =
   if String.isPrefix remote_prefix name then
     SOME name