diff -r 6d1ecdb81ff0 -r 8e55aa1306c5 src/HOL/SMT/Tools/z3_solver.ML
--- a/src/HOL/SMT/Tools/z3_solver.ML	Wed May 12 23:54:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(*  Title:      HOL/SMT/Tools/z3_solver.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Interface of the SMT solver Z3.
-*)
-
-signature Z3_SOLVER =
-sig
-  val proofs: bool Config.T
-  val options: string Config.T
-  val setup: theory -> theory
-end
-
-structure Z3_Solver: Z3_SOLVER =
-struct
-
-val solver_name = "z3"
-val env_var = "Z3_SOLVER"
-
-val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
-val (options, options_setup) = Attrib.config_string "z3_options" (K "")
-
-fun add xs ys = ys @ xs
-
-fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
-
-fun get_options ctxt =
-  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
-  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
-  |> add (explode_options (Config.get ctxt options))
-
-fun pretty_config context = [
-  Pretty.str ("With proofs: " ^
-    (if Config.get_generic context proofs then "true" else "false")),
-  Pretty.str ("Options: " ^
-    space_implode " " (get_options (Context.proof_of context))) ]
-
-fun cmdline_options ctxt =
-  get_options ctxt
-  |> add ["-smt"]
-
-fun raise_cex real recon ls =
-  let val cex = Z3_Model.parse_counterex recon ls
-  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
-
-fun if_unsat f (output, recon) =
-  let
-    fun jnk l =
-      String.isPrefix "WARNING" l orelse
-      String.isPrefix "ERROR" l orelse
-      forall Symbol.is_ascii_blank (Symbol.explode l)
-    val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
-  in
-    if String.isPrefix "unsat" l then f (ls, recon)
-    else if String.isPrefix "sat" l then raise_cex true recon ls
-    else if String.isPrefix "unknown" l then raise_cex false recon ls
-    else raise SMT_Solver.SMT (solver_name ^ " failed")
-  end
-
-val core_oracle = if_unsat (K @{cprop False})
-
-val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
-
-fun solver oracle ctxt =
-  let val with_proof = Config.get ctxt proofs
-  in
-   {command = {env_var=env_var, remote_name=SOME solver_name},
-    arguments = cmdline_options ctxt,
-    interface = Z3_Interface.interface,
-    reconstruct = if with_proof then prover else pair o oracle}
-  end
-
-val setup =
-  proofs_setup #>
-  options_setup #>
-  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
-  SMT_Solver.add_solver (solver_name, solver oracle)) #>
-  SMT_Solver.add_solver_info (solver_name, pretty_config)
-
-end