joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
authorboehmes
Tue Oct 26 11:45:12 2010 +0200 (2010-10-26)
changeset 401627f58a9a843c2
parent 40161 539d07b00e5f
child 40163 a462d5207aa6
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
NEWS
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/Tools/SMT/cvc3_solver.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/yices_solver.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_solver.ML
     1.1 --- a/NEWS	Tue Oct 26 11:39:26 2010 +0200
     1.2 +++ b/NEWS	Tue Oct 26 11:45:12 2010 +0200
     1.3 @@ -306,6 +306,15 @@
     1.4      sledgehammer [atp = ...] ~> sledgehammer [prover = ...]
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 +* Changed SMT configuration options:
     1.8 +  - Renamed:
     1.9 +    z3_proofs ~> smt_oracle (with swapped semantics)
    1.10 +    z3_trace_assms ~> smt_trace_used_facts
    1.11 +    INCOMPATIBILITY.
    1.12 +  - Added:
    1.13 +    cvc3_options
    1.14 +    yices_options
    1.15 +    smt_datatypes
    1.16  
    1.17  *** FOL ***
    1.18  
     2.1 --- a/src/HOL/IsaMakefile	Tue Oct 26 11:39:26 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Oct 26 11:45:12 2010 +0200
     2.3 @@ -336,20 +336,18 @@
     2.4    Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
     2.5    Tools/Sledgehammer/sledgehammer_atp_translate.ML \
     2.6    Tools/Sledgehammer/sledgehammer_util.ML \
     2.7 -  Tools/SMT/cvc3_solver.ML \
     2.8    Tools/SMT/smtlib_interface.ML \
     2.9    Tools/SMT/smt_monomorph.ML \
    2.10    Tools/SMT/smt_normalize.ML \
    2.11 +  Tools/SMT/smt_setup_solvers.ML \
    2.12    Tools/SMT/smt_solver.ML \
    2.13    Tools/SMT/smt_translate.ML \
    2.14 -  Tools/SMT/yices_solver.ML \
    2.15    Tools/SMT/z3_interface.ML \
    2.16    Tools/SMT/z3_model.ML \
    2.17    Tools/SMT/z3_proof_literals.ML \
    2.18    Tools/SMT/z3_proof_parser.ML \
    2.19    Tools/SMT/z3_proof_reconstruction.ML \
    2.20    Tools/SMT/z3_proof_tools.ML \
    2.21 -  Tools/SMT/z3_solver.ML \
    2.22    Tools/string_code.ML \
    2.23    Tools/string_syntax.ML \
    2.24    Tools/transfer.ML \
     3.1 --- a/src/HOL/SMT.thy	Tue Oct 26 11:39:26 2010 +0200
     3.2 +++ b/src/HOL/SMT.thy	Tue Oct 26 11:45:12 2010 +0200
     3.3 @@ -19,9 +19,7 @@
     3.4    ("Tools/SMT/z3_proof_reconstruction.ML")
     3.5    ("Tools/SMT/z3_model.ML")
     3.6    ("Tools/SMT/z3_interface.ML")
     3.7 -  ("Tools/SMT/z3_solver.ML")
     3.8 -  ("Tools/SMT/cvc3_solver.ML")
     3.9 -  ("Tools/SMT/yices_solver.ML")
    3.10 +  ("Tools/SMT/smt_setup_solvers.ML")
    3.11  begin
    3.12  
    3.13  
    3.14 @@ -124,16 +122,12 @@
    3.15  use "Tools/SMT/z3_proof_literals.ML"
    3.16  use "Tools/SMT/z3_proof_reconstruction.ML"
    3.17  use "Tools/SMT/z3_model.ML"
    3.18 -use "Tools/SMT/z3_solver.ML"
    3.19 -use "Tools/SMT/cvc3_solver.ML"
    3.20 -use "Tools/SMT/yices_solver.ML"
    3.21 +use "Tools/SMT/smt_setup_solvers.ML"
    3.22  
    3.23  setup {*
    3.24    SMT_Solver.setup #>
    3.25    Z3_Proof_Reconstruction.setup #>
    3.26 -  Z3_Solver.setup #>
    3.27 -  CVC3_Solver.setup #>
    3.28 -  Yices_Solver.setup
    3.29 +  SMT_Setup_Solvers.setup
    3.30  *}
    3.31  
    3.32  
    3.33 @@ -171,6 +165,31 @@
    3.34  
    3.35  declare [[ smt_timeout = 20 ]]
    3.36  
    3.37 +text {*
    3.38 +In general, the binding to SMT solvers runs as an oracle, i.e, the SMT
    3.39 +solvers are fully trusted without additional checks.  The following
    3.40 +option can cause the SMT solver to run in proof-producing mode, giving
    3.41 +a checkable certificate.  This is currently only implemented for Z3.
    3.42 +*}
    3.43 +
    3.44 +declare [[ smt_oracle = false ]]
    3.45 +
    3.46 +text {*
    3.47 +Each SMT solver provides several commandline options to tweak its
    3.48 +behaviour.  They can be passed to the solver by setting the following
    3.49 +options.
    3.50 +*}
    3.51 +
    3.52 +declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]]
    3.53 +
    3.54 +text {*
    3.55 +Enable the following option to use built-in support for datatypes and
    3.56 +records.  Currently, this is only implemented for Z3 running in oracle
    3.57 +mode.
    3.58 +*}
    3.59 +
    3.60 +declare [[ smt_datatypes = false ]]
    3.61 +
    3.62  
    3.63  
    3.64  subsection {* Certificates *}
    3.65 @@ -213,41 +232,14 @@
    3.66  
    3.67  declare [[ smt_trace = false ]]
    3.68  
    3.69 -
    3.70 -
    3.71 -subsection {* Z3-specific options *}
    3.72 -
    3.73  text {*
    3.74 -Z3 is the only SMT solver whose proofs are checked (or reconstructed)
    3.75 -in Isabelle (all other solvers are implemented as oracles).  Enabling
    3.76 -or disabling proof reconstruction for Z3 is controlled by the option
    3.77 -@{text z3_proofs}. 
    3.78 +From the set of assumptions given to the SMT solver, those assumptions
    3.79 +used in the proof are traced when the following option is set to
    3.80 +@{term true}.  This only works for Z3 when it runs in non-oracle mode
    3.81 +(see options @{text smt_solver} and @{text smt_oracle} above).
    3.82  *}
    3.83  
    3.84 -declare [[ z3_proofs = true ]]
    3.85 -
    3.86 -text {*
    3.87 -From the set of assumptions given to Z3, those assumptions used in
    3.88 -the proof are traced when the option @{text z3_trace_assms} is set to
    3.89 -@{term true}.
    3.90 -*}
    3.91 -
    3.92 -declare [[ z3_trace_assms = false ]]
    3.93 -
    3.94 -text {*
    3.95 -Z3 provides several commandline options to tweak its behaviour.  They
    3.96 -can be configured by writing them literally as value for the option
    3.97 -@{text z3_options}.
    3.98 -*}
    3.99 -
   3.100 -declare [[ z3_options = "" ]]
   3.101 -
   3.102 -text {*
   3.103 -The following configuration option may be used to enable mapping of
   3.104 -HOL datatypes and records to native datatypes provided by Z3.
   3.105 -*}
   3.106 -
   3.107 -declare [[ z3_datatypes = false ]]
   3.108 +declare [[ smt_trace_used_facts = false ]]
   3.109  
   3.110  
   3.111  
     4.1 --- a/src/HOL/Tools/SMT/cvc3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,48 +0,0 @@
     4.4 -(*  Title:      HOL/Tools/SMT/cvc3_solver.ML
     4.5 -    Author:     Sascha Boehme, TU Muenchen
     4.6 -
     4.7 -Interface of the SMT solver CVC3.
     4.8 -*)
     4.9 -
    4.10 -signature CVC3_SOLVER =
    4.11 -sig
    4.12 -  val setup: theory -> theory
    4.13 -end
    4.14 -
    4.15 -structure CVC3_Solver: CVC3_SOLVER =
    4.16 -struct
    4.17 -
    4.18 -val solver_name = "cvc3"
    4.19 -val env_var = "CVC3_SOLVER"
    4.20 -
    4.21 -val options = ["-lang", "smtlib", "-output-lang", "presentation"]
    4.22 -
    4.23 -val is_sat = String.isPrefix "Satisfiable."
    4.24 -val is_unsat = String.isPrefix "Unsatisfiable."
    4.25 -val is_unknown = String.isPrefix "Unknown."
    4.26 -
    4.27 -fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
    4.28 -
    4.29 -fun core_oracle (output, _) =
    4.30 -  let
    4.31 -    val empty_line = (fn "" => true | _ => false)
    4.32 -    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    4.33 -    val (l, _) = split_first (snd (chop_while empty_line output))
    4.34 -  in
    4.35 -    if is_unsat l then @{cprop False}
    4.36 -    else if is_sat l then raise_cex true
    4.37 -    else if is_unknown l then raise_cex false
    4.38 -    else raise SMT_Solver.SMT (solver_name ^ " failed")
    4.39 -  end
    4.40 -
    4.41 -fun solver oracle _ = {
    4.42 -  command = {env_var=env_var, remote_name=SOME solver_name},
    4.43 -  arguments = options,
    4.44 -  interface = SMTLIB_Interface.interface,
    4.45 -  reconstruct = pair o pair [] o oracle }
    4.46 -
    4.47 -val setup =
    4.48 -  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
    4.49 -  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
    4.50 -
    4.51 -end
     5.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:39:26 2010 +0200
     5.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:45:12 2010 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  
     5.5  signature SMT_NORMALIZE =
     5.6  sig
     5.7 -  type extra_norm = (int * thm) list -> Proof.context ->
     5.8 +  type extra_norm = bool -> (int * thm) list -> Proof.context ->
     5.9      (int * thm) list * Proof.context
    5.10    val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
    5.11      (int * thm) list * Proof.context
    5.12 @@ -480,7 +480,7 @@
    5.13  
    5.14  (* combined normalization *)
    5.15  
    5.16 -type extra_norm = (int * thm) list -> Proof.context ->
    5.17 +type extra_norm = bool -> (int * thm) list -> Proof.context ->
    5.18    (int * thm) list * Proof.context
    5.19  
    5.20  fun with_context f irules ctxt = (f ctxt irules, ctxt)
    5.21 @@ -492,7 +492,7 @@
    5.22    |> normalize_numerals ctxt
    5.23    |> nat_as_int ctxt
    5.24    |> rpair ctxt
    5.25 -  |-> extra_norm
    5.26 +  |-> extra_norm with_datatypes
    5.27    |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
    5.28    |-> SMT_Monomorph.monomorph
    5.29    |-> lift_lambdas
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 11:45:12 2010 +0200
     6.3 @@ -0,0 +1,93 @@
     6.4 +(*  Title:      HOL/Tools/SMT/smt_setup_solvers.ML
     6.5 +    Author:     Sascha Boehme, TU Muenchen
     6.6 +
     6.7 +Setup SMT solvers.
     6.8 +*)
     6.9 +
    6.10 +signature SMT_SETUP_SOLVERS =
    6.11 +sig
    6.12 +  val setup: theory -> theory
    6.13 +end
    6.14 +
    6.15 +structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
    6.16 +struct
    6.17 +
    6.18 +fun outcome_of unsat sat unknown solver_name line =
    6.19 +  if String.isPrefix unsat line then SMT_Solver.Unsat
    6.20 +  else if String.isPrefix sat line then SMT_Solver.Sat
    6.21 +  else if String.isPrefix unknown line then SMT_Solver.Unknown
    6.22 +  else raise SMT_Solver.SMT (SMT_Solver.Other_Failure ("Solver " ^
    6.23 +    quote solver_name ^ " failed, " ^ "see trace for details."))
    6.24 +
    6.25 +fun on_first_line test_outcome solver_name lines =
    6.26 +  let
    6.27 +    val empty_line = (fn "" => true | _ => false)
    6.28 +    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    6.29 +    val (l, ls) = split_first (snd (chop_while empty_line lines))
    6.30 +  in (test_outcome solver_name l, ls) end
    6.31 +
    6.32 +
    6.33 +(* CVC3 *)
    6.34 +
    6.35 +val cvc3 = {
    6.36 +  name = "cvc3",
    6.37 +  env_var = "CVC3_SOLVER",
    6.38 +  is_remote = true,
    6.39 +  options = K ["-lang", "smtlib", "-output-lang", "presentation"],
    6.40 +  interface = SMTLIB_Interface.interface,
    6.41 +  outcome =
    6.42 +    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    6.43 +  cex_parser = NONE,
    6.44 +  reconstruct = NONE }
    6.45 +
    6.46 +
    6.47 +(* Yices *)
    6.48 +
    6.49 +val yices = {
    6.50 +  name = "yices",
    6.51 +  env_var = "YICES_SOLVER",
    6.52 +  is_remote = false,
    6.53 +  options = K ["--smtlib"],
    6.54 +  interface = SMTLIB_Interface.interface,
    6.55 +  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    6.56 +  cex_parser = NONE,
    6.57 +  reconstruct = NONE }
    6.58 +
    6.59 +
    6.60 +(* Z3 *)
    6.61 +
    6.62 +fun z3_options ctxt =
    6.63 +  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
    6.64 +  |> not (Config.get ctxt SMT_Solver.oracle) ?
    6.65 +       append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
    6.66 +
    6.67 +fun z3_on_last_line solver_name lines =
    6.68 +  let
    6.69 +    fun junk l =
    6.70 +      String.isPrefix "WARNING" l orelse
    6.71 +      String.isPrefix "ERROR" l orelse
    6.72 +      forall Symbol.is_ascii_blank (Symbol.explode l)
    6.73 +  in
    6.74 +    the_default ("", []) (try (swap o split_last) (filter_out junk lines))
    6.75 +    |>> outcome_of "unsat" "sat" "unknown" solver_name
    6.76 +  end
    6.77 +
    6.78 +val z3 = {
    6.79 +  name = "z3",
    6.80 +  env_var = "Z3_SOLVER",
    6.81 +  is_remote = true,
    6.82 +  options = z3_options,
    6.83 +  interface = Z3_Interface.interface,
    6.84 +  outcome = z3_on_last_line,
    6.85 +  cex_parser = SOME Z3_Model.parse_counterex,
    6.86 +  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
    6.87 +
    6.88 +
    6.89 +(* overall setup *)
    6.90 +
    6.91 +val setup =
    6.92 +  SMT_Solver.add_solver cvc3 #>
    6.93 +  SMT_Solver.add_solver yices #>
    6.94 +  SMT_Solver.add_solver z3
    6.95 +
    6.96 +end
     7.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 26 11:45:12 2010 +0200
     7.3 @@ -6,24 +6,37 @@
     7.4  
     7.5  signature SMT_SOLVER =
     7.6  sig
     7.7 -  exception SMT of string
     7.8 -  exception SMT_COUNTEREXAMPLE of bool * term list
     7.9 +  datatype failure =
    7.10 +    Counterexample of bool * term list |
    7.11 +    Time_Out |
    7.12 +    Other_Failure of string
    7.13 +  val string_of_failure: Proof.context -> failure -> string
    7.14 +  exception SMT of failure
    7.15  
    7.16    type interface = {
    7.17      extra_norm: SMT_Normalize.extra_norm,
    7.18      translate: SMT_Translate.config }
    7.19 +  datatype outcome = Unsat | Sat | Unknown
    7.20    type solver_config = {
    7.21 -    command: {env_var: string, remote_name: string option},
    7.22 -    arguments: string list,
    7.23 +    name: string,
    7.24 +    env_var: string,
    7.25 +    is_remote: bool,
    7.26 +    options: Proof.context -> string list,
    7.27      interface: interface,
    7.28 -    reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
    7.29 -      (int list * thm) * Proof.context }
    7.30 +    outcome: string -> string list -> outcome * string list,
    7.31 +    cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
    7.32 +      term list) option,
    7.33 +    reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
    7.34 +      (int list * thm) * Proof.context) option }
    7.35  
    7.36    (*options*)
    7.37 +  val oracle: bool Config.T
    7.38 +  val datatypes: bool Config.T
    7.39    val timeout: int Config.T
    7.40    val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
    7.41    val trace: bool Config.T
    7.42    val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
    7.43 +  val trace_used_facts: bool Config.T
    7.44  
    7.45    (*certificates*)
    7.46    val fixed_certificates: bool Config.T
    7.47 @@ -31,19 +44,17 @@
    7.48  
    7.49    (*solvers*)
    7.50    type solver = Proof.context -> (int * thm) list -> int list * thm
    7.51 -  type solver_info = Context.generic -> Pretty.T list
    7.52 -  val add_solver: string * (Proof.context -> solver_config) ->
    7.53 -    Context.generic -> Context.generic
    7.54 +  val add_solver: solver_config -> theory -> theory
    7.55 +  val set_solver_options: string -> string -> Context.generic ->
    7.56 +    Context.generic
    7.57    val all_solver_names_of: Context.generic -> string list
    7.58 -  val add_solver_info: string * solver_info -> Context.generic ->
    7.59 -    Context.generic
    7.60    val solver_name_of: Context.generic -> string
    7.61    val select_solver: string -> Context.generic -> Context.generic
    7.62    val solver_of: Context.generic -> solver
    7.63  
    7.64 -  (*solver*)
    7.65 -  val smt_solver: Proof.context -> ('a * thm) list -> 'a list * thm
    7.66 -  val smt_filter: Proof.context -> ('a * thm) list -> 'a list * string
    7.67 +  (*filter*)
    7.68 +  val smt_filter: Proof.state -> int -> ('a * thm) list ->
    7.69 +    'a list * failure option
    7.70  
    7.71    (*tactic*)
    7.72    val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic
    7.73 @@ -57,36 +68,64 @@
    7.74  structure SMT_Solver: SMT_SOLVER =
    7.75  struct
    7.76  
    7.77 -exception SMT of string
    7.78 -exception SMT_COUNTEREXAMPLE of bool * term list
    7.79 +datatype failure =
    7.80 +  Counterexample of bool * term list |
    7.81 +  Time_Out |
    7.82 +  Other_Failure of string
    7.83  
    7.84 +fun string_of_failure ctxt (Counterexample (real, ex)) =
    7.85 +      let
    7.86 +        val msg = if real then "Counterexample found"
    7.87 +          else "Potential counterexample found"
    7.88 +      in
    7.89 +        if null ex then msg ^ "."
    7.90 +        else Pretty.string_of (Pretty.big_list (msg ^ ":")
    7.91 +          (map (Syntax.pretty_term ctxt) ex))
    7.92 +      end
    7.93 +  | string_of_failure _ Time_Out = "Time out."
    7.94 +  | string_of_failure _ (Other_Failure msg) = msg
    7.95 +
    7.96 +exception SMT of failure
    7.97  
    7.98  type interface = {
    7.99    extra_norm: SMT_Normalize.extra_norm,
   7.100    translate: SMT_Translate.config }
   7.101  
   7.102 +datatype outcome = Unsat | Sat | Unknown
   7.103 +
   7.104  type solver_config = {
   7.105 -  command: {env_var: string, remote_name: string option},
   7.106 -  arguments: string list,
   7.107 +  name: string,
   7.108 +  env_var: string,
   7.109 +  is_remote: bool,
   7.110 +  options: Proof.context -> string list,
   7.111    interface: interface,
   7.112 -  reconstruct: (string list * SMT_Translate.recon) -> Proof.context ->
   7.113 -    (int list * thm) * Proof.context }
   7.114 +  outcome: string -> string list -> outcome * string list,
   7.115 +  cex_parser: (Proof.context -> SMT_Translate.recon -> string list ->
   7.116 +    term list) option,
   7.117 +  reconstruct: (Proof.context -> SMT_Translate.recon -> string list ->
   7.118 +    (int list * thm) * Proof.context) option }
   7.119  
   7.120  
   7.121  
   7.122  (* SMT options *)
   7.123  
   7.124 +val (oracle, setup_oracle) = Attrib.config_bool "smt_oracle" (K true)
   7.125 +
   7.126 +val (datatypes, setup_datatypes) = Attrib.config_bool "smt_datatypes" (K false)
   7.127 +
   7.128  val (timeout, setup_timeout) = Attrib.config_int "smt_timeout" (K 30)
   7.129  
   7.130  fun with_timeout ctxt f x =
   7.131    TimeLimit.timeLimit (Time.fromSeconds (Config.get ctxt timeout)) f x
   7.132 -  handle TimeLimit.TimeOut => raise SMT "timeout"
   7.133 +  handle TimeLimit.TimeOut => raise SMT Time_Out
   7.134  
   7.135  val (trace, setup_trace) = Attrib.config_bool "smt_trace" (K false)
   7.136  
   7.137  fun trace_msg ctxt f x =
   7.138    if Config.get ctxt trace then tracing (f x) else ()
   7.139  
   7.140 +val (trace_used_facts, setup_trace_used_facts) =
   7.141 +  Attrib.config_bool "smt_trace_used_facts" (K false)
   7.142  
   7.143  
   7.144  (* SMT certificates *)
   7.145 @@ -115,21 +154,20 @@
   7.146  
   7.147  local
   7.148  
   7.149 -fun choose {env_var, remote_name} =
   7.150 +fun choose (env_var, is_remote, remote_name) =
   7.151    let
   7.152      val local_solver = getenv env_var
   7.153 -    val remote_solver = the_default "" remote_name
   7.154      val remote_url = getenv "REMOTE_SMT_URL"
   7.155    in
   7.156      if local_solver <> ""
   7.157      then 
   7.158       (tracing ("Invoking local SMT solver " ^ quote local_solver ^ " ...");
   7.159        [local_solver])
   7.160 -    else if remote_solver <> ""
   7.161 +    else if is_remote
   7.162      then
   7.163 -     (tracing ("Invoking remote SMT solver " ^ quote remote_solver ^ " at " ^
   7.164 +     (tracing ("Invoking remote SMT solver " ^ quote remote_name ^ " at " ^
   7.165          quote remote_url ^ " ...");
   7.166 -      [getenv "REMOTE_SMT", remote_solver])
   7.167 +      [getenv "REMOTE_SMT", remote_name])
   7.168      else error ("Undefined Isabelle environment variable: " ^ quote env_var)
   7.169    end
   7.170  
   7.171 @@ -181,30 +219,46 @@
   7.172        Pretty.big_list "functions:" (map pretty_term (Symtab.dest terms))])) ()
   7.173    end
   7.174  
   7.175 -fun invoke translate_config comments command arguments irules ctxt =
   7.176 -  irules
   7.177 -  |> SMT_Translate.translate translate_config ctxt comments
   7.178 -  ||> tap (trace_recon_data ctxt)
   7.179 -  |>> run_solver ctxt command arguments
   7.180 -  |> rpair ctxt
   7.181 +fun invoke translate_config name cmd more_opts options irules ctxt =
   7.182 +  let
   7.183 +    val args = more_opts @ options ctxt
   7.184 +    val comments = ("solver: " ^ name) ::
   7.185 +      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
   7.186 +      "arguments:" :: args
   7.187 +  in
   7.188 +    irules
   7.189 +    |> SMT_Translate.translate translate_config ctxt comments
   7.190 +    ||> tap (trace_recon_data ctxt)
   7.191 +    |>> run_solver ctxt cmd args
   7.192 +    |> rpair ctxt
   7.193 +  end
   7.194  
   7.195  fun discharge_definitions thm =
   7.196    if Thm.nprems_of thm = 0 then thm
   7.197    else discharge_definitions (@{thm reflexive} RS thm)
   7.198  
   7.199 -fun gen_solver name solver ctxt prems =
   7.200 +fun set_has_datatypes with_datatypes translate =
   7.201    let
   7.202 -    val {command, arguments, interface, reconstruct} = solver ctxt
   7.203 -    val comments = ("solver: " ^ name) ::
   7.204 -      ("timeout: " ^ string_of_int (Config.get ctxt timeout)) ::
   7.205 -      "arguments:" :: arguments
   7.206 +    val {prefixes, header, strict, builtins, serialize} = translate
   7.207 +    val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
   7.208 +    val with_datatypes' = has_datatypes andalso with_datatypes
   7.209 +    val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
   7.210 +      builtin_fun=builtin_fun, has_datatypes=with_datatypes}
   7.211 +    val translate' = {prefixes=prefixes, header=header, strict=strict,
   7.212 +      builtins=builtins', serialize=serialize}
   7.213 +  in (with_datatypes', translate') end
   7.214 +
   7.215 +fun gen_solver name info ctxt irules =
   7.216 +  let
   7.217 +    val {env_var, is_remote, options, more_options, interface, reconstruct} =
   7.218 +      info
   7.219      val {extra_norm, translate} = interface
   7.220 -    val {builtins, ...} = translate
   7.221 -    val {has_datatypes, ...} = builtins
   7.222 +    val (with_datatypes, translate') =
   7.223 +      set_has_datatypes (Config.get ctxt datatypes) translate
   7.224    in
   7.225 -    (prems, ctxt)
   7.226 -    |-> SMT_Normalize.normalize extra_norm has_datatypes
   7.227 -    |-> invoke translate comments command arguments
   7.228 +    (irules, ctxt)
   7.229 +    |-> SMT_Normalize.normalize extra_norm with_datatypes
   7.230 +    |-> invoke translate' name (env_var, is_remote, name) more_options options
   7.231      |-> reconstruct
   7.232      |-> (fn (idxs, thm) => fn ctxt' => thm
   7.233      |> singleton (ProofContext.export ctxt' ctxt)
   7.234 @@ -217,11 +271,19 @@
   7.235  (* solver store *)
   7.236  
   7.237  type solver = Proof.context -> (int * thm) list -> int list * thm
   7.238 -type solver_info = Context.generic -> Pretty.T list
   7.239 +
   7.240 +type solver_info = {
   7.241 +  env_var: string,
   7.242 +  is_remote: bool,
   7.243 +  options: Proof.context -> string list,
   7.244 +  more_options: string list,
   7.245 +  interface: interface,
   7.246 +  reconstruct: string list * SMT_Translate.recon -> Proof.context ->
   7.247 +    (int list * thm) * Proof.context }
   7.248  
   7.249  structure Solvers = Generic_Data
   7.250  (
   7.251 -  type T = ((Proof.context -> solver_config) * solver_info) Symtab.table
   7.252 +  type T = solver_info Symtab.table
   7.253    val empty = Symtab.empty
   7.254    val extend = I
   7.255    fun merge data = Symtab.merge (K true) data
   7.256 @@ -229,10 +291,48 @@
   7.257  )
   7.258  
   7.259  val no_solver = "(none)"
   7.260 -val add_solver = Solvers.map o Symtab.update_new o apsnd (rpair (K []))
   7.261 +
   7.262 +fun set_solver_options name opts = Solvers.map (Symtab.map_entry name (fn
   7.263 +  {env_var, is_remote, options, interface, reconstruct, ...} =>
   7.264 +  {env_var=env_var, is_remote=is_remote, options=options,
   7.265 +   more_options=String.tokens (Symbol.is_ascii_blank o str) opts,
   7.266 +   interface=interface, reconstruct=reconstruct}))
   7.267 +
   7.268 +local
   7.269 +  fun finish outcome cex_parser reconstruct ocl (output, recon) ctxt =
   7.270 +    (case outcome output of
   7.271 +      (Unsat, ls) =>
   7.272 +        if not (Config.get ctxt oracle) andalso is_some reconstruct
   7.273 +        then the reconstruct ctxt recon ls
   7.274 +        else (([], ocl ()), ctxt)
   7.275 +    | (result, ls) =>
   7.276 +        let val ts = (case cex_parser of SOME f => f ctxt recon ls | _ => [])
   7.277 +        in raise SMT (Counterexample (result = Sat, ts)) end)
   7.278 +in
   7.279 +
   7.280 +fun add_solver cfg =
   7.281 +  let
   7.282 +    val {name, env_var, is_remote, options, interface, outcome, cex_parser,
   7.283 +      reconstruct} = cfg
   7.284 +
   7.285 +    fun core_oracle () = @{cprop False}
   7.286 +
   7.287 +    fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
   7.288 +      more_options=[], interface=interface,
   7.289 +      reconstruct=finish (outcome name) cex_parser reconstruct ocl }
   7.290 +  in
   7.291 +    Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
   7.292 +    Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
   7.293 +    Attrib.setup (Binding.name (name ^ "_options"))
   7.294 +      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   7.295 +        (Thm.declaration_attribute o K o set_solver_options name))
   7.296 +      ("Additional command line options for SMT solver " ^ quote name)
   7.297 +  end
   7.298 +
   7.299 +end
   7.300 +
   7.301  val all_solver_names_of = Symtab.keys o Solvers.get
   7.302  val lookup_solver = Symtab.lookup o Solvers.get
   7.303 -fun add_solver_info (n, i) = Solvers.map (Symtab.map_entry n (apsnd (K i)))
   7.304  
   7.305  
   7.306  
   7.307 @@ -256,7 +356,7 @@
   7.308  fun raw_solver_of context name =
   7.309    (case lookup_solver context name of
   7.310      NONE => error "No SMT solver selected"
   7.311 -  | SOME (s, _) => s)
   7.312 +  | SOME s => s)
   7.313  
   7.314  fun solver_of context =
   7.315    let val name = solver_name_of context
   7.316 @@ -264,58 +364,57 @@
   7.317  
   7.318  
   7.319  
   7.320 -(* SMT solver *)
   7.321 +(* SMT filter *)
   7.322  
   7.323  val has_topsort = Term.exists_type (Term.exists_subtype (fn
   7.324      TFree (_, []) => true
   7.325    | TVar (_, []) => true
   7.326    | _ => false))
   7.327  
   7.328 -fun smt_solver ctxt xrules =
   7.329 +fun smt_solver ctxt irules =
   7.330    (* without this test, we would run into problems when atomizing the rules: *)
   7.331 -  if exists (has_topsort o Thm.prop_of o snd) xrules
   7.332 -  then raise SMT "proof state contains the universal sort {}"
   7.333 -  else
   7.334 +  if exists (has_topsort o Thm.prop_of o snd) irules
   7.335 +  then raise SMT (Other_Failure "proof state contains the universal sort {}")
   7.336 +  else solver_of (Context.Proof ctxt) ctxt irules
   7.337 +
   7.338 +fun smt_filter st i xrules =
   7.339 +  let
   7.340 +    val {context, facts, goal} = Proof.goal st
   7.341 +    val cprop =
   7.342 +      Thm.cprem_of goal i
   7.343 +      |> Thm.rhs_of o SMT_Normalize.atomize_conv context
   7.344 +      |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
   7.345 +    val irs = map (pair ~1) (Thm.assume cprop :: facts)
   7.346 +  in
   7.347      split_list xrules
   7.348 -    ||>> solver_of (Context.Proof ctxt) ctxt o map_index I
   7.349 +    ||>> solver_of (Context.Proof context) context o append irs o map_index I
   7.350      |>> uncurry (map_filter o try o nth) o apsnd (distinct (op =))
   7.351 -
   7.352 -fun smt_filter ctxt xrules =
   7.353 -  (fst (smt_solver ctxt xrules), "")
   7.354 -  handle SMT msg => ([], "SMT: " ^ msg)
   7.355 -       | SMT_COUNTEREXAMPLE _ => ([], "SMT: potential counterexample")
   7.356 +    |> rpair NONE o fst
   7.357 +  end
   7.358 +  handle SMT fail => ([], SOME fail)
   7.359  
   7.360  
   7.361  
   7.362  (* SMT tactic *)
   7.363  
   7.364  local
   7.365 -  fun pretty_cex ctxt (real, ex) =
   7.366 -    let
   7.367 -      val msg = if real then "SMT: counterexample found"
   7.368 -        else "SMT: potential counterexample found"
   7.369 -    in
   7.370 -      if null ex then msg ^ "."
   7.371 -      else Pretty.string_of (Pretty.big_list (msg ^ ":")
   7.372 -        (map (Syntax.pretty_term ctxt) ex))
   7.373 -    end
   7.374 -
   7.375    fun fail_tac f msg st = (f msg; Tactical.no_tac st)
   7.376  
   7.377    fun SAFE pass_exns tac ctxt i st =
   7.378      if pass_exns then tac ctxt i st
   7.379 -    else (tac ctxt i st
   7.380 -      handle SMT msg => fail_tac (trace_msg ctxt (prefix "SMT: ")) msg st
   7.381 -           | SMT_COUNTEREXAMPLE ce => fail_tac tracing (pretty_cex ctxt ce) st)
   7.382 +    else (tac ctxt i st handle SMT fail => fail_tac
   7.383 +      (trace_msg ctxt (prefix "SMT: ") o string_of_failure ctxt) fail st)
   7.384  in
   7.385 +
   7.386  fun smt_tac' pass_exns ctxt rules =
   7.387    CONVERSION (SMT_Normalize.atomize_conv ctxt)
   7.388    THEN' Tactic.rtac @{thm ccontr}
   7.389    THEN' SUBPROOF (fn {context, prems, ...} =>
   7.390 -    let fun solve cx = snd (smt_solver cx (map (pair ()) (rules @ prems)))
   7.391 +    let fun solve cx = snd (smt_solver cx (map (pair ~1) (rules @ prems)))
   7.392      in SAFE pass_exns (Tactic.rtac o solve) context 1 end) ctxt
   7.393  
   7.394  val smt_tac = smt_tac' false
   7.395 +
   7.396  end
   7.397  
   7.398  val smt_method =
   7.399 @@ -332,8 +431,11 @@
   7.400      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   7.401        (Thm.declaration_attribute o K o select_solver))
   7.402      "SMT solver configuration" #>
   7.403 +  setup_oracle #>
   7.404 +  setup_datatypes #>
   7.405    setup_timeout #>
   7.406    setup_trace #>
   7.407 +  setup_trace_used_facts #>
   7.408    setup_fixed_certificates #>
   7.409    Attrib.setup @{binding smt_certificates}
   7.410      (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
   7.411 @@ -348,13 +450,12 @@
   7.412      val t = string_of_int (Config.get_generic context timeout)
   7.413      val names = sort_strings (all_solver_names_of context)
   7.414      val ns = if null names then [no_solver] else names
   7.415 -    val take_info = (fn (_, []) => NONE | info => SOME info)
   7.416 -    val infos =
   7.417 -      Solvers.get context
   7.418 -      |> Symtab.dest
   7.419 -      |> map_filter (fn (n, (_, info)) => take_info (n, info context))
   7.420 -      |> sort (prod_ord string_ord (K EQUAL))
   7.421 -      |> map (fn (n, ps) => Pretty.big_list (n ^ ":") ps)
   7.422 +    val n = solver_name_of context
   7.423 +    val opts =
   7.424 +      (case Symtab.lookup (Solvers.get context) n of
   7.425 +        NONE => []
   7.426 +      | SOME {more_options, options, ...} =>
   7.427 +          more_options @ options (Context.proof_of context))
   7.428      val certs_filename =
   7.429        (case get_certificates_path context of
   7.430          SOME path => Path.implode path
   7.431 @@ -363,12 +464,14 @@
   7.432        else "false"
   7.433    in
   7.434      Pretty.writeln (Pretty.big_list "SMT setup:" [
   7.435 -      Pretty.str ("Current SMT solver: " ^ solver_name_of context),
   7.436 +      Pretty.str ("Current SMT solver: " ^ n),
   7.437 +      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
   7.438        Pretty.str_list "Available SMT solvers: "  "" ns,
   7.439        Pretty.str ("Current timeout: " ^ t ^ " seconds"),
   7.440 +      Pretty.str ("With proofs: " ^
   7.441 +        (if Config.get_generic context oracle then "false" else "true")),
   7.442        Pretty.str ("Certificates cache: " ^ certs_filename),
   7.443 -      Pretty.str ("Fixed certificates: " ^ fixed),
   7.444 -      Pretty.big_list "Solver-specific settings:" infos])
   7.445 +      Pretty.str ("Fixed certificates: " ^ fixed)])
   7.446    end
   7.447  
   7.448  val _ =
     8.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:39:26 2010 +0200
     8.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:45:12 2010 +0200
     8.3 @@ -15,7 +15,7 @@
     8.4    val add_builtins: builtins -> Context.generic -> Context.generic
     8.5    val add_logic: (term list -> string option) -> Context.generic ->
     8.6      Context.generic
     8.7 -  val extra_norm: bool -> SMT_Normalize.extra_norm
     8.8 +  val extra_norm: SMT_Normalize.extra_norm
     8.9    val interface: SMT_Solver.interface
    8.10  end
    8.11  
    8.12 @@ -283,7 +283,7 @@
    8.13  (** interfaces **)
    8.14  
    8.15  val interface = {
    8.16 -  extra_norm = extra_norm false,
    8.17 +  extra_norm = extra_norm,
    8.18    translate = {
    8.19      prefixes = {
    8.20        sort_prefix = "S",
     9.1 --- a/src/HOL/Tools/SMT/yices_solver.ML	Tue Oct 26 11:39:26 2010 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,44 +0,0 @@
     9.4 -(*  Title:      HOL/Tools/SMT/yices_solver.ML
     9.5 -    Author:     Sascha Boehme, TU Muenchen
     9.6 -
     9.7 -Interface of the SMT solver Yices.
     9.8 -*)
     9.9 -
    9.10 -signature YICES_SOLVER =
    9.11 -sig
    9.12 -  val setup: theory -> theory
    9.13 -end
    9.14 -
    9.15 -structure Yices_Solver: YICES_SOLVER =
    9.16 -struct
    9.17 -
    9.18 -val solver_name = "yices"
    9.19 -val env_var = "YICES_SOLVER"
    9.20 -
    9.21 -val options = ["--smtlib"]
    9.22 -
    9.23 -fun raise_cex real = raise SMT_Solver.SMT_COUNTEREXAMPLE (real, [])
    9.24 -
    9.25 -fun core_oracle (output, _) =
    9.26 -  let
    9.27 -    val empty_line = (fn "" => true | _ => false)
    9.28 -    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    9.29 -    val (l, _) = split_first (snd (chop_while empty_line output))
    9.30 -  in
    9.31 -    if String.isPrefix "unsat" l then @{cprop False}
    9.32 -    else if String.isPrefix "sat" l then raise_cex true
    9.33 -    else if String.isPrefix "unknown" l then raise_cex false
    9.34 -    else raise SMT_Solver.SMT (solver_name ^ " failed")
    9.35 -  end
    9.36 -
    9.37 -fun solver oracle _ = {
    9.38 -  command = {env_var=env_var, remote_name=NONE},
    9.39 -  arguments = options,
    9.40 -  interface = SMTLIB_Interface.interface,
    9.41 -  reconstruct = pair o pair [] o oracle }
    9.42 -
    9.43 -val setup =
    9.44 -  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
    9.45 -  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle)))
    9.46 -
    9.47 -end
    10.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:39:26 2010 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Tue Oct 26 11:45:12 2010 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  sig
    10.5    type builtin_fun = string * typ -> term list -> (string * term list) option
    10.6    val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
    10.7 -  val interface: bool -> SMT_Solver.interface
    10.8 +  val interface: SMT_Solver.interface
    10.9  
   10.10    datatype sym = Sym of string * sym list
   10.11    type mk_builtins = {
   10.12 @@ -95,8 +95,8 @@
   10.13    is_some (z3_builtin_fun' ctxt c ts) orelse 
   10.14    is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
   10.15  
   10.16 -fun interface has_datatypes = {
   10.17 -  extra_norm = extra_norm' has_datatypes,
   10.18 +val interface = {
   10.19 +  extra_norm = extra_norm',
   10.20    translate = {
   10.21      prefixes = prefixes,
   10.22      strict = strict,
   10.23 @@ -105,7 +105,7 @@
   10.24        builtin_typ = builtin_typ,
   10.25        builtin_num = builtin_num,
   10.26        builtin_fun = z3_builtin_fun',
   10.27 -      has_datatypes = has_datatypes},
   10.28 +      has_datatypes = true},
   10.29      serialize = serialize}}
   10.30  
   10.31  end
    11.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Oct 26 11:39:26 2010 +0200
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Tue Oct 26 11:45:12 2010 +0200
    11.3 @@ -240,8 +240,8 @@
    11.4  
    11.5  (* core parser *)
    11.6  
    11.7 -fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^
    11.8 -  string_of_int line_no ^ "): " ^ msg)
    11.9 +fun parse_exn line_no msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
   11.10 +  ("Z3 proof parser (line " ^ string_of_int line_no ^ "): " ^ msg))
   11.11  
   11.12  fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
   11.13  
    12.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:39:26 2010 +0200
    12.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Oct 26 11:45:12 2010 +0200
    12.3 @@ -8,7 +8,7 @@
    12.4  sig
    12.5    val add_z3_rule: thm -> Context.generic -> Context.generic
    12.6    val trace_assms: bool Config.T
    12.7 -  val reconstruct: string list * SMT_Translate.recon -> Proof.context ->
    12.8 +  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
    12.9      (int list * thm) * Proof.context
   12.10    val setup: theory -> theory
   12.11  end
   12.12 @@ -20,7 +20,8 @@
   12.13  structure T = Z3_Proof_Tools
   12.14  structure L = Z3_Proof_Literals
   12.15  
   12.16 -fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
   12.17 +fun z3_exn msg = raise SMT_Solver.SMT (SMT_Solver.Other_Failure
   12.18 +  ("Z3 proof reconstruction: " ^ msg))
   12.19  
   12.20  
   12.21  
   12.22 @@ -826,7 +827,7 @@
   12.23      (fn (idx, ptab) => result (lookup idx (ctxt, Inttab.map (K Unproved) ptab)))
   12.24    end
   12.25  
   12.26 -fun reconstruct (output, {typs, terms, unfolds, assms}) ctxt =
   12.27 +fun reconstruct ctxt {typs, terms, unfolds, assms} output =
   12.28    P.parse ctxt typs terms output
   12.29    |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab))
   12.30  
    13.1 --- a/src/HOL/Tools/SMT/z3_solver.ML	Tue Oct 26 11:39:26 2010 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,87 +0,0 @@
    13.4 -(*  Title:      HOL/Tools/SMT/z3_solver.ML
    13.5 -    Author:     Sascha Boehme, TU Muenchen
    13.6 -
    13.7 -Interface of the SMT solver Z3.
    13.8 -*)
    13.9 -
   13.10 -signature Z3_SOLVER =
   13.11 -sig
   13.12 -  val proofs: bool Config.T
   13.13 -  val options: string Config.T
   13.14 -  val datatypes: bool Config.T
   13.15 -  val setup: theory -> theory
   13.16 -end
   13.17 -
   13.18 -structure Z3_Solver: Z3_SOLVER =
   13.19 -struct
   13.20 -
   13.21 -val solver_name = "z3"
   13.22 -val env_var = "Z3_SOLVER"
   13.23 -
   13.24 -val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
   13.25 -val (options, options_setup) = Attrib.config_string "z3_options" (K "")
   13.26 -val (datatypes, datatypes_setup) = Attrib.config_bool "z3_datatypes" (K false)
   13.27 -
   13.28 -fun add xs ys = ys @ xs
   13.29 -
   13.30 -fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
   13.31 -
   13.32 -fun get_options ctxt =
   13.33 -  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
   13.34 -  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
   13.35 -  |> add (explode_options (Config.get ctxt options))
   13.36 -
   13.37 -fun pretty_config context = [
   13.38 -  Pretty.str ("With proofs: " ^
   13.39 -    (if Config.get_generic context proofs then "true" else "false")),
   13.40 -  Pretty.str ("Options: " ^
   13.41 -    space_implode " " (get_options (Context.proof_of context))) ]
   13.42 -
   13.43 -fun cmdline_options ctxt =
   13.44 -  get_options ctxt
   13.45 -  |> add ["-smt"]
   13.46 -
   13.47 -fun raise_cex ctxt real recon ls =
   13.48 -  let val cex = Z3_Model.parse_counterex ctxt recon ls
   13.49 -  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
   13.50 -
   13.51 -fun if_unsat f (output, recon) ctxt =
   13.52 -  let
   13.53 -    fun jnk l =
   13.54 -      String.isPrefix "WARNING" l orelse
   13.55 -      String.isPrefix "ERROR" l orelse
   13.56 -      forall Symbol.is_ascii_blank (Symbol.explode l)
   13.57 -    val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
   13.58 -  in
   13.59 -    if String.isPrefix "unsat" l then f (ls, recon) ctxt
   13.60 -    else if String.isPrefix "sat" l then raise_cex ctxt true recon ls
   13.61 -    else if String.isPrefix "unknown" l then raise_cex ctxt false recon ls
   13.62 -    else raise SMT_Solver.SMT (solver_name ^ " failed")
   13.63 -  end
   13.64 -
   13.65 -val core_oracle = uncurry (if_unsat (K (K @{cprop False})))
   13.66 -
   13.67 -val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
   13.68 -
   13.69 -fun solver oracle ctxt =
   13.70 -  let
   13.71 -    val with_datatypes = Config.get ctxt datatypes
   13.72 -    val with_proof = not with_datatypes andalso Config.get ctxt proofs
   13.73 -                     (* FIXME: implement proof reconstruction for datatypes *)
   13.74 -  in
   13.75 -   {command = {env_var=env_var, remote_name=SOME solver_name},
   13.76 -    arguments = cmdline_options ctxt,
   13.77 -    interface = Z3_Interface.interface with_datatypes,
   13.78 -    reconstruct =
   13.79 -      if with_proof then prover else (fn r => `(pair [] o oracle o pair r))}
   13.80 -  end
   13.81 -
   13.82 -val setup =
   13.83 -  proofs_setup #>
   13.84 -  options_setup #>
   13.85 -  datatypes_setup #>
   13.86 -  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
   13.87 -  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #>
   13.88 -  Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config))
   13.89 -
   13.90 -end