1 (* Title: HOL/Library/SMT/smt_failure.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Failures and exception of SMT. |
|
5 *) |
|
6 |
|
7 signature SMT_FAILURE = |
|
8 sig |
|
9 type counterexample = { |
|
10 is_real_cex: bool, |
|
11 free_constraints: term list, |
|
12 const_defs: term list} |
|
13 datatype failure = |
|
14 Counterexample of counterexample | |
|
15 Time_Out | |
|
16 Out_Of_Memory | |
|
17 Abnormal_Termination of int | |
|
18 Other_Failure of string |
|
19 val pretty_counterexample: Proof.context -> counterexample -> Pretty.T |
|
20 val string_of_failure: Proof.context -> failure -> string |
|
21 exception SMT of failure |
|
22 end |
|
23 |
|
24 structure SMT_Failure: SMT_FAILURE = |
|
25 struct |
|
26 |
|
27 type counterexample = { |
|
28 is_real_cex: bool, |
|
29 free_constraints: term list, |
|
30 const_defs: term list} |
|
31 |
|
32 datatype failure = |
|
33 Counterexample of counterexample | |
|
34 Time_Out | |
|
35 Out_Of_Memory | |
|
36 Abnormal_Termination of int | |
|
37 Other_Failure of string |
|
38 |
|
39 fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} = |
|
40 let |
|
41 val msg = |
|
42 if is_real_cex then "Counterexample found (possibly spurious)" |
|
43 else "Potential counterexample found" |
|
44 in |
|
45 if null free_constraints andalso null const_defs then Pretty.str msg |
|
46 else |
|
47 Pretty.big_list (msg ^ ":") |
|
48 (map (Syntax.pretty_term ctxt) (free_constraints @ const_defs)) |
|
49 end |
|
50 |
|
51 fun string_of_failure ctxt (Counterexample cex) = |
|
52 Pretty.string_of (pretty_counterexample ctxt cex) |
|
53 | string_of_failure _ Time_Out = "Timed out" |
|
54 | string_of_failure _ Out_Of_Memory = "Ran out of memory" |
|
55 | string_of_failure _ (Abnormal_Termination err) = |
|
56 "Solver terminated abnormally with error code " ^ string_of_int err |
|
57 | string_of_failure _ (Other_Failure msg) = msg |
|
58 |
|
59 exception SMT of failure |
|
60 |
|
61 end |
|