| author | blanchet |
| Thu, 28 Aug 2014 00:40:38 +0200 | |
| changeset 58057 | 883f3c4c928e |
| parent 58055 | src/HOL/Library/SMT/smt_failure.ML@625bdd5c70b2 |
| permissions | -rw-r--r-- |
| 58057 | 1 |
(* Title: HOL/Library/Old_SMT/smt_failure.ML |
|
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
|
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 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
9 |
type counterexample = {
|
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
10 |
is_real_cex: bool, |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
11 |
free_constraints: term list, |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
12 |
const_defs: term list} |
|
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
|
13 |
datatype failure = |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
14 |
Counterexample of counterexample | |
|
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
|
15 |
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
|
16 |
Out_Of_Memory | |
|
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
17 |
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
|
18 |
Other_Failure of string |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
19 |
val pretty_counterexample: Proof.context -> counterexample -> Pretty.T |
|
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
|
|
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 |
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
|
25 |
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
|
26 |
|
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
27 |
type counterexample = {
|
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
28 |
is_real_cex: bool, |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
29 |
free_constraints: term list, |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
30 |
const_defs: term list} |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
31 |
|
|
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
|
32 |
datatype failure = |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
33 |
Counterexample of counterexample | |
|
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 |
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
|
35 |
Out_Of_Memory | |
|
40561
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
|
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
39 |
fun pretty_counterexample ctxt {is_real_cex, free_constraints, const_defs} =
|
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
40 |
let |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
41 |
val msg = |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
42 |
if is_real_cex then "Counterexample found (possibly spurious)" |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
43 |
else "Potential counterexample found" |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
44 |
in |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
45 |
if null free_constraints andalso null const_defs then Pretty.str msg |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
46 |
else |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
47 |
Pretty.big_list (msg ^ ":") |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
48 |
(map (Syntax.pretty_term ctxt) (free_constraints @ const_defs)) |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
49 |
end |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
50 |
|
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
51 |
fun string_of_failure ctxt (Counterexample cex) = |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40561
diff
changeset
|
52 |
Pretty.string_of (pretty_counterexample ctxt cex) |
|
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
|
53 |
| 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
|
54 |
| 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
|
55 |
| string_of_failure _ (Abnormal_Termination err) = |
|
0125cbb5d3c7
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes
parents:
40538
diff
changeset
|
56 |
"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
|
57 |
| 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
|
58 |
|
|
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
|
59 |
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
|
60 |
|
|
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
|
61 |
end |