| author | haftmann |
| Wed, 17 Nov 2010 23:20:26 +0100 | |
| changeset 40595 | 448520778e38 |
| parent 40561 | 0125cbb5d3c7 |
| child 40828 | 47ff261431c4 |
| permissions | -rw-r--r-- |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/smt_failure.ML |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
3 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
4 |
Failures and exception of SMT. |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
5 |
*) |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
6 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
7 |
signature SMT_FAILURE = |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
8 |
sig |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
9 |
datatype failure = |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
10 |
Counterexample of bool * term list | |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
11 |
Time_Out | |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
12 |
Out_Of_Memory | |
|
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
13 |
Abnormal_Termination of int | |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
14 |
Other_Failure of string |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
15 |
val string_of_failure: Proof.context -> failure -> string |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
16 |
exception SMT of failure |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
17 |
end |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
18 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
19 |
structure SMT_Failure: SMT_FAILURE = |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
20 |
struct |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
21 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
22 |
datatype failure = |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
23 |
Counterexample of bool * term list | |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
24 |
Time_Out | |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
25 |
Out_Of_Memory | |
|
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
26 |
Abnormal_Termination of int | |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
27 |
Other_Failure of string |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
28 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
29 |
fun string_of_failure ctxt (Counterexample (real, ex)) = |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
30 |
let |
|
40515
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40424
diff
changeset
|
31 |
val msg = |
|
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40424
diff
changeset
|
32 |
if real then "Counterexample found (possibly spurious)" |
|
25f266144206
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes
parents:
40424
diff
changeset
|
33 |
else "Potential counterexample found" |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
34 |
in |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
35 |
if null ex then msg |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
36 |
else Pretty.string_of (Pretty.big_list (msg ^ ":") |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
37 |
(map (Syntax.pretty_term ctxt) ex)) |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
38 |
end |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
39 |
| string_of_failure _ Time_Out = "Timed out" |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
40 |
| string_of_failure _ Out_Of_Memory = "Ran out of memory" |
|
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
41 |
| string_of_failure _ (Abnormal_Termination err) = |
|
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
42 |
"Solver terminated abnormally with error code " ^ string_of_int err |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
43 |
| string_of_failure _ (Other_Failure msg) = msg |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
44 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
45 |
exception SMT of failure |
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
46 |
|
|
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
diff
changeset
|
47 |
end |