src/HOL/Tools/SMT/smt_systems.ML
author blanchet
Wed Sep 17 16:53:39 2014 +0200 (2014-09-17)
changeset 58360 dee1fd1cc631
parent 58061 3d060f43accb
child 58491 5ddbc170e46c
permissions -rw-r--r--
added interface for CVC4 extensions
     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   datatype z3_non_commercial =
    10     Z3_Non_Commercial_Unknown |
    11     Z3_Non_Commercial_Accepted |
    12     Z3_Non_Commercial_Declined
    13   val z3_non_commercial: unit -> z3_non_commercial
    14   val z3_extensions: bool Config.T
    15 end;
    16 
    17 structure SMT_Systems: SMT_SYSTEMS =
    18 struct
    19 
    20 (* helper functions *)
    21 
    22 fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
    23 
    24 fun make_command name () = [getenv (name ^ "_SOLVER")]
    25 
    26 fun outcome_of unsat sat unknown solver_name line =
    27   if String.isPrefix unsat line then SMT_Solver.Unsat
    28   else if String.isPrefix sat line then SMT_Solver.Sat
    29   else if String.isPrefix unknown line then SMT_Solver.Unknown
    30   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
    31     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
    32     " option for details"))
    33 
    34 fun on_first_line test_outcome solver_name lines =
    35   let
    36     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    37     val (l, ls) = split_first (snd (take_prefix (curry (op =) "") lines))
    38   in (test_outcome solver_name l, ls) end
    39 
    40 fun on_first_non_unsupported_line test_outcome solver_name lines =
    41   on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
    42 
    43 (* CVC3 *)
    44 
    45 local
    46   fun cvc3_options ctxt = [
    47     "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
    48     "-lang", "smt2",
    49     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
    50 in
    51 
    52 val cvc3: SMT_Solver.solver_config = {
    53   name = "cvc3",
    54   class = K SMTLIB_Interface.smtlibC,
    55   avail = make_avail "CVC3",
    56   command = make_command "CVC3",
    57   options = cvc3_options,
    58   smt_options = [],
    59   default_max_relevant = 400 (* FUDGE *),
    60   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    61   parse_proof = NONE,
    62   replay = NONE }
    63 
    64 end
    65 
    66 
    67 (* CVC4 *)
    68 
    69 val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
    70 
    71 local
    72   fun cvc4_options ctxt = [
    73     "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    74     "--lang=smt2",
    75     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
    76 
    77   fun select_class ctxt =
    78     if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
    79     else SMTLIB_Interface.smtlibC
    80 in
    81 
    82 val cvc4: SMT_Solver.solver_config = {
    83   name = "cvc4",
    84   class = select_class,
    85   avail = make_avail "CVC4",
    86   command = make_command "CVC4",
    87   options = cvc4_options,
    88   smt_options = [],
    89   default_max_relevant = 400 (* FUDGE *),
    90   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    91   parse_proof = NONE,
    92   replay = NONE }
    93 
    94 end
    95 
    96 (* veriT *)
    97 
    98 val veriT: SMT_Solver.solver_config = {
    99   name = "veriT",
   100   class = K SMTLIB_Interface.smtlibC,
   101   avail = make_avail "VERIT",
   102   command = make_command "VERIT",
   103   options = (fn ctxt => [
   104     "--proof-version=1",
   105     "--proof=-",
   106     "--proof-prune",
   107     "--proof-merge",
   108     "--disable-print-success",
   109     "--disable-banner",
   110     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
   111   smt_options = [],
   112   default_max_relevant = 120 (* FUDGE *),
   113   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
   114     "warning : proof_done: status is still open"),
   115   parse_proof = SOME VeriT_Proof_Parse.parse_proof,
   116   replay = NONE }
   117 
   118 (* Z3 *)
   119 
   120 datatype z3_non_commercial =
   121   Z3_Non_Commercial_Unknown |
   122   Z3_Non_Commercial_Accepted |
   123   Z3_Non_Commercial_Declined
   124 
   125 local
   126   val accepted = member (op =) ["yes", "Yes", "YES"]
   127   val declined = member (op =) ["no", "No", "NO"]
   128 in
   129 
   130 fun z3_non_commercial () =
   131   let
   132     val flag1 = Options.default_string @{system_option z3_non_commercial}
   133     val flag2 = getenv "Z3_NON_COMMERCIAL"
   134   in
   135     if accepted flag1 then Z3_Non_Commercial_Accepted
   136     else if declined flag1 then Z3_Non_Commercial_Declined
   137     else if accepted flag2 then Z3_Non_Commercial_Accepted
   138     else if declined flag2 then Z3_Non_Commercial_Declined
   139     else Z3_Non_Commercial_Unknown
   140   end
   141 
   142 fun if_z3_non_commercial f =
   143   (case z3_non_commercial () of
   144     Z3_Non_Commercial_Accepted => f ()
   145   | Z3_Non_Commercial_Declined =>
   146       error (Pretty.string_of (Pretty.para
   147         "The SMT solver Z3 may be used only for non-commercial applications."))
   148   | Z3_Non_Commercial_Unknown =>
   149       error (Pretty.string_of (Pretty.para
   150         ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
   151          \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
   152          \the Isabelle/jEdit menu Plugin Options / Isabelle / General)."))))
   153 
   154 end
   155 
   156 val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
   157 
   158 local
   159   fun z3_make_command name () = if_z3_non_commercial (make_command name)
   160 
   161   fun z3_options ctxt =
   162     ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
   163      "smt.refine_inj_axioms=false",
   164      "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
   165      "-smt2"]
   166 
   167   fun select_class ctxt =
   168     if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC
   169 in
   170 
   171 val z3: SMT_Solver.solver_config = {
   172   name = "z3",
   173   class = select_class,
   174   avail = make_avail "Z3_NEW",
   175   command = z3_make_command "Z3_NEW",
   176   options = z3_options,
   177   smt_options = [(":produce-proofs", "true")],
   178   default_max_relevant = 350 (* FUDGE *),
   179   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   180   parse_proof = SOME Z3_Replay.parse_proof,
   181   replay = SOME Z3_Replay.replay }
   182 
   183 end
   184 
   185 
   186 (* overall setup *)
   187 
   188 val _ = Theory.setup (
   189   SMT_Solver.add_solver cvc3 #>
   190   SMT_Solver.add_solver cvc4 #>
   191   SMT_Solver.add_solver veriT #>
   192   SMT_Solver.add_solver z3)
   193 
   194 end;