src/HOL/Tools/SMT/z3_solver.ML
author boehmes
Wed, 12 May 2010 23:54:04 +0200
changeset 36899 bcd6fce5bf06
child 39298 5aefb5bc8a93
permissions -rw-r--r--
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/z3_solver.ML
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     3
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     4
Interface of the SMT solver Z3.
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     5
*)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     6
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     7
signature Z3_SOLVER =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     8
sig
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
     9
  val proofs: bool Config.T
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    10
  val options: string Config.T
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    11
  val setup: theory -> theory
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    12
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    13
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    14
structure Z3_Solver: Z3_SOLVER =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    15
struct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    16
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    17
val solver_name = "z3"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    18
val env_var = "Z3_SOLVER"
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    19
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    20
val (proofs, proofs_setup) = Attrib.config_bool "z3_proofs" (K false)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    21
val (options, options_setup) = Attrib.config_string "z3_options" (K "")
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    22
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    23
fun add xs ys = ys @ xs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    24
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    25
fun explode_options s = String.tokens (Symbol.is_ascii_blank o str) s
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    26
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    27
fun get_options ctxt =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    28
  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false"]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    29
  |> Config.get ctxt proofs ? add ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    30
  |> add (explode_options (Config.get ctxt options))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    31
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    32
fun pretty_config context = [
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    33
  Pretty.str ("With proofs: " ^
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    34
    (if Config.get_generic context proofs then "true" else "false")),
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    35
  Pretty.str ("Options: " ^
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    36
    space_implode " " (get_options (Context.proof_of context))) ]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    37
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    38
fun cmdline_options ctxt =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    39
  get_options ctxt
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    40
  |> add ["-smt"]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    41
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    42
fun raise_cex real recon ls =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    43
  let val cex = Z3_Model.parse_counterex recon ls
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    44
  in raise SMT_Solver.SMT_COUNTEREXAMPLE (real, cex) end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    45
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    46
fun if_unsat f (output, recon) =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    47
  let
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    48
    fun jnk l =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    49
      String.isPrefix "WARNING" l orelse
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    50
      String.isPrefix "ERROR" l orelse
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    51
      forall Symbol.is_ascii_blank (Symbol.explode l)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    52
    val (ls, l) = the_default ([], "") (try split_last (filter_out jnk output))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    53
  in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    54
    if String.isPrefix "unsat" l then f (ls, recon)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    55
    else if String.isPrefix "sat" l then raise_cex true recon ls
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    56
    else if String.isPrefix "unknown" l then raise_cex false recon ls
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    57
    else raise SMT_Solver.SMT (solver_name ^ " failed")
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    58
  end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    59
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    60
val core_oracle = if_unsat (K @{cprop False})
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    61
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    62
val prover = if_unsat Z3_Proof_Reconstruction.reconstruct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    63
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    64
fun solver oracle ctxt =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    65
  let val with_proof = Config.get ctxt proofs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    66
  in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    67
   {command = {env_var=env_var, remote_name=SOME solver_name},
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    68
    arguments = cmdline_options ctxt,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    69
    interface = Z3_Interface.interface,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    70
    reconstruct = if with_proof then prover else pair o oracle}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    71
  end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    72
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    73
val setup =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    74
  proofs_setup #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    75
  options_setup #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    76
  Thm.add_oracle (Binding.name solver_name, core_oracle) #-> (fn (_, oracle) =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    77
  Context.theory_map (SMT_Solver.add_solver (solver_name, solver oracle))) #>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    78
  Context.theory_map (SMT_Solver.add_solver_info (solver_name, pretty_config))
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    79
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff changeset
    80
end