src/HOL/Tools/SMT/smt_setup_solvers.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40424 7550b2cba1cb
child 40981 67f436af0638
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
boehmes@40162
     1
(*  Title:      HOL/Tools/SMT/smt_setup_solvers.ML
boehmes@40162
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@40162
     3
boehmes@40162
     4
Setup SMT solvers.
boehmes@40162
     5
*)
boehmes@40162
     6
boehmes@40162
     7
signature SMT_SETUP_SOLVERS =
boehmes@40162
     8
sig
boehmes@40162
     9
  val setup: theory -> theory
boehmes@40162
    10
end
boehmes@40162
    11
boehmes@40162
    12
structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
boehmes@40162
    13
struct
boehmes@40162
    14
boehmes@40162
    15
fun outcome_of unsat sat unknown solver_name line =
boehmes@40162
    16
  if String.isPrefix unsat line then SMT_Solver.Unsat
boehmes@40162
    17
  else if String.isPrefix sat line then SMT_Solver.Sat
boehmes@40162
    18
  else if String.isPrefix unknown line then SMT_Solver.Unknown
boehmes@40424
    19
  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
boehmes@40276
    20
    quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
boehmes@40424
    21
    "configuration option " ^ quote SMT_Config.traceN ^ " and " ^
boehmes@40276
    22
    " see the trace for details."))
boehmes@40162
    23
boehmes@40162
    24
fun on_first_line test_outcome solver_name lines =
boehmes@40162
    25
  let
boehmes@40162
    26
    val empty_line = (fn "" => true | _ => false)
boehmes@40162
    27
    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
boehmes@40162
    28
    val (l, ls) = split_first (snd (chop_while empty_line lines))
boehmes@40162
    29
  in (test_outcome solver_name l, ls) end
boehmes@40162
    30
boehmes@40162
    31
boehmes@40162
    32
(* CVC3 *)
boehmes@40162
    33
boehmes@40208
    34
fun cvc3 () = {
boehmes@40162
    35
  name = "cvc3",
boehmes@40162
    36
  env_var = "CVC3_SOLVER",
boehmes@40162
    37
  is_remote = true,
boehmes@40162
    38
  options = K ["-lang", "smtlib", "-output-lang", "presentation"],
boehmes@40162
    39
  interface = SMTLIB_Interface.interface,
boehmes@40162
    40
  outcome =
boehmes@40162
    41
    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
boehmes@40162
    42
  cex_parser = NONE,
boehmes@40162
    43
  reconstruct = NONE }
boehmes@40162
    44
boehmes@40162
    45
boehmes@40162
    46
(* Yices *)
boehmes@40162
    47
boehmes@40208
    48
fun yices () = {
boehmes@40162
    49
  name = "yices",
boehmes@40162
    50
  env_var = "YICES_SOLVER",
boehmes@40162
    51
  is_remote = false,
boehmes@40162
    52
  options = K ["--smtlib"],
boehmes@40162
    53
  interface = SMTLIB_Interface.interface,
boehmes@40162
    54
  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
boehmes@40162
    55
  cex_parser = NONE,
boehmes@40162
    56
  reconstruct = NONE }
boehmes@40162
    57
boehmes@40162
    58
boehmes@40162
    59
(* Z3 *)
boehmes@40162
    60
boehmes@40162
    61
fun z3_options ctxt =
boehmes@40162
    62
  ["MODEL=true", "PRE_SIMPLIFY_EXPR=false", "CONTEXT_SIMPLIFIER=false", "-smt"]
boehmes@40424
    63
  |> not (Config.get ctxt SMT_Config.oracle) ?
boehmes@40162
    64
       append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
boehmes@40162
    65
boehmes@40162
    66
fun z3_on_last_line solver_name lines =
boehmes@40162
    67
  let
boehmes@40162
    68
    fun junk l =
boehmes@40197
    69
      if String.isPrefix "WARNING: Out of allocated virtual memory" l
boehmes@40424
    70
      then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
boehmes@40197
    71
      else
boehmes@40197
    72
        String.isPrefix "WARNING" l orelse
boehmes@40197
    73
        String.isPrefix "ERROR" l orelse
boehmes@40197
    74
        forall Symbol.is_ascii_blank (Symbol.explode l)
boehmes@40162
    75
  in
boehmes@40162
    76
    the_default ("", []) (try (swap o split_last) (filter_out junk lines))
boehmes@40162
    77
    |>> outcome_of "unsat" "sat" "unknown" solver_name
boehmes@40162
    78
  end
boehmes@40162
    79
boehmes@40208
    80
fun z3 () = {
boehmes@40162
    81
  name = "z3",
boehmes@40162
    82
  env_var = "Z3_SOLVER",
boehmes@40162
    83
  is_remote = true,
boehmes@40162
    84
  options = z3_options,
boehmes@40162
    85
  interface = Z3_Interface.interface,
boehmes@40162
    86
  outcome = z3_on_last_line,
boehmes@40162
    87
  cex_parser = SOME Z3_Model.parse_counterex,
boehmes@40162
    88
  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
boehmes@40162
    89
boehmes@40162
    90
boehmes@40162
    91
(* overall setup *)
boehmes@40162
    92
boehmes@40162
    93
val setup =
boehmes@40208
    94
  SMT_Solver.add_solver (cvc3 ()) #>
boehmes@40208
    95
  SMT_Solver.add_solver (yices ()) #>
boehmes@40208
    96
  SMT_Solver.add_solver (z3 ())
boehmes@40162
    97
boehmes@40162
    98
end