author  boehmes 
Mon, 06 Dec 2010 16:54:22 +0100  
changeset 41058  42e0a0bfef73 
parent 40840  2f97215e79bf 
child 41122  72176ec5e031 
permissions  rwrr 
36898  1 
(* Title: HOL/Tools/SMT/z3_model.ML 
2 
Author: Sascha Boehme and Philipp Meyer, TU Muenchen 

3 

4 
Parser for counterexamples generated by Z3. 

5 
*) 

6 

7 
signature Z3_MODEL = 

8 
sig 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

9 
val parse_counterex: Proof.context > SMT_Translate.recon > string list > 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

10 
term list * term list 
36898  11 
end 
12 

13 
structure Z3_Model: Z3_MODEL = 

14 
struct 

15 

40663  16 
structure U = SMT_Utils 
17 

18 

36898  19 
(* counterexample expressions *) 
20 

21 
datatype expr = True  False  Number of int * int option  Value of int  

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

22 
Array of array  App of string * expr list 
36898  23 
and array = Fresh of expr  Store of (array * expr) * expr 
24 

25 

26 
(* parsing *) 

27 

28 
val space = Scan.many Symbol.is_ascii_blank 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

29 
fun spaced p = p  space 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

30 
fun in_parens p = spaced (Scan.$$ "(")  p  spaced (Scan.$$ ")") 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

31 
fun in_braces p = spaced (Scan.$$ "{")  p  spaced (Scan.$$ "}") 
36898  32 

33 
val digit = (fn 

34 
"0" => SOME 0  "1" => SOME 1  "2" => SOME 2  "3" => SOME 3  

35 
"4" => SOME 4  "5" => SOME 5  "6" => SOME 6  "7" => SOME 7  

36 
"8" => SOME 8  "9" => SOME 9  _ => NONE) 

37 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

38 
val nat_num = spaced (Scan.repeat1 (Scan.some digit) >> 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

39 
(fn ds => fold (fn d => fn i => i * 10 + d) ds 0)) 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

40 
val int_num = spaced (Scan.optional ($$ "" >> K (fn i => ~i)) I : 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

41 
(fn sign => nat_num >> sign)) 
36898  42 

43 
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf 

40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40579
diff
changeset

44 
member (op =) (raw_explode "_+*/%~=<>$&?!.@^#") 
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

45 
val name = spaced (Scan.many1 is_char >> implode) 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

46 

c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

47 
fun $$$ s = spaced (Scan.this_string s) 
36898  48 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

49 
fun array_expr st = st > in_parens ( 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

50 
$$$ "const"  expr >> Fresh  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

51 
$$$ "store"  array_expr  expr  expr >> Store) 
36898  52 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

53 
and expr st = st > ( 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

54 
$$$ "true" >> K True  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

55 
$$$ "false" >> K False  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

56 
int_num  Scan.option ($$$ "/"  int_num) >> Number  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

57 
$$$ "val!"  nat_num >> Value  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

58 
name >> (App o rpair [])  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

59 
array_expr >> Array  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

60 
in_parens (name  Scan.repeat1 expr) >> App) 
36898  61 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

62 
fun args st = ($$$ ">" >> K []  expr ::: args) st 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

63 
val args_case = args  expr 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

64 
val else_case = $$$ "else"  $$$ ">"  expr >> pair ([] : expr list) 
36898  65 

66 
val func = 

67 
let fun cases st = (else_case >> single  args_case ::: cases) st 

68 
in in_braces cases end 

69 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

70 
val cex = space  
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

71 
Scan.repeat (name  $$$ ">"  (func  expr >> (single o pair []))) 
36898  72 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

73 
fun resolve terms ((n, k), cases) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

74 
(case Symtab.lookup terms n of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

75 
NONE => NONE 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

76 
 SOME t => SOME ((t, k), cases)) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

77 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

78 
fun annotate _ (_, []) = NONE 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

79 
 annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, [])) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

80 
 annotate _ (_, [_]) = NONE 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

81 
 annotate terms (n, cases as (args, _) :: _) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

82 
let val (cases', (_, else_case)) = split_last cases 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

83 
in resolve terms ((n, length args), (else_case, cases')) end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

84 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

85 
fun read_cex terms ls = 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40579
diff
changeset

86 
maps (cons "\n" o raw_explode) ls 
36898  87 
> try (fst o Scan.finite Symbol.stopper cex) 
88 
> the_default [] 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

89 
> map_filter (annotate terms) 
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

90 

c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

91 

36898  92 
(* translation into terms *) 
93 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

94 
fun max_value vs = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

95 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

96 
fun max_val_expr (Value i) = Integer.max i 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

97 
 max_val_expr (App (_, es)) = fold max_val_expr es 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

98 
 max_val_expr (Array a) = max_val_array a 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

99 
 max_val_expr _ = I 
36898  100 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

101 
and max_val_array (Fresh e) = max_val_expr e 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

102 
 max_val_array (Store ((a, e1), e2)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

103 
max_val_array a #> max_val_expr e1 #> max_val_expr e2 
36898  104 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

105 
fun max_val (_, (ec, cs)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

106 
max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

107 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

108 
in fold max_val vs ~1 end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

109 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

110 
fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1)) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

111 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

112 
fun get_term n T es (cx as (terms, next_val)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

113 
(case Symtab.lookup terms n of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

114 
SOME t => ((t, es), cx) 
36898  115 
 NONE => 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

116 
let val t = Var (("skolem", next_val), T) 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

117 
in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end) 
36898  118 

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:
40551
diff
changeset

119 
fun trans_expr _ True = pair @{const True} 
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:
40551
diff
changeset

120 
 trans_expr _ False = pair @{const False} 
36898  121 
 trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i) 
122 
 trans_expr T (Number (i, SOME j)) = 

123 
pair (Const (@{const_name divide}, [T, T] > T) $ 

124 
HOLogic.mk_number T i $ HOLogic.mk_number T j) 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

125 
 trans_expr T (Value i) = pair (Var (("value", i), T)) 
36898  126 
 trans_expr T (Array a) = trans_array T a 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

127 
 trans_expr T (App (n, es)) = get_term n T es #> (fn (t, es') => 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

128 
let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t)) 
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

129 
in 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

130 
fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

131 
end) 
36898  132 

133 
and trans_array T a = 

40840  134 
let val (dT, rT) = Term.dest_funT T 
36898  135 
in 
136 
(case a of 

137 
Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t)) 

138 
 Store ((a', e1), e2) => 

139 
trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>> 

140 
(fn ((m, k), v) => 

141 
Const (@{const_name fun_upd}, [T, dT, rT] > T) $ m $ k $ v)) 

142 
end 

143 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

144 
fun trans_pattern T ([], e) = trans_expr T e #>> pair [] 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

145 
 trans_pattern T (arg :: args, e) = 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

146 
trans_expr (Term.domain_type T) arg ##>> 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

147 
trans_pattern (Term.range_type T) (args, e) #>> 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

148 
(fn (arg', (args', e')) => (arg' :: args', e')) 
36898  149 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

150 
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T > U, T, U, T] > U) 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

151 

c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

152 
fun mk_update ([], u) _ = u 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

153 
 mk_update ([t], u) f = 
40840  154 
uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u 
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

155 
 mk_update (t :: ts, u) f = 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

156 
let 
40840  157 
val (dT, rT) = Term.dest_funT (Term.fastype_of f) 
158 
val (dT', rT') = Term.dest_funT rT 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

159 
in 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

160 
mk_fun_upd dT rT $ f $ t $ 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

161 
mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT'))) 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

162 
end 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

163 

c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

164 
fun mk_lambda Ts (t, pats) = 
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

165 
fold_rev (curry Term.absdummy) Ts t > fold mk_update pats 
36898  166 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

167 
fun translate ((t, k), (e, cs)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

168 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

169 
val T = Term.fastype_of t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

170 
val (Us, U) = U.dest_funT k (Term.fastype_of t) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

171 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

172 
fun mk_full_def u' pats = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

173 
pats 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

174 
> filter_out (fn (_, u) => u aconv u') 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

175 
> HOLogic.mk_eq o pair t o mk_lambda Us o pair u' 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

176 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

177 
fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

178 
fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')] 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

179 
 mk_eqs _ pats = map mk_eq pats 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

180 
in 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

181 
trans_expr U e ##>> 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

182 
(if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>> 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

183 
(fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats)) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

184 
end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

185 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

186 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

187 
(* normalization *) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

188 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

189 
fun partition_eqs f = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

190 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

191 
fun part t (xs, ts) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

192 
(case try HOLogic.dest_eq t of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

193 
SOME (l, r) => (case f l r of SOME x => (x::xs, ts)  _ => (xs, t::ts)) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

194 
 NONE => (xs, t :: ts)) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

195 
in (fn ts => fold part ts ([], [])) end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

196 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

197 
fun replace_vars tab = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

198 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

199 
fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

200 
 replace t = t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

201 
in map (Term.map_aterms replace) end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

202 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

203 
fun remove_int_nat_coercions (eqs, defs) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

204 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

205 
fun mk_nat_num t i = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

206 
(case try HOLogic.dest_number i of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

207 
SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

208 
 NONE => NONE) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

209 
fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

210 
 nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

211 
 nat_of _ _ = NONE 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

212 
val (nats, eqs') = partition_eqs nat_of eqs 
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

213 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

214 
fun is_coercion t = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

215 
(case try HOLogic.dest_eq t of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

216 
SOME (@{const of_nat (int)}, _) => true 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

217 
 SOME (@{const nat}, _) => true 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

218 
 _ => false) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

219 
in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

220 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

221 
fun unfold_funapp (eqs, defs) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

222 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

223 
fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

224 
 unfold_app t = t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

225 
fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

226 
eq $ unfold_app t $ u 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

227 
 unfold_eq t = t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

228 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

229 
fun is_fun_app t = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

230 
(case try HOLogic.dest_eq t of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

231 
SOME (Const (@{const_name SMT.fun_app}, _), _) => true 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

232 
 _ => false) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

233 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

234 
in (map unfold_eq eqs, filter_out is_fun_app defs) end 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

235 

41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

236 
fun unfold_eqs (eqs, defs) = 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

237 
let 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

238 
val is_ground = not o Term.exists_subterm (fn Var _ => true  _ => false) 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

239 
fun add_rewr l (r as Var _) = if is_ground l then SOME (r, l) else NONE 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

240 
 add_rewr _ _ = NONE 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

241 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

242 
fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

243 
 is_trivial _ = false 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

244 

42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

245 
fun replace rs = replace_vars rs #> filter_out is_trivial 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

246 

42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

247 
fun unfold (es, ds) = 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

248 
(case partition_eqs add_rewr es of 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

249 
([], _) => (es, ds) 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

250 
 (rs, es') => unfold (pairself (replace rs) (es', ds))) 
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

251 

42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

252 
in unfold (eqs, defs) end 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

253 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

254 
fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

255 
eq $ u $ t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

256 
 swap_free t = t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

257 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

258 
fun frees_for_vars ctxt (eqs, defs) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

259 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

260 
fun fresh_free i T (cx as (frees, ctxt)) = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

261 
(case Inttab.lookup frees i of 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

262 
SOME t => (t, cx) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

263 
 NONE => 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

264 
let 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

265 
val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

266 
val t = Free (n, T) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

267 
in (t, (Inttab.update (i, t) frees, ctxt')) end) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

268 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

269 
fun repl_var (Var ((_, i), T)) = fresh_free i T 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

270 
 repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $ 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

271 
 repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t')) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

272 
 repl_var t = pair t 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

273 
in 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

274 
(Inttab.empty, ctxt) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

275 
> fold_map repl_var eqs 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

276 
>> fold_map repl_var defs 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

277 
> fst 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

278 
end 
36898  279 

280 

281 
(* overall procedure *) 

282 

40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

283 
val is_free_constraint = Term.exists_subterm (fn Free _ => true  _ => false) 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

284 

47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

285 
fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

286 
 is_const_def _ = false 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

287 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

288 
fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls = 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

289 
read_cex terms ls 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

290 
> with_context terms translate 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

291 
> apfst flat o split_list 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

292 
> remove_int_nat_coercions 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

293 
> unfold_funapp 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

294 
> unfold_eqs 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

295 
>> map swap_free 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

296 
>> filter is_free_constraint 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

297 
> frees_for_vars ctxt 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

298 
> filter is_const_def 
36898  299 

300 
end 

39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset

301 