author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 59058  a78612c67ec0 
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_model.ML 
36898  2 
Author: Sascha Boehme and Philipp Meyer, TU Muenchen 
3 

4 
Parser for counterexamples generated by Z3. 

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_MODEL = 
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 parse_counterex: Proof.context > Old_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 

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

13 
structure Old_Z3_Model: OLD_Z3_MODEL = 
36898  14 
struct 
15 

40663  16 

36898  17 
(* counterexample expressions *) 
18 

19 
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

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

23 

24 
(* parsing *) 

25 

26 
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

27 
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

28 
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

29 
fun in_braces p = spaced (Scan.$$ "{")  p  spaced (Scan.$$ "}") 
36898  30 

31 
val digit = (fn 

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

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

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

35 

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

36 
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

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

38 
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

39 
(fn sign => nat_num >> sign)) 
36898  40 

41 
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

42 
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

43 
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

44 

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 
fun $$$ s = spaced (Scan.this_string s) 
36898  46 

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

47 
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

48 
$$$ "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

49 
$$$ "store"  array_expr  expr  expr >> Store) 
36898  50 

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

51 
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

52 
$$$ "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

53 
$$$ "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

54 
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

55 
$$$ "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

56 
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

57 
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

58 
in_parens (name  Scan.repeat1 expr) >> App) 
36898  59 

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

60 
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

61 
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

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

64 
val func = 

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

66 
in in_braces cases end 

67 

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

68 
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

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

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

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

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

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

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

75 

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

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

77 
 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

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

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

80 
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

81 
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

82 

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

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

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

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

87 
> 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

88 

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

89 

36898  90 
(* translation into terms *) 
91 

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

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

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

94 
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

95 
 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

96 
 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

97 
 max_val_expr _ = I 
36898  98 

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

99 
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

100 
 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

101 
max_val_array a #> max_val_expr e1 #> max_val_expr e2 
36898  102 

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

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

104 
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

105 

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

106 
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

107 

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

108 
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

109 

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

110 
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

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

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

114 
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

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

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

117 
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

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

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

122 
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

123 
 trans_expr T (Value i) = pair (Var (("value", i), T)) 
36898  124 
 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

125 
 trans_expr T (App (n, es)) = get_term n T es #> (fn (t, es') => 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

126 
let val Ts = fst (Old_SMT_Utils.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

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

128 
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

129 
end) 
36898  130 

131 
and trans_array T a = 

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

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

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

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

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

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

140 
end 

141 

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

142 
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

143 
 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

144 
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

145 
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

146 
(fn (arg', (args', e')) => (arg' :: args', e')) 
36898  147 

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

148 
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

149 

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_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

151 
 mk_update ([t], u) f = 
40840  152 
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

153 
 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

154 
let 
40840  155 
val (dT, rT) = Term.dest_funT (Term.fastype_of f) 
156 
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

157 
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

158 
mk_fun_upd dT rT $ f $ t $ 
44241  159 
mk_update (ts, u) (absdummy dT' (Const ("_", 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

160 
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

161 

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 
fun mk_lambda Ts (t, pats) = 
44241  163 
fold_rev absdummy Ts t > fold mk_update pats 
36898  164 

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

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

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

167 
val T = Term.fastype_of t 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

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

169 

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

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

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

172 
> 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

173 
> 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

174 

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

175 
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

176 
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

177 
 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

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

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

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

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

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

183 

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

184 

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

185 
(* normalization *) 
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 
fun partition_eqs f = 
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

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

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

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

191 
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

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

193 
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

194 

41122
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

195 
fun first_eq pred = 
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

196 
let 
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

197 
fun part _ [] = NONE 
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

198 
 part us (t :: ts) = 
41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

199 
(case try (pred o HOLogic.dest_eq) t of 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

200 
SOME (SOME lr) => SOME (lr, fold cons us ts) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

201 
 _ => part (t :: us) ts) 
41122
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

202 
in (fn ts => part [] ts) end 
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

203 

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

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

205 
let 
41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

206 
fun repl v = the_default v (AList.lookup (op aconv) tab v) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

207 
fun replace (v as Var _) = repl v 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

208 
 replace (v as Free _) = repl v 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

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

210 
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

211 

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

212 
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

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

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

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

216 
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

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

218 
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

219 
 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

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

221 
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

222 

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

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

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

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

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

227 
 _ => false) 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58058
diff
changeset

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

229 

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

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

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

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

234 
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

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

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

237 

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

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

239 
(case try HOLogic.dest_eq t of 
58057  240 
SOME (Const (@{const_name fun_app}, _), _) => true 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

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

242 

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

243 
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

244 

41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

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

246 
let 
41122
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

247 
val is_ground = not o Term.exists_subterm Term.is_Var 
41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

248 
fun is_non_rec (v, t) = not (Term.exists_subterm (equal v) t) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

249 

80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

250 
fun rewr_var (l as Var _, r) = if is_ground r then SOME (l, r) else NONE 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

251 
 rewr_var (r, l as Var _) = if is_ground r then SOME (l, r) else NONE 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

252 
 rewr_var _ = NONE 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

253 

80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

254 
fun rewr_free' e = if is_non_rec e then SOME e else NONE 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

255 
fun rewr_free (e as (Free _, _)) = rewr_free' e 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

256 
 rewr_free (e as (_, Free _)) = rewr_free' (swap e) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

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

258 

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

259 
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

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

261 

41122
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

262 
fun replace r = replace_vars [r] #> filter_out is_trivial 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

263 

41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

264 
fun unfold_vars (es, ds) = 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

265 
(case first_eq rewr_var es of 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58058
diff
changeset

266 
SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds)) 
41122
72176ec5e031
rewrite Z3 model equations onebyone (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset

267 
 NONE => (es, ds)) 
41058
42e0a0bfef73
more aggressive unfolding of unknowns in Z3 models
boehmes
parents:
40840
diff
changeset

268 

41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

269 
fun unfold_frees ues (es, ds) = 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

270 
(case first_eq rewr_free es of 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

271 
SOME (lr, es') => 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58058
diff
changeset

272 
apply2 (replace lr) (es', ds) 
41570
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

273 
> unfold_frees (HOLogic.mk_eq lr :: replace lr ues) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

274 
 NONE => (ues @ es, ds)) 
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

275 

80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset

276 
in unfold_vars #> unfold_frees [] end 
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset

277 

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

278 
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

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

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

281 

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

282 
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

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

284 
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

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

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

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

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

289 
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

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

291 
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

292 

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

293 
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

294 
 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

295 
 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

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

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

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

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

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

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

302 
end 
36898  303 

304 

305 
(* overall procedure *) 

306 

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

307 
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

308 

41129
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

309 
fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

310 
 is_free_def _ = false 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

311 

b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

312 
fun defined tp = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58058
diff
changeset

313 
try (apply2 (fst o HOLogic.dest_eq)) tp 
41129
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

314 
> the_default false o Option.map (op aconv) 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

315 

b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

316 
fun add_free_defs free_cs defs = 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

317 
let val (free_defs, defs') = List.partition is_free_def defs 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

318 
in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end 
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

319 

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

320 
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

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

322 

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

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

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

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

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

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

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

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

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

331 
>> filter is_free_constraint 
41129
b88cfc0f7456
also show function definitions for higherorder free variables in Z3 models
boehmes
parents:
41122
diff
changeset

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

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

334 
> filter is_const_def 
36898  335 

336 
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

337 