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