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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
-
--- 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] ],
--- 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)
--- 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
--- 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 =
--- 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 ^
--- 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 =)