# HG changeset patch # User blanchet # Date 1394713093 -3600 # Node ID 72fad75baf7e3e643d76bbaff7b7aff56a15da7c # Parent f8ed378ec45705170cbdba76dd894132151660ed integrate SMT2 with Sledgehammer diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Sledgehammer.thy --- 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" diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_commands.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)) diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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) diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- 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 diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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: " ^ diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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)) diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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 = diff -r f8ed378ec457 -r 72fad75baf7e src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- /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;