differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
authorboehmes
Thu Jan 06 17:51:56 2011 +0100 (2011-01-06)
changeset 414323214c39777ab
parent 41431 138f414f14cb
child 41433 1b8ff770f02c
differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3");
turned individual SMT solvers into components;
made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only");
tuned smt_filter interface
Admin/contributed_components
NEWS
src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
src/HOL/Boogie/Examples/Boogie_Max.thy
src/HOL/Boogie/Examples/VCC_Max.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/SMT.thy
src/HOL/Tools/SMT/etc/settings
src/HOL/Tools/SMT/lib/scripts/remote_smt
src/HOL/Tools/SMT/smt_config.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/Admin/contributed_components	Tue Jan 04 15:46:38 2011 -0800
     1.2 +++ b/Admin/contributed_components	Thu Jan 06 17:51:56 2011 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4  #contributed components
     1.5 +contrib/cvc3-2.2
     1.6  contrib/e-1.2
     1.7  contrib/jedit-4.3.2
     1.8  contrib/kodkodi-1.2.16
     1.9  contrib/spass-3.7
    1.10  contrib/scala-2.8.0.RC5
    1.11  contrib/vampire-1.0
    1.12 +contrib/z3-2.15
     2.1 --- a/NEWS	Tue Jan 04 15:46:38 2011 -0800
     2.2 +++ b/NEWS	Thu Jan 06 17:51:56 2011 +0100
     2.3 @@ -272,15 +272,31 @@
     2.4  * Auto Solve: Renamed "Auto Solve Direct".  The tool is now available
     2.5  manually as command 'solve_direct'.
     2.6  
     2.7 +* The default SMT solver is now CVC3.  Z3 must be enabled explicitly,
     2.8 +due to licensing issues.
     2.9 +
    2.10 +* Remote SMT solvers need to be referred to by the "remote_" prefix,
    2.11 +i.e., "remote_cvc3" and "remote_z3".
    2.12 +
    2.13 +* Added basic SMT support for datatypes, records, and typedefs
    2.14 +using the oracle mode (no proofs).  Direct support of pairs has been
    2.15 +dropped in exchange (pass theorems fst_conv snd_conv pair_collapse to
    2.16 +the SMT support for a similar behaviour).  MINOR INCOMPATIBILITY.
    2.17 +
    2.18  * Changed SMT configuration options:
    2.19    - Renamed:
    2.20 -    z3_proofs ~> smt_oracle (with swapped semantics)
    2.21 +    z3_proofs ~> smt_oracle (with inverted meaning)
    2.22      z3_trace_assms ~> smt_trace_used_facts
    2.23      INCOMPATIBILITY.
    2.24    - Added:
    2.25      smt_verbose
    2.26 +    smt_random_seed
    2.27      smt_datatypes
    2.28 +    smt_infer_triggers
    2.29 +    smt_monomorph_limit
    2.30      cvc3_options
    2.31 +    remote_cvc3_options
    2.32 +    remote_z3_options
    2.33      yices_options
    2.34  
    2.35  * Boogie output files (.b2i files) need to be declared in the theory
     3.1 --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Jan 04 15:46:38 2011 -0800
     3.2 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Thu Jan 06 17:51:56 2011 +0100
     3.3 @@ -84,7 +84,7 @@
     3.4  
     3.5  declare [[smt_certificates="Boogie_Dijkstra.certs"]]
     3.6  declare [[smt_fixed=true]]
     3.7 -declare [[smt_oracle=false]]
     3.8 +declare [[smt_solver=z3, smt_oracle=false]]
     3.9  
    3.10  boogie_vc Dijkstra
    3.11    by boogie
     4.1 --- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Jan 04 15:46:38 2011 -0800
     4.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Thu Jan 06 17:51:56 2011 +0100
     4.3 @@ -41,7 +41,7 @@
     4.4  
     4.5  declare [[smt_certificates="Boogie_Max.certs"]]
     4.6  declare [[smt_fixed=true]]
     4.7 -declare [[smt_oracle=false]]
     4.8 +declare [[smt_solver=z3, smt_oracle=false]]
     4.9  
    4.10  boogie_vc max
    4.11    by boogie
     5.1 --- a/src/HOL/Boogie/Examples/VCC_Max.thy	Tue Jan 04 15:46:38 2011 -0800
     5.2 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy	Thu Jan 06 17:51:56 2011 +0100
     5.3 @@ -49,7 +49,7 @@
     5.4  
     5.5  declare [[smt_certificates="VCC_Max.certs"]]
     5.6  declare [[smt_fixed=true]]
     5.7 -declare [[smt_oracle=false]]
     5.8 +declare [[smt_solver=z3, smt_oracle=false]]
     5.9  
    5.10  boogie_status
    5.11  
     6.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jan 04 15:46:38 2011 -0800
     6.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Jan 06 17:51:56 2011 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4  
     6.5  declare [[smt_certificates="Integration.certs"]]
     6.6  declare [[smt_fixed=true]]
     6.7 -declare [[smt_oracle=false]]
     6.8 +declare [[smt_solver=z3, smt_oracle=false]]
     6.9  
    6.10  setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
    6.11  
    6.12 @@ -5527,5 +5527,6 @@
    6.13  
    6.14  declare [[smt_certificates=""]]
    6.15  declare [[smt_fixed=false]]
    6.16 +declare [[smt_solver=cvc3]]
    6.17  
    6.18  end
     7.1 --- a/src/HOL/SMT.thy	Tue Jan 04 15:46:38 2011 -0800
     7.2 +++ b/src/HOL/SMT.thy	Thu Jan 06 17:51:56 2011 +0100
     7.3 @@ -176,17 +176,11 @@
     7.4  
     7.5  text {*
     7.6  The option @{text smt_solver} can be used to change the target SMT
     7.7 -solver.  The possible values are @{text cvc3}, @{text yices}, and
     7.8 -@{text z3}.  It is advisable to locally install the selected solver,
     7.9 -although this is not necessary for @{text cvc3} and @{text z3}, which
    7.10 -can also be used over an Internet-based service.
    7.11 -
    7.12 -When using local SMT solvers, the path to their binaries should be
    7.13 -declared by setting the following environment variables:
    7.14 -@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}.
    7.15 +solver.  The possible values can be obtained from the @{text smt_status}
    7.16 +command.
    7.17  *}
    7.18  
    7.19 -declare [[ smt_solver = z3 ]]
    7.20 +declare [[ smt_solver = cvc3 ]]
    7.21  
    7.22  text {*
    7.23  Since SMT solvers are potentially non-terminating, there is a timeout
    7.24 @@ -218,7 +212,9 @@
    7.25  options.
    7.26  *}
    7.27  
    7.28 -declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
    7.29 +declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
    7.30 +declare [[ yices_options = "" ]]
    7.31 +declare [[ z3_options = "", remote_z3_options = "" ]]
    7.32  
    7.33  text {*
    7.34  Enable the following option to use built-in support for datatypes and
     8.1 --- a/src/HOL/Tools/SMT/etc/settings	Tue Jan 04 15:46:38 2011 -0800
     8.2 +++ b/src/HOL/Tools/SMT/etc/settings	Thu Jan 06 17:51:56 2011 +0100
     8.3 @@ -2,14 +2,6 @@
     8.4  
     8.5  ISABELLE_SMT="$COMPONENT"
     8.6  
     8.7 -REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt"
     8.8 -
     8.9 -REMOTE_SMT_URL="http://smt.in.tum.de/smt"
    8.10 +ISABELLE_SMT_REMOTE="$ISABELLE_SMT/lib/scripts/remote_smt"
    8.11 +ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt"
    8.12  
    8.13 -#
    8.14 -# Paths to local SMT solvers:
    8.15 -#
    8.16 -# CVC_SOLVER=PATH
    8.17 -# YICES_SOLVER=PATH
    8.18 -# Z3_SOLVER=PATH
    8.19 -
     9.1 --- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Tue Jan 04 15:46:38 2011 -0800
     9.2 +++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt	Thu Jan 06 17:51:56 2011 +0100
     9.3 @@ -21,7 +21,7 @@
     9.4  my $agent = LWP::UserAgent->new;
     9.5  $agent->agent("SMT-Request");
     9.6  $agent->timeout(180);
     9.7 -my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [
     9.8 +my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [
     9.9    "Solver" => $solver,
    9.10    "Options" => join(" ", @options),
    9.11    "Problem" => [$problem_file] ],
    10.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Tue Jan 04 15:46:38 2011 -0800
    10.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Jan 06 17:51:56 2011 +0100
    10.3 @@ -7,9 +7,14 @@
    10.4  signature SMT_CONFIG =
    10.5  sig
    10.6    (*solver*)
    10.7 -  val add_solver: string * SMT_Utils.class -> Context.generic ->
    10.8 -    Context.generic
    10.9 +  type solver_info = {
   10.10 +    name: string,
   10.11 +    class: SMT_Utils.class,
   10.12 +    avail: unit -> bool,
   10.13 +    options: Proof.context -> string list }
   10.14 +  val add_solver: solver_info -> Context.generic -> Context.generic
   10.15    val set_solver_options: string * string -> Context.generic -> Context.generic
   10.16 +  val available_solvers_of: Proof.context -> string list
   10.17    val select_solver: string -> Context.generic -> Context.generic
   10.18    val solver_of: Proof.context -> string
   10.19    val solver_class_of: Proof.context -> SMT_Utils.class
   10.20 @@ -52,9 +57,15 @@
   10.21  
   10.22  (* solver *)
   10.23  
   10.24 +type solver_info = {
   10.25 +  name: string,
   10.26 +  class: SMT_Utils.class,
   10.27 +  avail: unit -> bool,
   10.28 +  options: Proof.context -> string list }
   10.29 +
   10.30  structure Solvers = Generic_Data
   10.31  (
   10.32 -  type T = (SMT_Utils.class * string list) Symtab.table * string option
   10.33 +  type T = (solver_info * string list) Symtab.table * string option
   10.34    val empty = (Symtab.empty, NONE)
   10.35    val extend = I
   10.36    fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
   10.37 @@ -64,39 +75,71 @@
   10.38    let val opts = String.tokens (Symbol.is_ascii_blank o str) options
   10.39    in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
   10.40  
   10.41 -fun add_solver (name, class) context =
   10.42 +fun add_solver (info as {name, ...} : solver_info) context =
   10.43    if Symtab.defined (fst (Solvers.get context)) name then
   10.44      error ("Solver already registered: " ^ quote name)
   10.45    else
   10.46      context
   10.47 -    |> Solvers.map (apfst (Symtab.update (name, (class, []))))
   10.48 +    |> Solvers.map (apfst (Symtab.update (name, (info, []))))
   10.49      |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
   10.50          (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   10.51            (Thm.declaration_attribute o K o set_solver_options o pair name))
   10.52          ("Additional command line options for SMT solver " ^ quote name))
   10.53  
   10.54 +fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
   10.55 +
   10.56 +fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
   10.57 +
   10.58 +fun is_available ctxt name =
   10.59 +  (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
   10.60 +    SOME ({avail, ...}, _) => avail ()
   10.61 +  | NONE => false)
   10.62 +
   10.63 +fun available_solvers_of ctxt =
   10.64 +  filter (is_available ctxt) (all_solvers_of ctxt)
   10.65 +
   10.66 +fun warn_solver name =
   10.67 +  let
   10.68 +    fun app p n = Path.append p (Path.explode n)
   10.69 +    val path = Path.explode (getenv "ISABELLE_HOME_USER")
   10.70 +    val path' = app (app path "etc") "components"
   10.71 +  in
   10.72 +    warning ("The SMT solver " ^ quote name ^ " is not installed. " ^
   10.73 +      "Please add the path to its component bundle to " ^
   10.74 +      "the components list in " ^ quote (Path.implode path') ^ ".")
   10.75 +  end
   10.76 +
   10.77  fun select_solver name context =
   10.78 -  if Symtab.defined (fst (Solvers.get context)) name then
   10.79 -    Solvers.map (apsnd (K (SOME name))) context
   10.80 -  else error ("Trying to select unknown solver: " ^ quote name)
   10.81 +  let
   10.82 +    val ctxt = Context.proof_of context
   10.83 +    val upd = Solvers.map (apsnd (K (SOME name)))
   10.84 +  in
   10.85 +    if not (member (op =) (all_solvers_of ctxt) name) then
   10.86 +      error ("Trying to select unknown solver: " ^ quote name)
   10.87 +    else if not (is_available ctxt name) then (warn_solver name; upd context)
   10.88 +    else upd context
   10.89 +  end
   10.90  
   10.91  fun no_solver_err () = error "No SMT solver selected"
   10.92  
   10.93  fun solver_of ctxt =
   10.94 +  (case solver_name_of ctxt of
   10.95 +    SOME name => name
   10.96 +  | NONE => no_solver_err ())
   10.97 +
   10.98 +fun solver_info_of default select ctxt =
   10.99    (case Solvers.get (Context.Proof ctxt) of
  10.100 -    (_, SOME name) => name
  10.101 -  | (_, NONE) => no_solver_err ())
  10.102 +    (solvers, SOME name) => select (Symtab.lookup solvers name)
  10.103 +  | (_, NONE) => default ())
  10.104  
  10.105  fun solver_class_of ctxt =
  10.106 -  (case Solvers.get (Context.Proof ctxt) of
  10.107 -    (solvers, SOME name) => fst (the (Symtab.lookup solvers name))
  10.108 -  | (_, NONE) => no_solver_err())
  10.109 +  solver_info_of no_solver_err (#class o fst o the) ctxt
  10.110  
  10.111  fun solver_options_of ctxt =
  10.112 -  (case Solvers.get (Context.Proof ctxt) of
  10.113 -    (solvers, SOME name) =>
  10.114 -      (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => [])
  10.115 -  | (_, NONE) => [])
  10.116 +  let
  10.117 +    fun all_options NONE = []
  10.118 +      | all_options (SOME ({options, ...}, opts)) = opts @ options ctxt
  10.119 +  in solver_info_of (K []) all_options ctxt end
  10.120  
  10.121  val setup_solver =
  10.122    Attrib.setup @{binding smt_solver}
  10.123 @@ -224,9 +267,9 @@
  10.124    let
  10.125      fun string_of_bool b = if b then "true" else "false"
  10.126  
  10.127 -    val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys
  10.128 +    val names = available_solvers_of ctxt
  10.129      val ns = if null names then ["(none)"] else sort_strings names
  10.130 -    val n = the_default "(none)" sel
  10.131 +    val n = the_default "(none)" (solver_name_of ctxt)
  10.132      val opts = solver_options_of ctxt
  10.133      
  10.134      val t = string_of_real (Config.get ctxt timeout)
    11.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Jan 04 15:46:38 2011 -0800
    11.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Thu Jan 06 17:51:56 2011 +0100
    11.3 @@ -12,6 +12,23 @@
    11.4  structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
    11.5  struct
    11.6  
    11.7 +(* helper functions *)
    11.8 +
    11.9 +val remote_prefix = "remote_"
   11.10 +fun make_name is_remote name = name |> is_remote ? prefix remote_prefix
   11.11 +
   11.12 +fun make_local_avail name () = getenv (name ^ "_INSTALLED") = "yes"
   11.13 +fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
   11.14 +fun make_avail is_remote name =
   11.15 +  if is_remote then make_remote_avail name else make_local_avail name
   11.16 +
   11.17 +fun make_local_command name () = [getenv (name ^ "_SOLVER")]
   11.18 +fun make_remote_command name () =
   11.19 +  [getenv "ISABELLE_SMT_REMOTE", getenv (name ^ "_REMOTE_SOLVER")]
   11.20 +fun make_command is_remote name =
   11.21 +  if is_remote then make_remote_command name
   11.22 +  else make_local_command name
   11.23 +
   11.24  fun outcome_of unsat sat unknown solver_name line =
   11.25    if String.isPrefix unsat line then SMT_Solver.Unsat
   11.26    else if String.isPrefix sat line then SMT_Solver.Sat
   11.27 @@ -31,76 +48,97 @@
   11.28  
   11.29  (* CVC3 *)
   11.30  
   11.31 -fun cvc3 () = {
   11.32 -  name = "cvc3",
   11.33 -  env_var = "CVC3_SOLVER",
   11.34 -  is_remote = true,
   11.35 -  options = (fn ctxt => [
   11.36 +local
   11.37 +  fun cvc3_options ctxt = [
   11.38      "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
   11.39 -    "-lang", "smtlib", "-output-lang", "presentation"]),
   11.40 -  class = SMTLIB_Interface.smtlibC,
   11.41 -  outcome =
   11.42 -    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   11.43 -  cex_parser = NONE,
   11.44 -  reconstruct = NONE,
   11.45 -  default_max_relevant = 250 }
   11.46 +    "-lang", "smtlib", "-output-lang", "presentation"]
   11.47 +
   11.48 +  fun mk is_remote = {
   11.49 +    name = make_name is_remote "cvc3",
   11.50 +    class = SMTLIB_Interface.smtlibC,
   11.51 +    avail = make_avail is_remote "CVC3",
   11.52 +    command = make_command is_remote "CVC3",
   11.53 +    options = cvc3_options,
   11.54 +    default_max_relevant = 250,
   11.55 +    supports_filter = false,
   11.56 +    outcome =
   11.57 +      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
   11.58 +    cex_parser = NONE,
   11.59 +    reconstruct = NONE }
   11.60 +in
   11.61 +
   11.62 +fun cvc3 () = mk false
   11.63 +fun remote_cvc3 () = mk true
   11.64 +
   11.65 +end
   11.66  
   11.67  
   11.68  (* Yices *)
   11.69  
   11.70  fun yices () = {
   11.71    name = "yices",
   11.72 -  env_var = "YICES_SOLVER",
   11.73 -  is_remote = false,
   11.74 +  class = SMTLIB_Interface.smtlibC,
   11.75 +  avail = make_local_avail "YICES",
   11.76 +  command = make_local_command "YICES",
   11.77    options = (fn ctxt => [
   11.78      "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
   11.79      "--smtlib"]),
   11.80 -  class = SMTLIB_Interface.smtlibC,
   11.81 +  default_max_relevant = 275,
   11.82 +  supports_filter = false,
   11.83    outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   11.84    cex_parser = NONE,
   11.85 -  reconstruct = NONE,
   11.86 -  default_max_relevant = 275 }
   11.87 +  reconstruct = NONE }
   11.88  
   11.89  
   11.90  (* Z3 *)
   11.91  
   11.92 -fun z3_options ctxt =
   11.93 -  ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
   11.94 -    "MODEL=true", "-smt"]
   11.95 -  |> not (Config.get ctxt SMT_Config.oracle) ?
   11.96 -       append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
   11.97 +local
   11.98 +  fun z3_options ctxt =
   11.99 +    ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
  11.100 +      "MODEL=true", "-smt"]
  11.101 +    |> not (Config.get ctxt SMT_Config.oracle) ?
  11.102 +         append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
  11.103  
  11.104 -fun z3_on_last_line solver_name lines =
  11.105 -  let
  11.106 -    fun junk l =
  11.107 -      if String.isPrefix "WARNING: Out of allocated virtual memory" l
  11.108 -      then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
  11.109 -      else
  11.110 -        String.isPrefix "WARNING" l orelse
  11.111 -        String.isPrefix "ERROR" l orelse
  11.112 -        forall Symbol.is_ascii_blank (Symbol.explode l)
  11.113 -  in
  11.114 -    the_default ("", []) (try (swap o split_last) (filter_out junk lines))
  11.115 -    |>> outcome_of "unsat" "sat" "unknown" solver_name
  11.116 -  end
  11.117 +  fun z3_on_last_line solver_name lines =
  11.118 +    let
  11.119 +      fun junk l =
  11.120 +        if String.isPrefix "WARNING: Out of allocated virtual memory" l
  11.121 +        then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
  11.122 +        else
  11.123 +          String.isPrefix "WARNING" l orelse
  11.124 +          String.isPrefix "ERROR" l orelse
  11.125 +          forall Symbol.is_ascii_blank (Symbol.explode l)
  11.126 +    in
  11.127 +      the_default ("", []) (try (swap o split_last) (filter_out junk lines))
  11.128 +      |>> outcome_of "unsat" "sat" "unknown" solver_name
  11.129 +    end
  11.130  
  11.131 -fun z3 () = {
  11.132 -  name = "z3",
  11.133 -  env_var = "Z3_SOLVER",
  11.134 -  is_remote = true,
  11.135 -  options = z3_options,
  11.136 -  class = Z3_Interface.smtlib_z3C,
  11.137 -  outcome = z3_on_last_line,
  11.138 -  cex_parser = SOME Z3_Model.parse_counterex,
  11.139 -  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
  11.140 -  default_max_relevant = 225 }
  11.141 +  fun mk is_remote = {
  11.142 +    name = make_name is_remote "z3",
  11.143 +    class = Z3_Interface.smtlib_z3C,
  11.144 +    avail = make_avail is_remote "Z3",
  11.145 +    command = make_command is_remote "Z3",
  11.146 +    options = z3_options,
  11.147 +    default_max_relevant = 225,
  11.148 +    supports_filter = true,
  11.149 +    outcome = z3_on_last_line,
  11.150 +    cex_parser = SOME Z3_Model.parse_counterex,
  11.151 +    reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
  11.152 +in
  11.153 +
  11.154 +fun z3 () = mk false
  11.155 +fun remote_z3 () = mk true
  11.156 +
  11.157 +end
  11.158  
  11.159  
  11.160  (* overall setup *)
  11.161  
  11.162  val setup =
  11.163    SMT_Solver.add_solver (cvc3 ()) #>
  11.164 +  SMT_Solver.add_solver (remote_cvc3 ()) #>
  11.165    SMT_Solver.add_solver (yices ()) #>
  11.166 -  SMT_Solver.add_solver (z3 ())
  11.167 +  SMT_Solver.add_solver (z3 ()) #>
  11.168 +  SMT_Solver.add_solver (remote_z3 ())
  11.169  
  11.170  end
    12.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Jan 04 15:46:38 2011 -0800
    12.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Thu Jan 06 17:51:56 2011 +0100
    12.3 @@ -10,39 +10,37 @@
    12.4    datatype outcome = Unsat | Sat | Unknown
    12.5    type solver_config = {
    12.6      name: string,
    12.7 -    env_var: string,
    12.8 -    is_remote: bool,
    12.9 +    class: SMT_Utils.class,
   12.10 +    avail: unit -> bool,
   12.11 +    command: unit -> string list,
   12.12      options: Proof.context -> string list,
   12.13 -    class: SMT_Utils.class,
   12.14 +    default_max_relevant: int,
   12.15 +    supports_filter: bool,
   12.16      outcome: string -> string list -> outcome * string list,
   12.17      cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
   12.18        term list * term list) option,
   12.19      reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
   12.20 -      int list * thm) option,
   12.21 -    default_max_relevant: int }
   12.22 +      int list * thm) option }
   12.23  
   12.24    (*registry*)
   12.25 -  type solver = bool option -> Proof.context ->
   12.26 -    (int * (int option * thm)) list -> int list * thm
   12.27    val add_solver: solver_config -> theory -> theory
   12.28    val solver_name_of: Proof.context -> string
   12.29 -  val solver_of: Proof.context -> solver
   12.30    val available_solvers_of: Proof.context -> string list
   12.31 -  val is_locally_installed: Proof.context -> string -> bool
   12.32 -  val is_remotely_available: Proof.context -> string -> bool
   12.33 +  val apply_solver: Proof.context -> (int * (int option * thm)) list ->
   12.34 +    int list * thm
   12.35    val default_max_relevant: Proof.context -> string -> int
   12.36  
   12.37    (*filter*)
   12.38 -  type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
   12.39 -    (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
   12.40 -  val smt_filter_head: Proof.state ->
   12.41 -    ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result
   12.42 -  val smt_filter_tail: Time.time -> bool -> 'a smt_filter_head_result ->
   12.43 +  type 'a smt_filter_data =
   12.44 +    ('a * thm) list * ((int * thm) list * Proof.context)
   12.45 +  val smt_filter_preprocess: Proof.state ->
   12.46 +    ('a * (int option * thm)) list -> int -> 'a smt_filter_data
   12.47 +  val smt_filter_apply: Time.time -> 'a smt_filter_data ->
   12.48      {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list}
   12.49  
   12.50    (*tactic*)
   12.51 -  val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
   12.52    val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic
   12.53 +  val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic
   12.54  
   12.55    (*setup*)
   12.56    val setup: theory -> theory
   12.57 @@ -52,88 +50,43 @@
   12.58  struct
   12.59  
   12.60  
   12.61 -(* configuration *)
   12.62 -
   12.63 -datatype outcome = Unsat | Sat | Unknown
   12.64 -
   12.65 -type solver_config = {
   12.66 -  name: string,
   12.67 -  env_var: string,
   12.68 -  is_remote: bool,
   12.69 -  options: Proof.context -> string list,
   12.70 -  class: SMT_Utils.class,
   12.71 -  outcome: string -> string list -> outcome * string list,
   12.72 -  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
   12.73 -    term list * term list) option,
   12.74 -  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
   12.75 -    int list * thm) option,
   12.76 -  default_max_relevant: int }
   12.77 -
   12.78 -
   12.79  (* interface to external solvers *)
   12.80  
   12.81 -fun get_local_solver env_var =
   12.82 -  let val local_solver = getenv env_var
   12.83 -  in if local_solver <> "" then SOME local_solver else NONE end
   12.84 -
   12.85  local
   12.86  
   12.87 -fun choose (rm, env_var, is_remote, name) =
   12.88 -  let
   12.89 -    val force_local = (case rm of SOME false => true | _ => false)
   12.90 -    val force_remote = (case rm of SOME true => true | _ => false)
   12.91 -    val lsolver = get_local_solver env_var
   12.92 -    val remote_url = getenv "REMOTE_SMT_URL"
   12.93 -    val trace = if is_some rm then K () else tracing
   12.94 -  in
   12.95 -    if not force_remote andalso is_some lsolver
   12.96 -    then 
   12.97 -     (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ...");
   12.98 -      [the lsolver])
   12.99 -    else if not force_local andalso is_remote
  12.100 -    then
  12.101 -     (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^
  12.102 -        quote remote_url ^ " ...");
  12.103 -      [getenv "REMOTE_SMT", name])
  12.104 -    else if force_remote
  12.105 -    then error ("The SMT solver " ^ quote name ^ " is not remotely available.")
  12.106 -    else error ("The SMT solver " ^ quote name ^ " has not been found " ^
  12.107 -      "on this computer. Please set the Isabelle environment variable " ^
  12.108 -      quote env_var ^ ".")
  12.109 -  end
  12.110 -
  12.111 -fun make_cmd solver args problem_path proof_path = space_implode " " (
  12.112 -  map File.shell_quote (solver @ args) @
  12.113 +fun make_cmd command options problem_path proof_path = space_implode " " (
  12.114 +  map File.shell_quote (command @ options) @
  12.115    [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
  12.116  
  12.117 -fun run ctxt cmd args input =
  12.118 +fun trace_and ctxt msg f x =
  12.119 +  let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
  12.120 +  in f x end
  12.121 +
  12.122 +fun run ctxt name mk_cmd input =
  12.123    (case SMT_Config.certificates_of ctxt of
  12.124      NONE =>
  12.125        if Config.get ctxt SMT_Config.debug_files = "" then
  12.126 -        Cache_IO.run (make_cmd (choose cmd) args) input
  12.127 +        trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...")
  12.128 +          (Cache_IO.run mk_cmd) input
  12.129        else
  12.130          let
  12.131            val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files)
  12.132            val in_path = Path.ext "smt_in" base_path
  12.133            val out_path = Path.ext "smt_out" base_path
  12.134 -        in
  12.135 -          Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path 
  12.136 -        end
  12.137 +        in Cache_IO.raw_run mk_cmd input in_path out_path end
  12.138    | SOME certs =>
  12.139        (case Cache_IO.lookup certs input of
  12.140          (NONE, key) =>
  12.141            if Config.get ctxt SMT_Config.fixed then
  12.142              error ("Bad certificates cache: missing certificate")
  12.143            else
  12.144 -            Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input
  12.145 +            Cache_IO.run_and_cache certs key mk_cmd input
  12.146        | (SOME output, _) =>
  12.147 -         (tracing ("Using cached certificate from " ^
  12.148 -            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
  12.149 -          output)))
  12.150 +          trace_and ctxt ("Using cached certificate from " ^
  12.151 +            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...")
  12.152 +            I output))
  12.153  
  12.154 -in
  12.155 -
  12.156 -fun run_solver ctxt cmd args input =
  12.157 +fun run_solver ctxt name mk_cmd input =
  12.158    let
  12.159      fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
  12.160        (map Pretty.str ls))
  12.161 @@ -141,7 +94,7 @@
  12.162      val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input
  12.163  
  12.164      val {redirected_output=res, output=err, return_code} =
  12.165 -      SMT_Config.with_timeout ctxt (run ctxt cmd args) input
  12.166 +      SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input
  12.167      val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err
  12.168  
  12.169      val ls = rev (snd (chop_while (equal "") (rev res)))
  12.170 @@ -151,8 +104,6 @@
  12.171        raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code)
  12.172    in ls end
  12.173  
  12.174 -end
  12.175 -
  12.176  fun trace_assms ctxt =
  12.177    SMT_Config.trace_msg ctxt (Pretty.string_of o
  12.178      Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd))
  12.179 @@ -169,65 +120,54 @@
  12.180          Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) ()
  12.181    end
  12.182  
  12.183 -fun invoke name cmd options ithms ctxt =
  12.184 +in
  12.185 +
  12.186 +fun invoke name command ithms ctxt =
  12.187    let
  12.188 -    val args = SMT_Config.solver_options_of ctxt @ options ctxt
  12.189 +    val options = SMT_Config.solver_options_of ctxt
  12.190      val comments = ("solver: " ^ name) ::
  12.191        ("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) ::
  12.192        ("random seed: " ^
  12.193          string_of_int (Config.get ctxt SMT_Config.random_seed)) ::
  12.194 -      "arguments:" :: args
  12.195 +      "arguments:" :: options
  12.196  
  12.197      val (str, recon as {context=ctxt', ...}) =
  12.198        ithms
  12.199        |> tap (trace_assms ctxt)
  12.200        |> SMT_Translate.translate ctxt comments
  12.201        ||> tap trace_recon_data
  12.202 -  in (run_solver ctxt' cmd args str, recon) end
  12.203 +  in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end
  12.204 +
  12.205 +end
  12.206 +
  12.207 +
  12.208 +(* configuration *)
  12.209 +
  12.210 +datatype outcome = Unsat | Sat | Unknown
  12.211  
  12.212 -fun trace_assumptions ctxt iwthms idxs =
  12.213 -  let
  12.214 -    val wthms =
  12.215 -      idxs
  12.216 -      |> filter (fn i => i >= 0)
  12.217 -      |> map_filter (AList.lookup (op =) iwthms)
  12.218 -  in
  12.219 -    if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0
  12.220 -    then
  12.221 -      tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
  12.222 -        (map (Display.pretty_thm ctxt o snd) wthms)))
  12.223 -    else ()
  12.224 -  end
  12.225 -
  12.226 +type solver_config = {
  12.227 +  name: string,
  12.228 +  class: SMT_Utils.class,
  12.229 +  avail: unit -> bool,
  12.230 +  command: unit -> string list,
  12.231 +  options: Proof.context -> string list,
  12.232 +  default_max_relevant: int,
  12.233 +  supports_filter: bool,
  12.234 +  outcome: string -> string list -> outcome * string list,
  12.235 +  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
  12.236 +    term list * term list) option,
  12.237 +  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
  12.238 +    int list * thm) option }
  12.239  
  12.240  
  12.241  (* registry *)
  12.242  
  12.243 -type solver = bool option -> Proof.context -> (int * (int option * thm)) list ->
  12.244 -  int list * thm
  12.245 -
  12.246  type solver_info = {
  12.247 -  env_var: string,
  12.248 -  is_remote: bool,
  12.249 -  options: Proof.context -> string list,
  12.250 +  command: unit -> string list,
  12.251 +  default_max_relevant: int,
  12.252 +  supports_filter: bool,
  12.253    reconstruct: Proof.context -> string list * SMT_Translate.recon ->
  12.254 -    int list * thm,
  12.255 -  default_max_relevant: int }
  12.256 -
  12.257 -fun gen_solver_head ctxt iwthms = SMT_Normalize.normalize iwthms ctxt
  12.258 -
  12.259 -fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms =
  12.260 -  let
  12.261 -    val {env_var, is_remote, options, reconstruct, ...} = info
  12.262 -    val cmd = (rm, env_var, is_remote, name)
  12.263 -  in
  12.264 -    (iwthms', ctxt)
  12.265 -    |-> invoke name cmd options
  12.266 -    |> reconstruct ctxt
  12.267 -    |> (fn (idxs, thm) => thm
  12.268 -    |> tap (fn _ => trace_assumptions ctxt iwthms idxs)
  12.269 -    |> pair idxs)
  12.270 -  end
  12.271 +    int list * thm }
  12.272  
  12.273  structure Solvers = Generic_Data
  12.274  (
  12.275 @@ -262,18 +202,22 @@
  12.276  
  12.277  fun add_solver cfg =
  12.278    let
  12.279 -    val {name, env_var, is_remote, options, class, outcome, cex_parser,
  12.280 -      reconstruct, default_max_relevant} = cfg
  12.281 +    val {name, class, avail, command, options, default_max_relevant,
  12.282 +      supports_filter, outcome, cex_parser, reconstruct} = cfg
  12.283  
  12.284      fun core_oracle () = cfalse
  12.285  
  12.286 -    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
  12.287 -      reconstruct=finish (outcome name) cex_parser reconstruct ocl,
  12.288 -      default_max_relevant=default_max_relevant }
  12.289 +    fun solver ocl = {
  12.290 +      command = command,
  12.291 +      default_max_relevant = default_max_relevant,
  12.292 +      supports_filter = supports_filter,
  12.293 +      reconstruct = finish (outcome name) cex_parser reconstruct ocl }
  12.294 +
  12.295 +    val info = {name=name, class=class, avail=avail, options=options}
  12.296    in
  12.297      Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
  12.298      Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
  12.299 -    Context.theory_map (SMT_Config.add_solver (name, class))
  12.300 +    Context.theory_map (SMT_Config.add_solver info)
  12.301    end
  12.302  
  12.303  end
  12.304 @@ -281,26 +225,33 @@
  12.305  fun get_info ctxt name =
  12.306    the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name)
  12.307  
  12.308 -fun name_and_solver_of ctxt =
  12.309 -  let val name = SMT_Config.solver_of ctxt
  12.310 +val solver_name_of = SMT_Config.solver_of
  12.311 +
  12.312 +val available_solvers_of = SMT_Config.available_solvers_of
  12.313 +
  12.314 +fun name_and_info_of ctxt =
  12.315 +  let val name = solver_name_of ctxt
  12.316    in (name, get_info ctxt name) end
  12.317  
  12.318 -val solver_name_of = fst o name_and_solver_of
  12.319 -fun solver_of ctxt rm ctxt' =
  12.320 -  `(gen_solver_head ctxt') #-> gen_solver_tail (name_and_solver_of ctxt) rm
  12.321 -
  12.322 -val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof
  12.323 +fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt
  12.324  
  12.325 -fun is_locally_installed ctxt name =
  12.326 -  let val {env_var, ...} = get_info ctxt name
  12.327 -  in is_some (get_local_solver env_var) end
  12.328 +fun gen_apply (ithms, ctxt) =
  12.329 +  let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt
  12.330 +  in
  12.331 +    (ithms, ctxt)
  12.332 +    |-> invoke name command
  12.333 +    |> reconstruct ctxt
  12.334 +    |>> distinct (op =)
  12.335 +  end
  12.336  
  12.337 -val is_remotely_available = #is_remote oo get_info
  12.338 +fun apply_solver ctxt = gen_apply o gen_preprocess ctxt
  12.339  
  12.340  val default_max_relevant = #default_max_relevant oo get_info
  12.341  
  12.342 +val supports_filter = #supports_filter o snd o name_and_info_of 
  12.343  
  12.344 -(* filter *)
  12.345 +
  12.346 +(* check well-sortedness *)
  12.347  
  12.348  val has_topsort = Term.exists_type (Term.exists_subtype (fn
  12.349      TFree (_, []) => true
  12.350 @@ -312,17 +263,18 @@
  12.351    if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then
  12.352      raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^
  12.353        "contains the universal sort {}"))
  12.354 -  else
  12.355 -    ()
  12.356 +  else ()
  12.357 +
  12.358 +
  12.359 +(* filter *)
  12.360  
  12.361  val cnot = Thm.cterm_of @{theory} @{const Not}
  12.362  
  12.363  fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
  12.364  
  12.365 -type 'a smt_filter_head_result = ('a list * (int option * thm) list) *
  12.366 -  (((int * thm) list * Proof.context) * (int * (int option * thm)) list)
  12.367 +type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context)
  12.368  
  12.369 -fun smt_filter_head st xwrules i =
  12.370 +fun smt_filter_preprocess st xwthms i =
  12.371    let
  12.372      val ctxt =
  12.373        Proof.context_of st
  12.374 @@ -334,28 +286,27 @@
  12.375      val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
  12.376      fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
  12.377      val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
  12.378 -
  12.379 -    val (xs, wthms) = split_list xwrules
  12.380    in
  12.381 -    ((xs, wthms),
  12.382 -     wthms
  12.383 -     |> map_index I
  12.384 -     |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
  12.385 -     |> tap check_topsort
  12.386 -     |> `(gen_solver_head ctxt'))
  12.387 +    map snd xwthms
  12.388 +    |> map_index I
  12.389 +    |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
  12.390 +    |> tap check_topsort
  12.391 +    |> gen_preprocess ctxt'
  12.392 +    |> pair (map (apsnd snd) xwthms)
  12.393    end
  12.394  
  12.395 -fun smt_filter_tail time_limit run_remote
  12.396 -    ((xs, wthms), ((iwthms', ctxt), iwthms)) =
  12.397 +fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) =
  12.398    let
  12.399 -    val ctxt = ctxt |> Config.put SMT_Config.timeout (Time.toReal time_limit)
  12.400 -    val xrules = xs ~~ map snd wthms
  12.401 +    val ctxt' =
  12.402 +      ctxt
  12.403 +      |> Config.put SMT_Config.timeout (Time.toReal time_limit)
  12.404 +
  12.405 +    fun filter_thms false = K xthms
  12.406 +      | filter_thms true = map_filter (try (nth xthms)) o fst
  12.407    in
  12.408 -    ((iwthms', ctxt), iwthms)
  12.409 -    |-> gen_solver_tail (name_and_solver_of ctxt) (SOME run_remote)
  12.410 -    |> distinct (op =) o fst
  12.411 -    |> map_filter (try (nth xrules))
  12.412 -    |> (if solver_name_of ctxt = "z3" (* FIXME *) then I else K xrules)
  12.413 +    (ithms, ctxt')
  12.414 +    |> gen_apply
  12.415 +    |> filter_thms (supports_filter ctxt')
  12.416      |> mk_result NONE
  12.417    end
  12.418    handle SMT_Failure.SMT fail => mk_result (SOME fail) []
  12.419 @@ -363,28 +314,57 @@
  12.420  
  12.421  (* SMT tactic *)
  12.422  
  12.423 -fun smt_tac' pass_exns ctxt rules =
  12.424 -  CONVERSION (SMT_Normalize.atomize_conv ctxt)
  12.425 -  THEN' Tactic.rtac @{thm ccontr}
  12.426 -  THEN' SUBPROOF (fn {context=ctxt', prems, ...} =>
  12.427 +local
  12.428 +  fun trace_assumptions ctxt iwthms idxs =
  12.429      let
  12.430 -      val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort
  12.431 -      val tag = "Solver " ^ SMT_Config.solver_of ctxt' ^ ": "
  12.432 -      val str_of = prefix tag o SMT_Failure.string_of_failure ctxt'
  12.433 -      fun safe_solve iwthms =
  12.434 -        if pass_exns then SOME (solve iwthms)
  12.435 -        else (SOME (solve iwthms)
  12.436 -          handle
  12.437 -            SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
  12.438 -              (SMT_Config.verbose_msg ctxt' str_of fail; NONE)
  12.439 -          | SMT_Failure.SMT fail =>
  12.440 -              (SMT_Config.trace_msg ctxt' str_of fail; NONE))
  12.441 +      val wthms =
  12.442 +        idxs
  12.443 +        |> filter (fn i => i >= 0)
  12.444 +        |> map_filter (AList.lookup (op =) iwthms)
  12.445      in
  12.446 -      safe_solve (map (pair ~1 o pair NONE) (rules @ prems))
  12.447 -      |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac)
  12.448 -    end) ctxt
  12.449 +      if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0
  12.450 +      then
  12.451 +        tracing (Pretty.string_of (Pretty.big_list "SMT used facts:"
  12.452 +          (map (Display.pretty_thm ctxt o snd) wthms)))
  12.453 +      else ()
  12.454 +    end
  12.455 +
  12.456 +  fun solve ctxt iwthms =
  12.457 +    iwthms
  12.458 +    |> tap check_topsort
  12.459 +    |> apply_solver ctxt
  12.460 +    |>> trace_assumptions ctxt iwthms
  12.461 +    |> snd
  12.462 +
  12.463 +  fun str_of ctxt fail =
  12.464 +    SMT_Failure.string_of_failure ctxt fail
  12.465 +    |> prefix ("Solver " ^ SMT_Config.solver_of ctxt ^ ": ")
  12.466  
  12.467 -val smt_tac = smt_tac' false
  12.468 +  fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms)
  12.469 +    handle
  12.470 +      SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) =>
  12.471 +        (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE)
  12.472 +    | SMT_Failure.SMT fail =>
  12.473 +        (SMT_Config.trace_msg ctxt (str_of ctxt) fail; NONE)
  12.474 +
  12.475 +  fun tag_rules thms = map_index (apsnd (pair NONE)) thms
  12.476 +  fun tag_prems thms = map (pair ~1 o pair NONE) thms
  12.477 +
  12.478 +  fun resolve (SOME thm) = Tactic.rtac thm 1
  12.479 +    | resolve NONE = Tactical.no_tac
  12.480 +
  12.481 +  fun tac prove ctxt rules =
  12.482 +    CONVERSION (SMT_Normalize.atomize_conv ctxt)
  12.483 +    THEN' Tactic.rtac @{thm ccontr}
  12.484 +    THEN' SUBPROOF (fn {context, prems, ...} =>
  12.485 +      resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt
  12.486 +in
  12.487 +
  12.488 +val smt_tac = tac safe_solve
  12.489 +val smt_tac' = tac (SOME oo solve)
  12.490 +
  12.491 +end
  12.492 +
  12.493  
  12.494  val smt_method =
  12.495    Scan.optional Attrib.thms [] >>
  12.496 @@ -392,7 +372,6 @@
  12.497      HEADGOAL (smt_tac ctxt (thms @ facts))))
  12.498  
  12.499  
  12.500 -
  12.501  (* setup *)
  12.502  
  12.503  val setup =
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jan 04 15:46:38 2011 -0800
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 06 17:51:56 2011 +0100
    13.3 @@ -42,7 +42,7 @@
    13.4       subgoal: int,
    13.5       subgoal_count: int,
    13.6       facts: prover_fact list,
    13.7 -     smt_head: (string * locality) SMT_Solver.smt_filter_head_result option}
    13.8 +     smt_head: (string * locality) SMT_Solver.smt_filter_data option}
    13.9  
   13.10    type prover_result =
   13.11      {outcome: failure option,
   13.12 @@ -115,43 +115,26 @@
   13.13     "Async_Manager". *)
   13.14  val das_Tool = "Sledgehammer"
   13.15  
   13.16 -val unremotify = perhaps (try (unprefix remote_prefix))
   13.17 -
   13.18  val select_smt_solver =
   13.19 -  Context.proof_map o SMT_Config.select_solver o unremotify
   13.20 +  Context.proof_map o SMT_Config.select_solver
   13.21  
   13.22  fun is_smt_prover ctxt name =
   13.23 -  let val smts = SMT_Solver.available_solvers_of ctxt in
   13.24 -    case try (unprefix remote_prefix) name of
   13.25 -      SOME base => member (op =) smts base andalso
   13.26 -                   SMT_Solver.is_remotely_available ctxt base
   13.27 -    | NONE => member (op =) smts name
   13.28 -  end
   13.29 +  member (op =) (SMT_Solver.available_solvers_of ctxt) name
   13.30  
   13.31  fun is_prover_available ctxt name =
   13.32    let val thy = ProofContext.theory_of ctxt in
   13.33      is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
   13.34    end
   13.35  
   13.36 -fun is_prover_installed ctxt name =
   13.37 -  let val thy = ProofContext.theory_of ctxt in
   13.38 -    if is_smt_prover ctxt name then
   13.39 -      String.isPrefix remote_prefix name orelse
   13.40 -      SMT_Solver.is_locally_installed ctxt name
   13.41 -    else
   13.42 -      is_atp_installed thy name
   13.43 -  end
   13.44 +fun is_prover_installed ctxt =
   13.45 +  is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt)
   13.46  
   13.47 -fun available_smt_solvers ctxt =
   13.48 -  let val smts = SMT_Solver.available_solvers_of ctxt in
   13.49 -    smts @ map (prefix remote_prefix)
   13.50 -               (filter (SMT_Solver.is_remotely_available ctxt) smts)
   13.51 -  end
   13.52 +fun available_smt_solvers ctxt = SMT_Solver.available_solvers_of ctxt
   13.53  
   13.54  fun default_max_relevant_for_prover ctxt name =
   13.55    let val thy = ProofContext.theory_of ctxt in
   13.56      if is_smt_prover ctxt name then
   13.57 -      SMT_Solver.default_max_relevant ctxt (unremotify name)
   13.58 +      SMT_Solver.default_max_relevant ctxt name
   13.59      else
   13.60        #default_max_relevant (get_atp thy name)
   13.61    end
   13.62 @@ -267,7 +250,7 @@
   13.63     subgoal: int,
   13.64     subgoal_count: int,
   13.65     facts: prover_fact list,
   13.66 -   smt_head: (string * locality) SMT_Solver.smt_filter_head_result option}
   13.67 +   smt_head: (string * locality) SMT_Solver.smt_filter_data option}
   13.68  
   13.69  type prover_result =
   13.70    {outcome: failure option,
   13.71 @@ -537,17 +520,13 @@
   13.72                      state i smt_head =
   13.73    let
   13.74      val ctxt = Proof.context_of state
   13.75 -    val (remote, base) =
   13.76 -      case try (unprefix remote_prefix) name of
   13.77 -        SOME base => (true, base)
   13.78 -      | NONE => (false, name)
   13.79      val repair_context =
   13.80 -      select_smt_solver base
   13.81 +      select_smt_solver name
   13.82        #> Config.put SMT_Config.verbose debug
   13.83        #> (if overlord then
   13.84              Config.put SMT_Config.debug_files
   13.85                         (overlord_file_location_for_prover name
   13.86 -                        |> (fn (path, base) => path ^ "/" ^ base))
   13.87 +                        |> (fn (path, name) => path ^ "/" ^ name))
   13.88            else
   13.89              I)
   13.90        #> Config.put SMT_Config.infer_triggers (!smt_triggers)
   13.91 @@ -579,9 +558,9 @@
   13.92            if debug then Output.urgent_message "Invoking SMT solver..." else ()
   13.93          val (outcome, used_facts) =
   13.94            (case (iter_num, smt_head) of
   13.95 -             (1, SOME head) => head |> apsnd (apfst (apsnd repair_context))
   13.96 -           | _ => SMT_Solver.smt_filter_head state facts i)
   13.97 -          |> SMT_Solver.smt_filter_tail iter_timeout remote
   13.98 +             (1, SOME head) => head |> apsnd (apsnd repair_context)
   13.99 +           | _ => SMT_Solver.smt_filter_preprocess state facts i)
  13.100 +          |> SMT_Solver.smt_filter_apply iter_timeout
  13.101            |> (fn {outcome, used_facts} => (outcome, used_facts))
  13.102            handle exn => if Exn.is_interrupt exn then
  13.103                            reraise exn
  13.104 @@ -668,10 +647,8 @@
  13.105              if can_apply_metis debug state subgoal (map snd used_facts) then
  13.106                ("metis", "")
  13.107              else
  13.108 -              let val base = unremotify name in
  13.109 -                ("smt", if base = SMT_Config.solver_of ctxt then ""
  13.110 -                        else "smt_solver = " ^ maybe_quote base)
  13.111 -              end
  13.112 +              ("smt", if name = SMT_Solver.solver_name_of ctxt then ""
  13.113 +                      else "smt_solver = " ^ maybe_quote name)
  13.114          in
  13.115            try_command_line (proof_banner auto)
  13.116                (apply_on_subgoal settings subgoal subgoal_count ^
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Jan 04 15:46:38 2011 -0800
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 06 17:51:56 2011 +0100
    14.3 @@ -255,7 +255,7 @@
    14.4              val weight = SMT_Weighted_Fact oo weight_smt_fact thy
    14.5              fun smt_head facts =
    14.6                (if debug then curry (op o) SOME else try)
    14.7 -                  (SMT_Solver.smt_filter_head state (facts ()))
    14.8 +                  (SMT_Solver.smt_filter_preprocess state (facts ()))
    14.9            in
   14.10              smts |> map (`(class_of_smt_solver ctxt))
   14.11                   |> AList.group (op =)