--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Feb 09 17:18:58 2011 +0100
@@ -393,7 +393,7 @@
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
- smt_head = NONE}
+ smt_filter = NONE}
in prover params (K "") problem end)) ()
handle TimeLimit.TimeOut =>
({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Wed Feb 09 17:18:58 2011 +0100
@@ -49,7 +49,7 @@
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
- smt_head = NONE}
+ smt_filter = NONE}
in
(case prover params (K "") problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Feb 09 17:18:58 2011 +0100
@@ -237,8 +237,7 @@
{exec = ("Z3_HOME", "z3"),
required_execs = [],
arguments = fn _ => fn timeout => fn _ =>
- "MBQI=true /p /t:" ^
- string_of_int (to_secs 0 timeout),
+ "MBQI=true /p /t:" ^ string_of_int (to_secs 0 timeout),
has_incomplete_mode = false,
proof_delims = [],
known_failures =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100
@@ -67,7 +67,7 @@
val {goal, ...} = Proof.goal state
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts, smt_head = NONE}
+ facts = facts, smt_filter = NONE}
val result as {outcome, used_facts, ...} = prover params (K "") problem
in
print silent (fn () =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Feb 09 17:18:58 2011 +0100
@@ -42,7 +42,7 @@
subgoal: int,
subgoal_count: int,
facts: prover_fact list,
- smt_head: (string * locality) SMT_Solver.smt_filter_data option}
+ smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
type prover_result =
{outcome: failure option,
@@ -248,7 +248,7 @@
subgoal: int,
subgoal_count: int,
facts: prover_fact list,
- smt_head: (string * locality) SMT_Solver.smt_filter_data option}
+ smt_filter: (string * locality) SMT_Solver.smt_filter_data option}
type prover_result =
{outcome: failure option,
@@ -515,7 +515,7 @@
val smt_monomorphize_limit = Unsynchronized.ref 4
fun smt_filter_loop name ({debug, verbose, overlord, timeout, ...} : params)
- state i smt_head =
+ state i smt_filter =
let
val ctxt = Proof.context_of state
val repair_context =
@@ -555,7 +555,7 @@
val _ =
if debug then Output.urgent_message "Invoking SMT solver..." else ()
val (outcome, used_facts) =
- (case (iter_num, smt_head) of
+ (case (iter_num, smt_filter) of
(1, SOME head) => head |> apsnd (apsnd repair_context)
| _ => SMT_Solver.smt_filter_preprocess state facts i)
|> SMT_Solver.smt_filter_apply iter_timeout
@@ -625,7 +625,7 @@
#> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
- ({state, subgoal, subgoal_count, facts, smt_head, ...}
+ ({state, subgoal, subgoal_count, facts, smt_filter, ...}
: prover_problem) =
let
val ctxt = Proof.context_of state
@@ -634,7 +634,7 @@
val facts = facts ~~ (0 upto num_facts - 1)
|> map (smt_weighted_fact thy num_facts)
val {outcome, used_facts, run_time_in_msecs} =
- smt_filter_loop name params state subgoal smt_head facts
+ smt_filter_loop name params state subgoal smt_filter facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
val outcome = outcome |> Option.map failure_from_smt_failure
val message =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Feb 09 17:18:58 2011 +0100
@@ -86,7 +86,7 @@
fun launch_prover
(params as {debug, blocking, max_relevant, timeout, expect, ...})
auto minimize_command only
- {state, goal, subgoal, subgoal_count, facts, smt_head} name =
+ {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
let
val ctxt = Proof.context_of state
val birth_time = Time.now ()
@@ -99,7 +99,7 @@
val problem =
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts = take num_facts facts,
- smt_head = smt_head}
+ smt_filter = smt_filter}
fun really_go () =
problem
|> get_minimizing_prover ctxt auto name params (minimize_command name)
@@ -188,7 +188,7 @@
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
- fun launch_provers state get_facts translate maybe_smt_head provers =
+ fun launch_provers state get_facts translate maybe_smt_filter provers =
let
val facts = get_facts ()
val num_facts = length facts
@@ -197,7 +197,7 @@
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts,
- smt_head = maybe_smt_head
+ smt_filter = maybe_smt_filter
(fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
val launch = launch_prover params auto minimize_command only
in
@@ -253,13 +253,13 @@
let
val facts = get_facts "SMT solver" true smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact thy
- fun smt_head facts =
+ fun smt_filter facts =
(if debug then curry (op o) SOME else try)
(SMT_Solver.smt_filter_preprocess state (facts ()))
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)
- |> map (launch_provers state (K facts) weight smt_head o snd)
+ |> map (launch_provers state (K facts) weight smt_filter o snd)
|> exists fst |> rpair state
end
fun launch_atps_and_smt_solvers () =