--- a/src/HOL/SMT2.thy Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/SMT2.thy Thu Mar 13 13:18:13 2014 +0100
@@ -100,11 +100,11 @@
ML_file "Tools/SMT2/smt2_datatypes.ML"
ML_file "Tools/SMT2/smt2_normalize.ML"
ML_file "Tools/SMT2/smt2_translate.ML"
-ML_file "Tools/SMT2/smt2_solver.ML"
ML_file "Tools/SMT2/smtlib2.ML"
ML_file "Tools/SMT2/smtlib2_interface.ML"
+ML_file "Tools/SMT2/z3_new_proof.ML"
+ML_file "Tools/SMT2/smt2_solver.ML"
ML_file "Tools/SMT2/z3_new_interface.ML"
-ML_file "Tools/SMT2/z3_new_proof.ML"
ML_file "Tools/SMT2/z3_new_proof_tools.ML"
ML_file "Tools/SMT2/z3_new_proof_literals.ML"
ML_file "Tools/SMT2/z3_new_proof_rules.ML"
--- a/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:13 2014 +0100
@@ -19,19 +19,21 @@
outcome: string -> string list -> outcome * string list,
cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
term list * term list) option,
- replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option }
+ replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+ (int list * Z3_New_Proof.z3_step list) * thm) option }
(*registry*)
val add_solver: solver_config -> theory -> theory
val solver_name_of: Proof.context -> string
val available_solvers_of: Proof.context -> string list
val apply_solver: Proof.context -> (int * (int option * thm)) list ->
- int list * thm
+ (int list * Z3_New_Proof.z3_step list) * thm
val default_max_relevant: Proof.context -> string -> int
(*filter*)
val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int ->
- Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list}
+ Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list,
+ z3_steps: Z3_New_Proof.z3_step list}
(*tactic*)
val smt2_tac: Proof.context -> thm list -> int -> tactic
@@ -147,7 +149,8 @@
outcome: string -> string list -> outcome * string list,
cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list ->
term list * term list) option,
- replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm) option }
+ replay: (Proof.context -> SMT2_Translate.replay_data -> string list ->
+ (int list * Z3_New_Proof.z3_step list) * thm) option }
(* registry *)
@@ -156,7 +159,8 @@
command: unit -> string list,
default_max_relevant: int,
supports_filter: bool,
- replay: Proof.context -> string list * SMT2_Translate.replay_data -> int list * thm }
+ replay: Proof.context -> string list * SMT2_Translate.replay_data ->
+ (int list * Z3_New_Proof.z3_step list) * thm }
structure Solvers = Generic_Data
(
@@ -173,12 +177,12 @@
(Unsat, ls) =>
if not (Config.get ctxt SMT2_Config.oracle) andalso is_some replay
then the replay outer_ctxt replay_data ls
- else ([], ocl ())
+ else (([], []), ocl ())
| (result, ls) =>
let
val (ts, us) =
(case cex_parser of SOME f => f ctxt replay_data ls | _ => ([], []))
- in
+ in
raise SMT2_Failure.SMT (SMT2_Failure.Counterexample {
is_real_cex = (result = Sat),
free_constraints = ts,
@@ -256,8 +260,6 @@
val cnot = Thm.cterm_of @{theory} @{const Not}
-fun mk_result outcome xrules = { outcome = outcome, used_facts = xrules }
-
fun smt2_filter ctxt facts goal xwthms i time_limit =
let
val ctxt =
@@ -276,18 +278,17 @@
val xthms = map (apsnd snd) xwthms
- fun filter_thms false = K xthms
- | filter_thms true = map_filter (try (nth xthms)) o fst
+ val filter_thms = if supports_filter ctxt then K xthms else map_filter (try (nth xthms))
in
map snd xwthms
|> map_index I
|> append (map (pair ~1 o pair NONE) (Thm.assume cprop :: prems @ facts))
|> check_topsorts ctxt
|> apply_solver ctxt
- |> filter_thms (supports_filter ctxt)
- |> mk_result NONE
+ |> fst
+ |> (fn (is, z3_steps) => {outcome = NONE, used_facts = filter_thms is, z3_steps = z3_steps})
end
- handle SMT2_Failure.SMT fail => mk_result (SOME fail) []
+ handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_facts = [], z3_steps = []}
(* SMT tactic *)
@@ -311,7 +312,7 @@
iwthms
|> check_topsorts ctxt
|> apply_solver ctxt
- |>> trace_assumptions ctxt iwthms
+ |>> apfst (trace_assumptions ctxt iwthms)
|> snd
fun str_of ctxt fail =
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 13:18:13 2014 +0100
@@ -78,9 +78,9 @@
fun step_name_of id = (string_of_int id, [])
(* FIXME: find actual conjecture *)
- val id_of_last_asserted =
+ val id_of_conjecture =
proof
- |> rev |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted)
+ |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted)
|> Option.map (fn Z3_New_Proof.Z3_Step {id, ...} => id)
fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
@@ -88,7 +88,7 @@
val role =
(case rule of
Z3_New_Proof.Asserted =>
- if id_of_last_asserted = SOME id then Negated_Conjecture else Hypothesis
+ if id_of_conjecture = SOME id then Negated_Conjecture else Hypothesis
| Z3_New_Proof.Rewrite => Lemma
| Z3_New_Proof.Rewrite_Star => Lemma
| Z3_New_Proof.Skolemize => Lemma
--- a/src/HOL/Tools/SMT2/z3_new_proof_replay.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_proof_replay.ML Thu Mar 13 13:18:13 2014 +0100
@@ -7,7 +7,8 @@
signature Z3_NEW_PROOF_REPLAY =
sig
- val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> int list * thm
+ val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
+ (int list * Z3_New_Proof.z3_step list) * thm
end
structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
@@ -185,8 +186,8 @@
val proofs = fold (replay_step ctxt3 assumed) steps assumed
val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
in
- if Config.get ctxt3 SMT2_Config.filter_only_facts then (is, TrueI)
- else ([], Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
+ if Config.get ctxt3 SMT2_Config.filter_only_facts then ((is, steps), TrueI)
+ else (([], steps), Inttab.lookup proofs id |> the |> snd |> discharge rules outer_ctxt ctxt3)
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:13 2014 +0100
@@ -39,6 +39,7 @@
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Proof_Methods
+open Sledgehammer_Isar
open Sledgehammer_Prover
val smt2_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt2_builtins} (K true)
@@ -153,16 +154,19 @@
val birth = Timer.checkRealTimer timer
val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
- val (outcome, used_facts) =
+ val {outcome, used_facts, z3_steps} =
SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i 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, [])
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
+ used_facts = [], z3_steps = []}
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 timeout = Time.- (timeout, Timer.checkRealTimer timer)
val too_many_facts_perhaps =
(case outcome of
@@ -172,8 +176,6 @@
| 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
@@ -205,13 +207,14 @@
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}
+ used_from = map (apsnd snd) weighted_facts, z3_steps = z3_steps, 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, ...})
+fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress_isar,
+ try0_isar, smt_proofs, minimize, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -223,7 +226,7 @@
end
val weighted_factss = factss |> map (apsnd weight_facts)
- val {outcome, used_facts = used_pairs, used_from, run_time} =
+ val {outcome, used_facts = used_pairs, used_from, z3_steps, 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
@@ -236,13 +239,17 @@
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
+ val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_steps
+ val isar_params =
+ K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
+ minimize <> SOME false, atp_proof, goal)
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
+ proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
end,
if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
| SOME failure =>