--- a/src/HOL/Sledgehammer.thy Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Mar 13 13:18:13 2014 +0100
@@ -27,6 +27,7 @@
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_atp.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_smt.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_prover_smt2.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 13 13:18:13 2014 +0100
@@ -29,7 +29,7 @@
(* val cvc3N = "cvc3" *)
val yicesN = "yices"
-val z3N = "z3"
+val z3_newN = "z3_new"
val runN = "run"
val minN = "min"
@@ -195,14 +195,6 @@
fun merge data : T = AList.merge (op =) (K true) data
)
-fun is_prover_supported ctxt =
- let val thy = Proof_Context.theory_of ctxt in
- is_proof_method orf is_atp thy orf is_smt_prover ctxt
- end
-
-fun is_prover_installed ctxt =
- is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
-
fun remotify_prover_if_supported_and_not_already_remote ctxt name =
if String.isPrefix remote_prefix name then
SOME name
@@ -220,7 +212,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put E first. *)
fun default_provers_param_value mode ctxt =
- [eN, spassN, z3N, e_sineN, vampireN, yicesN]
+ [eN, spassN, z3_newN, e_sineN, vampireN, yicesN]
|> map_filter (remotify_prover_if_not_installed ctxt)
(* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
|> take (Multithreading.max_threads_value () - (if mode = Try then 1 else 0))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 13 13:18:13 2014 +0100
@@ -134,7 +134,7 @@
fun massage_methods (meths as meth :: _) =
if not try0_isar then [meth]
- else if smt_proofs = SOME true then SMT_Method :: meths
+ else if smt_proofs = SOME true then SMT2_Method :: meths
else meths
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
@@ -368,7 +368,7 @@
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
(case play of
- Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
+ Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true
| Play_Timed_Out _ => true
| Play_Failed => true
| Not_Played => false)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Thu Mar 13 13:18:13 2014 +0100
@@ -259,7 +259,7 @@
fun is_direct_method (Metis_Method _) = true
| is_direct_method Meson_Method = true
- | is_direct_method SMT_Method = true
+ | is_direct_method SMT2_Method = true
| is_direct_method _ = false
(* Local facts are always passed via "using", which affects "meson" and "metis". This is
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu Mar 13 13:18:13 2014 +0100
@@ -12,7 +12,7 @@
datatype proof_method =
Metis_Method of string option * string option |
Meson_Method |
- SMT_Method |
+ SMT2_Method |
Blast_Method |
Simp_Method |
Simp_Size_Method |
@@ -51,7 +51,7 @@
datatype proof_method =
Metis_Method of string option * string option |
Meson_Method |
- SMT_Method |
+ SMT2_Method |
Blast_Method |
Simp_Method |
Simp_Size_Method |
@@ -78,7 +78,7 @@
| Metis_Method (type_enc_opt, lam_trans_opt) =>
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
| Meson_Method => "meson"
- | SMT_Method => "smt"
+ | SMT2_Method => "smt2"
| Blast_Method => "blast"
| Simp_Method => "simp"
| Simp_Size_Method => "simp add: size_ne_size_imp_ne"
@@ -93,7 +93,7 @@
exceeded" warnings and the like. *)
fun silence_proof_methods debug =
Try0.silence_methods debug
- #> Config.put SMT_Config.verbose debug
+ #> Config.put SMT2_Config.verbose debug
fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth =
let val ctxt = silence_proof_methods debug ctxt0 in
@@ -103,8 +103,7 @@
Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
(lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
| Meson_Method => Meson.meson_tac ctxt global_facts
-
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts
| _ =>
Method.insert_tac global_facts THEN'
(case meth of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Mar 13 13:18:13 2014 +0100
@@ -184,7 +184,7 @@
Metis_Method (SOME full_typesN, NONE),
Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
- (if smt_proofs then [SMT_Method] else [])
+ (if smt_proofs then [SMT2_Method] else [])
fun extract_proof_method ({type_enc, lam_trans, ...} : params)
(Metis_Method (type_enc', lam_trans')) =
@@ -195,7 +195,7 @@
(if is_none lam_trans' andalso is_none lam_trans then []
else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
in (metisN, override_params) end
- | extract_proof_method _ SMT_Method = (smtN, [])
+ | extract_proof_method _ SMT2_Method = (smtN, [])
(* based on "Mirabelle.can_apply" and generalized *)
fun timed_apply timeout tac state i =
@@ -279,7 +279,8 @@
val (remote_provers, local_provers) =
proof_method_names @
sort_strings (supported_atps thy) @
- sort_strings (SMT_Solver.available_solvers_of ctxt)
+ sort_strings (SMT_Solver.available_solvers_of ctxt) @
+ sort_strings (SMT2_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
Output.urgent_message ("Supported provers: " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu Mar 13 13:18:13 2014 +0100
@@ -49,6 +49,7 @@
open Sledgehammer_Prover
open Sledgehammer_Prover_ATP
open Sledgehammer_Prover_SMT
+open Sledgehammer_Prover_SMT2
fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
minimize_command
@@ -56,7 +57,7 @@
let
val meth =
if name = metisN then Metis_Method (type_enc, lam_trans)
- else if name = smtN then SMT_Method
+ else if name = smtN then SMT2_Method
else raise Fail ("unknown proof_method: " ^ quote name)
val used_facts = facts |> map fst
in
@@ -89,11 +90,12 @@
fun is_prover_supported ctxt =
let val thy = Proof_Context.theory_of ctxt in
- is_proof_method orf is_atp thy orf is_smt_prover ctxt
+ is_proof_method orf is_atp thy orf is_smt_prover ctxt orf is_smt2_prover ctxt
end
fun is_prover_installed ctxt =
- is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+ is_proof_method orf is_smt_prover ctxt orf is_smt2_prover ctxt orf
+ is_atp_installed (Proof_Context.theory_of ctxt)
val proof_method_default_max_facts = 20
@@ -103,8 +105,12 @@
proof_method_default_max_facts
else if is_atp thy name then
fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
- else (* is_smt_prover ctxt name *)
+ else if is_smt_prover ctxt name then
SMT_Solver.default_max_relevant ctxt name
+ else if is_smt2_prover ctxt name then
+ SMT2_Solver.default_max_relevant ctxt name
+ else
+ error ("No such prover: " ^ name ^ ".")
end
fun get_prover ctxt mode name =
@@ -112,6 +118,7 @@
if is_proof_method name then run_proof_method mode name
else if is_atp thy name then run_atp mode name
else if is_smt_prover ctxt name then run_smt_solver mode name
+ else if is_smt2_prover ctxt name then run_smt2_solver mode name
else error ("No such prover: " ^ name ^ ".")
end
@@ -344,7 +351,7 @@
adjust_proof_method_params override_params params))
else
(prover_fast_enough (), (name, params))
- | (SMT_Method, Played timeout) =>
+ | (SMT2_Method, Played timeout) =>
(* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
itself. *)
(can_min_fast_enough timeout, (name, params))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 13 13:18:13 2014 +0100
@@ -234,7 +234,7 @@
NONE =>
(Lazy.lazy (fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:13 2014 +0100
@@ -0,0 +1,257 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+SMT solvers as Sledgehammer provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_SMT2 =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type mode = Sledgehammer_Prover.mode
+ type prover = Sledgehammer_Prover.prover
+
+ val smt2_builtins : bool Config.T
+ val smt2_triggers : bool Config.T
+ val smt2_weights : bool Config.T
+ val smt2_weight_min_facts : int Config.T
+ val smt2_min_weight : int Config.T
+ val smt2_max_weight : int Config.T
+ val smt2_max_weight_index : int Config.T
+ val smt2_weight_curve : (int -> int) Unsynchronized.ref
+ val smt2_max_slices : int Config.T
+ val smt2_slice_fact_frac : real Config.T
+ val smt2_slice_time_frac : real Config.T
+ val smt2_slice_min_secs : int Config.T
+
+ val is_smt2_prover : Proof.context -> string -> bool
+ val run_smt2_solver : mode -> string -> prover
+end;
+
+structure Sledgehammer_Prover_SMT2 : SLEDGEHAMMER_PROVER_SMT2 =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Systems
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Proof_Methods
+open Sledgehammer_Prover
+
+val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
+val smt2_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt2_triggers} (K true)
+val smt2_weights = Attrib.setup_config_bool @{binding sledgehammer_smt2_weights} (K true)
+val smt2_weight_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_smt2_weight_min_facts} (K 20)
+
+fun is_smt2_prover ctxt = member (op =) (SMT2_Solver.available_solvers_of ctxt)
+
+(* FUDGE *)
+val smt2_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_min_weight} (K 0)
+val smt2_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight} (K 10)
+val smt2_max_weight_index =
+ Attrib.setup_config_int @{binding sledgehammer_smt2_max_weight_index} (K 200)
+val smt2_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt2_fact_weight ctxt j num_facts =
+ if Config.get ctxt smt2_weights andalso num_facts >= Config.get ctxt smt2_weight_min_facts then
+ let
+ val min = Config.get ctxt smt2_min_weight
+ val max = Config.get ctxt smt2_max_weight
+ val max_index = Config.get ctxt smt2_max_weight_index
+ val curve = !smt2_weight_curve
+ in
+ SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
+ end
+ else
+ NONE
+
+fun weight_smt2_fact ctxt num_facts ((info, th), j) =
+ let val thy = Proof_Context.theory_of ctxt in
+ (info, (smt2_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
+ end
+
+(* "SMT2_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
+ properly in the SMT module, we must interpret these here. *)
+val z3_failures =
+ [(101, OutOfResources),
+ (103, MalformedInput),
+ (110, MalformedInput),
+ (112, TimedOut)]
+val unix_failures =
+ [(138, Crashed),
+ (139, Crashed)]
+val smt2_failures = z3_failures @ unix_failures
+
+fun failure_of_smt2_failure (SMT2_Failure.Counterexample {is_real_cex, ...}) =
+ if is_real_cex then Unprovable else GaveUp
+ | failure_of_smt2_failure SMT2_Failure.Time_Out = TimedOut
+ | failure_of_smt2_failure (SMT2_Failure.Abnormal_Termination code) =
+ (case AList.lookup (op =) smt2_failures code of
+ SOME failure => failure
+ | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code ^ "."))
+ | failure_of_smt2_failure SMT2_Failure.Out_Of_Memory = OutOfResources
+ | failure_of_smt2_failure (SMT2_Failure.Other_Failure s) = UnknownError s
+
+(* FUDGE *)
+val smt2_max_slices = Attrib.setup_config_int @{binding sledgehammer_smt2_max_slices} (K 8)
+val smt2_slice_fact_frac =
+ Attrib.setup_config_real @{binding sledgehammer_smt2_slice_fact_frac} (K 0.667)
+val smt2_slice_time_frac =
+ Attrib.setup_config_real @{binding sledgehammer_smt2_slice_time_frac} (K 0.333)
+val smt2_slice_min_secs = Attrib.setup_config_int @{binding sledgehammer_smt2_slice_min_secs} (K 3)
+
+val is_boring_builtin_typ =
+ not o exists_subtype (member (op =) [@{typ nat}, @{typ int}, HOLogic.realT])
+
+fun smt2_filter_loop name ({debug, overlord, max_mono_iters, max_new_mono_instances, timeout, slice,
+ ...} : params) state goal i =
+ let
+ fun repair_context ctxt =
+ ctxt |> Context.proof_map (SMT2_Config.select_solver name)
+ |> Config.put SMT2_Config.verbose debug
+ |> (if overlord then
+ Config.put SMT2_Config.debug_files
+ (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name))
+ else
+ I)
+ |> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
+ |> not (Config.get ctxt smt2_builtins)
+ ? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
+ #> Config.put SMT2_Setup_Solvers.z3_extensions false)
+ |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
+ default_max_new_mono_instances
+
+ val state = Proof.map_context (repair_context) state
+ val ctxt = Proof.context_of state
+ val max_slices = if slice then Config.get ctxt smt2_max_slices else 1
+
+ fun do_slice timeout slice outcome0 time_so_far
+ (weighted_factss as (fact_filter, weighted_facts) :: _) =
+ let
+ val timer = Timer.startRealTimer ()
+ val slice_timeout =
+ if slice < max_slices then
+ let val ms = Time.toMilliseconds timeout in
+ Int.min (ms, Int.max (1000 * Config.get ctxt smt2_slice_min_secs,
+ Real.ceil (Config.get ctxt smt2_slice_time_frac * Real.fromInt ms)))
+ |> Time.fromMilliseconds
+ end
+ else
+ timeout
+ val num_facts = length weighted_facts
+ val _ =
+ if debug then
+ quote name ^ " slice " ^ string_of_int slice ^ " with " ^ string_of_int num_facts ^
+ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time slice_timeout
+ |> Output.urgent_message
+ else
+ ()
+ val birth = Timer.checkRealTimer timer
+ val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
+
+ val (outcome, used_facts) =
+ SMT2_Solver.smt2_filter_preprocess ctxt [] goal weighted_facts i
+ |> SMT2_Solver.smt2_filter_apply slice_timeout
+ |> (fn {outcome, used_facts} => (outcome, used_facts))
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else (ML_Compiler.exn_message exn |> SMT2_Failure.Other_Failure |> SOME, [])
+
+ val death = Timer.checkRealTimer timer
+ val outcome0 = if is_none outcome0 then SOME outcome else outcome0
+ val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
+
+ val too_many_facts_perhaps =
+ (case outcome of
+ NONE => false
+ | SOME (SMT2_Failure.Counterexample _) => false
+ | SOME SMT2_Failure.Time_Out => slice_timeout <> timeout
+ | SOME (SMT2_Failure.Abnormal_Termination _) => true (* kind of *)
+ | SOME SMT2_Failure.Out_Of_Memory => true
+ | SOME (SMT2_Failure.Other_Failure _) => true)
+
+ val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if too_many_facts_perhaps andalso slice < max_slices andalso num_facts > 0 andalso
+ Time.> (timeout, Time.zeroTime) then
+ let
+ val new_num_facts =
+ Real.ceil (Config.get ctxt smt2_slice_fact_frac * Real.fromInt num_facts)
+ val weighted_factss as (new_fact_filter, _) :: _ =
+ weighted_factss
+ |> (fn (x :: xs) => xs @ [x])
+ |> app_hd (apsnd (take new_num_facts))
+ val show_filter = fact_filter <> new_fact_filter
+
+ fun num_of_facts fact_filter num_facts =
+ string_of_int num_facts ^ (if show_filter then " " ^ quote fact_filter else "") ^
+ " fact" ^ plural_s num_facts
+
+ val _ =
+ if debug then
+ quote name ^ " invoked with " ^
+ num_of_facts fact_filter num_facts ^ ": " ^
+ string_of_atp_failure (failure_of_smt2_failure (the outcome)) ^
+ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
+ "..."
+ |> Output.urgent_message
+ else
+ ()
+ in
+ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
+ end
+ else
+ {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts,
+ used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
+ end
+ in
+ do_slice timeout 1 NONE Time.zeroTime
+ end
+
+fun run_smt2_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
+ minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
+ let
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
+
+ fun weight_facts facts =
+ let val num_facts = length facts in
+ map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1))
+ end
+
+ val weighted_factss = factss |> map (apsnd weight_facts)
+ val {outcome, used_facts = used_pairs, used_from, run_time} =
+ smt2_filter_loop name params state goal subgoal weighted_factss
+ val used_facts = used_pairs |> map fst
+ val outcome = outcome |> Option.map failure_of_smt2_failure
+
+ val (preplay, message, message_tail) =
+ (case outcome of
+ NONE =>
+ (Lazy.lazy (fn () =>
+ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+ SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ fn preplay =>
+ let
+ val one_line_params =
+ (preplay, proof_banner mode name, used_facts,
+ choose_minimize_command thy params minimize_command name preplay, subgoal,
+ subgoal_count)
+ val num_chained = length (#facts (Proof.goal state))
+ in
+ one_line_proof_text num_chained one_line_params
+ end,
+ if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
+ | SOME failure =>
+ (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+ fn _ => string_of_atp_failure failure, ""))
+ in
+ {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
+ end
+
+end;