--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/SMT/smt_setup_solvers.ML Thu Aug 28 00:40:37 2014 +0200
@@ -0,0 +1,193 @@
+(* Title: HOL/Library/SMT/smt_setup_solvers.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Setup SMT solvers.
+*)
+
+signature SMT_SETUP_SOLVERS =
+sig
+ datatype z3_non_commercial =
+ Z3_Non_Commercial_Unknown |
+ Z3_Non_Commercial_Accepted |
+ Z3_Non_Commercial_Declined
+ val z3_non_commercial: unit -> z3_non_commercial
+ val z3_with_extensions: bool Config.T
+ val setup: theory -> theory
+end
+
+structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
+struct
+
+(* helper functions *)
+
+fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
+
+fun make_command name () = [getenv (name ^ "_SOLVER")]
+
+fun outcome_of unsat sat unknown solver_name line =
+ if String.isPrefix unsat line then SMT_Solver.Unsat
+ else if String.isPrefix sat line then SMT_Solver.Sat
+ else if String.isPrefix unknown line then SMT_Solver.Unknown
+ else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^
+ quote solver_name ^ " failed. Enable SMT tracing by setting the " ^
+ "configuration option " ^ quote (Config.name_of SMT_Config.trace) ^ " and " ^
+ "see the trace for details."))
+
+fun on_first_line test_outcome solver_name lines =
+ let
+ val empty_line = (fn "" => true | _ => false)
+ val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
+ val (l, ls) = split_first (snd (take_prefix empty_line lines))
+ in (test_outcome solver_name l, ls) end
+
+
+(* CVC3 *)
+
+local
+ fun cvc3_options ctxt = [
+ "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
+ "-lang", "smtlib", "-output-lang", "presentation",
+ "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
+in
+
+val cvc3: SMT_Solver.solver_config = {
+ name = "cvc3",
+ class = K SMTLIB_Interface.smtlibC,
+ avail = make_avail "CVC3",
+ command = make_command "CVC3",
+ options = cvc3_options,
+ default_max_relevant = 400 (* FUDGE *),
+ supports_filter = false,
+ outcome =
+ on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+ cex_parser = NONE,
+ reconstruct = NONE }
+
+end
+
+
+(* Yices *)
+
+val yices: SMT_Solver.solver_config = {
+ name = "yices",
+ class = K SMTLIB_Interface.smtlibC,
+ avail = make_avail "YICES",
+ command = make_command "YICES",
+ options = (fn ctxt => [
+ "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+ "--timeout=" ^
+ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)),
+ "--smtlib"]),
+ default_max_relevant = 350 (* FUDGE *),
+ supports_filter = false,
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
+ cex_parser = NONE,
+ reconstruct = NONE }
+
+
+(* Z3 *)
+
+datatype z3_non_commercial =
+ Z3_Non_Commercial_Unknown |
+ Z3_Non_Commercial_Accepted |
+ Z3_Non_Commercial_Declined
+
+
+local
+ val accepted = member (op =) ["yes", "Yes", "YES"]
+ val declined = member (op =) ["no", "No", "NO"]
+in
+
+fun z3_non_commercial () =
+ let
+ val flag1 = Options.default_string @{system_option z3_non_commercial}
+ val flag2 = getenv "Z3_NON_COMMERCIAL"
+ in
+ if accepted flag1 then Z3_Non_Commercial_Accepted
+ else if declined flag1 then Z3_Non_Commercial_Declined
+ else if accepted flag2 then Z3_Non_Commercial_Accepted
+ else if declined flag2 then Z3_Non_Commercial_Declined
+ else Z3_Non_Commercial_Unknown
+ end
+
+fun if_z3_non_commercial f =
+ (case z3_non_commercial () of
+ Z3_Non_Commercial_Accepted => f ()
+ | Z3_Non_Commercial_Declined =>
+ error (Pretty.string_of (Pretty.para
+ "The SMT solver Z3 may only be used for non-commercial applications."))
+ | Z3_Non_Commercial_Unknown =>
+ error
+ (Pretty.string_of
+ (Pretty.para
+ ("The SMT solver Z3 is not activated. To activate it, set the Isabelle \
+ \system option \"z3_non_commercial\" to \"yes\" (e.g. via \
+ \the Isabelle/jEdit menu Plugin Options / Isabelle / General).")) ^
+ "\n\nSee also " ^ Url.print (Url.explode "http://z3.codeplex.com/license")))
+
+end
+
+
+val z3_with_extensions =
+ Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
+
+local
+ fun z3_make_command name () = if_z3_non_commercial (make_command name)
+
+ fun z3_options ctxt =
+ ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+ "MODEL=true",
+ "SOFT_TIMEOUT=" ^
+ string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout)),
+ "-smt"]
+ |> not (Config.get ctxt SMT_Config.oracle) ?
+ append ["DISPLAY_PROOF=true", "PROOF_MODE=2"]
+
+ fun z3_on_first_or_last_line solver_name lines =
+ let
+ fun junk l =
+ if String.isPrefix "WARNING: Out of allocated virtual memory" l
+ then raise SMT_Failure.SMT SMT_Failure.Out_Of_Memory
+ else
+ String.isPrefix "WARNING" l orelse
+ String.isPrefix "ERROR" l orelse
+ forall Symbol.is_ascii_blank (Symbol.explode l)
+ val lines = filter_out junk lines
+ fun outcome split =
+ the_default ("", []) (try split lines)
+ |>> outcome_of "unsat" "sat" "unknown" solver_name
+ in
+ (* Starting with version 4.0, Z3 puts the outcome on the first line of the
+ output rather than on the last line. *)
+ outcome (fn lines => (hd lines, tl lines))
+ handle SMT_Failure.SMT _ => outcome (swap o split_last)
+ end
+
+ fun select_class ctxt =
+ if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
+ else SMTLIB_Interface.smtlibC
+in
+
+val z3: SMT_Solver.solver_config = {
+ name = "z3",
+ class = select_class,
+ avail = make_avail "Z3",
+ command = z3_make_command "Z3",
+ options = z3_options,
+ default_max_relevant = 350 (* FUDGE *),
+ supports_filter = true,
+ outcome = z3_on_first_or_last_line,
+ cex_parser = SOME Z3_Model.parse_counterex,
+ reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
+
+end
+
+
+(* overall setup *)
+
+val setup =
+ SMT_Solver.add_solver cvc3 #>
+ SMT_Solver.add_solver yices #>
+ SMT_Solver.add_solver z3
+
+end