src/HOL/Library/Old_SMT/old_smt_setup_solvers.ML
author blanchet
Wed Sep 24 15:45:55 2014 +0200 (2014-09-24)
changeset 58425 246985c6b20b
parent 58063 663ae2463f32
child 59966 c01cea2ba71e
permissions -rw-r--r--
simpler proof
     1 (*  Title:      HOL/Library/Old_SMT/old_smt_setup_solvers.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Setup SMT solvers.
     5 *)
     6 
     7 signature OLD_SMT_SETUP_SOLVERS =
     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_with_extensions: bool Config.T
    15   val setup: theory -> theory
    16 end
    17 
    18 structure Old_SMT_Setup_Solvers: OLD_SMT_SETUP_SOLVERS =
    19 struct
    20 
    21 (* helper functions *)
    22 
    23 fun make_avail name () = getenv ("OLD_" ^ name ^ "_SOLVER") <> ""
    24 fun make_command name () = [getenv ("OLD_" ^ name ^ "_SOLVER")]
    25 
    26 fun outcome_of unsat sat unknown solver_name line =
    27   if String.isPrefix unsat line then Old_SMT_Solver.Unsat
    28   else if String.isPrefix sat line then Old_SMT_Solver.Sat
    29   else if String.isPrefix unknown line then Old_SMT_Solver.Unknown
    30   else raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure ("Solver " ^
    31     quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
    32     "configuration option " ^ quote (Config.name_of Old_SMT_Config.trace) ^ " and " ^
    33     "see the trace for details."))
    34 
    35 fun on_first_line test_outcome solver_name lines =
    36   let
    37     val empty_line = (fn "" => true | _ => false)
    38     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
    39     val (l, ls) = split_first (snd (take_prefix empty_line lines))
    40   in (test_outcome solver_name l, ls) end
    41 
    42 
    43 (* CVC3 *)
    44 
    45 local
    46   fun cvc3_options ctxt = [
    47     "-seed", string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
    48     "-lang", "smtlib", "-output-lang", "presentation",
    49     "-timeout", string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout))]
    50 in
    51 
    52 val cvc3: Old_SMT_Solver.solver_config = {
    53   name = "cvc3",
    54   class = K Old_SMTLIB_Interface.smtlibC,
    55   avail = make_avail "CVC3",
    56   command = make_command "CVC3",
    57   options = cvc3_options,
    58   default_max_relevant = 400 (* FUDGE *),
    59   supports_filter = false,
    60   outcome =
    61     on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    62   cex_parser = NONE,
    63   reconstruct = NONE }
    64 
    65 end
    66 
    67 
    68 (* Yices *)
    69 
    70 val yices: Old_SMT_Solver.solver_config = {
    71   name = "yices",
    72   class = K Old_SMTLIB_Interface.smtlibC,
    73   avail = make_avail "YICES",
    74   command = make_command "YICES",
    75   options = (fn ctxt => [
    76     "--rand-seed=" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
    77     "--timeout=" ^
    78       string_of_int (Real.ceil (Config.get ctxt Old_SMT_Config.timeout)),
    79     "--smtlib"]),
    80   default_max_relevant = 350 (* FUDGE *),
    81   supports_filter = false,
    82   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
    83   cex_parser = NONE,
    84   reconstruct = NONE }
    85 
    86 
    87 (* Z3 *)
    88 
    89 datatype z3_non_commercial =
    90   Z3_Non_Commercial_Unknown |
    91   Z3_Non_Commercial_Accepted |
    92   Z3_Non_Commercial_Declined
    93 
    94 
    95 local
    96   val accepted = member (op =) ["yes", "Yes", "YES"]
    97   val declined = member (op =) ["no", "No", "NO"]
    98 in
    99 
   100 fun z3_non_commercial () =
   101   let
   102     val flag1 = Options.default_string @{system_option z3_non_commercial}
   103     val flag2 = getenv "Z3_NON_COMMERCIAL"
   104   in
   105     if accepted flag1 then Z3_Non_Commercial_Accepted
   106     else if declined flag1 then Z3_Non_Commercial_Declined
   107     else if accepted flag2 then Z3_Non_Commercial_Accepted
   108     else if declined flag2 then Z3_Non_Commercial_Declined
   109     else Z3_Non_Commercial_Unknown
   110   end
   111 
   112 fun if_z3_non_commercial f =
   113   (case z3_non_commercial () of
   114     Z3_Non_Commercial_Accepted => f ()
   115   | Z3_Non_Commercial_Declined =>
   116       error (Pretty.string_of (Pretty.para
   117         "The SMT solver Z3 may only be used for non-commercial applications."))
   118   | Z3_Non_Commercial_Unknown =>
   119       error
   120         (Pretty.string_of
   121           (Pretty.para
   122             ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
   123              \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
   124              \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^
   125         "\n\nSee also " ^ Url.print (Url.explode "http://z3.codeplex.com/license")))
   126 
   127 end
   128 
   129 
   130 val z3_with_extensions =
   131   Attrib.setup_config_bool @{binding old_z3_with_extensions} (K false)
   132 
   133 local
   134   fun z3_make_command name () = if_z3_non_commercial (make_command name)
   135 
   136   fun z3_options ctxt =
   137     ["-rs:" ^ string_of_int (Config.get ctxt Old_SMT_Config.random_seed),
   138       "MODEL=true",
   139       "SOFT_TIMEOUT=" ^
   140         string_of_int (Real.ceil (1000.0 * Config.get ctxt Old_SMT_Config.timeout)),
   141       "-smt"]
   142     |> not (Config.get ctxt Old_SMT_Config.oracle) ?
   143          append ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
   144 
   145   fun z3_on_first_or_last_line solver_name lines =
   146     let
   147       fun junk l =
   148         if String.isPrefix "WARNING: Out of allocated virtual memory" l
   149         then raise Old_SMT_Failure.SMT Old_SMT_Failure.Out_Of_Memory
   150         else
   151           String.isPrefix "WARNING" l orelse
   152           String.isPrefix "ERROR" l orelse
   153           forall Symbol.is_ascii_blank (Symbol.explode l)
   154       val lines = filter_out junk lines
   155       fun outcome split =
   156         the_default ("", []) (try split lines)
   157         |>> outcome_of "unsat" "sat" "unknown" solver_name
   158     in
   159       (* Starting with version 4.0, Z3 puts the outcome on the first line of the
   160          output rather than on the last line. *)
   161       outcome (fn lines => (hd lines, tl lines))
   162       handle Old_SMT_Failure.SMT _ => outcome (swap o split_last)
   163     end
   164 
   165   fun select_class ctxt =
   166     if Config.get ctxt z3_with_extensions then Old_Z3_Interface.smtlib_z3C
   167     else Old_SMTLIB_Interface.smtlibC
   168 in
   169 
   170 val z3: Old_SMT_Solver.solver_config = {
   171   name = "z3",
   172   class = select_class,
   173   avail = make_avail "Z3",
   174   command = z3_make_command "Z3",
   175   options = z3_options,
   176   default_max_relevant = 350 (* FUDGE *),
   177   supports_filter = true,
   178   outcome = z3_on_first_or_last_line,
   179   cex_parser = SOME Old_Z3_Model.parse_counterex,
   180   reconstruct = SOME Old_Z3_Proof_Reconstruction.reconstruct }
   181 
   182 end
   183 
   184 
   185 (* overall setup *)
   186 
   187 val setup =
   188   Old_SMT_Solver.add_solver cvc3 #>
   189   Old_SMT_Solver.add_solver yices #>
   190   Old_SMT_Solver.add_solver z3
   191 
   192 end