author  boehmes 
Wed, 23 May 2012 16:03:38 +0200  
changeset 47965  8ba6438557bc 
parent 46497  89ccf66aa73d 
child 51717  9e7d1c139569 
permissions  rwrr 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

1 
(* Title: HOL/Tools/SMT/smt_real.ML 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

2 
Author: Sascha Boehme, TU Muenchen 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

3 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

4 
SMT setup for reals. 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

5 
*) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

6 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

7 
signature SMT_REAL = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

8 
sig 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

9 
val setup: theory > theory 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

10 
end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

11 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

12 
structure SMT_Real: SMT_REAL = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

13 
struct 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

14 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

15 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

16 
(* SMTLIB logic *) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

17 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

18 
fun smtlib_logic ts = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

19 
if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

20 
then SOME "AUFLIRA" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

21 
else NONE 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

22 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

23 

41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

24 
(* SMTLIB and Z3 builtins *) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

25 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

26 
local 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

27 
fun real_num _ i = SOME (string_of_int i ^ ".0") 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

28 

41439
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

29 
fun is_linear [t] = SMT_Utils.is_number t 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

30 
 is_linear [t, u] = SMT_Utils.is_number t orelse SMT_Utils.is_number u 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

31 
 is_linear _ = false 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

32 

41281
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

33 
fun mk_times ts = Term.list_comb (@{const times (real)}, ts) 
679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

34 

679118e35378
removed odd decoration of builtin symbols as Vars (instead provide builtin desctructor functions along with their inverse functions);
boehmes
parents:
41280
diff
changeset

35 
fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

36 
 times _ _ _ = NONE 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

37 
in 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

38 

41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

39 
val setup_builtins = 
41439
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

40 
SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

41 
(@{typ real}, K (SOME "Real"), real_num) #> 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

42 
fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [ 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

43 
(@{const less (real)}, "<"), 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

44 
(@{const less_eq (real)}, "<="), 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

45 
(@{const uminus (real)}, "~"), 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

46 
(@{const plus (real)}, "+"), 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

47 
(@{const minus (real)}, "") ] #> 
41439
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

48 
SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

49 
(Term.dest_Const @{const times (real)}, times) #> 
41439
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

50 
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

51 
(@{const times (real)}, "*") #> 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

52 
SMT_Builtin.add_builtin_fun' Z3_Interface.smtlib_z3C 
a31c451183e6
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41302
diff
changeset

53 
(@{const divide (real)}, "/") 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

54 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

55 
end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

56 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

57 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

58 
(* Z3 constructors *) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

59 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

60 
local 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

61 
fun z3_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME @{typ real} 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

62 
 z3_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME @{typ real} 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

63 
(*FIXME: delete*) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

64 
 z3_mk_builtin_typ _ = NONE 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

65 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

66 
fun z3_mk_builtin_num _ i T = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

67 
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

68 
else NONE 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

69 

47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

70 
fun mk_nary _ cu [] = cu 
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

71 
 mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) 
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

72 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
41691
diff
changeset

73 
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) 
47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

74 
val add = Thm.cterm_of @{theory} @{const plus (real)} 
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

75 
val real0 = Numeral.mk_cnumber @{ctyp real} 0 
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

76 
val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

77 
val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

78 
val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

79 
val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) 
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40516
diff
changeset

80 
val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

81 

41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

82 
fun z3_mk_builtin_fun (Z3_Interface.Sym ("", _)) [ct] = SOME (mk_uminus ct) 
47965
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

83 
 z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = 
8ba6438557bc
extend the Z3 proof parser to accept polyadic addition (on integers and reals) due to changes introduced in Z3 4.0
boehmes
parents:
46497
diff
changeset

84 
SOME (mk_nary add real0 cts) 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

85 
 z3_mk_builtin_fun (Z3_Interface.Sym ("", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

86 
SOME (mk_sub ct cu) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

87 
 z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

88 
SOME (mk_mul ct cu) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

89 
 z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

90 
SOME (mk_div ct cu) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

91 
 z3_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

92 
SOME (mk_lt ct cu) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

93 
 z3_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

94 
SOME (mk_le ct cu) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

95 
 z3_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

96 
SOME (mk_lt cu ct) 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

97 
 z3_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] = 
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41439
diff
changeset

98 
SOME (mk_le cu ct) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

99 
 z3_mk_builtin_fun _ _ = NONE 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

100 
in 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

101 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

102 
val z3_mk_builtins = { 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

103 
mk_builtin_typ = z3_mk_builtin_typ, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

104 
mk_builtin_num = z3_mk_builtin_num, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

105 
mk_builtin_fun = (fn _ => fn sym => fn cts => 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

106 
(case try (#T o Thm.rep_cterm o hd) cts of 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

107 
SOME @{typ real} => z3_mk_builtin_fun sym cts 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

108 
 _ => NONE)) } 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

109 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

110 
end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

111 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

112 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

113 
(* Z3 proof reconstruction *) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

114 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

115 
val real_rules = @{lemma 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

116 
"0 + (x::real) = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

117 
"x + 0 = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

118 
"0 * x = 0" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

119 
"1 * x = x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

120 
"x + y = y + x" 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

121 
by auto} 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

122 

38715
6513ea67d95d
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents:
36899
diff
changeset

123 
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [ 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

124 
"(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

125 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

126 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

127 
(* setup *) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

128 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

129 
val setup = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

130 
Context.theory_map ( 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

131 
SMTLIB_Interface.add_logic (10, smtlib_logic) #> 
41072
9f9bc1bdacef
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset

132 
setup_builtins #> 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

133 
Z3_Interface.add_mk_builtins z3_mk_builtins #> 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

134 
fold Z3_Proof_Reconstruction.add_z3_rule real_rules #> 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

135 
Z3_Proof_Tools.add_simproc real_linarith_proc) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

136 

bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

137 
end 