author  boehmes 
Sun, 19 Dec 2010 17:55:56 +0100  
changeset 41280  a7de9d36f4f2 
parent 41072  9f9bc1bdacef 
child 41281  679118e35378 
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 

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

15 
structure U = SMT_Utils 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

16 
structure B = SMT_Builtin 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

17 

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

18 

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

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

20 

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

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

22 
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

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

24 
else NONE 
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 

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

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

28 

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

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

30 
val smtlibC = SMTLIB_Interface.smtlibC 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

31 

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

32 
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

33 

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

34 
fun is_linear [t] = U.is_number t 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

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

36 
 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

37 

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

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

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

40 

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

41 
fun divide _ T (ts as [_, t]) = 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

42 
if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

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

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

45 

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

46 
val setup_builtins = 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

47 
B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #> 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40579
diff
changeset

48 
fold (B.add_builtin_fun' 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 
(@{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

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

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

52 
(@{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

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

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

55 
(Term.dest_Const @{const times (real)}, times) #> 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

56 
B.add_builtin_fun Z3_Interface.smtlib_z3C 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41072
diff
changeset

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

58 

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

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

60 

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

61 

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

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

63 

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

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

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

66 

40516  67 
fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real} 
68 
 z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*) 

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

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

70 

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

71 
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

72 
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

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

74 

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

75 
val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (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

76 
val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (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_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

78 
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

79 
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

80 
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

81 
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

82 

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

83 
fun z3_mk_builtin_fun (I.Sym ("", _)) [ct] = SOME (mk_uminus ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

84 
 z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

85 
 z3_mk_builtin_fun (I.Sym ("", _)) [ct, cu] = SOME (mk_sub ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

86 
 z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

87 
 z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

88 
 z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

89 
 z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

90 
 z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

91 
 z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
diff
changeset

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

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

94 

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

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

96 
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

97 
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

98 
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

99 
(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

100 
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

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

102 

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

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

104 

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

105 

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

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

107 

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

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

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

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

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

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

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

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

115 

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

116 
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

117 
"(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

118 

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

119 

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

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

121 

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

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

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

124 
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

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

126 
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

127 
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

128 
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

129 

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

130 
end 