--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Mon Nov 15 20:48:48 2010 +0100
@@ -244,6 +244,10 @@
done
qed
+section {* Setup for String.literal *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
+
section {* Simplification rules for optimisation *}
lemma [code_pred_simp]: "\<not> False == True"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Nov 15 20:48:48 2010 +0100
@@ -350,7 +350,8 @@
#> Config.put Sledgehammer.measure_run_time true)
val params as {full_types, relevance_thresholds, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt
- [("timeout", Int.toString timeout)]
+ [("verbose", "true"),
+ ("timeout", Int.toString timeout)]
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy prover_name
val is_built_in_const =
@@ -446,7 +447,9 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
- [("provers", prover_name), ("timeout", Int.toString timeout)]
+ [("verbose", "true"),
+ ("provers", prover_name),
+ ("timeout", Int.toString timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts params 1
(Sledgehammer_Util.subgoal_count st)
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Nov 15 20:48:48 2010 +0100
@@ -14,7 +14,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- MalformedInput | MalformedOutput | Interrupted | InternalError |
+ MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
UnknownError
type step_name = string * string option
@@ -48,7 +48,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | Interrupted | InternalError | UnknownError
+ MalformedOutput | Interrupted | Crashed | InternalError | UnknownError
fun strip_spaces_in_list _ [] = []
| strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -102,6 +102,7 @@
\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."
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Nov 15 20:48:48 2010 +0100
@@ -106,11 +106,6 @@
map File.shell_quote (solver @ args) @
[File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
-fun check_return_code {output, redirected_output, return_code} =
- if return_code <> 0 then
- raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
- else (redirected_output, output)
-
fun run ctxt cmd args input =
(case C.certificates_of ctxt of
NONE => Cache_IO.run (make_cmd (choose cmd) args) input
@@ -124,7 +119,7 @@
| (SOME output, _) =>
(tracing ("Using cached certificate from " ^
File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
- output))) |> check_return_code
+ output)))
in
@@ -135,11 +130,15 @@
val _ = C.trace_msg ctxt (pretty "Problem:" o split_lines) input
- val (res, err) = C.with_timeout ctxt (run ctxt cmd args) input
+ val {redirected_output=res, output=err, return_code} =
+ C.with_timeout ctxt (run ctxt cmd args) input
val _ = C.trace_msg ctxt (pretty "Solver:") err
val ls = rev (snd (chop_while (equal "") (rev res)))
val _ = C.trace_msg ctxt (pretty "Result:") ls
+
+ val _ = null ls andalso return_code <> 0 andalso
+ raise SMT_Failure.SMT (SMT_Failure.Solver_Crashed return_code)
in ls end
end
--- a/src/HOL/Tools/SMT/z3_model.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_model.ML Mon Nov 15 20:48:48 2010 +0100
@@ -114,18 +114,30 @@
let
fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
- val ints =
- find_first (match [@{term int}]) vs
- |> Option.map (fn (_, cases) =>
- let val (cs, (_, e)) = split_last cases
- in (e, map (apfst hd) cs) end)
- fun nat_of (v as Value _) =
- (case ints of
- NONE => v
- | SOME (e, tab) => the_default e (AList.lookup (op =) tab v))
- | nat_of e = e
+ val (default_int, ints) =
+ (case find_first (match [@{term int}]) vs of
+ NONE => (NONE, [])
+ | SOME (_, cases) =>
+ let val (cs, (_, e)) = split_last cases
+ in (SOME e, map (apfst hd) cs) end)
+
+ fun nat_of @{typ nat} (v as Value _) =
+ AList.lookup (op =) ints v |> the_default (the_default v default_int)
+ | nat_of _ e = e
+
+ fun subst_nat T k ([], e) =
+ let fun app f i = if i <= 0 then I else app f (i-1) o f
+ in ([], nat_of (app Term.range_type k T) e) end
+ | subst_nat T k (arg :: args, e) =
+ subst_nat (Term.range_type T) (k-1) (args, e)
+ |> apfst (cons (nat_of (Term.domain_type T) arg))
+
+ fun subst_nats (v as ((n, k), cases)) =
+ (case Symtab.lookup terms n of
+ NONE => v
+ | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
in
- map (subst nat_of) vs
+ map subst_nats vs
|> filter_out (match [@{term int}, @{term nat}])
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 20:48:48 2010 +0100
@@ -409,59 +409,92 @@
run_time_in_msecs = msecs}
end
+(* "SMT_Failure.Solver_Crashed" is a misnomer; it should really be called
+ "Abnormal_Termination". 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. *)
+
fun failure_from_smt_failure (SMT_Failure.Counterexample _) = Unprovable
| failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
+ | failure_from_smt_failure (SMT_Failure.Solver_Crashed code) =
+ if code >= 128 then Crashed else IncompleteUnprovable
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure _ = UnknownError
-val smt_max_iter = 5
+val smt_max_iter = 8
val smt_iter_fact_divisor = 2
val smt_iter_min_msecs = 5000
val smt_iter_timeout_divisor = 2
val smt_monomorph_limit = 4
-fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
+fun smt_filter_loop ({debug, verbose, timeout, ...} : params) remote state i =
let
- val timer = Timer.startRealTimer ()
- val ms = timeout |> Time.toMilliseconds
- val iter_timeout =
- if iter < smt_max_iter then
- Int.min (ms, Int.max (smt_iter_min_msecs,
- ms div smt_iter_timeout_divisor))
- |> Time.fromMilliseconds
- else
- timeout
- val {outcome, used_facts, run_time_in_msecs} =
- TimeLimit.timeLimit iter_timeout
- (SMT_Solver.smt_filter remote iter_timeout state facts) i
- handle TimeLimit.TimeOut =>
- {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
- run_time_in_msecs = NONE}
- val outcome0 = if is_none outcome0 then SOME outcome else outcome0
- val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
- val too_many_facts_perhaps =
- case outcome of
- NONE => false
- | SOME (SMT_Failure.Counterexample _) => false
- | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
- | SOME SMT_Failure.Out_Of_Memory => true
- | SOME _ => true
- val timeout = Time.- (timeout, Timer.checkRealTimer timer)
- in
- if too_many_facts_perhaps andalso iter < smt_max_iter andalso
- not (null facts) andalso Time.> (timeout, Time.zeroTime) then
- let val facts = take (length facts div smt_iter_fact_divisor) facts in
- smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state
- facts i
+ val ctxt = Proof.context_of state
+ fun iter timeout iter_num outcome0 msecs_so_far facts =
+ let
+ val timer = Timer.startRealTimer ()
+ val ms = timeout |> Time.toMilliseconds
+ val iter_timeout =
+ if iter_num < smt_max_iter then
+ Int.min (ms, Int.max (smt_iter_min_msecs,
+ ms div smt_iter_timeout_divisor))
+ |> Time.fromMilliseconds
+ else
+ timeout
+ val num_facts = length facts
+ val _ =
+ if verbose then
+ "SMT iteration with " ^ string_of_int num_facts ^ " fact" ^
+ plural_s num_facts ^ " for " ^ string_from_time iter_timeout ^
+ "..."
+ |> Output.urgent_message
+ else
+ ()
+ val {outcome, used_facts, run_time_in_msecs} =
+ TimeLimit.timeLimit iter_timeout
+ (SMT_Solver.smt_filter remote iter_timeout state facts) i
+ handle TimeLimit.TimeOut =>
+ {outcome = SOME SMT_Failure.Time_Out, used_facts = [],
+ run_time_in_msecs = NONE}
+ val _ =
+ if verbose andalso is_some outcome then
+ "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
+ |> Output.urgent_message
+ else
+ ()
+ val outcome0 = if is_none outcome0 then SOME outcome else outcome0
+ val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
+ val too_many_facts_perhaps =
+ case outcome of
+ NONE => false
+ | SOME (SMT_Failure.Counterexample _) => false
+ | SOME SMT_Failure.Time_Out => iter_timeout <> timeout
+ | SOME (SMT_Failure.Solver_Crashed 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 ^ "."
+ |> (if debug then error else warning)
+ else
+ ();
+ true (* kind of *))
+ | SOME SMT_Failure.Out_Of_Memory => true
+ | SOME _ => true
+ val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+ in
+ if too_many_facts_perhaps andalso iter_num < smt_max_iter andalso
+ num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
+ let val facts = take (num_facts div smt_iter_fact_divisor) facts in
+ iter timeout (iter_num + 1) outcome0 msecs_so_far facts
+ end
+ else
+ {outcome = if is_none outcome then NONE else the outcome0,
+ used_facts = used_facts, run_time_in_msecs = msecs_so_far}
end
- else
- {outcome = if is_none outcome then NONE else the outcome0,
- used_facts = used_facts, run_time_in_msecs = msecs_so_far}
- end
+ in iter timeout 1 NONE (SOME 0) end
-fun run_smt_solver auto remote ({debug, timeout, ...} : params) minimize_command
- ({state, subgoal, subgoal_count, facts, ...}
- : prover_problem) =
+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
@@ -469,8 +502,8 @@
val state = state |> Proof.map_context repair_context
val ctxt = Proof.context_of state
val {outcome, used_facts, run_time_in_msecs} =
- smt_filter_loop 1 NONE (SOME 0) remote timeout state
- (map_filter (try dest_Untranslated) facts) subgoal
+ smt_filter_loop params remote state subgoal
+ (map_filter (try dest_Untranslated) facts)
val message =
case outcome of
NONE =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Nov 15 17:40:38 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Nov 15 20:48:48 2010 +0100
@@ -27,10 +27,10 @@
(* wrapper for calling external prover *)
-fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure Interrupted = "Interrupted."
- | string_for_failure _ = "Unknown error."
+fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
+ | string_for_failure ATP_Proof.TimedOut = "Timed out."
+ | string_for_failure ATP_Proof.Interrupted = "Interrupted."
+ | string_for_failure _ = "Error."
fun n_facts names =
let val n = length names in