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