1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SMT/Tools/z3_solver.ML	Fri Sep 18 18:13:19 2009 +0200
     1.3 @@ -0,0 +1,83 @@
     1.4 +(*  Title:      HOL/SMT/Tools/z3_solver.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Interface of the SMT solver Z3.
     1.8 +*)
     1.9 +
    1.10 +signature Z3_SOLVER =
    1.11 +sig
    1.12 +  val proofs: bool Config.T
    1.13 +  val options: string Config.T
    1.14 +
    1.15 +  val setup: theory -> theory
    1.16 +end
    1.17 +
    1.18 +structure Z3_Solver: Z3_SOLVER =
    1.19 +struct
    1.20 +
    1.21 +val solver_name = "z3"
    1.22 +val env_var = "Z3_SOLVER"
    1.23 +
    1.24 +val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" false
    1.25 +val (options, options_setup) = Attrib.config_string "z3_options" ""
    1.26 +
    1.27 +fun add xs ys = ys @ xs
    1.28 +
    1.29 +fun get_options ctxt =
    1.30 +  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
    1.31 +  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
    1.32 +  |> add (space_explode " " (Config.get ctxt options))
    1.33 +
    1.34 +fun pretty_config context = [
    1.35 +  Pretty.str ("With proofs: " ^
    1.36 +    (if Config.get_generic context proofs then "true" else "false")),
    1.37 +  Pretty.str ("Options: " ^
    1.38 +    space_implode " " (get_options (Context.proof_of context))) ]
    1.39 +
    1.40 +fun cmdline_options ctxt =
    1.41 +  get_options ctxt
    1.42 +  |> add ["-smt"]
    1.43 +
    1.44 +fun raise_cex real recon ls =
    1.45 +  let val cex = Z3_Model.parse_counterex recon ls
    1.46 +  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
    1.47 +
    1.48 +fun check_unsat recon output =
    1.49 +  let
    1.50 +    val raw = not o String.isPrefix "WARNING" orf String.isPrefix "ERROR"
    1.51 +    val (ls, l) = the_default ([], "") (try split_last (filter raw output))
    1.52 +  in
    1.53 +    if String.isPrefix "unsat" l then ls
    1.54 +    else if String.isPrefix "sat" l then raise_cex true recon ls
    1.55 +    else if String.isPrefix "unknown" l then raise_cex false recon ls
    1.56 +    else error (solver_name ^ " failed")
    1.57 +  end
    1.58 +
    1.59 +fun core_oracle (SMT_Solver.ProofData {output, recon, ...}) =
    1.60 +  check_unsat recon output
    1.61 +  |> K @{cprop False}
    1.62 +
    1.63 +(* FIXME
    1.64 +fun prover (SMT_Solver.ProofData {context, output, recon, assms}) =
    1.65 +  check_unsat recon output
    1.66 +  |> Z3_Proof.reconstruct context assms recon
    1.67 +*)
    1.68 +
    1.69 +fun solver oracle ctxt =
    1.70 +  let val with_proof = Config.get ctxt proofs
    1.71 +  in
    1.72 +    SMT_Solver.SolverConfig {
    1.73 +      name = {env_var=env_var, remote_name=solver_name},
    1.74 +      interface = Z3_Interface.interface,
    1.75 +      arguments = cmdline_options ctxt,
    1.76 +      reconstruct = (*FIXME:if with_proof then prover else*) oracle }
    1.77 +  end
    1.78 +
    1.79 +val setup =
    1.80 +  proofs_setup #>
    1.81 +  options_setup #>
    1.82 +  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
    1.83 +  SMT_Solver.add_solver (solver_name, solver oracle)) #>
    1.84 +  SMT_Solver.add_solver_info (solver_name, pretty_config)
    1.85 +
    1.86 +end