author | boehmes |
Sat, 15 Jan 2011 13:48:45 +0100 | |
changeset 41570 | 80c7622a7ff3 |
parent 41328 | 6792a5c92a58 |
child 44241 | 7943b69f0188 |
permissions | -rw-r--r-- |
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 |
|
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') => |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41129
diff
changeset
|
126 |
let val Ts = fst (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 $ |
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 |
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
|
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) = |
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 |
fold_rev (curry Term.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 |
41328
6792a5c92a58
avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents:
41129
diff
changeset
|
168 |
val (Us, U) = 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 one-by-one (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset
|
195 |
fun first_eq pred = |
72176ec5e031
rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset
|
196 |
let |
72176ec5e031
rewrite Z3 model equations one-by-one (the previous approach led to loss of information)
boehmes
parents:
41058
diff
changeset
|
197 |
fun part _ [] = NONE |
72176ec5e031
rewrite Z3 model equations one-by-one (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 one-by-one (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 one-by-one (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) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
228 |
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
|
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 |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
232 |
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
|
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 |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
240 |
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
|
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 one-by-one (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 one-by-one (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 |
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset
|
266 |
SOME (lr, es') => unfold_vars (pairself (replace lr) (es', ds)) |
41122
72176ec5e031
rewrite Z3 model equations one-by-one (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') => |
80c7622a7ff3
normalize Z3 models: assignments to free variables should ideally not refer to other free variables
boehmes
parents:
41328
diff
changeset
|
272 |
pairself (replace lr) (es', ds) |
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 higher-order 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 higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
310 |
| is_free_def _ = false |
b88cfc0f7456
also show function definitions for higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
311 |
|
b88cfc0f7456
also show function definitions for higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
312 |
fun defined tp = |
b88cfc0f7456
also show function definitions for higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
313 |
try (pairself (fst o HOLogic.dest_eq)) tp |
b88cfc0f7456
also show function definitions for higher-order 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 higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
315 |
|
b88cfc0f7456
also show function definitions for higher-order free variables in Z3 models
boehmes
parents:
41122
diff
changeset
|
316 |
fun add_free_defs free_cs defs = |
b88cfc0f7456
also show function definitions for higher-order 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 higher-order 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 higher-order 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 |
|
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
|
323 |
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
|
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 higher-order 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 |