--- a/src/HOL/IsaMakefile Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Nov 23 23:11:06 2010 +0100
@@ -349,9 +349,11 @@
Tools/SMT/smt_setup_solvers.ML \
Tools/SMT/smt_solver.ML \
Tools/SMT/smt_translate.ML \
+ Tools/SMT/smt_utils.ML \
Tools/SMT/z3_interface.ML \
Tools/SMT/z3_model.ML \
Tools/SMT/z3_proof_literals.ML \
+ Tools/SMT/z3_proof_methods.ML \
Tools/SMT/z3_proof_parser.ML \
Tools/SMT/z3_proof_reconstruction.ML \
Tools/SMT/z3_proof_tools.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 23 23:11:06 2010 +0100
@@ -15,9 +15,8 @@
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun metis_tag smt id =
- "#" ^ string_of_int id ^ " " ^ (if smt then "smt" else "metis") ^
- " (sledgehammer): "
+fun reconstructor_tag reconstructor id =
+ "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
val separator = "-----"
@@ -33,7 +32,7 @@
time_prover: int,
time_prover_fail: int}
-datatype me_data = MeData of {
+datatype re_data = ReData of {
calls: int,
success: int,
nontriv_calls: int,
@@ -61,15 +60,15 @@
fun make_min_data (succs, ab_ratios) =
MinData{succs=succs, ab_ratios=ab_ratios}
-fun make_me_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
+fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,
timeout,lemmas,posns) =
- MeData{calls=calls, success=success, nontriv_calls=nontriv_calls,
+ ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,
nontriv_success=nontriv_success, proofs=proofs, time=time,
timeout=timeout, lemmas=lemmas, posns=posns}
val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
val empty_min_data = make_min_data (0, 0)
-val empty_me_data = make_me_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
+val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])
fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,
lemmas, max_lems, time_isa,
@@ -78,53 +77,54 @@
fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
-fun tuple_of_me_data (MeData {calls, success, nontriv_calls, nontriv_success,
+fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,
proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
nontriv_success, proofs, time, timeout, lemmas, posns)
-datatype metis = Unminimized | Minimized | UnminimizedFT | MinimizedFT
+datatype reconstructor_mode =
+ Unminimized | Minimized | UnminimizedFT | MinimizedFT
datatype data = Data of {
sh: sh_data,
min: min_data,
- me_u: me_data, (* metis with unminimized set of lemmas *)
- me_m: me_data, (* metis with minimized set of lemmas *)
- me_uft: me_data, (* metis with unminimized set of lemmas and fully-typed *)
- me_mft: me_data, (* metis with minimized set of lemmas and fully-typed *)
+ re_u: re_data, (* reconstructor with unminimized set of lemmas *)
+ re_m: re_data, (* reconstructor with minimized set of lemmas *)
+ re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
+ re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
mini: bool (* with minimization *)
}
-fun make_data (sh, min, me_u, me_m, me_uft, me_mft, mini) =
- Data {sh=sh, min=min, me_u=me_u, me_m=me_m, me_uft=me_uft, me_mft=me_mft,
+fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =
+ Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,
mini=mini}
val empty_data = make_data (empty_sh_data, empty_min_data,
- empty_me_data, empty_me_data, empty_me_data, empty_me_data, false)
+ empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)
-fun map_sh_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
let val sh' = make_sh_data (f (tuple_of_sh_data sh))
- in make_data (sh', min, me_u, me_m, me_uft, me_mft, mini) end
+ in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end
-fun map_min_data f (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
let val min' = make_min_data (f (tuple_of_min_data min))
- in make_data (sh, min', me_u, me_m, me_uft, me_mft, mini) end
+ in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end
-fun map_me_data f m (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
let
fun map_me g Unminimized (u, m, uft, mft) = (g u, m, uft, mft)
| map_me g Minimized (u, m, uft, mft) = (u, g m, uft, mft)
| map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)
| map_me g MinimizedFT (u, m, uft, mft) = (u, m, uft, g mft)
- val f' = make_me_data o f o tuple_of_me_data
+ val f' = make_re_data o f o tuple_of_re_data
- val (me_u', me_m', me_uft', me_mft') =
- map_me f' m (me_u, me_m, me_uft, me_mft)
- in make_data (sh, min, me_u', me_m', me_uft', me_mft', mini) end
+ val (re_u', re_m', re_uft', re_mft') =
+ map_me f' m (re_u, re_m, re_uft, re_mft)
+ in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end
-fun set_mini mini (Data {sh, min, me_u, me_m, me_uft, me_mft, ...}) =
- make_data (sh, min, me_u, me_m, me_uft, me_mft, mini)
+fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =
+ make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)
fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));
@@ -170,39 +170,39 @@
fun inc_min_ab_ratios r = map_min_data
(fn (succs, ab_ratios) => (succs, ab_ratios+r))
-val inc_metis_calls = map_me_data
+val inc_reconstructor_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_metis_success = map_me_data
+val inc_reconstructor_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_metis_nontriv_calls = map_me_data
+val inc_reconstructor_nontriv_calls = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
-val inc_metis_nontriv_success = map_me_data
+val inc_reconstructor_nontriv_success = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
-val inc_metis_proofs = map_me_data
+val inc_reconstructor_proofs = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
-fun inc_metis_time m t = map_me_data
+fun inc_reconstructor_time m t = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
-val inc_metis_timeout = map_me_data
+val inc_reconstructor_timeout = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
-fun inc_metis_lemmas m n = map_me_data
+fun inc_reconstructor_lemmas m n = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
-fun inc_metis_posns m pos = map_me_data
+fun inc_reconstructor_posns m pos = map_re_data
(fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
=> (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
@@ -243,26 +243,25 @@
(if triv then "[T]" else "")
end
-fun log_me_data log tag sh_calls (metis_calls, metis_success,
- metis_nontriv_calls, metis_nontriv_success,
- metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
- metis_posns) =
- (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
- log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^
- " (proof: " ^ str metis_proofs ^ ")");
- log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
- log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
- log ("Total number of nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_calls);
- log ("Number of successful nontrivial " ^ tag ^ "metis calls: " ^ str metis_nontriv_success ^
- " (proof: " ^ str metis_proofs ^ ")");
- log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas);
- log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos);
- log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max);
- log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time));
- log ("Average time for successful " ^ tag ^ "metis calls: " ^
- str3 (avg_time metis_time metis_success));
+fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
+ re_nontriv_success, re_proofs, re_time, re_timeout,
+ (lemmas, lems_sos, lems_max), re_posns) =
+ (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
+ log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
+ " (proof: " ^ str re_proofs ^ ")");
+ log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
+ log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
+ log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
+ log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
+ " (proof: " ^ str re_proofs ^ ")");
+ log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
+ log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
+ log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
+ log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
+ log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
+ str3 (avg_time re_time re_success));
if tag=""
- then log ("Proved: " ^ space_implode " " (map str_of_pos metis_posns))
+ then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
else ()
)
@@ -273,15 +272,15 @@
in
-fun log_data id log (Data {sh, min, me_u, me_m, me_uft, me_mft, mini}) =
+fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =
let
val ShData {calls=sh_calls, ...} = sh
- fun app_if (MeData {calls, ...}) f = if calls > 0 then f () else ()
- fun log_me tag m =
- log_me_data log tag sh_calls (tuple_of_me_data m)
- fun log_metis (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
- (log_me tag1 m1; log ""; app_if m2 (fn () => log_me tag2 m2)))
+ fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
+ fun log_re tag m =
+ log_re_data log tag sh_calls (tuple_of_re_data m)
+ fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+ (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
in
if sh_calls > 0
then
@@ -289,14 +288,14 @@
log_sh_data log (tuple_of_sh_data sh);
log "";
if not mini
- then log_metis ("", me_u) ("fully-typed ", me_uft)
+ then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
else
- app_if me_u (fn () =>
- (log_metis ("unminimized ", me_u) ("unminimized fully-typed ", me_uft);
+ app_if re_u (fn () =>
+ (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
log "";
- app_if me_m (fn () =>
+ app_if re_m (fn () =>
(log_min_data log (tuple_of_min_data min); log "";
- log_metis ("", me_m) ("fully-typed ", me_mft))))))
+ log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
else ()
end
@@ -330,6 +329,10 @@
type locality = Sledgehammer_Filter.locality
+(* hack *)
+fun reconstructor_from_msg msg =
+ if String.isSubstring "metis" msg then "metis" else "smt"
+
local
datatype sh_result =
@@ -399,7 +402,7 @@
in
-fun run_sledgehammer trivial args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
val triv_str = if trivial then "[T] " else ""
val _ = change_data id inc_sh_calls
@@ -423,6 +426,7 @@
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
change_data id (inc_sh_time_prover time_prover);
+ reconstructor := reconstructor_from_msg msg;
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -437,7 +441,8 @@
end
-fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
+fun run_minimize args reconstructor named_thms id
+ ({pre=st, log, ...}: Mirabelle.run_args) =
let
val ctxt = Proof.context_of st
val n0 = length (these (!named_thms))
@@ -461,43 +466,48 @@
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
- else (named_thms := SOME named_thms';
+ else (reconstructor := reconstructor_from_msg msg;
+ named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
| (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)
end
-fun run_metis smt trivial full m name named_thms id
+fun run_reconstructor trivial full m name reconstructor named_thms id
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
- fun metis thms ctxt =
- (if smt then SMT_Solver.smt_tac
+ fun do_reconstructor thms ctxt =
+ (if !reconstructor = "smt" then SMT_Solver.smt_tac
else if full then Metis_Tactics.metisFT_tac
else Metis_Tactics.metis_tac) ctxt thms
- fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+ fun apply_reconstructor thms =
+ Mirabelle.can_apply timeout (do_reconstructor thms) st
fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
- | with_time (true, t) = (change_data id (inc_metis_success m);
- if trivial then () else change_data id (inc_metis_nontriv_success m);
- change_data id (inc_metis_lemmas m (length named_thms));
- change_data id (inc_metis_time m t);
- change_data id (inc_metis_posns m (pos, trivial));
- if name = "proof" then change_data id (inc_metis_proofs m) else ();
+ | with_time (true, t) = (change_data id (inc_reconstructor_success m);
+ if trivial then ()
+ else change_data id (inc_reconstructor_nontriv_success m);
+ change_data id (inc_reconstructor_lemmas m (length named_thms));
+ change_data id (inc_reconstructor_time m t);
+ change_data id (inc_reconstructor_posns m (pos, trivial));
+ if name = "proof" then change_data id (inc_reconstructor_proofs m)
+ else ();
"succeeded (" ^ string_of_int t ^ ")")
- fun timed_metis thms =
- (with_time (Mirabelle.cpu_time apply_metis thms), true)
- handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
+ fun timed_reconstructor thms =
+ (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)
+ handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);
("timeout", false))
| ERROR msg => ("error: " ^ msg, false)
val _ = log separator
- val _ = change_data id (inc_metis_calls m)
- val _ = if trivial then () else change_data id (inc_metis_nontriv_calls m)
+ val _ = change_data id (inc_reconstructor_calls m)
+ val _ = if trivial then ()
+ else change_data id (inc_reconstructor_nontriv_calls m)
in
maps snd named_thms
- |> timed_metis
- |>> log o prefix (metis_tag smt id)
+ |> timed_reconstructor
+ |>> log o prefix (reconstructor_tag reconstructor id)
|> snd
end
@@ -509,38 +519,46 @@
if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
then () else
let
+ val reconstructor = Unsynchronized.ref ""
val named_thms =
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val ctxt = Proof.context_of pre
val (prover_name, _) = get_prover ctxt args
- val smt = String.isSuffix "smt" prover_name (* hack *)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
- val trivial = TimeLimit.timeLimit try_outer_timeout
+ val trivial = false
+(* FIXME
+ TimeLimit.timeLimit try_outer_timeout
(Try.invoke_try (SOME try_inner_timeout)) pre
handle TimeLimit.TimeOut => false
- fun apply_metis m1 m2 =
+*)
+ fun apply_reconstructor m1 m2 =
if metis_ft
then
- if not (Mirabelle.catch_result (metis_tag smt) false
- (run_metis smt trivial false m1 name (these (!named_thms))) id st)
+ if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial false m1 name reconstructor
+ (these (!named_thms))) id st)
then
- (Mirabelle.catch_result (metis_tag smt) false
- (run_metis smt trivial true m2 name (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial true m2 name reconstructor
+ (these (!named_thms))) id st; ())
else ()
else
- (Mirabelle.catch_result (metis_tag smt) false
- (run_metis smt trivial false m1 name (these (!named_thms))) id st; ())
+ (Mirabelle.catch_result (reconstructor_tag reconstructor) false
+ (run_reconstructor trivial false m1 name reconstructor
+ (these (!named_thms))) id st; ())
in
change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer trivial args named_thms) id st;
+ Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
+ named_thms) id st;
if is_some (!named_thms)
then
- (apply_metis Unminimized UnminimizedFT;
+ (apply_reconstructor Unminimized UnminimizedFT;
if minimize andalso not (null (these (!named_thms)))
then
- (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
- apply_metis Minimized MinimizedFT)
+ (Mirabelle.catch minimize_tag
+ (run_minimize args reconstructor named_thms) id st;
+ apply_reconstructor Minimized MinimizedFT)
else ())
else ()
end
--- a/src/HOL/SMT.thy Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/SMT.thy Tue Nov 23 23:11:06 2010 +0100
@@ -10,6 +10,7 @@
"Tools/Datatype/datatype_selectors.ML"
"Tools/SMT/smt_failure.ML"
"Tools/SMT/smt_config.ML"
+ "Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_monomorph.ML"
("Tools/SMT/smt_builtin.ML")
("Tools/SMT/smt_normalize.ML")
@@ -19,6 +20,7 @@
("Tools/SMT/z3_proof_parser.ML")
("Tools/SMT/z3_proof_tools.ML")
("Tools/SMT/z3_proof_literals.ML")
+ ("Tools/SMT/z3_proof_methods.ML")
("Tools/SMT/z3_proof_reconstruction.ML")
("Tools/SMT/z3_model.ML")
("Tools/SMT/z3_interface.ML")
@@ -52,6 +54,33 @@
+subsection {* Quantifier weights *}
+
+text {*
+Weight annotations to quantifiers influence the priority of quantifier
+instantiations. They should be handled with care for solvers, which support
+them, because incorrect choices of weights might render a problem unsolvable.
+*}
+
+definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
+
+text {*
+Weights must be non-negative. The value @{text 0} is equivalent to providing
+no weight at all.
+
+Weights should only be used at quantifiers and only inside triggers (if the
+quantifier has triggers). Valid usages of weights are as follows:
+
+\begin{itemize}
+\item
+@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
+\item
+@{term "\<forall>x. weight 3 (P x)"}
+\end{itemize}
+*}
+
+
+
subsection {* Distinctness *}
text {*
@@ -137,6 +166,7 @@
use "Tools/SMT/z3_proof_parser.ML"
use "Tools/SMT/z3_proof_tools.ML"
use "Tools/SMT/z3_proof_literals.ML"
+use "Tools/SMT/z3_proof_methods.ML"
use "Tools/SMT/z3_proof_reconstruction.ML"
use "Tools/SMT/z3_model.ML"
use "Tools/SMT/smt_setup_solvers.ML"
@@ -339,7 +369,7 @@
hide_type (open) pattern
hide_const Pattern term_eq
-hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
+hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Nov 23 23:11:06 2010 +0100
@@ -26,7 +26,7 @@
type 'a proof = 'a uniform_formula step list
val strip_spaces : (char -> bool) -> string -> string
- val string_for_failure : failure -> string
+ val string_for_failure : string -> failure -> string
val extract_important_message : string -> string
val extract_known_failure :
(failure * string) list -> string -> failure option
@@ -75,13 +75,15 @@
" appears to be missing. You will need to install it if you want to run \
\ATPs remotely."
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
- | string_for_failure IncompleteUnprovable =
- "The ATP cannot prove the problem."
- | string_for_failure CantConnect = "Can't connect to remote server."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure SpassTooOld =
+fun string_for_failure prover Unprovable =
+ "The " ^ prover ^ " problem is unprovable."
+ | string_for_failure prover IncompleteUnprovable =
+ "The " ^ prover ^ " cannot prove the problem."
+ | string_for_failure _ CantConnect = "Cannot connect to remote server."
+ | string_for_failure _ TimedOut = "Timed out."
+ | string_for_failure prover OutOfResources =
+ "The " ^ prover ^ " ran out of resources."
+ | string_for_failure _ SpassTooOld =
"Isabelle requires a more recent version of SPASS with support for the \
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -90,21 +92,24 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
- | string_for_failure VampireTooOld =
+ | string_for_failure _ VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
\the instructions from the Sledgehammer manual (\"isabelle doc\
\ sledgehammer\")."
- | string_for_failure NoPerl = "Perl" ^ missing_message_tail
- | string_for_failure NoLibwwwPerl =
+ | string_for_failure _ NoPerl = "Perl" ^ missing_message_tail
+ | string_for_failure _ NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_for_failure MalformedInput =
- "The ATP problem is malformed. Please report this to the Isabelle \
+ | string_for_failure prover MalformedInput =
+ "The " ^ prover ^ " problem is malformed. Please report this to the Isabelle \
\developers."
- | string_for_failure MalformedOutput = "The ATP output is malformed."
- | string_for_failure Interrupted = "The ATP was interrupted."
- | string_for_failure Crashed = "The ATP crashed."
- | string_for_failure InternalError = "An internal ATP error occurred."
- | string_for_failure UnknownError = "An unknown ATP error occurred."
+ | string_for_failure prover MalformedOutput =
+ "The " ^ prover ^ " output is malformed."
+ | string_for_failure prover Interrupted = "The " ^ prover ^ " was interrupted."
+ | string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
+ | string_for_failure prover InternalError =
+ "An internal " ^ prover ^ " error occurred."
+ | string_for_failure prover UnknownError =
+ "An unknown " ^ prover ^ " error occurred."
fun extract_delimited (begin_delim, end_delim) output =
output |> first_field begin_delim |> the |> snd
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Nov 23 23:11:06 2010 +0100
@@ -186,7 +186,7 @@
(output, 0) => split_lines output
| (output, _) =>
error (case extract_known_failure known_perl_failures output of
- SOME failure => string_for_failure failure
+ SOME failure => string_for_failure "ATP" failure
| NONE => perhaps (try (unsuffix "\n")) output ^ ".")
fun find_system name [] systems = find_first (String.isPrefix name) systems
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Nov 23 23:11:06 2010 +0100
@@ -13,6 +13,8 @@
val trace : bool Config.T
val trace_msg : Proof.context -> (unit -> string) -> unit
+ val verbose : bool Config.T
+ val verbose_warning : Proof.context -> string -> unit
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term -> term -> bool
val replay_one_inference :
@@ -30,8 +32,11 @@
open Metis_Translate
val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
+val (verbose, verbose_setup) = Attrib.config_bool "verbose_metis" (K true)
fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
+fun verbose_warning ctxt msg =
+ if Config.get ctxt verbose then warning msg else ()
datatype term_or_type = SomeTerm of term | SomeType of typ
@@ -821,6 +826,6 @@
\Error when discharging Skolem assumptions.")
end
-val setup = trace_setup
+val setup = trace_setup #> verbose_setup
end;
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Nov 23 23:11:06 2010 +0100
@@ -10,6 +10,7 @@
signature METIS_TACTICS =
sig
val trace : bool Config.T
+ val verbose : bool Config.T
val type_lits : bool Config.T
val new_skolemizer : bool Config.T
val metis_tac : Proof.context -> thm list -> int -> tactic
@@ -103,12 +104,12 @@
if have_common_thm used cls then NONE else SOME name)
in
if not (null cls) andalso not (have_common_thm used cls) then
- warning "Metis: The assumptions are inconsistent."
+ verbose_warning ctxt "Metis: The assumptions are inconsistent"
else
();
if not (null unused) then
- warning ("Metis: Unused theorems: " ^ commas_quote unused
- ^ ".")
+ verbose_warning ctxt ("Metis: Unused theorems: " ^
+ commas_quote unused)
else
();
case result of
@@ -154,7 +155,8 @@
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
- (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
+ (verbose_warning ctxt "Metis: Proof state contains the universal sort {}";
+ Seq.empty)
else
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
--- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Nov 23 23:11:06 2010 +0100
@@ -55,6 +55,7 @@
(@{const_name SMT.pat}, K true),
(@{const_name SMT.nopat}, K true),
(@{const_name SMT.trigger}, K true),
+ (@{const_name SMT.weight}, K true),
(@{const_name SMT.fun_app}, K true),
(@{const_name SMT.z3div}, K true),
(@{const_name SMT.z3mod}, K true),
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Nov 23 23:11:06 2010 +0100
@@ -28,12 +28,11 @@
structure SMT_Normalize: SMT_NORMALIZE =
struct
+structure U = SMT_Utils
+
infix 2 ??
fun (test ?? f) x = if test x then f x else x
-fun if_conv c cv1 cv2 ct = (if c (Thm.term_of ct) then cv1 else cv2) ct
-fun if_true_conv c cv = if_conv c cv Conv.all_conv
-
(* simplification of trivial distincts (distinct should have at least
@@ -53,7 +52,7 @@
"SMT.distinct [x, y] = (x ~= y)"
by (simp_all add: distinct_def)}
fun distinct_conv _ =
- if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
+ U.if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
in
fun trivial_distinct ctxt =
map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
@@ -71,7 +70,7 @@
val thm = mk_meta_eq @{lemma
"(case P of True => x | False => y) = (if P then x else y)" by simp}
- val unfold_conv = if_true_conv is_bool_case (Conv.rewr_conv thm)
+ val unfold_conv = U.if_true_conv is_bool_case (Conv.rewr_conv thm)
in
fun rewrite_bool_cases ctxt =
map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
@@ -105,7 +104,7 @@
"Int.Bit1 (- k) = - Int.Bit1 (Int.pred k)"
by simp_all (simp add: pred_def)}
- fun pos_conv ctxt = if_conv (is_strange_number ctxt)
+ fun pos_conv ctxt = U.if_conv (is_strange_number ctxt)
(Simplifier.rewrite (Simplifier.context ctxt pos_numeral_ss))
Conv.no_conv
in
@@ -282,7 +281,7 @@
| (_, ts) => forall (is_normed ctxt) ts))
in
fun norm_binder_conv ctxt =
- if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
+ U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
end
fun norm_def ctxt thm =
@@ -321,13 +320,6 @@
(* lift lambda terms into additional rules *)
local
- val meta_eq = @{cpat "op =="}
- val meta_eqT = hd (Thm.dest_ctyp (Thm.ctyp_of_term meta_eq))
- fun inst_meta cT = Thm.instantiate_cterm ([(meta_eqT, cT)], []) meta_eq
- fun mk_meta_eq ct cu = Thm.mk_binop (inst_meta (Thm.ctyp_of_term ct)) ct cu
-
- fun cert ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
fun used_vars cvs ct =
let
val lookup = AList.lookup (op aconv) (map (` Thm.term_of) cvs)
@@ -350,7 +342,7 @@
let
val {T, ...} = Thm.rep_cterm ct' and n = Name.uu
val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
- val cu = mk_meta_eq (cert ctxt (Free (n', T))) ct'
+ val cu = U.mk_cequals (U.certify ctxt (Free (n', T))) ct'
val (eq, ctxt'') = yield_singleton Assumption.add_assumes cu ctxt'
val defs' = Termtab.update (Thm.term_of ct', eq) defs
in (apply_def cvs' eq, (ctxt'', defs')) end)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 23 23:11:06 2010 +0100
@@ -32,7 +32,7 @@
(*filter*)
val smt_filter: bool -> Time.time -> Proof.state -> ('a * thm) list -> int ->
- {outcome: SMT_Failure.failure option, used_facts: 'a list,
+ {outcome: SMT_Failure.failure option, used_facts: ('a * thm) list,
run_time_in_msecs: int option}
(*tactic*)
@@ -331,7 +331,7 @@
val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in
- split_list xrules
+ (xrules, map snd xrules)
||> distinct (op =) o fst o smt_solver rm ctxt' o append irs o map_index I
|-> map_filter o try o nth
|> (fn xs => {outcome=NONE, used_facts=xs, run_time_in_msecs=NONE})
--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Nov 23 23:11:06 2010 +0100
@@ -13,7 +13,7 @@
SVar of int |
SApp of string * sterm list |
SLet of string * sterm * sterm |
- SQua of squant * string list * sterm spattern list * sterm
+ SQua of squant * string list * sterm spattern list * int option * sterm
(* configuration options *)
type prefixes = {sort_prefix: string, func_prefix: string}
@@ -52,6 +52,9 @@
structure SMT_Translate: SMT_TRANSLATE =
struct
+structure U = SMT_Utils
+
+
(* intermediate term structure *)
datatype squant = SForall | SExists
@@ -62,7 +65,7 @@
SVar of int |
SApp of string * sterm list |
SLet of string * sterm * sterm |
- SQua of squant * string list * sterm spattern list * sterm
+ SQua of squant * string list * sterm spattern list * int option * sterm
@@ -107,13 +110,6 @@
(* utility functions *)
-val dest_funT =
- let
- fun dest Ts 0 T = (rev Ts, T)
- | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
- | dest _ _ T = raise TYPE ("dest_funT", [T], [])
- in dest [] end
-
val quantifier = (fn
@{const_name All} => SOME SForall
| @{const_name Ex} => SOME SExists
@@ -123,6 +119,10 @@
if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
| group_quant _ Ts t = (Ts, t)
+fun dest_weight (@{const SMT.weight} $ w $ t) =
+ (SOME (snd (HOLogic.dest_number w)), t)
+ | dest_weight t = (NONE, t)
+
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
| dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
| dest_pat t = raise TERM ("dest_pat", [t])
@@ -141,8 +141,9 @@
fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
let
val (Ts, u) = group_quant qn [T] t
- val (ps, b) = dest_trigger u
- in (q, rev Ts, ps, b) end)
+ val (ps, p) = dest_trigger u
+ val (w, b) = dest_weight p
+ in (q, rev Ts, ps, w, b) end)
fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
| fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
@@ -218,6 +219,9 @@
| (h as Free _, ts) => Term.list_comb (h, map in_term ts)
| _ => t)
+ and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
+ | in_weight t = in_form t
+
and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
| in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
| in_pat t = raise TERM ("in_pat", [t])
@@ -225,8 +229,8 @@
and in_pats ps =
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
- and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
- | in_trig t = in_form t
+ and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
+ | in_trig t = in_weight t
and in_form t =
(case Term.strip_comb t of
@@ -348,7 +352,7 @@
and new_dtyps dts cx =
let
fun new_decl i t =
- let val (Ts, T) = dest_funT i (Term.fastype_of t)
+ let val (Ts, T) = U.dest_funT i (Term.fastype_of t)
in
fold_map transT Ts ##>> transT T ##>>
new_fun func_prefix t NONE #>> swap
@@ -370,9 +374,9 @@
(case Term.strip_comb t of
(Const (qn, _), [Abs (_, T, t1)]) =>
(case dest_quant qn T t1 of
- SOME (q, Ts, ps, b) =>
+ SOME (q, Ts, ps, w, b) =>
fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
- trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
+ trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
| NONE => raise TERM ("intermediate", [t]))
| (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
transT T ##>> trans t1 ##>> trans t2 #>>
@@ -396,7 +400,7 @@
| _ => raise TERM ("smt_translate", [t]))
and transs t T ts =
- let val (Us, U) = dest_funT (length ts) T
+ let val (Us, U) = U.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/smt_utils.ML Tue Nov 23 23:11:06 2010 +0100
@@ -0,0 +1,140 @@
+(* Title: HOL/Tools/SMT/smt_utils.ML
+ Author: Sascha Boehme, TU Muenchen
+
+General utility functions.
+*)
+
+signature SMT_UTILS =
+sig
+ val repeat: ('a -> 'a option) -> 'a -> 'a
+ val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
+
+ (* types *)
+ val split_type: typ -> typ * typ
+ val dest_funT: int -> typ -> typ list * typ
+
+ (* terms *)
+ val dest_conj: term -> term * term
+ val dest_disj: term -> term * term
+
+ (* patterns and instantiations *)
+ val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
+ val destT1: ctyp -> ctyp
+ val destT2: ctyp -> ctyp
+ val instTs: ctyp list -> ctyp list * cterm -> cterm
+ val instT: ctyp -> ctyp * cterm -> cterm
+ val instT': cterm -> ctyp * cterm -> cterm
+
+ (* certified terms *)
+ val certify: Proof.context -> term -> cterm
+ val typ_of: cterm -> typ
+ val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
+ val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
+ val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
+ val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
+ val mk_cprop: cterm -> cterm
+ val dest_cprop: cterm -> cterm
+ val mk_cequals: cterm -> cterm -> cterm
+
+ (* conversions *)
+ val if_conv: (term -> bool) -> conv -> conv -> conv
+ val if_true_conv: (term -> bool) -> conv -> conv
+ val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val prop_conv: conv -> conv
+end
+
+structure SMT_Utils: SMT_UTILS =
+struct
+
+fun repeat f =
+ let fun rep x = (case f x of SOME y => rep y | NONE => x)
+ in rep end
+
+fun repeat_yield f =
+ let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
+ in rep end
+
+
+(* types *)
+
+fun split_type T = (Term.domain_type T, Term.range_type T)
+
+val dest_funT =
+ let
+ fun dest Ts 0 T = (rev Ts, T)
+ | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
+ | dest _ _ T = raise TYPE ("not a function type", [T], [])
+ in dest [] end
+
+
+(* terms *)
+
+fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
+ | dest_conj t = raise TERM ("not a conjunction", [t])
+
+fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u)
+ | dest_disj t = raise TERM ("not a disjunction", [t])
+
+
+(* patterns and instantiations *)
+
+fun mk_const_pat thy name destT =
+ let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
+ in (destT (Thm.ctyp_of_term cpat), cpat) end
+
+val destT1 = hd o Thm.dest_ctyp
+val destT2 = hd o tl o Thm.dest_ctyp
+
+fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
+fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
+fun instT' ct = instT (Thm.ctyp_of_term ct)
+
+
+(* certified terms *)
+
+fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+fun typ_of ct = #T (Thm.rep_cterm ct)
+
+fun dest_cabs ct ctxt =
+ (case Thm.term_of ct of
+ Abs _ =>
+ let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
+ in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
+ | _ => raise CTERM ("no abstraction", [ct]))
+
+val dest_all_cabs = repeat_yield (try o dest_cabs)
+
+fun dest_cbinder ct ctxt =
+ (case Thm.term_of ct of
+ Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt
+ | _ => raise CTERM ("not a binder", [ct]))
+
+val dest_all_cbinders = repeat_yield (try o dest_cbinder)
+
+val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
+fun dest_cprop ct =
+ (case Thm.term_of ct of
+ @{const Trueprop} $ _ => Thm.dest_arg ct
+ | _ => raise CTERM ("not a property", [ct]))
+
+val equals = mk_const_pat @{theory} @{const_name "=="} destT1
+fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
+
+
+(* conversions *)
+
+fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
+
+fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
+
+fun binders_conv cv ctxt =
+ Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt
+
+fun prop_conv cv ct =
+ (case Thm.term_of ct of
+ @{const Trueprop} $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("not a property", [ct]))
+
+end
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Nov 23 23:11:06 2010 +0100
@@ -238,7 +238,7 @@
fun sterm l (T.SVar i) = sep (var (l - i - 1))
| sterm l (T.SApp (n, ts)) = app n (sterm l) ts
| sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
- | sterm l (T.SQua (q, ss, ps, t)) =
+ | sterm l (T.SQua (q, ss, ps, w, t)) =
let
val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
val vs = map_index (apfst (Integer.add l)) ss
@@ -247,7 +247,12 @@
fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
fun pats (T.SPat ts) = pat ":pat" ts
| pats (T.SNoPat ts) = pat ":nopat" ts
- in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
+ fun weight NONE = I
+ | weight (SOME i) =
+ sep (add ":weight { " #> add (string_of_int i) #> add " }")
+ in
+ par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
+ end
fun ssort sorts = sort fast_string_ord sorts
fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
--- a/src/HOL/Tools/SMT/z3_interface.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Nov 23 23:11:06 2010 +0100
@@ -21,16 +21,13 @@
val mk_builtin_fun: Proof.context -> sym -> cterm list -> cterm option
val is_builtin_theory_term: Proof.context -> term -> bool
-
- val mk_inst_pair: (ctyp -> 'a) -> cterm -> 'a * cterm
- val destT1: ctyp -> ctyp
- val destT2: ctyp -> ctyp
- val instT': cterm -> ctyp * cterm -> cterm
end
structure Z3_Interface: Z3_INTERFACE =
struct
+structure U = SMT_Utils
+
(** Z3-specific builtins **)
@@ -163,13 +160,6 @@
| mk_builtin_num ctxt i T =
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun instT' ct = instT (Thm.ctyp_of_term ct)
-fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
val mk_false = Thm.cterm_of @{theory} @{const False}
val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
@@ -181,31 +171,34 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
-val eq = mk_inst_pair destT1 @{cpat HOL.eq}
-fun mk_eq ct cu = Thm.mk_binop (instT' ct eq) ct cu
+val eq = U.mk_const_pat @{theory} @{const_name HOL.eq} U.destT1
+fun mk_eq ct cu = Thm.mk_binop (U.instT' ct eq) ct cu
-val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
-fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (instT' ct if_term) cc) ct cu
+val if_term = U.mk_const_pat @{theory} @{const_name If} (U.destT1 o U.destT2)
+fun mk_if cc ct cu = Thm.mk_binop (Thm.capply (U.instT' ct if_term) cc) ct cu
-val nil_term = mk_inst_pair destT1 @{cpat Nil}
-val cons_term = mk_inst_pair destT1 @{cpat Cons}
+val nil_term = U.mk_const_pat @{theory} @{const_name Nil} U.destT1
+val cons_term = U.mk_const_pat @{theory} @{const_name Cons} U.destT1
fun mk_list cT cts =
- fold_rev (Thm.mk_binop (instT cT cons_term)) cts (instT cT nil_term)
+ fold_rev (Thm.mk_binop (U.instT cT cons_term)) cts (U.instT cT nil_term)
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat SMT.distinct}
+val distinct = U.mk_const_pat @{theory} @{const_name SMT.distinct}
+ (U.destT1 o U.destT1)
fun mk_distinct [] = mk_true
| mk_distinct (cts as (ct :: _)) =
- Thm.capply (instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
+ Thm.capply (U.instT' ct distinct) (mk_list (Thm.ctyp_of_term ct) cts)
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_app}
+val access = U.mk_const_pat @{theory} @{const_name fun_app}
+ (Thm.dest_ctyp o U.destT1)
fun mk_access array index =
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
- in Thm.mk_binop (instTs cTs access) array index end
+ in Thm.mk_binop (U.instTs cTs access) array index end
-val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
+val update = U.mk_const_pat @{theory} @{const_name fun_upd}
+ (Thm.dest_ctyp o U.destT1)
fun mk_update array index value =
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
- in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
+ in Thm.capply (Thm.mk_binop (U.instTs cTs update) array index) value end
val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
--- a/src/HOL/Tools/SMT/z3_model.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Tue Nov 23 23:11:06 2010 +0100
@@ -13,6 +13,9 @@
structure Z3_Model: Z3_MODEL =
struct
+structure U = SMT_Utils
+
+
(* counterexample expressions *)
datatype expr = True | False | Number of int * int option | Value of int |
@@ -214,15 +217,13 @@
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
fun mk_update ([], u) _ = u
| mk_update ([t], u) f =
- uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
+ uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
| mk_update (t :: ts, u) f =
let
- val (dT, rT) = split_type (Term.fastype_of f)
- val (dT', rT') = split_type rT
+ val (dT, rT) = U.split_type (Term.fastype_of f)
+ val (dT', rT') = U.split_type rT
in
mk_fun_upd dT rT $ f $ t $
mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Tue Nov 23 23:11:06 2010 +0100
@@ -0,0 +1,132 @@
+(* Title: HOL/Tools/SMT/z3_proof_methods.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Proof methods for Z3 proof reconstruction.
+*)
+
+signature Z3_PROOF_METHODS =
+sig
+ val prove_injectivity: Proof.context -> cterm -> thm
+end
+
+structure Z3_Proof_Methods: Z3_PROOF_METHODS =
+struct
+
+structure U = SMT_Utils
+structure T = Z3_Proof_Tools
+
+
+fun apply tac st =
+ (case Seq.pull (tac 1 st) of
+ NONE => raise THM ("tactic failed", 1, [st])
+ | SOME (st', _) => st')
+
+
+
+(* injectivity *)
+
+local
+
+val B = @{typ bool}
+fun mk_univ T = Const (@{const_name top}, T --> B)
+fun mk_inj_on T U =
+ Const (@{const_name inj_on}, (T --> U) --> (T --> B) --> B)
+fun mk_inv_into T U =
+ Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T)
+
+fun mk_inv_of ctxt ct =
+ let
+ val (dT, rT) = U.split_type (U.typ_of ct)
+ val inv = U.certify ctxt (mk_inv_into dT rT)
+ val univ = U.certify ctxt (mk_univ dT)
+ in Thm.mk_binop inv univ ct end
+
+fun mk_inj_prop ctxt ct =
+ let
+ val (dT, rT) = U.split_type (U.typ_of ct)
+ val inj = U.certify ctxt (mk_inj_on dT rT)
+ val univ = U.certify ctxt (mk_univ dT)
+ in U.mk_cprop (Thm.mk_binop inj ct univ) end
+
+
+val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
+
+fun prove_inj_prop ctxt def lhs =
+ let
+ val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
+ val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
+ in
+ Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
+ |> apply (Tactic.rtac @{thm injI})
+ |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
+ |> Goal.norm_result o Goal.finish ctxt'
+ |> singleton (Variable.export ctxt' ctxt)
+ end
+
+fun prove_rhs ctxt def lhs =
+ T.by_tac (
+ CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
+ THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
+ THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
+ Thm.elim_implies def
+
+
+fun expand thm ct =
+ let
+ val cpat = Thm.dest_arg (Thm.rhs_of thm)
+ val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
+ val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
+ val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
+ in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
+
+fun prove_lhs ctxt rhs =
+ let
+ val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
+ in
+ T.by_tac (
+ CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
+ THEN' Simplifier.simp_tac HOL_ss)
+ end
+
+
+fun mk_inv_def ctxt rhs =
+ let
+ val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
+ val (cl, cv) = Thm.dest_binop ct
+ val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
+ val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
+ in Thm.assume (U.mk_cequals cg cu) end
+
+fun prove_inj_eq ctxt ct =
+ let
+ val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
+ val lhs_thm = prove_lhs ctxt rhs lhs
+ val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
+ in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
+
+
+val swap_eq_thm = mk_meta_eq @{thm eq_commute}
+val swap_disj_thm = mk_meta_eq @{thm disj_commute}
+
+fun swap_conv dest eq =
+ U.if_true_conv ((op <) o pairself Term.size_of_term o dest)
+ (Conv.rewr_conv eq)
+
+val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
+val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm
+
+fun norm_conv ctxt =
+ swap_eq_conv then_conv
+ Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv
+ Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt)
+
+in
+
+fun prove_injectivity ctxt =
+ T.by_tac (
+ CONVERSION (U.prop_conv (norm_conv ctxt))
+ THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
+
+end
+
+end
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Nov 23 23:11:06 2010 +0100
@@ -29,6 +29,7 @@
structure Z3_Proof_Parser: Z3_PROOF_PARSER =
struct
+structure U = SMT_Utils
structure I = Z3_Interface
@@ -102,24 +103,20 @@
context-independent modulo the current proof context to be able to
use fast inference kernel rules during proof reconstruction. *)
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
val maxidx_of = #maxidx o Thm.rep_cterm
fun mk_inst ctxt vars =
let
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
- fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+ fun mk (i, v) = (v, U.certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
fun close ctxt (ct, vars) =
let
val inst = mk_inst ctxt vars
val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
- in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
+ in (U.mk_cprop (Thm.instantiate_cterm ([], inst) ct), names) end
fun mk_bound thy (i, T) =
@@ -134,10 +131,11 @@
SOME cv => cv
| _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
- in (Thm.capply (I.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
+ in (Thm.capply (U.instT' cv q) (Thm.cabs cv ct), map_filter dec vars) end
- val forall = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat All}
- val exists = I.mk_inst_pair (I.destT1 o I.destT1) @{cpat Ex}
+ fun quant name = U.mk_const_pat @{theory} name (U.destT1 o U.destT1)
+ val forall = quant @{const_name All}
+ val exists = quant @{const_name Ex}
in
fun mk_forall thy = fold_rev (mk_quant thy forall)
fun mk_exists thy = fold_rev (mk_quant thy exists)
@@ -193,7 +191,7 @@
|> Symtab.fold (Variable.declare_term o snd) terms
fun cert @{const True} = not_false
- | cert t = certify ctxt' t
+ | cert t = U.certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
@@ -208,7 +206,7 @@
SOME _ => cx
| NONE => cx |> fresh_name (decl_prefix ^ n)
|> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
- let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
+ let val upd = Symtab.update (n, U.certify ctxt (Free (m, T)))
in (typs, upd terms, exprs, steps, vars, ctxt) end))
fun mk_typ (typs, _, _, _, _, ctxt) (s as I.Sym (n, _)) =
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Nov 23 23:11:06 2010 +0100
@@ -18,6 +18,7 @@
structure P = Z3_Proof_Parser
structure T = Z3_Proof_Tools
structure L = Z3_Proof_Literals
+structure M = Z3_Proof_Methods
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
("Z3 proof reconstruction: " ^ msg))
@@ -141,7 +142,11 @@
val remove_trigger = @{lemma "trigger t p == p"
by (rule eq_reflection, rule trigger_def)}
- val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
+ val remove_weight = @{lemma "weight w p == p"
+ by (rule eq_reflection, rule weight_def)}
+
+ val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
+ L.rewrite_true]
fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
(Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
@@ -682,23 +687,29 @@
val unfold_conv =
Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
+
+ fun assume_prems ctxt thm =
+ Assumption.add_assumes (Drule.cprems_of thm) ctxt
+ |>> (fn thms => fold Thm.elim_implies thms thm)
in
-fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
- named ctxt "conj/disj/distinct" prove_conj_disj_eq,
- T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
- T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW (
- NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
- ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
- T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
- NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
- THEN_ALL_NEW (
- NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
- ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt'))))])
+fun rewrite simpset ths ct ctxt =
+ apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
+ named ctxt "conj/disj/distinct" prove_conj_disj_eq,
+ T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
+ NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+ T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
+ NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW (
+ NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+ ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
+ T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
+ NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW (
+ NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+ ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
+ named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
end
@@ -789,9 +800,8 @@
(* theory rules *)
| (P.ThLemma _, _) => (* FIXME: use arguments *)
(th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
- | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
- | (P.RewriteStar, ps) =>
- (rewrite cx simpset (map fst ps) ct, cxp)
+ | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
+ | (P.RewriteStar, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
| (P.NnfStar, _) => not_supported r
| (P.CnfStar, _) => not_supported r
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Tue Nov 23 23:11:06 2010 +0100
@@ -9,7 +9,6 @@
(* accessing and modifying terms *)
val term_of: cterm -> term
val prop_of: thm -> term
- val mk_prop: cterm -> cterm
val as_meta_eq: cterm -> cterm
(* theorem nets *)
@@ -47,6 +46,7 @@
structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
struct
+structure U = SMT_Utils
structure I = Z3_Interface
@@ -58,12 +58,7 @@
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
-val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
-
-val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
-fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
-
-fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
+fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
@@ -87,7 +82,7 @@
(* proof combinators *)
fun under_assumption f ct =
- let val ct' = mk_prop ct
+ let val ct' = U.mk_cprop ct
in Thm.implies_intr ct' (f (Thm.assume ct')) end
fun with_conv conv prove ct =
@@ -112,7 +107,7 @@
let
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
val (cf, cvs) = Drule.strip_comb lhs
- val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
+ val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
fun apply cv th =
Thm.combination th (Thm.reflexive cv)
|> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
@@ -127,9 +122,6 @@
local
-fun typ_of ct = #T (Thm.rep_cterm ct)
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
fun context_of (ctxt, _, _, _) = ctxt
@@ -155,7 +147,8 @@
| NONE =>
let
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
- val cv = certify ctxt' (Free (n, map typ_of cvs' ---> typ_of ct))
+ val cv = U.certify ctxt'
+ (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
val cu = Drule.list_comb (cv, cvs')
val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
val beta_norm' = beta_norm orelse not (null cvs')
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 22 17:49:24 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Nov 23 23:11:06 2010 +0100
@@ -403,21 +403,25 @@
important_message
else
""))
- | SOME failure => (string_for_failure failure, [])
+ | SOME failure => (string_for_failure "ATP" failure, [])
in
{outcome = outcome, message = message, used_facts = used_facts,
run_time_in_msecs = msecs}
end
-(* "SMT_Failure.Abnormal_Termination" carries the solver's return code.
- Return codes 1 to 127 are application-specific, whereas (at least on
- Unix) 128 to 255 are reserved for signals (e.g., SIGSEGV) and other
- system codes. *)
+(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
+ these are sorted out properly in the SMT module, we have to interpret these
+ ourselves. *)
+
+val z3_malformed_input_codes = [103, 110]
+val sigsegv_code = 139
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
- if code >= 128 then Crashed else IncompleteUnprovable
+ if member (op =) z3_malformed_input_codes code then MalformedInput
+ else if code = sigsegv_code then Crashed
+ else IncompleteUnprovable
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
@@ -445,8 +449,7 @@
val _ =
if verbose then
"SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^
- "..."
+ plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^ "..."
|> Output.urgent_message
else
()
@@ -472,8 +475,8 @@
| SOME (SMT_Failure.Abnormal_Termination code) =>
(if verbose then
"The SMT solver invoked with " ^ string_of_int num_facts ^
- " fact" ^ plural_s num_facts ^ " terminated abnormally with \
- \exit code " ^ string_of_int code ^ "."
+ " fact" ^ plural_s num_facts ^ " terminated abnormally with exit\
+ \code " ^ string_of_int code ^ "."
|> (if debug then error else warning)
else
();
@@ -493,35 +496,53 @@
end
in iter timeout 1 NONE (SOME 0) end
+(* taken from "Mirabelle" and generalized *)
+fun can_apply timeout tac state i =
+ let
+ val {context = ctxt, facts, goal} = Proof.goal state
+ val full_tac = Method.insert_tac facts i THEN tac ctxt i
+ in
+ case try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal of
+ SOME (SOME _) => true
+ | _ => false
+ end
+
+val smt_metis_timeout = seconds 0.5
+
+fun can_apply_metis state i ths =
+ can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths)
+ state i
+
fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
let
val repair_context =
- Config.put SMT_Config.verbose debug
+ Config.put Metis_Tactics.verbose debug
+ #> Config.put SMT_Config.verbose debug
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
val state = state |> Proof.map_context repair_context
val ctxt = Proof.context_of state
+ val thy = Proof.theory_of state
+ val smt_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
val {outcome, used_facts, run_time_in_msecs} =
- smt_filter_loop params remote state subgoal
- (map_filter (try dest_Untranslated) facts)
+ smt_filter_loop params remote state subgoal (map_filter smt_fact facts)
+ val outcome = outcome |> Option.map failure_from_smt_failure
val message =
case outcome of
NONE =>
- try_command_line (proof_banner auto)
- (apply_on_subgoal subgoal subgoal_count ^
- command_call smtN (map fst used_facts)) ^
- minimize_line minimize_command (map fst used_facts)
- | SOME SMT_Failure.Time_Out => "Timed out."
- | SOME (SMT_Failure.Abnormal_Termination code) =>
- "The SMT solver terminated abnormally with exit code " ^
- string_of_int code ^ "."
- | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
- | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
- | SOME failure =>
- SMT_Failure.string_of_failure ctxt failure
- val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)
+ let
+ val method =
+ if can_apply_metis state subgoal (map snd used_facts) then "metis"
+ else "smt"
+ in
+ try_command_line (proof_banner auto)
+ (apply_on_subgoal subgoal subgoal_count ^
+ command_call method (map (fst o fst) used_facts)) ^
+ minimize_line minimize_command (map (fst o fst) used_facts)
+ end
+ | SOME failure => string_for_failure "SMT solver" failure
in
- {outcome = outcome, used_facts = used_facts,
+ {outcome = outcome, used_facts = map fst used_facts,
run_time_in_msecs = run_time_in_msecs, message = message}
end