author  boehmes 
Tue, 30 Nov 2010 18:22:43 +0100  
changeset 40828  47ff261431c4 
parent 40561  0125cbb5d3c7 
permissions  rwrr 
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 
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 