# HG changeset patch
# User blanchet
# Date 1287671140 -7200
# Node ID 5ef6747aa6194d1fdba957f9db9dde254fb7f820
# Parent  6ad9081665db3dc59f427761172ad625412c2240
first step in adding support for an SMT backend to Sledgehammer

diff -r 6ad9081665db -r 5ef6747aa619 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Thu Oct 21 14:55:09 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Thu Oct 21 16:25:40 2010 +0200
@@ -199,19 +199,19 @@
 
 \prew
 \slshape
-Sledgehammer: Prover ``\textit{e}'' for subgoal 1: \\
+Sledgehammer: ``\textit{e}'' for subgoal 1: \\
 $([a] = [b]) = (a = b)$ \\
 Try this command: \textbf{by} (\textit{metis hd.simps}). \\
 To minimize the number of lemmas, try this: \\
 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
 %
-Sledgehammer: Prover ``\textit{spass}'' for subgoal 1: \\
+Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
 $([a] = [b]) = (a = b)$ \\
 Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
 To minimize the number of lemmas, try this: \\
 \textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
 %
-Sledgehammer: Prover ``\textit{remote\_vampire}'' for subgoal 1: \\
+Sledgehammer: ``\textit{remote\_vampire}'' for subgoal 1: \\
 $([a] = [b]) = (a = b)$ \\
 Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
 \phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
@@ -220,6 +220,7 @@
 \phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
 \phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
 \postw
+%%% TODO: Mention SInE-E
 
 Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
 is not installed (\S\ref{installation}), you will see references to
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -318,7 +318,7 @@
     fun default_atp_name () =
       hd (#provers (Sledgehammer_Isar.default_params thy []))
       handle Empty => error "No ATP available."
-    fun get_atp name = (name, Sledgehammer.get_atp_fun thy name)
+    fun get_atp name = (name, Sledgehammer.run_atp thy name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_atp name
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -25,7 +25,7 @@
   val vampireN : string
   val sine_eN : string
   val snarkN : string
-  val remote_atp_prefix : string
+  val remote_prefix : string
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val available_atps : theory -> string list
@@ -64,7 +64,7 @@
 val vampireN = "vampire"
 val sine_eN = "sine_e"
 val snarkN = "snark"
-val remote_atp_prefix = "remote_"
+val remote_prefix = "remote_"
 
 structure Data = Theory_Data
 (
@@ -229,11 +229,11 @@
 
 fun remote_atp name system_name system_versions proof_delims known_failures
                default_max_relevant use_conjecture_for_hypotheses =
-  (remote_atp_prefix ^ name,
+  (remote_prefix ^ name,
    remote_config system_name system_versions proof_delims known_failures
                  default_max_relevant use_conjecture_for_hypotheses)
 fun remotify_atp (name, config) system_name system_versions =
-  (remote_atp_prefix ^ name, remotify_config system_name system_versions config)
+  (remote_prefix ^ name, remotify_config system_name system_versions config)
 
 val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
 val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -49,6 +49,7 @@
 
   type atp = params -> minimize_command -> atp_problem -> atp_result
 
+  val smtN : string
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
@@ -56,7 +57,10 @@
   val kill_provers : unit -> unit
   val running_provers : unit -> unit
   val messages : int option -> unit
-  val get_atp_fun : theory -> string -> atp
+  val run_atp : theory -> string -> atp
+  val run_smt_solver :
+    Proof.context -> bool -> Time.time -> ('a * thm) list -> string * 'a list
+  val is_smt_solver_installed : unit -> bool
   val run_sledgehammer :
     params -> bool -> int -> relevance_override -> (string -> minimize_command)
     -> Proof.state -> bool * Proof.state
@@ -82,9 +86,18 @@
    "Async_Manager". *)
 val das_Tool = "Sledgehammer"
 
+val smtN = "smt"
+val smt_names = [smtN, remote_prefix ^ smtN]
+
 fun available_provers thy =
-  priority ("Available provers: " ^
-             commas (sort_strings (available_atps thy)) ^ ".")
+  let
+    val (remote_provers, local_provers) =
+      sort_strings (available_atps thy) @ smt_names
+      |> List.partition (String.isPrefix remote_prefix)
+  in
+    priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
+              ".")
+  end
 
 fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
 fun running_provers () = Async_Manager.running_threads das_Tool "provers"
@@ -145,6 +158,22 @@
   |> Exn.release
   |> tap (after path)
 
+fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
+                       i n goal =
+  quote name ^
+  (if verbose then
+     " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
+   else
+     "") ^
+  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+  (if blocking then
+     ""
+   else
+     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+
+fun proof_banner auto =
+  if auto then "Sledgehammer found a proof" else "Try this command"
+
 (* generic TPTP-based ATPs *)
 
 (* Important messages are important but not so important that users want to see
@@ -268,15 +297,13 @@
         extract_important_message output
       else
         ""
-    val banner = if auto then "Sledgehammer found a proof"
-                 else "Try this command"
     val (message, used_thm_names) =
       case outcome of
         NONE =>
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-            (banner, full_types, minimize_command, tstplike_proof, axiom_names,
-             goal, subgoal)
+            (proof_banner auto, full_types, minimize_command, tstplike_proof,
+             axiom_names, goal, subgoal)
         |>> (fn message =>
                 message ^ (if verbose then
                              "\nATP real CPU time: " ^ string_of_int msecs ^
@@ -296,30 +323,20 @@
      axiom_names = axiom_names, conjecture_shape = conjecture_shape}
   end
 
-fun get_atp_fun thy name = atp_fun false name (get_atp thy name)
+fun run_atp thy name = atp_fun false name (get_atp thy name)
 
-fun run_atp (params as {blocking, debug, verbose, max_relevant, timeout, expect,
-                        ...})
-            auto i n minimize_command
-            (atp_problem as {state, goal, axioms, ...})
-            (atp as {default_max_relevant, ...}, atp_name) =
+fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
+                                expect, ...})
+                    auto i n minimize_command
+                    (atp_problem as {state, goal, axioms, ...})
+                    (atp as {default_max_relevant, ...}, atp_name) =
   let
     val ctxt = Proof.context_of state
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val max_relevant = the_default default_max_relevant max_relevant
     val num_axioms = Int.min (length axioms, max_relevant)
-    val desc =
-      "ATP " ^ quote atp_name ^
-      (if verbose then
-         " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
-       else
-         "") ^
-      " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
-      (if blocking then
-         ""
-       else
-         "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+    val desc = prover_description ctxt params atp_name num_axioms i n goal
     fun go () =
       let
         fun really_go () =
@@ -361,10 +378,36 @@
        (false, state))
   end
 
-val auto_max_relevant_divisor = 2
+(* FIXME: dummy *)
+fun run_smt_solver ctxt remote timeout axioms =
+  ("", axioms |> take 5 |> map fst)
+
+(* FIXME: dummy *)
+fun is_smt_solver_installed () = true
+
+fun run_smt_solver_somehow ctxt (params as {timeout, ...}) i n goal axioms
+                           (remote, name) =
+  let
+    val desc =
+      prover_description ctxt params name (length axioms) i n goal
+    val (failure, used_thm_names) = run_smt_solver ctxt remote timeout axioms
+    val success = (failure = "")
+    val message =
+      das_Tool ^ ": " ^ desc ^ "\n" ^
+      (if success then
+         sendback_line (proof_banner false)
+                       (apply_on_subgoal i n ^
+                        command_call "smt" (map fst used_thm_names))
+       else
+         "Error: " ^ failure)
+  in priority message; success end
+
+val smt_default_max_relevant = 300 (* FUDGE *)
+val auto_max_relevant_divisor = 2 (* FUDGE *)
 
 fun run_sledgehammer (params as {blocking, provers, full_types,
-                                 relevance_thresholds, max_relevant, ...})
+                                 relevance_thresholds, max_relevant, timeout,
+                                 ...})
                      auto i (relevance_override as {only, ...}) minimize_command
                      state =
   if null provers then
@@ -375,37 +418,67 @@
     let
       val _ = Proof.assert_backward state
       val thy = Proof.theory_of state
+      val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
+      val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val _ = () |> not blocking ? kill_provers
       val _ = if auto then () else priority "Sledgehammering..."
-      val atps = map (`(get_atp thy)) provers
-      fun go () =
-        let
-          val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
-          val (_, hyp_ts, concl_t) = strip_subgoal goal i
-          val max_max_relevant =
-            case max_relevant of
-              SOME n => n
-            | NONE =>
-              0 |> fold (Integer.max o #default_max_relevant o fst) atps
-                |> auto ? (fn n => n div auto_max_relevant_divisor)
-          val axioms =
-            relevant_facts ctxt full_types relevance_thresholds
-                           max_max_relevant relevance_override chained_ths
-                           hyp_ts concl_t
-          val atp_problem =
-            {state = state, goal = goal, subgoal = i,
-             axioms = map (prepare_axiom ctxt) axioms, only = only}
-          val run_atp = run_atp params auto i n minimize_command atp_problem
-        in
-          if auto then
-            fold (fn atp => fn (true, state) => (true, state)
-                             | (false, _) => run_atp atp)
-                 atps (false, state)
-          else
-            (if blocking then Par_List.map else map) run_atp atps
-            |> exists fst |> rpair state
-        end
-    in if blocking then go () else Future.fork (tap go) |> K (false, state) end
+      val (smts, atps) =
+        provers |> List.partition (member (op =) smt_names)
+                |>> (take 1 #> map (`(String.isPrefix remote_prefix)))
+                ||> map (`(get_atp thy))
+      fun run_atps (res as (success, state)) =
+        if success orelse null atps then
+          res
+        else
+          let
+            val max_max_relevant =
+              case max_relevant of
+                SOME n => n
+              | NONE =>
+                0 |> fold (Integer.max o #default_max_relevant o fst) atps
+                  |> auto ? (fn n => n div auto_max_relevant_divisor)
+            val axioms =
+              relevant_facts ctxt full_types relevance_thresholds
+                             max_max_relevant relevance_override chained_ths
+                             hyp_ts concl_t
+            val atp_problem =
+              {state = state, goal = goal, subgoal = i,
+               axioms = map (prepare_axiom ctxt) axioms, only = only}
+            val run_atp_somehow =
+              run_atp_somehow params auto i n minimize_command atp_problem
+          in
+            if auto then
+              fold (fn atp => fn (true, state) => (true, state)
+                               | (false, _) => run_atp_somehow atp)
+                   atps (false, state)
+            else
+              atps |> (if blocking then Par_List.map else map) run_atp_somehow
+                   |> exists fst |> rpair state
+          end
+      fun run_smt_solvers (res as (success, state)) =
+        if success orelse null smts then
+          res
+        else
+          let
+            val max_relevant =
+              max_relevant |> the_default smt_default_max_relevant
+            val axioms =
+              relevant_facts ctxt full_types relevance_thresholds
+                             max_relevant relevance_override chained_ths
+                             hyp_ts concl_t
+          in
+            smts |> map (run_smt_solver_somehow ctxt params i n goal axioms)
+                 |> exists I |> rpair state
+          end
+      fun run_atps_and_smt_solvers () =
+        [run_atps, run_smt_solvers]
+        |> Par_List.map (fn f => f (false, state) |> K ())
+    in
+      if blocking then
+        (false, state) |> run_atps |> not auto ? run_smt_solvers
+      else
+        Future.fork (tap run_atps_and_smt_solvers) |> K (false, state)
+    end
 
 val setup =
   dest_dir_setup
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -131,18 +131,19 @@
   fun merge p : T = AList.merge (op =) (K true) p)
 
 fun maybe_remote_atp thy name =
-  name |> not (is_atp_installed thy name) ? prefix remote_atp_prefix
+  name |> not (is_atp_installed thy name) ? prefix remote_prefix
+fun maybe_remote_smt_solver thy =
+  smtN |> not (is_smt_solver_installed ()) ? prefix remote_prefix
 
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
 fun default_provers_param_value thy =
   (filter (is_atp_installed thy) [spassN] @
    [maybe_remote_atp thy eN,
-    if forall (is_atp_installed thy) [spassN, eN] then
-      remote_atp_prefix ^ vampireN
-    else
-      maybe_remote_atp thy vampireN,
-    remote_atp_prefix ^ sine_eN])
+    if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
+    else maybe_remote_atp thy vampireN,
+    remote_prefix ^ sine_eN,
+    maybe_remote_smt_solver thy])
   |> space_implode " "
 
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -96,7 +96,7 @@
                       i (_ : int) state axioms =
   let
     val thy = Proof.theory_of state
-    val atp = get_atp_fun thy prover
+    val atp = run_atp thy prover
     val msecs = Time.toMilliseconds timeout
     val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".")
     val {context = ctxt, goal, ...} = Proof.goal state
diff -r 6ad9081665db -r 5ef6747aa619 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 21 16:25:40 2010 +0200
@@ -20,6 +20,9 @@
   val repair_conjecture_shape_and_axiom_names :
     string -> int list list -> (string * locality) list vector
     -> int list list * (string * locality) list vector
+  val apply_on_subgoal : int -> int -> string
+  val command_call : string -> string list -> string
+  val sendback_line : string -> string -> string
   val metis_proof_text : metis_params -> text_result
   val isar_proof_text : isar_params -> metis_params -> text_result
   val proof_text : bool -> isar_params -> metis_params -> text_result
@@ -111,21 +114,22 @@
 
 fun string_for_label (s, num) = s ^ string_of_int num
 
-fun metis_using [] = ""
-  | metis_using ls =
+fun apply_on_subgoal _ 1 = "by "
+  | apply_on_subgoal 1 _ = "apply "
+  | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
+fun command_call name [] = name
+  | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun sendback_line banner command =
+  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
+fun using_labels [] = ""
+  | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_apply _ 1 = "by "
-  | metis_apply 1 _ = "apply "
-  | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
 fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types [] = metis_name full_types
-  | metis_call full_types ss =
-    "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
+fun metis_call full_types ss = command_call (metis_name full_types) ss
 fun metis_command full_types i n (ls, ss) =
-  metis_using ls ^ metis_apply i n ^ metis_call full_types ss
+  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
 fun metis_line banner full_types i n ss =
-  banner ^ ": " ^
-  Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
+  sendback_line banner (metis_command full_types i n ([], ss))
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of