equal
deleted
inserted
replaced
|
1 (* Title: HOL/Tools/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 datatype failure = |
|
10 Counterexample of bool * term list | |
|
11 Time_Out | |
|
12 Out_Of_Memory | |
|
13 Other_Failure of string |
|
14 val string_of_failure: Proof.context -> failure -> string |
|
15 exception SMT of failure |
|
16 end |
|
17 |
|
18 structure SMT_Failure: SMT_FAILURE = |
|
19 struct |
|
20 |
|
21 datatype failure = |
|
22 Counterexample of bool * term list | |
|
23 Time_Out | |
|
24 Out_Of_Memory | |
|
25 Other_Failure of string |
|
26 |
|
27 fun string_of_failure ctxt (Counterexample (real, ex)) = |
|
28 let |
|
29 val msg = (if real then "C" else "Potential c") ^ "ounterexample found" |
|
30 in |
|
31 if null ex then msg |
|
32 else Pretty.string_of (Pretty.big_list (msg ^ ":") |
|
33 (map (Syntax.pretty_term ctxt) ex)) |
|
34 end |
|
35 | string_of_failure _ Time_Out = "Timed out" |
|
36 | string_of_failure _ Out_Of_Memory = "Ran out of memory" |
|
37 | string_of_failure _ (Other_Failure msg) = msg |
|
38 |
|
39 exception SMT of failure |
|
40 |
|
41 end |