# HG changeset patch # User boehmes # Date 1294332716 -3600 # Node ID 3214c39777ab50c72a509d7226ca60501d140dfd # Parent 138f414f14cb69c0bf82170e2c9327a448cc9108 differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); turned individual SMT solvers into components; made CVC3 the default SMT solver (Z3 is licensed as "non-commercial only"); tuned smt_filter interface diff -r 138f414f14cb -r 3214c39777ab Admin/contributed_components --- a/Admin/contributed_components Tue Jan 04 15:46:38 2011 -0800 +++ b/Admin/contributed_components Thu Jan 06 17:51:56 2011 +0100 @@ -1,7 +1,9 @@ #contributed components +contrib/cvc3-2.2 contrib/e-1.2 contrib/jedit-4.3.2 contrib/kodkodi-1.2.16 contrib/spass-3.7 contrib/scala-2.8.0.RC5 contrib/vampire-1.0 +contrib/z3-2.15 diff -r 138f414f14cb -r 3214c39777ab NEWS --- a/NEWS Tue Jan 04 15:46:38 2011 -0800 +++ b/NEWS Thu Jan 06 17:51:56 2011 +0100 @@ -272,15 +272,31 @@ * Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as command 'solve_direct'. +* The default SMT solver is now CVC3. Z3 must be enabled explicitly, +due to licensing issues. + +* Remote SMT solvers need to be referred to by the "remote_" prefix, +i.e., "remote_cvc3" and "remote_z3". + +* Added basic SMT support for datatypes, records, and typedefs +using the oracle mode (no proofs). Direct support of pairs has been +dropped in exchange (pass theorems fst_conv snd_conv pair_collapse to +the SMT support for a similar behaviour). MINOR INCOMPATIBILITY. + * Changed SMT configuration options: - Renamed: - z3_proofs ~> smt_oracle (with swapped semantics) + z3_proofs ~> smt_oracle (with inverted meaning) z3_trace_assms ~> smt_trace_used_facts INCOMPATIBILITY. - Added: smt_verbose + smt_random_seed smt_datatypes + smt_infer_triggers + smt_monomorph_limit cvc3_options + remote_cvc3_options + remote_z3_options yices_options * Boogie output files (.b2i files) need to be declared in the theory diff -r 138f414f14cb -r 3214c39777ab src/HOL/Boogie/Examples/Boogie_Dijkstra.thy --- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Thu Jan 06 17:51:56 2011 +0100 @@ -84,7 +84,7 @@ declare [[smt_certificates="Boogie_Dijkstra.certs"]] declare [[smt_fixed=true]] -declare [[smt_oracle=false]] +declare [[smt_solver=z3, smt_oracle=false]] boogie_vc Dijkstra by boogie diff -r 138f414f14cb -r 3214c39777ab src/HOL/Boogie/Examples/Boogie_Max.thy --- a/src/HOL/Boogie/Examples/Boogie_Max.thy Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Thu Jan 06 17:51:56 2011 +0100 @@ -41,7 +41,7 @@ declare [[smt_certificates="Boogie_Max.certs"]] declare [[smt_fixed=true]] -declare [[smt_oracle=false]] +declare [[smt_solver=z3, smt_oracle=false]] boogie_vc max by boogie diff -r 138f414f14cb -r 3214c39777ab src/HOL/Boogie/Examples/VCC_Max.thy --- a/src/HOL/Boogie/Examples/VCC_Max.thy Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Boogie/Examples/VCC_Max.thy Thu Jan 06 17:51:56 2011 +0100 @@ -49,7 +49,7 @@ declare [[smt_certificates="VCC_Max.certs"]] declare [[smt_fixed=true]] -declare [[smt_oracle=false]] +declare [[smt_solver=z3, smt_oracle=false]] boogie_status diff -r 138f414f14cb -r 3214c39777ab src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Jan 06 17:51:56 2011 +0100 @@ -12,7 +12,7 @@ declare [[smt_certificates="Integration.certs"]] declare [[smt_fixed=true]] -declare [[smt_oracle=false]] +declare [[smt_solver=z3, smt_oracle=false]] setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *} @@ -5527,5 +5527,6 @@ declare [[smt_certificates=""]] declare [[smt_fixed=false]] +declare [[smt_solver=cvc3]] end diff -r 138f414f14cb -r 3214c39777ab src/HOL/SMT.thy --- a/src/HOL/SMT.thy Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/SMT.thy Thu Jan 06 17:51:56 2011 +0100 @@ -176,17 +176,11 @@ text {* The option @{text smt_solver} can be used to change the target SMT -solver. The possible values are @{text cvc3}, @{text yices}, and -@{text z3}. It is advisable to locally install the selected solver, -although this is not necessary for @{text cvc3} and @{text z3}, which -can also be used over an Internet-based service. - -When using local SMT solvers, the path to their binaries should be -declared by setting the following environment variables: -@{text CVC3_SOLVER}, @{text YICES_SOLVER}, and @{text Z3_SOLVER}. +solver. The possible values can be obtained from the @{text smt_status} +command. *} -declare [[ smt_solver = z3 ]] +declare [[ smt_solver = cvc3 ]] text {* Since SMT solvers are potentially non-terminating, there is a timeout @@ -218,7 +212,9 @@ options. *} -declare [[ cvc3_options = "", yices_options = "", z3_options = "" ]] +declare [[ cvc3_options = "", remote_cvc3_options = "" ]] +declare [[ yices_options = "" ]] +declare [[ z3_options = "", remote_z3_options = "" ]] text {* Enable the following option to use built-in support for datatypes and diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/SMT/etc/settings --- a/src/HOL/Tools/SMT/etc/settings Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/SMT/etc/settings Thu Jan 06 17:51:56 2011 +0100 @@ -2,14 +2,6 @@ ISABELLE_SMT="$COMPONENT" -REMOTE_SMT="$ISABELLE_SMT/lib/scripts/remote_smt" - -REMOTE_SMT_URL="http://smt.in.tum.de/smt" +ISABELLE_SMT_REMOTE="$ISABELLE_SMT/lib/scripts/remote_smt" +ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt" -# -# Paths to local SMT solvers: -# -# CVC_SOLVER=PATH -# YICES_SOLVER=PATH -# Z3_SOLVER=PATH - diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/SMT/lib/scripts/remote_smt --- a/src/HOL/Tools/SMT/lib/scripts/remote_smt Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/SMT/lib/scripts/remote_smt Thu Jan 06 17:51:56 2011 +0100 @@ -21,7 +21,7 @@ my $agent = LWP::UserAgent->new; $agent->agent("SMT-Request"); $agent->timeout(180); -my $response = $agent->post($ENV{"REMOTE_SMT_URL"}, [ +my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [ "Solver" => $solver, "Options" => join(" ", @options), "Problem" => [$problem_file] ], diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/SMT/smt_config.ML Thu Jan 06 17:51:56 2011 +0100 @@ -7,9 +7,14 @@ signature SMT_CONFIG = sig (*solver*) - val add_solver: string * SMT_Utils.class -> Context.generic -> - Context.generic + type solver_info = { + name: string, + class: SMT_Utils.class, + avail: unit -> bool, + options: Proof.context -> string list } + val add_solver: solver_info -> Context.generic -> Context.generic val set_solver_options: string * string -> Context.generic -> Context.generic + val available_solvers_of: Proof.context -> string list val select_solver: string -> Context.generic -> Context.generic val solver_of: Proof.context -> string val solver_class_of: Proof.context -> SMT_Utils.class @@ -52,9 +57,15 @@ (* solver *) +type solver_info = { + name: string, + class: SMT_Utils.class, + avail: unit -> bool, + options: Proof.context -> string list } + structure Solvers = Generic_Data ( - type T = (SMT_Utils.class * string list) Symtab.table * string option + type T = (solver_info * string list) Symtab.table * string option val empty = (Symtab.empty, NONE) val extend = I fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s) @@ -64,39 +75,71 @@ let val opts = String.tokens (Symbol.is_ascii_blank o str) options in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end -fun add_solver (name, class) context = +fun add_solver (info as {name, ...} : solver_info) context = if Symtab.defined (fst (Solvers.get context)) name then error ("Solver already registered: " ^ quote name) else context - |> Solvers.map (apfst (Symtab.update (name, (class, [])))) + |> Solvers.map (apfst (Symtab.update (name, (info, [])))) |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options")) (Scan.lift (Parse.$$$ "=" |-- Args.name) >> (Thm.declaration_attribute o K o set_solver_options o pair name)) ("Additional command line options for SMT solver " ^ quote name)) +fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt))) + +fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt)) + +fun is_available ctxt name = + (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of + SOME ({avail, ...}, _) => avail () + | NONE => false) + +fun available_solvers_of ctxt = + filter (is_available ctxt) (all_solvers_of ctxt) + +fun warn_solver name = + let + fun app p n = Path.append p (Path.explode n) + val path = Path.explode (getenv "ISABELLE_HOME_USER") + val path' = app (app path "etc") "components" + in + warning ("The SMT solver " ^ quote name ^ " is not installed. " ^ + "Please add the path to its component bundle to " ^ + "the components list in " ^ quote (Path.implode path') ^ ".") + end + fun select_solver name context = - if Symtab.defined (fst (Solvers.get context)) name then - Solvers.map (apsnd (K (SOME name))) context - else error ("Trying to select unknown solver: " ^ quote name) + let + val ctxt = Context.proof_of context + val upd = Solvers.map (apsnd (K (SOME name))) + in + if not (member (op =) (all_solvers_of ctxt) name) then + error ("Trying to select unknown solver: " ^ quote name) + else if not (is_available ctxt name) then (warn_solver name; upd context) + else upd context + end fun no_solver_err () = error "No SMT solver selected" fun solver_of ctxt = + (case solver_name_of ctxt of + SOME name => name + | NONE => no_solver_err ()) + +fun solver_info_of default select ctxt = (case Solvers.get (Context.Proof ctxt) of - (_, SOME name) => name - | (_, NONE) => no_solver_err ()) + (solvers, SOME name) => select (Symtab.lookup solvers name) + | (_, NONE) => default ()) fun solver_class_of ctxt = - (case Solvers.get (Context.Proof ctxt) of - (solvers, SOME name) => fst (the (Symtab.lookup solvers name)) - | (_, NONE) => no_solver_err()) + solver_info_of no_solver_err (#class o fst o the) ctxt fun solver_options_of ctxt = - (case Solvers.get (Context.Proof ctxt) of - (solvers, SOME name) => - (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => []) - | (_, NONE) => []) + let + fun all_options NONE = [] + | all_options (SOME ({options, ...}, opts)) = opts @ options ctxt + in solver_info_of (K []) all_options ctxt end val setup_solver = Attrib.setup @{binding smt_solver} @@ -224,9 +267,9 @@ let fun string_of_bool b = if b then "true" else "false" - val (names, sel) = Solvers.get (Context.Proof ctxt) |> apfst Symtab.keys + val names = available_solvers_of ctxt val ns = if null names then ["(none)"] else sort_strings names - val n = the_default "(none)" sel + val n = the_default "(none)" (solver_name_of ctxt) val opts = solver_options_of ctxt val t = string_of_real (Config.get ctxt timeout) diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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 diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Jan 06 17:51:56 2011 +0100 @@ -10,39 +10,37 @@ datatype outcome = Unsat | Sat | Unknown type solver_config = { name: string, - env_var: string, - is_remote: bool, + class: SMT_Utils.class, + avail: unit -> bool, + command: unit -> string list, options: Proof.context -> string list, - class: SMT_Utils.class, + default_max_relevant: int, + supports_filter: bool, outcome: string -> string list -> outcome * string list, cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> term list * term list) option, reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> - int list * thm) option, - default_max_relevant: int } + int list * thm) option } (*registry*) - type solver = bool option -> Proof.context -> - (int * (int option * thm)) list -> int list * thm val add_solver: solver_config -> theory -> theory val solver_name_of: Proof.context -> string - val solver_of: Proof.context -> solver val available_solvers_of: Proof.context -> string list - val is_locally_installed: Proof.context -> string -> bool - val is_remotely_available: Proof.context -> string -> bool + val apply_solver: Proof.context -> (int * (int option * thm)) list -> + int list * thm val default_max_relevant: Proof.context -> string -> int (*filter*) - type 'a smt_filter_head_result = ('a list * (int option * thm) list) * - (((int * thm) list * Proof.context) * (int * (int option * thm)) list) - val smt_filter_head: Proof.state -> - ('a * (int option * thm)) list -> int -> 'a smt_filter_head_result - val smt_filter_tail: Time.time -> bool -> 'a smt_filter_head_result -> + type 'a smt_filter_data = + ('a * thm) list * ((int * thm) list * Proof.context) + val smt_filter_preprocess: Proof.state -> + ('a * (int option * thm)) list -> int -> 'a smt_filter_data + val smt_filter_apply: Time.time -> 'a smt_filter_data -> {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list} (*tactic*) - val smt_tac': bool -> Proof.context -> thm list -> int -> Tactical.tactic val smt_tac: Proof.context -> thm list -> int -> Tactical.tactic + val smt_tac': Proof.context -> thm list -> int -> Tactical.tactic (*setup*) val setup: theory -> theory @@ -52,88 +50,43 @@ struct -(* configuration *) - -datatype outcome = Unsat | Sat | Unknown - -type solver_config = { - name: string, - env_var: string, - is_remote: bool, - options: Proof.context -> string list, - class: SMT_Utils.class, - outcome: string -> string list -> outcome * string list, - cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> - term list * term list) option, - reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> - int list * thm) option, - default_max_relevant: int } - - (* interface to external solvers *) -fun get_local_solver env_var = - let val local_solver = getenv env_var - in if local_solver <> "" then SOME local_solver else NONE end - local -fun choose (rm, env_var, is_remote, name) = - let - val force_local = (case rm of SOME false => true | _ => false) - val force_remote = (case rm of SOME true => true | _ => false) - val lsolver = get_local_solver env_var - val remote_url = getenv "REMOTE_SMT_URL" - val trace = if is_some rm then K () else tracing - in - if not force_remote andalso is_some lsolver - then - (trace ("Invoking local SMT solver " ^ quote (the lsolver) ^ " ..."); - [the lsolver]) - else if not force_local andalso is_remote - then - (trace ("Invoking remote SMT solver " ^ quote name ^ " at " ^ - quote remote_url ^ " ..."); - [getenv "REMOTE_SMT", name]) - else if force_remote - then error ("The SMT solver " ^ quote name ^ " is not remotely available.") - else error ("The SMT solver " ^ quote name ^ " has not been found " ^ - "on this computer. Please set the Isabelle environment variable " ^ - quote env_var ^ ".") - end - -fun make_cmd solver args problem_path proof_path = space_implode " " ( - map File.shell_quote (solver @ args) @ +fun make_cmd command options problem_path proof_path = space_implode " " ( + map File.shell_quote (command @ options) @ [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path]) -fun run ctxt cmd args input = +fun trace_and ctxt msg f x = + let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () + in f x end + +fun run ctxt name mk_cmd input = (case SMT_Config.certificates_of ctxt of NONE => if Config.get ctxt SMT_Config.debug_files = "" then - Cache_IO.run (make_cmd (choose cmd) args) input + trace_and ctxt ("Invoking SMT solver " ^ quote name ^ " ...") + (Cache_IO.run mk_cmd) input else let val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) val in_path = Path.ext "smt_in" base_path val out_path = Path.ext "smt_out" base_path - in - Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path - end + in Cache_IO.raw_run mk_cmd input in_path out_path end | SOME certs => (case Cache_IO.lookup certs input of (NONE, key) => if Config.get ctxt SMT_Config.fixed then error ("Bad certificates cache: missing certificate") else - Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args) input + Cache_IO.run_and_cache certs key mk_cmd input | (SOME output, _) => - (tracing ("Using cached certificate from " ^ - File.shell_path (Cache_IO.cache_path_of certs) ^ " ..."); - output))) + trace_and ctxt ("Using cached certificate from " ^ + File.shell_path (Cache_IO.cache_path_of certs) ^ " ...") + I output)) -in - -fun run_solver ctxt cmd args input = +fun run_solver ctxt name mk_cmd input = let fun pretty tag ls = Pretty.string_of (Pretty.big_list tag (map Pretty.str ls)) @@ -141,7 +94,7 @@ val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input val {redirected_output=res, output=err, return_code} = - SMT_Config.with_timeout ctxt (run ctxt cmd args) input + SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val ls = rev (snd (chop_while (equal "") (rev res))) @@ -151,8 +104,6 @@ raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in ls end -end - fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o Pretty.big_list "Assertions:" o map (Display.pretty_thm ctxt o snd)) @@ -169,65 +120,54 @@ Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () end -fun invoke name cmd options ithms ctxt = +in + +fun invoke name command ithms ctxt = let - val args = SMT_Config.solver_options_of ctxt @ options ctxt + val options = SMT_Config.solver_options_of ctxt val comments = ("solver: " ^ name) :: ("timeout: " ^ string_of_real (Config.get ctxt SMT_Config.timeout)) :: ("random seed: " ^ string_of_int (Config.get ctxt SMT_Config.random_seed)) :: - "arguments:" :: args + "arguments:" :: options val (str, recon as {context=ctxt', ...}) = ithms |> tap (trace_assms ctxt) |> SMT_Translate.translate ctxt comments ||> tap trace_recon_data - in (run_solver ctxt' cmd args str, recon) end + in (run_solver ctxt' name (make_cmd (command ()) options) str, recon) end + +end + + +(* configuration *) + +datatype outcome = Unsat | Sat | Unknown -fun trace_assumptions ctxt iwthms idxs = - let - val wthms = - idxs - |> filter (fn i => i >= 0) - |> map_filter (AList.lookup (op =) iwthms) - in - if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0 - then - tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" - (map (Display.pretty_thm ctxt o snd) wthms))) - else () - end - +type solver_config = { + name: string, + class: SMT_Utils.class, + avail: unit -> bool, + command: unit -> string list, + options: Proof.context -> string list, + default_max_relevant: int, + supports_filter: bool, + outcome: string -> string list -> outcome * string list, + cex_parser: (Proof.context -> SMT_Translate.recon -> string list -> + term list * term list) option, + reconstruct: (Proof.context -> SMT_Translate.recon -> string list -> + int list * thm) option } (* registry *) -type solver = bool option -> Proof.context -> (int * (int option * thm)) list -> - int list * thm - type solver_info = { - env_var: string, - is_remote: bool, - options: Proof.context -> string list, + command: unit -> string list, + default_max_relevant: int, + supports_filter: bool, reconstruct: Proof.context -> string list * SMT_Translate.recon -> - int list * thm, - default_max_relevant: int } - -fun gen_solver_head ctxt iwthms = SMT_Normalize.normalize iwthms ctxt - -fun gen_solver_tail (name, info : solver_info) rm (iwthms', ctxt) iwthms = - let - val {env_var, is_remote, options, reconstruct, ...} = info - val cmd = (rm, env_var, is_remote, name) - in - (iwthms', ctxt) - |-> invoke name cmd options - |> reconstruct ctxt - |> (fn (idxs, thm) => thm - |> tap (fn _ => trace_assumptions ctxt iwthms idxs) - |> pair idxs) - end + int list * thm } structure Solvers = Generic_Data ( @@ -262,18 +202,22 @@ fun add_solver cfg = let - val {name, env_var, is_remote, options, class, outcome, cex_parser, - reconstruct, default_max_relevant} = cfg + val {name, class, avail, command, options, default_max_relevant, + supports_filter, outcome, cex_parser, reconstruct} = cfg fun core_oracle () = cfalse - fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options, - reconstruct=finish (outcome name) cex_parser reconstruct ocl, - default_max_relevant=default_max_relevant } + fun solver ocl = { + command = command, + default_max_relevant = default_max_relevant, + supports_filter = supports_filter, + reconstruct = finish (outcome name) cex_parser reconstruct ocl } + + val info = {name=name, class=class, avail=avail, options=options} in Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) => Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #> - Context.theory_map (SMT_Config.add_solver (name, class)) + Context.theory_map (SMT_Config.add_solver info) end end @@ -281,26 +225,33 @@ fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) -fun name_and_solver_of ctxt = - let val name = SMT_Config.solver_of ctxt +val solver_name_of = SMT_Config.solver_of + +val available_solvers_of = SMT_Config.available_solvers_of + +fun name_and_info_of ctxt = + let val name = solver_name_of ctxt in (name, get_info ctxt name) end -val solver_name_of = fst o name_and_solver_of -fun solver_of ctxt rm ctxt' = - `(gen_solver_head ctxt') #-> gen_solver_tail (name_and_solver_of ctxt) rm - -val available_solvers_of = Symtab.keys o Solvers.get o Context.Proof +fun gen_preprocess ctxt iwthms = SMT_Normalize.normalize iwthms ctxt -fun is_locally_installed ctxt name = - let val {env_var, ...} = get_info ctxt name - in is_some (get_local_solver env_var) end +fun gen_apply (ithms, ctxt) = + let val (name, {command, reconstruct, ...}) = name_and_info_of ctxt + in + (ithms, ctxt) + |-> invoke name command + |> reconstruct ctxt + |>> distinct (op =) + end -val is_remotely_available = #is_remote oo get_info +fun apply_solver ctxt = gen_apply o gen_preprocess ctxt val default_max_relevant = #default_max_relevant oo get_info +val supports_filter = #supports_filter o snd o name_and_info_of -(* filter *) + +(* check well-sortedness *) val has_topsort = Term.exists_type (Term.exists_subtype (fn TFree (_, []) => true @@ -312,17 +263,18 @@ if exists (has_topsort o Thm.prop_of o snd o snd) iwthms then raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("proof state " ^ "contains the universal sort {}")) - else - () + else () + + +(* filter *) val cnot = Thm.cterm_of @{theory} @{const Not} fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules } -type 'a smt_filter_head_result = ('a list * (int option * thm) list) * - (((int * thm) list * Proof.context) * (int * (int option * thm)) list) +type 'a smt_filter_data = ('a * thm) list * ((int * thm) list * Proof.context) -fun smt_filter_head st xwrules i = +fun smt_filter_preprocess st xwthms i = let val ctxt = Proof.context_of st @@ -334,28 +286,27 @@ val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) - - val (xs, wthms) = split_list xwrules in - ((xs, wthms), - wthms - |> map_index I - |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) - |> tap check_topsort - |> `(gen_solver_head ctxt')) + map snd xwthms + |> map_index I + |> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts)) + |> tap check_topsort + |> gen_preprocess ctxt' + |> pair (map (apsnd snd) xwthms) end -fun smt_filter_tail time_limit run_remote - ((xs, wthms), ((iwthms', ctxt), iwthms)) = +fun smt_filter_apply time_limit (xthms, (ithms, ctxt)) = let - val ctxt = ctxt |> Config.put SMT_Config.timeout (Time.toReal time_limit) - val xrules = xs ~~ map snd wthms + val ctxt' = + ctxt + |> Config.put SMT_Config.timeout (Time.toReal time_limit) + + fun filter_thms false = K xthms + | filter_thms true = map_filter (try (nth xthms)) o fst in - ((iwthms', ctxt), iwthms) - |-> gen_solver_tail (name_and_solver_of ctxt) (SOME run_remote) - |> distinct (op =) o fst - |> map_filter (try (nth xrules)) - |> (if solver_name_of ctxt = "z3" (* FIXME *) then I else K xrules) + (ithms, ctxt') + |> gen_apply + |> filter_thms (supports_filter ctxt') |> mk_result NONE end handle SMT_Failure.SMT fail => mk_result (SOME fail) [] @@ -363,28 +314,57 @@ (* SMT tactic *) -fun smt_tac' pass_exns ctxt rules = - CONVERSION (SMT_Normalize.atomize_conv ctxt) - THEN' Tactic.rtac @{thm ccontr} - THEN' SUBPROOF (fn {context=ctxt', prems, ...} => +local + fun trace_assumptions ctxt iwthms idxs = let - val solve = snd o solver_of ctxt' NONE ctxt' o tap check_topsort - val tag = "Solver " ^ SMT_Config.solver_of ctxt' ^ ": " - val str_of = prefix tag o SMT_Failure.string_of_failure ctxt' - fun safe_solve iwthms = - if pass_exns then SOME (solve iwthms) - else (SOME (solve iwthms) - handle - SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => - (SMT_Config.verbose_msg ctxt' str_of fail; NONE) - | SMT_Failure.SMT fail => - (SMT_Config.trace_msg ctxt' str_of fail; NONE)) + val wthms = + idxs + |> filter (fn i => i >= 0) + |> map_filter (AList.lookup (op =) iwthms) in - safe_solve (map (pair ~1 o pair NONE) (rules @ prems)) - |> (fn SOME thm => Tactic.rtac thm 1 | _ => Tactical.no_tac) - end) ctxt + if Config.get ctxt SMT_Config.trace_used_facts andalso length wthms > 0 + then + tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" + (map (Display.pretty_thm ctxt o snd) wthms))) + else () + end + + fun solve ctxt iwthms = + iwthms + |> tap check_topsort + |> apply_solver ctxt + |>> trace_assumptions ctxt iwthms + |> snd + + fun str_of ctxt fail = + SMT_Failure.string_of_failure ctxt fail + |> prefix ("Solver " ^ SMT_Config.solver_of ctxt ^ ": ") -val smt_tac = smt_tac' false + fun safe_solve ctxt iwthms = SOME (solve ctxt iwthms) + handle + SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => + (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) + | SMT_Failure.SMT fail => + (SMT_Config.trace_msg ctxt (str_of ctxt) fail; NONE) + + fun tag_rules thms = map_index (apsnd (pair NONE)) thms + fun tag_prems thms = map (pair ~1 o pair NONE) thms + + fun resolve (SOME thm) = Tactic.rtac thm 1 + | resolve NONE = Tactical.no_tac + + fun tac prove ctxt rules = + CONVERSION (SMT_Normalize.atomize_conv ctxt) + THEN' Tactic.rtac @{thm ccontr} + THEN' SUBPROOF (fn {context, prems, ...} => + resolve (prove context (tag_rules rules @ tag_prems prems))) ctxt +in + +val smt_tac = tac safe_solve +val smt_tac' = tac (SOME oo solve) + +end + val smt_method = Scan.optional Attrib.thms [] >> @@ -392,7 +372,6 @@ HEADGOAL (smt_tac ctxt (thms @ facts)))) - (* setup *) val setup = diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jan 06 17:51:56 2011 +0100 @@ -42,7 +42,7 @@ subgoal: int, subgoal_count: int, facts: prover_fact list, - smt_head: (string * locality) SMT_Solver.smt_filter_head_result option} + smt_head: (string * locality) SMT_Solver.smt_filter_data option} type prover_result = {outcome: failure option, @@ -115,43 +115,26 @@ "Async_Manager". *) val das_Tool = "Sledgehammer" -val unremotify = perhaps (try (unprefix remote_prefix)) - val select_smt_solver = - Context.proof_map o SMT_Config.select_solver o unremotify + Context.proof_map o SMT_Config.select_solver fun is_smt_prover ctxt name = - let val smts = SMT_Solver.available_solvers_of ctxt in - case try (unprefix remote_prefix) name of - SOME base => member (op =) smts base andalso - SMT_Solver.is_remotely_available ctxt base - | NONE => member (op =) smts name - end + member (op =) (SMT_Solver.available_solvers_of ctxt) name fun is_prover_available ctxt name = let val thy = ProofContext.theory_of ctxt in is_smt_prover ctxt name orelse member (op =) (available_atps thy) name end -fun is_prover_installed ctxt name = - let val thy = ProofContext.theory_of ctxt in - if is_smt_prover ctxt name then - String.isPrefix remote_prefix name orelse - SMT_Solver.is_locally_installed ctxt name - else - is_atp_installed thy name - end +fun is_prover_installed ctxt = + is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt) -fun available_smt_solvers ctxt = - let val smts = SMT_Solver.available_solvers_of ctxt in - smts @ map (prefix remote_prefix) - (filter (SMT_Solver.is_remotely_available ctxt) smts) - end +fun available_smt_solvers ctxt = SMT_Solver.available_solvers_of ctxt fun default_max_relevant_for_prover ctxt name = let val thy = ProofContext.theory_of ctxt in if is_smt_prover ctxt name then - SMT_Solver.default_max_relevant ctxt (unremotify name) + SMT_Solver.default_max_relevant ctxt name else #default_max_relevant (get_atp thy name) end @@ -267,7 +250,7 @@ subgoal: int, subgoal_count: int, facts: prover_fact list, - smt_head: (string * locality) SMT_Solver.smt_filter_head_result option} + smt_head: (string * locality) SMT_Solver.smt_filter_data option} type prover_result = {outcome: failure option, @@ -537,17 +520,13 @@ state i smt_head = let val ctxt = Proof.context_of state - val (remote, base) = - case try (unprefix remote_prefix) name of - SOME base => (true, base) - | NONE => (false, name) val repair_context = - select_smt_solver base + select_smt_solver name #> Config.put SMT_Config.verbose debug #> (if overlord then Config.put SMT_Config.debug_files (overlord_file_location_for_prover name - |> (fn (path, base) => path ^ "/" ^ base)) + |> (fn (path, name) => path ^ "/" ^ name)) else I) #> Config.put SMT_Config.infer_triggers (!smt_triggers) @@ -579,9 +558,9 @@ if debug then Output.urgent_message "Invoking SMT solver..." else () val (outcome, used_facts) = (case (iter_num, smt_head) of - (1, SOME head) => head |> apsnd (apfst (apsnd repair_context)) - | _ => SMT_Solver.smt_filter_head state facts i) - |> SMT_Solver.smt_filter_tail iter_timeout remote + (1, SOME head) => head |> apsnd (apsnd repair_context) + | _ => SMT_Solver.smt_filter_preprocess state facts i) + |> SMT_Solver.smt_filter_apply iter_timeout |> (fn {outcome, used_facts} => (outcome, used_facts)) handle exn => if Exn.is_interrupt exn then reraise exn @@ -668,10 +647,8 @@ if can_apply_metis debug state subgoal (map snd used_facts) then ("metis", "") else - let val base = unremotify name in - ("smt", if base = SMT_Config.solver_of ctxt then "" - else "smt_solver = " ^ maybe_quote base) - end + ("smt", if name = SMT_Solver.solver_name_of ctxt then "" + else "smt_solver = " ^ maybe_quote name) in try_command_line (proof_banner auto) (apply_on_subgoal settings subgoal subgoal_count ^ diff -r 138f414f14cb -r 3214c39777ab src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Jan 04 15:46:38 2011 -0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 06 17:51:56 2011 +0100 @@ -255,7 +255,7 @@ val weight = SMT_Weighted_Fact oo weight_smt_fact thy fun smt_head facts = (if debug then curry (op o) SOME else try) - (SMT_Solver.smt_filter_head state (facts ())) + (SMT_Solver.smt_filter_preprocess state (facts ())) in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =)