equal
deleted
inserted
replaced
|
1 (* Title: HOL/Mirabelle/Actions/mirabelle_refute.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 structure Mirabelle_Refute : MIRABELLE_ACTION = |
|
6 struct |
|
7 |
|
8 |
|
9 (* FIXME: |
|
10 fun refute_action args timeout {pre=st, ...} = |
|
11 let |
|
12 val subgoal = 1 |
|
13 val thy = Proof.theory_of st |
|
14 val thm = #goal (Proof.raw_goal st) |
|
15 |
|
16 val refute = Refute.refute_goal thy args thm |
|
17 val _ = TimeLimit.timeLimit timeout refute subgoal |
|
18 in |
|
19 val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) |
|
20 val warn_log = Substring.full (the (Symtab.lookup tab "warning")) |
|
21 |
|
22 val r = |
|
23 if Substring.isSubstring "model found" writ_log |
|
24 then |
|
25 if Substring.isSubstring "spurious" warn_log |
|
26 then SOME "potential counterexample" |
|
27 else SOME "real counterexample (bug?)" |
|
28 else |
|
29 if Substring.isSubstring "time limit" writ_log |
|
30 then SOME "no counterexample (timeout)" |
|
31 else if Substring.isSubstring "Search terminated" writ_log |
|
32 then SOME "no counterexample (normal termination)" |
|
33 else SOME "no counterexample (unknown)" |
|
34 in r end |
|
35 *) |
|
36 |
|
37 fun invoke args = I (*Mirabelle.register ("refute", refute_action args)*) |
|
38 |
|
39 end |