author | blanchet |
Wed, 28 Oct 2009 17:43:43 +0100 | |
changeset 33552 | ab01b72715ef |
child 33600 | 16a263d2b1c9 |
permissions | -rw-r--r-- |
blanchet@33552 | 1 |
(* Title: Tools/auto_counterexample.ML |
blanchet@33552 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
blanchet@33552 | 3 |
|
blanchet@33552 | 4 |
Counterexample Search Unit (do not abbreviate!). |
blanchet@33552 | 5 |
*) |
blanchet@33552 | 6 |
|
blanchet@33552 | 7 |
signature AUTO_COUNTEREXAMPLE = |
blanchet@33552 | 8 |
sig |
blanchet@33552 | 9 |
val time_limit: int Unsynchronized.ref |
blanchet@33552 | 10 |
|
blanchet@33552 | 11 |
val register_tool : |
blanchet@33552 | 12 |
string * (Proof.state -> bool * Proof.state) -> theory -> theory |
blanchet@33552 | 13 |
end; |
blanchet@33552 | 14 |
|
blanchet@33552 | 15 |
structure Auto_Counterexample : AUTO_COUNTEREXAMPLE = |
blanchet@33552 | 16 |
struct |
blanchet@33552 | 17 |
|
blanchet@33552 | 18 |
(* preferences *) |
blanchet@33552 | 19 |
|
blanchet@33552 | 20 |
val time_limit = Unsynchronized.ref 2500 |
blanchet@33552 | 21 |
|
blanchet@33552 | 22 |
val _ = |
blanchet@33552 | 23 |
ProofGeneralPgip.add_preference Preferences.category_tracing |
blanchet@33552 | 24 |
(Preferences.nat_pref time_limit |
blanchet@33552 | 25 |
"auto-counterexample-time-limit" |
blanchet@33552 | 26 |
"Time limit for automatic counterexample search (in milliseconds).") |
blanchet@33552 | 27 |
|
blanchet@33552 | 28 |
|
blanchet@33552 | 29 |
(* configuration *) |
blanchet@33552 | 30 |
|
blanchet@33552 | 31 |
structure Data = TheoryDataFun( |
blanchet@33552 | 32 |
type T = (string * (Proof.state -> bool * Proof.state)) list |
blanchet@33552 | 33 |
val empty = [] |
blanchet@33552 | 34 |
val copy = I |
blanchet@33552 | 35 |
val extend = I |
blanchet@33552 | 36 |
fun merge _ (tools1, tools2) = AList.merge (op =) (K true) (tools1, tools2) |
blanchet@33552 | 37 |
) |
blanchet@33552 | 38 |
|
blanchet@33552 | 39 |
val register_tool = Data.map o AList.update (op =) |
blanchet@33552 | 40 |
|
blanchet@33552 | 41 |
|
blanchet@33552 | 42 |
(* automatic testing *) |
blanchet@33552 | 43 |
|
blanchet@33552 | 44 |
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => |
blanchet@33552 | 45 |
case !time_limit of |
blanchet@33552 | 46 |
0 => state |
blanchet@33552 | 47 |
| ms => |
blanchet@33552 | 48 |
TimeLimit.timeLimit (Time.fromMilliseconds ms) |
blanchet@33552 | 49 |
(fn () => |
blanchet@33552 | 50 |
if interact andalso not (!Toplevel.quiet) then |
blanchet@33552 | 51 |
fold_rev (fn (_, tool) => fn (true, state) => (true, state) |
blanchet@33552 | 52 |
| (false, state) => tool state) |
blanchet@33552 | 53 |
(Data.get (Proof.theory_of state)) (false, state) |> snd |
blanchet@33552 | 54 |
else |
blanchet@33552 | 55 |
state) () |
blanchet@33552 | 56 |
handle TimeLimit.TimeOut => |
blanchet@33552 | 57 |
(warning "Automatic counterexample search timed out."; state))) |
blanchet@33552 | 58 |
|
blanchet@33552 | 59 |
end; |