optionally force the remote version of an SMT solver to be executed

--- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:49:36 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:51:09 2010 +0200
@@ -44,7 +44,7 @@
   val select_certificates: string -> Context.generic -> Context.generic
 
   (*solvers*)
-  type solver = Proof.context -> (int * thm) list -> int list * thm
+  type solver = bool -> Proof.context -> (int * thm) list -> int list * thm
   val add_solver: solver_config -> theory -> theory
   val set_solver_options: string -> string -> Context.generic ->
     Context.generic
@@ -52,6 +52,7 @@
   val solver_name_of: Context.generic -> string
   val select_solver: string -> Context.generic -> Context.generic
   val solver_of: Context.generic -> solver
+  val is_locally_installed: Proof.context -> bool
 
   (*filter*)
   val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
@@ -155,22 +156,28 @@
 
 (* interface to external solvers *)
 
+fun get_local_solver env_var =
+  let val local_solver = getenv env_var
+  in if local_solver <> "" then SOME local_solver else NONE end
+
 local
 
-fun choose (env_var, is_remote, remote_name) =
+fun choose (force_remote, env_var, is_remote, name) =
   let
-    val local_solver = getenv env_var
+    val lsolver = get_local_solver env_var
     val remote_url = getenv "REMOTE_SMT_URL"
   in
-    if local_solver <> ""
+    if not force_remote andalso is_some lsolver
     then 
-     (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
-      [local_solver])
+     (tracing ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
+      [the lsolver])
     else if is_remote
     then
-     (tracing ("Invoking remote SMT solver " ^ quote remote_name ^ " at " ^
+     (tracing ("Invoking remote SMT solver " ^ quote name ^ " at " ^
         quote remote_url ^ " ...");
-      [getenv "REMOTE_SMT", remote_name])
+      [getenv "REMOTE_SMT", name])
+    else if force_remote
+    then error ("SMT solver " ^ quote name ^ " is not remotely available.")
     else error ("Undefined Isabelle environment variable: " ^ quote env_var)
   end
 
@@ -263,17 +270,18 @@
     else ()
   end
 
-fun gen_solver name info ctxt irules =
+fun gen_solver name info force_remote ctxt irules =
   let
     val {env_var, is_remote, options, more_options, interface, reconstruct} =
       info
     val {extra_norm, translate} = interface
     val (with_datatypes, translate') =
       set_has_datatypes (Config.get ctxt datatypes) translate
+    val cmd = (force_remote, env_var, is_remote, name)
   in
     (irules, ctxt)
     |-> SMT_Normalize.normalize extra_norm with_datatypes
-    |-> invoke translate' name (env_var, is_remote, name) more_options options
+    |-> invoke translate' name cmd more_options options
     |-> reconstruct
     |-> (fn (idxs, thm) => fn ctxt' => thm
     |> singleton (ProofContext.export ctxt' ctxt)
@@ -286,7 +294,7 @@
 
 (* solver store *)
 
-type solver = Proof.context -> (int * thm) list -> int list * thm
+type solver = bool -> Proof.context -> (int * thm) list -> int list * thm
 
 type solver_info = {
   env_var: string,
@@ -378,6 +386,12 @@
   let val name = solver_name_of context
   in gen_solver name (raw_solver_of context name) end
 
+fun is_locally_installed ctxt =
+  let
+    val name = solver_name_of (Context.Proof ctxt)
+    val {env_var, ...} = raw_solver_of (Context.Proof ctxt) name
+  in is_some (get_local_solver env_var) end
+
 
 
 (* SMT filter *)
@@ -387,13 +401,13 @@
   | TVar (_, []) => true
   | _ => false))
 
-fun smt_solver ctxt irules =
+fun smt_solver force_remote ctxt irules =
   (* without this test, we would run into problems when atomizing the rules: *)
   if exists (has_topsort o Thm.prop_of o snd) irules
   then raise SMT (Other_Failure "proof state contains the universal sort {}")
-  else solver_of (Context.Proof ctxt) ctxt irules
+  else solver_of (Context.Proof ctxt) force_remote ctxt irules
 
-fun smt_filter remote time_limit st xrules i =
+fun smt_filter rm time_limit st xrules i =
   let
     val {context, facts, goal} = Proof.goal st
     val ctxt =
@@ -408,11 +422,12 @@
     val irs = map (pair ~1) (Thm.assume cprop :: facts)
   in
     split_list xrules
-    ||> distinct (op =) o fst o smt_solver ctxt o append irs o map_index I
+    ||> 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= ~1})
   end
   handle SMT fail => {outcome=SOME fail, used_facts=[], run_time_in_msecs= ~1}
+  (* FIXME: measure runtime *)
 
 
 
@@ -421,15 +436,15 @@
 fun smt_tac' pass_exns ctxt rules =
   CONVERSION (SMT_Normalize.atomize_conv ctxt)
   THEN' Tactic.rtac @{thm ccontr}
-  THEN' SUBPROOF (fn {context, prems, ...} =>
+  THEN' SUBPROOF (fn {context=cx, prems, ...} =>
     let
-      fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems)))
-      fun trace cx f = trace_msg cx (prefix "SMT: " o string_of_failure cx) f
+      fun solve () = snd (smt_solver false cx (map (pair ~1) (rules @ prems)))
+      val trace = trace_msg cx (prefix "SMT: " o string_of_failure cx)
     in
-      (if pass_exns then SOME (solve cx)
-       else (SOME (solve cx) handle SMT fail => (trace cx fail; NONE)))
+      (if pass_exns then SOME (solve ())
+       else (SOME (solve ()) handle SMT fail => (trace fail; NONE)))
       |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
-    end
+    end) ctxt
 
 val smt_tac = smt_tac' false