--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Jan 04 15:46:38 2011 -0800
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Thu Jan 06 17:51:56 2011 +0100
@@ -12,6 +12,23 @@
structure SMT_Setup_Solvers: SMT_SETUP_SOLVERS =
struct
+(* helper functions *)
+
+val remote_prefix = "remote_"
+fun make_name is_remote name = name |> is_remote ? prefix remote_prefix
+
+fun make_local_avail name () = getenv (name ^ "_INSTALLED") = "yes"
+fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
+fun make_avail is_remote name =
+ if is_remote then make_remote_avail name else make_local_avail name
+
+fun make_local_command name () = [getenv (name ^ "_SOLVER")]
+fun make_remote_command name () =
+ [getenv "ISABELLE_SMT_REMOTE", getenv (name ^ "_REMOTE_SOLVER")]
+fun make_command is_remote name =
+ if is_remote then make_remote_command name
+ else make_local_command name
+
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
@@ -31,76 +48,97 @@
(* CVC3 *)
-fun cvc3 () = {
- name = "cvc3",
- env_var = "CVC3_SOLVER",
- is_remote = true,
- options = (fn ctxt => [
+local
+ fun cvc3_options ctxt = [
"-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
- "-lang", "smtlib", "-output-lang", "presentation"]),
- class = SMTLIB_Interface.smtlibC,
- outcome =
- on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
- cex_parser = NONE,
- reconstruct = NONE,
- default_max_relevant = 250 }
+ "-lang", "smtlib", "-output-lang", "presentation"]
+
+ fun mk is_remote = {
+ name = make_name is_remote "cvc3",
+ class = SMTLIB_Interface.smtlibC,
+ avail = make_avail is_remote "CVC3",
+ command = make_command is_remote "CVC3",
+ options = cvc3_options,
+ default_max_relevant = 250,
+ supports_filter = false,
+ outcome =
+ on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+ cex_parser = NONE,
+ reconstruct = NONE }
+in
+
+fun cvc3 () = mk false
+fun remote_cvc3 () = mk true
+
+end
(* Yices *)
fun yices () = {
name = "yices",
- env_var = "YICES_SOLVER",
- is_remote = false,
+ class = SMTLIB_Interface.smtlibC,
+ avail = make_local_avail "YICES",
+ command = make_local_command "YICES",
options = (fn ctxt => [
"--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--smtlib"]),
- class = SMTLIB_Interface.smtlibC,
+ default_max_relevant = 275,
+ supports_filter = false,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
cex_parser = NONE,
- reconstruct = NONE,
- default_max_relevant = 275 }
+ reconstruct = NONE }
(* Z3 *)
-fun z3_options ctxt =
- ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
- "MODEL=true", "-smt"]
- |> not (Config.get ctxt SMT_Config.oracle) ?
- append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
+local
+ fun z3_options ctxt =
+ ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+ "MODEL=true", "-smt"]
+ |> not (Config.get ctxt SMT_Config.oracle) ?
+ append ["DISPLAY_PROOF=true","PROOF_MODE=2"]
-fun z3_on_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)
- in
- the_default ("", []) (try (swap o split_last) (filter_out junk lines))
- |>> outcome_of "unsat" "sat" "unknown" solver_name
- end
+ fun z3_on_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)
+ in
+ the_default ("", []) (try (swap o split_last) (filter_out junk lines))
+ |>> outcome_of "unsat" "sat" "unknown" solver_name
+ end
-fun z3 () = {
- name = "z3",
- env_var = "Z3_SOLVER",
- is_remote = true,
- options = z3_options,
- class = Z3_Interface.smtlib_z3C,
- outcome = z3_on_last_line,
- cex_parser = SOME Z3_Model.parse_counterex,
- reconstruct = SOME Z3_Proof_Reconstruction.reconstruct,
- default_max_relevant = 225 }
+ fun mk is_remote = {
+ name = make_name is_remote "z3",
+ class = Z3_Interface.smtlib_z3C,
+ avail = make_avail is_remote "Z3",
+ command = make_command is_remote "Z3",
+ options = z3_options,
+ default_max_relevant = 225,
+ supports_filter = true,
+ outcome = z3_on_last_line,
+ cex_parser = SOME Z3_Model.parse_counterex,
+ reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
+in
+
+fun z3 () = mk false
+fun remote_z3 () = mk true
+
+end
(* overall setup *)
val setup =
SMT_Solver.add_solver (cvc3 ()) #>
+ SMT_Solver.add_solver (remote_cvc3 ()) #>
SMT_Solver.add_solver (yices ()) #>
- SMT_Solver.add_solver (z3 ())
+ SMT_Solver.add_solver (z3 ()) #>
+ SMT_Solver.add_solver (remote_z3 ())
end