author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63950  cdc1e59aa513 
permissions  rwrr 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

1 
(* Title: HOL/Library/Old_SMT/old_z3_interface.ML 
36898  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
Interface to Z3 based on a relaxed version of SMTLIB. 

5 
*) 

6 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

7 
signature OLD_Z3_INTERFACE = 
36898  8 
sig 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

9 
val smtlib_z3C: Old_SMT_Utils.class 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40681
diff
changeset

10 
val setup: theory > theory 
36898  11 

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

12 
datatype sym = Sym of string * sym list 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

13 
type mk_builtins = { 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

14 
mk_builtin_typ: sym > typ option, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

15 
mk_builtin_num: theory > int > typ > cterm option, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

16 
mk_builtin_fun: theory > sym > cterm list > cterm option } 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

17 
val add_mk_builtins: mk_builtins > Context.generic > Context.generic 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

18 
val mk_builtin_typ: Proof.context > sym > typ option 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

19 
val mk_builtin_num: Proof.context > int > typ > cterm option 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

20 
val mk_builtin_fun: Proof.context > sym > cterm list > cterm option 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

21 

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

22 
val is_builtin_theory_term: Proof.context > term > bool 
36898  23 
end 
24 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

25 
structure Old_Z3_Interface: OLD_Z3_INTERFACE = 
36898  26 
struct 
27 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

28 
val smtlib_z3C = Old_SMTLIB_Interface.smtlibC @ ["z3"] 
36898  29 

30 

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

31 

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

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

33 

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

34 
local 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

35 
fun translate_config ctxt = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

36 
let 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

37 
val {prefixes, header, is_fol, serialize, ...} = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

38 
Old_SMTLIB_Interface.translate_config ctxt 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

39 
in 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

40 
{prefixes=prefixes, header=header, is_fol=is_fol, serialize=serialize, 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

41 
has_datatypes=true} 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

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

43 

60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59634
diff
changeset

44 
fun is_div_mod @{const divide (int)} = true 
63950
cdc1e59aa513
syntactic type class for operation mod named after mod;
haftmann
parents:
60352
diff
changeset

45 
 is_div_mod @{const modulo (int)} = true 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

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

47 

41302
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

48 
val div_by_z3div = @{lemma 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

49 
"ALL k l. k div l = ( 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

50 
if k = 0  l = 0 then 0 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

51 
else if (0 < k & 0 < l)  (k < 0 & 0 < l) then z3div k l 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

52 
else z3div (k) (l))" 
58057  53 
by (simp add: z3div_def)} 
37151  54 

41302
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

55 
val mod_by_z3mod = @{lemma 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

56 
"ALL k l. k mod l = ( 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

57 
if l = 0 then k 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

58 
else if k = 0 then 0 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

59 
else if (0 < k & 0 < l)  (k < 0 & 0 < l) then z3mod k l 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

60 
else  z3mod (k) (l))" 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

61 
by (simp add: z3mod_def)} 
37151  62 

41302
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

63 
val have_int_div_mod = 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

64 
exists (Term.exists_subterm is_div_mod o Thm.prop_of) 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41127
diff
changeset

65 

41302
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

66 
fun add_div_mod _ (thms, extra_thms) = 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

67 
if have_int_div_mod thms orelse have_int_div_mod extra_thms then 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

68 
(thms, div_by_z3div :: mod_by_z3mod :: extra_thms) 
0485186839a7
reintroduced support for nonlinear multiplication in Z3 (overriding the builtin linear multiplication of the SMTLIB class of solvers)
boehmes
parents:
41280
diff
changeset

69 
else (thms, extra_thms) 
41072
9f9bc1bdacef
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset

70 

9f9bc1bdacef
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset

71 
val setup_builtins = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

72 
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const times (int)}, "*") #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

73 
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

74 
Old_SMT_Builtin.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod") 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

76 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

77 
val setup = Context.theory_map ( 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

78 
setup_builtins #> 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

79 
Old_SMT_Normalize.add_extra_norm (smtlib_z3C, add_div_mod) #> 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

80 
Old_SMT_Translate.add_config (smtlib_z3C, translate_config)) 
41072
9f9bc1bdacef
be more flexible: store SMT builtin symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset

81 

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

83 

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

84 

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

85 

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

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

87 

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

88 
datatype sym = Sym of string * sym list 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

89 

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

90 

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

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

92 

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

93 
type mk_builtins = { 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

94 
mk_builtin_typ: sym > typ option, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

95 
mk_builtin_num: theory > int > typ > cterm option, 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

96 
mk_builtin_fun: theory > sym > cterm list > cterm option } 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

97 

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

98 
fun chained _ [] = NONE 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

99 
 chained f (b :: bs) = (case f b of SOME y => SOME y  NONE => chained f bs) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

100 

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

101 
fun chained_mk_builtin_typ bs sym = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

102 
chained (fn {mk_builtin_typ=mk, ...} : mk_builtins => mk sym) bs 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

103 

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

104 
fun chained_mk_builtin_num ctxt bs i T = 
42361  105 
let val thy = Proof_Context.theory_of ctxt 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

106 
in chained (fn {mk_builtin_num=mk, ...} : mk_builtins => mk thy i T) bs end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

107 

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

108 
fun chained_mk_builtin_fun ctxt bs s cts = 
42361  109 
let val thy = Proof_Context.theory_of ctxt 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

110 
in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

111 

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

112 
fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2) 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40681
diff
changeset

113 

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

114 
structure Mk_Builtins = Generic_Data 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

116 
type T = (int * mk_builtins) list 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

117 
val empty = [] 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

118 
val extend = I 
41473  119 
fun merge data = Ord_List.merge fst_int_ord data 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

121 

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

122 
fun add_mk_builtins mk = 
39687  123 
Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk)) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

124 

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

125 
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt)) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

126 

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

127 

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

128 
(** basic and additional constructors **) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

129 

49720  130 
fun mk_builtin_typ _ (Sym ("Bool", _)) = SOME @{typ bool} 
40516  131 
 mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int} 
49720  132 
 mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool} (*FIXME: legacy*) 
133 
 mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int} (*FIXME: legacy*) 

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

134 
 mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

135 

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

136 
fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

137 
 mk_builtin_num ctxt i T = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

138 
chained_mk_builtin_num ctxt (get_mk_builtins ctxt) i T 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

139 

59634  140 
val mk_true = Thm.cterm_of @{context} (@{const Not} $ @{const False}) 
141 
val mk_false = Thm.cterm_of @{context} @{const False} 

142 
val mk_not = Thm.apply (Thm.cterm_of @{context} @{const Not}) 

143 
val mk_implies = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.implies}) 

144 
val mk_iff = Thm.mk_binop (Thm.cterm_of @{context} @{const HOL.eq (bool)}) 

145 
val conj = Thm.cterm_of @{context} @{const HOL.conj} 

146 
val disj = Thm.cterm_of @{context} @{const HOL.disj} 

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

147 

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

148 
fun mk_nary _ cu [] = cu 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

149 
 mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

150 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

151 
val eq = Old_SMT_Utils.mk_const_pat @{theory} @{const_name HOL.eq} Old_SMT_Utils.destT1 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

152 
fun mk_eq ct cu = Thm.mk_binop (Old_SMT_Utils.instT' ct eq) ct cu 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

153 

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

154 
val if_term = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

155 
Old_SMT_Utils.mk_const_pat @{theory} @{const_name If} 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

156 
(Old_SMT_Utils.destT1 o Old_SMT_Utils.destT2) 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41473
diff
changeset

157 
fun mk_if cc ct cu = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

158 
Thm.mk_binop (Thm.apply (Old_SMT_Utils.instT' ct if_term) cc) ct cu 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

159 

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

160 
val nil_term = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

161 
Old_SMT_Utils.mk_const_pat @{theory} @{const_name Nil} Old_SMT_Utils.destT1 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41473
diff
changeset

162 
val cons_term = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

163 
Old_SMT_Utils.mk_const_pat @{theory} @{const_name Cons} Old_SMT_Utils.destT1 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

164 
fun mk_list cT cts = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

165 
fold_rev (Thm.mk_binop (Old_SMT_Utils.instT cT cons_term)) cts 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

166 
(Old_SMT_Utils.instT cT nil_term) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

167 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

168 
val distinct = Old_SMT_Utils.mk_const_pat @{theory} @{const_name distinct} 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

169 
(Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

170 
fun mk_distinct [] = mk_true 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

171 
 mk_distinct (cts as (ct :: _)) = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

172 
Thm.apply (Old_SMT_Utils.instT' ct distinct) 
59586  173 
(mk_list (Thm.ctyp_of_cterm ct) cts) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

174 

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

175 
val access = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

176 
Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} Old_SMT_Utils.destT1 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

177 
fun mk_access array = Thm.apply (Old_SMT_Utils.instT' array access) array 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

178 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

179 
val update = Old_SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd} 
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

180 
(Thm.dest_ctyp o Old_SMT_Utils.destT1) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

181 
fun mk_update array index value = 
59586  182 
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array) 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41473
diff
changeset

183 
in 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

184 
Thm.apply (Thm.mk_binop (Old_SMT_Utils.instTs cTs update) array index) value 
41691
8f0531cf34f8
avoid ML structure aliases (especially singleletter abbreviations)
boehmes
parents:
41473
diff
changeset

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

186 

59634  187 
val mk_uminus = Thm.apply (Thm.cterm_of @{context} @{const uminus (int)}) 
188 
val add = Thm.cterm_of @{context} @{const plus (int)} 

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

189 
val int0 = Numeral.mk_cnumber @{ctyp int} 0 
59634  190 
val mk_sub = Thm.mk_binop (Thm.cterm_of @{context} @{const minus (int)}) 
191 
val mk_mul = Thm.mk_binop (Thm.cterm_of @{context} @{const times (int)}) 

192 
val mk_div = Thm.mk_binop (Thm.cterm_of @{context} @{const z3div}) 

193 
val mk_mod = Thm.mk_binop (Thm.cterm_of @{context} @{const z3mod}) 

194 
val mk_lt = Thm.mk_binop (Thm.cterm_of @{context} @{const less (int)}) 

195 
val mk_le = Thm.mk_binop (Thm.cterm_of @{context} @{const less_eq (int)}) 

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

196 

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

197 
fun mk_builtin_fun ctxt sym cts = 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

198 
(case (sym, cts) of 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

199 
(Sym ("true", _), []) => SOME mk_true 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

200 
 (Sym ("false", _), []) => SOME mk_false 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

201 
 (Sym ("not", _), [ct]) => SOME (mk_not ct) 
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

202 
 (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts) 
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

203 
 (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

204 
 (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

205 
 (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

206 
 (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

207 
 (Sym ("xor", _), [ct, cu]) => SOME (mk_not (mk_iff ct cu)) 
41761
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41691
diff
changeset

208 
 (Sym ("if", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) 
2dc75bae5226
more explicit errors to inform users about problems related to SMT solvers;
boehmes
parents:
41691
diff
changeset

209 
 (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

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

211 
 (Sym ("distinct", _), _) => SOME (mk_distinct cts) 
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:
42361
diff
changeset

212 
 (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

213 
 (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

214 
 _ => 
59586  215 
(case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of 
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

216 
(Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

217 
 (Sym ("", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

218 
 (Sym ("", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

219 
 (Sym ("*", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mul ct cu) 
37151  220 
 (Sym ("div", _), SOME @{typ int}, [ct, cu]) => SOME (mk_div ct cu) 
221 
 (Sym ("mod", _), SOME @{typ int}, [ct, cu]) => SOME (mk_mod ct cu) 

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

222 
 (Sym ("<", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

223 
 (Sym ("<=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le ct cu) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

224 
 (Sym (">", _), SOME @{typ int}, [ct, cu]) => SOME (mk_lt cu ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

225 
 (Sym (">=", _), SOME @{typ int}, [ct, cu]) => SOME (mk_le cu ct) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

226 
 _ => chained_mk_builtin_fun ctxt (get_mk_builtins ctxt) sym cts)) 
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

227 

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

228 

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

229 

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

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

231 

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

232 
fun is_builtin_theory_term ctxt t = 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

233 
if Old_SMT_Builtin.is_builtin_num ctxt t then true 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40681
diff
changeset

234 
else 
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40681
diff
changeset

235 
(case Term.strip_comb t of 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

236 
(Const c, ts) => Old_SMT_Builtin.is_builtin_fun ctxt c ts 
41059
d2b1fc1b8e19
centralized handling of builtin types and constants;
boehmes
parents:
40681
diff
changeset

237 
 _ => false) 
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset

238 

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

239 
end 