src/HOL/Tools/SMT/smt_systems.ML
author nipkow
Wed Jan 10 15:25:09 2018 +0100 (19 months ago)
changeset 67399 eab6ce8368fa
parent 66551 4df6b0ae900d
child 67405 e9ab4ad7bd15
permissions -rw-r--r--
ran isabelle update_op on all sources
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smt_systems.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Setup SMT solvers.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature SMT_SYSTEMS =
blanchet@56078
     8
sig
blanchet@59960
     9
  val cvc4_extensions: bool Config.T
blanchet@56078
    10
  val z3_extensions: bool Config.T
blanchet@57229
    11
end;
blanchet@56078
    12
blanchet@58061
    13
structure SMT_Systems: SMT_SYSTEMS =
blanchet@56078
    14
struct
blanchet@56078
    15
blanchet@56078
    16
(* helper functions *)
blanchet@56078
    17
blanchet@56078
    18
fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
blanchet@56078
    19
blanchet@56078
    20
fun make_command name () = [getenv (name ^ "_SOLVER")]
blanchet@56078
    21
blanchet@56078
    22
fun outcome_of unsat sat unknown solver_name line =
blanchet@58061
    23
  if String.isPrefix unsat line then SMT_Solver.Unsat
blanchet@58061
    24
  else if String.isPrefix sat line then SMT_Solver.Sat
blanchet@58061
    25
  else if String.isPrefix unknown line then SMT_Solver.Unknown
blanchet@58061
    26
  else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
blanchet@58061
    27
    " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
blanchet@56094
    28
    " option for details"))
blanchet@56078
    29
blanchet@60201
    30
fun is_blank_or_error_line "" = true
blanchet@60201
    31
  | is_blank_or_error_line s = String.isPrefix "(error " s
blanchet@60201
    32
blanchet@57239
    33
fun on_first_line test_outcome solver_name lines =
blanchet@56078
    34
  let
blanchet@56078
    35
    val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
blanchet@60201
    36
    val (l, ls) = split_first (snd (take_prefix is_blank_or_error_line lines))
blanchet@56078
    37
  in (test_outcome solver_name l, ls) end
blanchet@56078
    38
fleury@57704
    39
fun on_first_non_unsupported_line test_outcome solver_name lines =
nipkow@67399
    40
  on_first_line test_outcome solver_name (filter (curry (<>) "unsupported") lines)
blanchet@56078
    41
blanchet@56078
    42
(* CVC3 *)
blanchet@56078
    43
blanchet@56078
    44
local
blanchet@56078
    45
  fun cvc3_options ctxt = [
blanchet@58061
    46
    "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
blanchet@57239
    47
    "-lang", "smt2",
blanchet@58061
    48
    "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
blanchet@56078
    49
in
blanchet@56078
    50
blanchet@58061
    51
val cvc3: SMT_Solver.solver_config = {
blanchet@57209
    52
  name = "cvc3",
blanchet@58061
    53
  class = K SMTLIB_Interface.smtlibC,
blanchet@57210
    54
  avail = make_avail "CVC3",
blanchet@57210
    55
  command = make_command "CVC3",
blanchet@56078
    56
  options = cvc3_options,
blanchet@57239
    57
  smt_options = [],
blanchet@56078
    58
  default_max_relevant = 400 (* FUDGE *),
blanchet@57239
    59
  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
blanchet@57157
    60
  parse_proof = NONE,
blanchet@56078
    61
  replay = NONE }
blanchet@56078
    62
blanchet@56078
    63
end
blanchet@56078
    64
blanchet@66551
    65
blanchet@57240
    66
(* CVC4 *)
blanchet@57240
    67
blanchet@58360
    68
val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
blanchet@58360
    69
blanchet@57240
    70
local
blanchet@57240
    71
  fun cvc4_options ctxt = [
blanchet@64461
    72
    "--no-statistics",
blanchet@58061
    73
    "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
blanchet@57240
    74
    "--lang=smt2",
blanchet@60201
    75
    "--continued-execution",
blanchet@58061
    76
    "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
blanchet@58360
    77
blanchet@58360
    78
  fun select_class ctxt =
blanchet@66551
    79
    if Config.get ctxt cvc4_extensions then
blanchet@66551
    80
      if Config.get ctxt SMT_Config.higher_order then
blanchet@66551
    81
        CVC4_Interface.hosmtlib_cvc4C
blanchet@66551
    82
      else
blanchet@66551
    83
        CVC4_Interface.smtlib_cvc4C
blanchet@66551
    84
    else
blanchet@66551
    85
      if Config.get ctxt SMT_Config.higher_order then
blanchet@66551
    86
        SMTLIB_Interface.hosmtlibC
blanchet@66551
    87
      else
blanchet@66551
    88
        SMTLIB_Interface.smtlibC
blanchet@57240
    89
in
blanchet@57240
    90
blanchet@58061
    91
val cvc4: SMT_Solver.solver_config = {
blanchet@57240
    92
  name = "cvc4",
blanchet@58360
    93
  class = select_class,
blanchet@57240
    94
  avail = make_avail "CVC4",
blanchet@57240
    95
  command = make_command "CVC4",
blanchet@57240
    96
  options = cvc4_options,
blanchet@59015
    97
  smt_options = [(":produce-unsat-cores", "true")],
blanchet@57240
    98
  default_max_relevant = 400 (* FUDGE *),
blanchet@57240
    99
  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
blanchet@59015
   100
  parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
blanchet@57240
   101
  replay = NONE }
blanchet@57240
   102
blanchet@57240
   103
end
blanchet@57240
   104
blanchet@66551
   105
fleury@57704
   106
(* veriT *)
fleury@57704
   107
blanchet@66551
   108
local
blanchet@66551
   109
  fun select_class ctxt =
blanchet@66551
   110
    if Config.get ctxt SMT_Config.higher_order then
blanchet@66551
   111
      SMTLIB_Interface.hosmtlibC
blanchet@66551
   112
    else
blanchet@66551
   113
      SMTLIB_Interface.smtlibC
blanchet@66551
   114
in
blanchet@66551
   115
blanchet@58061
   116
val veriT: SMT_Solver.solver_config = {
blanchet@59035
   117
  name = "verit",
blanchet@66551
   118
  class = select_class,
fleury@57704
   119
  avail = make_avail "VERIT",
fleury@57704
   120
  command = make_command "VERIT",
fleury@57704
   121
  options = (fn ctxt => [
fleury@57704
   122
    "--proof-version=1",
fleury@57704
   123
    "--proof-prune",
fleury@57704
   124
    "--proof-merge",
fleury@57704
   125
    "--disable-print-success",
fleury@57704
   126
    "--disable-banner",
blanchet@58061
   127
    "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
Mathias@61587
   128
  smt_options = [(":produce-proofs", "true")],
blanchet@58496
   129
  default_max_relevant = 200 (* FUDGE *),
Mathias@63102
   130
  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown"),
blanchet@58491
   131
  parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
fleury@57704
   132
  replay = NONE }
blanchet@57240
   133
blanchet@66551
   134
end
blanchet@66551
   135
blanchet@66551
   136
blanchet@56078
   137
(* Z3 *)
blanchet@56078
   138
blanchet@58061
   139
val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
blanchet@56078
   140
blanchet@56078
   141
local
blanchet@56078
   142
  fun z3_options ctxt =
blanchet@58061
   143
    ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
blanchet@57168
   144
     "smt.refine_inj_axioms=false",
blanchet@58061
   145
     "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
blanchet@56078
   146
     "-smt2"]
blanchet@56078
   147
blanchet@56078
   148
  fun select_class ctxt =
blanchet@58061
   149
    if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
blanchet@56078
   150
in
blanchet@56078
   151
blanchet@58061
   152
val z3: SMT_Solver.solver_config = {
blanchet@57209
   153
  name = "z3",
blanchet@56078
   154
  class = select_class,
blanchet@59960
   155
  avail = make_avail "Z3",
blanchet@59960
   156
  command = make_command "Z3",
blanchet@56078
   157
  options = z3_options,
blanchet@57239
   158
  smt_options = [(":produce-proofs", "true")],
blanchet@56078
   159
  default_max_relevant = 350 (* FUDGE *),
blanchet@57239
   160
  outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
blanchet@58061
   161
  parse_proof = SOME Z3_Replay.parse_proof,
blanchet@58061
   162
  replay = SOME Z3_Replay.replay }
blanchet@56078
   163
blanchet@56078
   164
end
blanchet@56078
   165
blanchet@56078
   166
blanchet@56078
   167
(* overall setup *)
blanchet@56078
   168
blanchet@56078
   169
val _ = Theory.setup (
blanchet@58061
   170
  SMT_Solver.add_solver cvc3 #>
blanchet@58061
   171
  SMT_Solver.add_solver cvc4 #>
blanchet@58061
   172
  SMT_Solver.add_solver veriT #>
blanchet@58061
   173
  SMT_Solver.add_solver z3)
blanchet@56078
   174
blanchet@57229
   175
end;