| author | boehmes |
| Fri, 12 Nov 2010 17:28:43 +0100 | |
| changeset 40538 | b8482ff0bc92 |
| parent 40515 | 25f266144206 |
| child 40561 | 0125cbb5d3c7 |
| 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 | |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
13 |
Solver_Crashed 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 | |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
26 |
Solver_Crashed 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" |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
41 |
| string_of_failure _ (Solver_Crashed err) = |
|
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40515
diff
changeset
|
42 |
"Solver crashed 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 |