src/HOL/SMT/Tools/smt_solver.ML

--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 08:10:47 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 10:11:30 2009 +0200
@@ -19,9 +19,9 @@
     assms: thm list option }
 
   datatype solver_config = SolverConfig of {
-    name: {env_var: string, remote_name: string},
+    command: {env_var: string, remote_name: string},
+    arguments: string list,
     interface: interface,
-    arguments: string list,
     reconstruct: proof_data -> thm }
 
   (*options*)
@@ -29,6 +29,8 @@
   val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
   val trace: bool Config.T
   val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
+  val keep: string Config.T
+  val cert: string Config.T
 
   (*solvers*)
   type solver = Proof.context -> thm list -> thm
@@ -67,9 +69,9 @@
   assms: thm list option }
 
 datatype solver_config = SolverConfig of {
-  name: {env_var: string, remote_name: string},
+  command: {env_var: string, remote_name: string},
+  arguments: string list,
   interface: interface,
-  arguments: string list,
   reconstruct: proof_data -> thm }
 
 
@@ -86,17 +88,28 @@
 fun trace_msg ctxt f x =
   if Config.get ctxt trace then tracing (f x) else ()
 
+val (keep, setup_keep) = Attrib.config_string "smt_keep" ""
+val (cert, setup_cert) = Attrib.config_string "smt_cert" ""
+
 
 (* interface to external solvers *)
 
 local
 
-fun with_tmp_files f x =
+fun with_files ctxt f x =
   let
-    fun tmp_path () = File.tmp_path (Path.explode ("smt-" ^ serial_string ()))
-    val in_path = tmp_path () and out_path = tmp_path ()
-    val y = Exn.capture (f in_path out_path) x
-    val _ = try File.rm in_path and _ = try File.rm out_path
+    fun make_names n = (n, n ^ ".proof")
+
+    val keep' = Config.get ctxt keep
+    val paths as (problem_path, proof_path) =
+      if keep' <> "" andalso File.exists (Path.dir (Path.explode keep'))
+      then pairself Path.explode (make_names keep')
+      else pairself (File.tmp_path o Path.explode)
+        (make_names ("smt-" ^ serial_string ()))
+
+    val y = Exn.capture (f problem_path proof_path) x
+
+    val _ = if keep' = "" then (pairself (try File.rm) paths; ()) else ()
   in Exn.release y end
 
 fun run in_path out_path (ctxt, cmd, output) =
@@ -115,12 +128,18 @@
 fun run_solver ctxt {env_var, remote_name} args output =
   let
     val qf = File.shell_path and qq = File.shell_quote
-    val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER"
+    val qs = qf o Path.explode
+    val local_name = getenv env_var
+    val cert_name = Config.get ctxt cert
+    val remote = qs (getenv "REMOTE_SMT_SOLVER")
+    val cert_script = qs (getenv "CERT_SMT_SOLVER")
     fun cmd f1 f2 =
-      if path <> ""
-      then map qq (path :: args) @ [qf f1, ">", qf f2]
-      else "perl -w" :: map qq (remote :: remote_name :: args) @ [qf f1, qf f2]
-  in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end
+      if cert_name <> ""
+      then "perl -w" :: [cert_script, qs cert_name, qf f1, ">", qf f2]
+      else if local_name <> ""
+      then qs local_name :: map qq args @ [qf f1, ">", qf f2]
+      else "perl -w" :: remote :: map qq (remote_name :: args) @ [qf f1, qf f2]
+  in with_files ctxt run (ctxt, space_implode " " oo cmd, output) end
 
 end
 
@@ -129,12 +148,12 @@
 
 fun gen_solver solver ctxt prems =
   let
-    val SolverConfig {name, interface, arguments, reconstruct} = solver ctxt
+    val SolverConfig {command, arguments, interface, reconstruct} = solver ctxt
     val Interface {normalize=nc, translate=tc} = interface
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize nc ctxt prems
-    ||> run_solver ctxt name arguments o SMT_Translate.translate tc thy
+    ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy
     ||> reconstruct o make_proof_data ctxt
     |-> fold SMT_Normalize.discharge_definition
   end
@@ -196,8 +215,8 @@
 
 fun pretty_counterex ctxt (real, ex) =
   let
-    val msg = if real then "Counterexample found:"
-      else "Potential counterexample found:"
+    val msg = if real then "SMT: counterexample found:"
+      else "SMT: potential counterexample found:"
     val cex = if null ex then [Pretty.str "(no assignments)"]
       else map (Syntax.pretty_term ctxt) ex
   in Pretty.string_of (Pretty.big_list msg cex) end
@@ -212,6 +231,11 @@
 
 val smt_tac = smt_tac' false
 
+val smt_method =
+  Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) [] >>
+  (fn thms => fn ctxt => METHOD (fn facts =>
+    HEADGOAL (smt_tac ctxt (thms @ facts))))
+
 
 (* setup *)
 
@@ -221,7 +245,11 @@
       (Thm.declaration_attribute o K o select_solver))
     "SMT solver configuration" #>
   setup_timeout #>
-  setup_trace
+  setup_trace #>
+  setup_keep #>
+  setup_cert #>
+  Method.setup (Binding.name "smt") smt_method
+    "Applies an SMT solver to the current goal."
 
 fun print_setup gen =
   let
@@ -243,4 +271,10 @@
       Pretty.big_list "Solver-specific settings:" infos])
   end
 
+val _ = OuterSyntax.improper_command "smt_status"
+  "Show the available SMT solvers and the currently selected solver."
+  OuterKeyword.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
+      print_setup (Context.Proof (Toplevel.context_of state)))))
+
 end